From: Gereon Kremer Date: Wed, 17 Feb 2021 13:42:50 +0000 (+0100) Subject: Add InferenceId to buffered inference manager (#5911) X-Git-Tag: cvc5-1.0.0~2274 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=2d6de44a51fed47a625ae73181efbcc3dac0c751;p=cvc5.git Add InferenceId to buffered inference manager (#5911) This PR collects the InferenceId in the InferenceManagerBuffered class. --- diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp index 153f7c850..dc7bdc369 100644 --- a/src/theory/datatypes/theory_datatypes.cpp +++ b/src/theory/datatypes/theory_datatypes.cpp @@ -850,7 +850,7 @@ Node TheoryDatatypes::getTermSkolemFor( Node n ) { d_term_sk[n] = k; Node eq = k.eqNode( n ); Trace("datatypes-infer") << "DtInfer : ref : " << eq << std::endl; - d_im.addPendingLemma(eq); + d_im.addPendingLemma(eq, InferenceId::UNKNOWN); return k; }else{ return (*it).second; @@ -1473,7 +1473,7 @@ void TheoryDatatypes::collectTerms( Node n ) { Node lem = nm->mkNode(LEQ, d_zero, n); Trace("datatypes-infer") << "DtInfer : size geq zero : " << lem << std::endl; - d_im.addPendingLemma(lem); + d_im.addPendingLemma(lem, InferenceId::UNKNOWN); } else if (nk == DT_HEIGHT_BOUND && n[1].getConst().isZero()) { @@ -1498,7 +1498,7 @@ void TheoryDatatypes::collectTerms( Node n ) { : nm->mkNode(OR, children)); } Trace("datatypes-infer") << "DtInfer : zero height : " << lem << std::endl; - d_im.addPendingLemma(lem); + d_im.addPendingLemma(lem, InferenceId::UNKNOWN); } } diff --git a/src/theory/inference_manager_buffered.cpp b/src/theory/inference_manager_buffered.cpp index e5f6ae4e4..6789043b1 100644 --- a/src/theory/inference_manager_buffered.cpp +++ b/src/theory/inference_manager_buffered.cpp @@ -45,6 +45,7 @@ bool InferenceManagerBuffered::hasPendingLemma() const } bool InferenceManagerBuffered::addPendingLemma(Node lem, + InferenceId id, LemmaProperty p, ProofGenerator* pg, bool checkCache) @@ -59,7 +60,7 @@ bool InferenceManagerBuffered::addPendingLemma(Node lem, } } // make the simple theory lemma - d_pendingLem.emplace_back(new SimpleTheoryLemma(InferenceId::UNKNOWN, lem, p, pg)); + d_pendingLem.emplace_back(new SimpleTheoryLemma(id, lem, p, pg)); return true; } @@ -70,12 +71,13 @@ void InferenceManagerBuffered::addPendingLemma( } void InferenceManagerBuffered::addPendingFact(Node conc, + InferenceId id, Node exp, ProofGenerator* pg) { // make a simple theory internal fact Assert(conc.getKind() != AND && conc.getKind() != OR); - d_pendingFact.emplace_back(new SimpleTheoryInternalFact(InferenceId::UNKNOWN, conc, exp, pg)); + d_pendingFact.emplace_back(new SimpleTheoryInternalFact(id, conc, exp, pg)); } void InferenceManagerBuffered::addPendingFact( diff --git a/src/theory/inference_manager_buffered.h b/src/theory/inference_manager_buffered.h index 28014ce8e..f9cddadd3 100644 --- a/src/theory/inference_manager_buffered.h +++ b/src/theory/inference_manager_buffered.h @@ -54,6 +54,7 @@ class InferenceManagerBuffered : public TheoryInferenceManager * doPendingLemmas. * * @param lem The lemma to send + * @param id The identifier of the inference * @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 @@ -62,6 +63,7 @@ class InferenceManagerBuffered : public TheoryInferenceManager * false if the lemma is already cached. */ bool addPendingLemma(Node lem, + InferenceId id, LemmaProperty p = LemmaProperty::NONE, ProofGenerator* pg = nullptr, bool checkCache = true); @@ -79,8 +81,12 @@ class InferenceManagerBuffered : public TheoryInferenceManager * * Pending facts are sent to the equality engine of this class using * doPendingFacts. + * @param conc The conclustion + * @param id The identifier of the inference + * @param exp The explanation in the equality engine of the theory + * @param pg The proof generator which can provide a proof for conc */ - void addPendingFact(Node conc, Node exp, ProofGenerator* pg = nullptr); + void addPendingFact(Node conc, InferenceId id, Node exp, ProofGenerator* pg = nullptr); /** * Add pending fact, where fact can be a (derived) class of the * theory inference base class. diff --git a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp index 208933456..c37054fdd 100644 --- a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp +++ b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp @@ -394,7 +394,7 @@ void InstStrategyCegqi::registerCounterexampleLemma(Node q, Node lem) { Trace("cegqi-debug") << "Auxiliary CE lemma " << i << " : " << auxLems[i] << std::endl; - d_qim.addPendingLemma(auxLems[i]); + d_qim.addPendingLemma(auxLems[i], InferenceId::UNKNOWN); } } @@ -495,7 +495,7 @@ bool InstStrategyCegqi::doAddInstantiation( std::vector< Node >& subs ) { bool InstStrategyCegqi::addPendingLemma(Node lem) const { - return d_qim.addPendingLemma(lem); + return d_qim.addPendingLemma(lem, InferenceId::UNKNOWN); } CegInstantiator * InstStrategyCegqi::getInstantiator( Node q ) { @@ -536,7 +536,7 @@ bool InstStrategyCegqi::processNestedQe(Node q, bool isPreregister) // add lemmas to process for (const Node& lem : lems) { - d_qim.addPendingLemma(lem); + d_qim.addPendingLemma(lem, InferenceId::UNKNOWN); } // don't need to process this, since it has been reduced return true; diff --git a/src/theory/quantifiers/conjecture_generator.cpp b/src/theory/quantifiers/conjecture_generator.cpp index 57c5533a9..96bb9a9f7 100644 --- a/src/theory/quantifiers/conjecture_generator.cpp +++ b/src/theory/quantifiers/conjecture_generator.cpp @@ -349,7 +349,7 @@ bool ConjectureGenerator::hasEnumeratedUf( Node n ) { if( !lem.empty() ){ for (const Node& l : lem) { - d_qim.addPendingLemma(l); + d_qim.addPendingLemma(l, InferenceId::UNKNOWN); } d_hasAddedLemma = true; return false; @@ -934,7 +934,7 @@ unsigned ConjectureGenerator::flushWaitingConjectures( unsigned& addedLemmas, in d_eq_conjectures[rhs].push_back( lhs ); Node lem = NodeManager::currentNM()->mkNode( OR, rsg.negate(), rsg ); - d_qim.addPendingLemma(lem); + d_qim.addPendingLemma(lem, InferenceId::UNKNOWN); d_qim.addPendingPhaseRequirement(rsg, false); addedLemmas++; if( (int)addedLemmas>=options::conjectureGenPerRound() ){ diff --git a/src/theory/quantifiers/ematching/ho_trigger.cpp b/src/theory/quantifiers/ematching/ho_trigger.cpp index 7cc1074aa..0ab2988d2 100644 --- a/src/theory/quantifiers/ematching/ho_trigger.cpp +++ b/src/theory/quantifiers/ematching/ho_trigger.cpp @@ -498,7 +498,7 @@ uint64_t HigherOrderTrigger::addHoTypeMatchPredicateLemmas() { Node u = tdb->getHoTypeMatchPredicate(tn); Node au = nm->mkNode(kind::APPLY_UF, u, f); - if (d_qim.addPendingLemma(au)) + if (d_qim.addPendingLemma(au, InferenceId::UNKNOWN)) { // 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/inst_strategy_e_matching.cpp b/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp index 881133432..90d8de128 100644 --- a/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp +++ b/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp @@ -632,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_qim.addPendingLemma(lem); + d_qim.addPendingLemma(lem, InferenceId::UNKNOWN); return; } unsigned tindex; diff --git a/src/theory/quantifiers/ematching/trigger.cpp b/src/theory/quantifiers/ematching/trigger.cpp index 58d94a11d..3bc5ded16 100644 --- a/src/theory/quantifiers/ematching/trigger.cpp +++ b/src/theory/quantifiers/ematching/trigger.cpp @@ -123,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_qim.addPendingLemma(eq); + d_qim.addPendingLemma(eq, InferenceId::UNKNOWN); gtAddedLemmas++; } } diff --git a/src/theory/quantifiers/fmf/bounded_integers.cpp b/src/theory/quantifiers/fmf/bounded_integers.cpp index 0a0d155f9..5a0407f1f 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_qim.addPendingLemma(prangeLem); + d_qim.addPendingLemma(prangeLem, InferenceId::UNKNOWN); addedLemma = true; } } diff --git a/src/theory/quantifiers/instantiate.cpp b/src/theory/quantifiers/instantiate.cpp index 9588bba7f..b4fed5b13 100644 --- a/src/theory/quantifiers/instantiate.cpp +++ b/src/theory/quantifiers/instantiate.cpp @@ -324,11 +324,11 @@ bool Instantiate::addInstantiation( if (hasProof) { // use proof generator - addedLem = d_qim.addPendingLemma(lem, LemmaProperty::NONE, d_pfInst.get()); + addedLem = d_qim.addPendingLemma(lem, InferenceId::UNKNOWN, LemmaProperty::NONE, d_pfInst.get()); } else { - addedLem = d_qim.addPendingLemma(lem); + addedLem = d_qim.addPendingLemma(lem, InferenceId::UNKNOWN); } if (!addedLem) diff --git a/src/theory/quantifiers/quant_split.cpp b/src/theory/quantifiers/quant_split.cpp index f782ae7ef..a0b780836 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_qim.addPendingLemma(lem); + d_qim.addPendingLemma(lem, InferenceId::UNKNOWN); } Trace("quant-dsplit") << "QuantDSplit::check finished" << std::endl; } diff --git a/src/theory/quantifiers/sygus/synth_conjecture.cpp b/src/theory/quantifiers/sygus/synth_conjecture.cpp index 7bae92184..59edd3070 100644 --- a/src/theory/quantifiers/sygus/synth_conjecture.cpp +++ b/src/theory/quantifiers/sygus/synth_conjecture.cpp @@ -723,7 +723,7 @@ bool SynthConjecture::doRefine() { Trace("cegqi-lemma") << "Cegqi::Lemma : candidate refinement : " << lem << std::endl; - bool res = d_qim.addPendingLemma(lem); + bool res = d_qim.addPendingLemma(lem, InferenceId::UNKNOWN); if (res) { ++(d_stats.d_cegqi_lemmas_refine); diff --git a/src/theory/quantifiers/sygus/synth_engine.cpp b/src/theory/quantifiers/sygus/synth_engine.cpp index c12f387bc..e4c8c6cec 100644 --- a/src/theory/quantifiers/sygus/synth_engine.cpp +++ b/src/theory/quantifiers/sygus/synth_engine.cpp @@ -224,7 +224,7 @@ bool SynthEngine::checkConjecture(SynthConjecture* conj) bool addedLemma = false; for (const Node& lem : cclems) { - if (d_qim.addPendingLemma(lem)) + if (d_qim.addPendingLemma(lem, InferenceId::UNKNOWN)) { ++(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 f6827d1c4..e59b788b6 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& lemmas) for (const Node& lem : lemmas) { Trace("sygus-inst") << "Evaluation unfolding: " << lem << std::endl; - added_lemma |= d_qim.addPendingLemma(lem); + added_lemma |= d_qim.addPendingLemma(lem, InferenceId::UNKNOWN); } return added_lemma; } @@ -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_qim.addPendingLemma(lem); + d_qim.addPendingLemma(lem, InferenceId::UNKNOWN); 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 b83cdf3e5..61a62a820 100644 --- a/src/theory/quantifiers/term_database.cpp +++ b/src/theory/quantifiers/term_database.cpp @@ -435,7 +435,7 @@ void TermDb::computeUfTerms( TNode f ) { } Trace("term-db-lemma") << " add lemma : " << lem << std::endl; } - d_qim.addPendingLemma(lem); + d_qim.addPendingLemma(lem, InferenceId::UNKNOWN); d_qstate.notifyInConflict(); d_consistent_ee = false; return; @@ -1044,7 +1044,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_qim.addPendingLemma(eq); + d_qim.addPendingLemma(eq, InferenceId::UNKNOWN); d_qstate.notifyInConflict(); d_consistent_ee = false; return false; diff --git a/src/theory/sep/theory_sep.cpp b/src/theory/sep/theory_sep.cpp index a38a92b6a..8782bfe34 100644 --- a/src/theory/sep/theory_sep.cpp +++ b/src/theory/sep/theory_sep.cpp @@ -1782,7 +1782,7 @@ void TheorySep::sendLemma( std::vector< Node >& ant, Node conc, const char * c, if( infer && conc!=d_false ){ Node ant_n = NodeManager::currentNM()->mkAnd(ant); Trace("sep-lemma") << "Sep::Infer: " << conc << " from " << ant_n << " by " << c << std::endl; - d_im.addPendingFact(conc, ant_n); + d_im.addPendingFact(conc, InferenceId::UNKNOWN, ant_n); }else{ if( conc==d_false ){ Trace("sep-lemma") << "Sep::Conflict: " << ant << " by " << c @@ -1793,7 +1793,7 @@ void TheorySep::sendLemma( std::vector< Node >& ant, Node conc, const char * c, << " by " << c << std::endl; TrustNode trn = d_im.mkLemmaExp(conc, ant, {}); d_im.addPendingLemma( - trn.getNode(), LemmaProperty::NONE, trn.getGenerator()); + trn.getNode(), InferenceId::UNKNOWN, LemmaProperty::NONE, trn.getGenerator()); } } } diff --git a/src/theory/sets/inference_manager.cpp b/src/theory/sets/inference_manager.cpp index 15b7f64dc..2629e2cbd 100644 --- a/src/theory/sets/inference_manager.cpp +++ b/src/theory/sets/inference_manager.cpp @@ -46,7 +46,7 @@ bool InferenceManager::assertFactRec(Node fact, Node exp, int inferType) { lem = NodeManager::currentNM()->mkNode(IMPLIES, exp, fact); } - addPendingLemma(lem); + addPendingLemma(lem, InferenceId::UNKNOWN); return true; } Trace("sets-fact") << "Assert fact rec : " << fact << ", exp = " << exp @@ -104,7 +104,7 @@ bool InferenceManager::assertFactRec(Node fact, Node exp, int inferType) { lem = NodeManager::currentNM()->mkNode(IMPLIES, exp, fact); } - addPendingLemma(lem); + addPendingLemma(lem, InferenceId::UNKNOWN); return true; } return false;