Simplify entailment check interface (#4744)

The generality of this interface is unnecessary.

diff --git a/src/theory/arith/infer_bounds.cpp b/src/theory/arith/infer_bounds.cpp
index 3714f3eb6392c1c3a6a671d09dc74c85f7256607..1f7383a96e70dde8e4743c96a828f078ed3a2c83 100644 (file)
--- 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 e9ea010712ac7026096e0519e8560d237b15f153..22e9f51547d764317dde69c0f976798890aeb23f 100644 (file)
--- 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 83ae5a032f17d085912c091596357409bc89dd70..eb5bf3685150766abc8e18f11b20a980602a0801 100644 (file)
--- 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 9381b7341d24607ad39203d06076a04a181e4b36..30de7bbadb8648fb75813e56a97432ed94e8ba9a 100644 (file)
--- 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)
   {

diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp
index e19beb7f3dac82513f4e8e23e13e51c25a1affd0..d6cb3b37e94c55e7556e00ce9a1b1990a612eb51 100644 (file)
--- a/src/theory/datatypes/theory_datatypes.cpp
+++ b/src/theory/datatypes/theory_datatypes.cpp
@@ -2295,7 +2295,8 @@ void TheoryDatatypes::getRelevantTerms( std::set<Node>& termSet ) {
                   << " relevant terms..." << std::endl;
 }
 
-std::pair<bool, Node> TheoryDatatypes::entailmentCheck(TNode lit, const EntailmentCheckParameters* params, EntailmentCheckSideEffects* out) {
+std::pair<bool, Node> TheoryDatatypes::entailmentCheck(TNode lit)
+{
   Trace("dt-entail") << "Check entailed : " << lit << std::endl;
   Node atom = lit.getKind()==NOT ? lit[0] : lit;
   bool pol = lit.getKind()!=NOT;
@@ -2323,8 +2324,6 @@ std::pair<bool, Node> TheoryDatatypes::entailmentCheck(TNode lit, const Entailme
         return make_pair(true, exp);
       }
     }
-  }else{
-
   }
   return make_pair(false, Node::null());
 }

diff --git a/src/theory/datatypes/theory_datatypes.h b/src/theory/datatypes/theory_datatypes.h
index b2d416ecf575d1c2d947bdaf6005b2de2c9e0f99..ba8321e5028019fd4b54dcfd1089f42acc6edd97 100644 (file)
--- a/src/theory/datatypes/theory_datatypes.h
+++ b/src/theory/datatypes/theory_datatypes.h
@@ -326,10 +326,7 @@ private:
   /** debug print */
   void printModelDebug( const char* c );
   /** entailment check */
-  std::pair<bool, Node> entailmentCheck(
-      TNode lit,
-      const EntailmentCheckParameters* params = NULL,
-      EntailmentCheckSideEffects* out = NULL) override;
+  std::pair<bool, Node> entailmentCheck(TNode lit) override;
 
  private:
   /** add tester to equivalence class info */

diff --git a/src/theory/theory.cpp b/src/theory/theory.cpp
index 6fb739aa4a7a14e75a17a85989341db5bd63fe86..b0db8ab302392a7e6343e31b87408447284b6d14 100644 (file)
--- a/src/theory/theory.cpp
+++ b/src/theory/theory.cpp
@@ -390,10 +390,8 @@ Theory::PPAssertStatus Theory::ppAssert(TNode in,
   return PP_ASSERT_STATUS_UNSOLVED;
 }
 
-std::pair<bool, Node> Theory::entailmentCheck(
-    TNode lit,
-    const EntailmentCheckParameters* params,
-    EntailmentCheckSideEffects* out) {
+std::pair<bool, Node> Theory::entailmentCheck(TNode lit)
+{
   return make_pair(false, Node::null());
 }
 
@@ -436,27 +434,5 @@ void Theory::setupExtTheory() {
   d_extTheory = new ExtTheory(this);
 }
 
-
-EntailmentCheckParameters::EntailmentCheckParameters(TheoryId tid)
-  : d_tid(tid) {
-}
-
-EntailmentCheckParameters::~EntailmentCheckParameters(){}
-
-TheoryId EntailmentCheckParameters::getTheoryId() const {
-  return d_tid;
-}
-
-EntailmentCheckSideEffects::EntailmentCheckSideEffects(TheoryId tid)
-  : d_tid(tid)
-{}
-
-TheoryId EntailmentCheckSideEffects::getTheoryId() const {
-  return d_tid;
-}
-
-EntailmentCheckSideEffects::~EntailmentCheckSideEffects() {
-}
-
 }/* CVC4::theory namespace */
 }/* CVC4 namespace */

