Make equality solver the entry point for all equality engine explanations in arithmet...

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 aa3e31fac43d20f5c3c5fd01b36abbced723b40c..2a6c8ee7b928044935f16b777860838c3a1050d2 100644 (file)
--- 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 eabc9e5483374329a3886787ee0983256210b9b5..8ab23f79cb1d477ded5e3e51124d464b7dd5be8b 100644 (file)
--- 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<TNode> s,
-                                           NodeBuilder& nb)
-{
-  std::set<TNode>::const_iterator it = s.begin();
-  std::set<TNode>::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 8e9ba410482275aaebe6095b119bfee6a8fb9f91..8282f2bcfa8fa9202b4f598ca9957f5559a9563e 100644 (file)
--- 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<TNode> 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 b18aa02cd2cae2477c9eaa67a8a147fcb872868e..628750973856f528866234496dc550e15f489047 100644 (file)
--- a/src/theory/arith/linear/constraint.cpp
+++ b/src/theory/arith/linear/constraint.cpp
@@ -1721,39 +1721,16 @@ std::shared_ptr<ProofNode> 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<std::shared_ptr<ProofNode>> 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<ProofNode> 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 5abe9ee9f5e9342e607f1b9d1e25e25edfe8d900..4757688f827c6dcc35d1af92dff711ad79a131d7 100644 (file)
--- 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 793eb816a3a5f56788846cfac6d23fccdb986332..67cc9d702baa8ff1bfe5e33a2a89ef798a01ad7c 100644 (file)
--- 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 1fca6459ba70439985b782afe6dc96f7bc88a8c6..b9b57599838e1d5559f0f18cd04343d90265fa46 100644 (file)
--- 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);
 }