From: Andrew Reynolds Date: Wed, 4 May 2022 19:44:39 +0000 (-0500) Subject: Make equality solver the entry point for all equality engine explanations in arithmet... X-Git-Tag: cvc5-1.0.1~171 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=65e8b07964b4115bedee139cb88e5f866b3a8df6;p=cvc5.git Make equality solver the entry point for all equality engine explanations in arithmetic (#8719) This makes it so that EqSolver is the main entry point for all equality engine explanations in arithmetic; it still defers to the CongruenceManager to compute these explanations. To do this, when the core linear solver depends on an explanation from the equality engine, it instead provides a placeholder. Since explanations are computed recursively in TheoryEngine, this will trigger another call to TheoryArith::explain, which will then be handled by the EqSolver. Thus, there should be no net effect on the overall explanations in this commit. This is work towards eliminating the dependency of the linear solver on the equality engine. --- diff --git a/src/theory/arith/equality_solver.cpp b/src/theory/arith/equality_solver.cpp index aa3e31fac..2a6c8ee7b 100644 --- a/src/theory/arith/equality_solver.cpp +++ b/src/theory/arith/equality_solver.cpp @@ -72,6 +72,16 @@ bool EqualitySolver::preNotifyFact( TrustNode EqualitySolver::explain(TNode lit) { Trace("arith-eq-solver-debug") << "explain " << lit << "?" << std::endl; + if (d_acm != nullptr) + { + // if we are using the congruence manager, consult whether it can explain + if (d_acm->canExplain(lit)) + { + return d_acm->explain(lit); + } + // otherwise, don't explain + return TrustNode::null(); + } // check if we propagated it? if (d_propLits.find(lit) == d_propLits.end()) { diff --git a/src/theory/arith/linear/congruence_manager.cpp b/src/theory/arith/linear/congruence_manager.cpp index eabc9e548..8ab23f79c 100644 --- a/src/theory/arith/linear/congruence_manager.cpp +++ b/src/theory/arith/linear/congruence_manager.cpp @@ -394,16 +394,6 @@ bool ArithCongruenceManager::propagate(TNode x){ return true; } -void ArithCongruenceManager::enqueueIntoNB(const std::set s, - NodeBuilder& nb) -{ - std::set::const_iterator it = s.begin(); - std::set::const_iterator it_end = s.end(); - for(; it != it_end; ++it) { - nb << *it; - } -} - TrustNode ArithCongruenceManager::explainInternal(TNode internal) { if (isProofEnabled()) diff --git a/src/theory/arith/linear/congruence_manager.h b/src/theory/arith/linear/congruence_manager.h index 8e9ba4104..8282f2bcf 100644 --- a/src/theory/arith/linear/congruence_manager.h +++ b/src/theory/arith/linear/congruence_manager.h @@ -193,8 +193,6 @@ class ArithCongruenceManager : protected EnvObj void enableSharedTerms(); void dequeueLiterals(); - void enqueueIntoNB(const std::set all, NodeBuilder& nb); - /** * Determine an explaination for `internal`. That is a conjunction of theory * literals which imply `internal`. diff --git a/src/theory/arith/linear/constraint.cpp b/src/theory/arith/linear/constraint.cpp index b18aa02cd..628750973 100644 --- a/src/theory/arith/linear/constraint.cpp +++ b/src/theory/arith/linear/constraint.cpp @@ -1721,39 +1721,16 @@ std::shared_ptr Constraint::externalExplain( } else if (hasEqualityEngineProof()) { - Trace("pf::arith::explain") << " going to ee:" << std::endl; - TrustNode exp = d_database->eeExplain(this); + // just assume, it will be explained again + Node lit = getLiteral(); if (d_database->isProofEnabled()) { - Assert(exp.getProven().getKind() == Kind::IMPLIES); - std::vector> hypotheses; - hypotheses.push_back(exp.getGenerator()->getProofFor(exp.getProven())); - if (exp.getNode().getKind() == Kind::AND) - { - for (const auto& h : exp.getNode()) - { - hypotheses.push_back( - pnm->mkNode(PfRule::TRUE_INTRO, {pnm->mkAssume(h)}, {})); - } - } - else - { - hypotheses.push_back(pnm->mkNode( - PfRule::TRUE_INTRO, {pnm->mkAssume(exp.getNode())}, {})); - } + std::shared_ptr a = pnm->mkAssume(getLiteral()); pf = pnm->mkNode( - PfRule::MACRO_SR_PRED_TRANSFORM, {hypotheses}, {getProofLiteral()}); - } - Trace("pf::arith::explain") - << " explanation: " << exp.getNode() << std::endl; - if (exp.getNode().getKind() == Kind::AND) - { - nb.append(exp.getNode().begin(), exp.getNode().end()); - } - else - { - nb << exp.getNode(); + PfRule::MACRO_SR_PRED_TRANSFORM, {a}, {getProofLiteral()}); } + Assert(lit.getKind() != kind::AND); + nb << lit; } else { @@ -2004,11 +1981,6 @@ ConstraintP ConstraintDatabase::getBestImpliedBound(ArithVar v, ConstraintType t } } } -TrustNode ConstraintDatabase::eeExplain(const Constraint* const c) const -{ - Assert(c->hasLiteral()); - return d_congruenceManager.explain(c->getLiteral()); -} bool ConstraintDatabase::variableDatabaseIsSetup(ArithVar v) const { return v < d_varDatabases.size(); diff --git a/src/theory/arith/linear/constraint.h b/src/theory/arith/linear/constraint.h index 5abe9ee9f..4757688f8 100644 --- a/src/theory/arith/linear/constraint.h +++ b/src/theory/arith/linear/constraint.h @@ -1150,10 +1150,6 @@ class ConstraintDatabase : protected EnvObj bool variableDatabaseIsSetup(ArithVar v) const; void removeVariable(ArithVar v); - /** Get an explanation and proof for this constraint from the equality engine - */ - TrustNode eeExplain(ConstraintCP c) const; - /** * Returns a constraint with the variable v, the constraint type t, and a value * dominated by r (explained below) if such a constraint exists in the database. diff --git a/src/theory/arith/linear/theory_arith_private.cpp b/src/theory/arith/linear/theory_arith_private.cpp index 793eb816a..67cc9d702 100644 --- a/src/theory/arith/linear/theory_arith_private.cpp +++ b/src/theory/arith/linear/theory_arith_private.cpp @@ -3586,24 +3586,23 @@ TrustNode TheoryArithPrivate::explain(TNode n) ConstraintP c = d_constraintDatabase.lookup(n); TrustNode exp; - if(c != NullConstraint){ + // explanations that involve the congruence manager are handled in the + // main theory class. + Assert(!d_congruenceManager.canExplain(n)); + if (c != NullConstraint) + { Assert(!c->isAssumption()); exp = c->externalExplainForPropagation(n); Trace("arith::explain") << "constraint explanation" << n << ":" << exp << endl; - }else if(d_assertionsThatDoNotMatchTheirLiterals.find(n) != d_assertionsThatDoNotMatchTheirLiterals.end()){ + } + else if (d_assertionsThatDoNotMatchTheirLiterals.find(n) + != d_assertionsThatDoNotMatchTheirLiterals.end()) + { c = d_assertionsThatDoNotMatchTheirLiterals[n]; if(!c->isAssumption()){ exp = c->externalExplainForPropagation(n); Trace("arith::explain") << "assertions explanation" << n << ":" << exp << endl; - }else{ - Trace("arith::explain") << "this is a strange mismatch" << n << endl; - Assert(d_congruenceManager.canExplain(n)); - exp = d_congruenceManager.explain(n); } - }else{ - Assert(d_congruenceManager.canExplain(n)); - Trace("arith::explain") << "dm explanation" << n << endl; - exp = d_congruenceManager.explain(n); } return exp; } diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp index 1fca6459b..b9b575998 100644 --- a/src/theory/arith/theory_arith.cpp +++ b/src/theory/arith/theory_arith.cpp @@ -251,14 +251,11 @@ bool TheoryArith::needsCheckLastEffort() { TrustNode TheoryArith::explain(TNode n) { - if (options().arith.arithEqSolver) + // if the equality solver has an explanation for it, use it + TrustNode texp = d_eqSolver->explain(n); + if (!texp.isNull()) { - // if the equality solver has an explanation for it, use it - TrustNode texp = d_eqSolver->explain(n); - if (!texp.isNull()) - { - return texp; - } + return texp; } return d_internal->explain(n); }