From eb58f1ef8917c5d57d64c54f9188b0ed489b47c1 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Wed, 15 Jul 2020 03:58:54 -0500 Subject: [PATCH] Simplify entailment check interface (#4744) The generality of this interface is unnecessary. --- src/theory/arith/infer_bounds.cpp | 56 +---------------------- src/theory/arith/infer_bounds.h | 10 ++-- src/theory/arith/theory_arith.cpp | 38 ++------------- src/theory/arith/theory_arith.h | 5 +- src/theory/datatypes/theory_datatypes.cpp | 5 +- src/theory/datatypes/theory_datatypes.h | 5 +- src/theory/theory.cpp | 28 +----------- src/theory/theory.h | 41 +---------------- src/theory/theory_engine.cpp | 17 +++---- src/theory/theory_engine.h | 6 +-- src/theory/valuation.cpp | 9 ++-- src/theory/valuation.h | 8 +--- 12 files changed, 31 insertions(+), 197 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& 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 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 TheoryArith::entailmentCheck (TNode lit, - const EntailmentCheckParameters* params, - EntailmentCheckSideEffects* out) +std::pair 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(params); - } - Assert(aparams != NULL); - - ArithEntailmentCheckSideEffects* ase = NULL; - if(out == NULL){ - ase = new ArithEntailmentCheckSideEffects(); - }else{ - AlwaysAssert(out->getTheoryId() == getId()); - ase = dynamic_cast(out); - } - Assert(ase != NULL); - - std::pair 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 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 entailmentCheck( - TNode lit, - const EntailmentCheckParameters* params, - EntailmentCheckSideEffects* out) override; + std::pair 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 e19beb7f3..d6cb3b37e 100644 --- a/src/theory/datatypes/theory_datatypes.cpp +++ b/src/theory/datatypes/theory_datatypes.cpp @@ -2295,7 +2295,8 @@ void TheoryDatatypes::getRelevantTerms( std::set& termSet ) { << " relevant terms..." << std::endl; } -std::pair TheoryDatatypes::entailmentCheck(TNode lit, const EntailmentCheckParameters* params, EntailmentCheckSideEffects* out) { +std::pair 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 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 b2d416ecf..ba8321e50 100644 --- 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 entailmentCheck( - TNode lit, - const EntailmentCheckParameters* params = NULL, - EntailmentCheckSideEffects* out = NULL) override; + std::pair entailmentCheck(TNode lit) override; private: /** add tester to equivalence class info */ diff --git a/src/theory/theory.cpp b/src/theory/theory.cpp index 6fb739aa4..b0db8ab30 100644 --- 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 Theory::entailmentCheck( - TNode lit, - const EntailmentCheckParameters* params, - EntailmentCheckSideEffects* out) { +std::pair 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 0cea604bf..1dead8183 100644 --- 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 s.t. if b is true, then a formula E such that * E |= lit in the theory. */ - virtual std::pair entailmentCheck( - TNode lit, const EntailmentCheckParameters* params = NULL, - EntailmentCheckSideEffects* out = NULL); + virtual std::pair 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 4bca07170..70e744acf 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -2020,11 +2020,8 @@ void TheoryEngine::checkTheoryAssertionsWithModel(bool hardFailure) { } } -std::pair TheoryEngine::entailmentCheck( - options::TheoryOfMode mode, - TNode lit, - const EntailmentCheckParameters* params, - EntailmentCheckSideEffects* seffects) +std::pair 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 TheoryEngine::entailmentCheck( if( pol==( lit.getKind()==kind::IMPLIES && i==0 ) ){ ch = atom[i].negate(); } - std::pair chres = entailmentCheck( mode, ch, params, seffects ); + std::pair chres = entailmentCheck(mode, ch); if( chres.first ){ if( !is_conjunction ){ return chres; @@ -2060,13 +2057,13 @@ std::pair TheoryEngine::entailmentCheck( if( r==1 ){ ch = ch.negate(); } - std::pair chres = entailmentCheck( mode, ch, params, seffects ); + std::pair 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 chres2 = entailmentCheck( mode, ch2, params, seffects ); + std::pair chres2 = entailmentCheck(mode, ch2); if( chres2.first ){ return std::pair(true, NodeManager::currentNM()->mkNode(kind::AND, chres.second, chres2.second)); }else{ @@ -2081,11 +2078,9 @@ std::pair 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 chres = th->entailmentCheck(lit, params, seffects); + std::pair chres = th->entailmentCheck(lit); return chres; } } diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index 59d6f9583..8c0ce6dbf 100644 --- 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 entailmentCheck( - options::TheoryOfMode mode, - TNode lit, - const theory::EntailmentCheckParameters* params = NULL, - theory::EntailmentCheckSideEffects* out = NULL); + std::pair 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 c4529992a..d8233bff7 100644 --- 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 Valuation::entailmentCheck( - options::TheoryOfMode mode, - TNode lit, - const theory::EntailmentCheckParameters* params, - theory::EntailmentCheckSideEffects* out) +std::pair 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 01ae61fcb..b1985971a 100644 --- 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 entailmentCheck( - options::TheoryOfMode mode, - TNode lit, - const theory::EntailmentCheckParameters* params = NULL, - theory::EntailmentCheckSideEffects* out = NULL); + std::pair entailmentCheck(options::TheoryOfMode mode, TNode lit); /** need check ? */ bool needCheck() const; -- 2.30.2