diff options
Diffstat (limited to 'src/theory/quantifiers')
-rw-r--r-- | src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp | 6 | ||||
-rw-r--r-- | src/theory/quantifiers/conjecture_generator.cpp | 4 | ||||
-rw-r--r-- | src/theory/quantifiers/ematching/ho_trigger.cpp | 2 | ||||
-rw-r--r-- | src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp | 2 | ||||
-rw-r--r-- | src/theory/quantifiers/ematching/trigger.cpp | 2 | ||||
-rw-r--r-- | src/theory/quantifiers/fmf/bounded_integers.cpp | 2 | ||||
-rw-r--r-- | src/theory/quantifiers/instantiate.cpp | 4 | ||||
-rw-r--r-- | src/theory/quantifiers/quant_split.cpp | 2 | ||||
-rw-r--r-- | src/theory/quantifiers/sygus/synth_conjecture.cpp | 2 | ||||
-rw-r--r-- | src/theory/quantifiers/sygus/synth_engine.cpp | 2 | ||||
-rw-r--r-- | src/theory/quantifiers/sygus_inst.cpp | 4 | ||||
-rw-r--r-- | src/theory/quantifiers/term_database.cpp | 4 |
12 files changed, 18 insertions, 18 deletions
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<Node>& 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; |