diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/expr/kind_template.h | 2 | ||||
| -rw-r--r-- | src/smt/smt_engine.cpp | 38 | ||||
| -rw-r--r-- | src/smt/smt_engine.h | 16 | ||||
| -rw-r--r-- | src/theory/Makefile.am | 2 | ||||
| -rw-r--r-- | src/theory/logic_info.cpp | 285 | ||||
| -rw-r--r-- | src/theory/logic_info.h | 188 | ||||
| -rw-r--r-- | src/theory/term_registration_visitor.cpp | 1 | ||||
| -rw-r--r-- | src/theory/theory.h | 10 | ||||
| -rw-r--r-- | src/theory/theory_engine.cpp | 24 | ||||
| -rw-r--r-- | src/theory/theory_engine.h | 29 |
10 files changed, 544 insertions, 51 deletions
diff --git a/src/expr/kind_template.h b/src/expr/kind_template.h index 973163d62..fb76c1857 100644 --- a/src/expr/kind_template.h +++ b/src/expr/kind_template.h @@ -124,6 +124,8 @@ namespace theory { enum TheoryId { ${theory_enum} + THEORY_QUANTIFIERS, + THEORY_REWRITERULES, THEORY_LAST }; diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index c95b9d197..4b3410cf7 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -57,6 +57,7 @@ #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; @@ -230,7 +231,8 @@ SmtEngine::SmtEngine(ExprManager* em) throw(AssertionException) : 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), @@ -256,7 +258,7 @@ SmtEngine::SmtEngine(ExprManager* em) throw(AssertionException) : // 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 @@ -356,36 +358,44 @@ SmtEngine::~SmtEngine() throw() { } } -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); @@ -513,7 +523,7 @@ void SmtEngine::setOption(const std::string& key, const SExpr& value) } 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"); } diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h index 7feaa7e61..43d3e1125 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -37,6 +37,7 @@ #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) @@ -131,7 +132,12 @@ class CVC4_PUBLIC SmtEngine { /** * 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 @@ -212,7 +218,7 @@ class CVC4_PUBLIC SmtEngine { /** * 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; @@ -226,7 +232,6 @@ class CVC4_PUBLIC SmtEngine { /** how the SMT engine got the answer -- SAT solver or DE */ BackedStat<std::string> d_statResultSource; - public: /** @@ -245,6 +250,11 @@ 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. */ void setInfo(const std::string& key, const SExpr& value) diff --git a/src/theory/Makefile.am b/src/theory/Makefile.am index eb289937f..4a077450c 100644 --- a/src/theory/Makefile.am +++ b/src/theory/Makefile.am @@ -9,6 +9,8 @@ DIST_SUBDIRS = $(SUBDIRS) example noinst_LTLIBRARIES = libtheory.la libtheory_la_SOURCES = \ + logic_info.h \ + logic_info.cpp \ output_channel.h \ interrupted.h \ theory_engine.h \ diff --git a/src/theory/logic_info.cpp b/src/theory/logic_info.cpp new file mode 100644 index 000000000..ba7119071 --- /dev/null +++ b/src/theory/logic_info.cpp @@ -0,0 +1,285 @@ +/********************* */ +/*! \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 */ diff --git a/src/theory/logic_info.h b/src/theory/logic_info.h new file mode 100644 index 000000000..560b72509 --- /dev/null +++ b/src/theory/logic_info.h @@ -0,0 +1,188 @@ +/********************* */ +/*! \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 */ + diff --git a/src/theory/term_registration_visitor.cpp b/src/theory/term_registration_visitor.cpp index 1e7222532..db95edfa0 100644 --- a/src/theory/term_registration_visitor.cpp +++ b/src/theory/term_registration_visitor.cpp @@ -93,7 +93,6 @@ void PreRegisterVisitor::start(TNode node) { } bool PreRegisterVisitor::done(TNode node) { - d_engine->markActive(d_theories); return d_multipleTheories; } diff --git a/src/theory/theory.h b/src/theory/theory.h index 2b91da3b2..d0218236d 100644 --- a/src/theory/theory.h +++ b/src/theory/theory.h @@ -27,6 +27,7 @@ #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" @@ -139,6 +140,11 @@ private: context::UserContext* d_userContext; /** + * Information about the logic we're operating within. + */ + const LogicInfo* d_logicInfo; + + /** * The assertFact() queue. * * These can not be TNodes as some atoms (such as equalities) are sent @@ -257,6 +263,10 @@ protected: return fact; } + const LogicInfo& getLogicInfo() const { + return *d_logicInfo; + } + /** * The theory that owns the uninterpreted sort. */ diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index 46a9f5855..d5616221d 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -38,11 +38,12 @@ using namespace CVC4; 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(), @@ -110,7 +111,7 @@ void TheoryEngine::check(Theory::Effort effort) { #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; \ @@ -135,9 +136,9 @@ void TheoryEngine::check(Theory::Effort effort) { 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(); @@ -248,7 +249,7 @@ void TheoryEngine::combineTheories() { #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); \ } @@ -309,7 +310,7 @@ void TheoryEngine::propagate(Theory::Effort effort) { #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); \ } @@ -447,7 +448,7 @@ void TheoryEngine::notifyRestart() { #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(); \ } @@ -482,7 +483,7 @@ void TheoryEngine::shutdown() { 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(); } @@ -642,7 +643,6 @@ void TheoryEngine::assertFact(TNode node) } } d_sharedTerms.markNotified(term, theories); - markActive(theories); } } @@ -665,7 +665,7 @@ void TheoryEngine::assertFact(TNode node) // 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; } } @@ -678,7 +678,7 @@ void TheoryEngine::assertFact(TNode node) // 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) { diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index faa6bbd26..5dfc4c36c 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -90,13 +90,13 @@ class TheoryEngine { 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 { @@ -309,13 +309,6 @@ class TheoryEngine { 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 */ @@ -469,7 +462,7 @@ class TheoryEngine { 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(); @@ -483,6 +476,7 @@ public: 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; } /** @@ -491,13 +485,6 @@ public: */ 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; |