diff options
Diffstat (limited to 'src/preprocessing')
| -rw-r--r-- | src/preprocessing/assertion_pipeline.cpp | 92 | ||||
| -rw-r--r-- | src/preprocessing/assertion_pipeline.h | 41 |
2 files changed, 88 insertions, 45 deletions
diff --git a/src/preprocessing/assertion_pipeline.cpp b/src/preprocessing/assertion_pipeline.cpp index 99e22b28f..cd92e5f3d 100644 --- a/src/preprocessing/assertion_pipeline.cpp +++ b/src/preprocessing/assertion_pipeline.cpp @@ -18,6 +18,7 @@ #include "expr/node_manager.h" #include "options/smt_options.h" #include "proof/proof_manager.h" +#include "theory/builtin/proof_checker.h" #include "theory/rewriter.h" namespace CVC4 { @@ -61,10 +62,17 @@ void AssertionPipeline::push_back(Node n, Assert(d_assumptionsStart + d_numAssumptions == d_nodes.size() - 1); d_numAssumptions++; } - if (!isInput && isProofEnabled()) + if (isProofEnabled()) { - // notice this is always called, regardless of whether pgen is nullptr - d_pppg->notifyNewAssert(n, pgen); + if (!isInput) + { + // notice this is always called, regardless of whether pgen is nullptr + d_pppg->notifyNewAssert(n, pgen); + } + else + { + Trace("smt-pppg") << "...input assertion " << n << std::endl; + } } } @@ -77,6 +85,13 @@ void AssertionPipeline::pushBackTrusted(theory::TrustNode trn) void AssertionPipeline::replace(size_t i, Node n, ProofGenerator* pgen) { + if (n == d_nodes[i]) + { + // no change, skip + return; + } + Trace("smt-pppg-repl") << "Replace " << d_nodes[i] << " with " << n + << std::endl; if (options::unsatCores()) { ProofManager::currentPM()->addDependence(n, d_nodes[i]); @@ -94,26 +109,6 @@ void AssertionPipeline::replaceTrusted(size_t i, theory::TrustNode trn) replace(i, trn.getNode(), trn.getGenerator()); } -void AssertionPipeline::replace(size_t i, - Node n, - const std::vector<Node>& addnDeps, - ProofGenerator* pgen) -{ - if (options::unsatCores()) - { - ProofManager::currentPM()->addDependence(n, d_nodes[i]); - for (const auto& addnDep : addnDeps) - { - ProofManager::currentPM()->addDependence(n, addnDep); - } - } - if (isProofEnabled()) - { - d_pppg->notifyPreprocessed(d_nodes[i], n, pgen); - } - d_nodes[i] = n; -} - void AssertionPipeline::setProofGenerator(smt::PreprocessProofGenerator* pppg) { d_pppg = pppg; @@ -133,14 +128,55 @@ void AssertionPipeline::disableStoreSubstsInAsserts() d_storeSubstsInAsserts = false; } -void AssertionPipeline::addSubstitutionNode(Node n) +void AssertionPipeline::addSubstitutionNode(Node n, ProofGenerator* pg) { Assert(d_storeSubstsInAsserts); Assert(n.getKind() == kind::EQUAL); - d_nodes[d_substsIndex] = theory::Rewriter::rewrite( - NodeManager::currentNM()->mkNode(kind::AND, n, d_nodes[d_substsIndex])); - Assert(theory::Rewriter::rewrite(d_nodes[d_substsIndex]) - == d_nodes[d_substsIndex]); + conjoin(d_substsIndex, n, pg); +} + +void AssertionPipeline::conjoin(size_t i, Node n, ProofGenerator* pg) +{ + NodeManager* nm = NodeManager::currentNM(); + Node newConj = nm->mkNode(kind::AND, d_nodes[i], n); + Node newConjr = theory::Rewriter::rewrite(newConj); + if (newConjr == d_nodes[i]) + { + // trivial, skip + return; + } + if (isProofEnabled()) + { + // ---------- from pppg --------- from pg + // d_nodes[i] n + // -------------------------------- AND_INTRO + // d_nodes[i] ^ n + // -------------------------------- MACRO_SR_PRED_TRANSFORM + // rewrite( d_nodes[i] ^ n ) + // allocate a fresh proof which will act as the proof generator + LazyCDProof* lcp = d_pppg->allocateHelperProof(); + lcp->addLazyStep(d_nodes[i], d_pppg, false); + lcp->addLazyStep( + n, pg, false, "AssertionPipeline::conjoin", false, PfRule::PREPROCESS); + lcp->addStep(newConj, PfRule::AND_INTRO, {d_nodes[i], n}, {}); + if (newConjr != newConj) + { + lcp->addStep( + newConjr, PfRule::MACRO_SR_PRED_TRANSFORM, {newConj}, {newConjr}); + } + // Notice we have constructed a proof of a new assertion, where d_pppg + // is referenced in the lazy proof above. If alternatively we had + // constructed a proof of d_nodes[i] = rewrite( d_nodes[i] ^ n ), we would + // have used notifyPreprocessed. However, it is simpler to make the + // above proof. + d_pppg->notifyNewAssert(newConjr, lcp); + } + if (options::unsatCores()) + { + ProofManager::currentPM()->addDependence(newConjr, d_nodes[i]); + } + d_nodes[i] = newConjr; + Assert(theory::Rewriter::rewrite(newConjr) == newConjr); } } // namespace preprocessing diff --git a/src/preprocessing/assertion_pipeline.h b/src/preprocessing/assertion_pipeline.h index 63e2bdd2a..6ca430ac4 100644 --- a/src/preprocessing/assertion_pipeline.h +++ b/src/preprocessing/assertion_pipeline.h @@ -49,7 +49,9 @@ class AssertionPipeline */ void clear(); + /** TODO (projects #75): remove this */ Node& operator[](size_t i) { return d_nodes[i]; } + /** Get the assertion at index i */ const Node& operator[](size_t i) const { return d_nodes[i]; } /** @@ -70,7 +72,13 @@ class AssertionPipeline /** Same as above, with TrustNode */ void pushBackTrusted(theory::TrustNode trn); + /** TODO (projects #75): remove this */ std::vector<Node>& ref() { return d_nodes; } + + /** + * Get the constant reference to the underlying assertions. It is only + * possible to modify these via the replace methods below. + */ const std::vector<Node>& ref() const { return d_nodes; } std::vector<Node>::const_iterator begin() const { return d_nodes.cbegin(); } @@ -89,22 +97,6 @@ class AssertionPipeline /** Same as above, with TrustNode */ void replaceTrusted(size_t i, theory::TrustNode trn); - /* - * Replaces assertion i with node n and records that this replacement depends - * on assertion i and the nodes listed in addnDeps. The dependency - * information is used for unsat cores and proofs. - * - * @param i The position of the assertion to replace. - * @param n The replacement assertion. - * @param addnDeps The dependencies. - * @param pg The proof generator who can provide a proof of d_nodes[i] == n, - * where d_nodes[i] is the assertion at position i prior to this call. - */ - void replace(size_t i, - Node n, - const std::vector<Node>& addnDeps, - ProofGenerator* pg = nullptr); - IteSkolemMap& getIteSkolemMap() { return d_iteSkolemMap; } const IteSkolemMap& getIteSkolemMap() const { return d_iteSkolemMap; } @@ -136,8 +128,23 @@ class AssertionPipeline /** * Adds a substitution node of the form (= lhs rhs) to the assertions. + * This conjoins n to assertions at a distinguished index given by + * d_substsIndex. + * + * @param n The substitution node + * @param pg The proof generator that can provide a proof of n. + */ + void addSubstitutionNode(Node n, ProofGenerator* pgen = nullptr); + + /** + * Conjoin n to the assertion vector at position i. This replaces + * d_nodes[i] with the rewritten form of (AND d_nodes[i] n). + * + * @param i The assertion to replace + * @param n The formula to conjoin at position i + * @param pg The proof generator that can provide a proof of n */ - void addSubstitutionNode(Node n); + void conjoin(size_t i, Node n, ProofGenerator* pg = nullptr); /** * Checks whether the assertion at a given index represents substitutions. |