From: Andrew Reynolds Date: Mon, 19 Oct 2020 16:06:16 +0000 (-0500) Subject: (proof-new) Update preprocessing pass context for proofs (#5298) X-Git-Tag: cvc5-1.0.0~2694 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=a8e839e29325f06ecd2d5dda7d8f64a44ddafb0c;p=cvc5.git (proof-new) Update preprocessing pass context for proofs (#5298) This sets up the preprocessing pass context in preparation for proof production. This PR makes the top level substitutions map into a TrustSubstitutionMap, the data structure that applies substitutions in a way that tracks proofs. This PR also makes the "apply subst" preprocessing pass proof producing. --- diff --git a/src/preprocessing/assertion_pipeline.cpp b/src/preprocessing/assertion_pipeline.cpp index cd92e5f3d..4529ad5e1 100644 --- a/src/preprocessing/assertion_pipeline.cpp +++ b/src/preprocessing/assertion_pipeline.cpp @@ -104,7 +104,12 @@ void AssertionPipeline::replace(size_t i, Node n, ProofGenerator* pgen) } void AssertionPipeline::replaceTrusted(size_t i, theory::TrustNode trn) -{ +{ + if (trn.isNull()) + { + // null trust node denotes no change, nothing to do + return; + } Assert(trn.getKind() == theory::TrustNodeKind::REWRITE); replace(i, trn.getNode(), trn.getGenerator()); } diff --git a/src/preprocessing/passes/apply_substs.cpp b/src/preprocessing/passes/apply_substs.cpp index 0ce3f20b2..06821ab56 100644 --- a/src/preprocessing/passes/apply_substs.cpp +++ b/src/preprocessing/passes/apply_substs.cpp @@ -41,7 +41,7 @@ PreprocessingPassResult ApplySubsts::applyInternal( // TODO(#1255): Substitutions in incremental mode should be managed with a // proper data structure. - theory::SubstitutionMap& substMap = + theory::TrustSubstitutionMap& tlsm = d_preprocContext->getTopLevelSubstitutions(); unsigned size = assertionsToPreprocess->size(); for (unsigned i = 0; i < size; ++i) @@ -54,9 +54,8 @@ PreprocessingPassResult ApplySubsts::applyInternal( << std::endl; d_preprocContext->spendResource( ResourceManager::Resource::PreprocessStep); - assertionsToPreprocess->replace(i, - theory::Rewriter::rewrite(substMap.apply( - (*assertionsToPreprocess)[i]))); + assertionsToPreprocess->replaceTrusted( + i, tlsm.apply((*assertionsToPreprocess)[i])); Trace("apply-substs") << " got " << (*assertionsToPreprocess)[i] << std::endl; } diff --git a/src/preprocessing/passes/miplib_trick.cpp b/src/preprocessing/passes/miplib_trick.cpp index 3d7fd120a..f55665bc5 100644 --- a/src/preprocessing/passes/miplib_trick.cpp +++ b/src/preprocessing/passes/miplib_trick.cpp @@ -189,8 +189,9 @@ PreprocessingPassResult MipLibTrick::applyInternal( propagator->getBackEdges(); unordered_set removeAssertions; - SubstitutionMap& top_level_substs = + theory::TrustSubstitutionMap& tlsm = d_preprocContext->getTopLevelSubstitutions(); + SubstitutionMap& top_level_substs = tlsm.get(); NodeManager* nm = NodeManager::currentNM(); Node zero = nm->mkConst(Rational(0)), one = nm->mkConst(Rational(1)); diff --git a/src/preprocessing/passes/non_clausal_simp.cpp b/src/preprocessing/passes/non_clausal_simp.cpp index 823e93f52..a3650c988 100644 --- a/src/preprocessing/passes/non_clausal_simp.cpp +++ b/src/preprocessing/passes/non_clausal_simp.cpp @@ -114,8 +114,8 @@ PreprocessingPassResult NonClausalSimp::applyInternal( << "Iterate through " << propagator->getLearnedLiterals().size() << " learned literals." << std::endl; // No conflict, go through the literals and solve them - SubstitutionMap& top_level_substs = - d_preprocContext->getTopLevelSubstitutions(); + TrustSubstitutionMap& ttls = d_preprocContext->getTopLevelSubstitutions(); + CVC4_UNUSED SubstitutionMap& top_level_substs = ttls.get(); SubstitutionMap constantPropagations(d_preprocContext->getUserContext()); TrustSubstitutionMap tnewSubstituions(d_preprocContext->getUserContext(), nullptr); diff --git a/src/preprocessing/preprocessing_pass_context.cpp b/src/preprocessing/preprocessing_pass_context.cpp index 65e26cabb..5893635cf 100644 --- a/src/preprocessing/preprocessing_pass_context.cpp +++ b/src/preprocessing/preprocessing_pass_context.cpp @@ -14,7 +14,7 @@ ** The preprocessing pass context for passes. **/ -#include "preprocessing_pass_context.h" +#include "preprocessing/preprocessing_pass_context.h" #include "expr/node_algorithm.h" @@ -24,12 +24,14 @@ namespace preprocessing { PreprocessingPassContext::PreprocessingPassContext( SmtEngine* smt, RemoveTermFormulas* iteRemover, - theory::booleans::CircuitPropagator* circuitPropagator) + theory::booleans::CircuitPropagator* circuitPropagator, + ProofNodeManager* pnm) : d_smt(smt), d_resourceManager(smt->getResourceManager()), d_iteRemover(iteRemover), - d_topLevelSubstitutions(smt->getUserContext()), + d_topLevelSubstitutions(smt->getUserContext(), pnm), d_circuitPropagator(circuitPropagator), + d_pnm(pnm), d_symsInAssertions(smt->getUserContext()) { } @@ -40,6 +42,12 @@ void PreprocessingPassContext::widenLogic(theory::TheoryId id) req.widenLogic(id); } +theory::TrustSubstitutionMap& +PreprocessingPassContext::getTopLevelSubstitutions() +{ + return d_topLevelSubstitutions; +} + void PreprocessingPassContext::enableIntegers() { LogicRequest req(*d_smt); @@ -61,5 +69,10 @@ void PreprocessingPassContext::recordSymbolsInAssertions( } } +ProofNodeManager* PreprocessingPassContext::getProofNodeManager() +{ + return d_pnm; +} + } // namespace preprocessing } // namespace CVC4 diff --git a/src/preprocessing/preprocessing_pass_context.h b/src/preprocessing/preprocessing_pass_context.h index f93c96fde..d0747b5d9 100644 --- a/src/preprocessing/preprocessing_pass_context.h +++ b/src/preprocessing/preprocessing_pass_context.h @@ -29,6 +29,7 @@ #include "smt/term_formula_removal.h" #include "theory/booleans/circuit_propagator.h" #include "theory/theory_engine.h" +#include "theory/trust_substitutions.h" #include "util/resource_manager.h" namespace CVC4 { @@ -40,7 +41,8 @@ class PreprocessingPassContext PreprocessingPassContext( SmtEngine* smt, RemoveTermFormulas* iteRemover, - theory::booleans::CircuitPropagator* circuitPropagator); + theory::booleans::CircuitPropagator* circuitPropagator, + ProofNodeManager* pnm); SmtEngine* getSmt() { return d_smt; } TheoryEngine* getTheoryEngine() { return d_smt->getTheoryEngine(); } @@ -70,10 +72,7 @@ class PreprocessingPassContext void widenLogic(theory::TheoryId id); /** Gets a reference to the top-level substitution map */ - theory::SubstitutionMap& getTopLevelSubstitutions() - { - return d_topLevelSubstitutions; - } + theory::TrustSubstitutionMap& getTopLevelSubstitutions(); /* Enable Integers. */ void enableIntegers(); @@ -85,6 +84,9 @@ class PreprocessingPassContext */ void recordSymbolsInAssertions(const std::vector& assertions); + /** The the proof node manager associated with this context, if it exists */ + ProofNodeManager* getProofNodeManager(); + private: /** Pointer to the SmtEngine that this context was created in. */ SmtEngine* d_smt; @@ -96,10 +98,12 @@ class PreprocessingPassContext RemoveTermFormulas* d_iteRemover; /* The top level substitutions */ - theory::SubstitutionMap d_topLevelSubstitutions; + theory::TrustSubstitutionMap d_topLevelSubstitutions; /** Instance of the circuit propagator */ theory::booleans::CircuitPropagator* d_circuitPropagator; + /** Pointer to the proof node manager, if it exists */ + ProofNodeManager* d_pnm; /** * The (user-context-dependent) set of symbols that occur in at least one diff --git a/src/smt/preprocessor.cpp b/src/smt/preprocessor.cpp index 02323561d..912c0ea28 100644 --- a/src/smt/preprocessor.cpp +++ b/src/smt/preprocessor.cpp @@ -30,12 +30,14 @@ namespace smt { Preprocessor::Preprocessor(SmtEngine& smt, context::UserContext* u, AbstractValues& abs) - : d_smt(smt), + : d_context(u), + d_smt(smt), d_absValues(abs), d_propagator(true, true), d_assertionsProcessed(u, false), d_processor(smt, *smt.getResourceManager()), - d_rtf(u) + d_rtf(u), + d_pnm(nullptr) { } @@ -51,7 +53,7 @@ Preprocessor::~Preprocessor() void Preprocessor::finishInit() { d_ppContext.reset(new preprocessing::PreprocessingPassContext( - &d_smt, &d_rtf, &d_propagator)); + &d_smt, &d_rtf, &d_propagator, d_pnm)); // initialize the preprocessing passes d_processor.finishInit(d_ppContext.get()); @@ -62,7 +64,8 @@ bool Preprocessor::process(Assertions& as) preprocessing::AssertionPipeline& ap = as.getAssertionPipeline(); // should not be called if empty - Assert(ap.size() != 0) << "Can only preprocess a non-empty list of assertions"; + Assert(ap.size() != 0) + << "Can only preprocess a non-empty list of assertions"; if (d_assertionsProcessed && options::incrementalSolving()) { @@ -140,7 +143,8 @@ Node Preprocessor::simplify(const Node& node, bool removeItes) } std::unordered_map cache; Node n = d_processor.expandDefinitions(nas, cache); - Node ns = applySubstitutions(n); + TrustNode ts = d_ppContext->getTopLevelSubstitutions().apply(n); + Node ns = ts.isNull() ? n : ts.getNode(); if (removeItes) { // also remove ites if asked @@ -149,9 +153,11 @@ Node Preprocessor::simplify(const Node& node, bool removeItes) return ns; } -Node Preprocessor::applySubstitutions(TNode node) +void Preprocessor::setProofGenerator(PreprocessProofGenerator* pppg) { - return Rewriter::rewrite(d_ppContext->getTopLevelSubstitutions().apply(node)); + Assert(pppg != nullptr); + d_pnm = pppg->getManager(); + d_rtf.setProofNodeManager(d_pnm); } } // namespace smt diff --git a/src/smt/preprocessor.h b/src/smt/preprocessor.h index 81757de37..b07e7ec97 100644 --- a/src/smt/preprocessor.h +++ b/src/smt/preprocessor.h @@ -100,12 +100,14 @@ class Preprocessor */ RemoveTermFormulas& getTermFormulaRemover(); - private: /** - * Apply substitutions that have been inferred by preprocessing, return the - * substituted form of node. + * Set proof node manager. Enables proofs in this preprocessor. */ - Node applySubstitutions(TNode node); + void setProofGenerator(PreprocessProofGenerator* pppg); + + private: + /** A copy of the current context */ + context::Context* d_context; /** Reference to the parent SmtEngine */ SmtEngine& d_smt; /** Reference to the abstract values utility */ @@ -130,6 +132,8 @@ class Preprocessor * in term contexts. */ RemoveTermFormulas d_rtf; + /** Proof node manager */ + ProofNodeManager* d_pnm; }; } // namespace smt diff --git a/src/smt/process_assertions.cpp b/src/smt/process_assertions.cpp index 719165048..f8af72c3a 100644 --- a/src/smt/process_assertions.cpp +++ b/src/smt/process_assertions.cpp @@ -105,9 +105,6 @@ bool ProcessAssertions::apply(Assertions& as) return true; } - SubstitutionMap& top_level_substs = - d_preprocessingPassContext->getTopLevelSubstitutions(); - if (options::bvGaussElim()) { d_passes["bv-gauss"]->apply(&assertions); @@ -330,6 +327,8 @@ bool ProcessAssertions::apply(Assertions& as) // First, find all skolems that appear in the substitution map - their // associated iteExpr will need to be moved to the main assertion set set skolemSet; + SubstitutionMap& top_level_substs = + d_preprocessingPassContext->getTopLevelSubstitutions().get(); SubstitutionMap::iterator pos = top_level_substs.begin(); for (; pos != top_level_substs.end(); ++pos) { diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 2a771ce76..2f9918486 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -259,14 +259,17 @@ void SmtEngine::finishInit() if (options::proofNew()) { d_pfManager.reset(new PfManager(getUserContext(), this)); + PreprocessProofGenerator* pppg = d_pfManager->getPreprocessProofGenerator(); // use this proof node manager pnm = d_pfManager->getProofNodeManager(); // enable proof support in the rewriter d_rewriter->setProofNodeManager(pnm); // enable it in the assertions pipeline - d_asserts->setProofGenerator(d_pfManager->getPreprocessProofGenerator()); + d_asserts->setProofGenerator(pppg); // enable it in the SmtSolver d_smtSolver->setProofNodeManager(pnm); + // enabled proofs in the preprocessor + d_pp->setProofGenerator(pppg); } Trace("smt-debug") << "SmtEngine::finishInit" << std::endl;