update copyrights
[cvc5.git] / src / theory / logic_info.h
1 /********************* */
2 /*! \file logic_info.h
3 ** \verbatim
4 ** Original author: Morgan Deters <mdeters@cs.nyu.edu>
5 ** Major contributors: none
6 ** Minor contributors (to current version): Dejan Jovanović <dejan.jovanovic@gmail.com>
7 ** This file is part of the CVC4 project.
8 ** Copyright (c) 2009-2013 New York University and The University of Iowa
9 ** See the file COPYING in the top-level source directory for licensing
10 ** 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 #include "expr/kind.h"
27
28 namespace CVC4 {
29
30 /**
31 * A LogicInfo instance describes a collection of theory modules and some
32 * basic configuration about them. Conceptually, it provides a background
33 * context for all operations in CVC4. Typically, when CVC4's SmtEngine
34 * is created, it is issued a setLogic() command indicating features of the
35 * assertions and queries to follow---for example, whether quantifiers are
36 * used, whether integers or reals (or both) will be used, etc.
37 *
38 * Most places in CVC4 will only ever need to access a const reference to an
39 * instance of this class. Such an instance is generally set by the SmtEngine
40 * when setLogic() is called. However, mutating member functions are also
41 * provided by this class so that it can be used as a more general mechanism
42 * (e.g., for communicating to the SmtEngine which theories should be used,
43 * rather than having to provide an SMT-LIB string).
44 */
45 class CVC4_PUBLIC LogicInfo {
46 mutable std::string d_logicString; /**< an SMT-LIB-like logic string */
47 std::vector<bool> d_theories; /**< set of active theories */
48 size_t d_sharingTheories; /**< count of theories that need sharing */
49
50 // for arithmetic
51 bool d_integers; /**< are integers used in this logic? */
52 bool d_reals; /**< are reals used in this logic? */
53 bool d_linear; /**< linear-only arithmetic in this logic? */
54 bool d_differenceLogic; /**< difference-only arithmetic in this logic? */
55
56 bool d_locked; /**< is this LogicInfo instance locked (and thus immutable)? */
57
58 /**
59 * Returns true iff this is a "true" theory (one that must be worried
60 * about for sharing
61 */
62 static inline bool isTrueTheory(theory::TheoryId theory) {
63 switch(theory) {
64 case theory::THEORY_BUILTIN:
65 case theory::THEORY_BOOL:
66 case theory::THEORY_QUANTIFIERS:
67 case theory::THEORY_REWRITERULES:
68 return false;
69 default:
70 return true;
71 }
72 }
73
74 public:
75
76 /**
77 * Constructs a LogicInfo for the most general logic (quantifiers, all
78 * background theory modules, ...).
79 */
80 LogicInfo();
81
82 /**
83 * Construct a LogicInfo from an SMT-LIB-like logic string.
84 * Throws an IllegalArgumentException if the logic string cannot
85 * be interpreted.
86 */
87 LogicInfo(std::string logicString) throw(IllegalArgumentException);
88
89 /**
90 * Construct a LogicInfo from an SMT-LIB-like logic string.
91 * Throws an IllegalArgumentException if the logic string cannot
92 * be interpreted.
93 */
94 LogicInfo(const char* logicString) throw(IllegalArgumentException);
95
96 // ACCESSORS
97
98 /**
99 * Get an SMT-LIB-like logic string. These are only guaranteed to
100 * be SMT-LIB-compliant if an SMT-LIB-compliant string was used in
101 * the constructor and no mutating functions were called.
102 */
103 std::string getLogicString() const;
104
105 /** Is sharing enabled for this logic? */
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
111 /** Is the given theory module active in this logic? */
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
117 /** Is this a quantified logic? */
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
123 /** Is this the all-inclusive logic? */
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
131 /** Is this the all-exclusive logic? (Here, that means propositional logic) */
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
139 /**
140 * Is this a pure logic (only one "true" background theory). Quantifiers
141 * can exist in such logics though; to test for quantifier-free purity,
142 * use "isPure(theory) && !isQuantified()".
143 */
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
155 /** Are integers in this logic? */
156 bool areIntegersUsed() const {
157 CheckArgument(d_locked, *this, "This LogicInfo isn't locked yet, and cannot be queried");
158 return d_integers;
159 }
160 /** Are reals in this logic? */
161 bool areRealsUsed() const {
162 CheckArgument(d_locked, *this, "This LogicInfo isn't locked yet, and cannot be queried");
163 return d_reals;
164 }
165 /** Does this logic only linear arithmetic? */
166 bool isLinear() const {
167 CheckArgument(d_locked, *this, "This LogicInfo isn't locked yet, and cannot be queried");
168 return d_linear || d_differenceLogic;
169 }
170 /** Does this logic only permit difference reasoning? (implies linear) */
171 bool isDifferenceLogic() const {
172 CheckArgument(d_locked, *this, "This LogicInfo isn't locked yet, and cannot be queried");
173 return d_differenceLogic;
174 }
175
176 // MUTATORS
177
178 /**
179 * Initialize the LogicInfo with an SMT-LIB-like logic string.
180 * Throws an IllegalArgumentException if the string can't be
181 * interpreted.
182 */
183 void setLogicString(std::string logicString) throw(IllegalArgumentException);
184
185 /**
186 * Enable all functionality. All theories, plus quantifiers, will be
187 * enabled.
188 */
189 void enableEverything();
190
191 /**
192 * Disable all functionality. The result will be a LogicInfo with
193 * the BUILTIN and BOOLEAN theories enabled only ("QF_SAT").
194 */
195 void disableEverything();
196
197 /**
198 * Enable the given theory module.
199 */
200 void enableTheory(theory::TheoryId theory);
201
202 /**
203 * Disable the given theory module. THEORY_BUILTIN and THEORY_BOOL cannot
204 * be disabled (and if given here, the request will be silently ignored).
205 */
206 void disableTheory(theory::TheoryId theory);
207
208 /**
209 * Quantifiers are a special case, since two theory modules handle them.
210 */
211 void enableQuantifiers() {
212 enableTheory(theory::THEORY_QUANTIFIERS);
213 enableTheory(theory::THEORY_REWRITERULES);
214 }
215
216 /**
217 * Quantifiers are a special case, since two theory modules handle them.
218 */
219 void disableQuantifiers() {
220 disableTheory(theory::THEORY_QUANTIFIERS);
221 disableTheory(theory::THEORY_REWRITERULES);
222 }
223
224 // these are for arithmetic
225
226 /** Enable the use of integers in this logic. */
227 void enableIntegers();
228 /** Disable the use of integers in this logic. */
229 void disableIntegers();
230 /** Enable the use of reals in this logic. */
231 void enableReals();
232 /** Disable the use of reals in this logic. */
233 void disableReals();
234 /** Only permit difference arithmetic in this logic. */
235 void arithOnlyDifference();
236 /** Only permit linear arithmetic in this logic. */
237 void arithOnlyLinear();
238 /** Permit nonlinear arithmetic in this logic. */
239 void arithNonLinear();
240
241 // LOCKING FUNCTIONALITY
242
243 /** Lock this LogicInfo, disabling further mutation and allowing queries */
244 void lock() { d_locked = true; }
245 /** Check whether this LogicInfo is locked, disallowing further mutation */
246 bool isLocked() const { return d_locked; }
247 /** Get a copy of this LogicInfo that is identical, but unlocked */
248 LogicInfo getUnlockedCopy() const;
249
250 // COMPARISON
251
252 /** Are these two LogicInfos equal? */
253 bool operator==(const LogicInfo& other) const {
254 CheckArgument(isLocked() && other.isLocked(), *this, "This LogicInfo isn't locked yet, and cannot be queried");
255 for(theory::TheoryId id = theory::THEORY_FIRST; id < theory::THEORY_LAST; ++id) {
256 if(d_theories[id] != other.d_theories[id]) {
257 return false;
258 }
259 }
260 CheckArgument(d_sharingTheories == other.d_sharingTheories, *this, "LogicInfo internal inconsistency");
261 if(isTheoryEnabled(theory::THEORY_ARITH)) {
262 return
263 d_integers == other.d_integers &&
264 d_reals == other.d_reals &&
265 d_linear == other.d_linear &&
266 d_differenceLogic == other.d_differenceLogic;
267 } else {
268 return true;
269 }
270 }
271 /** Are these two LogicInfos disequal? */
272 bool operator!=(const LogicInfo& other) const {
273 return !(*this == other);
274 }
275 /** Is this LogicInfo "greater than" (does it contain everything and more) the other? */
276 bool operator>(const LogicInfo& other) const {
277 return *this >= other && *this != other;
278 }
279 /** Is this LogicInfo "less than" (does it contain strictly less) the other? */
280 bool operator<(const LogicInfo& other) const {
281 return *this <= other && *this != other;
282 }
283 /** Is this LogicInfo "less than or equal" the other? */
284 bool operator<=(const LogicInfo& other) const {
285 CheckArgument(isLocked() && other.isLocked(), *this, "This LogicInfo isn't locked yet, and cannot be queried");
286 for(theory::TheoryId id = theory::THEORY_FIRST; id < theory::THEORY_LAST; ++id) {
287 if(d_theories[id] && !other.d_theories[id]) {
288 return false;
289 }
290 }
291 CheckArgument(d_sharingTheories <= other.d_sharingTheories, *this, "LogicInfo internal inconsistency");
292 if(isTheoryEnabled(theory::THEORY_ARITH) && other.isTheoryEnabled(theory::THEORY_ARITH)) {
293 return
294 (!d_integers || other.d_integers) &&
295 (!d_reals || other.d_reals) &&
296 (d_linear || !other.d_linear) &&
297 (d_differenceLogic || !other.d_differenceLogic);
298 } else {
299 return true;
300 }
301 }
302 /** Is this LogicInfo "greater than or equal" the other? */
303 bool operator>=(const LogicInfo& other) const {
304 CheckArgument(isLocked() && other.isLocked(), *this, "This LogicInfo isn't locked yet, and cannot be queried");
305 for(theory::TheoryId id = theory::THEORY_FIRST; id < theory::THEORY_LAST; ++id) {
306 if(!d_theories[id] && other.d_theories[id]) {
307 return false;
308 }
309 }
310 CheckArgument(d_sharingTheories >= other.d_sharingTheories, *this, "LogicInfo internal inconsistency");
311 if(isTheoryEnabled(theory::THEORY_ARITH) && other.isTheoryEnabled(theory::THEORY_ARITH)) {
312 return
313 (d_integers || !other.d_integers) &&
314 (d_reals || !other.d_reals) &&
315 (!d_linear || other.d_linear) &&
316 (!d_differenceLogic || other.d_differenceLogic);
317 } else {
318 return true;
319 }
320 }
321
322 /** Are two LogicInfos comparable? That is, is one of <= or > true? */
323 bool isComparableTo(const LogicInfo& other) const {
324 return *this <= other || *this >= other;
325 }
326
327 };/* class LogicInfo */
328
329 std::ostream& operator<<(std::ostream& out, const LogicInfo& logic) CVC4_PUBLIC;
330
331 }/* CVC4 namespace */
332
333 #endif /* __CVC4__LOGIC_INFO_H */
334