summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/options/quantifiers_options.toml17
-rw-r--r--src/theory/quantifiers/equality_query.cpp2
-rw-r--r--src/theory/quantifiers/instantiate.cpp16
-rw-r--r--src/theory/quantifiers/instantiate.h1
-rw-r--r--src/theory/quantifiers/quant_util.cpp2
-rw-r--r--src/theory/quantifiers/term_database.cpp40
-rw-r--r--src/theory/quantifiers_engine.cpp36
-rw-r--r--src/theory/quantifiers_engine.h6
8 files changed, 26 insertions, 94 deletions
diff --git a/src/options/quantifiers_options.toml b/src/options/quantifiers_options.toml
index b62468cdd..4b130158c 100644
--- a/src/options/quantifiers_options.toml
+++ b/src/options/quantifiers_options.toml
@@ -493,15 +493,6 @@ header = "options/quantifiers_options.h"
help = "allow theory combination to happen once initially, before quantifier strategies are run"
[[option]]
- name = "quantModelEe"
- category = "regular"
- long = "quant-model-ee"
- type = "bool"
- default = "false"
- read_only = true
- help = "use equality engine of model for last call effort"
-
-[[option]]
name = "instMaxLevel"
category = "regular"
long = "inst-max-level=N"
@@ -824,14 +815,6 @@ header = "options/quantifiers_options.h"
help = "do not consider instances of quantified formulas that are currently entailed"
[[option]]
- name = "instNoModelTrue"
- category = "regular"
- long = "inst-no-model-true"
- type = "bool"
- default = "false"
- help = "do not consider instances of quantified formulas that are currently true in model, if it is available"
-
-[[option]]
name = "qcfEagerTest"
category = "regular"
long = "qcf-eager-test"
diff --git a/src/theory/quantifiers/equality_query.cpp b/src/theory/quantifiers/equality_query.cpp
index 94e60513c..feaa0f223 100644
--- a/src/theory/quantifiers/equality_query.cpp
+++ b/src/theory/quantifiers/equality_query.cpp
@@ -182,7 +182,7 @@ Node EqualityQueryQuantifiersEngine::getInternalRepresentative(Node a,
}
eq::EqualityEngine* EqualityQueryQuantifiersEngine::getEngine(){
- return d_qe->getActiveEqualityEngine();
+ return d_qe->getMasterEqualityEngine();
}
void EqualityQueryQuantifiersEngine::getEquivalenceClass( Node a, std::vector< Node >& eqc ){
diff --git a/src/theory/quantifiers/instantiate.cpp b/src/theory/quantifiers/instantiate.cpp
index c9048fc95..77b61e9dd 100644
--- a/src/theory/quantifiers/instantiate.cpp
+++ b/src/theory/quantifiers/instantiate.cpp
@@ -242,17 +242,6 @@ bool Instantiate::addInstantiation(
// construct the lemma
Trace("inst-assert") << "(assert " << body << ")" << std::endl;
- if (d_qe->usingModelEqualityEngine() && options::instNoModelTrue())
- {
- Node val_body = d_qe->getModel()->getValue(body);
- if (val_body.isConst() && val_body.getConst<bool>())
- {
- Trace("inst-add-debug") << " --> True in model." << std::endl;
- ++(d_statistics.d_inst_duplicate_model_true);
- return false;
- }
- }
-
Node lem = NodeManager::currentNM()->mkNode(kind::OR, q.negate(), body);
lem = Rewriter::rewrite(lem);
@@ -845,14 +834,12 @@ Instantiate::Statistics::Statistics()
: d_instantiations("Instantiate::Instantiations_Total", 0),
d_inst_duplicate("Instantiate::Duplicate_Inst", 0),
d_inst_duplicate_eq("Instantiate::Duplicate_Inst_Eq", 0),
- d_inst_duplicate_ent("Instantiate::Duplicate_Inst_Entailed", 0),
- d_inst_duplicate_model_true("Instantiate::Duplicate_Inst_Model_True", 0)
+ d_inst_duplicate_ent("Instantiate::Duplicate_Inst_Entailed", 0)
{
smtStatisticsRegistry()->registerStat(&d_instantiations);
smtStatisticsRegistry()->registerStat(&d_inst_duplicate);
smtStatisticsRegistry()->registerStat(&d_inst_duplicate_eq);
smtStatisticsRegistry()->registerStat(&d_inst_duplicate_ent);
- smtStatisticsRegistry()->registerStat(&d_inst_duplicate_model_true);
}
Instantiate::Statistics::~Statistics()
@@ -861,7 +848,6 @@ Instantiate::Statistics::~Statistics()
smtStatisticsRegistry()->unregisterStat(&d_inst_duplicate);
smtStatisticsRegistry()->unregisterStat(&d_inst_duplicate_eq);
smtStatisticsRegistry()->unregisterStat(&d_inst_duplicate_ent);
- smtStatisticsRegistry()->unregisterStat(&d_inst_duplicate_model_true);
}
} /* CVC4::theory::quantifiers namespace */
diff --git a/src/theory/quantifiers/instantiate.h b/src/theory/quantifiers/instantiate.h
index 16ff1f2c3..cb40bbbbc 100644
--- a/src/theory/quantifiers/instantiate.h
+++ b/src/theory/quantifiers/instantiate.h
@@ -305,7 +305,6 @@ class Instantiate : public QuantifiersUtil
IntStat d_inst_duplicate;
IntStat d_inst_duplicate_eq;
IntStat d_inst_duplicate_ent;
- IntStat d_inst_duplicate_model_true;
Statistics();
~Statistics();
}; /* class Instantiate::Statistics */
diff --git a/src/theory/quantifiers/quant_util.cpp b/src/theory/quantifiers/quant_util.cpp
index a8eda10bb..cb1207912 100644
--- a/src/theory/quantifiers/quant_util.cpp
+++ b/src/theory/quantifiers/quant_util.cpp
@@ -32,7 +32,7 @@ QuantifiersModule::QEffort QuantifiersModule::needsModel(Theory::Effort e)
eq::EqualityEngine* QuantifiersModule::getEqualityEngine() const
{
- return d_quantEngine->getActiveEqualityEngine();
+ return d_quantEngine->getMasterEqualityEngine();
}
bool QuantifiersModule::areEqual(TNode n1, TNode n2) const
diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp
index 7caa103a0..6e5dca4ef 100644
--- a/src/theory/quantifiers/term_database.cpp
+++ b/src/theory/quantifiers/term_database.cpp
@@ -249,7 +249,7 @@ void TermDb::addTerm(Node n,
void TermDb::computeArgReps( TNode n ) {
if (d_arg_reps.find(n) == d_arg_reps.end())
{
- eq::EqualityEngine * ee = d_quantEngine->getActiveEqualityEngine();
+ eq::EqualityEngine* ee = d_quantEngine->getMasterEqualityEngine();
for (const TNode& nc : n)
{
TNode r = ee->hasTerm(nc) ? ee->getRepresentative(nc) : nc;
@@ -272,7 +272,7 @@ void TermDb::computeUfEqcTerms( TNode f ) {
{
ops.insert(ops.end(), d_ho_op_slaves[f].begin(), d_ho_op_slaves[f].end());
}
- eq::EqualityEngine* ee = d_quantEngine->getActiveEqualityEngine();
+ eq::EqualityEngine* ee = d_quantEngine->getMasterEqualityEngine();
for (const Node& ff : ops)
{
for (const TNode& n : d_op_map[ff])
@@ -307,7 +307,7 @@ void TermDb::computeUfTerms( TNode f ) {
unsigned nonCongruentCount = 0;
unsigned alreadyCongruentCount = 0;
unsigned relevantCount = 0;
- eq::EqualityEngine* ee = d_quantEngine->getActiveEqualityEngine();
+ eq::EqualityEngine* ee = d_quantEngine->getMasterEqualityEngine();
NodeManager* nm = NodeManager::currentNM();
for (const Node& ff : ops)
{
@@ -503,8 +503,8 @@ bool TermDb::inRelevantDomain( TNode f, unsigned i, TNode r ) {
f = getOperatorRepresentative( f );
}
computeUfTerms( f );
- Assert(!d_quantEngine->getActiveEqualityEngine()->hasTerm(r)
- || d_quantEngine->getActiveEqualityEngine()->getRepresentative(r)
+ Assert(!d_quantEngine->getMasterEqualityEngine()->hasTerm(r)
+ || d_quantEngine->getMasterEqualityEngine()->getRepresentative(r)
== r);
std::map< Node, std::map< unsigned, std::vector< Node > > >::iterator it = d_func_map_rel_dom.find( f );
if( it != d_func_map_rel_dom.end() ){
@@ -905,22 +905,18 @@ void TermDb::setTermInactive( Node n ) {
bool TermDb::hasTermCurrent( Node n, bool useMode ) {
if( !useMode ){
return d_has_map.find( n )!=d_has_map.end();
- }else{
- //return d_quantEngine->getActiveEqualityEngine()->hasTerm( n ); //some assertions are not sent to EE
- if (options::termDbMode() == options::TermDbMode::ALL)
- {
- return true;
- }
- else if (options::termDbMode() == options::TermDbMode::RELEVANT)
- {
- return d_has_map.find( n )!=d_has_map.end();
- }
- else
- {
- Assert(false);
- return false;
- }
}
+ //some assertions are not sent to EE
+ if (options::termDbMode() == options::TermDbMode::ALL)
+ {
+ return true;
+ }
+ else if (options::termDbMode() == options::TermDbMode::RELEVANT)
+ {
+ return d_has_map.find( n )!=d_has_map.end();
+ }
+ Assert(false) << "TermDb::hasTermCurrent: Unknown termDbMode : " << options::termDbMode();
+ return false;
}
bool TermDb::isTermEligibleForInstantiation(TNode n, TNode f)
@@ -966,7 +962,7 @@ Node TermDb::getEligibleTermInEqc( TNode r ) {
std::map< Node, Node >::iterator it = d_term_elig_eqc.find( r );
if( it==d_term_elig_eqc.end() ){
Node h;
- eq::EqualityEngine* ee = d_quantEngine->getActiveEqualityEngine();
+ eq::EqualityEngine* ee = d_quantEngine->getMasterEqualityEngine();
eq::EqClassIterator eqc_i = eq::EqClassIterator( r, ee );
while (!eqc_i.isFinished())
{
@@ -1021,7 +1017,7 @@ bool TermDb::reset( Theory::Effort effort ){
d_func_map_rel_dom.clear();
d_consistent_ee = true;
- eq::EqualityEngine* ee = d_quantEngine->getActiveEqualityEngine();
+ eq::EqualityEngine* ee = d_quantEngine->getMasterEqualityEngine();
Assert(ee->consistent());
// if higher-order, add equalities for the purification terms now
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index bb5950c5e..eafcc1e85 100644
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -223,7 +223,6 @@ QuantifiersEngine::QuantifiersEngine(context::Context* c,
d_curr_effort_level = QuantifiersModule::QEFFORT_NONE;
d_conflict = false;
d_hasAddedLemma = false;
- d_useModelEe = false;
//don't add true lemma
d_lemmas_produced_c[d_term_util->d_true] = true;
@@ -513,22 +512,9 @@ void QuantifiersEngine::ppNotifyAssertions(
void QuantifiersEngine::check( Theory::Effort e ){
CodeTimer codeTimer(d_statistics.d_time);
- d_useModelEe = options::quantModelEe() && ( e>=Theory::EFFORT_LAST_CALL );
- // if we want to use the model's equality engine, build the model now
- if( d_useModelEe && !d_model->isBuilt() ){
- Trace("quant-engine-debug") << "Build the model." << std::endl;
- if (!d_te->getModelBuilder()->buildModel(d_model.get()))
- {
- //we are done if model building was unsuccessful
- flushLemmas();
- if( d_hasAddedLemma ){
- Trace("quant-engine-debug") << "...failed." << std::endl;
- return;
- }
- }
- }
-
- if( !getActiveEqualityEngine()->consistent() ){
+
+ if (!getMasterEqualityEngine()->consistent())
+ {
Trace("quant-engine-debug") << "Master equality engine not consistent, return." << std::endl;
return;
}
@@ -1275,20 +1261,8 @@ eq::EqualityEngine* QuantifiersEngine::getMasterEqualityEngine() const
return d_te->getMasterEqualityEngine();
}
-eq::EqualityEngine* QuantifiersEngine::getActiveEqualityEngine() const
-{
- if( d_useModelEe ){
- return d_model->getEqualityEngine();
- }
- return d_te->getMasterEqualityEngine();
-}
-
Node QuantifiersEngine::getInternalRepresentative( Node a, Node q, int index ){
- bool prevModelEe = d_useModelEe;
- d_useModelEe = false;
- Node ret = d_eq_query->getInternalRepresentative( a, q, index );
- d_useModelEe = prevModelEe;
- return ret;
+ return d_eq_query->getInternalRepresentative(a, q, index);
}
bool QuantifiersEngine::getSynthSolutions(
@@ -1298,7 +1272,7 @@ bool QuantifiersEngine::getSynthSolutions(
}
void QuantifiersEngine::debugPrintEqualityEngine( const char * c ) {
- eq::EqualityEngine* ee = getActiveEqualityEngine();
+ eq::EqualityEngine* ee = getMasterEqualityEngine();
eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( ee );
std::map< TypeNode, int > typ_num;
while( !eqcs_i.isFinished() ){
diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h
index a4d858b16..dd86c0db9 100644
--- a/src/theory/quantifiers_engine.h
+++ b/src/theory/quantifiers_engine.h
@@ -74,8 +74,6 @@ public:
//---------------------- utilities
/** get the master equality engine */
eq::EqualityEngine* getMasterEqualityEngine() const;
- /** get the active equality engine */
- eq::EqualityEngine* getActiveEqualityEngine() const;
/** get equality query */
EqualityQuery* getEqualityQuery() const;
/** get the model builder */
@@ -228,8 +226,6 @@ public:
void addTermToDatabase( Node n, bool withinQuant = false, bool withinInstClosure = false );
/** notification when master equality engine is updated */
void eqNotifyNewClass(TNode t);
- /** use model equality engine */
- bool usingModelEqualityEngine() const { return d_useModelEe; }
/** debug print equality engine */
void debugPrintEqualityEngine( const char * c );
/** get internal representative
@@ -364,8 +360,6 @@ public:
context::CDO<bool> d_conflict_c;
/** has added lemma this round */
bool d_hasAddedLemma;
- /** whether to use model equality engine */
- bool d_useModelEe;
//------------- end temporary information during check
private:
/** list of all quantifiers seen */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback