diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-02-19 09:26:36 -0600 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-02-19 09:26:36 -0600 |
| commit | c4822869beac8d4a0eac4b234e0662d3db49f995 (patch) | |
| tree | d34b86c54b0ac8de6df4734e1e76afa5f43d5efb /src/theory/uf | |
| parent | 00479d03cdeac3e864a1930dddb16c71c5bf2ce9 (diff) | |
Refactoring theory inference process (#5920)
This PR refactors TheoryInference so that it is not responsible for calling back into InferenceManager, instead it sets data so that InferenceManagerBuffered has enough information to do this itself. It also makes the decision of whether to cache lemmas in theory inference manager a global choice per-theory instead of per-lemma.
Diffstat (limited to 'src/theory/uf')
| -rw-r--r-- | src/theory/uf/cardinality_extension.cpp | 6 | ||||
| -rw-r--r-- | src/theory/uf/theory_uf.cpp | 2 |
2 files changed, 4 insertions, 4 deletions
diff --git a/src/theory/uf/cardinality_extension.cpp b/src/theory/uf/cardinality_extension.cpp index 861da3558..aa73e3419 100644 --- a/src/theory/uf/cardinality_extension.cpp +++ b/src/theory/uf/cardinality_extension.cpp @@ -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, InferenceId::UF_CARD_ENFORCE_NEGATIVE, LemmaProperty::NONE, false); + d_im.lemma(lem, InferenceId::UF_CARD_ENFORCE_NEGATIVE); 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, InferenceId::UF_CARD_EQUIV, LemmaProperty::NONE, false); + d_im.lemma(eqv_lit, InferenceId::UF_CARD_EQUIV); 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, InferenceId::UF_CARD_SPLIT, LemmaProperty::NONE, false); + d_im.lemma(lem, InferenceId::UF_CARD_SPLIT); d_im.requirePhase(eq, true); type_proc[tn] = true; break; diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp index 0328080ee..db8b89d89 100644 --- a/src/theory/uf/theory_uf.cpp +++ b/src/theory/uf/theory_uf.cpp @@ -51,7 +51,7 @@ TheoryUF::TheoryUF(context::Context* c, d_functionsTerms(c), d_symb(u, instanceName), d_state(c, u, valuation), - d_im(*this, d_state, pnm, "theory::uf"), + d_im(*this, d_state, pnm, "theory::uf", false), d_notify(d_im, *this) { d_true = NodeManager::currentNM()->mkConst( true ); |