diff options
Diffstat (limited to 'src/theory/arith')
-rw-r--r-- | src/theory/arith/congruence_manager.cpp | 41 | ||||
-rw-r--r-- | src/theory/arith/congruence_manager.h | 22 | ||||
-rw-r--r-- | src/theory/arith/theory_arith.cpp | 14 | ||||
-rw-r--r-- | src/theory/arith/theory_arith.h | 17 | ||||
-rw-r--r-- | src/theory/arith/theory_arith_private.cpp | 30 | ||||
-rw-r--r-- | src/theory/arith/theory_arith_private.h | 14 |
6 files changed, 91 insertions, 47 deletions
diff --git a/src/theory/arith/congruence_manager.cpp b/src/theory/arith/congruence_manager.cpp index ab3b485a8..a70339c01 100644 --- a/src/theory/arith/congruence_manager.cpp +++ b/src/theory/arith/congruence_manager.cpp @@ -42,16 +42,29 @@ ArithCongruenceManager::ArithCongruenceManager( d_constraintDatabase(cd), d_setupLiteral(setup), d_avariables(avars), - d_ee(d_notify, c, "theory::arith::ArithCongruenceManager", true) + d_ee(nullptr) { - d_ee.addFunctionKind(kind::NONLINEAR_MULT); - d_ee.addFunctionKind(kind::EXPONENTIAL); - d_ee.addFunctionKind(kind::SINE); - d_ee.addFunctionKind(kind::IAND); } ArithCongruenceManager::~ArithCongruenceManager() {} +bool ArithCongruenceManager::needsEqualityEngine(EeSetupInfo& esi) +{ + esi.d_notify = &d_notify; + esi.d_name = "theory::arith::ArithCongruenceManager"; + return true; +} + +void ArithCongruenceManager::finishInit(eq::EqualityEngine* ee) +{ + Assert(ee != nullptr); + d_ee = ee; + d_ee->addFunctionKind(kind::NONLINEAR_MULT); + d_ee->addFunctionKind(kind::EXPONENTIAL); + d_ee->addFunctionKind(kind::SINE); + d_ee->addFunctionKind(kind::IAND); +} + ArithCongruenceManager::Statistics::Statistics(): d_watchedVariables("theory::arith::congruence::watchedVariables", 0), d_watchedVariableIsZero("theory::arith::congruence::watchedVariableIsZero", 0), @@ -141,10 +154,6 @@ bool ArithCongruenceManager::canExplain(TNode n) const { return d_explanationMap.find(n) != d_explanationMap.end(); } -void ArithCongruenceManager::setMasterEqualityEngine(eq::EqualityEngine* eq) { - d_ee.setMasterEqualityEngine(eq); -} - Node ArithCongruenceManager::externalToInternal(TNode n) const{ Assert(canExplain(n)); ExplainMap::const_iterator iter = d_explanationMap.find(n); @@ -320,9 +329,9 @@ bool ArithCongruenceManager::propagate(TNode x){ void ArithCongruenceManager::explain(TNode literal, std::vector<TNode>& assumptions) { if (literal.getKind() != kind::NOT) { - d_ee.explainEquality(literal[0], literal[1], true, assumptions); + d_ee->explainEquality(literal[0], literal[1], true, assumptions); } else { - d_ee.explainEquality(literal[0][0], literal[0][1], false, assumptions); + d_ee->explainEquality(literal[0][0], literal[0][1], false, assumptions); } } @@ -392,9 +401,9 @@ void ArithCongruenceManager::assertionToEqualityEngine(bool isEquality, ArithVar Trace("arith-ee") << "Assert " << eq << ", pol " << isEquality << ", reason " << reason << std::endl; if(isEquality){ - d_ee.assertEquality(eq, true, reason); + d_ee->assertEquality(eq, true, reason); }else{ - d_ee.assertEquality(eq, false, reason); + d_ee->assertEquality(eq, false, reason); } } @@ -417,7 +426,7 @@ void ArithCongruenceManager::equalsConstant(ConstraintCP c){ d_keepAlive.push_back(reason); Trace("arith-ee") << "Assert equalsConstant " << eq << ", reason " << reason << std::endl; - d_ee.assertEquality(eq, true, reason); + d_ee->assertEquality(eq, true, reason); } void ArithCongruenceManager::equalsConstant(ConstraintCP lb, ConstraintCP ub){ @@ -441,11 +450,11 @@ void ArithCongruenceManager::equalsConstant(ConstraintCP lb, ConstraintCP ub){ d_keepAlive.push_back(reason); Trace("arith-ee") << "Assert equalsConstant2 " << eq << ", reason " << reason << std::endl; - d_ee.assertEquality(eq, true, reason); + d_ee->assertEquality(eq, true, reason); } void ArithCongruenceManager::addSharedTerm(Node x){ - d_ee.addTriggerTerm(x, THEORY_ARITH); + d_ee->addTriggerTerm(x, THEORY_ARITH); } }/* CVC4::theory::arith namespace */ diff --git a/src/theory/arith/congruence_manager.h b/src/theory/arith/congruence_manager.h index aeb72ec94..f3b5641b4 100644 --- a/src/theory/arith/congruence_manager.h +++ b/src/theory/arith/congruence_manager.h @@ -95,7 +95,8 @@ private: const ArithVariables& d_avariables; - eq::EqualityEngine d_ee; + /** The equality engine being used by this class */ + eq::EqualityEngine* d_ee; void raiseConflict(Node conflict); public: @@ -108,8 +109,6 @@ public: bool canExplain(TNode n) const; - void setMasterEqualityEngine(eq::EqualityEngine* eq); - private: Node externalToInternal(TNode n) const; @@ -138,6 +137,19 @@ public: ArithCongruenceManager(context::Context* satContext, ConstraintDatabase&, SetupLiteralCallBack, const ArithVariables&, RaiseEqualityEngineConflict raiseConflict); ~ArithCongruenceManager(); + //--------------------------------- initialization + /** + * Returns true if we need an equality engine, see + * Theory::needsEqualityEngine. + */ + bool needsEqualityEngine(EeSetupInfo& esi); + /** + * Finish initialize. This class is instructed by TheoryArithPrivate to use + * the equality engine ee. + */ + void finishInit(eq::EqualityEngine* ee); + //--------------------------------- end initialization + Node explain(TNode literal); void explain(TNode lit, NodeBuilder<>& out); @@ -166,10 +178,8 @@ public: void addSharedTerm(Node x); - - eq::EqualityEngine * getEqualityEngine() { return &d_ee; } -private: + private: class Statistics { public: IntStat d_watchedVariables; diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp index bc6e18a83..b95b5e243 100644 --- a/src/theory/arith/theory_arith.cpp +++ b/src/theory/arith/theory_arith.cpp @@ -56,10 +56,10 @@ TheoryRewriter* TheoryArith::getTheoryRewriter() return d_internal->getTheoryRewriter(); } -void TheoryArith::preRegisterTerm(TNode n){ - d_internal->preRegisterTerm(n); +bool TheoryArith::needsEqualityEngine(EeSetupInfo& esi) +{ + return d_internal->needsEqualityEngine(esi); } - void TheoryArith::finishInit() { if (getLogicInfo().isTheoryEnabled(THEORY_ARITH) @@ -72,17 +72,17 @@ void TheoryArith::finishInit() d_valuation.setUnevaluatedKind(kind::SINE); d_valuation.setUnevaluatedKind(kind::PI); } + // finish initialize internally + d_internal->finishInit(); } +void TheoryArith::preRegisterTerm(TNode n) { d_internal->preRegisterTerm(n); } + TrustNode TheoryArith::expandDefinition(Node node) { return d_internal->expandDefinition(node); } -void TheoryArith::setMasterEqualityEngine(eq::EqualityEngine* eq) { - d_internal->setMasterEqualityEngine(eq); -} - 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 30de7bbad..ad3b91b07 100644 --- a/src/theory/arith/theory_arith.h +++ b/src/theory/arith/theory_arith.h @@ -55,19 +55,28 @@ class TheoryArith : public Theory { ProofNodeManager* pnm = nullptr); virtual ~TheoryArith(); + //--------------------------------- initialization + /** get the official theory rewriter of this theory */ TheoryRewriter* getTheoryRewriter() override; + /** + * Returns true if this theory needs an equality engine, which is assigned + * to it (d_equalityEngine) by the equality engine manager during + * TheoryEngine::finishInit, prior to calling finishInit for this theory. + * If this method returns true, it stores instructions for the notifications + * this Theory wishes to receive from its equality engine. + */ + bool needsEqualityEngine(EeSetupInfo& esi) override; + /** finish initialization */ + void finishInit() override; + //--------------------------------- end initialization /** * Does non-context dependent setup for a node connected to a theory. */ void preRegisterTerm(TNode n) override; - void finishInit() override; - TrustNode expandDefinition(Node node) override; - void setMasterEqualityEngine(eq::EqualityEngine* eq) override; - void check(Effort e) override; bool needsCheckLastEffort() override; void propagate(Effort e) override; diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp index 6f47ffb0e..8ca99d369 100644 --- a/src/theory/arith/theory_arith_private.cpp +++ b/src/theory/arith/theory_arith_private.cpp @@ -134,7 +134,7 @@ TheoryArithPrivate::TheoryArithPrivate(TheoryArith& containing, d_linEq, d_errorSet, RaiseConflict(*this), TempVarMalloc(*this)), d_attemptSolSimplex( d_linEq, d_errorSet, RaiseConflict(*this), TempVarMalloc(*this)), - d_nonlinearExtension(NULL), + d_nonlinearExtension(nullptr), d_pass1SDP(NULL), d_otherSDP(NULL), d_lastContextIntegerAttempted(c, -1), @@ -159,12 +159,6 @@ TheoryArithPrivate::TheoryArithPrivate(TheoryArith& containing, d_statistics(), d_opElim(pnm, logicInfo) { - // only need to create if non-linear logic - if (logicInfo.isTheoryEnabled(THEORY_ARITH) && !logicInfo.isLinear()) - { - d_nonlinearExtension = new nl::NonlinearExtension( - containing, d_congruenceManager.getEqualityEngine()); - } } TheoryArithPrivate::~TheoryArithPrivate(){ @@ -173,6 +167,24 @@ TheoryArithPrivate::~TheoryArithPrivate(){ if(d_nonlinearExtension != NULL) { delete d_nonlinearExtension; } } +TheoryRewriter* TheoryArithPrivate::getTheoryRewriter() { return &d_rewriter; } +bool TheoryArithPrivate::needsEqualityEngine(EeSetupInfo& esi) +{ + return d_congruenceManager.needsEqualityEngine(esi); +} +void TheoryArithPrivate::finishInit() +{ + eq::EqualityEngine* ee = d_containing.getEqualityEngine(); + Assert(ee != nullptr); + d_congruenceManager.finishInit(ee); + const LogicInfo& logicInfo = getLogicInfo(); + // only need to create nonlinear extension if non-linear logic + if (logicInfo.isTheoryEnabled(THEORY_ARITH) && !logicInfo.isLinear()) + { + d_nonlinearExtension = new nl::NonlinearExtension(d_containing, ee); + } +} + static bool contains(const ConstraintCPVec& v, ConstraintP con){ for(unsigned i = 0, N = v.size(); i < N; ++i){ if(v[i] == con){ @@ -227,10 +239,6 @@ static void resolve(ConstraintCPVec& buf, ConstraintP c, const ConstraintCPVec& // return safeConstructNary(nb); } -void TheoryArithPrivate::setMasterEqualityEngine(eq::EqualityEngine* eq) { - d_congruenceManager.setMasterEqualityEngine(eq); -} - TheoryArithPrivate::ModelException::ModelException(TNode n, const char* msg) { stringstream ss; diff --git a/src/theory/arith/theory_arith_private.h b/src/theory/arith/theory_arith_private.h index 42ec7f47b..4c4aedf00 100644 --- a/src/theory/arith/theory_arith_private.h +++ b/src/theory/arith/theory_arith_private.h @@ -427,7 +427,17 @@ private: ProofNodeManager* pnm); ~TheoryArithPrivate(); - TheoryRewriter* getTheoryRewriter() { return &d_rewriter; } + //--------------------------------- initialization + /** get the official theory rewriter of this theory */ + TheoryRewriter* getTheoryRewriter(); + /** + * Returns true if we need an equality engine, see + * Theory::needsEqualityEngine. + */ + bool needsEqualityEngine(EeSetupInfo& esi); + /** finish initialize */ + void finishInit(); + //--------------------------------- end initialization /** * Does non-context dependent setup for a node connected to a theory. @@ -435,8 +445,6 @@ private: void preRegisterTerm(TNode n); TrustNode expandDefinition(Node node); - void setMasterEqualityEngine(eq::EqualityEngine* eq); - void check(Theory::Effort e); bool needsCheckLastEffort(); void propagate(Theory::Effort e); |