enum TheoryId {
${theory_enum}
+ THEORY_QUANTIFIERS,
+ THEORY_REWRITERULES,
THEORY_LAST
};
#include "theory/bv/theory_bv.h"
#include "theory/datatypes/theory_datatypes.h"
#include "theory/theory_traits.h"
+#include "theory/logic_info.h"
#include "util/ite_removal.h"
using namespace std;
d_definedFunctions(NULL),
d_assertionList(NULL),
d_assignments(NULL),
- d_logic(""),
+ d_logic(),
+ d_logicIsSet(false),
d_problemExtended(false),
d_queryMade(false),
d_needPostsolve(false),
// We have mutual dependency here, so we add the prop engine to the theory
// engine later (it is non-essential there)
- d_theoryEngine = new TheoryEngine(d_context, d_userContext);
+ d_theoryEngine = new TheoryEngine(d_context, d_userContext, const_cast<const LogicInfo&>(d_logic));
// Add the theories
#ifdef CVC4_FOR_EACH_THEORY_STATEMENT
}
}
-void SmtEngine::setLogic(const std::string& s) throw(ModalException) {
+void SmtEngine::setLogic(const LogicInfo& logic) throw(ModalException) {
NodeManagerScope nms(d_nodeManager);
- if(d_logic != "") {
+ if(d_logicIsSet) {
throw ModalException("logic already set");
}
if(Dump.isOn("benchmark")) {
- Dump("benchmark") << SetBenchmarkLogicCommand(s);
+ Dump("benchmark") << SetBenchmarkLogicCommand(logic.getLogicString());
}
- setLogicInternal(s);
+ setLogicInternal(logic);
+}
+
+void SmtEngine::setLogic(const std::string& s) throw(ModalException) {
+ NodeManagerScope nms(d_nodeManager);
+
+ setLogic(LogicInfo(s));
}
-void SmtEngine::setLogicInternal(const std::string& s) throw() {
- d_logic = s;
+void SmtEngine::setLogicInternal(const LogicInfo& logic) throw() {
+ d_logic = logic;
// by default, symmetry breaker is on only for QF_UF
if(! Options::current()->ufSymmetryBreakerSetByUser) {
- Trace("smt") << "setting uf symmetry breaker to " << (s == "QF_UF") << std::endl;
- NodeManager::currentNM()->getOptions()->ufSymmetryBreaker = (s == "QF_UF");
+ bool qf_uf = logic.isPure(theory::THEORY_UF) && !logic.isQuantified();
+ Trace("smt") << "setting uf symmetry breaker to " << qf_uf << std::endl;
+ NodeManager::currentNM()->getOptions()->ufSymmetryBreaker = qf_uf;
}
// by default, nonclausal simplification is off for QF_SAT
if(! Options::current()->simplificationModeSetByUser) {
- Trace("smt") << "setting simplification mode to <" << s << "> " << (s != "QF_SAT") << std::endl;
- NodeManager::currentNM()->getOptions()->simplificationMode = (s == "QF_SAT" ? Options::SIMPLIFICATION_MODE_NONE : Options::SIMPLIFICATION_MODE_BATCH);
+ bool qf_sat = logic.isPure(theory::THEORY_BOOL) && !logic.isQuantified();
+ Trace("smt") << "setting simplification mode to <" << logic.getLogicString() << "> " << (!qf_sat) << std::endl;
+ NodeManager::currentNM()->getOptions()->simplificationMode = (qf_sat ? Options::SIMPLIFICATION_MODE_NONE : Options::SIMPLIFICATION_MODE_BATCH);
}
// If in arrays, set the UF handler to arrays
- if(s == "QF_AX") {
+ if(logic.isPure(theory::THEORY_ARRAY) && !logic.isQuantified()) {
theory::Theory::setUninterpretedSortOwner(theory::THEORY_ARRAY);
} else {
theory::Theory::setUninterpretedSortOwner(theory::THEORY_UF);
} else {
// The following options can only be set at the beginning; we throw
// a ModalException if someone tries.
- if(d_logic != "") {
+ if(d_logicIsSet) {
throw ModalException("logic already set; cannot set options");
}
#include "util/result.h"
#include "util/sexpr.h"
#include "util/stats.h"
+#include "theory/logic_info.h"
// In terms of abstraction, this is below (and provides services to)
// ValidityChecker and above (and requires the services of)
/**
* The logic we're in.
*/
- std::string d_logic;
+ LogicInfo d_logic;
+
+ /**
+ * Whether the logic has been set yet.
+ */
+ bool d_logicIsSet;
/**
* Whether or not we have added any assertions/declarations/definitions
/**
* Internally handle the setting of a logic.
*/
- void setLogicInternal(const std::string& logic) throw();
+ void setLogicInternal(const LogicInfo& logic) throw();
friend class ::CVC4::smt::SmtEnginePrivate;
/** how the SMT engine got the answer -- SAT solver or DE */
BackedStat<std::string> d_statResultSource;
-
public:
/**
*/
void setLogic(const std::string& logic) throw(ModalException);
+ /**
+ * Set the logic of the script.
+ */
+ void setLogic(const LogicInfo& logic) throw(ModalException);
+
/**
* Set information about the script executing.
*/
noinst_LTLIBRARIES = libtheory.la
libtheory_la_SOURCES = \
+ logic_info.h \
+ logic_info.cpp \
output_channel.h \
interrupted.h \
theory_engine.h \
--- /dev/null
+/********************* */
+/*! \file logic_info.cpp
+ ** \verbatim
+ ** Original author: mdeters
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009--2012 The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief A class giving information about a logic (group a theory modules
+ ** and configuration information)
+ **
+ ** A class giving information about a logic (group of theory modules and
+ ** configuration information).
+ **/
+
+#include <string>
+#include <cstring>
+#include <sstream>
+
+#include "expr/kind.h"
+#include "theory/logic_info.h"
+#include "util/Assert.h"
+
+using namespace std;
+using namespace CVC4::theory;
+
+namespace CVC4 {
+
+LogicInfo::LogicInfo() :
+ d_logicString(""),
+ d_theories(),
+ d_sharingTheories(0),
+ d_integers(true),
+ d_reals(true),
+ d_linear(false) {
+
+ for(TheoryId id = THEORY_FIRST; id < THEORY_LAST; ++id) {
+ d_theories[id] = false;// ensure it's cleared
+ enableTheory(id);
+ }
+}
+
+LogicInfo::LogicInfo(std::string logicString) throw(IllegalArgumentException) :
+ d_logicString(""),
+ d_theories(),
+ d_sharingTheories(0),
+ d_integers(false),
+ d_reals(false),
+ d_linear(false) {
+ setLogicString(logicString);
+}
+
+std::string LogicInfo::getLogicString() const {
+ if(d_logicString == "") {
+ size_t seen = 0; // make sure we support all the active theories
+
+ stringstream ss;
+ if(!isQuantified()) {
+ ss << "QF_";
+ }
+ if(d_theories[THEORY_ARRAY]) {
+ ss << (d_sharingTheories == 1 ? "AX" : "A");
+ ++seen;
+ }
+ if(d_theories[THEORY_UF]) {
+ ss << "UF";
+ ++seen;
+ }
+ if(d_theories[THEORY_BV]) {
+ ss << "BV";
+ ++seen;
+ }
+ if(d_theories[THEORY_DATATYPES]) {
+ ss << "DT";
+ ++seen;
+ }
+ if(d_theories[THEORY_ARITH]) {
+ if(isDifferenceLogic()) {
+ ss << (areIntegersUsed() ? "I" : "");
+ ss << (areRealsUsed() ? "R" : "");
+ ss << "DL";
+ } else {
+ ss << (isLinear() ? "L" : "N");
+ ss << (areIntegersUsed() ? "I" : "");
+ ss << (areRealsUsed() ? "R" : "");
+ ss << "A";
+ }
+ ++seen;
+ }
+
+ if(seen != d_sharingTheories) {
+ Unhandled("can't extract a logic string from LogicInfo; at least one "
+ "active theory is unknown to LogicInfo::getLogicString() !");
+ }
+
+ if(seen == 0) {
+ ss << "SAT";
+ }
+
+ d_logicString = ss.str();
+ }
+ return d_logicString;
+}
+
+void LogicInfo::setLogicString(std::string logicString) throw(IllegalArgumentException) {
+ for(TheoryId id = THEORY_FIRST; id < THEORY_LAST; ++id) {
+ d_theories[id] = false;// ensure it's cleared
+ }
+ d_sharingTheories = 0;
+
+ // Below, ONLY use enableTheory()/disableTheory() rather than
+ // accessing d_theories[] directly. This makes sure to set up
+ // sharing properly.
+
+ enableTheory(THEORY_BUILTIN);
+ enableTheory(THEORY_BOOL);
+
+ const char* p = logicString.c_str();
+ if(!strcmp(p, "QF_SAT") || *p == '\0') {
+ // propositional logic only; we're done.
+ p += 6;
+ } else {
+ if(!strncmp(p, "QF_", 3)) {
+ disableQuantifiers();
+ p += 3;
+ } else {
+ enableQuantifiers();
+ }
+ if(!strncmp(p, "AX", 2)) {
+ enableTheory(THEORY_ARRAY);
+ p += 2;
+ } else {
+ if(*p == 'A') {
+ enableTheory(THEORY_ARRAY);
+ ++p;
+ }
+ if(!strncmp(p, "UF", 2)) {
+ enableTheory(THEORY_UF);
+ p += 2;
+ }
+ if(!strncmp(p, "BV", 2)) {
+ enableTheory(THEORY_BV);
+ p += 2;
+ }
+ if(!strncmp(p, "DT", 2)) {
+ enableTheory(THEORY_DATATYPES);
+ p += 2;
+ }
+ if(!strncmp(p, "IDL", 3)) {
+ enableIntegers();
+ disableReals();
+ arithOnlyDifference();
+ p += 3;
+ } else if(!strncmp(p, "RDL", 3)) {
+ disableIntegers();
+ enableReals();
+ arithOnlyDifference();
+ p += 3;
+ } else if(!strncmp(p, "IRDL", 4)) {
+ // "IRDL" ?! --not very useful, but getLogicString() can produce
+ // that string, so we really had better be able to read it back in.
+ enableIntegers();
+ enableReals();
+ arithOnlyDifference();
+ p += 4;
+ } else if(!strncmp(p, "LIA", 3)) {
+ enableIntegers();
+ disableReals();
+ arithOnlyLinear();
+ p += 3;
+ } else if(!strncmp(p, "LRA", 3)) {
+ disableIntegers();
+ enableReals();
+ arithOnlyLinear();
+ p += 3;
+ } else if(!strncmp(p, "LIRA", 4)) {
+ enableIntegers();
+ enableReals();
+ arithOnlyLinear();
+ p += 4;
+ } else if(!strncmp(p, "NIA", 3)) {
+ enableIntegers();
+ disableReals();
+ arithNonLinear();
+ p += 3;
+ } else if(!strncmp(p, "NRA", 3)) {
+ disableIntegers();
+ enableReals();
+ arithNonLinear();
+ p += 3;
+ } else if(!strncmp(p, "NIRA", 4)) {
+ enableIntegers();
+ enableReals();
+ arithNonLinear();
+ p += 4;
+ }
+ }
+ }
+ if(*p != '\0') {
+ stringstream err;
+ err << "LogicInfo::setLogicString(): junk (\"" << p << "\") at end of logic string: " << logicString;
+ IllegalArgument(logicString, err.str().c_str());
+ }
+
+ // ensure a getLogic() returns the same thing as was set
+ d_logicString = logicString;
+}
+
+void LogicInfo::enableTheory(theory::TheoryId theory) {
+ if(!d_theories[theory]) {
+ if(isTrueTheory(theory)) {
+ ++d_sharingTheories;
+ }
+ d_logicString = "";
+ d_theories[theory] = true;
+ }
+}
+
+void LogicInfo::disableTheory(theory::TheoryId theory) {
+ if(d_theories[theory]) {
+ if(isTrueTheory(theory)) {
+ Assert(d_sharingTheories > 0);
+ --d_sharingTheories;
+ }
+ if(theory == THEORY_BUILTIN ||
+ theory == THEORY_BOOL) {
+ return;
+ }
+ d_logicString = "";
+ d_theories[theory] = false;
+ }
+}
+
+void LogicInfo::enableIntegers() {
+ d_logicString = "";
+ enableTheory(THEORY_ARITH);
+ d_integers = true;
+}
+
+void LogicInfo::disableIntegers() {
+ d_logicString = "";
+ d_integers = false;
+ if(!d_reals) {
+ disableTheory(THEORY_ARITH);
+ }
+}
+
+void LogicInfo::enableReals() {
+ d_logicString = "";
+ enableTheory(THEORY_ARITH);
+ d_reals = true;
+}
+
+void LogicInfo::disableReals() {
+ d_logicString = "";
+ d_reals = false;
+ if(!d_integers) {
+ disableTheory(THEORY_ARITH);
+ }
+}
+
+void LogicInfo::arithOnlyDifference() {
+ d_logicString = "";
+ d_linear = true;
+ d_differenceLogic = true;
+}
+
+void LogicInfo::arithOnlyLinear() {
+ d_logicString = "";
+ d_linear = true;
+ d_differenceLogic = false;
+}
+
+void LogicInfo::arithNonLinear() {
+ d_logicString = "";
+ d_linear = false;
+ d_differenceLogic = false;
+}
+
+}/* CVC4 namespace */
--- /dev/null
+/********************* */
+/*! \file logic_info.h
+ ** \verbatim
+ ** Original author: mdeters
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009--2012 The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief A class giving information about a logic (group a theory modules
+ ** and configuration information)
+ **
+ ** A class giving information about a logic (group of theory modules and
+ ** configuration information).
+ **/
+
+#include "cvc4_public.h"
+
+#ifndef __CVC4__LOGIC_INFO_H
+#define __CVC4__LOGIC_INFO_H
+
+#include <string>
+#include "expr/kind.h"
+
+namespace CVC4 {
+
+/**
+ * A LogicInfo instance describes a collection of theory modules and some
+ * basic configuration about them. Conceptually, it provides a background
+ * context for all operations in CVC4. Typically, when CVC4's SmtEngine
+ * is created, it is issued a setLogic() command indicating features of the
+ * assertions and queries to follow---for example, whether quantifiers are
+ * used, whether integers or reals (or both) will be used, etc.
+ *
+ * Most places in CVC4 will only ever need to access a const reference to an
+ * instance of this class. Such an instance is generally set by the SmtEngine
+ * when setLogic() is called. However, mutating member functions are also
+ * provided by this class so that it can be used as a more general mechanism
+ * (e.g., for communicating to the SmtEngine which theories should be used,
+ * rather than having to provide an SMT-LIB string).
+ */
+class LogicInfo {
+ mutable std::string d_logicString; /**< an SMT-LIB-like logic string */
+ bool d_theories[theory::THEORY_LAST]; /**< set of active theories */
+ size_t d_sharingTheories; /**< count of theories that need sharing */
+
+ // for arithmetic
+ bool d_integers; /**< are integers used in this logic? */
+ bool d_reals; /**< are reals used in this logic? */
+ bool d_linear; /**< linear-only arithmetic in this logic? */
+ bool d_differenceLogic; /**< difference-only arithmetic in this logic? */
+
+ /**
+ * Returns true iff this is a "true" theory (one that must be worried
+ * about for sharing
+ */
+ static inline bool isTrueTheory(theory::TheoryId theory) {
+ switch(theory) {
+ case theory::THEORY_BUILTIN:
+ case theory::THEORY_BOOL:
+ case theory::THEORY_QUANTIFIERS:
+ case theory::THEORY_REWRITERULES:
+ return false;
+ default:
+ return true;
+ }
+ }
+
+public:
+
+ /**
+ * Constructs a LogicInfo for the most general logic (quantifiers, all
+ * background theory modules, ...).
+ */
+ LogicInfo();
+
+ /**
+ * Construct a LogicInfo from an SMT-LIB-like logic string.
+ * Throws an IllegalArgumentException if the logic string cannot
+ * be interpreted.
+ */
+ LogicInfo(std::string logicString) throw(IllegalArgumentException);
+
+ // ACCESSORS
+
+ /**
+ * Get an SMT-LIB-like logic string. These are only guaranteed to
+ * be SMT-LIB-compliant if an SMT-LIB-compliant string was used in
+ * the constructor and no mutating functions were called.
+ */
+ std::string getLogicString() const;
+
+ /** Is sharing enabled for this logic? */
+ bool isSharingEnabled() const { return d_sharingTheories > 1; }
+ /** Is the given theory module active in this logic? */
+ bool isTheoryEnabled(theory::TheoryId theory) const { return d_theories[theory]; }
+
+ /** Is this a quantified logic? */
+ bool isQuantified() const {
+ return isTheoryEnabled(theory::THEORY_QUANTIFIERS) || isTheoryEnabled(theory::THEORY_REWRITERULES);
+ }
+
+ /**
+ * Is this a pure logic (only one "true" background theory). Quantifiers
+ * can exist in such logics though; to test for quantifier-free purity,
+ * use "isPure(theory) && !isQuantified()".
+ */
+ bool isPure(theory::TheoryId theory) const {
+ // the third conjuct is really just to rule out the misleading case where you ask
+ // isPure(THEORY_BOOL) and get true even in e.g. QF_LIA
+ return isTheoryEnabled(theory) && !isSharingEnabled() &&
+ ( !isTrueTheory(theory) || d_sharingTheories == 1 );
+ }
+
+ // these are for arithmetic
+
+ /** Are integers in this logic? */
+ bool areIntegersUsed() const { return d_integers; }
+ /** Are reals in this logic? */
+ bool areRealsUsed() const { return d_reals; }
+ /** Does this logic only linear arithmetic? */
+ bool isLinear() const { return d_linear || d_differenceLogic; }
+ /** Does this logic only permit difference reasoning? (implies linear) */
+ bool isDifferenceLogic() const { return d_differenceLogic; }
+
+ // MUTATORS
+
+ /**
+ * Initialize the LogicInfo with an SMT-LIB-like logic string.
+ * Throws an IllegalArgumentException if the string can't be
+ * interpreted.
+ */
+ void setLogicString(std::string logicString) throw(IllegalArgumentException);
+
+ /**
+ * Enable the given theory module.
+ */
+ void enableTheory(theory::TheoryId theory);
+
+ /**
+ * Disable the given theory module. THEORY_BUILTIN and THEORY_BOOL cannot
+ * be disabled (and if given here, the request will be silently ignored).
+ */
+ void disableTheory(theory::TheoryId theory);
+
+ /**
+ * Quantifiers are a special case, since two theory modules handle them.
+ */
+ void enableQuantifiers() {
+ enableTheory(theory::THEORY_QUANTIFIERS);
+ enableTheory(theory::THEORY_REWRITERULES);
+ }
+
+ /**
+ * Quantifiers are a special case, since two theory modules handle them.
+ */
+ void disableQuantifiers() {
+ disableTheory(theory::THEORY_QUANTIFIERS);
+ disableTheory(theory::THEORY_REWRITERULES);
+ }
+
+ // these are for arithmetic
+
+ /** Enable the use of integers in this logic. */
+ void enableIntegers();
+ /** Disable the use of integers in this logic. */
+ void disableIntegers();
+ /** Enable the use of reals in this logic. */
+ void enableReals();
+ /** Disable the use of reals in this logic. */
+ void disableReals();
+ /** Only permit difference arithmetic in this logic. */
+ void arithOnlyDifference();
+ /** Only permit linear arithmetic in this logic. */
+ void arithOnlyLinear();
+ /** Permit nonlinear arithmetic in this logic. */
+ void arithNonLinear();
+
+};/* class LogicInfo */
+
+}/* CVC4 namespace */
+
+#endif /* __CVC4__LOGIC_INFO_H */
+
}
bool PreRegisterVisitor::done(TNode node) {
- d_engine->markActive(d_theories);
return d_multipleTheories;
}
#include "theory/valuation.h"
#include "theory/substitutions.h"
#include "theory/output_channel.h"
+#include "theory/logic_info.h"
#include "context/context.h"
#include "context/cdlist.h"
#include "context/cdo.h"
*/
context::UserContext* d_userContext;
+ /**
+ * Information about the logic we're operating within.
+ */
+ const LogicInfo* d_logicInfo;
+
/**
* The assertFact() queue.
*
return fact;
}
+ const LogicInfo& getLogicInfo() const {
+ return *d_logicInfo;
+ }
+
/**
* The theory that owns the uninterpreted sort.
*/
using namespace CVC4::theory;
TheoryEngine::TheoryEngine(context::Context* context,
- context::UserContext* userContext)
+ context::UserContext* userContext,
+ const LogicInfo& logicInfo)
: d_propEngine(NULL),
d_context(context),
d_userContext(userContext),
- d_activeTheories(context, 0),
+ d_logicInfo(logicInfo),
d_notify(*this),
d_sharedTerms(d_notify, context),
d_ppCache(),
#undef CVC4_FOR_EACH_THEORY_STATEMENT
#endif
#define CVC4_FOR_EACH_THEORY_STATEMENT(THEORY) \
- if (theory::TheoryTraits<THEORY>::hasCheck && isActive(THEORY)) { \
+ if (theory::TheoryTraits<THEORY>::hasCheck && d_logicInfo.isTheoryEnabled(THEORY)) { \
reinterpret_cast<theory::TheoryTraits<THEORY>::theory_class*>(theoryOf(THEORY))->check(effort); \
if (d_inConflict) { \
break; \
Debug("theory") << "TheoryEngine::check(" << effort << "): running check" << std::endl;
if (Debug.isOn("theory::assertions")) {
- for (unsigned theoryId = 0; theoryId < THEORY_LAST; ++ theoryId) {
+ for (TheoryId theoryId = THEORY_FIRST; theoryId < THEORY_LAST; ++theoryId) {
Theory* theory = d_theoryTable[theoryId];
- if (theory && Theory::setContains((TheoryId)theoryId, d_activeTheories)) {
+ if (theory && d_logicInfo.isTheoryEnabled(theoryId)) {
Debug("theory::assertions") << "--------------------------------------------" << std::endl;
Debug("theory::assertions") << "Assertions of " << theory->getId() << ": " << std::endl;
context::CDList<Assertion>::const_iterator it = theory->facts_begin(), it_end = theory->facts_end();
#undef CVC4_FOR_EACH_THEORY_STATEMENT
#endif
#define CVC4_FOR_EACH_THEORY_STATEMENT(THEORY) \
- if (theory::TheoryTraits<THEORY>::isParametric && isActive(THEORY)) { \
+ if (theory::TheoryTraits<THEORY>::isParametric && d_logicInfo.isTheoryEnabled(THEORY)) { \
reinterpret_cast<theory::TheoryTraits<THEORY>::theory_class*>(theoryOf(THEORY))->getCareGraph(careGraph); \
}
#undef CVC4_FOR_EACH_THEORY_STATEMENT
#endif
#define CVC4_FOR_EACH_THEORY_STATEMENT(THEORY) \
- if (theory::TheoryTraits<THEORY>::hasPropagate && isActive(THEORY)) { \
+ if (theory::TheoryTraits<THEORY>::hasPropagate && d_logicInfo.isTheoryEnabled(THEORY)) { \
reinterpret_cast<theory::TheoryTraits<THEORY>::theory_class*>(theoryOf(THEORY))->propagate(effort); \
}
#undef CVC4_FOR_EACH_THEORY_STATEMENT
#endif
#define CVC4_FOR_EACH_THEORY_STATEMENT(THEORY) \
- if (theory::TheoryTraits<THEORY>::hasNotifyRestart && isActive(THEORY)) { \
+ if (theory::TheoryTraits<THEORY>::hasNotifyRestart && d_logicInfo.isTheoryEnabled(THEORY)) { \
reinterpret_cast<theory::TheoryTraits<THEORY>::theory_class*>(theoryOf(THEORY))->notifyRestart(); \
}
d_hasShutDown = true;
// Shutdown all the theories
- for(unsigned theoryId = 0; theoryId < theory::THEORY_LAST; ++theoryId) {
+ for(TheoryId theoryId = theory::THEORY_FIRST; theoryId < theory::THEORY_LAST; ++theoryId) {
if(d_theoryTable[theoryId]) {
theoryOf(static_cast<TheoryId>(theoryId))->shutdown();
}
}
}
d_sharedTerms.markNotified(term, theories);
- markActive(theories);
}
}
// TODO: have processSharedLiteral propagate disequalities?
if (node.getKind() == kind::EQUAL) {
// Don't have to assert it - this will be taken care of by processSharedLiteral
- Assert(isActive(theory->getId()));
+ Assert(d_logicInfo.isTheoryEnabled(theory->getId()));
return;
}
}
// Assert the fact to the appropriate theory and mark it active
theory->assertFact(node, true);
- markActive(Theory::setInsert(theory->getId()));
+ Assert(d_logicInfo.isTheoryEnabled(theory->getId()));
}
void TheoryEngine::propagate(TNode literal, theory::TheoryId theory) {
theory::Theory* d_theoryTable[theory::THEORY_LAST];
/**
- * A bitmap of theories that are "active" for the current run. We
- * mark a theory active when we first see a term or type belonging to
- * it. This is important because we can optimize for single-theory
- * runs (no sharing), can reduce the cost of walking the DAG on
- * registration, etc.
+ * A collection of theories that are "active" for the current run.
+ * This set is provided by the user (as a logic string, say, in SMT-LIBv2
+ * format input), or else by default it's all-inclusive. This is important
+ * because we can optimize for single-theory runs (no sharing), can reduce
+ * the cost of walking the DAG on registration, etc.
*/
- context::CDO<theory::Theory::Set> d_activeTheories;
+ const LogicInfo& d_logicInfo;
// NotifyClass: template helper class for Shared Terms Database
class NotifyClass :public SharedTermsDatabase::SharedTermsNotifyClass {
d_propEngine->spendResource();
}
- /**
- * Is the theory active.
- */
- bool isActive(theory::TheoryId theory) {
- return theory::Theory::setContains(theory, d_activeTheories);
- }
-
struct SharedLiteral {
/** The node/theory pair for the assertion */
/** THEORY_LAST indicates this is a SAT literal and should be sent to the SAT solver */
public:
/** Constructs a theory engine */
- TheoryEngine(context::Context* context, context::UserContext* userContext);
+ TheoryEngine(context::Context* context, context::UserContext* userContext, const LogicInfo& logic);
/** Destroys a theory engine */
~TheoryEngine();
Assert(d_theoryTable[theoryId] == NULL && d_theoryOut[theoryId] == NULL);
d_theoryOut[theoryId] = new EngineOutputChannel(this, theoryId);
d_theoryTable[theoryId] = new TheoryClass(d_context, d_userContext, *d_theoryOut[theoryId], theory::Valuation(this));
+ d_theoryTable[theoryId]->d_logicInfo = &d_logicInfo;
}
/**
*/
void setLogic(std::string logic);
- /**
- * Mark a theory active if it's not already.
- */
- void markActive(theory::Theory::Set theories) {
- d_activeTheories = theory::Theory::setUnion(d_activeTheories, theories);
- }
-
inline void setPropEngine(prop::PropEngine* propEngine) {
Assert(d_propEngine == NULL);
d_propEngine = propEngine;
-(set-logic QF_LIA)
+(set-logic QF_UFLIA)
(set-info :status unsat)
;; don't use a datatypes for currently focusing in uf
# All unit tests
UNIT_TESTS = \
+ theory/logic_info_white \
theory/theory_engine_white \
theory/theory_black \
theory/theory_arith_white \
/** The SAT solver proxy */
FakeSatSolver* d_satSolver;
+ /** The logic info */
+ LogicInfo* d_logicInfo;
+
/** The theory engine */
TheoryEngine* d_theoryEngine;
d_nodeManager = new NodeManager(d_context, NULL);
NodeManagerScope nms(d_nodeManager);
d_satSolver = new FakeSatSolver();
- d_theoryEngine = new TheoryEngine(d_context, d_userContext);
+ d_logicInfo = new LogicInfo();
+ d_theoryEngine = new TheoryEngine(d_context, d_userContext, *d_logicInfo);
d_theoryEngine->addTheory<theory::builtin::TheoryBuiltin>(theory::THEORY_BUILTIN);
d_theoryEngine->addTheory<theory::booleans::TheoryBool>(theory::THEORY_BOOL);
d_theoryEngine->addTheory<theory::arith::TheoryArith>(theory::THEORY_ARITH);
delete d_cnfStream;
d_theoryEngine->shutdown();
delete d_theoryEngine;
+ delete d_logicInfo;
delete d_satSolver;
delete d_nodeManager;
delete d_userContext;
--- /dev/null
+/********************* */
+/*! \file logic_info_white.h
+ ** \verbatim
+ ** Original author: mdeters
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009--2012 The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief Unit testing for CVC4::LogicInfo class
+ **
+ ** Unit testing for CVC4::LogicInfo class.
+ **/
+
+#include <cxxtest/TestSuite.h>
+
+#include "expr/kind.h"
+#include "theory/logic_info.h"
+
+using namespace CVC4;
+using namespace CVC4::theory;
+
+using namespace std;
+
+class LogicInfoWhite : public CxxTest::TestSuite {
+
+public:
+
+ void testSmtlibLogics() {
+ LogicInfo info("QF_SAT");
+ TS_ASSERT( !info.isSharingEnabled() );
+ TS_ASSERT( info.isPure( THEORY_BOOL ) );
+ TS_ASSERT( !info.isQuantified() );
+
+ info.setLogicString("AUFLIA");
+ TS_ASSERT( info.isSharingEnabled() );
+ TS_ASSERT( info.isQuantified() );
+ TS_ASSERT( info.isTheoryEnabled( THEORY_ARRAY ) );
+ TS_ASSERT( info.isTheoryEnabled( THEORY_UF ) );
+ TS_ASSERT( info.isTheoryEnabled( THEORY_ARITH ) );
+ TS_ASSERT( !info.isTheoryEnabled( THEORY_BV ) );
+ TS_ASSERT( info.isTheoryEnabled( THEORY_BOOL ) );
+ TS_ASSERT( info.isLinear() );
+ TS_ASSERT( info.areIntegersUsed() );
+ TS_ASSERT( !info.isDifferenceLogic() );
+ TS_ASSERT( !info.areRealsUsed() );
+
+ info.setLogicString("AUFLIRA");
+ TS_ASSERT( info.isSharingEnabled() );
+ TS_ASSERT( info.isQuantified() );
+ TS_ASSERT( info.isTheoryEnabled( THEORY_ARRAY ) );
+ TS_ASSERT( info.isTheoryEnabled( THEORY_UF ) );
+ TS_ASSERT( info.isTheoryEnabled( THEORY_ARITH ) );
+ TS_ASSERT( !info.isTheoryEnabled( THEORY_BV ) );
+ TS_ASSERT( info.isTheoryEnabled( THEORY_BOOL ) );
+ TS_ASSERT( info.isLinear() );
+ TS_ASSERT( info.areIntegersUsed() );
+ TS_ASSERT( !info.isDifferenceLogic() );
+ TS_ASSERT( info.areRealsUsed() );
+
+ info.setLogicString("AUFNIRA");
+ TS_ASSERT( info.isSharingEnabled() );
+ TS_ASSERT( info.isQuantified() );
+ TS_ASSERT( info.isTheoryEnabled( THEORY_ARRAY ) );
+ TS_ASSERT( info.isTheoryEnabled( THEORY_UF ) );
+ TS_ASSERT( info.isTheoryEnabled( THEORY_ARITH ) );
+ TS_ASSERT( !info.isTheoryEnabled( THEORY_BV ) );
+ TS_ASSERT( info.isTheoryEnabled( THEORY_BOOL ) );
+ TS_ASSERT( !info.isLinear() );
+ TS_ASSERT( info.areIntegersUsed() );
+ TS_ASSERT( !info.isDifferenceLogic() );
+ TS_ASSERT( info.areRealsUsed() );
+
+ info.setLogicString("LRA");
+ TS_ASSERT( !info.isSharingEnabled() );
+ TS_ASSERT( info.isQuantified() );
+ TS_ASSERT( !info.isTheoryEnabled( THEORY_ARRAY ) );
+ TS_ASSERT( !info.isTheoryEnabled( THEORY_UF ) );
+ TS_ASSERT( info.isTheoryEnabled( THEORY_ARITH ) );
+ TS_ASSERT( info.isPure( THEORY_ARITH ) );
+ TS_ASSERT( !info.isTheoryEnabled( THEORY_BV ) );
+ TS_ASSERT( info.isTheoryEnabled( THEORY_BOOL ) );
+ TS_ASSERT( info.isLinear() );
+ TS_ASSERT( !info.areIntegersUsed() );
+ TS_ASSERT( !info.isDifferenceLogic() );
+ TS_ASSERT( info.areRealsUsed() );
+
+ info.setLogicString("QF_ABV");
+ TS_ASSERT( !info.isQuantified() );
+ TS_ASSERT( info.isSharingEnabled() );
+ TS_ASSERT( info.isTheoryEnabled( THEORY_ARRAY ) );
+ TS_ASSERT( !info.isTheoryEnabled( THEORY_UF ) );
+ TS_ASSERT( !info.isTheoryEnabled( THEORY_ARITH ) );
+ TS_ASSERT( !info.isPure( THEORY_ARRAY ) );
+ TS_ASSERT( info.isTheoryEnabled( THEORY_BV ) );
+ TS_ASSERT( info.isTheoryEnabled( THEORY_BOOL ) );
+
+ info.setLogicString("QF_AUFBV");
+ TS_ASSERT( !info.isQuantified() );
+ TS_ASSERT( info.isSharingEnabled() );
+ TS_ASSERT( info.isTheoryEnabled( THEORY_ARRAY ) );
+ TS_ASSERT( info.isTheoryEnabled( THEORY_UF ) );
+ TS_ASSERT( !info.isTheoryEnabled( THEORY_ARITH ) );
+ TS_ASSERT( !info.isPure( THEORY_ARRAY ) );
+ TS_ASSERT( info.isTheoryEnabled( THEORY_BV ) );
+ TS_ASSERT( info.isTheoryEnabled( THEORY_BOOL ) );
+
+ info.setLogicString("QF_AUFLIA");
+ TS_ASSERT( !info.isQuantified() );
+ TS_ASSERT( info.isSharingEnabled() );
+ TS_ASSERT( info.isTheoryEnabled( THEORY_ARRAY ) );
+ TS_ASSERT( info.isTheoryEnabled( THEORY_UF ) );
+ TS_ASSERT( info.isTheoryEnabled( THEORY_ARITH ) );
+ TS_ASSERT( !info.isPure( THEORY_ARRAY ) );
+ TS_ASSERT( !info.isTheoryEnabled( THEORY_BV ) );
+ TS_ASSERT( info.isTheoryEnabled( THEORY_BOOL ) );
+ TS_ASSERT( info.isLinear() );
+ TS_ASSERT( info.areIntegersUsed() );
+ TS_ASSERT( !info.isDifferenceLogic() );
+ TS_ASSERT( !info.areRealsUsed() );
+
+ info.setLogicString("QF_AX");
+ TS_ASSERT( !info.isQuantified() );
+ TS_ASSERT( !info.isSharingEnabled() );
+ TS_ASSERT( info.isTheoryEnabled( THEORY_ARRAY ) );
+ TS_ASSERT( !info.isTheoryEnabled( THEORY_UF ) );
+ TS_ASSERT( !info.isTheoryEnabled( THEORY_ARITH ) );
+ TS_ASSERT( info.isPure( THEORY_ARRAY ) );
+ TS_ASSERT( !info.isTheoryEnabled( THEORY_BV ) );
+ TS_ASSERT( info.isTheoryEnabled( THEORY_BOOL ) );
+
+ info.setLogicString("QF_BV");
+ TS_ASSERT( !info.isQuantified() );
+ TS_ASSERT( !info.isSharingEnabled() );
+ TS_ASSERT( !info.isTheoryEnabled( THEORY_ARRAY ) );
+ TS_ASSERT( !info.isTheoryEnabled( THEORY_UF ) );
+ TS_ASSERT( !info.isTheoryEnabled( THEORY_ARITH ) );
+ TS_ASSERT( !info.isPure( THEORY_ARRAY ) );
+ TS_ASSERT( info.isTheoryEnabled( THEORY_BV ) );
+ TS_ASSERT( info.isTheoryEnabled( THEORY_BOOL ) );
+
+ info.setLogicString("QF_IDL");
+ TS_ASSERT( !info.isQuantified() );
+ TS_ASSERT( !info.isSharingEnabled() );
+ TS_ASSERT( !info.isTheoryEnabled( THEORY_ARRAY ) );
+ TS_ASSERT( !info.isTheoryEnabled( THEORY_UF ) );
+ TS_ASSERT( info.isTheoryEnabled( THEORY_ARITH ) );
+ TS_ASSERT( info.isPure( THEORY_ARITH ) );
+ TS_ASSERT( !info.isTheoryEnabled( THEORY_BV ) );
+ TS_ASSERT( info.isTheoryEnabled( THEORY_BOOL ) );
+ TS_ASSERT( info.isLinear() );
+ TS_ASSERT( info.isDifferenceLogic() );
+ TS_ASSERT( info.areIntegersUsed() );
+ TS_ASSERT( !info.areRealsUsed() );
+
+ info.setLogicString("QF_LIA");
+ TS_ASSERT( !info.isQuantified() );
+ TS_ASSERT( !info.isSharingEnabled() );
+ TS_ASSERT( !info.isTheoryEnabled( THEORY_ARRAY ) );
+ TS_ASSERT( !info.isTheoryEnabled( THEORY_UF ) );
+ TS_ASSERT( info.isTheoryEnabled( THEORY_ARITH ) );
+ TS_ASSERT( info.isPure( THEORY_ARITH ) );
+ TS_ASSERT( !info.isTheoryEnabled( THEORY_BV ) );
+ TS_ASSERT( info.isTheoryEnabled( THEORY_BOOL ) );
+ TS_ASSERT( info.isLinear() );
+ TS_ASSERT( !info.isDifferenceLogic() );
+ TS_ASSERT( info.areIntegersUsed() );
+ TS_ASSERT( !info.areRealsUsed() );
+
+ info.setLogicString("QF_LRA");
+ TS_ASSERT( !info.isQuantified() );
+ TS_ASSERT( !info.isSharingEnabled() );
+ TS_ASSERT( !info.isTheoryEnabled( THEORY_ARRAY ) );
+ TS_ASSERT( !info.isTheoryEnabled( THEORY_UF ) );
+ TS_ASSERT( info.isTheoryEnabled( THEORY_ARITH ) );
+ TS_ASSERT( info.isPure( THEORY_ARITH ) );
+ TS_ASSERT( !info.isTheoryEnabled( THEORY_BV ) );
+ TS_ASSERT( info.isTheoryEnabled( THEORY_BOOL ) );
+ TS_ASSERT( info.isLinear() );
+ TS_ASSERT( !info.isDifferenceLogic() );
+ TS_ASSERT( !info.areIntegersUsed() );
+ TS_ASSERT( info.areRealsUsed() );
+
+ info.setLogicString("QF_NIA");
+ TS_ASSERT( !info.isQuantified() );
+ TS_ASSERT( !info.isSharingEnabled() );
+ TS_ASSERT( !info.isTheoryEnabled( THEORY_ARRAY ) );
+ TS_ASSERT( !info.isTheoryEnabled( THEORY_UF ) );
+ TS_ASSERT( info.isTheoryEnabled( THEORY_ARITH ) );
+ TS_ASSERT( info.isPure( THEORY_ARITH ) );
+ TS_ASSERT( !info.isTheoryEnabled( THEORY_BV ) );
+ TS_ASSERT( info.isTheoryEnabled( THEORY_BOOL ) );
+ TS_ASSERT( !info.isLinear() );
+ TS_ASSERT( !info.isDifferenceLogic() );
+ TS_ASSERT( info.areIntegersUsed() );
+ TS_ASSERT( !info.areRealsUsed() );
+
+ info.setLogicString("QF_NRA");
+ TS_ASSERT( !info.isQuantified() );
+ TS_ASSERT( !info.isSharingEnabled() );
+ TS_ASSERT( !info.isTheoryEnabled( THEORY_ARRAY ) );
+ TS_ASSERT( !info.isTheoryEnabled( THEORY_UF ) );
+ TS_ASSERT( info.isTheoryEnabled( THEORY_ARITH ) );
+ TS_ASSERT( info.isPure( THEORY_ARITH ) );
+ TS_ASSERT( !info.isTheoryEnabled( THEORY_BV ) );
+ TS_ASSERT( info.isTheoryEnabled( THEORY_BOOL ) );
+ TS_ASSERT( !info.isLinear() );
+ TS_ASSERT( !info.isDifferenceLogic() );
+ TS_ASSERT( !info.areIntegersUsed() );
+ TS_ASSERT( info.areRealsUsed() );
+
+ info.setLogicString("QF_RDL");
+ TS_ASSERT( !info.isQuantified() );
+ TS_ASSERT( !info.isSharingEnabled() );
+ TS_ASSERT( !info.isTheoryEnabled( THEORY_ARRAY ) );
+ TS_ASSERT( !info.isTheoryEnabled( THEORY_UF ) );
+ TS_ASSERT( info.isTheoryEnabled( THEORY_ARITH ) );
+ TS_ASSERT( info.isPure( THEORY_ARITH ) );
+ TS_ASSERT( !info.isTheoryEnabled( THEORY_BV ) );
+ TS_ASSERT( info.isTheoryEnabled( THEORY_BOOL ) );
+ TS_ASSERT( info.isLinear() );
+ TS_ASSERT( info.isDifferenceLogic() );
+ TS_ASSERT( !info.areIntegersUsed() );
+ TS_ASSERT( info.areRealsUsed() );
+
+ info.setLogicString("QF_UF");
+ TS_ASSERT( !info.isQuantified() );
+ TS_ASSERT( !info.isSharingEnabled() );
+ TS_ASSERT( !info.isTheoryEnabled( THEORY_ARRAY ) );
+ TS_ASSERT( info.isTheoryEnabled( THEORY_UF ) );
+ TS_ASSERT( !info.isTheoryEnabled( THEORY_ARITH ) );
+ TS_ASSERT( !info.isPure( THEORY_ARITH ) );
+ TS_ASSERT( info.isPure( THEORY_UF ) );
+ TS_ASSERT( !info.isTheoryEnabled( THEORY_BV ) );
+ TS_ASSERT( info.isTheoryEnabled( THEORY_BOOL ) );
+
+ info.setLogicString("QF_UFBV");
+ TS_ASSERT( !info.isQuantified() );
+ TS_ASSERT( info.isSharingEnabled() );
+ TS_ASSERT( !info.isTheoryEnabled( THEORY_ARRAY ) );
+ TS_ASSERT( info.isTheoryEnabled( THEORY_UF ) );
+ TS_ASSERT( !info.isTheoryEnabled( THEORY_ARITH ) );
+ TS_ASSERT( !info.isPure( THEORY_ARITH ) );
+ TS_ASSERT( !info.isPure( THEORY_BV ) );
+ TS_ASSERT( info.isTheoryEnabled( THEORY_BV ) );
+ TS_ASSERT( info.isTheoryEnabled( THEORY_BOOL ) );
+
+ info.setLogicString("QF_UFIDL");
+ TS_ASSERT( !info.isQuantified() );
+ TS_ASSERT( info.isSharingEnabled() );
+ TS_ASSERT( !info.isTheoryEnabled( THEORY_ARRAY ) );
+ TS_ASSERT( info.isTheoryEnabled( THEORY_UF ) );
+ TS_ASSERT( info.isTheoryEnabled( THEORY_ARITH ) );
+ TS_ASSERT( !info.isPure( THEORY_ARITH ) );
+ TS_ASSERT( !info.isTheoryEnabled( THEORY_BV ) );
+ TS_ASSERT( info.isTheoryEnabled( THEORY_BOOL ) );
+ TS_ASSERT( info.isLinear() );
+ TS_ASSERT( info.isDifferenceLogic() );
+ TS_ASSERT( info.areIntegersUsed() );
+ TS_ASSERT( !info.areRealsUsed() );
+
+ info.setLogicString("QF_UFLIA");
+ TS_ASSERT( !info.isQuantified() );
+ TS_ASSERT( info.isSharingEnabled() );
+ TS_ASSERT( !info.isTheoryEnabled( THEORY_ARRAY ) );
+ TS_ASSERT( info.isTheoryEnabled( THEORY_UF ) );
+ TS_ASSERT( info.isTheoryEnabled( THEORY_ARITH ) );
+ TS_ASSERT( !info.isPure( THEORY_ARITH ) );
+ TS_ASSERT( !info.isTheoryEnabled( THEORY_BV ) );
+ TS_ASSERT( info.isTheoryEnabled( THEORY_BOOL ) );
+ TS_ASSERT( info.isLinear() );
+ TS_ASSERT( !info.isDifferenceLogic() );
+ TS_ASSERT( info.areIntegersUsed() );
+ TS_ASSERT( !info.areRealsUsed() );
+
+ info.setLogicString("QF_UFLRA");
+ TS_ASSERT( !info.isQuantified() );
+ TS_ASSERT( info.isSharingEnabled() );
+ TS_ASSERT( !info.isTheoryEnabled( THEORY_ARRAY ) );
+ TS_ASSERT( info.isTheoryEnabled( THEORY_UF ) );
+ TS_ASSERT( info.isTheoryEnabled( THEORY_ARITH ) );
+ TS_ASSERT( !info.isPure( THEORY_ARITH ) );
+ TS_ASSERT( !info.isTheoryEnabled( THEORY_BV ) );
+ TS_ASSERT( info.isTheoryEnabled( THEORY_BOOL ) );
+ TS_ASSERT( info.isLinear() );
+ TS_ASSERT( !info.isDifferenceLogic() );
+ TS_ASSERT( !info.areIntegersUsed() );
+ TS_ASSERT( info.areRealsUsed() );
+
+ info.setLogicString("QF_UFNRA");
+ TS_ASSERT( !info.isQuantified() );
+ TS_ASSERT( info.isSharingEnabled() );
+ TS_ASSERT( !info.isTheoryEnabled( THEORY_ARRAY ) );
+ TS_ASSERT( info.isTheoryEnabled( THEORY_UF ) );
+ TS_ASSERT( info.isTheoryEnabled( THEORY_ARITH ) );
+ TS_ASSERT( !info.isPure( THEORY_ARITH ) );
+ TS_ASSERT( !info.isTheoryEnabled( THEORY_BV ) );
+ TS_ASSERT( info.isTheoryEnabled( THEORY_BOOL ) );
+ TS_ASSERT( !info.isLinear() );
+ TS_ASSERT( !info.isDifferenceLogic() );
+ TS_ASSERT( !info.areIntegersUsed() );
+ TS_ASSERT( info.areRealsUsed() );
+
+ info.setLogicString("UFLRA");
+ TS_ASSERT( info.isQuantified() );
+ TS_ASSERT( info.isSharingEnabled() );
+ TS_ASSERT( !info.isTheoryEnabled( THEORY_ARRAY ) );
+ TS_ASSERT( info.isTheoryEnabled( THEORY_UF ) );
+ TS_ASSERT( info.isTheoryEnabled( THEORY_ARITH ) );
+ TS_ASSERT( !info.isPure( THEORY_ARITH ) );
+ TS_ASSERT( !info.isTheoryEnabled( THEORY_BV ) );
+ TS_ASSERT( info.isTheoryEnabled( THEORY_BOOL ) );
+ TS_ASSERT( info.isLinear() );
+ TS_ASSERT( !info.isDifferenceLogic() );
+ TS_ASSERT( !info.areIntegersUsed() );
+ TS_ASSERT( info.areRealsUsed() );
+
+ info.setLogicString("UFNIA");
+ TS_ASSERT( info.isQuantified() );
+ TS_ASSERT( info.isSharingEnabled() );
+ TS_ASSERT( !info.isTheoryEnabled( THEORY_ARRAY ) );
+ TS_ASSERT( info.isTheoryEnabled( THEORY_UF ) );
+ TS_ASSERT( info.isTheoryEnabled( THEORY_ARITH ) );
+ TS_ASSERT( !info.isPure( THEORY_ARITH ) );
+ TS_ASSERT( !info.isTheoryEnabled( THEORY_BV ) );
+ TS_ASSERT( info.isTheoryEnabled( THEORY_BOOL ) );
+ TS_ASSERT( !info.isLinear() );
+ TS_ASSERT( !info.isDifferenceLogic() );
+ TS_ASSERT( info.areIntegersUsed() );
+ TS_ASSERT( !info.areRealsUsed() );
+ }
+
+ void testDefaultLogic() {
+ LogicInfo info;
+ TS_ASSERT_EQUALS( info.getLogicString(), "AUFBVDTNIRA" );
+ TS_ASSERT( info.isSharingEnabled() );
+ TS_ASSERT( info.isTheoryEnabled( THEORY_BUILTIN ) );
+ TS_ASSERT( info.isTheoryEnabled( THEORY_BOOL ) );
+ TS_ASSERT( info.isTheoryEnabled( THEORY_UF ) );
+ TS_ASSERT( info.isTheoryEnabled( THEORY_ARITH ) );
+ TS_ASSERT( info.isTheoryEnabled( THEORY_ARRAY ) );
+ TS_ASSERT( info.isTheoryEnabled( THEORY_BV ) );
+ TS_ASSERT( info.isTheoryEnabled( THEORY_DATATYPES ) );
+ TS_ASSERT( info.isTheoryEnabled( THEORY_QUANTIFIERS ) );
+ TS_ASSERT( info.isTheoryEnabled( THEORY_REWRITERULES ) );
+ TS_ASSERT( ! info.isPure( THEORY_BUILTIN ) );
+ TS_ASSERT( ! info.isPure( THEORY_BOOL ) );
+ TS_ASSERT( ! info.isPure( THEORY_UF ) );
+ TS_ASSERT( ! info.isPure( THEORY_ARITH ) );
+ TS_ASSERT( ! info.isPure( THEORY_ARRAY ) );
+ TS_ASSERT( ! info.isPure( THEORY_BV ) );
+ TS_ASSERT( ! info.isPure( THEORY_DATATYPES ) );
+ TS_ASSERT( ! info.isPure( THEORY_QUANTIFIERS ) );
+ TS_ASSERT( ! info.isPure( THEORY_REWRITERULES ) );
+ TS_ASSERT( info.isQuantified() );
+ TS_ASSERT( info.areIntegersUsed() );
+ TS_ASSERT( info.areRealsUsed() );
+ TS_ASSERT( ! info.isLinear() );
+
+ info.arithOnlyLinear();
+ info.disableIntegers();
+ TS_ASSERT_EQUALS( info.getLogicString(), "AUFBVDTLRA" );
+ info.disableQuantifiers();
+ TS_ASSERT_EQUALS( info.getLogicString(), "QF_AUFBVDTLRA" );
+ info.disableTheory(THEORY_BV);
+ info.disableTheory(THEORY_DATATYPES);
+ info.enableIntegers();
+ info.disableReals();
+ TS_ASSERT_EQUALS( info.getLogicString(), "QF_AUFLIA" );
+ info.disableTheory(THEORY_ARITH);
+ info.disableTheory(THEORY_UF);
+ TS_ASSERT_EQUALS( info.getLogicString(), "QF_AX" );
+ TS_ASSERT( info.isPure( THEORY_ARRAY ) );
+ TS_ASSERT( ! info.isQuantified() );
+ }
+
+};/* class LogicInfoWhite */
+
NodeManagerScope* d_scope;
FakeOutputChannel *d_nullChannel;
TheoryEngine* d_theoryEngine;
+ LogicInfo* d_logicInfo;
public:
d_nullChannel = new FakeOutputChannel();
// create the TheoryEngine
- d_theoryEngine = new TheoryEngine(d_ctxt, d_uctxt);
+ d_logicInfo = new LogicInfo();
+ d_theoryEngine = new TheoryEngine(d_ctxt, d_uctxt, *d_logicInfo);
d_theoryEngine->addTheory< FakeTheory<THEORY_BUILTIN> >(THEORY_BUILTIN);
d_theoryEngine->addTheory< FakeTheory<THEORY_BOOL> >(THEORY_BOOL);
void tearDown() {
d_theoryEngine->shutdown();
delete d_theoryEngine;
+ delete d_logicInfo;
delete d_nullChannel;
projects / cvc5.git / commitdiff