diff options
| -rw-r--r-- | src/preprocessing/assertion_pipeline.cpp | 54 | ||||
| -rw-r--r-- | src/preprocessing/assertion_pipeline.h | 50 |
2 files changed, 80 insertions, 24 deletions
diff --git a/src/preprocessing/assertion_pipeline.cpp b/src/preprocessing/assertion_pipeline.cpp index caad369b7..a6b9531b6 100644 --- a/src/preprocessing/assertion_pipeline.cpp +++ b/src/preprocessing/assertion_pipeline.cpp @@ -28,7 +28,8 @@ AssertionPipeline::AssertionPipeline() d_storeSubstsInAsserts(false), d_substsIndex(0), d_assumptionsStart(0), - d_numAssumptions(0) + d_numAssumptions(0), + d_pppg(nullptr) { } @@ -40,11 +41,15 @@ void AssertionPipeline::clear() d_numAssumptions = 0; } -void AssertionPipeline::push_back(Node n, bool isAssumption) +void AssertionPipeline::push_back(Node n, + bool isAssumption, + bool isInput, + ProofGenerator* pgen) { d_nodes.push_back(n); if (isAssumption) { + Assert(pgen == nullptr); if (d_numAssumptions == 0) { d_assumptionsStart = d_nodes.size() - 1; @@ -56,39 +61,60 @@ void AssertionPipeline::push_back(Node n, bool isAssumption) Assert(d_assumptionsStart + d_numAssumptions == d_nodes.size() - 1); d_numAssumptions++; } + if (!isInput && isProofEnabled()) + { + // notice this is always called, regardless of whether pgen is nullptr + d_pppg->notifyNewAssert(n, pgen); + } +} + +void AssertionPipeline::pushBackTrusted(theory::TrustNode trn) +{ + Assert(trn.getKind() == theory::TrustNodeKind::LEMMA); + // push back what was proven + push_back(trn.getProven(), false, trn.getGenerator()); } -void AssertionPipeline::replace(size_t i, Node n) +void AssertionPipeline::replace(size_t i, Node n, ProofGenerator* pgen) { PROOF(ProofManager::currentPM()->addDependence(n, d_nodes[i]);); + if (isProofEnabled()) + { + d_pppg->notifyPreprocessed(d_nodes[i], n, pgen); + } d_nodes[i] = n; } +void AssertionPipeline::replaceTrusted(size_t i, theory::TrustNode trn) +{ + Assert(trn.getKind() == theory::TrustNodeKind::REWRITE); + replace(i, trn.getNode(), trn.getGenerator()); +} + void AssertionPipeline::replace(size_t i, Node n, - const std::vector<Node>& addnDeps) + const std::vector<Node>& addnDeps, + ProofGenerator* pgen) { PROOF(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::replace(size_t i, const std::vector<Node>& ns) +void AssertionPipeline::setProofGenerator(smt::PreprocessProofGenerator* pppg) { - PROOF( - for (const auto& n - : ns) { ProofManager::currentPM()->addDependence(n, d_nodes[i]); }); - d_nodes[i] = NodeManager::currentNM()->mkConst<bool>(true); - - for (const auto& n : ns) - { - d_nodes.push_back(n); - } + d_pppg = pppg; } +bool AssertionPipeline::isProofEnabled() const { return d_pppg != nullptr; } + void AssertionPipeline::enableStoreSubstsInAsserts() { d_storeSubstsInAsserts = true; diff --git a/src/preprocessing/assertion_pipeline.h b/src/preprocessing/assertion_pipeline.h index 5d8f64594..4fa8b5bb4 100644 --- a/src/preprocessing/assertion_pipeline.h +++ b/src/preprocessing/assertion_pipeline.h @@ -21,7 +21,11 @@ #include <vector> #include "expr/node.h" +#include "expr/proof_generator.h" +#include "expr/proof_node_manager.h" +#include "smt/preprocess_proof_generator.h" #include "smt/term_formula_removal.h" +#include "theory/trust_node.h" namespace CVC4 { namespace preprocessing { @@ -54,8 +58,17 @@ class AssertionPipeline * @param n The assertion/assumption * @param isAssumption If true, records that \p n is an assumption. Note that * all assumptions have to be added contiguously. + * @param isInput If true, n is an input formula (an assumption in the main + * body of the overall proof). + * @param pg The proof generator who can provide a proof of n. The proof + * generator is not required and is ignored if isInput is true. */ - void push_back(Node n, bool isAssumption = false); + void push_back(Node n, + bool isAssumption = false, + bool isInput = false, + ProofGenerator* pg = nullptr); + /** Same as above, with TrustNode */ + void pushBackTrusted(theory::TrustNode trn); std::vector<Node>& ref() { return d_nodes; } const std::vector<Node>& ref() const { return d_nodes; } @@ -66,21 +79,31 @@ class AssertionPipeline /* * Replaces assertion i with node n and records the dependency between the * original assertion and its replacement. + * + * @param i The position of the assertion to replace. + * @param n The replacement assertion. + * @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); + void replace(size_t i, Node n, ProofGenerator* pg = nullptr); + /** 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); - - /* - * Replaces an assertion with a vector of assertions and records the - * dependencies. - */ - void replace(size_t i, const std::vector<Node>& ns); + 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; } @@ -125,7 +148,12 @@ class AssertionPipeline { return d_storeSubstsInAsserts && i == d_substsIndex; } - + //------------------------------------ for proofs + /** Set proof generator */ + void setProofGenerator(smt::PreprocessProofGenerator* pppg); + /** Is proof enabled? */ + bool isProofEnabled() const; + //------------------------------------ end for proofs private: /** The list of current assertions */ std::vector<Node> d_nodes; @@ -157,6 +185,8 @@ class AssertionPipeline size_t d_assumptionsStart; /** The number of assumptions */ size_t d_numAssumptions; + /** The proof generator, if one is provided */ + smt::PreprocessProofGenerator* d_pppg; }; /* class AssertionPipeline */ } // namespace preprocessing |