Simplify entailment check interface (#4744)

The generality of this interface is unnecessary.

1 files changed, 5 insertions, 33 deletions

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;
 }