1 /********************* */
4 ** Original author: mdeters
5 ** Major contributors: none
6 ** Minor contributors (to current version): none
7 ** This file is part of the CVC4 prototype.
8 ** Copyright (c) 2009--2012 The Analysis of Computer Systems Group (ACSys)
9 ** Courant Institute of Mathematical Sciences
10 ** New York University
11 ** See the file COPYING in the top-level source directory for licensing
12 ** information.\endverbatim
14 ** \brief A class giving information about a logic (group a theory modules
15 ** and configuration information)
17 ** A class giving information about a logic (group of theory modules and
18 ** configuration information).
21 #include "cvc4_public.h"
23 #ifndef __CVC4__LOGIC_INFO_H
24 #define __CVC4__LOGIC_INFO_H
27 #include "expr/kind.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).
47 mutable std::string d_logicString
; /**< an SMT-LIB-like logic string */
48 bool d_theories
[theory::THEORY_LAST
]; /**< 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? */
57 bool d_locked
; /**< is this LogicInfo instance locked (and thus immutable)? */
60 * Returns true iff this is a "true" theory (one that must be worried
63 static inline bool isTrueTheory(theory::TheoryId theory
) {
65 case theory::THEORY_BUILTIN
:
66 case theory::THEORY_BOOL
:
67 case theory::THEORY_QUANTIFIERS
:
68 case theory::THEORY_REWRITERULES
:
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
);
93 * Get an SMT-LIB-like logic string. These are only guaranteed to
94 * be SMT-LIB-compliant if an SMT-LIB-compliant string was used in
95 * the constructor and no mutating functions were called.
97 std::string
getLogicString() const;
99 /** Is sharing enabled for this logic? */
100 bool isSharingEnabled() const {
101 Assert(d_locked
, "This LogicInfo isn't locked yet, and cannot be queried");
102 return d_sharingTheories
> 1;
104 /** Is the given theory module active in this logic? */
105 bool isTheoryEnabled(theory::TheoryId theory
) const {
106 Assert(d_locked
, "This LogicInfo isn't locked yet, and cannot be queried");
107 return d_theories
[theory
];
110 /** Is this a quantified logic? */
111 bool isQuantified() const {
112 Assert(d_locked
, "This LogicInfo isn't locked yet, and cannot be queried");
113 return isTheoryEnabled(theory::THEORY_QUANTIFIERS
) || isTheoryEnabled(theory::THEORY_REWRITERULES
);
117 * Is this a pure logic (only one "true" background theory). Quantifiers
118 * can exist in such logics though; to test for quantifier-free purity,
119 * use "isPure(theory) && !isQuantified()".
121 bool isPure(theory::TheoryId theory
) const {
122 Assert(d_locked
, "This LogicInfo isn't locked yet, and cannot be queried");
123 // the third and fourth conjucts are really just to rule out the misleading
124 // case where you ask isPure(THEORY_BOOL) and get true even in e.g. QF_LIA
125 return isTheoryEnabled(theory
) && !isSharingEnabled() &&
126 ( !isTrueTheory(theory
) || d_sharingTheories
== 1 ) &&
127 ( isTrueTheory(theory
) || d_sharingTheories
== 0 );
130 // these are for arithmetic
132 /** Are integers in this logic? */
133 bool areIntegersUsed() const {
134 Assert(d_locked
, "This LogicInfo isn't locked yet, and cannot be queried");
137 /** Are reals in this logic? */
138 bool areRealsUsed() const {
139 Assert(d_locked
, "This LogicInfo isn't locked yet, and cannot be queried");
142 /** Does this logic only linear arithmetic? */
143 bool isLinear() const {
144 Assert(d_locked
, "This LogicInfo isn't locked yet, and cannot be queried");
145 return d_linear
|| d_differenceLogic
;
147 /** Does this logic only permit difference reasoning? (implies linear) */
148 bool isDifferenceLogic() const {
149 Assert(d_locked
, "This LogicInfo isn't locked yet, and cannot be queried");
150 return d_differenceLogic
;
156 * Initialize the LogicInfo with an SMT-LIB-like logic string.
157 * Throws an IllegalArgumentException if the string can't be
160 void setLogicString(std::string logicString
) throw(IllegalArgumentException
);
163 * Enable all functionality. All theories, plus quantifiers, will be
166 void enableEverything();
169 * Disable all functionality. The result will be a LogicInfo with
170 * the BUILTIN and BOOLEAN theories enabled only ("QF_SAT").
172 void disableEverything();
175 * Enable the given theory module.
177 void enableTheory(theory::TheoryId theory
);
180 * Disable the given theory module. THEORY_BUILTIN and THEORY_BOOL cannot
181 * be disabled (and if given here, the request will be silently ignored).
183 void disableTheory(theory::TheoryId theory
);
186 * Quantifiers are a special case, since two theory modules handle them.
188 void enableQuantifiers() {
189 enableTheory(theory::THEORY_QUANTIFIERS
);
190 enableTheory(theory::THEORY_REWRITERULES
);
194 * Quantifiers are a special case, since two theory modules handle them.
196 void disableQuantifiers() {
197 disableTheory(theory::THEORY_QUANTIFIERS
);
198 disableTheory(theory::THEORY_REWRITERULES
);
201 // these are for arithmetic
203 /** Enable the use of integers in this logic. */
204 void enableIntegers();
205 /** Disable the use of integers in this logic. */
206 void disableIntegers();
207 /** Enable the use of reals in this logic. */
209 /** Disable the use of reals in this logic. */
211 /** Only permit difference arithmetic in this logic. */
212 void arithOnlyDifference();
213 /** Only permit linear arithmetic in this logic. */
214 void arithOnlyLinear();
215 /** Permit nonlinear arithmetic in this logic. */
216 void arithNonLinear();
218 // LOCKING FUNCTIONALITY
220 /** Lock this LogicInfo, disabling further mutation and allowing queries */
221 void lock() { d_locked
= true; }
222 /** Check whether this LogicInfo is locked, disallowing further mutation */
223 bool isLocked() const { return d_locked
; }
224 /** Get a copy of this LogicInfo that is identical, but unlocked */
225 LogicInfo
getUnlockedCopy() const;
227 };/* class LogicInfo */
229 }/* CVC4 namespace */
231 #endif /* __CVC4__LOGIC_INFO_H */