diff options
30 files changed, 96 insertions, 57 deletions
diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp index 395d51d3e..239385bfc 100644 --- a/src/theory/arith/theory_arith.cpp +++ b/src/theory/arith/theory_arith.cpp @@ -25,9 +25,9 @@ namespace CVC4 { namespace theory { namespace arith { -TheoryArith::TheoryArith(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo, QuantifiersEngine* qe) - : Theory(THEORY_ARITH, c, u, out, valuation, logicInfo, qe) - , d_internal(new TheoryArithPrivate(*this, c, u, out, valuation, logicInfo, qe)) +TheoryArith::TheoryArith(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo) + : Theory(THEORY_ARITH, c, u, out, valuation, logicInfo) + , d_internal(new TheoryArithPrivate(*this, c, u, out, valuation, logicInfo)) {} TheoryArith::~TheoryArith(){ @@ -42,6 +42,11 @@ void TheoryArith::setMasterEqualityEngine(eq::EqualityEngine* eq) { d_internal->setMasterEqualityEngine(eq); } +void TheoryArith::setQuantifiersEngine(QuantifiersEngine* qe) { + this->Theory::setQuantifiersEngine(qe); + d_internal->setQuantifiersEngine(qe); +} + void TheoryArith::addSharedTerm(TNode n){ d_internal->addSharedTerm(n); } diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h index 2408094d8..428c101a6 100644 --- a/src/theory/arith/theory_arith.h +++ b/src/theory/arith/theory_arith.h @@ -45,7 +45,7 @@ private: KEEP_STATISTIC(TimerStat, d_ppRewriteTimer, "theory::arith::ppRewriteTimer"); public: - TheoryArith(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo, QuantifiersEngine* qe); + TheoryArith(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo); virtual ~TheoryArith(); /** @@ -54,6 +54,7 @@ public: void preRegisterTerm(TNode n); void setMasterEqualityEngine(eq::EqualityEngine* eq); + void setQuantifiersEngine(QuantifiersEngine* qe); void check(Effort e); void propagate(Effort e); diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp index 002d503d0..40a336a4a 100644 --- a/src/theory/arith/theory_arith_private.cpp +++ b/src/theory/arith/theory_arith_private.cpp @@ -82,7 +82,7 @@ namespace CVC4 { namespace theory { namespace arith { -TheoryArithPrivate::TheoryArithPrivate(TheoryArith& containing, context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo, QuantifiersEngine* qe) : +TheoryArithPrivate::TheoryArithPrivate(TheoryArith& containing, context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo) : d_containing(containing), d_nlIncomplete( false), d_rowTracking(), @@ -91,7 +91,7 @@ TheoryArithPrivate::TheoryArithPrivate(TheoryArith& containing, context::Context d_unknownsInARow(0), d_hasDoneWorkSinceCut(false), d_learner(u), - d_quantEngine(qe), + d_quantEngine(NULL), d_assertionsThatDoNotMatchTheirLiterals(c), d_nextIntegerCheckVar(0), d_constantIntegerVariables(c), @@ -132,6 +132,10 @@ void TheoryArithPrivate::setMasterEqualityEngine(eq::EqualityEngine* eq) { d_congruenceManager.setMasterEqualityEngine(eq); } +void TheoryArithPrivate::setQuantifiersEngine(QuantifiersEngine* qe) { + d_quantEngine = qe; +} + Node TheoryArithPrivate::getRealDivideBy0Func(){ Assert(!getLogicInfo().isLinear()); Assert(getLogicInfo().areRealsUsed()); diff --git a/src/theory/arith/theory_arith_private.h b/src/theory/arith/theory_arith_private.h index 710610346..7ff93b021 100644 --- a/src/theory/arith/theory_arith_private.h +++ b/src/theory/arith/theory_arith_private.h @@ -350,7 +350,7 @@ private: Node ppRewriteTerms(TNode atom); public: - TheoryArithPrivate(TheoryArith& containing, context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo, QuantifiersEngine* qe); + TheoryArithPrivate(TheoryArith& containing, context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo); ~TheoryArithPrivate(); /** @@ -359,6 +359,7 @@ public: void preRegisterTerm(TNode n); void setMasterEqualityEngine(eq::EqualityEngine* eq); + void setQuantifiersEngine(QuantifiersEngine* qe); void check(Theory::Effort e); void propagate(Theory::Effort e); diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp index 3aee02316..b82216378 100644 --- a/src/theory/arrays/theory_arrays.cpp +++ b/src/theory/arrays/theory_arrays.cpp @@ -49,8 +49,8 @@ const bool d_solveWrite2 = false; //bool d_lazyRIntro1 = true; //bool d_eagerIndexSplitting = false; -TheoryArrays::TheoryArrays(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo, QuantifiersEngine* qe) : - Theory(THEORY_ARRAY, c, u, out, valuation, logicInfo, qe), +TheoryArrays::TheoryArrays(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo) : + Theory(THEORY_ARRAY, c, u, out, valuation, logicInfo), d_numRow("theory::arrays::number of Row lemmas", 0), d_numExt("theory::arrays::number of Ext lemmas", 0), d_numProp("theory::arrays::number of propagations", 0), diff --git a/src/theory/arrays/theory_arrays.h b/src/theory/arrays/theory_arrays.h index e0191ccc9..a4029dc2e 100644 --- a/src/theory/arrays/theory_arrays.h +++ b/src/theory/arrays/theory_arrays.h @@ -128,7 +128,7 @@ class TheoryArrays : public Theory { public: - TheoryArrays(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo, QuantifiersEngine* qe); + TheoryArrays(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo); ~TheoryArrays(); void setMasterEqualityEngine(eq::EqualityEngine* eq); diff --git a/src/theory/booleans/theory_bool.h b/src/theory/booleans/theory_bool.h index 49bf905c0..a8c904fe3 100644 --- a/src/theory/booleans/theory_bool.h +++ b/src/theory/booleans/theory_bool.h @@ -28,8 +28,8 @@ namespace booleans { class TheoryBool : public Theory { public: - TheoryBool(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo, QuantifiersEngine* qe) : - Theory(THEORY_BOOL, c, u, out, valuation, logicInfo, qe) { + TheoryBool(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo) : + Theory(THEORY_BOOL, c, u, out, valuation, logicInfo) { } PPAssertStatus ppAssert(TNode in, SubstitutionMap& outSubstitutions); diff --git a/src/theory/builtin/theory_builtin.h b/src/theory/builtin/theory_builtin.h index b49147c91..3bc0a2ce1 100644 --- a/src/theory/builtin/theory_builtin.h +++ b/src/theory/builtin/theory_builtin.h @@ -27,8 +27,8 @@ namespace builtin { class TheoryBuiltin : public Theory { public: - TheoryBuiltin(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo, QuantifiersEngine* qe) : - Theory(THEORY_BUILTIN, c, u, out, valuation, logicInfo, qe) {} + TheoryBuiltin(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo) : + Theory(THEORY_BUILTIN, c, u, out, valuation, logicInfo) {} std::string identify() const { return std::string("TheoryBuiltin"); } };/* class TheoryBuiltin */ diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp index 14a19f2d0..6daf99c8b 100644 --- a/src/theory/bv/theory_bv.cpp +++ b/src/theory/bv/theory_bv.cpp @@ -35,8 +35,8 @@ using namespace CVC4::context; using namespace std; using namespace CVC4::theory::bv::utils; -TheoryBV::TheoryBV(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo, QuantifiersEngine* qe) - : Theory(THEORY_BV, c, u, out, valuation, logicInfo, qe), +TheoryBV::TheoryBV(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo) + : Theory(THEORY_BV, c, u, out, valuation, logicInfo), d_context(c), d_alreadyPropagatedSet(c), d_sharedTermsSet(c), diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h index 90093edfd..3d093c861 100644 --- a/src/theory/bv/theory_bv.h +++ b/src/theory/bv/theory_bv.h @@ -48,7 +48,7 @@ class TheoryBV : public Theory { __gnu_cxx::hash_map<SubTheory, SubtheorySolver*, std::hash<int> > d_subtheoryMap; public: - TheoryBV(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo, QuantifiersEngine* qe); + TheoryBV(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo); ~TheoryBV(); void setMasterEqualityEngine(eq::EqualityEngine* eq); diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp index 3c9fd7bd2..a3339f9a9 100644 --- a/src/theory/datatypes/theory_datatypes.cpp +++ b/src/theory/datatypes/theory_datatypes.cpp @@ -39,8 +39,8 @@ using namespace CVC4::theory; using namespace CVC4::theory::datatypes; -TheoryDatatypes::TheoryDatatypes(Context* c, UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo, QuantifiersEngine* qe) : - Theory(THEORY_DATATYPES, c, u, out, valuation, logicInfo, qe), +TheoryDatatypes::TheoryDatatypes(Context* c, UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo) : + Theory(THEORY_DATATYPES, c, u, out, valuation, logicInfo), d_cycle_check(c), d_hasSeenCycle(c, false), d_infer(c), diff --git a/src/theory/datatypes/theory_datatypes.h b/src/theory/datatypes/theory_datatypes.h index 4f061507c..d094451b8 100644 --- a/src/theory/datatypes/theory_datatypes.h +++ b/src/theory/datatypes/theory_datatypes.h @@ -181,8 +181,9 @@ protected: /** compute care graph */ void computeCareGraph(); public: - TheoryDatatypes(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, - const LogicInfo& logicInfo, QuantifiersEngine* qe); + TheoryDatatypes(context::Context* c, context::UserContext* u, + OutputChannel& out, Valuation valuation, + const LogicInfo& logicInfo); ~TheoryDatatypes(); void setMasterEqualityEngine(eq::EqualityEngine* eq); diff --git a/src/theory/example/theory_uf_tim.cpp b/src/theory/example/theory_uf_tim.cpp index 03748d567..20f190486 100644 --- a/src/theory/example/theory_uf_tim.cpp +++ b/src/theory/example/theory_uf_tim.cpp @@ -25,8 +25,8 @@ using namespace CVC4::theory; using namespace CVC4::theory::uf; using namespace CVC4::theory::uf::tim; -TheoryUFTim::TheoryUFTim(Context* c, UserContext* u, OutputChannel& out, Valuation valuation, QuantifiersEngine* qe) : - Theory(THEORY_UF, c, u, out, valuation, qe), +TheoryUFTim::TheoryUFTim(Context* c, UserContext* u, OutputChannel& out, Valuation valuation) : + Theory(THEORY_UF, c, u, out, valuation), d_assertions(c), d_pending(c), d_currentPendingIdx(c,0), diff --git a/src/theory/example/theory_uf_tim.h b/src/theory/example/theory_uf_tim.h index 64639bbfa..d24c0787d 100644 --- a/src/theory/example/theory_uf_tim.h +++ b/src/theory/example/theory_uf_tim.h @@ -83,7 +83,7 @@ private: public: /** Constructs a new instance of TheoryUF w.r.t. the provided context.*/ - TheoryUFTim(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, QuantifiersEngine* qe); + TheoryUFTim(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation); /** Destructor for the TheoryUF object. */ ~TheoryUFTim(); diff --git a/src/theory/idl/theory_idl.cpp b/src/theory/idl/theory_idl.cpp index 987973bf3..11aa2d8a5 100644 --- a/src/theory/idl/theory_idl.cpp +++ b/src/theory/idl/theory_idl.cpp @@ -29,8 +29,8 @@ using namespace theory; using namespace idl; TheoryIdl::TheoryIdl(context::Context* c, context::UserContext* u, OutputChannel& out, - Valuation valuation, const LogicInfo& logicInfo, QuantifiersEngine* qe) -: Theory(THEORY_ARITH, c, u, out, valuation, logicInfo, qe) + Valuation valuation, const LogicInfo& logicInfo) +: Theory(THEORY_ARITH, c, u, out, valuation, logicInfo) , d_model(c) , d_assertionsDB(c) {} diff --git a/src/theory/idl/theory_idl.h b/src/theory/idl/theory_idl.h index 4597d4c6a..1eea28069 100644 --- a/src/theory/idl/theory_idl.h +++ b/src/theory/idl/theory_idl.h @@ -45,7 +45,7 @@ public: /** Theory constructor. */ TheoryIdl(context::Context* c, context::UserContext* u, OutputChannel& out, - Valuation valuation, const LogicInfo& logicInfo, QuantifiersEngine* qe); + Valuation valuation, const LogicInfo& logicInfo); /** Pre-processing of input atoms */ Node ppRewrite(TNode atom); diff --git a/src/theory/quantifiers/theory_quantifiers.cpp b/src/theory/quantifiers/theory_quantifiers.cpp index e72242fe9..6a3a6fca1 100644 --- a/src/theory/quantifiers/theory_quantifiers.cpp +++ b/src/theory/quantifiers/theory_quantifiers.cpp @@ -33,8 +33,8 @@ using namespace CVC4::context; using namespace CVC4::theory; using namespace CVC4::theory::quantifiers; -TheoryQuantifiers::TheoryQuantifiers(Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo, QuantifiersEngine* qe) : - Theory(THEORY_QUANTIFIERS, c, u, out, valuation, logicInfo, qe), +TheoryQuantifiers::TheoryQuantifiers(Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo) : + Theory(THEORY_QUANTIFIERS, c, u, out, valuation, logicInfo), d_numRestarts(0), d_masterEqualityEngine(0) { diff --git a/src/theory/quantifiers/theory_quantifiers.h b/src/theory/quantifiers/theory_quantifiers.h index 8ebde136d..8ace5f181 100644 --- a/src/theory/quantifiers/theory_quantifiers.h +++ b/src/theory/quantifiers/theory_quantifiers.h @@ -54,7 +54,7 @@ private: eq::EqualityEngine* d_masterEqualityEngine; public: - TheoryQuantifiers(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo, QuantifiersEngine* qe); + TheoryQuantifiers(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo); ~TheoryQuantifiers(); void setMasterEqualityEngine(eq::EqualityEngine* eq); diff --git a/src/theory/rewriterules/theory_rewriterules.cpp b/src/theory/rewriterules/theory_rewriterules.cpp index 0a89e2518..df74ea8b3 100644 --- a/src/theory/rewriterules/theory_rewriterules.cpp +++ b/src/theory/rewriterules/theory_rewriterules.cpp @@ -129,12 +129,11 @@ TheoryRewriteRules::TheoryRewriteRules(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, - const LogicInfo& logicInfo, - QuantifiersEngine* qe) : - Theory(THEORY_REWRITERULES, c, u, out, valuation, logicInfo, qe), + const LogicInfo& logicInfo) : + Theory(THEORY_REWRITERULES, c, u, out, valuation, logicInfo), d_rules(c), d_ruleinsts(c), d_guardeds(c), d_checkLevel(c,0), d_explanations(c), d_ruleinsts_to_add(), d_ppAssert_on(false) - { +{ d_true = NodeManager::currentNM()->mkConst<bool>(true); d_false = NodeManager::currentNM()->mkConst<bool>(false); } diff --git a/src/theory/rewriterules/theory_rewriterules.h b/src/theory/rewriterules/theory_rewriterules.h index a542214b2..ea9eb4769 100644 --- a/src/theory/rewriterules/theory_rewriterules.h +++ b/src/theory/rewriterules/theory_rewriterules.h @@ -198,8 +198,7 @@ private: context::UserContext* u, OutputChannel& out, Valuation valuation, - const LogicInfo& logicInfo, - QuantifiersEngine* qe); + const LogicInfo& logicInfo); /** Usual function for theories */ void check(Theory::Effort e); diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index 231173058..dbda080cc 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -33,8 +33,8 @@ namespace CVC4 { namespace theory { namespace strings { -TheoryStrings::TheoryStrings(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo, QuantifiersEngine* qe) - : Theory(THEORY_STRINGS, c, u, out, valuation, logicInfo, qe), +TheoryStrings::TheoryStrings(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo) + : Theory(THEORY_STRINGS, c, u, out, valuation, logicInfo), d_notify( *this ), d_equalityEngine(d_notify, c, "theory::strings::TheoryStrings"), d_conflict( c, false ), diff --git a/src/theory/strings/theory_strings.h b/src/theory/strings/theory_strings.h index c0a979cb0..824dbcb37 100644 --- a/src/theory/strings/theory_strings.h +++ b/src/theory/strings/theory_strings.h @@ -42,7 +42,7 @@ class TheoryStrings : public Theory { typedef context::CDHashMap<Node, int, NodeHashFunction> NodeIntMap; public: - TheoryStrings(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo, QuantifiersEngine* qe); + TheoryStrings(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo); ~TheoryStrings(); void setMasterEqualityEngine(eq::EqualityEngine* eq); diff --git a/src/theory/theory.h b/src/theory/theory.h index 43d35ac9d..2359d5d86 100644 --- a/src/theory/theory.h +++ b/src/theory/theory.h @@ -239,8 +239,7 @@ protected: * Construct a Theory. */ Theory(TheoryId id, context::Context* satContext, context::UserContext* userContext, - OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo, - QuantifiersEngine* qe, eq::EqualityEngine* master = 0) throw() + OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo) throw() : d_id(id) , d_satContext(satContext) , d_userContext(userContext) @@ -248,8 +247,8 @@ protected: , d_facts(satContext) , d_factsHead(satContext, 0) , d_sharedTermsIndex(satContext, 0) - , d_careGraph(0) - , d_quantEngine(qe) + , d_careGraph(NULL) + , d_quantEngine(NULL) , d_computeCareGraphTime(statName(id, "computeCareGraphTime")) , d_sharedTerms(satContext) , d_out(&out) @@ -474,6 +473,14 @@ public: } /** + * Finish theory initialization. At this point, options and the logic + * setting are final, and the master equality engine and quantifiers + * engine (if any) are initialized. This base class implementation + * does nothing. + */ + virtual void finishInit() { } + + /** * Pre-register a term. Done one time for a Node, ever. */ virtual void preRegisterTerm(TNode) { } @@ -498,6 +505,13 @@ public: virtual void setMasterEqualityEngine(eq::EqualityEngine* eq) { } /** + * Called to set the quantifiers engine. + */ + virtual void setQuantifiersEngine(QuantifiersEngine* qe) { + d_quantEngine = qe; + } + + /** * Return the current theory care graph. Theories should overload computeCareGraph to do * the actual computation, and use addCarePair to add pairs to the care graph. */ diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index ff84e63b7..47ba50aad 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -60,6 +60,9 @@ using namespace CVC4; using namespace CVC4::theory; void TheoryEngine::finishInit() { + // initialize the quantifiers engine + d_quantEngine = new QuantifiersEngine(d_context, d_userContext, this); + if (d_logicInfo.isQuantified()) { d_quantEngine->finishInit(); Assert(d_masterEqualityEngine == 0); @@ -67,10 +70,17 @@ void TheoryEngine::finishInit() { for(TheoryId theoryId = theory::THEORY_FIRST; theoryId != theory::THEORY_LAST; ++ theoryId) { if (d_theoryTable[theoryId]) { + d_theoryTable[theoryId]->setQuantifiersEngine(d_quantEngine); d_theoryTable[theoryId]->setMasterEqualityEngine(d_masterEqualityEngine); } } } + + for(TheoryId theoryId = theory::THEORY_FIRST; theoryId != theory::THEORY_LAST; ++ theoryId) { + if (d_theoryTable[theoryId]) { + d_theoryTable[theoryId]->finishInit(); + } + } } void TheoryEngine::eqNotifyNewClass(TNode t){ @@ -146,9 +156,6 @@ TheoryEngine::TheoryEngine(context::Context* context, d_theoryOut[theoryId] = NULL; } - // initialize the quantifiers engine - d_quantEngine = new QuantifiersEngine(context, userContext, this); - // build model information if applicable d_curr_model = new theory::TheoryModel(userContext, "DefaultModel", true); d_curr_model_builder = new theory::TheoryEngineModelBuilder(this); diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index 8f292e008..d5de8e3b2 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -488,7 +488,7 @@ public: inline void addTheory(theory::TheoryId theoryId) { 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_logicInfo, getQuantifiersEngine()); + d_theoryTable[theoryId] = new TheoryClass(d_context, d_userContext, *d_theoryOut[theoryId], theory::Valuation(this), d_logicInfo); } inline void setPropEngine(prop::PropEngine* propEngine) { diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp index fd46ed7f4..bb948d785 100644 --- a/src/theory/uf/theory_uf.cpp +++ b/src/theory/uf/theory_uf.cpp @@ -28,12 +28,12 @@ using namespace CVC4::theory; using namespace CVC4::theory::uf; /** Constructs a new instance of TheoryUF w.r.t. the provided context.*/ -TheoryUF::TheoryUF(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo, QuantifiersEngine* qe) : - Theory(THEORY_UF, c, u, out, valuation, logicInfo, qe), +TheoryUF::TheoryUF(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo) : + Theory(THEORY_UF, c, u, out, valuation, logicInfo), d_notify(*this), /* The strong theory solver can be notified by EqualityEngine::init(), * so make sure it's initialized first. */ - d_thss(options::finiteModelFind() ? new StrongSolverTheoryUF(c, u, out, this) : NULL), + d_thss(NULL), d_equalityEngine(d_notify, c, "theory::uf::TheoryUF"), d_conflict(c, false), d_literalsToPropagate(c), @@ -49,6 +49,13 @@ void TheoryUF::setMasterEqualityEngine(eq::EqualityEngine* eq) { d_equalityEngine.setMasterEqualityEngine(eq); } +void TheoryUF::finishInit() { + // initialize the strong solver + if (options::finiteModelFind()) { + d_thss = new StrongSolverTheoryUF(getSatContext(), getUserContext(), *d_out, this); + } +} + static Node mkAnd(const std::vector<TNode>& conjunctions) { Assert(conjunctions.size() > 0); diff --git a/src/theory/uf/theory_uf.h b/src/theory/uf/theory_uf.h index 2c9b4b7d5..b9ca17154 100644 --- a/src/theory/uf/theory_uf.h +++ b/src/theory/uf/theory_uf.h @@ -174,7 +174,7 @@ private: public: /** Constructs a new instance of TheoryUF w.r.t. the provided context.*/ - TheoryUF(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo, QuantifiersEngine* qe); + TheoryUF(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo); ~TheoryUF() { // destruct all ppRewrite() callbacks @@ -186,6 +186,7 @@ public: } void setMasterEqualityEngine(eq::EqualityEngine* eq); + void finishInit(); void check(Effort); void preRegisterTerm(TNode term); diff --git a/test/unit/theory/theory_arith_white.h b/test/unit/theory/theory_arith_white.h index 3247b8c73..c99c66fff 100644 --- a/test/unit/theory/theory_arith_white.h +++ b/test/unit/theory/theory_arith_white.h @@ -115,7 +115,7 @@ public: d_smt->d_theoryEngine->d_theoryTable[THEORY_ARITH] = NULL; d_smt->d_theoryEngine->d_theoryOut[THEORY_ARITH] = NULL; - d_arith = new TheoryArith(d_ctxt, d_uctxt, d_outputChannel, Valuation(NULL), d_logicInfo, d_smt->d_theoryEngine->d_quantEngine); + d_arith = new TheoryArith(d_ctxt, d_uctxt, d_outputChannel, Valuation(NULL), d_logicInfo); preregistered = new std::set<Node>(); diff --git a/test/unit/theory/theory_engine_white.h b/test/unit/theory/theory_engine_white.h index 99dc17594..803b24527 100644 --- a/test/unit/theory/theory_engine_white.h +++ b/test/unit/theory/theory_engine_white.h @@ -120,8 +120,8 @@ class FakeTheory : public Theory { // static std::deque<RewriteItem> s_expected; public: - FakeTheory(context::Context* ctxt, context::UserContext* uctxt, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo, QuantifiersEngine* qe) : - Theory(theoryId, ctxt, uctxt, out, valuation, logicInfo, qe) + FakeTheory(context::Context* ctxt, context::UserContext* uctxt, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo) : + Theory(theoryId, ctxt, uctxt, out, valuation, logicInfo) { } /** Register an expected rewrite call */ diff --git a/test/unit/theory/theory_white.h b/test/unit/theory/theory_white.h index a824a3f68..e2dfcc464 100644 --- a/test/unit/theory/theory_white.h +++ b/test/unit/theory/theory_white.h @@ -119,8 +119,8 @@ public: set<Node> d_registered; vector<Node> d_getSequence; - DummyTheory(Context* ctxt, UserContext* uctxt, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo, QuantifiersEngine* qe) : - Theory(theory::THEORY_BUILTIN, ctxt, uctxt, out, valuation, logicInfo, qe) { + DummyTheory(Context* ctxt, UserContext* uctxt, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo) : + Theory(theory::THEORY_BUILTIN, ctxt, uctxt, out, valuation, logicInfo) { } void registerTerm(TNode n) { @@ -196,7 +196,7 @@ public: d_smt->d_theoryEngine->d_theoryTable[THEORY_BUILTIN] = NULL; d_smt->d_theoryEngine->d_theoryOut[THEORY_BUILTIN] = NULL; - d_dummy = new DummyTheory(d_ctxt, d_uctxt, d_outputChannel, Valuation(NULL), *d_logicInfo, NULL); + d_dummy = new DummyTheory(d_ctxt, d_uctxt, d_outputChannel, Valuation(NULL), *d_logicInfo); d_outputChannel.clear(); atom0 = d_nm->mkConst(true); atom1 = d_nm->mkConst(false); |