cvc4-1.3
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;
56  bool d_locked;
62  static inline bool isTrueTheory(theory::TheoryId theory) {
63  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) || isTheoryEnabled(theory::THEORY_REWRITERULES);
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  }
179 
180  // MUTATORS
181 
187  void setLogicString(std::string logicString) throw(IllegalArgumentException);
188 
193  void enableEverything();
194 
199  void disableEverything();
200 
204  void enableTheory(theory::TheoryId theory);
205 
210  void disableTheory(theory::TheoryId theory);
211 
216  enableTheory(theory::THEORY_QUANTIFIERS);
217  enableTheory(theory::THEORY_REWRITERULES);
218  }
219 
224  disableTheory(theory::THEORY_QUANTIFIERS);
225  disableTheory(theory::THEORY_REWRITERULES);
226  }
227 
228  // these are for arithmetic
229 
231  void enableIntegers();
233  void disableIntegers();
235  void enableReals();
237  void disableReals();
239  void arithOnlyDifference();
241  void arithOnlyLinear();
243  void arithNonLinear();
244 
245  // LOCKING FUNCTIONALITY
246 
248  void lock() { d_locked = true; }
250  bool isLocked() const { return d_locked; }
252  LogicInfo getUnlockedCopy() const;
253 
254  // COMPARISON
255 
257  bool operator==(const LogicInfo& other) const {
258  CheckArgument(isLocked() && other.isLocked(), *this, "This LogicInfo isn't locked yet, and cannot be queried");
260  if(d_theories[id] != other.d_theories[id]) {
261  return false;
262  }
263  }
264  CheckArgument(d_sharingTheories == other.d_sharingTheories, *this, "LogicInfo internal inconsistency");
265  if(isTheoryEnabled(theory::THEORY_ARITH)) {
266  return
267  d_integers == other.d_integers &&
268  d_reals == other.d_reals &&
269  d_linear == other.d_linear &&
270  d_differenceLogic == other.d_differenceLogic;
271  } else {
272  return true;
273  }
274  }
276  bool operator!=(const LogicInfo& other) const {
277  return !(*this == other);
278  }
280  bool operator>(const LogicInfo& other) const {
281  return *this >= other && *this != other;
282  }
284  bool operator<(const LogicInfo& other) const {
285  return *this <= other && *this != other;
286  }
288  bool operator<=(const LogicInfo& other) const {
289  CheckArgument(isLocked() && other.isLocked(), *this, "This LogicInfo isn't locked yet, and cannot be queried");
291  if(d_theories[id] && !other.d_theories[id]) {
292  return false;
293  }
294  }
295  CheckArgument(d_sharingTheories <= other.d_sharingTheories, *this, "LogicInfo internal inconsistency");
296  if(isTheoryEnabled(theory::THEORY_ARITH) && other.isTheoryEnabled(theory::THEORY_ARITH)) {
297  return
298  (!d_integers || other.d_integers) &&
299  (!d_reals || other.d_reals) &&
300  (d_linear || !other.d_linear) &&
301  (d_differenceLogic || !other.d_differenceLogic);
302  } else {
303  return true;
304  }
305  }
307  bool operator>=(const LogicInfo& other) const {
308  CheckArgument(isLocked() && other.isLocked(), *this, "This LogicInfo isn't locked yet, and cannot be queried");
310  if(!d_theories[id] && other.d_theories[id]) {
311  return false;
312  }
313  }
314  CheckArgument(d_sharingTheories >= other.d_sharingTheories, *this, "LogicInfo internal inconsistency");
315  if(isTheoryEnabled(theory::THEORY_ARITH) && other.isTheoryEnabled(theory::THEORY_ARITH)) {
316  return
317  (d_integers || !other.d_integers) &&
318  (d_reals || !other.d_reals) &&
319  (!d_linear || other.d_linear) &&
320  (!d_differenceLogic || other.d_differenceLogic);
321  } else {
322  return true;
323  }
324  }
325 
327  bool isComparableTo(const LogicInfo& other) const {
328  return *this <= other || *this >= other;
329  }
330 
331 };/* class LogicInfo */
332 
333 std::ostream& operator<<(std::ostream& out, const LogicInfo& logic) CVC4_PUBLIC;
334 
335 }/* CVC4 namespace */
336 
337 #endif /* __CVC4__LOGIC_INFO_H */
338 
bool hasNothing() const
Is this the all-exclusive logic? (Here, that means propositional logic)
Definition: logic_info.h:132
bool areIntegersUsed() const
Are integers in this logic?
Definition: logic_info.h:156
bool operator==(const LogicInfo &other) const
Are these two LogicInfos equal?
Definition: logic_info.h:257
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:248
bool isLinear() const
Does this logic only linear arithmetic?
Definition: logic_info.h:168
bool operator>(const LogicInfo &other) const
Is this LogicInfo "greater than" (does it contain everything and more) the other? ...
Definition: logic_info.h:280
void CheckArgument(bool cond, const T &arg, const char *fmt,...)
Definition: exception.h:140
const TheoryId THEORY_FIRST
Definition: kind.h:547
bool isQuantified() const
Is this a quantified logic?
Definition: logic_info.h:118
void enableQuantifiers()
Quantifiers are a special case, since two theory modules handle them.
Definition: logic_info.h:215
bool operator<(const LogicInfo &other) const
Is this LogicInfo "less than" (does it contain strictly less) the other?
Definition: logic_info.h:284
This is CVC4 release version For build and installation please see the INSTALL file included with this distribution This first official release of CVC4 is the result of more than three years of efforts by researchers at New York University and The University of Iowa The project leaders are Clark please refer to the AUTHORS file in the source distribution CVC4 is a tool for determining the satisfiability of a first order formula modulo a first order CVC CVC3 but does not directly incorporate code from any previous version CVC4 is intended to be an open and extensible SMT engine It can be used as a stand alone tool or as a library It has been designed to increase the performance and reduce the memory overhead of its predecessors It is written entirely in C and is released under a free software see the INSTALL file that comes with this distribution We recommend that you visit our CVC4 tutorials online please write to the cvc users cs nyu edu mailing list *if you need to report a bug with CVC4
Definition: README:39
#define CVC4_PUBLIC
Definition: cvc4_public.h:30
bool operator<=(const LogicInfo &other) const
Is this LogicInfo "less than or equal" the other?
Definition: logic_info.h:288
This is CVC4 release version For build and installation please see the INSTALL file included with this distribution This first official release of CVC4 is the result of more than three years of efforts by researchers at New York University and The University of Iowa The project leaders are Clark please refer to the AUTHORS file in the source distribution CVC4 is a tool for determining the satisfiability of a first order formula modulo a first order theory(or a combination of such theories).It is the fourth in the Cooperating Validity Checker family of tools(CVC
bool operator!=(const LogicInfo &other) const
Are these two LogicInfos disequal?
Definition: logic_info.h:276
std::ostream & operator<<(std::ostream &out, const TypeCheckingException &e)
bool operator>=(const LogicInfo &other) const
Is this LogicInfo "greater than or equal" the other?
Definition: logic_info.h:307
Macros that should be defined everywhere during the building of the libraries and driver binary...
bool isSharingEnabled() const
Is sharing enabled for this logic?
Definition: logic_info.h:106
bool hasEverything() const
Is this the all-inclusive logic?
Definition: logic_info.h:124
bool isPure(theory::TheoryId theory) const
Is this a pure logic (only one "true" background theory).
Definition: logic_info.h:144
bool isDifferenceLogic() const
Does this logic only permit difference reasoning? (implies linear)
Definition: logic_info.h:174
kind.h
void disableQuantifiers()
Quantifiers are a special case, since two theory modules handle them.
Definition: logic_info.h:223
struct CVC4::options::out__option_t out
bool isComparableTo(const LogicInfo &other) const
Are two LogicInfos comparable? That is, is one of <= or > true?
Definition: logic_info.h:327
bool areRealsUsed() const
Are reals in this logic?
Definition: logic_info.h:162
bool isTheoryEnabled(theory::TheoryId theory) const
Is the given theory module active in this logic?
Definition: logic_info.h:112
bool isLocked() const
Check whether this LogicInfo is locked, disallowing further mutation.
Definition: logic_info.h:250