summaryrefslogtreecommitdiff
path: root/src/theory
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory')
-rw-r--r--src/theory/datatypes/theory_datatypes.cpp6
-rw-r--r--src/theory/inference_manager_buffered.cpp6
-rw-r--r--src/theory/inference_manager_buffered.h8
-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
-rw-r--r--src/theory/sep/theory_sep.cpp4
-rw-r--r--src/theory/sets/inference_manager.cpp4
17 files changed, 36 insertions, 28 deletions
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<Rational>().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<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;
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;
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback