diff options
Diffstat (limited to 'src/theory/uf')
-rw-r--r-- | src/theory/uf/cardinality_extension.cpp | 16 | ||||
-rw-r--r-- | src/theory/uf/ho_extension.cpp | 10 | ||||
-rw-r--r-- | src/theory/uf/theory_uf.cpp | 2 |
3 files changed, 14 insertions, 14 deletions
diff --git a/src/theory/uf/cardinality_extension.cpp b/src/theory/uf/cardinality_extension.cpp index bd69245b8..697a828a4 100644 --- a/src/theory/uf/cardinality_extension.cpp +++ b/src/theory/uf/cardinality_extension.cpp @@ -1037,7 +1037,7 @@ int SortModel::addSplit(Region* r) //split on the equality s Node lem = NodeManager::currentNM()->mkNode( kind::OR, ss, ss.negate() ); // send lemma, with caching - if (d_im.lemma(lem)) + if (d_im.lemma(lem, InferenceId::UNKNOWN)) { Trace("uf-ss-lemma") << "*** Split on " << s << std::endl; //tell the sat solver to explore the equals branch first @@ -1070,7 +1070,7 @@ void SortModel::addCliqueLemma(std::vector<Node>& clique) eqs.push_back(d_cardinality_literal[d_cardinality].notNode()); Node lem = NodeManager::currentNM()->mkNode(OR, eqs); // send lemma, with caching - if (d_im.lemma(lem)) + if (d_im.lemma(lem, InferenceId::UNKNOWN)) { Trace("uf-ss-lemma") << "*** Add clique lemma " << lem << std::endl; ++(d_thss->d_statistics.d_clique_lemmas); @@ -1082,7 +1082,7 @@ void SortModel::simpleCheckCardinality() { Node lem = NodeManager::currentNM()->mkNode( AND, getCardinalityLiteral( d_cardinality.get() ), getCardinalityLiteral( d_maxNegCard.get() ).negate() ); Trace("uf-ss-lemma") << "*** Simple cardinality conflict : " << lem << std::endl; - d_im.conflict(lem); + d_im.conflict(lem, InferenceId::UNKNOWN); } } @@ -1179,7 +1179,7 @@ bool SortModel::checkLastCall() Node lem = NodeManager::currentNM()->mkNode( OR, cl, NodeManager::currentNM()->mkAnd(force_cl)); Trace("uf-ss-lemma") << "*** Enforce negative cardinality constraint lemma : " << lem << std::endl; - d_im.lemma(lem, LemmaProperty::NONE, false); + d_im.lemma(lem, InferenceId::UNKNOWN, LemmaProperty::NONE, false); return false; } } @@ -1399,7 +1399,7 @@ void CardinalityExtension::assertNode(Node n, bool isDecision) Node eqv_lit = NodeManager::currentNM()->mkNode( CARDINALITY_CONSTRAINT, ct, lit[1] ); eqv_lit = lit.eqNode( eqv_lit ); Trace("uf-ss-lemma") << "*** Cardinality equiv lemma : " << eqv_lit << std::endl; - d_im.lemma(eqv_lit, LemmaProperty::NONE, false); + d_im.lemma(eqv_lit, InferenceId::UNKNOWN, LemmaProperty::NONE, false); d_card_assertions_eqv_lemma[lit] = true; } } @@ -1528,7 +1528,7 @@ void CardinalityExtension::check(Theory::Effort level) Node eq = Rewriter::rewrite( a.eqNode( b ) ); Node lem = NodeManager::currentNM()->mkNode( kind::OR, eq, eq.negate() ); Trace("uf-ss-lemma") << "*** Split (no-minimal) : " << lem << std::endl; - d_im.lemma(lem, LemmaProperty::NONE, false); + d_im.lemma(lem, InferenceId::UNKNOWN, LemmaProperty::NONE, false); d_im.requirePhase(eq, true); type_proc[tn] = true; break; @@ -1707,7 +1707,7 @@ void CardinalityExtension::checkCombinedCardinality() << " : " << cf << std::endl; Trace("uf-ss-com-card") << "*** Combined monotone cardinality conflict" << " : " << cf << std::endl; - d_im.conflict(cf); + d_im.conflict(cf, InferenceId::UNKNOWN); return; } } @@ -1745,7 +1745,7 @@ void CardinalityExtension::checkCombinedCardinality() << std::endl; Trace("uf-ss-com-card") << "*** Combined cardinality conflict : " << cf << std::endl; - d_im.conflict(cf); + d_im.conflict(cf, InferenceId::UNKNOWN); } } } diff --git a/src/theory/uf/ho_extension.cpp b/src/theory/uf/ho_extension.cpp index 66bcbc76f..55e2500af 100644 --- a/src/theory/uf/ho_extension.cpp +++ b/src/theory/uf/ho_extension.cpp @@ -107,7 +107,7 @@ unsigned HoExtension::applyExtensionality(TNode deq) Node lem = NodeManager::currentNM()->mkNode(OR, deq[0], conc); Trace("uf-ho-lemma") << "uf-ho-lemma : extensionality : " << lem << std::endl; - d_im.lemma(lem); + d_im.lemma(lem, InferenceId::UNKNOWN); return 1; } return 0; @@ -167,7 +167,7 @@ Node HoExtension::getApplyUfForHoApply(Node node) Trace("uf-ho-lemma") << "uf-ho-lemma : Skolem definition for apply-conversion : " << lem << std::endl; - d_im.lemma(lem); + d_im.lemma(lem, InferenceId::UNKNOWN); d_uf_std_skolem[f] = new_f; } else @@ -256,7 +256,7 @@ unsigned HoExtension::checkExtensionality(TheoryModel* m) Node lem = nm->mkNode(OR, deq.negate(), eq); Trace("uf-ho") << "HoExtension: cmi extensionality lemma " << lem << std::endl; - d_im.lemma(lem); + d_im.lemma(lem, InferenceId::UNKNOWN); return 1; } } @@ -284,7 +284,7 @@ unsigned HoExtension::applyAppCompletion(TNode n) Node eq = n.eqNode(ret); Trace("uf-ho-lemma") << "uf-ho-lemma : infer, by apply-expand : " << eq << std::endl; - d_im.assertInternalFact(eq, true, PfRule::HO_APP_ENCODE, {}, {n}); + d_im.assertInternalFact(eq, true, InferenceId::UNKNOWN, PfRule::HO_APP_ENCODE, {}, {n}); return 1; } Trace("uf-ho-debug") << " ...already have " << ret << " == " << n << "." @@ -441,7 +441,7 @@ bool HoExtension::collectModelInfoHoTerm(Node n, TheoryModel* m) Node eq = n.eqNode(hn); Trace("uf-ho") << "HoExtension: cmi app completion lemma " << eq << std::endl; - d_im.lemma(eq); + d_im.lemma(eq, InferenceId::UNKNOWN); return false; } } diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp index 6fdc969a4..c8cfe295e 100644 --- a/src/theory/uf/theory_uf.cpp +++ b/src/theory/uf/theory_uf.cpp @@ -315,7 +315,7 @@ void TheoryUF::presolve() { ++i) { Debug("uf") << "uf: generating a lemma: " << *i << std::endl; // no proof generator provided - d_im.lemma(*i); + d_im.lemma(*i, InferenceId::UNKNOWN); } } if( d_thss ){ |