1 /********************* */
4 ** Original author: Morgan Deters
5 ** Major contributors: none
6 ** Minor contributors (to current version): Dejan Jovanovic, Andrew Reynolds
7 ** This file is part of the CVC4 project.
8 ** Copyright (c) 2009-2014 New York University and The University of Iowa
9 ** See the file COPYING in the top-level source directory for licensing
10 ** information.\endverbatim
12 ** \brief A class giving information about a logic (group a theory modules
13 ** and configuration information)
15 ** A class giving information about a logic (group of theory modules and
16 ** configuration information).
19 #include "cvc4_public.h"
21 #ifndef __CVC4__LOGIC_INFO_H
22 #define __CVC4__LOGIC_INFO_H
26 #include "expr/kind.h"
27 #include "options/logic_info_forward.h"
32 * A LogicInfo instance describes a collection of theory modules and some
33 * basic configuration about them. Conceptually, it provides a background
34 * context for all operations in CVC4. Typically, when CVC4's SmtEngine
35 * is created, it is issued a setLogic() command indicating features of the
36 * assertions and queries to follow---for example, whether quantifiers are
37 * used, whether integers or reals (or both) will be used, etc.
39 * Most places in CVC4 will only ever need to access a const reference to an
40 * instance of this class. Such an instance is generally set by the SmtEngine
41 * when setLogic() is called. However, mutating member functions are also
42 * provided by this class so that it can be used as a more general mechanism
43 * (e.g., for communicating to the SmtEngine which theories should be used,
44 * rather than having to provide an SMT-LIB string).
46 class CVC4_PUBLIC LogicInfo
{
47 mutable std::string d_logicString
; /**< an SMT-LIB-like logic string */
48 std::vector
<bool> d_theories
; /**< set of active theories */
49 size_t d_sharingTheories
; /**< count of theories that need sharing */
52 bool d_integers
; /**< are integers used in this logic? */
53 bool d_reals
; /**< are reals used in this logic? */
54 bool d_linear
; /**< linear-only arithmetic in this logic? */
55 bool d_differenceLogic
; /**< difference-only arithmetic in this logic? */
56 bool d_cardinalityConstraints
; /**< cardinality constraints in this logic? */
58 bool d_locked
; /**< is this LogicInfo instance locked (and thus immutable)? */
61 * Returns true iff this is a "true" theory (one that must be worried
64 static inline bool isTrueTheory(theory::TheoryId theory
) {
66 case theory::THEORY_BUILTIN
:
67 case theory::THEORY_BOOL
:
68 case theory::THEORY_QUANTIFIERS
:
78 * Constructs a LogicInfo for the most general logic (quantifiers, all
79 * background theory modules, ...).
84 * Construct a LogicInfo from an SMT-LIB-like logic string.
85 * Throws an IllegalArgumentException if the logic string cannot
88 LogicInfo(std::string logicString
) throw(IllegalArgumentException
);
91 * Construct a LogicInfo from an SMT-LIB-like logic string.
92 * Throws an IllegalArgumentException if the logic string cannot
95 LogicInfo(const char* logicString
) throw(IllegalArgumentException
);
100 * Get an SMT-LIB-like logic string. These are only guaranteed to
101 * be SMT-LIB-compliant if an SMT-LIB-compliant string was used in
102 * the constructor and no mutating functions were called.
104 std::string
getLogicString() const;
106 /** Is sharing enabled for this logic? */
107 bool isSharingEnabled() const {
108 CheckArgument(d_locked
, *this, "This LogicInfo isn't locked yet, and cannot be queried");
109 return d_sharingTheories
> 1;
112 /** Is the given theory module active in this logic? */
113 bool isTheoryEnabled(theory::TheoryId theory
) const {
114 CheckArgument(d_locked
, *this, "This LogicInfo isn't locked yet, and cannot be queried");
115 return d_theories
[theory
];
118 /** Is this a quantified logic? */
119 bool isQuantified() const {
120 CheckArgument(d_locked
, *this, "This LogicInfo isn't locked yet, and cannot be queried");
121 return isTheoryEnabled(theory::THEORY_QUANTIFIERS
);
124 /** Is this the all-inclusive logic? */
125 bool hasEverything() const {
126 CheckArgument(d_locked
, *this, "This LogicInfo isn't locked yet, and cannot be queried");
127 LogicInfo everything
;
129 return *this == everything
;
132 /** Is this the all-exclusive logic? (Here, that means propositional logic) */
133 bool hasNothing() const {
134 CheckArgument(d_locked
, *this, "This LogicInfo isn't locked yet, and cannot be queried");
135 LogicInfo
nothing("");
137 return *this == nothing
;
141 * Is this a pure logic (only one "true" background theory). Quantifiers
142 * can exist in such logics though; to test for quantifier-free purity,
143 * use "isPure(theory) && !isQuantified()".
145 bool isPure(theory::TheoryId theory
) const {
146 CheckArgument(d_locked
, *this, "This LogicInfo isn't locked yet, and cannot be queried");
147 // the third and fourth conjucts are really just to rule out the misleading
148 // case where you ask isPure(THEORY_BOOL) and get true even in e.g. QF_LIA
149 return isTheoryEnabled(theory
) && !isSharingEnabled() &&
150 ( !isTrueTheory(theory
) || d_sharingTheories
== 1 ) &&
151 ( isTrueTheory(theory
) || d_sharingTheories
== 0 );
154 // these are for arithmetic
156 /** Are integers in this logic? */
157 bool areIntegersUsed() const {
158 CheckArgument(d_locked
, *this, "This LogicInfo isn't locked yet, and cannot be queried");
159 CheckArgument(isTheoryEnabled(theory::THEORY_ARITH
), *this, "Arithmetic not used in this LogicInfo; cannot ask whether integers are used");
162 /** Are reals in this logic? */
163 bool areRealsUsed() const {
164 CheckArgument(d_locked
, *this, "This LogicInfo isn't locked yet, and cannot be queried");
165 CheckArgument(isTheoryEnabled(theory::THEORY_ARITH
), *this, "Arithmetic not used in this LogicInfo; cannot ask whether reals are used");
168 /** Does this logic only linear arithmetic? */
169 bool isLinear() const {
170 CheckArgument(d_locked
, *this, "This LogicInfo isn't locked yet, and cannot be queried");
171 CheckArgument(isTheoryEnabled(theory::THEORY_ARITH
), *this, "Arithmetic not used in this LogicInfo; cannot ask whether it's linear");
172 return d_linear
|| d_differenceLogic
;
174 /** Does this logic only permit difference reasoning? (implies linear) */
175 bool isDifferenceLogic() const {
176 CheckArgument(d_locked
, *this, "This LogicInfo isn't locked yet, and cannot be queried");
177 CheckArgument(isTheoryEnabled(theory::THEORY_ARITH
), *this, "Arithmetic not used in this LogicInfo; cannot ask whether it's difference logic");
178 return d_differenceLogic
;
180 /** Does this logic allow cardinality constraints? */
181 bool hasCardinalityConstraints() const {
182 CheckArgument(d_locked
, *this, "This LogicInfo isn't locked yet, and cannot be queried");
183 return d_cardinalityConstraints
;
189 * Initialize the LogicInfo with an SMT-LIB-like logic string.
190 * Throws an IllegalArgumentException if the string can't be
193 void setLogicString(std::string logicString
) throw(IllegalArgumentException
);
196 * Enable all functionality. All theories, plus quantifiers, will be
199 void enableEverything();
202 * Disable all functionality. The result will be a LogicInfo with
203 * the BUILTIN and BOOLEAN theories enabled only ("QF_SAT").
205 void disableEverything();
208 * Enable the given theory module.
210 void enableTheory(theory::TheoryId theory
);
213 * Disable the given theory module. THEORY_BUILTIN and THEORY_BOOL cannot
214 * be disabled (and if given here, the request will be silently ignored).
216 void disableTheory(theory::TheoryId theory
);
219 * Quantifiers are a special case, since two theory modules handle them.
221 void enableQuantifiers() {
222 enableTheory(theory::THEORY_QUANTIFIERS
);
226 * Quantifiers are a special case, since two theory modules handle them.
228 void disableQuantifiers() {
229 disableTheory(theory::THEORY_QUANTIFIERS
);
232 // these are for arithmetic
234 /** Enable the use of integers in this logic. */
235 void enableIntegers();
236 /** Disable the use of integers in this logic. */
237 void disableIntegers();
238 /** Enable the use of reals in this logic. */
240 /** Disable the use of reals in this logic. */
242 /** Only permit difference arithmetic in this logic. */
243 void arithOnlyDifference();
244 /** Only permit linear arithmetic in this logic. */
245 void arithOnlyLinear();
246 /** Permit nonlinear arithmetic in this logic. */
247 void arithNonLinear();
249 // LOCKING FUNCTIONALITY
251 /** Lock this LogicInfo, disabling further mutation and allowing queries */
252 void lock() { d_locked
= true; }
253 /** Check whether this LogicInfo is locked, disallowing further mutation */
254 bool isLocked() const { return d_locked
; }
255 /** Get a copy of this LogicInfo that is identical, but unlocked */
256 LogicInfo
getUnlockedCopy() const;
260 /** Are these two LogicInfos equal? */
261 bool operator==(const LogicInfo
& other
) const {
262 CheckArgument(isLocked() && other
.isLocked(), *this, "This LogicInfo isn't locked yet, and cannot be queried");
263 for(theory::TheoryId id
= theory::THEORY_FIRST
; id
< theory::THEORY_LAST
; ++id
) {
264 if(d_theories
[id
] != other
.d_theories
[id
]) {
268 CheckArgument(d_sharingTheories
== other
.d_sharingTheories
, *this, "LogicInfo internal inconsistency");
269 if(isTheoryEnabled(theory::THEORY_ARITH
)) {
271 d_integers
== other
.d_integers
&&
272 d_reals
== other
.d_reals
&&
273 d_linear
== other
.d_linear
&&
274 d_differenceLogic
== other
.d_differenceLogic
;
279 /** Are these two LogicInfos disequal? */
280 bool operator!=(const LogicInfo
& other
) const {
281 return !(*this == other
);
283 /** Is this LogicInfo "greater than" (does it contain everything and more) the other? */
284 bool operator>(const LogicInfo
& other
) const {
285 return *this >= other
&& *this != other
;
287 /** Is this LogicInfo "less than" (does it contain strictly less) the other? */
288 bool operator<(const LogicInfo
& other
) const {
289 return *this <= other
&& *this != other
;
291 /** Is this LogicInfo "less than or equal" the other? */
292 bool operator<=(const LogicInfo
& other
) const {
293 CheckArgument(isLocked() && other
.isLocked(), *this, "This LogicInfo isn't locked yet, and cannot be queried");
294 for(theory::TheoryId id
= theory::THEORY_FIRST
; id
< theory::THEORY_LAST
; ++id
) {
295 if(d_theories
[id
] && !other
.d_theories
[id
]) {
299 CheckArgument(d_sharingTheories
<= other
.d_sharingTheories
, *this, "LogicInfo internal inconsistency");
300 if(isTheoryEnabled(theory::THEORY_ARITH
) && other
.isTheoryEnabled(theory::THEORY_ARITH
)) {
302 (!d_integers
|| other
.d_integers
) &&
303 (!d_reals
|| other
.d_reals
) &&
304 (d_linear
|| !other
.d_linear
) &&
305 (d_differenceLogic
|| !other
.d_differenceLogic
);
310 /** Is this LogicInfo "greater than or equal" the other? */
311 bool operator>=(const LogicInfo
& other
) const {
312 CheckArgument(isLocked() && other
.isLocked(), *this, "This LogicInfo isn't locked yet, and cannot be queried");
313 for(theory::TheoryId id
= theory::THEORY_FIRST
; id
< theory::THEORY_LAST
; ++id
) {
314 if(!d_theories
[id
] && other
.d_theories
[id
]) {
318 CheckArgument(d_sharingTheories
>= other
.d_sharingTheories
, *this, "LogicInfo internal inconsistency");
319 if(isTheoryEnabled(theory::THEORY_ARITH
) && other
.isTheoryEnabled(theory::THEORY_ARITH
)) {
321 (d_integers
|| !other
.d_integers
) &&
322 (d_reals
|| !other
.d_reals
) &&
323 (!d_linear
|| other
.d_linear
) &&
324 (!d_differenceLogic
|| other
.d_differenceLogic
);
330 /** Are two LogicInfos comparable? That is, is one of <= or > true? */
331 bool isComparableTo(const LogicInfo
& other
) const {
332 return *this <= other
|| *this >= other
;
335 };/* class LogicInfo */
337 std::ostream
& operator<<(std::ostream
& out
, const LogicInfo
& logic
) CVC4_PUBLIC
;
339 }/* CVC4 namespace */
341 #endif /* __CVC4__LOGIC_INFO_H */