diff --git a/src/theory/theory.h b/src/theory/theory.h
index 0cea604bfe2682722646eff6d51493d94547ccea..1dead81834e487dcc34bf99e498235beb8c65df2 100644 (file)
--- a/src/theory/theory.h
+++ b/src/theory/theory.h
@@ -60,9 +60,6 @@ class SubstitutionMap;
 class ExtTheory;
 class TheoryRewriter;
 
-class EntailmentCheckParameters;
-class EntailmentCheckSideEffects;
-
 namespace rrinst {
   class CandidateGenerator;
 }/* CVC4::theory::rrinst namespace */
@@ -837,29 +834,13 @@ class Theory {
    *
    * The theory may always return false!
    *
-   * The search is controlled by the parameter params.  For default behavior,
-   * this may be left NULL.
-   *
-   * Theories that want parameters extend the virtual EntailmentCheckParameters
-   * class.  Users ask the theory for an appropriate subclass from the theory
-   * and configure that.  How this is implemented is on a per theory basis.
-   *
-   * The search may provide additional output to guide the user of
-   * this function.  This output is stored in a EntailmentCheckSideEffects*
-   * output parameter.  The implementation of this is theory specific.  For
-   * no output, this is NULL.
-   *
    * Theories may not touch their output stream during an entailment check.
    *
    * @param  lit     a literal belonging to the theory.
-   * @param  params  the control parameters for the entailment check.
-   * @param  out     a theory specific output object of the entailment search.
    * @return         a pair <b,E> s.t. if b is true, then a formula E such that
    * E |= lit in the theory.
    */
-  virtual std::pair<bool, Node> entailmentCheck(
-      TNode lit, const EntailmentCheckParameters* params = NULL,
-      EntailmentCheckSideEffects* out = NULL);
+  virtual std::pair<bool, Node> entailmentCheck(TNode lit);
 
   /* equality engine TODO: use? */
   virtual eq::EqualityEngine* getEqualityEngine() { return NULL; }
@@ -934,26 +915,6 @@ inline std::ostream& operator << (std::ostream& out, theory::Theory::PPAssertSta
   return out;
 }
 
-class EntailmentCheckParameters {
-private:
-  TheoryId d_tid;
-protected:
-  EntailmentCheckParameters(TheoryId tid);
-public:
-  TheoryId getTheoryId() const;
-  virtual ~EntailmentCheckParameters();
-};/* class EntailmentCheckParameters */
-
-class EntailmentCheckSideEffects {
-private:
-  TheoryId d_tid;
-protected:
-  EntailmentCheckSideEffects(TheoryId tid);
-public:
-  TheoryId getTheoryId() const;
-  virtual ~EntailmentCheckSideEffects();
-};/* class EntailmentCheckSideEffects */
-
 }/* CVC4::theory namespace */
 }/* CVC4 namespace */
 

diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index 4bca07170bc46b386d4853b0db7fd68cf5683494..70e744acfd6c0c4775b5316de8ee99ad21d3d287 100644 (file)
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -2020,11 +2020,8 @@ void TheoryEngine::checkTheoryAssertionsWithModel(bool hardFailure) {
   }
 }
 
