GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/logic_info.h Lines: 23 23 100.0 %
Date: 2021-03-23 Branches: 15 18 83.3 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file logic_info.h
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Morgan Deters, Andrew Reynolds, Tim King
6
 ** This file is part of the CVC4 project.
7
 ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
8
 ** in the top-level source directory and their institutional affiliations.
9
 ** All rights reserved.  See the file COPYING in the top-level source
10
 ** directory for licensing information.\endverbatim
11
 **
12
 ** \brief A class giving information about a logic (group a theory modules
13
 ** and configuration information)
14
 **
15
 ** A class giving information about a logic (group of theory modules and
16
 ** configuration information).
17
 **/
18
19
#include "cvc4_public.h"
20
21
#ifndef CVC4__LOGIC_INFO_H
22
#define CVC4__LOGIC_INFO_H
23
24
#include <string>
25
#include <vector>
26
27
#include "cvc4_export.h"
28
#include "theory/theory_id.h"
29
30
namespace CVC4 {
31
32
/**
33
 * A LogicInfo instance describes a collection of theory modules and some
34
 * basic configuration about them.  Conceptually, it provides a background
35
 * context for all operations in CVC4.  Typically, when CVC4's SmtEngine
36
 * is created, it is issued a setLogic() command indicating features of the
37
 * assertions and queries to follow---for example, whether quantifiers are
38
 * used, whether integers or reals (or both) will be used, etc.
39
 *
40
 * Most places in CVC4 will only ever need to access a const reference to an
41
 * instance of this class.  Such an instance is generally set by the SmtEngine
42
 * when setLogic() is called.  However, mutating member functions are also
43
 * provided by this class so that it can be used as a more general mechanism
44
 * (e.g., for communicating to the SmtEngine which theories should be used,
45
 * rather than having to provide an SMT-LIB string).
46
 */
47
443168
class CVC4_EXPORT LogicInfo
48
{
49
  mutable std::string d_logicString; /**< an SMT-LIB-like logic string */
50
  std::vector<bool> d_theories; /**< set of active theories */
51
  size_t d_sharingTheories; /**< count of theories that need sharing */
52
53
  /** are integers used in this logic? */
54
  bool d_integers;
55
  /** are reals used in this logic? */
56
  bool d_reals;
57
  /** transcendentals in this logic? */
58
  bool d_transcendentals;
59
  /** linear-only arithmetic in this logic? */
60
  bool d_linear;
61
  /** difference-only arithmetic in this logic? */
62
  bool d_differenceLogic;
63
  /** cardinality constraints in this logic? */
64
  bool d_cardinalityConstraints;
65
  /** higher-order constraints in this logic? */
66
  bool d_higherOrder;
67
68
  bool d_locked; /**< is this LogicInfo instance locked (and thus immutable)? */
69
70
  /**
71
   * Returns true iff this is a "true" theory (one that must be worried
72
   * about for sharing
73
   */
74
741743
  static inline bool isTrueTheory(theory::TheoryId theory) {
75
741743
    switch(theory) {
76
201167
    case theory::THEORY_BUILTIN:
77
    case theory::THEORY_BOOL:
78
    case theory::THEORY_QUANTIFIERS:
79
201167
      return false;
80
540576
    default:
81
540576
      return true;
82
    }
83
  }
84
85
public:
86
87
  /**
88
   * Constructs a LogicInfo for the most general logic (quantifiers, all
89
   * background theory modules, ...).
90
   */
91
  LogicInfo();
92
93
  /**
94
   * Construct a LogicInfo from an SMT-LIB-like logic string.
95
   * Throws an IllegalArgumentException if the logic string cannot
96
   * be interpreted.
97
   */
98
  LogicInfo(std::string logicString);
99
100
  /**
101
   * Construct a LogicInfo from an SMT-LIB-like logic string.
102
   * Throws an IllegalArgumentException if the logic string cannot
103
   * be interpreted.
104
   */
105
  LogicInfo(const char* logicString);
106
107
  // ACCESSORS
108
109
  /**
110
   * Get an SMT-LIB-like logic string.  These are only guaranteed to
111
   * be SMT-LIB-compliant if an SMT-LIB-compliant string was used in
112
   * the constructor and no mutating functions were called.
113
   */
114
  std::string getLogicString() const;
115
116
  /** Is sharing enabled for this logic? */
117
  bool isSharingEnabled() const;
118
119
  /** Is the given theory module active in this logic? */
120
  bool isTheoryEnabled(theory::TheoryId theory) const;
121
122
  /** Is this a quantified logic? */
123
  bool isQuantified() const;
124
125
  /** Is this the all-inclusive logic? */
126
  bool hasEverything() const;
127
128
  /** Is this the all-exclusive logic?  (Here, that means propositional logic) */
129
  bool hasNothing() const;
130
131
  /**
132
   * Is this a pure logic (only one "true" background theory).  Quantifiers
133
   * can exist in such logics though; to test for quantifier-free purity,
134
   * use "isPure(theory) && !isQuantified()".
135
   */
136
  bool isPure(theory::TheoryId theory) const;
137
138
  // these are for arithmetic
139
140
  /** Are integers in this logic? */
141
  bool areIntegersUsed() const;
142
143
  /** Are reals in this logic? */
144
  bool areRealsUsed() const;
145
146
  /** Are transcendentals in this logic? */
147
  bool areTranscendentalsUsed() const;
148
149
  /** Does this logic only linear arithmetic? */
150
  bool isLinear() const;
151
152
  /** Does this logic only permit difference reasoning? (implies linear) */
153
  bool isDifferenceLogic() const;
154
155
  /** Does this logic allow cardinality constraints? */
156
  bool hasCardinalityConstraints() const;
157
158
  /** Is this a higher order logic? */
159
  bool isHigherOrder() const;
160
161
  // MUTATORS
162
163
  /**
164
   * Initialize the LogicInfo with an SMT-LIB-like logic string.
165
   * Throws an IllegalArgumentException if the string can't be
166
   * interpreted.
167
   */
168
  void setLogicString(std::string logicString);
169
170
  /**
171
   * Enable all functionality.  All theories, plus quantifiers, will be
172
   * enabled.
173
   */
174
  void enableEverything();
175
176
  /**
177
   * Disable all functionality.  The result will be a LogicInfo with
178
   * the BUILTIN and BOOLEAN theories enabled only ("QF_SAT").
179
   */
180
  void disableEverything();
181
182
  /**
183
   * Enable the given theory module.
184
   */
185
  void enableTheory(theory::TheoryId theory);
186
187
  /**
188
   * Disable the given theory module.  THEORY_BUILTIN and THEORY_BOOL cannot
189
   * be disabled (and if given here, the request will be silently ignored).
190
   */
191
  void disableTheory(theory::TheoryId theory);
192
193
  /**
194
   * Quantifiers are a special case, since two theory modules handle them.
195
   */
196
6928
  void enableQuantifiers() {
197
6928
    enableTheory(theory::THEORY_QUANTIFIERS);
198
6928
  }
199
200
  /**
201
   * Quantifiers are a special case, since two theory modules handle them.
202
   */
203
19038
  void disableQuantifiers() {
204
19038
    disableTheory(theory::THEORY_QUANTIFIERS);
205
19036
  }
206
207
  /**
208
   * Enable everything that is needed for sygus with respect to this logic info.
209
   * This means enabling quantifiers, datatypes, UF, integers, and higher order.
210
   */
211
  void enableSygus();
212
  /**
213
   * Enable everything that is needed for separation logic. This means enabling
214
   * the theories of separation logic, UF and sets.
215
   */
216
  void enableSeparationLogic();
217
218
  // these are for arithmetic
219
220
  /** Enable the use of integers in this logic. */
221
  void enableIntegers();
222
  /** Disable the use of integers in this logic. */
223
  void disableIntegers();
224
  /** Enable the use of reals in this logic. */
225
  void enableReals();
226
  /** Disable the use of reals in this logic. */
227
  void disableReals();
228
  /** Enable the use of transcendentals in this logic. */
229
  void arithTranscendentals();
230
  /** Only permit difference arithmetic in this logic. */
231
  void arithOnlyDifference();
232
  /** Only permit linear arithmetic in this logic. */
233
  void arithOnlyLinear();
234
  /** Permit nonlinear arithmetic in this logic. */
235
  void arithNonLinear();
236
237
  // for cardinality constraints
238
239
  /** Enable the use of cardinality constraints in this logic. */
240
  void enableCardinalityConstraints();
241
  /** Disable the use of cardinality constraints in this logic. */
242
  void disableCardinalityConstraints();
243
244
  // for higher-order
245
246
  /** Enable the use of higher-order in this logic. */
247
  void enableHigherOrder();
248
  /** Disable the use of higher-order in this logic. */
249
  void disableHigherOrder();
250
251
  // LOCKING FUNCTIONALITY
252
253
  /** Lock this LogicInfo, disabling further mutation and allowing queries */
254
68812
  void lock() { d_locked = true; }
255
  /** Check whether this LogicInfo is locked, disallowing further mutation */
256
116342
  bool isLocked() const { return d_locked; }
257
  /** Get a copy of this LogicInfo that is identical, but unlocked */
258
  LogicInfo getUnlockedCopy() const;
259
260
  // COMPARISON
261
262
  /** Are these two LogicInfos equal? */
263
  bool operator==(const LogicInfo& other) const;
264
265
  /** Are these two LogicInfos disequal? */
266
3416
  bool operator!=(const LogicInfo& other) const {
267
3416
    return !(*this == other);
268
  }
269
270
  /** Is this LogicInfo "greater than" (does it contain everything and more) the other? */
271
2348
  bool operator>(const LogicInfo& other) const {
272
2348
    return *this >= other && *this != other;
273
  }
274
275
  /** Is this LogicInfo "less than" (does it contain strictly less) the other? */
276
2348
  bool operator<(const LogicInfo& other) const {
277
2348
    return *this <= other && *this != other;
278
  }
279
  /** Is this LogicInfo "less than or equal" the other? */
280
  bool operator<=(const LogicInfo& other) const;
281
282
  /** Is this LogicInfo "greater than or equal" the other? */
283
  bool operator>=(const LogicInfo& other) const;
284
285
  /** Are two LogicInfos comparable?  That is, is one of <= or > true? */
286
2348
  bool isComparableTo(const LogicInfo& other) const {
287
2348
    return *this <= other || *this >= other;
288
  }
289
290
}; /* class LogicInfo */
291
292
std::ostream& operator<<(std::ostream& out, const LogicInfo& logic);
293
294
}/* CVC4 namespace */
295
296
#endif /* CVC4__LOGIC_INFO_H */