summaryrefslogtreecommitdiff
path: root/src/theory/quantifiers
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/quantifiers')
-rw-r--r--src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp6
-rw-r--r--src/theory/quantifiers/conjecture_generator.cpp4
-rw-r--r--src/theory/quantifiers/ematching/ho_trigger.cpp2
-rw-r--r--src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp2
-rw-r--r--src/theory/quantifiers/ematching/trigger.cpp2
-rw-r--r--src/theory/quantifiers/fmf/bounded_integers.cpp2
-rw-r--r--src/theory/quantifiers/instantiate.cpp4
-rw-r--r--src/theory/quantifiers/quant_split.cpp2
-rw-r--r--src/theory/quantifiers/sygus/synth_conjecture.cpp2
-rw-r--r--src/theory/quantifiers/sygus/synth_engine.cpp2
-rw-r--r--src/theory/quantifiers/sygus_inst.cpp4
-rw-r--r--src/theory/quantifiers/term_database.cpp4
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;
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback