Simplify entailment check interface (#4744)

The generality of this interface is unnecessary.

4 files changed, 14 insertions, 95 deletions

diff --git a/src/theory/arith/infer_bounds.cpp b/src/theory/arith/infer_bounds.cpp
index 3714f3eb6..1f7383a96 100644
--- a/src/theory/arith/infer_bounds.cpp
+++ b/src/theory/arith/infer_bounds.cpp
@@ -61,8 +61,7 @@ InferBoundAlgorithm InferBoundAlgorithm::mkSimplex(const Maybe<int>& rounds){
 }
 
 ArithEntailmentCheckParameters::ArithEntailmentCheckParameters()
-  : EntailmentCheckParameters(theory::THEORY_ARITH)
-  , d_algorithms()
+    : d_algorithms()
 {}
 
 ArithEntailmentCheckParameters::~ArithEntailmentCheckParameters()
@@ -86,50 +85,6 @@ ArithEntailmentCheckParameters::const_iterator ArithEntailmentCheckParameters::e
   return d_algorithms.end();
 }
 
-
-// SimplexInferBoundsParameters::SimplexInferBoundsParameters()
-//   : d_parameter(1)
-//   , d_upperBound(true)
-//   , d_threshold()
-// {}
-
-// SimplexInferBoundsParameters::~SimplexInferBoundsParameters(){}
-
-
-
-// int SimplexInferBoundsParameters::getSimplexRoundParameter() const {
-//   return d_parameter;
-// }
-
-// bool SimplexInferBoundsParameters::findLowerBound() const {
-//   return ! findUpperBound();
-// }
-
-// bool SimplexInferBoundsParameters::findUpperBound() const {
-//   return d_upperBound;
-// }
-
-// void SimplexInferBoundsParameters::setThreshold(const DeltaRational& th){
-//   d_threshold = th;
-//   d_useThreshold = true;
-// }
-
-// bool SimplexInferBoundsParameters::useThreshold() const{
-//   return d_useThreshold;
-// }
-
-// const DeltaRational& SimplexInferBoundsParameters::getThreshold() const{
-//   return d_threshold;
-// }
-
-// SimplexInferBoundsParameters::SimplexInferBoundsParameters(int p, bool ub)
-//   : d_parameter(p)
-//   , d_upperBound(ub)
-//   , d_useThreshold(false)
-//   , d_threshold()
-// {}
-
-
 InferBoundsResult::InferBoundsResult()
   : d_foundBound(false)
   , d_budgetExhausted(false)
@@ -219,11 +174,6 @@ void InferBoundsResult::setBound(const DeltaRational& dr, Node exp){
   d_explanation = exp;
 }
 
-//bool InferBoundsResult::foundBound() const { return d_foundBound; }
-//bool InferBoundsResult::boundIsOptimal() const { return d_boundIsProvenOpt; }
-//bool InferBoundsResult::inconsistentState() const { return d_inconsistentState; }
-
-
 void InferBoundsResult::setBudgetExhausted() { d_budgetExhausted = true; }
 void InferBoundsResult::setReachedThreshold() { d_reachedThreshold = true; }
 void InferBoundsResult::setIsOptimal() { d_boundIsProvenOpt = true; }
@@ -277,10 +227,8 @@ std::ostream& operator<<(std::ostream& os, const InferBoundsResult& ibr){
   return os;
 }
 
-
 ArithEntailmentCheckSideEffects::ArithEntailmentCheckSideEffects()
-  : EntailmentCheckSideEffects(theory::THEORY_ARITH)
-  , d_simplexSideEffects (NULL)
+    : d_simplexSideEffects(NULL)
 {}
 
 ArithEntailmentCheckSideEffects::~ArithEntailmentCheckSideEffects(){
diff --git a/src/theory/arith/infer_bounds.h b/src/theory/arith/infer_bounds.h
index e9ea01071..22e9f5154 100644
--- a/src/theory/arith/infer_bounds.h
+++ b/src/theory/arith/infer_bounds.h
@@ -58,8 +58,9 @@ public:
 std::ostream& operator<<(std::ostream& os, const Algorithms a);
 } /* namespace inferbounds */
 
-class ArithEntailmentCheckParameters : public EntailmentCheckParameters {
-private:
+class ArithEntailmentCheckParameters
+{
+ private:
   typedef std::vector<inferbounds::InferBoundAlgorithm> VecInferBoundAlg;
   VecInferBoundAlg d_algorithms;
 
@@ -146,8 +147,9 @@ private:
 
 std::ostream& operator<<(std::ostream& os, const InferBoundsResult& ibr);
 
-class ArithEntailmentCheckSideEffects : public EntailmentCheckSideEffects{
-public:
+class ArithEntailmentCheckSideEffects
+{
+ public:
   ArithEntailmentCheckSideEffects();
   ~ArithEntailmentCheckSideEffects();
 
diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp
index 83ae5a032..eb5bf3685 100644
--- a/src/theory/arith/theory_arith.cpp
+++ b/src/theory/arith/theory_arith.cpp
@@ -166,40 +166,12 @@ Node TheoryArith::getModelValue(TNode var) {
   return d_internal->getModelValue( var );
 }
 
-
-std::pair<bool, Node> TheoryArith::entailmentCheck (TNode lit,
-                                                    const EntailmentCheckParameters* params,
-                                                    EntailmentCheckSideEffects* out)
+std::pair<bool, Node> TheoryArith::entailmentCheck(TNode lit)
 {
-  const ArithEntailmentCheckParameters* aparams = NULL;
-  if(params == NULL){
-    ArithEntailmentCheckParameters* def = new ArithEntailmentCheckParameters();
-    def->addLookupRowSumAlgorithms();
-    aparams = def;
-  }else{
-    AlwaysAssert(params->getTheoryId() == getId());
-    aparams = dynamic_cast<const ArithEntailmentCheckParameters*>(params);
-  }
-  Assert(aparams != NULL);
-
-  ArithEntailmentCheckSideEffects* ase = NULL;
-  if(out == NULL){
-    ase = new ArithEntailmentCheckSideEffects();
-  }else{
-    AlwaysAssert(out->getTheoryId() == getId());
-    ase = dynamic_cast<ArithEntailmentCheckSideEffects*>(out);
-  }
-  Assert(ase != NULL);
-
-  std::pair<bool, Node> res = d_internal->entailmentCheck(lit, *aparams, *ase);
-
-  if(params == NULL){
-    delete aparams;
-  }
-  if(out == NULL){
-    delete ase;
-  }
-
+  ArithEntailmentCheckParameters def;
+  def.addLookupRowSumAlgorithms();
+  ArithEntailmentCheckSideEffects ase;
+  std::pair<bool, Node> res = d_internal->entailmentCheck(lit, def, ase);
   return res;
 }
 
diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h
index 9381b7341..30de7bbad 100644
--- a/src/theory/arith/theory_arith.h
+++ b/src/theory/arith/theory_arith.h
@@ -99,10 +99,7 @@ class TheoryArith : public Theory {
 
   Node getModelValue(TNode var) override;
 
-  std::pair<bool, Node> entailmentCheck(
-      TNode lit,
-      const EntailmentCheckParameters* params,
-      EntailmentCheckSideEffects* out) override;
+  std::pair<bool, Node> entailmentCheck(TNode lit) override;
 
   void setProofRecorder(proof::ArithProofRecorder* proofRecorder)
   {