diff options
Diffstat (limited to 'src/preprocessing/assertion_pipeline.cpp')
| -rw-r--r-- | src/preprocessing/assertion_pipeline.cpp | 92 |
1 files changed, 64 insertions, 28 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 |