diff options
Diffstat (limited to 'src/theory/shared_terms_database.cpp')
| -rw-r--r-- | src/theory/shared_terms_database.cpp | 39 |
1 files changed, 25 insertions, 14 deletions
diff --git a/src/theory/shared_terms_database.cpp b/src/theory/shared_terms_database.cpp index a13ac207a..6d87530cb 100644 --- a/src/theory/shared_terms_database.cpp +++ b/src/theory/shared_terms_database.cpp @@ -23,8 +23,11 @@ using namespace CVC4::theory; namespace CVC4 { +// below, proofs are enabled in d_pfee if we are provided a lazy proof SharedTermsDatabase::SharedTermsDatabase(TheoryEngine* theoryEngine, - context::Context* context) + context::Context* context, + context::UserContext* userContext, + ProofNodeManager* pnm, LazyCDProof* lcp) : ContextNotifyObj(context), d_statSharedTerms("theory::shared_terms", 0), d_addedSharedTermsSize(context, 0), @@ -33,9 +36,11 @@ SharedTermsDatabase::SharedTermsDatabase(TheoryEngine* theoryEngine, d_registeredEqualities(context), d_EENotify(*this), d_equalityEngine(d_EENotify, context, "SharedTermsDatabase", true), + d_pfee(context,userContext,d_equalityEngine,pnm, lcp!=nullptr), d_theoryEngine(theoryEngine), d_inConflict(context, false), - d_conflictPolarity() { + d_conflictPolarity(), + d_lazyPf(lcp) { smtStatisticsRegistry()->registerStat(&d_statSharedTerms); } @@ -198,7 +203,8 @@ void SharedTermsDatabase::assertEquality(TNode equality, bool polarity, TNode re { Debug("shared-terms-database::assert") << "SharedTermsDatabase::assertEquality(" << equality << ", " << (polarity ? "true" : "false") << ", " << reason << ")" << endl; // Add it to the equality engine - d_equalityEngine.assertEquality(equality, polarity, reason); + //d_equalityEngine.assertEquality(equality, polarity, reason); + d_pfee.assertAssume(reason); // Check for conflict checkForConflict(); } @@ -237,10 +243,19 @@ static Node mkAnd(const std::vector<TNode>& conjunctions) { void SharedTermsDatabase::checkForConflict() { if (d_inConflict) { d_inConflict = false; - std::vector<TNode> assumptions; - d_equalityEngine.explainEquality(d_conflictLHS, d_conflictRHS, d_conflictPolarity, assumptions); - Node conflict = mkAnd(assumptions); - d_theoryEngine->conflict(conflict, THEORY_BUILTIN); + Node conflict = d_conflictLHS.eqNode(d_conflictRHS); + if (!d_conflictPolarity) + { + conflict = conflict.notNode(); + } + TrustNode trnc = d_pfee.assertConflict(conflict); + if (d_lazyPf!=nullptr) + { + // add the step to the proof + Node ckey = TrustNode::getConflictKeyValue(trnc.getNode()); + d_lazyPf->addLazyStep(ckey, &d_pfee); + } + d_theoryEngine->conflict(trnc.getNode(), THEORY_BUILTIN); d_conflictLHS = d_conflictRHS = Node::null(); } } @@ -255,13 +270,9 @@ bool SharedTermsDatabase::isKnown(TNode literal) const { } } -Node SharedTermsDatabase::explain(TNode literal) const { - bool polarity = literal.getKind() != kind::NOT; - TNode atom = polarity ? literal : literal[0]; - Assert(atom.getKind() == kind::EQUAL); - std::vector<TNode> assumptions; - d_equalityEngine.explainEquality(atom[0], atom[1], polarity, assumptions); - return mkAnd(assumptions); +theory::TrustNode SharedTermsDatabase::explain(TNode literal) { + TrustNode trn = d_pfee.explain(literal); + return trn; } } /* namespace CVC4 */ |