-std::pair<bool, Node> TheoryEngine::entailmentCheck(
-    options::TheoryOfMode mode,
-    TNode lit,
-    const EntailmentCheckParameters* params,
-    EntailmentCheckSideEffects* seffects)
+std::pair<bool, Node> TheoryEngine::entailmentCheck(options::TheoryOfMode mode,
+                                                    TNode lit)
 {
   TNode atom = (lit.getKind() == kind::NOT) ? lit[0] : lit;
   if( atom.getKind()==kind::AND || atom.getKind()==kind::OR || atom.getKind()==kind::IMPLIES ){
@@ -2037,7 +2034,7 @@ std::pair<bool, Node> TheoryEngine::entailmentCheck(
       if( pol==( lit.getKind()==kind::IMPLIES && i==0 ) ){
         ch = atom[i].negate();
       }
-      std::pair<bool, Node> chres = entailmentCheck( mode, ch, params, seffects );
+      std::pair<bool, Node> chres = entailmentCheck(mode, ch);
       if( chres.first ){
         if( !is_conjunction ){
           return chres;
@@ -2060,13 +2057,13 @@ std::pair<bool, Node> TheoryEngine::entailmentCheck(
       if( r==1 ){
         ch = ch.negate();
       }
-      std::pair<bool, Node> chres = entailmentCheck( mode, ch, params, seffects );
+      std::pair<bool, Node> chres = entailmentCheck(mode, ch);
       if( chres.first ){
         Node ch2 = atom[ atom.getKind()==kind::ITE ? r+1 : 1 ];
         if( pol==( atom.getKind()==kind::ITE ? true : r==1 ) ){
           ch2 = ch2.negate();
         }
-        std::pair<bool, Node> chres2 = entailmentCheck( mode, ch2, params, seffects );
+        std::pair<bool, Node> chres2 = entailmentCheck(mode, ch2);
         if( chres2.first ){
           return std::pair<bool, Node>(true, NodeManager::currentNM()->mkNode(kind::AND, chres.second, chres2.second));
         }else{
@@ -2081,11 +2078,9 @@ std::pair<bool, Node> TheoryEngine::entailmentCheck(
     theory::Theory* th = theoryOf(tid);
 
     Assert(th != NULL);
-    Assert(params == NULL || tid == params->getTheoryId());
-    Assert(seffects == NULL || tid == seffects->getTheoryId());
     Trace("theory-engine-entc") << "Entailment check : " << lit << std::endl;
 
-    std::pair<bool, Node> chres = th->entailmentCheck(lit, params, seffects);
+    std::pair<bool, Node> chres = th->entailmentCheck(lit);
     return chres;
   }
 }

diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h
index 59d6f9583a49e7edf063405d36863a1ac32dea45..8c0ce6dbf98a21ac69dbadc32c40106e7c29259a 100644 (file)
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -753,11 +753,7 @@ public:
    * Forwards an entailment check according to the given theoryOfMode.
    * See theory.h for documentation on entailmentCheck().
    */
-  std::pair<bool, Node> entailmentCheck(
-      options::TheoryOfMode mode,
-      TNode lit,
-      const theory::EntailmentCheckParameters* params = NULL,
-      theory::EntailmentCheckSideEffects* out = NULL);
+  std::pair<bool, Node> entailmentCheck(options::TheoryOfMode mode, TNode lit);
 
  private:
   /** Default visitor for pre-registration */

diff --git a/src/theory/valuation.cpp b/src/theory/valuation.cpp
index c4529992ac73d7602d3b630bcea9086e551bd2ed..d8233bff7abc4930bba5cc8f0c935a7bc50b9c26 100644 (file)
--- a/src/theory/valuation.cpp
+++ b/src/theory/valuation.cpp
@@ -125,13 +125,10 @@ unsigned Valuation::getAssertionLevel() const{
   return d_engine->getPropEngine()->getAssertionLevel();
 }
 
-std::pair<bool, Node> Valuation::entailmentCheck(
-    options::TheoryOfMode mode,
-    TNode lit,
-    const theory::EntailmentCheckParameters* params,
-    theory::EntailmentCheckSideEffects* out)
+std::pair<bool, Node> Valuation::entailmentCheck(options::TheoryOfMode mode,
+                                                 TNode lit)
 {
-  return d_engine->entailmentCheck(mode, lit, params, out);
+  return d_engine->entailmentCheck(mode, lit);
 }
 
 bool Valuation::needCheck() const{

diff --git a/src/theory/valuation.h b/src/theory/valuation.h
index 01ae61fcb7e954437698eeec7f9bff50a4da34bd..b1985971accfcc39ef98e4ffbbce818838363251 100644 (file)
--- a/src/theory/valuation.h
+++ b/src/theory/valuation.h
@@ -30,8 +30,6 @@ class TheoryEngine;
 
 namespace theory {
 
-class EntailmentCheckParameters;
-class EntailmentCheckSideEffects;
 class TheoryModel;
 
 /**
@@ -141,11 +139,7 @@ public:
    * Request an entailment check according to the given theoryOfMode.
    * See theory.h for documentation on entailmentCheck().
    */
-  std::pair<bool, Node> entailmentCheck(
-      options::TheoryOfMode mode,
-      TNode lit,
-      const theory::EntailmentCheckParameters* params = NULL,
-      theory::EntailmentCheckSideEffects* out = NULL);
+  std::pair<bool, Node> entailmentCheck(options::TheoryOfMode mode, TNode lit);
 
   /** need check ? */
   bool needCheck() const;