From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Wed, 4 May 2022 07:28:31 +0000 (-0500)
Subject: Remove unecessary calls to equality engine from congruence manager (#8715)
X-Git-Tag: cvc5-1.0.1~175
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=6e5505c92c9586f5e388fd5002e9c7d5f0b666e2;p=cvc5.git

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 017fef675..eabc9e548 100644
--- 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 180cbcef1..8e9ba4104 100644
--- 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 d33a40c1d..b18aa02cd 100644
--- 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 745462e4b..5abe9ee9f 100644
--- 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