diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-03-09 21:36:24 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-03-09 19:36:24 -0700 |
commit | 3ebc297e6ff589f7b98519cd2aa23963a4e06652 (patch) | |
tree | afbc6f530317a259c929238e5627c5be214b0a61 /src/theory/quantifiers_engine.cpp | |
parent | 7d3df3b642aa1b346c11066be69a46f2edd1a9d9 (diff) |
Remove instantiation propagator infrastructure (#3975)
Diffstat (limited to 'src/theory/quantifiers_engine.cpp')
-rw-r--r-- | src/theory/quantifiers_engine.cpp | 25 |
1 files changed, 2 insertions, 23 deletions
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index 1db0937ff..b3ee7ad49 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -24,7 +24,6 @@ #include "theory/quantifiers/fmf/bounded_integers.h" #include "theory/quantifiers/fmf/full_model_check.h" #include "theory/quantifiers/fmf/model_engine.h" -#include "theory/quantifiers/inst_propagator.h" #include "theory/quantifiers/inst_strategy_enumerative.h" #include "theory/quantifiers/local_theory_ext.h" #include "theory/quantifiers/quant_conflict_find.h" @@ -45,8 +44,7 @@ class QuantifiersEnginePrivate { public: QuantifiersEnginePrivate() - : d_inst_prop(nullptr), - d_rel_dom(nullptr), + : d_rel_dom(nullptr), d_alpha_equiv(nullptr), d_inst_engine(nullptr), d_model_engine(nullptr), @@ -63,8 +61,6 @@ class QuantifiersEnginePrivate } ~QuantifiersEnginePrivate() {} //------------------------------ private quantifier utilities - /** quantifiers instantiation propagator */ - std::unique_ptr<quantifiers::InstPropagator> d_inst_prop; /** relevant domain */ std::unique_ptr<quantifiers::RelevantDomain> d_rel_dom; //------------------------------ end private quantifier utilities @@ -218,15 +214,7 @@ QuantifiersEngine::QuantifiersEngine(context::Context* c, if (options::ceGuidedInst()) { d_sygus_tdb.reset(new quantifiers::TermDbSygus(c, this)); - } - - if( options::instPropagate() ){ - // notice that this option is incompatible with options::qcfAllConflict() - d_private->d_inst_prop.reset(new quantifiers::InstPropagator(this)); - d_util.push_back(d_private->d_inst_prop.get()); - d_instantiate->addNotify(d_private->d_inst_prop->getInstantiationNotify()); - } - + } d_util.push_back(d_instantiate.get()); @@ -1125,15 +1113,6 @@ options::UserPatMode QuantifiersEngine::getInstUserPatMode() void QuantifiersEngine::flushLemmas(){ if( !d_lemmas_waiting.empty() ){ - //filter based on notify classes - if (d_instantiate->hasNotify()) - { - unsigned prev_lem_sz = d_lemmas_waiting.size(); - d_instantiate->notifyFlushLemmas(); - if( prev_lem_sz!=d_lemmas_waiting.size() ){ - Trace("quant-engine") << "...filtered instances : " << d_lemmas_waiting.size() << " / " << prev_lem_sz << std::endl; - } - } //take default output channel if none is provided d_hasAddedLemma = true; for( unsigned i=0; i<d_lemmas_waiting.size(); i++ ){ |