cvc4-1.4
logic_info.h
Go to the documentation of this file.
1 /********************* */
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 #include "expr/kind.h"
27 
28 namespace CVC4 {
29 
46  mutable std::string d_logicString;
47  std::vector<bool> d_theories;
48  size_t d_sharingTheories;
50  // for arithmetic
51  bool d_integers;
52  bool d_reals;
53  bool d_linear;
54  bool d_differenceLogic;
55  bool d_cardinalityConstraints;
57  bool d_locked;
63  static inline bool isTrueTheory(theory::TheoryId theory) {
64  switch(theory) {
68  return false;
69  default:
70  return true;
71  }
72  }
73 
74 public:
75 
80  LogicInfo();
81 
87  LogicInfo(std::string logicString) throw(IllegalArgumentException);
88 
94  LogicInfo(const char* logicString) throw(IllegalArgumentException);
95 
96  // ACCESSORS
97 
103  std::string getLogicString() const;
104 
106  bool isSharingEnabled() const {
107  CheckArgument(d_locked, *this, "This LogicInfo isn't locked yet, and cannot be queried");
108  return d_sharingTheories > 1;
109  }
110 
112  bool isTheoryEnabled(theory::TheoryId theory) const {
113  CheckArgument(d_locked, *this, "This LogicInfo isn't locked yet, and cannot be queried");
114  return d_theories[theory];
115  }
116 
118  bool isQuantified() const {
119  CheckArgument(d_locked, *this, "This LogicInfo isn't locked yet, and cannot be queried");
120  return isTheoryEnabled(theory::THEORY_QUANTIFIERS);
121  }
122 
124  bool hasEverything() const {
125  CheckArgument(d_locked, *this, "This LogicInfo isn't locked yet, and cannot be queried");
126  LogicInfo everything;
127  everything.lock();
128  return *this == everything;
129  }
130 
132  bool hasNothing() const {
133  CheckArgument(d_locked, *this, "This LogicInfo isn't locked yet, and cannot be queried");
134  LogicInfo nothing("");
135  nothing.lock();
136  return *this == nothing;
137  }
138 
144  bool isPure(theory::TheoryId theory) const {
145  CheckArgument(d_locked, *this, "This LogicInfo isn't locked yet, and cannot be queried");
146  // the third and fourth conjucts are really just to rule out the misleading
147  // case where you ask isPure(THEORY_BOOL) and get true even in e.g. QF_LIA
148  return isTheoryEnabled(theory) && !isSharingEnabled() &&
149  ( !isTrueTheory(theory) || d_sharingTheories == 1 ) &&
150  ( isTrueTheory(theory) || d_sharingTheories == 0 );
151  }
152 
153  // these are for arithmetic
154 
156  bool areIntegersUsed() const {
157  CheckArgument(d_locked, *this, "This LogicInfo isn't locked yet, and cannot be queried");
158  CheckArgument(isTheoryEnabled(theory::THEORY_ARITH), *this, "Arithmetic not used in this LogicInfo; cannot ask whether integers are used");
159  return d_integers;
160  }
162  bool areRealsUsed() const {
163  CheckArgument(d_locked, *this, "This LogicInfo isn't locked yet, and cannot be queried");
164  CheckArgument(isTheoryEnabled(theory::THEORY_ARITH), *this, "Arithmetic not used in this LogicInfo; cannot ask whether reals are used");
165  return d_reals;
166  }
168  bool isLinear() const {
169  CheckArgument(d_locked, *this, "This LogicInfo isn't locked yet, and cannot be queried");
170  CheckArgument(isTheoryEnabled(theory::THEORY_ARITH), *this, "Arithmetic not used in this LogicInfo; cannot ask whether it's linear");
171  return d_linear || d_differenceLogic;
172  }
174  bool isDifferenceLogic() const {
175  CheckArgument(d_locked, *this, "This LogicInfo isn't locked yet, and cannot be queried");
176  CheckArgument(isTheoryEnabled(theory::THEORY_ARITH), *this, "Arithmetic not used in this LogicInfo; cannot ask whether it's difference logic");
177  return d_differenceLogic;
178  }
181  CheckArgument(d_locked, *this, "This LogicInfo isn't locked yet, and cannot be queried");
182  return d_cardinalityConstraints;
183  }
184 
185  // MUTATORS
186 
192  void setLogicString(std::string logicString) throw(IllegalArgumentException);
193 
198  void enableEverything();
199 
204  void disableEverything();
205 
209  void enableTheory(theory::TheoryId theory);
210 
215  void disableTheory(theory::TheoryId theory);
216 
221  enableTheory(theory::THEORY_QUANTIFIERS);
222  }
223 
228  disableTheory(theory::THEORY_QUANTIFIERS);
229  }
230 
231  // these are for arithmetic
232 
234  void enableIntegers();
236  void disableIntegers();
238  void enableReals();
240  void disableReals();
242  void arithOnlyDifference();
244  void arithOnlyLinear();
246  void arithNonLinear();
247 
248  // LOCKING FUNCTIONALITY
249 
251  void lock() { d_locked = true; }
253  bool isLocked() const { return d_locked; }
255  LogicInfo getUnlockedCopy() const;
256 
257  // COMPARISON
258 
260  bool operator==(const LogicInfo& other) const {
261  CheckArgument(isLocked() && other.isLocked(), *this, "This LogicInfo isn't locked yet, and cannot be queried");
263  if(d_theories[id] != other.d_theories[id]) {
264  return false;
265  }
266  }
267  CheckArgument(d_sharingTheories == other.d_sharingTheories, *this, "LogicInfo internal inconsistency");
268  if(isTheoryEnabled(theory::THEORY_ARITH)) {
269  return
270  d_integers == other.d_integers &&
271  d_reals == other.d_reals &&
272  d_linear == other.d_linear &&
273  d_differenceLogic == other.d_differenceLogic;
274  } else {
275  return true;
276  }
277  }
279  bool operator!=(const LogicInfo& other) const {
280  return !(*this == other);
281  }
283  bool operator>(const LogicInfo& other) const {
284  return *this >= other && *this != other;
285  }
287  bool operator<(const LogicInfo& other) const {
288  return *this <= other && *this != other;
289  }
291  bool operator<=(const LogicInfo& other) const {
292  CheckArgument(isLocked() && other.isLocked(), *this, "This LogicInfo isn't locked yet, and cannot be queried");
294  if(d_theories[id] && !other.d_theories[id]) {
295  return false;
296  }
297  }
298  CheckArgument(d_sharingTheories <= other.d_sharingTheories, *this, "LogicInfo internal inconsistency");
299  if(isTheoryEnabled(theory::THEORY_ARITH) && other.isTheoryEnabled(theory::THEORY_ARITH)) {
300  return
301  (!d_integers || other.d_integers) &&
302  (!d_reals || other.d_reals) &&
303  (d_linear || !other.d_linear) &&
304  (d_differenceLogic || !other.d_differenceLogic);
305  } else {
306  return true;
307  }
308  }
310  bool operator>=(const LogicInfo& other) const {
311  CheckArgument(isLocked() && other.isLocked(), *this, "This LogicInfo isn't locked yet, and cannot be queried");
313  if(!d_theories[id] && other.d_theories[id]) {
314  return false;
315  }
316  }
317  CheckArgument(d_sharingTheories >= other.d_sharingTheories, *this, "LogicInfo internal inconsistency");
318  if(isTheoryEnabled(theory::THEORY_ARITH) && other.isTheoryEnabled(theory::THEORY_ARITH)) {
319  return
320  (d_integers || !other.d_integers) &&
321  (d_reals || !other.d_reals) &&
322  (!d_linear || other.d_linear) &&
323  (!d_differenceLogic || other.d_differenceLogic);
324  } else {
325  return true;
326  }
327  }
328 
330  bool isComparableTo(const LogicInfo& other) const {
331  return *this <= other || *this >= other;
332  }
333 
334 };/* class LogicInfo */
335 
336 std::ostream& operator<<(std::ostream& out, const LogicInfo& logic) CVC4_PUBLIC;
337 
338 }/* CVC4 namespace */
339 
340 #endif /* __CVC4__LOGIC_INFO_H */
341 
bool operator!=(const LogicInfo &other) const
Are these two LogicInfos disequal?
Definition: logic_info.h:279
bool operator==(const LogicInfo &other) const
Are these two LogicInfos equal?
Definition: logic_info.h:260
A LogicInfo instance describes a collection of theory modules and some basic configuration about them...
Definition: logic_info.h:45
void lock()
Lock this LogicInfo, disabling further mutation and allowing queries.
Definition: logic_info.h:251
std::ostream & operator<<(std::ostream &, const Command &)
void CheckArgument(bool cond, const T &arg, const char *fmt,...)
Definition: exception.h:140
bool operator>=(const LogicInfo &other) const
Is this LogicInfo "greater than or equal" the other?
Definition: logic_info.h:310
bool operator>(const LogicInfo &other) const
Is this LogicInfo "greater than" (does it contain everything and more) the other? ...
Definition: logic_info.h:283
bool areRealsUsed() const
Are reals in this logic?
Definition: logic_info.h:162
const TheoryId THEORY_FIRST
Definition: kind.h:607
void enableQuantifiers()
Quantifiers are a special case, since two theory modules handle them.
Definition: logic_info.h:220
bool isQuantified() const
Is this a quantified logic?
Definition: logic_info.h:118
bool isPure(theory::TheoryId theory) const
Is this a pure logic (only one "true" background theory).
Definition: logic_info.h:144
bool hasNothing() const
Is this the all-exclusive logic? (Here, that means propositional logic)
Definition: logic_info.h:132
#define CVC4_PUBLIC
Definition: cvc4_public.h:30
bool isSharingEnabled() const
Is sharing enabled for this logic?
Definition: logic_info.h:106
bool hasCardinalityConstraints() const
Does this logic allow cardinality constraints?
Definition: logic_info.h:180
Macros that should be defined everywhere during the building of the libraries and driver binary...
bool isComparableTo(const LogicInfo &other) const
Are two LogicInfos comparable? That is, is one of <= or > true?
Definition: logic_info.h:330
bool isLocked() const
Check whether this LogicInfo is locked, disallowing further mutation.
Definition: logic_info.h:253
kind.h
void disableQuantifiers()
Quantifiers are a special case, since two theory modules handle them.
Definition: logic_info.h:227
bool isDifferenceLogic() const
Does this logic only permit difference reasoning? (implies linear)
Definition: logic_info.h:174
bool isLinear() const
Does this logic only linear arithmetic?
Definition: logic_info.h:168
struct CVC4::options::out__option_t out
bool areIntegersUsed() const
Are integers in this logic?
Definition: logic_info.h:156
bool operator<=(const LogicInfo &other) const
Is this LogicInfo "less than or equal" the other?
Definition: logic_info.h:291
bool isTheoryEnabled(theory::TheoryId theory) const
Is the given theory module active in this logic?
Definition: logic_info.h:112
bool hasEverything() const
Is this the all-inclusive logic?
Definition: logic_info.h:124
bool operator<(const LogicInfo &other) const
Is this LogicInfo "less than" (does it contain strictly less) the other?
Definition: logic_info.h:287