summaryrefslogtreecommitdiff
path: root/src/theory/arith
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/arith')
-rw-r--r--src/theory/arith/congruence_manager.cpp41
-rw-r--r--src/theory/arith/congruence_manager.h22
-rw-r--r--src/theory/arith/theory_arith.cpp14
-rw-r--r--src/theory/arith/theory_arith.h17
-rw-r--r--src/theory/arith/theory_arith_private.cpp30
-rw-r--r--src/theory/arith/theory_arith_private.h14
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);
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback