diff options
Diffstat (limited to 'src/theory')
34 files changed, 193 insertions, 253 deletions
diff --git a/src/theory/inference_manager_buffered.cpp b/src/theory/inference_manager_buffered.cpp index cdba5dfd6..bc038a149 100644 --- a/src/theory/inference_manager_buffered.cpp +++ b/src/theory/inference_manager_buffered.cpp @@ -44,12 +44,23 @@ bool InferenceManagerBuffered::hasPendingLemma() const return !d_pendingLem.empty(); } -void InferenceManagerBuffered::addPendingLemma(Node lem, +bool InferenceManagerBuffered::addPendingLemma(Node lem, LemmaProperty p, - ProofGenerator* pg) + ProofGenerator* pg, + bool checkCache) { + if (checkCache) + { + // check if it is unique up to rewriting + Node lemr = Rewriter::rewrite(lem); + if (hasCachedLemma(lemr, p)) + { + return false; + } + } // make the simple theory lemma d_pendingLem.emplace_back(new SimpleTheoryLemma(lem, p, pg)); + return true; } void InferenceManagerBuffered::addPendingLemma( diff --git a/src/theory/inference_manager_buffered.h b/src/theory/inference_manager_buffered.h index 6edc0298f..28014ce8e 100644 --- a/src/theory/inference_manager_buffered.h +++ b/src/theory/inference_manager_buffered.h @@ -52,10 +52,19 @@ class InferenceManagerBuffered : public TheoryInferenceManager * non-null, pg must be able to provide a proof for lem for the remainder * of the user context. Pending lemmas are sent to the output channel using * doPendingLemmas. + * + * @param lem The lemma to send + * @param p The property of the lemma + * @param pg The proof generator which can provide a proof for lem + * @param checkCache Whether we want to check that the lemma is already in + * the cache. + * @return true if the lemma was added to the list of pending lemmas and + * false if the lemma is already cached. */ - void addPendingLemma(Node lem, + bool addPendingLemma(Node lem, LemmaProperty p = LemmaProperty::NONE, - ProofGenerator* pg = nullptr); + ProofGenerator* pg = nullptr, + bool checkCache = true); /** * Add pending lemma, where lemma can be a (derived) class of the * theory inference base class. diff --git a/src/theory/quantifiers/cegqi/ceg_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_instantiator.cpp index 411ab36b9..b2fff012e 100644 --- a/src/theory/quantifiers/cegqi/ceg_instantiator.cpp +++ b/src/theory/quantifiers/cegqi/ceg_instantiator.cpp @@ -1082,8 +1082,9 @@ bool CegInstantiator::doAddInstantiation( std::vector< Node >& vars, std::vector } Trace("cegqi-inst-debug") << "Do the instantiation...." << std::endl; bool ret = d_parent->doAddInstantiation(subs); - for( unsigned i=0; i<lemmas.size(); i++ ){ - d_parent->addLemma(lemmas[i]); + for (const Node& l : lemmas) + { + d_parent->addPendingLemma(l); } return ret; } diff --git a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp index 037cb74d7..208933456 100644 --- a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp +++ b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp @@ -108,7 +108,7 @@ bool InstStrategyCegqi::registerCbqiLemma(Node q) //add counterexample lemma Node lem = NodeManager::currentNM()->mkNode( OR, ceLit.negate(), ceBody.negate() ); //require any decision on cel to be phase=true - d_quantEngine->addRequirePhase( ceLit, true ); + d_qim.addPendingPhaseRequirement(ceLit, true); Debug("cegqi-debug") << "Require phase " << ceLit << " = true." << std::endl; //add counterexample lemma lem = Rewriter::rewrite( lem ); @@ -259,7 +259,7 @@ void InstStrategyCegqi::check(Theory::Effort e, QEffort quant_e) clSet = double(clock())/double(CLOCKS_PER_SEC); Trace("cegqi-engine") << "---Cbqi Engine Round, effort = " << e << "---" << std::endl; } - unsigned lastWaiting = d_quantEngine->getNumLemmasWaiting(); + size_t lastWaiting = d_qim.numPendingLemmas(); for( int ee=0; ee<=1; ee++ ){ //for( unsigned i=0; i<d_quantEngine->getModel()->getNumAssertedQuantifiers(); i++ ){ // Node q = d_quantEngine->getModel()->getAssertedQuantifier( i ); @@ -273,15 +273,17 @@ void InstStrategyCegqi::check(Theory::Effort e, QEffort quant_e) break; } } - if (d_qstate.isInConflict() - || d_quantEngine->getNumLemmasWaiting() > lastWaiting) + if (d_qstate.isInConflict() || d_qim.numPendingLemmas() > lastWaiting) { break; } } if( Trace.isOn("cegqi-engine") ){ - if( d_quantEngine->getNumLemmasWaiting()>lastWaiting ){ - Trace("cegqi-engine") << "Added lemmas = " << (d_quantEngine->getNumLemmasWaiting()-lastWaiting) << std::endl; + if (d_qim.numPendingLemmas() > lastWaiting) + { + Trace("cegqi-engine") + << "Added lemmas = " << (d_qim.numPendingLemmas() - lastWaiting) + << std::endl; } double clSet2 = double(clock())/double(CLOCKS_PER_SEC); Trace("cegqi-engine") << "Finished cbqi engine, time = " << (clSet2-clSet) << std::endl; @@ -392,7 +394,7 @@ void InstStrategyCegqi::registerCounterexampleLemma(Node q, Node lem) { Trace("cegqi-debug") << "Auxiliary CE lemma " << i << " : " << auxLems[i] << std::endl; - d_quantEngine->addLemma(auxLems[i], false); + d_qim.addPendingLemma(auxLems[i]); } } @@ -491,11 +493,11 @@ bool InstStrategyCegqi::doAddInstantiation( std::vector< Node >& subs ) { } } -bool InstStrategyCegqi::addLemma( Node lem ) { - return d_quantEngine->addLemma( lem ); +bool InstStrategyCegqi::addPendingLemma(Node lem) const +{ + return d_qim.addPendingLemma(lem); } - CegInstantiator * InstStrategyCegqi::getInstantiator( Node q ) { std::map<Node, std::unique_ptr<CegInstantiator>>::iterator it = d_cinst.find(q); @@ -534,7 +536,7 @@ bool InstStrategyCegqi::processNestedQe(Node q, bool isPreregister) // add lemmas to process for (const Node& lem : lems) { - d_quantEngine->addLemma(lem); + d_qim.addPendingLemma(lem); } // don't need to process this, since it has been reduced return true; diff --git a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.h b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.h index a6a3c36cd..7d39efc6b 100644 --- a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.h +++ b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.h @@ -123,8 +123,8 @@ class InstStrategyCegqi : public QuantifiersModule //------------------- interface for CegqiOutputInstStrategy /** Instantiate the current quantified formula forall x. Q with x -> subs. */ bool doAddInstantiation(std::vector<Node>& subs); - /** Add lemma lem via the output channel of this class. */ - bool addLemma(Node lem); + /** Add pending lemma lem via the inference manager of this class. */ + bool addPendingLemma(Node lem) const; //------------------- end interface for CegqiOutputInstStrategy protected: diff --git a/src/theory/quantifiers/conjecture_generator.cpp b/src/theory/quantifiers/conjecture_generator.cpp index 83a102633..bfaf0b83c 100644 --- a/src/theory/quantifiers/conjecture_generator.cpp +++ b/src/theory/quantifiers/conjecture_generator.cpp @@ -347,10 +347,11 @@ bool ConjectureGenerator::hasEnumeratedUf( Node n ) { std::vector< Node > lem; getEnumeratePredUfTerm( n, options::conjectureGenGtEnum(), lem ); if( !lem.empty() ){ - for( unsigned j=0; j<lem.size(); j++ ){ - d_quantEngine->addLemma( lem[j], false ); - d_hasAddedLemma = true; + for (const Node& l : lem) + { + d_qim.addPendingLemma(l); } + d_hasAddedLemma = true; return false; } } @@ -929,8 +930,8 @@ unsigned ConjectureGenerator::flushWaitingConjectures( unsigned& addedLemmas, in d_eq_conjectures[rhs].push_back( lhs ); Node lem = NodeManager::currentNM()->mkNode( OR, rsg.negate(), rsg ); - d_quantEngine->addLemma( lem, false ); - d_quantEngine->addRequirePhase( rsg, false ); + d_qim.addPendingLemma(lem); + d_qim.addPendingPhaseRequirement(rsg, false); addedLemmas++; if( (int)addedLemmas>=options::conjectureGenPerRound() ){ break; diff --git a/src/theory/quantifiers/ematching/ho_trigger.cpp b/src/theory/quantifiers/ematching/ho_trigger.cpp index 7479d005a..7cc1074aa 100644 --- a/src/theory/quantifiers/ematching/ho_trigger.cpp +++ b/src/theory/quantifiers/ematching/ho_trigger.cpp @@ -30,10 +30,11 @@ namespace inst { HigherOrderTrigger::HigherOrderTrigger( QuantifiersEngine* qe, + quantifiers::QuantifiersInferenceManager& qim, Node q, std::vector<Node>& nodes, std::map<Node, std::vector<Node> >& ho_apps) - : Trigger(qe, q, nodes), d_ho_var_apps(ho_apps) + : Trigger(qe, qim, q, nodes), d_ho_var_apps(ho_apps) { NodeManager* nm = NodeManager::currentNM(); // process the higher-order variable applications @@ -497,7 +498,7 @@ uint64_t HigherOrderTrigger::addHoTypeMatchPredicateLemmas() { Node u = tdb->getHoTypeMatchPredicate(tn); Node au = nm->mkNode(kind::APPLY_UF, u, f); - if (d_quantEngine->addLemma(au)) + if (d_qim.addPendingLemma(au)) { // this forces f to be a first-class member of the quantifier-free // equality engine, which in turn forces the quantifier-free diff --git a/src/theory/quantifiers/ematching/ho_trigger.h b/src/theory/quantifiers/ematching/ho_trigger.h index d9636cd65..e424f69d1 100644 --- a/src/theory/quantifiers/ematching/ho_trigger.h +++ b/src/theory/quantifiers/ematching/ho_trigger.h @@ -93,6 +93,7 @@ class HigherOrderTrigger : public Trigger private: HigherOrderTrigger(QuantifiersEngine* qe, + quantifiers::QuantifiersInferenceManager& qim, Node q, std::vector<Node>& nodes, std::map<Node, std::vector<Node> >& ho_apps); diff --git a/src/theory/quantifiers/ematching/inst_strategy.h b/src/theory/quantifiers/ematching/inst_strategy.h index 916790d9c..3baa25fa0 100644 --- a/src/theory/quantifiers/ematching/inst_strategy.h +++ b/src/theory/quantifiers/ematching/inst_strategy.h @@ -29,6 +29,7 @@ class QuantifiersEngine; namespace quantifiers { class QuantifiersState; +class QuantifiersInferenceManager; /** A status response to process */ enum class InstStrategyStatus @@ -45,8 +46,10 @@ enum class InstStrategyStatus class InstStrategy { public: - InstStrategy(QuantifiersEngine* qe, QuantifiersState& qs) - : d_quantEngine(qe), d_qstate(qs) + InstStrategy(QuantifiersEngine* qe, + QuantifiersState& qs, + QuantifiersInferenceManager& qim) + : d_quantEngine(qe), d_qstate(qs), d_qim(qim) { } virtual ~InstStrategy() {} @@ -64,6 +67,8 @@ class InstStrategy QuantifiersEngine* d_quantEngine; /** The quantifiers state object */ QuantifiersState& d_qstate; + /** The quantifiers inference manager object */ + QuantifiersInferenceManager& d_qim; }; /* class InstStrategy */ } // namespace quantifiers diff --git a/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp b/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp index 7c302e68c..7c8ab5ec2 100644 --- a/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp +++ b/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp @@ -58,10 +58,12 @@ struct sortTriggers { } }; -InstStrategyAutoGenTriggers::InstStrategyAutoGenTriggers(QuantifiersEngine* qe, - QuantifiersState& qs, - QuantRelevance* qr) - : InstStrategy(qe, qs), d_quant_rel(qr) +InstStrategyAutoGenTriggers::InstStrategyAutoGenTriggers( + QuantifiersEngine* qe, + QuantifiersState& qs, + QuantifiersInferenceManager& qim, + QuantRelevance* qr) + : InstStrategy(qe, qs, qim), d_quant_rel(qr) { //how to select trigger terms d_tr_strategy = options::triggerSelMode(); @@ -280,6 +282,7 @@ void InstStrategyAutoGenTriggers::generateTriggers( Node f ){ if (d_is_single_trigger[patTerms[0]]) { tr = Trigger::mkTrigger(d_quantEngine, + d_qim, f, patTerms[0], false, @@ -316,6 +319,7 @@ void InstStrategyAutoGenTriggers::generateTriggers( Node f ){ } // will possibly want to get an old trigger tr = Trigger::mkTrigger(d_quantEngine, + d_qim, f, patTerms, false, @@ -357,6 +361,7 @@ void InstStrategyAutoGenTriggers::generateTriggers( Node f ){ { d_single_trigger_gen[patTerms[index]] = true; Trigger* tr2 = Trigger::mkTrigger(d_quantEngine, + d_qim, f, patTerms[index], false, @@ -627,7 +632,7 @@ void InstStrategyAutoGenTriggers::addTrigger( inst::Trigger * tr, Node q ) { << "Make partially specified user pattern: " << std::endl; Trace("auto-gen-trigger-partial") << " " << qq << std::endl; Node lem = nm->mkNode(OR, q.negate(), qq); - d_quantEngine->addLemma(lem); + d_qim.addPendingLemma(lem); return; } unsigned tindex; diff --git a/src/theory/quantifiers/ematching/inst_strategy_e_matching.h b/src/theory/quantifiers/ematching/inst_strategy_e_matching.h index ac3c60ffe..81b40f067 100644 --- a/src/theory/quantifiers/ematching/inst_strategy_e_matching.h +++ b/src/theory/quantifiers/ematching/inst_strategy_e_matching.h @@ -87,6 +87,7 @@ class InstStrategyAutoGenTriggers : public InstStrategy public: InstStrategyAutoGenTriggers(QuantifiersEngine* qe, QuantifiersState& qs, + QuantifiersInferenceManager& qim, QuantRelevance* qr); ~InstStrategyAutoGenTriggers() {} diff --git a/src/theory/quantifiers/ematching/inst_strategy_e_matching_user.cpp b/src/theory/quantifiers/ematching/inst_strategy_e_matching_user.cpp index c9165c648..9d730e055 100644 --- a/src/theory/quantifiers/ematching/inst_strategy_e_matching_user.cpp +++ b/src/theory/quantifiers/ematching/inst_strategy_e_matching_user.cpp @@ -24,9 +24,11 @@ namespace CVC4 { namespace theory { namespace quantifiers { -InstStrategyUserPatterns::InstStrategyUserPatterns(QuantifiersEngine* ie, - QuantifiersState& qs) - : InstStrategy(ie, qs) +InstStrategyUserPatterns::InstStrategyUserPatterns( + QuantifiersEngine* ie, + QuantifiersState& qs, + QuantifiersInferenceManager& qim) + : InstStrategy(ie, qs, qim) { } InstStrategyUserPatterns::~InstStrategyUserPatterns() {} @@ -104,7 +106,7 @@ InstStrategyStatus InstStrategyUserPatterns::process(Node q, for (size_t i = 0, usize = ugw.size(); i < usize; i++) { Trigger* t = Trigger::mkTrigger( - d_quantEngine, q, ugw[i], true, Trigger::TR_RETURN_NULL); + d_quantEngine, d_qim, q, ugw[i], true, Trigger::TR_RETURN_NULL); if (t) { d_user_gen[q].push_back(t); @@ -162,8 +164,8 @@ void InstStrategyUserPatterns::addUserPattern(Node q, Node pat) d_user_gen_wait[q].push_back(nodes); return; } - Trigger* t = - Trigger::mkTrigger(d_quantEngine, q, nodes, true, Trigger::TR_MAKE_NEW); + Trigger* t = Trigger::mkTrigger( + d_quantEngine, d_qim, q, nodes, true, Trigger::TR_MAKE_NEW); if (t) { d_user_gen[q].push_back(t); diff --git a/src/theory/quantifiers/ematching/inst_strategy_e_matching_user.h b/src/theory/quantifiers/ematching/inst_strategy_e_matching_user.h index 3d7ddd97b..92b427621 100644 --- a/src/theory/quantifiers/ematching/inst_strategy_e_matching_user.h +++ b/src/theory/quantifiers/ematching/inst_strategy_e_matching_user.h @@ -33,7 +33,9 @@ namespace quantifiers { class InstStrategyUserPatterns : public InstStrategy { public: - InstStrategyUserPatterns(QuantifiersEngine* qe, QuantifiersState& qs); + InstStrategyUserPatterns(QuantifiersEngine* qe, + QuantifiersState& qs, + QuantifiersInferenceManager& qim); ~InstStrategyUserPatterns(); /** add pattern */ void addUserPattern(Node q, Node pat); diff --git a/src/theory/quantifiers/ematching/instantiation_engine.cpp b/src/theory/quantifiers/ematching/instantiation_engine.cpp index 96b3bd0b0..4f3b207be 100644 --- a/src/theory/quantifiers/ematching/instantiation_engine.cpp +++ b/src/theory/quantifiers/ematching/instantiation_engine.cpp @@ -53,13 +53,13 @@ InstantiationEngine::InstantiationEngine(QuantifiersEngine* qe, // user-provided patterns if (options::userPatternsQuant() != options::UserPatMode::IGNORE) { - d_isup.reset(new InstStrategyUserPatterns(d_quantEngine, qs)); + d_isup.reset(new InstStrategyUserPatterns(d_quantEngine, qs, qim)); d_instStrategies.push_back(d_isup.get()); } // auto-generated patterns - d_i_ag.reset( - new InstStrategyAutoGenTriggers(d_quantEngine, qs, d_quant_rel.get())); + d_i_ag.reset(new InstStrategyAutoGenTriggers( + d_quantEngine, qs, qim, d_quant_rel.get())); d_instStrategies.push_back(d_i_ag.get()); } } @@ -73,7 +73,7 @@ void InstantiationEngine::presolve() { } void InstantiationEngine::doInstantiationRound( Theory::Effort effort ){ - unsigned lastWaiting = d_quantEngine->getNumLemmasWaiting(); + size_t lastWaiting = d_qim.numPendingLemmas(); //iterate over an internal effort level e int e = 0; int eLimit = effort==Theory::EFFORT_LAST_CALL ? 10 : 2; @@ -111,7 +111,8 @@ void InstantiationEngine::doInstantiationRound( Theory::Effort effort ){ } } //do not consider another level if already added lemma at this level - if( d_quantEngine->getNumLemmasWaiting()>lastWaiting ){ + if (d_qim.numPendingLemmas() > lastWaiting) + { finished = true; } e++; @@ -164,21 +165,19 @@ void InstantiationEngine::check(Theory::Effort e, QEffort quant_e) Trace("inst-engine-debug") << nquant << " " << quantActive << std::endl; if (quantActive) { - unsigned lastWaiting = d_quantEngine->getNumLemmasWaiting(); + size_t lastWaiting = d_qim.numPendingLemmas(); doInstantiationRound(e); if (d_qstate.isInConflict()) { - Assert(d_quantEngine->getNumLemmasWaiting() > lastWaiting); + Assert(d_qim.numPendingLemmas() > lastWaiting); Trace("inst-engine") << "Conflict, added lemmas = " - << (d_quantEngine->getNumLemmasWaiting() - - lastWaiting) + << (d_qim.numPendingLemmas() - lastWaiting) << std::endl; } - else if (d_quantEngine->hasAddedLemma()) + else if (d_qim.hasPendingLemma()) { Trace("inst-engine") << "Added lemmas = " - << (d_quantEngine->getNumLemmasWaiting() - - lastWaiting) + << (d_qim.numPendingLemmas() - lastWaiting) << std::endl; } } diff --git a/src/theory/quantifiers/ematching/trigger.cpp b/src/theory/quantifiers/ematching/trigger.cpp index b1caa739e..58d94a11d 100644 --- a/src/theory/quantifiers/ematching/trigger.cpp +++ b/src/theory/quantifiers/ematching/trigger.cpp @@ -24,6 +24,7 @@ #include "theory/quantifiers/ematching/pattern_term_selector.h" #include "theory/quantifiers/instantiate.h" #include "theory/quantifiers/quantifiers_attributes.h" +#include "theory/quantifiers/quantifiers_inference_manager.h" #include "theory/quantifiers_engine.h" using namespace CVC4::kind; @@ -33,8 +34,11 @@ namespace theory { namespace inst { /** trigger class constructor */ -Trigger::Trigger(QuantifiersEngine* qe, Node q, std::vector<Node>& nodes) - : d_quantEngine(qe), d_quant(q) +Trigger::Trigger(QuantifiersEngine* qe, + quantifiers::QuantifiersInferenceManager& qim, + Node q, + std::vector<Node>& nodes) + : d_quantEngine(qe), d_qim(qim), d_quant(q) { // We must ensure that the ground subterms of the trigger have been // preprocessed. @@ -119,7 +123,7 @@ uint64_t Trigger::addInstantiations() Node eq = k.eqNode(gt); Trace("trigger-gt-lemma") << "Trigger: ground term purify lemma: " << eq << std::endl; - d_quantEngine->addLemma(eq); + d_qim.addPendingLemma(eq); gtAddedLemmas++; } } @@ -228,6 +232,7 @@ bool Trigger::mkTriggerTerms(Node q, } Trigger* Trigger::mkTrigger(QuantifiersEngine* qe, + quantifiers::QuantifiersInferenceManager& qim, Node f, std::vector<Node>& nodes, bool keepAll, @@ -268,11 +273,11 @@ Trigger* Trigger::mkTrigger(QuantifiersEngine* qe, Trigger* t; if (!ho_apps.empty()) { - t = new HigherOrderTrigger(qe, f, trNodes, ho_apps); + t = new HigherOrderTrigger(qe, qim, f, trNodes, ho_apps); } else { - t = new Trigger(qe, f, trNodes); + t = new Trigger(qe, qim, f, trNodes); } qe->getTriggerDatabase()->addTrigger( trNodes, t ); @@ -280,6 +285,7 @@ Trigger* Trigger::mkTrigger(QuantifiersEngine* qe, } Trigger* Trigger::mkTrigger(QuantifiersEngine* qe, + quantifiers::QuantifiersInferenceManager& qim, Node f, Node n, bool keepAll, @@ -288,7 +294,7 @@ Trigger* Trigger::mkTrigger(QuantifiersEngine* qe, { std::vector< Node > nodes; nodes.push_back( n ); - return mkTrigger(qe, f, nodes, keepAll, trOption, useNVars); + return mkTrigger(qe, qim, f, nodes, keepAll, trOption, useNVars); } int Trigger::getActiveScore() { diff --git a/src/theory/quantifiers/ematching/trigger.h b/src/theory/quantifiers/ematching/trigger.h index e2d3f7788..e2ce61bd1 100644 --- a/src/theory/quantifiers/ematching/trigger.h +++ b/src/theory/quantifiers/ematching/trigger.h @@ -29,11 +29,14 @@ namespace theory { class QuantifiersEngine; +namespace quantifiers { +class QuantifiersInferenceManager; +} + namespace inst { class IMGenerator; class InstMatchGenerator; - /** A collection of nodes representing a trigger. * * This class encapsulates all implementations of E-matching in CVC4. @@ -159,6 +162,7 @@ class Trigger { TR_RETURN_NULL //return null if a duplicate is found }; static Trigger* mkTrigger(QuantifiersEngine* qe, + quantifiers::QuantifiersInferenceManager& qim, Node q, std::vector<Node>& nodes, bool keepAll = true, @@ -166,6 +170,7 @@ class Trigger { size_t useNVars = 0); /** single trigger version that calls the above function */ static Trigger* mkTrigger(QuantifiersEngine* qe, + quantifiers::QuantifiersInferenceManager& qim, Node q, Node n, bool keepAll = true, @@ -187,7 +192,10 @@ class Trigger { protected: /** trigger constructor, intentionally protected (use Trigger::mkTrigger). */ - Trigger(QuantifiersEngine* ie, Node q, std::vector<Node>& nodes); + Trigger(QuantifiersEngine* ie, + quantifiers::QuantifiersInferenceManager& qim, + Node q, + std::vector<Node>& nodes); /** add an instantiation (called by InstMatchGenerator) * * This calls Instantiate::addInstantiation(...) for instantiations @@ -233,6 +241,8 @@ class Trigger { std::vector<Node> d_groundTerms; /** The quantifiers engine associated with this trigger. */ QuantifiersEngine* d_quantEngine; + /** Reference to the quantifiers inference manager */ + quantifiers::QuantifiersInferenceManager& d_qim; /** The quantified formula this trigger is for. */ Node d_quant; /** match generator diff --git a/src/theory/quantifiers/fmf/bounded_integers.cpp b/src/theory/quantifiers/fmf/bounded_integers.cpp index a6862f513..0a0d155f9 100644 --- a/src/theory/quantifiers/fmf/bounded_integers.cpp +++ b/src/theory/quantifiers/fmf/bounded_integers.cpp @@ -294,7 +294,7 @@ void BoundedIntegers::check(Theory::Effort e, QEffort quant_e) { Trace("bound-int-lemma") << "*** bound int : proxy lemma : " << prangeLem << std::endl; - d_quantEngine->addLemma(prangeLem); + d_qim.addPendingLemma(prangeLem); addedLemma = true; } } diff --git a/src/theory/quantifiers/fmf/model_engine.cpp b/src/theory/quantifiers/fmf/model_engine.cpp index 618a72047..428c435df 100644 --- a/src/theory/quantifiers/fmf/model_engine.cpp +++ b/src/theory/quantifiers/fmf/model_engine.cpp @@ -70,7 +70,7 @@ void ModelEngine::check(Theory::Effort e, QEffort quant_e) { bool doCheck = false; if( options::mbqiInterleave() ){ - doCheck = quant_e == QEFFORT_STANDARD && d_quantEngine->hasAddedLemma(); + doCheck = quant_e == QEFFORT_STANDARD && d_qim.hasPendingLemma(); } if( !doCheck ){ doCheck = quant_e == QEFFORT_MODEL; diff --git a/src/theory/quantifiers/inst_strategy_enumerative.cpp b/src/theory/quantifiers/inst_strategy_enumerative.cpp index f22e67815..1b011481b 100644 --- a/src/theory/quantifiers/inst_strategy_enumerative.cpp +++ b/src/theory/quantifiers/inst_strategy_enumerative.cpp @@ -77,7 +77,7 @@ void InstStrategyEnum::check(Theory::Effort e, QEffort quant_e) if (options::fullSaturateInterleave()) { // we only add when interleaved with other strategies - doCheck = quant_e == QEFFORT_STANDARD && d_quantEngine->hasAddedLemma(); + doCheck = quant_e == QEFFORT_STANDARD && d_qim.hasPendingLemma(); } if (options::fullSaturateQuant() && !doCheck) { diff --git a/src/theory/quantifiers/instantiate.cpp b/src/theory/quantifiers/instantiate.cpp index 49f1fe116..4db53c4b7 100644 --- a/src/theory/quantifiers/instantiate.cpp +++ b/src/theory/quantifiers/instantiate.cpp @@ -38,9 +38,11 @@ namespace quantifiers { Instantiate::Instantiate(QuantifiersEngine* qe, QuantifiersState& qs, + QuantifiersInferenceManager& qim, ProofNodeManager* pnm) : d_qe(qe), d_qstate(qs), + d_qim(qim), d_pnm(pnm), d_term_db(nullptr), d_term_util(nullptr), @@ -321,13 +323,12 @@ bool Instantiate::addInstantiation( bool addedLem = false; if (hasProof) { - // use trust interface - TrustNode tlem = TrustNode::mkTrustLemma(lem, d_pfInst.get()); - addedLem = d_qe->addTrustedLemma(tlem, true, false); + // use proof generator + addedLem = d_qim.addPendingLemma(lem, LemmaProperty::NONE, d_pfInst.get()); } else { - addedLem = d_qe->addLemma(lem, true, false); + addedLem = d_qim.addPendingLemma(lem); } if (!addedLem) @@ -400,18 +401,6 @@ bool Instantiate::addInstantiation( return true; } -bool Instantiate::removeInstantiation(Node q, - Node lem, - std::vector<Node>& terms) -{ - // lem must occur in d_waiting_lemmas - if (d_qe->removeLemma(lem)) - { - return removeInstantiationInternal(q, terms); - } - return false; -} - bool Instantiate::recordInstantiation(Node q, std::vector<Node>& terms, bool modEq, diff --git a/src/theory/quantifiers/instantiate.h b/src/theory/quantifiers/instantiate.h index bbb1a0a44..154cda681 100644 --- a/src/theory/quantifiers/instantiate.h +++ b/src/theory/quantifiers/instantiate.h @@ -78,7 +78,7 @@ class InstantiationRewriter * * Its main interface is ::addInstantiation(...), which is called by many of * the quantifiers modules, which enqueues instantiation lemmas in quantifiers - * engine via calls to QuantifiersEngine::addLemma. + * engine via calls to QuantifiersInferenceManager::addPendingLemma. * * It also has utilities for constructing instantiations, and interfaces for * getting the results of the instantiations produced during check-sat calls. @@ -90,6 +90,7 @@ class Instantiate : public QuantifiersUtil public: Instantiate(QuantifiersEngine* qe, QuantifiersState& qs, + QuantifiersInferenceManager& qim, ProofNodeManager* pnm = nullptr); ~Instantiate(); @@ -117,7 +118,7 @@ class Instantiate : public QuantifiersUtil * * This function returns true if the instantiation lemma for quantified * formula q for the substitution specified by m is successfully enqueued - * via a call to QuantifiersEngine::addLemma. + * via a call to QuantifiersInferenceManager::addPendingLemma. * mkRep : whether to take the representatives of the terms in the range of * the substitution m, * modEq : whether to check for duplication modulo equality in instantiation @@ -326,6 +327,8 @@ class Instantiate : public QuantifiersUtil QuantifiersEngine* d_qe; /** Reference to the quantifiers state */ QuantifiersState& d_qstate; + /** Reference to the quantifiers inference manager */ + QuantifiersInferenceManager& d_qim; /** pointer to the proof node manager */ ProofNodeManager* d_pnm; /** cache of term database for quantifiers engine */ diff --git a/src/theory/quantifiers/quant_conflict_find.h b/src/theory/quantifiers/quant_conflict_find.h index 5ffe4426a..086d492f4 100644 --- a/src/theory/quantifiers/quant_conflict_find.h +++ b/src/theory/quantifiers/quant_conflict_find.h @@ -249,7 +249,7 @@ private: //for equivalence classes * * This method attempts to construct a conflicting or propagating instance. * If such an instance exists, then it makes a call to - * Instantiation::addInstantiation or QuantifiersEngine::addLemma. + * Instantiation::addInstantiation. */ void check(Theory::Effort level, QEffort quant_e) override; diff --git a/src/theory/quantifiers/quant_split.cpp b/src/theory/quantifiers/quant_split.cpp index a1dc5acf3..f782ae7ef 100644 --- a/src/theory/quantifiers/quant_split.cpp +++ b/src/theory/quantifiers/quant_split.cpp @@ -198,7 +198,7 @@ void QuantDSplit::check(Theory::Effort e, QEffort quant_e) for (const Node& lem : lemmas) { Trace("quant-dsplit") << "QuantDSplit lemma : " << lem << std::endl; - d_quantEngine->addLemma(lem, false); + d_qim.addPendingLemma(lem); } Trace("quant-dsplit") << "QuantDSplit::check finished" << std::endl; } diff --git a/src/theory/quantifiers/quant_util.h b/src/theory/quantifiers/quant_util.h index 9037e94fa..551143e40 100644 --- a/src/theory/quantifiers/quant_util.h +++ b/src/theory/quantifiers/quant_util.h @@ -185,10 +185,10 @@ public: QuantifiersUtil(){} virtual ~QuantifiersUtil(){} /* reset - * Called at the beginning of an instantiation round - * Returns false if the reset failed. When reset fails, the utility should have - * added a lemma via a call to qe->addLemma. TODO: improve this contract #1163 - */ + * Called at the beginning of an instantiation round + * Returns false if the reset failed. When reset fails, the utility should + * have added a lemma via a call to d_qim.addPendingLemma. + */ virtual bool reset( Theory::Effort e ) = 0; /* Called for new quantifiers */ virtual void registerQuantifier(Node q) = 0; diff --git a/src/theory/quantifiers/quantifiers_inference_manager.cpp b/src/theory/quantifiers/quantifiers_inference_manager.cpp index f456dd407..652c42839 100644 --- a/src/theory/quantifiers/quantifiers_inference_manager.cpp +++ b/src/theory/quantifiers/quantifiers_inference_manager.cpp @@ -26,6 +26,12 @@ QuantifiersInferenceManager::QuantifiersInferenceManager( QuantifiersInferenceManager::~QuantifiersInferenceManager() {} +void QuantifiersInferenceManager::doPending() +{ + doPendingLemmas(); + doPendingPhaseRequirements(); +} + } // namespace quantifiers } // namespace theory } // namespace CVC4 diff --git a/src/theory/quantifiers/quantifiers_inference_manager.h b/src/theory/quantifiers/quantifiers_inference_manager.h index f89606d75..afdcfbdeb 100644 --- a/src/theory/quantifiers/quantifiers_inference_manager.h +++ b/src/theory/quantifiers/quantifiers_inference_manager.h @@ -34,6 +34,10 @@ class QuantifiersInferenceManager : public InferenceManagerBuffered QuantifiersState& state, ProofNodeManager* pnm); ~QuantifiersInferenceManager(); + /** + * Do all pending lemmas, then do all pending phase requirements. + */ + void doPending(); }; } // namespace quantifiers diff --git a/src/theory/quantifiers/sygus/synth_conjecture.cpp b/src/theory/quantifiers/sygus/synth_conjecture.cpp index c1333b85f..7bae92184 100644 --- a/src/theory/quantifiers/sygus/synth_conjecture.cpp +++ b/src/theory/quantifiers/sygus/synth_conjecture.cpp @@ -42,9 +42,11 @@ namespace quantifiers { SynthConjecture::SynthConjecture(QuantifiersEngine* qe, QuantifiersState& qs, + QuantifiersInferenceManager& qim, SygusStatistics& s) : d_qe(qe), d_qstate(qs), + d_qim(qim), d_stats(s), d_tds(qe->getTermDatabaseSygus()), d_hasSolution(false), @@ -721,7 +723,7 @@ bool SynthConjecture::doRefine() { Trace("cegqi-lemma") << "Cegqi::Lemma : candidate refinement : " << lem << std::endl; - bool res = d_qe->addLemma(lem); + bool res = d_qim.addPendingLemma(lem); if (res) { ++(d_stats.d_cegqi_lemmas_refine); diff --git a/src/theory/quantifiers/sygus/synth_conjecture.h b/src/theory/quantifiers/sygus/synth_conjecture.h index 1d43e30ff..ca3f2983b 100644 --- a/src/theory/quantifiers/sygus/synth_conjecture.h +++ b/src/theory/quantifiers/sygus/synth_conjecture.h @@ -84,6 +84,7 @@ class SynthConjecture public: SynthConjecture(QuantifiersEngine* qe, QuantifiersState& qs, + QuantifiersInferenceManager& qim, SygusStatistics& s); ~SynthConjecture(); /** presolve */ @@ -203,6 +204,8 @@ class SynthConjecture QuantifiersEngine* d_qe; /** Reference to the quantifiers state */ QuantifiersState& d_qstate; + /** Reference to the quantifiers inference manager */ + QuantifiersInferenceManager& d_qim; /** reference to the statistics of parent */ SygusStatistics& d_stats; /** term database sygus of d_qe */ diff --git a/src/theory/quantifiers/sygus/synth_engine.cpp b/src/theory/quantifiers/sygus/synth_engine.cpp index 869d22737..c12f387bc 100644 --- a/src/theory/quantifiers/sygus/synth_engine.cpp +++ b/src/theory/quantifiers/sygus/synth_engine.cpp @@ -39,7 +39,7 @@ SynthEngine::SynthEngine(QuantifiersEngine* qe, d_sqp(qe) { d_conjs.push_back(std::unique_ptr<SynthConjecture>( - new SynthConjecture(d_quantEngine, qs, d_statistics))); + new SynthConjecture(d_quantEngine, qs, qim, d_statistics))); d_conj = d_conjs.back().get(); } @@ -160,7 +160,7 @@ void SynthEngine::assignConjecture(Node q) if (d_conjs.back()->isAssigned()) { d_conjs.push_back(std::unique_ptr<SynthConjecture>( - new SynthConjecture(d_quantEngine, d_qstate, d_statistics))); + new SynthConjecture(d_quantEngine, d_qstate, d_qim, d_statistics))); } d_conjs.back()->assign(q); } @@ -224,7 +224,7 @@ bool SynthEngine::checkConjecture(SynthConjecture* conj) bool addedLemma = false; for (const Node& lem : cclems) { - if (d_quantEngine->addLemma(lem)) + if (d_qim.addPendingLemma(lem)) { ++(d_statistics.d_cegqi_lemmas_ce); addedLemma = true; diff --git a/src/theory/quantifiers/sygus_inst.cpp b/src/theory/quantifiers/sygus_inst.cpp index 69836feba..f6827d1c4 100644 --- a/src/theory/quantifiers/sygus_inst.cpp +++ b/src/theory/quantifiers/sygus_inst.cpp @@ -309,7 +309,7 @@ bool SygusInst::sendEvalUnfoldLemmas(const std::vector<Node>& lemmas) for (const Node& lem : lemmas) { Trace("sygus-inst") << "Evaluation unfolding: " << lem << std::endl; - added_lemma |= d_quantEngine->addLemma(lem); + added_lemma |= d_qim.addPendingLemma(lem); } return added_lemma; } @@ -511,7 +511,7 @@ void SygusInst::registerCeLemma(Node q, std::vector<TypeNode>& types) d_var_eval.emplace(q, evals); Node lit = getCeLiteral(q); - d_quantEngine->addRequirePhase(lit, true); + d_qim.addPendingPhaseRequirement(lit, true); /* The decision strategy for quantified formula 'q' ensures that its * counterexample literal is decided on first. It is user-context dependent. @@ -545,7 +545,7 @@ void SygusInst::addCeLemma(Node q) if (d_ce_lemma_added.find(q) != d_ce_lemma_added.end()) return; Node lem = d_ce_lemmas[q]; - d_quantEngine->addLemma(lem, false); + d_qim.addPendingLemma(lem); d_ce_lemma_added.insert(q); Trace("sygus-inst") << "Add CE Lemma: " << lem << std::endl; } diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp index 1498c29b7..56f85e99e 100644 --- a/src/theory/quantifiers/term_database.cpp +++ b/src/theory/quantifiers/term_database.cpp @@ -405,7 +405,7 @@ void TermDb::computeUfTerms( TNode f ) { } Trace("term-db-lemma") << " add lemma : " << lem << std::endl; } - d_quantEngine->addLemma(lem); + d_qim.addPendingLemma(lem); d_qstate.notifyInConflict(); d_consistent_ee = false; return; @@ -1015,7 +1015,7 @@ bool TermDb::reset( Theory::Effort effort ){ // equality is sent out as a lemma here. Trace("term-db-lemma") << "Purify equality lemma: " << eq << std::endl; - d_quantEngine->addLemma(eq); + d_qim.addPendingLemma(eq); d_qstate.notifyInConflict(); d_consistent_ee = false; return false; diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index 0e28cab76..bdc12cdaa 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -49,12 +49,11 @@ QuantifiersEngine::QuantifiersEngine( d_eq_query(nullptr), d_sygus_tdb(nullptr), d_quant_attr(new quantifiers::QuantAttributes), - d_instantiate(new quantifiers::Instantiate(this, qstate, pnm)), + d_instantiate(new quantifiers::Instantiate(this, qstate, qim, pnm)), d_skolemize(new quantifiers::Skolemize(this, qstate, pnm)), d_term_enum(new quantifiers::TermEnumeration), d_quants_prereg(qstate.getUserContext()), d_quants_red(qstate.getUserContext()), - d_lemmas_produced_c(qstate.getUserContext()), d_ierCounter_c(qstate.getSatContext()), d_presolve(qstate.getUserContext(), true), d_presolve_in(qstate.getUserContext()), @@ -73,10 +72,6 @@ QuantifiersEngine::QuantifiersEngine( d_util.push_back(d_instantiate.get()); - d_hasAddedLemma = false; - //don't add true lemma - d_lemmas_produced_c[d_term_util->d_true] = true; - Trace("quant-engine-debug") << "Initialize quantifiers engine." << std::endl; Trace("quant-engine-debug") << "Initialize model, mbqi : " << options::mbqiMode() << std::endl; @@ -261,8 +256,7 @@ bool QuantifiersEngine::getBoundElements(RepSetIterator* rsi, void QuantifiersEngine::presolve() { Trace("quant-engine-proc") << "QuantifiersEngine : presolve " << std::endl; - d_lemmas_waiting.clear(); - d_phase_req_waiting.clear(); + d_qim.clearPending(); for( unsigned i=0; i<d_modules.size(); i++ ){ d_modules[i]->presolve(); } @@ -342,7 +336,7 @@ void QuantifiersEngine::check( Theory::Effort e ){ // proceed with the check. Assert(false); } - bool needsCheck = !d_lemmas_waiting.empty(); + bool needsCheck = d_qim.hasPendingLemma(); QuantifiersModule::QEffort needsModelE = QuantifiersModule::QEFFORT_NONE; std::vector< QuantifiersModule* > qm; if( d_model->checkNeeded() ){ @@ -362,14 +356,15 @@ void QuantifiersEngine::check( Theory::Effort e ){ } } - d_hasAddedLemma = false; + d_qim.reset(); bool setIncomplete = false; Trace("quant-engine-debug2") << "Quantifiers Engine call to check, level = " << e << ", needsCheck=" << needsCheck << std::endl; if( needsCheck ){ //flush previous lemmas (for instance, if was interrupted), or other lemmas to process - flushLemmas(); - if( d_hasAddedLemma ){ + d_qim.doPending(); + if (d_qim.hasSentLemma()) + { return; } @@ -388,8 +383,10 @@ void QuantifiersEngine::check( Theory::Effort e ){ } Trace("quant-engine-debug") << std::endl; Trace("quant-engine-debug") << " # quantified formulas = " << d_model->getNumAssertedQuantifiers() << std::endl; - if( !d_lemmas_waiting.empty() ){ - Trace("quant-engine-debug") << " lemmas waiting = " << d_lemmas_waiting.size() << std::endl; + if (d_qim.hasPendingLemma()) + { + Trace("quant-engine-debug") + << " lemmas waiting = " << d_qim.numPendingLemmas() << std::endl; } Trace("quant-engine-debug") << " Theory engine finished : " @@ -415,8 +412,9 @@ void QuantifiersEngine::check( Theory::Effort e ){ << "..." << std::endl; if (!util->reset(e)) { - flushLemmas(); - if( d_hasAddedLemma ){ + d_qim.doPending(); + if (d_qim.hasSentLemma()) + { return; }else{ //should only fail reset if added a lemma @@ -444,8 +442,9 @@ void QuantifiersEngine::check( Theory::Effort e ){ } Trace("quant-engine-debug") << "Done resetting all modules." << std::endl; //reset may have added lemmas - flushLemmas(); - if( d_hasAddedLemma ){ + d_qim.doPending(); + if (d_qim.hasSentLemma()) + { return; } @@ -469,11 +468,12 @@ void QuantifiersEngine::check( Theory::Effort e ){ { // If we failed to build the model, flush all pending lemmas and // finish. - flushLemmas(); + d_qim.doPending(); break; } } - if( !d_hasAddedLemma ){ + if (!d_qim.hasSentLemma()) + { //check each module for (QuantifiersModule*& mdl : qm) { @@ -488,10 +488,11 @@ void QuantifiersEngine::check( Theory::Effort e ){ } } //flush all current lemmas - flushLemmas(); + d_qim.doPending(); } //if we have added one, stop - if( d_hasAddedLemma ){ + if (d_qim.hasSentLemma()) + { break; }else{ Assert(!d_qstate.isInConflict()); @@ -580,7 +581,7 @@ void QuantifiersEngine::check( Theory::Effort e ){ } Trace("quant-engine-debug") << "Done check modules that needed check." << std::endl; // debug print - if (d_hasAddedLemma) + if (d_qim.hasSentLemma()) { bool debugInstTrace = Trace.isOn("inst-per-quant-round"); if (options::debugInst() || debugInstTrace) @@ -593,7 +594,7 @@ void QuantifiersEngine::check( Theory::Effort e ){ if( Trace.isOn("quant-engine") ){ double clSet2 = double(clock())/double(CLOCKS_PER_SEC); Trace("quant-engine") << "Finished quantifiers engine, total time = " << (clSet2-clSet); - Trace("quant-engine") << ", added lemma = " << d_hasAddedLemma; + Trace("quant-engine") << ", sent lemma = " << d_qim.hasSentLemma(); Trace("quant-engine") << std::endl; } @@ -603,7 +604,8 @@ void QuantifiersEngine::check( Theory::Effort e ){ } //SAT case - if( e==Theory::EFFORT_LAST_CALL && !d_hasAddedLemma ){ + if (e == Theory::EFFORT_LAST_CALL && !d_qim.hasSentLemma()) + { if( setIncomplete ){ Trace("quant-engine") << "Set incomplete flag." << std::endl; getOutputChannel().setIncomplete(); @@ -656,7 +658,7 @@ void QuantifiersEngine::registerQuantifierInternal(Node f) if( it==d_quants.end() ){ Trace("quant") << "QuantifiersEngine : Register quantifier "; Trace("quant") << " : " << f << std::endl; - unsigned prev_lemma_waiting = d_lemmas_waiting.size(); + size_t prev_lemma_waiting = d_qim.numPendingLemmas(); ++(d_statistics.d_num_quant); Assert(f.getKind() == FORALL); // register with utilities @@ -684,11 +686,11 @@ void QuantifiersEngine::registerQuantifierInternal(Node f) mdl->registerQuantifier(f); // since this is context-independent, we should not add any lemmas during // this call - Assert(d_lemmas_waiting.size() == prev_lemma_waiting); + Assert(d_qim.numPendingLemmas() == prev_lemma_waiting); } Trace("quant-debug") << "...finish." << std::endl; d_quants[f] = true; - AlwaysAssert(d_lemmas_waiting.size() == prev_lemma_waiting); + AlwaysAssert(d_qim.numPendingLemmas() == prev_lemma_waiting); } } @@ -717,7 +719,7 @@ void QuantifiersEngine::preRegisterQuantifier(Node q) mdl->preRegisterQuantifier(q); } // flush the lemmas - flushLemmas(); + d_qim.doPending(); Trace("quant-debug") << "...finish pre-register " << q << "..." << std::endl; } @@ -780,66 +782,10 @@ void QuantifiersEngine::eqNotifyNewClass(TNode t) { addTermToDatabase( t ); } -bool QuantifiersEngine::addLemma( Node lem, bool doCache, bool doRewrite ){ - if( doCache ){ - if( doRewrite ){ - lem = Rewriter::rewrite(lem); - } - Trace("inst-add-debug") << "Adding lemma : " << lem << std::endl; - BoolMap::const_iterator itp = d_lemmas_produced_c.find( lem ); - if( itp==d_lemmas_produced_c.end() || !(*itp).second ){ - d_lemmas_produced_c[ lem ] = true; - d_lemmas_waiting.push_back( lem ); - Trace("inst-add-debug") << "Added lemma" << std::endl; - return true; - }else{ - Trace("inst-add-debug") << "Duplicate." << std::endl; - return false; - } - }else{ - //do not need to rewrite, will be rewritten after sending - d_lemmas_waiting.push_back( lem ); - return true; - } -} - -bool QuantifiersEngine::addTrustedLemma(TrustNode tlem, - bool doCache, - bool doRewrite) -{ - Node lem = tlem.getProven(); - if (!addLemma(lem, doCache, doRewrite)) - { - return false; - } - d_lemmasWaitingPg[lem] = tlem.getGenerator(); - return true; -} - -bool QuantifiersEngine::removeLemma( Node lem ) { - std::vector< Node >::iterator it = std::find( d_lemmas_waiting.begin(), d_lemmas_waiting.end(), lem ); - if( it!=d_lemmas_waiting.end() ){ - d_lemmas_waiting.erase( it, it + 1 ); - d_lemmas_produced_c[ lem ] = false; - return true; - }else{ - return false; - } -} - -void QuantifiersEngine::addRequirePhase( Node lit, bool req ){ - d_phase_req_waiting[lit] = req; -} - void QuantifiersEngine::markRelevant( Node q ) { d_model->markRelevant( q ); } -bool QuantifiersEngine::hasAddedLemma() const -{ - return !d_lemmas_waiting.empty() || d_hasAddedLemma; -} - bool QuantifiersEngine::getInstWhenNeedsCheck( Theory::Effort e ) { Trace("quant-engine-debug2") << "Get inst when needs check, counts=" << d_ierCounter << ", " << d_ierCounter_lc << std::endl; //determine if we should perform check, based on instWhenMode @@ -889,41 +835,6 @@ options::UserPatMode QuantifiersEngine::getInstUserPatMode() } } -void QuantifiersEngine::flushLemmas(){ - OutputChannel& out = getOutputChannel(); - if( !d_lemmas_waiting.empty() ){ - //take default output channel if none is provided - d_hasAddedLemma = true; - std::map<Node, ProofGenerator*>::iterator itp; - // Note: Do not use foreach loop here and do not cache size() call. - // New lemmas can be added while iterating over d_lemmas_waiting. - for (size_t i = 0; i < d_lemmas_waiting.size(); ++i) - { - const Node& lemw = d_lemmas_waiting[i]; - Trace("qe-lemma") << "Lemma : " << lemw << std::endl; - itp = d_lemmasWaitingPg.find(lemw); - LemmaProperty p = LemmaProperty::NEEDS_JUSTIFY; - if (itp != d_lemmasWaitingPg.end()) - { - TrustNode tlemw = TrustNode::mkTrustLemma(lemw, itp->second); - out.trustedLemma(tlemw, p); - } - else - { - out.lemma(lemw, p); - } - } - d_lemmas_waiting.clear(); - } - if( !d_phase_req_waiting.empty() ){ - for( std::map< Node, bool >::iterator it = d_phase_req_waiting.begin(); it != d_phase_req_waiting.end(); ++it ){ - Trace("qe-lemma") << "Require phase : " << it->first << " -> " << it->second << std::endl; - out.requirePhase(it->first, it->second); - } - d_phase_req_waiting.clear(); - } -} - void QuantifiersEngine::getInstantiationTermVectors( Node q, std::vector< std::vector< Node > >& tvecs ) { d_instantiate->getInstantiationTermVectors(q, tvecs); } diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h index 83e01e9e6..cab452e2b 100644 --- a/src/theory/quantifiers_engine.h +++ b/src/theory/quantifiers_engine.h @@ -173,36 +173,11 @@ private: void registerQuantifierInternal(Node q); /** reduceQuantifier, return true if reduced */ bool reduceQuantifier(Node q); - /** flush lemmas */ - void flushLemmas(); public: - /** - * Add lemma to the lemma buffer of this quantifiers engine. - * @param lem The lemma to send - * @param doCache Whether to cache the lemma (to check for duplicate lemmas) - * @param doRewrite Whether to rewrite the lemma - * @return true if the lemma was successfully added to the buffer - */ - bool addLemma(Node lem, bool doCache = true, bool doRewrite = true); - /** - * Add trusted lemma lem, same as above, but where a proof generator may be - * provided along with the lemma. - */ - bool addTrustedLemma(TrustNode tlem, - bool doCache = true, - bool doRewrite = true); - /** remove pending lemma */ - bool removeLemma(Node lem); - /** add require phase */ - void addRequirePhase(Node lit, bool req); /** mark relevant quantified formula, this will indicate it should be checked * before the others */ void markRelevant(Node q); - /** has added lemma */ - bool hasAddedLemma() const; - /** get number of waiting lemmas */ - unsigned getNumLemmasWaiting() { return d_lemmas_waiting.size(); } /** get needs check */ bool getInstWhenNeedsCheck(Theory::Effort e); /** get user pat mode */ @@ -345,9 +320,6 @@ public: * The modules utility, which contains all of the quantifiers modules. */ std::unique_ptr<quantifiers::QuantifiersModules> d_qmodules; - //------------- temporary information during check - /** has added lemma this round */ - bool d_hasAddedLemma; //------------- end temporary information during check private: /** list of all quantifiers seen */ @@ -357,15 +329,6 @@ public: /** quantifiers reduced */ BoolMap d_quants_red; std::map<Node, Node> d_quants_red_lem; - /** list of all lemmas produced */ - // std::map< Node, bool > d_lemmas_produced; - BoolMap d_lemmas_produced_c; - /** lemmas waiting */ - std::vector<Node> d_lemmas_waiting; - /** map from waiting lemmas to their proof generators */ - std::map<Node, ProofGenerator*> d_lemmasWaitingPg; - /** phase requirements waiting */ - std::map<Node, bool> d_phase_req_waiting; /** inst round counters TODO: make context-dependent? */ context::CDO<int> d_ierCounter_c; int d_ierCounter; diff --git a/src/theory/theory_inference_manager.cpp b/src/theory/theory_inference_manager.cpp index ebd68a982..58a8b86a4 100644 --- a/src/theory/theory_inference_manager.cpp +++ b/src/theory/theory_inference_manager.cpp @@ -36,6 +36,9 @@ TheoryInferenceManager::TheoryInferenceManager(Theory& t, d_numCurrentLemmas(0), d_numCurrentFacts(0) { + // don't add true lemma + Node truen = NodeManager::currentNM()->mkConst(true); + d_lemmasSent.insert(truen); } void TheoryInferenceManager::setEqualityEngine(eq::EqualityEngine* ee) |