From ccda071a9605baa42602d580affa296cbc674807 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Mon, 21 Dec 2020 11:48:22 -0600 Subject: Move ownership of theory preprocessor to TheoryProxy (#5690) With this PR, TheoryEngine is independent of theory preprocessing. All theory preprocessing is handled at the level of PropEngine. No significant behavior changes in this PR. The next step will make theory preprocessing not mandatory in preprocessing, and optionally done instead at the time when literals are asserted to TheoryEngine. --- src/prop/prop_engine.cpp | 130 +++++++++++++++++++++++++++++++++++++---------- 1 file changed, 104 insertions(+), 26 deletions(-) (limited to 'src/prop/prop_engine.cpp') diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp index a8a92096c..8352373c5 100644 --- a/src/prop/prop_engine.cpp +++ b/src/prop/prop_engine.cpp @@ -36,6 +36,7 @@ #include "prop/sat_solver_factory.h" #include "prop/theory_proxy.h" #include "smt/smt_statistics_registry.h" +#include "theory/output_channel.h" #include "theory/theory_engine.h" #include "theory/theory_registrar.h" #include "util/resource_manager.h" @@ -94,8 +95,14 @@ PropEngine::PropEngine(TheoryEngine* te, d_registrar = new theory::TheoryRegistrar(d_theoryEngine); d_cnfStream = new CVC4::prop::CnfStream( d_satSolver, d_registrar, userContext, &d_outMgr, rm, true); - d_theoryProxy = new TheoryProxy( - this, d_theoryEngine, d_decisionEngine.get(), d_context, d_cnfStream); + + d_theoryProxy = new TheoryProxy(this, + d_theoryEngine, + d_decisionEngine.get(), + d_context, + userContext, + d_cnfStream, + pnm); d_satSolver->initialize(d_context, d_theoryProxy, userContext, pnm); d_decisionEngine->setSatSolver(d_satSolver); @@ -143,6 +150,16 @@ PropEngine::~PropEngine() { delete d_theoryProxy; } +theory::TrustNode PropEngine::preprocess( + TNode node, + std::vector& newLemmas, + std::vector& newSkolems, + bool doTheoryPreprocess) +{ + return d_theoryProxy->preprocess( + node, newLemmas, newSkolems, doTheoryPreprocess); +} + void PropEngine::notifyPreprocessedAssertions( const preprocessing::AssertionPipeline& ap) { @@ -168,7 +185,6 @@ void PropEngine::notifyPreprocessedAssertions( void PropEngine::assertFormula(TNode node) { Assert(!d_inCheckSat) << "Sat solver in solve()!"; Debug("prop") << "assertFormula(" << node << ")" << endl; - // Assert as non-removable if (isProofEnabled()) { d_pfCnfStream->convertAndAssert(node, false, false, nullptr); @@ -181,35 +197,47 @@ void PropEngine::assertFormula(TNode node) { } } -void PropEngine::assertLemma(theory::TrustNode trn, bool removable) +Node PropEngine::assertLemma(theory::TrustNode tlemma, theory::LemmaProperty p) { - Node node = trn.getNode(); - bool negated = trn.getKind() == theory::TrustNodeKind::CONFLICT; - Debug("prop::lemmas") << "assertLemma(" << node << ")" << endl; - // Assert as (possibly) removable - if (isProofEnabled()) + bool removable = isLemmaPropertyRemovable(p); + bool preprocess = isLemmaPropertyPreprocess(p); + + // call preprocessor + std::vector ppLemmas; + std::vector ppSkolems; + theory::TrustNode tplemma = + d_theoryProxy->preprocessLemma(tlemma, ppLemmas, ppSkolems, preprocess); + + Assert(ppSkolems.size() == ppLemmas.size()); + + // do final checks on the lemmas we are about to send + if (isProofEnabled() && options::proofNewEagerChecking()) { - Assert(trn.getGenerator()); - d_pfCnfStream->convertAndAssert( - node, negated, removable, trn.getGenerator()); + Assert(tplemma.getGenerator() != nullptr); + // ensure closed, make the proof node eagerly here to debug + tplemma.debugCheckClosed("te-proof-debug", "TheoryEngine::lemma"); + for (size_t i = 0, lsize = ppLemmas.size(); i < lsize; ++i) + { + Assert(ppLemmas[i].getGenerator() != nullptr); + ppLemmas[i].debugCheckClosed("te-proof-debug", "TheoryEngine::lemma_new"); + } } - else + + if (Trace.isOn("te-lemma")) { - d_cnfStream->convertAndAssert(node, removable, negated); + Trace("te-lemma") << "Lemma, output: " << tplemma.getProven() << std::endl; + for (size_t i = 0, lsize = ppLemmas.size(); i < lsize; ++i) + { + Trace("te-lemma") << "Lemma, new lemma: " << ppLemmas[i].getProven() + << " (skolem is " << ppSkolems[i] << ")" << std::endl; + } } -} -void PropEngine::assertLemmas(theory::TrustNode lem, - std::vector& ppLemmas, - std::vector& ppSkolems, - bool removable) -{ - Assert(ppSkolems.size() == ppLemmas.size()); - // assert the lemmas - assertLemma(lem, removable); + // now, assert the lemmas + assertLemmaInternal(tplemma, removable); for (size_t i = 0, lsize = ppLemmas.size(); i < lsize; ++i) { - assertLemma(ppLemmas[i], removable); + assertLemmaInternal(ppLemmas[i], removable); } // assert to decision engine @@ -217,7 +245,7 @@ void PropEngine::assertLemmas(theory::TrustNode lem, { // also add to the decision engine, where notice we don't need proofs std::vector assertions; - assertions.push_back(lem.getProven()); + assertions.push_back(tplemma.getProven()); std::vector ppLemmasF; for (const theory::TrustNode& tnl : ppLemmas) { @@ -225,6 +253,38 @@ void PropEngine::assertLemmas(theory::TrustNode lem, } d_decisionEngine->addAssertions(assertions, ppLemmasF, ppSkolems); } + + // make the return lemma, which the theory engine will use + Node retLemma = tplemma.getProven(); + if (!ppLemmas.empty()) + { + std::vector lemmas{retLemma}; + for (const theory::TrustNode& tnl : ppLemmas) + { + lemmas.push_back(tnl.getProven()); + } + // the returned lemma is the conjunction of all additional lemmas. + retLemma = NodeManager::currentNM()->mkNode(kind::AND, lemmas); + } + return retLemma; +} + +void PropEngine::assertLemmaInternal(theory::TrustNode trn, bool removable) +{ + Node node = trn.getNode(); + bool negated = trn.getKind() == theory::TrustNodeKind::CONFLICT; + Debug("prop::lemmas") << "assertLemma(" << node << ")" << endl; + // Assert as (possibly) removable + if (isProofEnabled()) + { + Assert(trn.getGenerator()); + d_pfCnfStream->convertAndAssert( + node, negated, removable, trn.getGenerator()); + } + else + { + d_cnfStream->convertAndAssert(node, removable, negated); + } } void PropEngine::requirePhase(TNode n, bool phase) { @@ -361,7 +421,25 @@ void PropEngine::getBooleanVariables(std::vector& outputVariables) const d_cnfStream->getBooleanVariables(outputVariables); } -void PropEngine::ensureLiteral(TNode n) { d_cnfStream->ensureLiteral(n); } +Node PropEngine::ensureLiteral(TNode n) +{ + // must preprocess + std::vector newLemmas; + std::vector newSkolems; + theory::TrustNode tpn = + d_theoryProxy->preprocess(n, newLemmas, newSkolems, true); + // send lemmas corresponding to the skolems introduced by preprocessing n + for (const theory::TrustNode& tnl : newLemmas) + { + Trace("ensureLiteral") << " lemma: " << tnl.getNode() << std::endl; + assertLemma(tnl, theory::LemmaProperty::NONE); + } + Node preprocessed = tpn.isNull() ? Node(n) : tpn.getNode(); + Trace("ensureLiteral") << "ensureLiteral preprocessed: " << preprocessed + << std::endl; + d_cnfStream->ensureLiteral(preprocessed); + return preprocessed; +} void PropEngine::push() { -- cgit v1.2.3