From: Dejan Jovanović Date: Mon, 12 Dec 2011 09:47:37 +0000 (+0000) Subject: * merging some uf stuff from incremental_work branch that somehow nobody merged-in X-Git-Tag: cvc5-1.0.0~8359 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=6d04f19e1c1fbf7714fbb95dc62648ac44b419dd;p=cvc5.git * merging some uf stuff from incremental_work branch that somehow nobody merged-in * since two theories can propagate the same literal minisat now explicitly checks that a propagated literal has not been asserted yet --- diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc index 8a883b1cb..e1a8ded8e 100644 --- a/src/prop/minisat/core/Solver.cc +++ b/src/prop/minisat/core/Solver.cc @@ -698,9 +698,18 @@ CRef Solver::propagate(TheoryCheckType type) void Solver::propagateTheory() { std::vector propagatedLiterals; proxy->theoryPropagate(propagatedLiterals); + int oldTrailSize = trail.size(); for (unsigned i = 0, i_end = propagatedLiterals.size(); i < i_end; ++ i) { Debug("minisat") << "Theory propagated: " << propagatedLiterals[i] << std::endl; - uncheckedEnqueue(propagatedLiterals[i], CRef_Lazy); + // multiple theories can propagate the same literal + Lit p = propagatedLiterals[i]; + if (value(p) == l_Undef) { + uncheckedEnqueue(p, CRef_Lazy); + } else { + // but we check that this is the case and that they agree + Assert(trail_index(var(p)) >= oldTrailSize); + Assert(value(p) == lbool(!sign(p))); + } } } diff --git a/src/theory/arith/difference_manager.cpp b/src/theory/arith/difference_manager.cpp index dfb07bcf4..f366116d4 100644 --- a/src/theory/arith/difference_manager.cpp +++ b/src/theory/arith/difference_manager.cpp @@ -33,7 +33,7 @@ void DifferenceManager::explain(TNode literal, std::vector& assumptions) default: Unreachable(); } - d_ee.getExplanation(lhs, rhs, assumptions); + d_ee.explainEquality(lhs, rhs, assumptions); } #warning "Stolen from theory_uf.h verbatim. Generalize me!" diff --git a/src/theory/uf/equality_engine.h b/src/theory/uf/equality_engine.h index 13b8898d5..01ae6bfb4 100644 --- a/src/theory/uf/equality_engine.h +++ b/src/theory/uf/equality_engine.h @@ -613,9 +613,16 @@ public: /** * Get an explanation of the equality t1 = t2. Returns the asserted equalities that * imply t1 = t2. Returns TNodes as the assertion equalities should be hashed somewhere - * else. TODO: mark the phantom equalities (skolems). + * else. + */ + void explainEquality(TNode t1, TNode t2, std::vector& equalities) const; + + /** + * Get an explanation of the equality t1 = t2. Returns the asserted equalities that + * imply t1 = t2. Returns TNodes as the assertion equalities should be hashed somewhere + * else. */ - void getExplanation(TNode t1, TNode t2, std::vector& equalities) const; + void explainDisequality(TNode t1, TNode t2, std::vector& equalities) const; /** * Add term to the trigger terms. The notify class will get notified when two diff --git a/src/theory/uf/equality_engine_impl.h b/src/theory/uf/equality_engine_impl.h index 77c8e80b4..61823c143 100644 --- a/src/theory/uf/equality_engine_impl.h +++ b/src/theory/uf/equality_engine_impl.h @@ -549,10 +549,17 @@ std::string EqualityEngine::edgesToString(EqualityEdgeId edgeId) co } template -void EqualityEngine::getExplanation(TNode t1, TNode t2, std::vector& equalities) const { - Debug("equality") << "EqualityEngine::getExplanation(" << t1 << "," << t2 << ")" << std::endl; - - Assert(getRepresentative(t1) == getRepresentative(t2)); +void EqualityEngine::explainEquality(TNode t1, TNode t2, std::vector& equalities) const { + Debug("equality") << "EqualityEngine::explainEquality(" << t1 << "," << t2 << ")" << std::endl; + + Assert(getRepresentative(t1) == getRepresentative(t2), + "Cannot explain an equality, because the two terms are not equal!\n" + "The representative of %s\n" + " is %s\n" + "The representative of %s\n" + " is %s", + t1.toString().c_str(), getRepresentative(t1).toString().c_str(), + t2.toString().c_str(), getRepresentative(t2).toString().c_str()); // Get the explanation EqualityNodeId t1Id = getNodeId(t1); @@ -560,6 +567,28 @@ void EqualityEngine::getExplanation(TNode t1, TNode t2, std::vector getExplanation(t1Id, t2Id, equalities); } +template +void EqualityEngine::explainDisequality(TNode t1, TNode t2, std::vector& equalities) const { + Debug("equality") << "EqualityEngine::explainDisequality(" << t1 << "," << t2 << ")" << std::endl; + + Node equality = t1.eqNode(t2); + + Assert(getRepresentative(equality) == getRepresentative(d_false), + "Cannot explain the dis-equality, because the two terms are not dis-equal!\n" + "The representative of %s\n" + " is %s\n" + "The representative of %s\n" + " is %s", + equality.toString().c_str(), getRepresentative(equality).toString().c_str(), + d_false.toString().c_str(), getRepresentative(d_false).toString().c_str()); + + // Get the explanation + EqualityNodeId equalityId = getNodeId(equality); + EqualityNodeId falseId = getNodeId(d_false); + getExplanation(equalityId, falseId, equalities); +} + + template void EqualityEngine::getExplanation(EqualityNodeId t1Id, EqualityNodeId t2Id, std::vector& equalities) const { @@ -672,12 +701,12 @@ void EqualityEngine::addTriggerEquality(TNode t1, TNode t2, TNode t // Get the information about t1 EqualityNodeId t1Id = getNodeId(t1); EqualityNodeId t1classId = getEqualityNode(t1Id).getFind(); - TriggerId t1TriggerId = d_nodeTriggers[t1Id]; + TriggerId t1TriggerId = d_nodeTriggers[t1classId]; // Get the information about t2 EqualityNodeId t2Id = getNodeId(t2); EqualityNodeId t2classId = getEqualityNode(t2Id).getFind(); - TriggerId t2TriggerId = d_nodeTriggers[t2Id]; + TriggerId t2TriggerId = d_nodeTriggers[t2classId]; Debug("equality") << "EqualityEngine::addTrigger(" << trigger << "): " << t1Id << " (" << t1classId << ") = " << t2Id << " (" << t2classId << ")" << std::endl; @@ -836,6 +865,7 @@ bool EqualityEngine::areDisequal(TNode t1, TNode t2) Node equality1 = t1.eqNode(t2); addTerm(equality1); if (getEqualityNode(equality1).getFind() == getEqualityNode(d_false).getFind()) { + d_context->pop(); return true; } @@ -843,6 +873,7 @@ bool EqualityEngine::areDisequal(TNode t1, TNode t2) Node equality2 = t2.eqNode(t1); addTerm(equality2); if (getEqualityNode(equality2).getFind() == getEqualityNode(d_false).getFind()) { + d_context->pop(); return true; } diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp index 58fa44358..e2462f244 100644 --- a/src/theory/uf/theory_uf.cpp +++ b/src/theory/uf/theory_uf.cpp @@ -236,9 +236,16 @@ void TheoryUF::explain(TNode literal, std::vector& assumptions) { rhs = d_true; break; case kind::NOT: - lhs = literal[0]; - rhs = d_false; - break; + if (literal[0].getKind() == kind::EQUAL) { + // Disequalities + d_equalityEngine.explainDisequality(literal[0][0], literal[0][1], assumptions); + return; + } else { + // Predicates + lhs = literal[0]; + rhs = d_false; + break; + } case kind::CONST_BOOLEAN: // we get to explain true = false, since we set false to be the trigger of this lhs = d_true; @@ -247,8 +254,8 @@ void TheoryUF::explain(TNode literal, std::vector& assumptions) { default: Unreachable(); } - d_equalityEngine.getExplanation(lhs, rhs, assumptions); -}/* TheoryUF::explain() */ + d_equalityEngine.explainEquality(lhs, rhs, assumptions); +} Node TheoryUF::explain(TNode literal) { Debug("uf") << "TheoryUF::explain(" << literal << ")" << std::endl;