diff options
| -rw-r--r-- | src/preprocessing/passes/ite_removal.cpp | 6 | ||||
| -rw-r--r-- | src/preprocessing/passes/theory_preprocess.cpp | 43 | ||||
| -rw-r--r-- | src/prop/prop_engine.cpp | 130 | ||||
| -rw-r--r-- | src/prop/prop_engine.h | 59 | ||||
| -rw-r--r-- | src/prop/theory_proxy.cpp | 30 | ||||
| -rw-r--r-- | src/prop/theory_proxy.h | 27 | ||||
| -rw-r--r-- | src/smt/process_assertions.cpp | 7 | ||||
| -rw-r--r-- | src/theory/theory_engine.cpp | 81 | ||||
| -rw-r--r-- | src/theory/theory_engine.h | 11 | ||||
| -rw-r--r-- | src/theory/theory_preprocessor.h | 11 |
10 files changed, 238 insertions, 167 deletions
diff --git a/src/preprocessing/passes/ite_removal.cpp b/src/preprocessing/passes/ite_removal.cpp index 3531497e8..d2f053379 100644 --- a/src/preprocessing/passes/ite_removal.cpp +++ b/src/preprocessing/passes/ite_removal.cpp @@ -38,15 +38,13 @@ PreprocessingPassResult IteRemoval::applyInternal(AssertionPipeline* assertions) IteSkolemMap& imap = assertions->getIteSkolemMap(); // Remove all of the ITE occurrences and normalize - theory::TheoryPreprocessor* tpp = - d_preprocContext->getTheoryEngine()->getTheoryPreprocess(); + prop::PropEngine* pe = d_preprocContext->getPropEngine(); for (unsigned i = 0, size = assertions->size(); i < size; ++i) { Node assertion = (*assertions)[i]; std::vector<theory::TrustNode> newAsserts; std::vector<Node> newSkolems; - // TODO (project #42): this will call the prop engine - TrustNode trn = tpp->preprocess(assertion, newAsserts, newSkolems, false); + TrustNode trn = pe->preprocess(assertion, newAsserts, newSkolems, false); if (!trn.isNull()) { // process diff --git a/src/preprocessing/passes/theory_preprocess.cpp b/src/preprocessing/passes/theory_preprocess.cpp index e888e7a2b..6c751f864 100644 --- a/src/preprocessing/passes/theory_preprocess.cpp +++ b/src/preprocessing/passes/theory_preprocess.cpp @@ -29,17 +29,44 @@ TheoryPreprocess::TheoryPreprocess(PreprocessingPassContext* preprocContext) : PreprocessingPass(preprocContext, "theory-preprocess"){}; PreprocessingPassResult TheoryPreprocess::applyInternal( - AssertionPipeline* assertionsToPreprocess) + AssertionPipeline* assertions) { - TheoryEngine* te = d_preprocContext->getTheoryEngine(); - for (size_t i = 0, size = assertionsToPreprocess->size(); i < size; ++i) + d_preprocContext->spendResource(ResourceManager::Resource::PreprocessStep); + + IteSkolemMap& imap = assertions->getIteSkolemMap(); + PropEngine* propEngine = d_preprocContext->getPropEngine(); + // Remove all of the ITE occurrences and normalize + for (unsigned i = 0, size = assertions->size(); i < size; ++i) { - TNode a = (*assertionsToPreprocess)[i]; - Assert(Rewriter::rewrite(a) == a); - assertionsToPreprocess->replaceTrusted(i, te->preprocess(a)); - a = (*assertionsToPreprocess)[i]; - Assert(Rewriter::rewrite(a) == a); + Node assertion = (*assertions)[i]; + std::vector<theory::TrustNode> newAsserts; + std::vector<Node> newSkolems; + TrustNode trn = + propEngine->preprocess(assertion, newAsserts, newSkolems, true); + if (!trn.isNull()) + { + // process + assertions->replaceTrusted(i, trn); + // rewritten assertion has a dependence on the node (old pf architecture) + if (options::unsatCores()) + { + ProofManager::currentPM()->addDependence(trn.getNode(), assertion); + } + } + Assert(newSkolems.size() == newAsserts.size()); + for (unsigned j = 0, nnasserts = newAsserts.size(); j < nnasserts; j++) + { + imap[newSkolems[j]] = assertions->size(); + assertions->pushBackTrusted(newAsserts[j]); + // new assertions have a dependence on the node (old pf architecture) + if (options::unsatCores()) + { + ProofManager::currentPM()->addDependence(newAsserts[j].getProven(), + assertion); + } + } } + return PreprocessingPassResult::NO_CONFLICT; } 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<theory::TrustNode>& newLemmas, + std::vector<Node>& 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<theory::TrustNode> ppLemmas; + std::vector<Node> 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<theory::TrustNode>& ppLemmas, - std::vector<Node>& 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<Node> assertions; - assertions.push_back(lem.getProven()); + assertions.push_back(tplemma.getProven()); std::vector<Node> 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<Node> 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<TNode>& outputVariables) const d_cnfStream->getBooleanVariables(outputVariables); } -void PropEngine::ensureLiteral(TNode n) { d_cnfStream->ensureLiteral(n); } +Node PropEngine::ensureLiteral(TNode n) +{ + // must preprocess + std::vector<theory::TrustNode> newLemmas; + std::vector<Node> 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() { diff --git a/src/prop/prop_engine.h b/src/prop/prop_engine.h index 55a42c2a7..ac2b35ad6 100644 --- a/src/prop/prop_engine.h +++ b/src/prop/prop_engine.h @@ -95,6 +95,23 @@ class PropEngine void shutdown() {} /** + * Preprocess the given node. Return the REWRITE trust node corresponding to + * rewriting node. New lemmas and skolems are added to ppLemmas and + * ppSkolems respectively. + * + * @param node The assertion to preprocess, + * @param ppLemmas The lemmas to add to the set of assertions, + * @param ppSkolems The skolems that newLemmas correspond to, + * @param doTheoryPreprocess whether to run theory-specific preprocessing. + * @return The (REWRITE) trust node corresponding to rewritten node via + * preprocessing. + */ + theory::TrustNode preprocess(TNode node, + std::vector<theory::TrustNode>& ppLemmas, + std::vector<Node>& ppSkolems, + bool doTheoryPreprocess); + + /** * Notify preprocessed assertions. This method is called just before the * assertions are asserted to this prop engine. This method notifies the * decision engine and the theory engine of the assertions in ap. @@ -114,27 +131,10 @@ class PropEngine * than the (SAT and SMT) level at which it was asserted. * * @param trn the trust node storing the formula to assert - * @param removable whether this lemma can be quietly removed based - * on an activity heuristic + * @param p the properties of the lemma + * @return the (preprocessed) lemma */ - void assertLemma(theory::TrustNode trn, bool removable); - - /** - * Assert lemma trn with preprocessing lemmas ppLemmas which correspond - * to lemmas for skolems in ppSkolems. - * - * @param trn the trust node storing the formula to assert - * @param ppLemmas the lemmas from preprocessing and term formula removal on - * the proven node of trn - * @param ppSkolem the skolem that each lemma in ppLemma constrains. It should - * be the case that ppLemmas.size()==ppSkolems.size(). - * @param removable whether this lemma can be quietly removed based - * on an activity heuristic - */ - void assertLemmas(theory::TrustNode trn, - std::vector<theory::TrustNode>& ppLemmas, - std::vector<Node>& ppSkolems, - bool removable); + Node assertLemma(theory::TrustNode tlemma, theory::LemmaProperty p); /** * If ever n is decided upon, it must be in the given phase. This @@ -185,10 +185,11 @@ class PropEngine /** * Ensure that the given node will have a designated SAT literal - * that is definitionally equal to it. The result of this function - * is that the Node can be queried via getSatValue(). + * that is definitionally equal to it. Note that theory preprocessing is + * applied to n. The node returned by this method can be subsequently queried + * via getSatValue(). */ - void ensureLiteral(TNode n); + Node ensureLiteral(TNode n); /** * Push the context level. @@ -261,6 +262,18 @@ class PropEngine private: /** Dump out the satisfying assignment (after SAT result) */ void printSatisfyingAssignment(); + + /** + * Converts the given formula to CNF and asserts the CNF to the SAT solver. + * The formula can be removed by the SAT solver after backtracking lower + * than the (SAT and SMT) level at which it was asserted. + * + * @param trn the trust node storing the formula to assert + * @param removable whether this lemma can be quietly removed based + * on an activity heuristic + */ + void assertLemmaInternal(theory::TrustNode trn, bool removable); + /** * Indicates that the SAT solver is currently solving something and we should * not mess with it's internal state. diff --git a/src/prop/theory_proxy.cpp b/src/prop/theory_proxy.cpp index 1b9e78d80..23405675a 100644 --- a/src/prop/theory_proxy.cpp +++ b/src/prop/theory_proxy.cpp @@ -19,15 +19,14 @@ #include "context/context.h" #include "decision/decision_engine.h" #include "options/decision_options.h" +#include "proof/cnf_proof.h" #include "prop/cnf_stream.h" #include "prop/prop_engine.h" -#include "proof/cnf_proof.h" #include "smt/smt_statistics_registry.h" #include "theory/rewriter.h" #include "theory/theory_engine.h" #include "util/statistics_registry.h" - namespace CVC4 { namespace prop { @@ -35,12 +34,15 @@ TheoryProxy::TheoryProxy(PropEngine* propEngine, TheoryEngine* theoryEngine, DecisionEngine* decisionEngine, context::Context* context, - CnfStream* cnfStream) + context::UserContext* userContext, + CnfStream* cnfStream, + ProofNodeManager* pnm) : d_propEngine(propEngine), d_cnfStream(cnfStream), d_decisionEngine(decisionEngine), d_theoryEngine(theoryEngine), - d_queue(context) + d_queue(context), + d_tpp(*theoryEngine, userContext, pnm) { } @@ -165,5 +167,25 @@ SatValue TheoryProxy::getDecisionPolarity(SatVariable var) { CnfStream* TheoryProxy::getCnfStream() { return d_cnfStream; } +theory::TrustNode TheoryProxy::preprocessLemma( + theory::TrustNode trn, + std::vector<theory::TrustNode>& newLemmas, + std::vector<Node>& newSkolems, + bool doTheoryPreprocess) +{ + return d_tpp.preprocessLemma(trn, newLemmas, newSkolems, doTheoryPreprocess); +} + +theory::TrustNode TheoryProxy::preprocess( + TNode node, + std::vector<theory::TrustNode>& newLemmas, + std::vector<Node>& newSkolems, + bool doTheoryPreprocess) +{ + theory::TrustNode pnode = + d_tpp.preprocess(node, newLemmas, newSkolems, doTheoryPreprocess); + return pnode; +} + }/* CVC4::prop namespace */ }/* CVC4 namespace */ diff --git a/src/prop/theory_proxy.h b/src/prop/theory_proxy.h index e16728d0d..4d460434d 100644 --- a/src/prop/theory_proxy.h +++ b/src/prop/theory_proxy.h @@ -26,10 +26,13 @@ #include <iosfwd> #include <unordered_set> +#include "context/cdhashmap.h" #include "context/cdqueue.h" #include "expr/node.h" #include "prop/sat_solver.h" #include "theory/theory.h" +#include "theory/theory_preprocessor.h" +#include "theory/trust_node.h" #include "util/resource_manager.h" #include "util/statistics_registry.h" @@ -53,7 +56,9 @@ class TheoryProxy TheoryEngine* theoryEngine, DecisionEngine* decisionEngine, context::Context* context, - CnfStream* cnfStream); + context::UserContext* userContext, + CnfStream* cnfStream, + ProofNodeManager* pnm); ~TheoryProxy(); @@ -90,6 +95,23 @@ class TheoryProxy CnfStream* getCnfStream(); + /** + * Call the preprocessor on node, return trust node corresponding to the + * rewrite. + */ + theory::TrustNode preprocessLemma(theory::TrustNode trn, + std::vector<theory::TrustNode>& newLemmas, + std::vector<Node>& newSkolems, + bool doTheoryPreprocess); + /** + * Call the preprocessor on node, return trust node corresponding to the + * rewrite. + */ + theory::TrustNode preprocess(TNode node, + std::vector<theory::TrustNode>& newLemmas, + std::vector<Node>& newSkolems, + bool doTheoryPreprocess); + private: /** The prop engine we are using. */ PropEngine* d_propEngine; @@ -111,6 +133,9 @@ class TheoryProxy * all imported and exported lemmas. */ std::unordered_set<Node, NodeHashFunction> d_shared; + + /** The theory preprocessor */ + theory::TheoryPreprocessor d_tpp; }; /* class TheoryProxy */ }/* CVC4::prop namespace */ diff --git a/src/smt/process_assertions.cpp b/src/smt/process_assertions.cpp index 77c7d450e..8b9b0a53c 100644 --- a/src/smt/process_assertions.cpp +++ b/src/smt/process_assertions.cpp @@ -328,13 +328,8 @@ bool ProcessAssertions::apply(Assertions& as) // ensure rewritten d_passes["rewrite"]->apply(&assertions); - // apply theory preprocess + // apply theory preprocess, which includes ITE removal d_passes["theory-preprocess"]->apply(&assertions); - // Must remove ITEs again since theory preprocessing may introduce them. - // Notice that we alternatively could ensure that the theory-preprocess - // pass above calls TheoryPreprocess::preprocess instead of - // TheoryPreprocess::theoryPreprocess, as the former also does ITE removal. - d_passes["ite-removal"]->apply(&assertions); // This is needed because when solving incrementally, removeITEs may // introduce skolems that were solved for earlier and thus appear in the // substitution map. diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index ecb15fbe9..941d900d3 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -249,7 +249,6 @@ TheoryEngine::TheoryEngine(context::Context* context, d_propagatedLiterals(context), d_propagatedLiteralsIndex(context, 0), d_atomRequests(context), - d_tpp(*this, userContext, d_pnm), d_combineTheoriesTime("TheoryEngine::combineTheoriesTime"), d_true(), d_false(), @@ -853,11 +852,6 @@ theory::Theory::PPAssertStatus TheoryEngine::solve( return solveStatus; } -TrustNode TheoryEngine::preprocess(TNode assertion) -{ - return d_tpp.theoryPreprocess(assertion); -} - void TheoryEngine::notifyPreprocessedAssertions( const std::vector<Node>& assertions) { // call all the theories @@ -1171,21 +1165,7 @@ Node TheoryEngine::getModelValue(TNode var) { Node TheoryEngine::ensureLiteral(TNode n) { Trace("ensureLiteral") << "ensureLiteral rewriting: " << n << std::endl; Node rewritten = Rewriter::rewrite(n); - Trace("ensureLiteral") << " got: " << rewritten << std::endl; - std::vector<TrustNode> newLemmas; - std::vector<Node> newSkolems; - TrustNode tpn = d_tpp.preprocess(n, newLemmas, newSkolems, true); - // send lemmas corresponding to the skolems introduced by preprocessing n - for (const TrustNode& tnl : newLemmas) - { - Trace("ensureLiteral") << " lemma: " << tnl.getNode() << std::endl; - lemma(tnl, LemmaProperty::NONE); - } - Node preprocessed = tpn.isNull() ? rewritten : tpn.getNode(); - Trace("ensureLiteral") << "ensureLiteral preprocessed: " << preprocessed - << std::endl; - d_propEngine->ensureLiteral(preprocessed); - return preprocessed; + return d_propEngine->ensureLiteral(rewritten); } @@ -1440,75 +1420,20 @@ theory::LemmaStatus TheoryEngine::lemma(theory::TrustNode tlemma, printer.toStreamCmdComment(out, "theory lemma: expect valid"); printer.toStreamCmdCheckSat(out, n); } - bool removable = isLemmaPropertyRemovable(p); - bool preprocess = isLemmaPropertyPreprocess(p); - - // ensure closed - tlemma.debugCheckClosed("te-proof-debug", "TheoryEngine::lemma_initial"); - - // call preprocessor - std::vector<TrustNode> newLemmas; - std::vector<Node> newSkolems; - TrustNode tplemma = - d_tpp.preprocessLemma(tlemma, newLemmas, newSkolems, preprocess); - Assert(newSkolems.size() == newLemmas.size()); + Node retLemma = d_propEngine->assertLemma(tlemma, p); // If specified, we must add this lemma to the set of those that need to be // justified, where note we pass all auxiliary lemmas in lemmas, since these // by extension must be justified as well. if (d_relManager != nullptr && isLemmaPropertyNeedsJustify(p)) { - d_relManager->notifyPreprocessedAssertion(tplemma.getProven()); - for (const theory::TrustNode& tnl : newLemmas) - { - d_relManager->notifyPreprocessedAssertion(tnl.getProven()); - } - } - - // do final checks on the lemmas we are about to send - if (isProofEnabled()) - { - 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 = newLemmas.size(); i < lsize; ++i) - { - Assert(newLemmas[i].getGenerator() != nullptr); - newLemmas[i].debugCheckClosed("te-proof-debug", - "TheoryEngine::lemma_new"); - } - } - - if (Trace.isOn("te-lemma")) - { - Trace("te-lemma") << "Lemma, output: " << tplemma.getProven() << std::endl; - for (size_t i = 0, lsize = newLemmas.size(); i < lsize; ++i) - { - Trace("te-lemma") << "Lemma, new lemma: " << newLemmas[i].getProven() - << " (skolem is " << newSkolems[i] << ")" << std::endl; - } + d_relManager->notifyPreprocessedAssertion(retLemma); } - // now, send the lemmas to the prop engine - d_propEngine->assertLemmas(tplemma, newLemmas, newSkolems, removable); - // Mark that we added some lemmas d_lemmasAdded = true; - // Lemma analysis isn't online yet; this lemma may only live for this - // user level. - Node retLemma = tplemma.getNode(); - if (!newLemmas.empty()) - { - std::vector<Node> lemmas{retLemma}; - for (const theory::TrustNode& tnl : newLemmas) - { - lemmas.push_back(tnl.getProven()); - } - // the returned lemma is the conjunction of all additional lemmas. - retLemma = NodeManager::currentNM()->mkNode(kind::AND, lemmas); - } return theory::LemmaStatus(retLemma, d_userContext->getLevel()); } diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index bdc79931f..bade5a206 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -290,9 +290,6 @@ class TheoryEngine { /** sort inference module */ SortInference d_sortInfer; - /** The theory preprocessor */ - theory::TheoryPreprocessor d_tpp; - /** Time spent in theory combination */ TimerStat d_combineTheoriesTime; @@ -442,14 +439,6 @@ class TheoryEngine { bool isProofEnabled() const; public: - /** - * Runs theory specific preprocessing on the non-Boolean parts of - * the formula. This is only called on input assertions, after ITEs - * have been removed. - */ - theory::TrustNode preprocess(TNode node); - /** Get the theory preprocessor TODO (project #42) remove this */ - theory::TheoryPreprocessor* getTheoryPreprocess() { return &d_tpp; } /** Notify (preprocessed) assertions. */ void notifyPreprocessedAssertions(const std::vector<Node>& assertions); diff --git a/src/theory/theory_preprocessor.h b/src/theory/theory_preprocessor.h index 349e7917e..8bda3f5aa 100644 --- a/src/theory/theory_preprocessor.h +++ b/src/theory/theory_preprocessor.h @@ -72,7 +72,7 @@ class TheoryPreprocessor bool doTheoryPreprocess); /** * Same as above, but transforms the proof of node into a proof of the - * preprocessed node. + * preprocessed node and returns the LEMMA trust node. * * @param node The assertion to preprocess, * @param newLemmas The lemmas to add to the set of assertions, @@ -85,14 +85,13 @@ class TheoryPreprocessor std::vector<TrustNode>& newLemmas, std::vector<Node>& newSkolems, bool doTheoryPreprocess); + + private: /** - * Runs theory specific preprocessing on the non-Boolean parts of - * the formula. This is only called on input assertions, after ITEs - * have been removed. + * Runs theory specific preprocessing (Theory::ppRewrite) on the non-Boolean + * parts of the node. */ TrustNode theoryPreprocess(TNode node); - - private: /** Reference to owning theory engine */ TheoryEngine& d_engine; /** Logic info of theory engine */ |