diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-08-18 16:42:22 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-08-18 16:42:22 -0500 |
commit | 77fdb2327ae969a7d97b6eb67ad3526d78867b3a (patch) | |
tree | 8a16e05c53feca4085254566e7a15e1b14310704 /src/theory/theory_preprocessor.h | |
parent | aa8da1ff4e7f119408dbf14074b9a5efcb06618b (diff) |
(proof-new) Theory preprocessor proof producing (#4807)
This makes the theory preprocessor proof producing in the new infrastructure, which involves updating its interfaces to TrustNode in a few places.
Diffstat (limited to 'src/theory/theory_preprocessor.h')
-rw-r--r-- | src/theory/theory_preprocessor.h | 31 |
1 files changed, 27 insertions, 4 deletions
diff --git a/src/theory/theory_preprocessor.h b/src/theory/theory_preprocessor.h index 2f3813e68..95236ded3 100644 --- a/src/theory/theory_preprocessor.h +++ b/src/theory/theory_preprocessor.h @@ -19,15 +19,16 @@ #include <unordered_map> +#include "expr/lazy_proof.h" #include "expr/node.h" -#include "preprocessing/assertion_pipeline.h" +#include "expr/term_conversion_proof_generator.h" +#include "theory/trust_node.h" namespace CVC4 { class LogicInfo; class TheoryEngine; class RemoveTermFormulas; -class LazyCDProof; namespace theory { @@ -40,7 +41,9 @@ class TheoryPreprocessor public: /** Constructs a theory preprocessor */ - TheoryPreprocessor(TheoryEngine& engine, RemoveTermFormulas& tfr); + TheoryPreprocessor(TheoryEngine& engine, + RemoveTermFormulas& tfr, + ProofNodeManager* pnm = nullptr); /** Destroys a theory preprocessor */ ~TheoryPreprocessor(); /** Clear the cache of this class */ @@ -69,7 +72,7 @@ class TheoryPreprocessor * the formula. This is only called on input assertions, after ITEs * have been removed. */ - Node theoryPreprocess(TNode node); + TrustNode theoryPreprocess(TNode node); private: /** Reference to owning theory engine */ @@ -80,8 +83,28 @@ class TheoryPreprocessor NodeMap d_ppCache; /** The term formula remover */ RemoveTermFormulas& d_tfr; + /** The context for the proof generator below */ + context::Context d_pfContext; + /** A term conversion proof generator */ + std::unique_ptr<TConvProofGenerator> d_tpg; + /** A lazy proof, for additional lemmas. */ + std::unique_ptr<LazyCDProof> d_lp; /** Helper for theoryPreprocess */ Node ppTheoryRewrite(TNode term); + /** + * Rewrite with proof, which stores a REWRITE step in d_tpg if necessary + * and returns the rewritten form of term. + */ + Node rewriteWithProof(Node term); + /** + * Preprocess with proof, which calls the appropriate ppRewrite method, + * stores the corresponding rewrite step in d_tpg if necessary and returns + * the preprocessed and rewritten form of term. It should be the case that + * term is already in rewritten form. + */ + Node preprocessWithProof(Node term); + /** Proofs enabled */ + bool isProofEnabled() const; }; } // namespace theory |