Remove unecessary calls to equality engine from congruence manager (#8715)

Removes a deprecated explain interface.

diff --git a/src/theory/arith/linear/congruence_manager.cpp b/src/theory/arith/linear/congruence_manager.cpp
index 017fef67548743fb66c4f754e4c3c77b5012d774..eabc9e5483374329a3886787ee0983256210b9b5 100644 (file)
--- a/src/theory/arith/linear/congruence_manager.cpp
+++ b/src/theory/arith/linear/congruence_manager.cpp
@@ -394,14 +394,6 @@ bool ArithCongruenceManager::propagate(TNode x){
   return true;
 }
 
-void ArithCongruenceManager::explain(TNode literal, std::vector<TNode>& assumptions) {
-  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);
-  }
-}
-
 void ArithCongruenceManager::enqueueIntoNB(const std::set<TNode> s,
                                            NodeBuilder& nb)
 {
@@ -452,18 +444,6 @@ TrustNode ArithCongruenceManager::explain(TNode external)
   return trn;
 }
 
-void ArithCongruenceManager::explain(TNode external, NodeBuilder& out)
-{
-  Node internal = externalToInternal(external);
-
-  std::vector<TNode> assumptions;
-  explain(internal, assumptions);
-  std::set<TNode> assumptionSet;
-  assumptionSet.insert(assumptions.begin(), assumptions.end());
-
-  enqueueIntoNB(assumptionSet, out);
-}
-
 void ArithCongruenceManager::addWatchedPair(ArithVar s, TNode x, TNode y){
   Assert(!isWatchedVariable(s));
 

diff --git a/src/theory/arith/linear/congruence_manager.h b/src/theory/arith/linear/congruence_manager.h
index 180cbcef1c0e2f3b80656ff3bec2ca4d79ea7e8f..8e9ba410482275aaebe6095b119bfee6a8fb9f91 100644 (file)
--- a/src/theory/arith/linear/congruence_manager.h
+++ b/src/theory/arith/linear/congruence_manager.h
@@ -158,8 +158,6 @@ class ArithCongruenceManager : protected EnvObj
 
   void pushBack(TNode n, TNode r, TNode w);
 
-  void explain(TNode literal, std::vector<TNode>& assumptions);
-
   /** Assert this literal to the eq engine. Common functionality for
    *   * assertionToEqualityEngine(..)
    *   * equalsConstant(c)
@@ -227,8 +225,6 @@ class ArithCongruenceManager : protected EnvObj
    */
   TrustNode explain(TNode literal);
 
-  void explain(TNode lit, NodeBuilder& out);
-
   void addWatchedPair(ArithVar s, TNode x, TNode y);
 
   inline bool isWatchedVariable(ArithVar s) const {

diff --git a/src/theory/arith/linear/constraint.cpp b/src/theory/arith/linear/constraint.cpp
index d33a40c1d4aacd2fe382db9044bc70dabef77c5a..b18aa02cd2cae2477c9eaa67a8a147fcb872868e 100644 (file)
--- a/src/theory/arith/linear/constraint.cpp
+++ b/src/theory/arith/linear/constraint.cpp
@@ -2010,13 +2010,6 @@ TrustNode ConstraintDatabase::eeExplain(const Constraint* const c) const
   return d_congruenceManager.explain(c->getLiteral());
 }
 
-void ConstraintDatabase::eeExplain(ConstraintCP c, NodeBuilder& nb) const
-{
-  Assert(c->hasLiteral());
-  // NOTE: this is not a recommended method since it ignores proofs
-  d_congruenceManager.explain(c->getLiteral(), nb);
-}
-
 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 745462e4bc645c1b983d2a41cb67fc7f0e0d5580..5abe9ee9f5e9342e607f1b9d1e25e25edfe8d900 100644 (file)
--- a/src/theory/arith/linear/constraint.h
+++ b/src/theory/arith/linear/constraint.h
@@ -1153,8 +1153,6 @@ class ConstraintDatabase : protected EnvObj
   /** Get an explanation and proof for this constraint from the equality engine
    */
   TrustNode eeExplain(ConstraintCP c) const;
-  /** Get an explanation for this constraint from the equality engine */
-  void eeExplain(ConstraintCP c, NodeBuilder& nb) const;
 
   /**
    * Returns a constraint with the variable v, the constraint type t, and a value