diff options
Diffstat (limited to 'src/theory/arith')
-rw-r--r-- | src/theory/arith/congruence_manager.cpp | 34 | ||||
-rw-r--r-- | src/theory/arith/congruence_manager.h | 42 | ||||
-rw-r--r-- | src/theory/arith/theory_arith.cpp | 4 |
3 files changed, 42 insertions, 38 deletions
diff --git a/src/theory/arith/congruence_manager.cpp b/src/theory/arith/congruence_manager.cpp index 201eb08e7..39468e928 100644 --- a/src/theory/arith/congruence_manager.cpp +++ b/src/theory/arith/congruence_manager.cpp @@ -1,5 +1,4 @@ #include "theory/arith/congruence_manager.h" -#include "theory/uf/equality_engine_impl.h" #include "theory/arith/constraint.h" #include "theory/arith/arith_utilities.h" @@ -17,8 +16,7 @@ ArithCongruenceManager::ArithCongruenceManager(context::Context* c, ConstraintDa d_constraintDatabase(cd), d_setupLiteral(setup), d_av2Node(av2Node), - d_ee(d_notify, c, "theory::arith::ArithCongruenceManager"), - d_false(mkBoolNode(false)) + d_ee(d_notify, c, "theory::arith::ArithCongruenceManager") {} ArithCongruenceManager::Statistics::Statistics(): @@ -113,7 +111,7 @@ bool ArithCongruenceManager::propagate(TNode x){ }else{ ++(d_statistics.d_conflicts); - Node conf = explainInternal(x); + Node conf = flattenAnd(explainInternal(x)); d_conflict.set(conf); Debug("arith::congruenceManager") << "rewritten to false "<<x<<" with explanation "<< conf << std::endl; return false; @@ -181,20 +179,11 @@ bool ArithCongruenceManager::propagate(TNode x){ } void ArithCongruenceManager::explain(TNode literal, std::vector<TNode>& assumptions) { - TNode lhs, rhs; - switch (literal.getKind()) { - case kind::EQUAL: - lhs = literal[0]; - rhs = literal[1]; - break; - case kind::NOT: - lhs = literal[0]; - rhs = d_false; - break; - default: - Unreachable(); + if (literal.getKind() != kind::NOT) { + d_ee.explainEquality(literal[0], literal[1], true, assumptions); + } else { + d_ee.explainEquality(literal[0][0], literal[0][1], false, assumptions); } - d_ee.explainEquality(lhs, rhs, assumptions); } void ArithCongruenceManager::enqueueIntoNB(const std::set<TNode> s, NodeBuilder<>& nb){ @@ -258,13 +247,10 @@ void ArithCongruenceManager::assertionToEqualityEngine(bool isEquality, ArithVar TNode eq = d_watchedEqualities[s]; Assert(eq.getKind() == kind::EQUAL); - TNode x = eq[0]; - TNode y = eq[1]; - if(isEquality){ - d_ee.addEquality(x, y, reason); + d_ee.assertEquality(eq, true, reason); }else{ - d_ee.addDisequality(x, y, reason); + d_ee.assertEquality(eq, false, reason); } } @@ -286,7 +272,7 @@ void ArithCongruenceManager::equalsConstant(Constraint c){ Node reason = c->explainForConflict(); d_keepAlive.push_back(reason); - d_ee.addEquality(xAsNode, asRational, reason); + d_ee.assertEquality(eq, true, reason); } void ArithCongruenceManager::equalsConstant(Constraint lb, Constraint ub){ @@ -310,7 +296,7 @@ void ArithCongruenceManager::equalsConstant(Constraint lb, Constraint ub){ d_keepAlive.push_back(reason); - d_ee.addEquality(xAsNode, asRational, reason); + d_ee.assertEquality(eq, true, reason); } void ArithCongruenceManager::addSharedTerm(Node x){ diff --git a/src/theory/arith/congruence_manager.h b/src/theory/arith/congruence_manager.h index a72989498..18ecbeb9d 100644 --- a/src/theory/arith/congruence_manager.h +++ b/src/theory/arith/congruence_manager.h @@ -37,24 +37,43 @@ private: ArithVarToNodeMap d_watchedEqualities; - class ArithCongruenceNotify { + class ArithCongruenceNotify : public eq::EqualityEngineNotify { private: ArithCongruenceManager& d_acm; public: ArithCongruenceNotify(ArithCongruenceManager& acm): d_acm(acm) {} - bool notify(TNode propagation) { - Debug("arith::congruences") << "ArithCongruenceNotify::notify(" << propagation << ")" << std::endl; - // Just forward to dm - return d_acm.propagate(propagation); + bool eqNotifyTriggerEquality(TNode equality, bool value) { + Debug("arith::congruences") << "ArithCongruenceNotify::eqNotifyTriggerEquality(" << equality << ", " << (value ? "true" : "false") << ")" << std::endl; + if (value) { + return d_acm.propagate(equality); + } else { + return d_acm.propagate(equality.notNode()); + } } - void notify(TNode t1, TNode t2) { - Debug("arith::congruences") << "ArithCongruenceNotify::notify(" << t1 << ", " << t2 << ")" << std::endl; - Node equality = t1.eqNode(t2); - d_acm.propagate(equality); + bool eqNotifyTriggerPredicate(TNode predicate, bool value) { + Unreachable(); } - }; + + bool eqNotifyTriggerTermEquality(TNode t1, TNode t2, bool value) { + Debug("arith::congruences") << "ArithCongruenceNotify::eqNotifyTriggerTermEquality(" << t1 << ", " << t2 << ", " << (value ? "true" : "false") << ")" << std::endl; + if (value) { + return d_acm.propagate(t1.eqNode(t2)); + } else { + return d_acm.propagate(t1.eqNode(t2).notNode()); + } + } + + bool eqNotifyConstantTermMerge(TNode t1, TNode t2) { + Debug("arith::congruences") << "ArithCongruenceNotify::eqNotifyConstantTermMerge(" << t1 << ", " << t2 << std::endl; + if (t1.getKind() == kind::CONST_BOOLEAN) { + return d_acm.propagate(t1.iffNode(t2)); + } else { + return d_acm.propagate(t1.eqNode(t2)); + } + } + }; ArithCongruenceNotify d_notify; context::CDList<Node> d_keepAlive; @@ -75,8 +94,7 @@ private: const ArithVarNodeMap& d_av2Node; - theory::uf::EqualityEngine<ArithCongruenceNotify> d_ee; - Node d_false; + eq::EqualityEngine d_ee; public: diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp index c7072de72..6bb3821da 100644 --- a/src/theory/arith/theory_arith.cpp +++ b/src/theory/arith/theory_arith.cpp @@ -1001,8 +1001,8 @@ Node TheoryArith::assertionCases(TNode assertion){ if(Debug.isOn("whytheoryenginewhy")){ debugPrintFacts(); } - Warning() << "arith: Theory engine is sending me both a literal and its negation?" - << "BOOOOOOOOOOOOOOOOOOOOOO!!!!"<< endl; +// Warning() << "arith: Theory engine is sending me both a literal and its negation?" +// << "BOOOOOOOOOOOOOOOOOOOOOO!!!!"<< endl; } Debug("arith::eq") << constraint << endl; Debug("arith::eq") << negation << endl; |