summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/theory/arith/infer_bounds.cpp56
-rw-r--r--src/theory/arith/infer_bounds.h10
-rw-r--r--src/theory/arith/theory_arith.cpp38
-rw-r--r--src/theory/arith/theory_arith.h5
-rw-r--r--src/theory/datatypes/theory_datatypes.cpp5
-rw-r--r--src/theory/datatypes/theory_datatypes.h5
-rw-r--r--src/theory/theory.cpp28
-rw-r--r--src/theory/theory.h41
-rw-r--r--src/theory/theory_engine.cpp17
-rw-r--r--src/theory/theory_engine.h6
-rw-r--r--src/theory/valuation.cpp9
-rw-r--r--src/theory/valuation.h8
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<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)
{
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<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 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<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 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<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 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 <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 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<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 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<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 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<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 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<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;
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback