From 6e5505c92c9586f5e388fd5002e9c7d5f0b666e2 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Wed, 4 May 2022 02:28:31 -0500 Subject: [PATCH] Remove unecessary calls to equality engine from congruence manager (#8715) Removes a deprecated explain interface. --- .../arith/linear/congruence_manager.cpp | 20 ------------------- src/theory/arith/linear/congruence_manager.h | 4 ---- src/theory/arith/linear/constraint.cpp | 7 ------- src/theory/arith/linear/constraint.h | 2 -- 4 files changed, 33 deletions(-) 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& 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 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 assumptions; - explain(internal, assumptions); - std::set 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& 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 -- 2.30.2