From 3a3735d58ddac7ecfac80dad35da963901f15f55 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Wed, 16 Dec 2020 09:03:45 -0600 Subject: [PATCH] Move ownership of term formula removal to theory preprocessor (#5670) This is work towards refactoring ITE removal (more generally, term formula removal) so that it happens at a configurable time, preferably post-CNF conversion. This moves the TermFormulaRemover to the TheoryPreprocessor and changes several interfaces as a consequence of this move. The next step will move the TheoryPreprocessor inside prop::TheoryProxy. There are no behavior changes to solving in this PR. One aspect of CheckModels is simplified. --- src/preprocessing/passes/ite_removal.cpp | 27 ++++++-- .../preprocessing_pass_context.cpp | 2 - .../preprocessing_pass_context.h | 5 -- src/smt/check_models.cpp | 5 +- src/smt/preprocessor.cpp | 13 +--- src/smt/preprocessor.h | 14 +---- src/smt/smt_solver.cpp | 1 - src/smt/term_formula_removal.cpp | 61 ++++++------------- src/smt/term_formula_removal.h | 12 +--- src/theory/theory_engine.cpp | 3 +- src/theory/theory_engine.h | 8 +-- src/theory/theory_preprocessor.cpp | 5 +- src/theory/theory_preprocessor.h | 4 +- 13 files changed, 54 insertions(+), 106 deletions(-) diff --git a/src/preprocessing/passes/ite_removal.cpp b/src/preprocessing/passes/ite_removal.cpp index a75b6f5ad..3531497e8 100644 --- a/src/preprocessing/passes/ite_removal.cpp +++ b/src/preprocessing/passes/ite_removal.cpp @@ -18,6 +18,7 @@ #include "preprocessing/passes/ite_removal.h" #include "theory/rewriter.h" +#include "theory/theory_preprocessor.h" namespace CVC4 { namespace preprocessing { @@ -25,6 +26,7 @@ namespace passes { using namespace CVC4::theory; +// TODO (project #42): note this preprocessing pass is deprecated IteRemoval::IteRemoval(PreprocessingPassContext* preprocContext) : PreprocessingPass(preprocContext, "ite-removal") { @@ -36,19 +38,36 @@ PreprocessingPassResult IteRemoval::applyInternal(AssertionPipeline* assertions) IteSkolemMap& imap = assertions->getIteSkolemMap(); // Remove all of the ITE occurrences and normalize + theory::TheoryPreprocessor* tpp = + d_preprocContext->getTheoryEngine()->getTheoryPreprocess(); for (unsigned i = 0, size = assertions->size(); i < size; ++i) { + Node assertion = (*assertions)[i]; std::vector newAsserts; std::vector newSkolems; - TrustNode trn = d_preprocContext->getIteRemover()->run( - (*assertions)[i], newAsserts, newSkolems, true); - // process - assertions->replaceTrusted(i, trn); + // TODO (project #42): this will call the prop engine + TrustNode trn = tpp->preprocess(assertion, newAsserts, newSkolems, false); + 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); + } } } for (unsigned i = 0, size = assertions->size(); i < size; ++i) diff --git a/src/preprocessing/preprocessing_pass_context.cpp b/src/preprocessing/preprocessing_pass_context.cpp index ff4a0e6ca..707d1314c 100644 --- a/src/preprocessing/preprocessing_pass_context.cpp +++ b/src/preprocessing/preprocessing_pass_context.cpp @@ -23,12 +23,10 @@ namespace preprocessing { PreprocessingPassContext::PreprocessingPassContext( SmtEngine* smt, - RemoveTermFormulas* iteRemover, theory::booleans::CircuitPropagator* circuitPropagator, ProofNodeManager* pnm) : d_smt(smt), d_resourceManager(smt->getResourceManager()), - d_iteRemover(iteRemover), d_topLevelSubstitutions(smt->getUserContext(), pnm), d_circuitPropagator(circuitPropagator), d_pnm(pnm), diff --git a/src/preprocessing/preprocessing_pass_context.h b/src/preprocessing/preprocessing_pass_context.h index 824197bc5..c22a69255 100644 --- a/src/preprocessing/preprocessing_pass_context.h +++ b/src/preprocessing/preprocessing_pass_context.h @@ -40,7 +40,6 @@ class PreprocessingPassContext public: PreprocessingPassContext( SmtEngine* smt, - RemoveTermFormulas* iteRemover, theory::booleans::CircuitPropagator* circuitPropagator, ProofNodeManager* pnm); @@ -49,7 +48,6 @@ class PreprocessingPassContext prop::PropEngine* getPropEngine() { return d_smt->getPropEngine(); } context::Context* getUserContext() { return d_smt->getUserContext(); } context::Context* getDecisionContext() { return d_smt->getContext(); } - RemoveTermFormulas* getIteRemover() { return d_iteRemover; } theory::booleans::CircuitPropagator* getCircuitPropagator() { @@ -95,9 +93,6 @@ class PreprocessingPassContext /** Pointer to the ResourceManager for this context. */ ResourceManager* d_resourceManager; - /** Instance of the ITE remover */ - RemoveTermFormulas* d_iteRemover; - /* The top level substitutions */ theory::TrustSubstitutionMap d_topLevelSubstitutions; diff --git a/src/smt/check_models.cpp b/src/smt/check_models.cpp index a41c750ec..2338ebd61 100644 --- a/src/smt/check_models.cpp +++ b/src/smt/check_models.cpp @@ -184,9 +184,8 @@ void CheckModels::checkModel(Model* m, n = m->getValue(n); Notice() << "SmtEngine::checkModel(): -- get value : " << n << std::endl; - // Simplify the result and replace the already-known ITEs (this is important - // for ground ITEs under quantifiers). - n = pp->simplify(n, true); + // Simplify the result + n = pp->simplify(n); Notice() << "SmtEngine::checkModel(): -- simplifies with ite replacement to " << n << std::endl; diff --git a/src/smt/preprocessor.cpp b/src/smt/preprocessor.cpp index c2b8f73f1..ec7751a54 100644 --- a/src/smt/preprocessor.cpp +++ b/src/smt/preprocessor.cpp @@ -38,7 +38,6 @@ Preprocessor::Preprocessor(SmtEngine& smt, d_assertionsProcessed(u, false), d_exDefs(smt, *smt.getResourceManager(), stats), d_processor(smt, d_exDefs, *smt.getResourceManager(), stats), - d_rtf(u), d_pnm(nullptr) { } @@ -55,7 +54,7 @@ Preprocessor::~Preprocessor() void Preprocessor::finishInit() { d_ppContext.reset(new preprocessing::PreprocessingPassContext( - &d_smt, &d_rtf, &d_propagator, d_pnm)); + &d_smt, &d_propagator, d_pnm)); // initialize the preprocessing passes d_processor.finishInit(d_ppContext.get()); @@ -104,8 +103,6 @@ void Preprocessor::clearLearnedLiterals() void Preprocessor::cleanup() { d_processor.cleanup(); } -RemoveTermFormulas& Preprocessor::getTermFormulaRemover() { return d_rtf; } - Node Preprocessor::expandDefinitions(const Node& n, bool expandOnly) { std::unordered_map cache; @@ -129,7 +126,7 @@ Node Preprocessor::expandDefinitions( return d_exDefs.expandDefinitions(n, cache, expandOnly); } -Node Preprocessor::simplify(const Node& node, bool removeItes) +Node Preprocessor::simplify(const Node& node) { Trace("smt") << "SMT simplify(" << node << ")" << endl; if (Dump.isOn("benchmark")) @@ -147,11 +144,6 @@ Node Preprocessor::simplify(const Node& node, bool removeItes) Node n = d_exDefs.expandDefinitions(nas, cache); TrustNode ts = d_ppContext->getTopLevelSubstitutions().apply(n); Node ns = ts.isNull() ? n : ts.getNode(); - if (removeItes) - { - // also remove ites if asked - ns = d_rtf.replace(ns); - } return ns; } @@ -161,7 +153,6 @@ void Preprocessor::setProofGenerator(PreprocessProofGenerator* pppg) d_pnm = pppg->getManager(); d_exDefs.setProofNodeManager(d_pnm); d_propagator.setProof(d_pnm, d_context, pppg); - d_rtf.setProofNodeManager(d_pnm); } } // namespace smt diff --git a/src/smt/preprocessor.h b/src/smt/preprocessor.h index 220a433fe..367490306 100644 --- a/src/smt/preprocessor.h +++ b/src/smt/preprocessor.h @@ -22,7 +22,6 @@ #include "preprocessing/preprocessing_pass_context.h" #include "smt/expand_definitions.h" #include "smt/process_assertions.h" -#include "smt/term_formula_removal.h" #include "theory/booleans/circuit_propagator.h" namespace CVC4 { @@ -79,11 +78,9 @@ class Preprocessor * has been constructed. It also involves theory normalization. * * @param n The node to simplify - * @param removeItes Whether to remove ITE (and other terms with formulas in - * term positions) from the result. * @return The simplified term. */ - Node simplify(const Node& n, bool removeItes = false); + Node simplify(const Node& n); /** * Expand the definitions in a term or formula n. No other * simplification or normalization is done. @@ -99,10 +96,6 @@ class Preprocessor const Node& n, std::unordered_map& cache, bool expandOnly = false); - /** - * Get the underlying term formula remover utility. - */ - RemoveTermFormulas& getTermFormulaRemover(); /** * Set proof node manager. Enables proofs in this preprocessor. @@ -133,11 +126,6 @@ class Preprocessor * passes. */ ProcessAssertions d_processor; - /** - * The term formula remover, responsible for eliminating formulas that occur - * in term contexts. - */ - RemoveTermFormulas d_rtf; /** Proof node manager */ ProofNodeManager* d_pnm; }; diff --git a/src/smt/smt_solver.cpp b/src/smt/smt_solver.cpp index e53401f79..3e8d0f147 100644 --- a/src/smt/smt_solver.cpp +++ b/src/smt/smt_solver.cpp @@ -50,7 +50,6 @@ void SmtSolver::finishInit(const LogicInfo& logicInfo) d_theoryEngine.reset(new TheoryEngine(d_smt.getContext(), d_smt.getUserContext(), d_rm, - d_pp.getTermFormulaRemover(), logicInfo, d_smt.getOutputManager(), d_pnm)); diff --git a/src/smt/term_formula_removal.cpp b/src/smt/term_formula_removal.cpp index f3e0d0bd6..60b850a31 100644 --- a/src/smt/term_formula_removal.cpp +++ b/src/smt/term_formula_removal.cpp @@ -26,13 +26,23 @@ using namespace std; namespace CVC4 { -RemoveTermFormulas::RemoveTermFormulas(context::UserContext* u) - : d_tfCache(u), - d_skolem_cache(u), - d_pnm(nullptr), - d_tpg(nullptr), - d_lp(nullptr) +RemoveTermFormulas::RemoveTermFormulas(context::UserContext* u, + ProofNodeManager* pnm) + : d_tfCache(u), d_skolem_cache(u), d_pnm(pnm), d_tpg(nullptr), d_lp(nullptr) { + // enable proofs if necessary + if (d_pnm != nullptr) + { + d_tpg.reset( + new TConvProofGenerator(d_pnm, + nullptr, + TConvPolicy::FIXPOINT, + TConvCachePolicy::NEVER, + "RemoveTermFormulas::TConvProofGenerator", + &d_rtfc)); + d_lp.reset(new LazyCDProof( + d_pnm, nullptr, nullptr, "RemoveTermFormulas::LazyCDProof")); + } } RemoveTermFormulas::~RemoveTermFormulas() {} @@ -40,29 +50,9 @@ RemoveTermFormulas::~RemoveTermFormulas() {} theory::TrustNode RemoveTermFormulas::run( Node assertion, std::vector& newAsserts, - std::vector& newSkolems, - bool reportDeps) + std::vector& newSkolems) { Node itesRemoved = runInternal(assertion, newAsserts, newSkolems); - // In some calling contexts, not necessary to report dependence information. - if (reportDeps && options::unsatCores()) - { - // new assertions have a dependence on the node - if (options::unsatCores()) - { - ProofManager::currentPM()->addDependence(itesRemoved, assertion); - } - unsigned n = 0; - while (n < newAsserts.size()) - { - if (options::unsatCores()) - { - ProofManager::currentPM()->addDependence(newAsserts[n].getProven(), - assertion); - } - ++n; - } - } // The rewriting of assertion can be justified by the term conversion proof // generator d_tpg. return theory::TrustNode::mkTrustRewrite(assertion, itesRemoved, d_tpg.get()); @@ -536,23 +526,6 @@ Node RemoveTermFormulas::getAxiomFor(Node n) return Node::null(); } -void RemoveTermFormulas::setProofNodeManager(ProofNodeManager* pnm) -{ - if (d_tpg == nullptr) - { - d_pnm = pnm; - d_tpg.reset( - new TConvProofGenerator(d_pnm, - nullptr, - TConvPolicy::FIXPOINT, - TConvCachePolicy::NEVER, - "RemoveTermFormulas::TConvProofGenerator", - &d_rtfc)); - d_lp.reset(new LazyCDProof( - d_pnm, nullptr, nullptr, "RemoveTermFormulas::LazyCDProof")); - } -} - ProofGenerator* RemoveTermFormulas::getTConvProofGenerator() { return d_tpg.get(); diff --git a/src/smt/term_formula_removal.h b/src/smt/term_formula_removal.h index 25dcd0295..fc10e19c9 100644 --- a/src/smt/term_formula_removal.h +++ b/src/smt/term_formula_removal.h @@ -38,7 +38,7 @@ typedef std::unordered_map IteSkolemMap; class RemoveTermFormulas { public: - RemoveTermFormulas(context::UserContext* u); + RemoveTermFormulas(context::UserContext* u, ProofNodeManager* pnm = nullptr); ~RemoveTermFormulas(); /** @@ -83,15 +83,13 @@ class RemoveTermFormulas { * @param newAsserts The new assertions corresponding to axioms for newly * introduced skolems. * @param newSkolems The skolems corresponding to each of the newAsserts. - * @param reportDeps Used for unsat cores in the old proof infrastructure. * @return a trust node of kind TrustNodeKind::REWRITE whose * right hand side is assertion after removing term formulas, and the proof * generator (if provided) that can prove the equivalence. */ theory::TrustNode run(Node assertion, std::vector& newAsserts, - std::vector& newSkolems, - bool reportDeps = false); + std::vector& newSkolems); /** * Substitute under node using pre-existing cache. Do not remove @@ -105,12 +103,6 @@ class RemoveTermFormulas { /** Garbage collects non-context dependent data-structures. */ void garbageCollect(); - /** - * Set proof node manager, which signals this class to enable proofs using the - * given proof node manager. - */ - void setProofNodeManager(ProofNodeManager* pnm); - /** * Get proof generator that is responsible for all proofs for removing term * formulas from nodes. When proofs are enabled, the returned trust node diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index 7b38bd844..ecb15fbe9 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -218,7 +218,6 @@ ProofNodeManager* TheoryEngine::getProofNodeManager() const { return d_pnm; } TheoryEngine::TheoryEngine(context::Context* context, context::UserContext* userContext, ResourceManager* rm, - RemoveTermFormulas& iteRemover, const LogicInfo& logicInfo, OutputManager& outMgr, ProofNodeManager* pnm) @@ -250,7 +249,7 @@ TheoryEngine::TheoryEngine(context::Context* context, d_propagatedLiterals(context), d_propagatedLiteralsIndex(context, 0), d_atomRequests(context), - d_tpp(*this, iteRemover, userContext, d_pnm), + d_tpp(*this, userContext, d_pnm), d_combineTheoriesTime("TheoryEngine::combineTheoriesTime"), d_true(), d_false(), diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index 1412d7464..bdc79931f 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -95,13 +95,8 @@ class RelevanceManager; namespace eq { class EqualityEngine; } // namespace eq - -class EntailmentCheckParameters; -class EntailmentCheckSideEffects; }/* CVC4::theory namespace */ -class RemoveTermFormulas; - /** * This is essentially an abstraction for a collection of theories. A * TheoryEngine provides services to a PropEngine, making various @@ -313,7 +308,6 @@ class TheoryEngine { TheoryEngine(context::Context* context, context::UserContext* userContext, ResourceManager* rm, - RemoveTermFormulas& iteRemover, const LogicInfo& logic, OutputManager& outMgr, ProofNodeManager* pnm); @@ -454,6 +448,8 @@ class TheoryEngine { * 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& assertions); diff --git a/src/theory/theory_preprocessor.cpp b/src/theory/theory_preprocessor.cpp index ad9250a78..179ecc130 100644 --- a/src/theory/theory_preprocessor.cpp +++ b/src/theory/theory_preprocessor.cpp @@ -26,13 +26,12 @@ namespace CVC4 { namespace theory { TheoryPreprocessor::TheoryPreprocessor(TheoryEngine& engine, - RemoveTermFormulas& tfr, context::UserContext* userContext, ProofNodeManager* pnm) : d_engine(engine), d_logicInfo(engine.getLogicInfo()), d_ppCache(userContext), - d_tfr(tfr), + d_tfr(userContext, pnm), d_tpg(pnm ? new TConvProofGenerator( pnm, userContext, @@ -102,7 +101,7 @@ TrustNode TheoryPreprocessor::preprocess(TNode node, } // Remove the ITEs - TrustNode ttfr = d_tfr.run(ppNode, newLemmas, newSkolems, false); + TrustNode ttfr = d_tfr.run(ppNode, newLemmas, newSkolems); Node rtfNode = ttfr.getNode(); if (Debug.isOn("lemma-ites")) diff --git a/src/theory/theory_preprocessor.h b/src/theory/theory_preprocessor.h index 147c17f4a..349e7917e 100644 --- a/src/theory/theory_preprocessor.h +++ b/src/theory/theory_preprocessor.h @@ -25,6 +25,7 @@ #include "expr/node.h" #include "expr/tconv_seq_proof_generator.h" #include "expr/term_conversion_proof_generator.h" +#include "smt/term_formula_removal.h" #include "theory/trust_node.h" namespace CVC4 { @@ -45,7 +46,6 @@ class TheoryPreprocessor public: /** Constructs a theory preprocessor */ TheoryPreprocessor(TheoryEngine& engine, - RemoveTermFormulas& tfr, context::UserContext* userContext, ProofNodeManager* pnm = nullptr); /** Destroys a theory preprocessor */ @@ -100,7 +100,7 @@ class TheoryPreprocessor /** Cache for theory-preprocessing of assertions */ NodeMap d_ppCache; /** The term formula remover */ - RemoveTermFormulas& d_tfr; + RemoveTermFormulas d_tfr; /** The term context, which computes hash values for term contexts. */ InQuantTermContext d_iqtc; /** -- 2.30.2