diff options
Diffstat (limited to 'src/expr/term_conversion_proof_generator.h')
-rw-r--r-- | src/expr/term_conversion_proof_generator.h | 31 |
1 files changed, 29 insertions, 2 deletions
diff --git a/src/expr/term_conversion_proof_generator.h b/src/expr/term_conversion_proof_generator.h index d7ff6e8f6..e634b8a83 100644 --- a/src/expr/term_conversion_proof_generator.h +++ b/src/expr/term_conversion_proof_generator.h @@ -35,6 +35,19 @@ enum class TConvPolicy : uint32_t /** Writes a term conversion policy name to a stream. */ std::ostream& operator<<(std::ostream& out, TConvPolicy tcpol); +/** A policy for how proofs are cached in TConvProofGenerator */ +enum class TConvCachePolicy : uint32_t +{ + // proofs are statically cached + STATIC, + // proofs are dynamically cached, cleared when a new rewrite is added + DYNAMIC, + // proofs are never cached + NEVER, +}; +/** Writes a term conversion cache policy name to a stream. */ +std::ostream& operator<<(std::ostream& out, TConvCachePolicy tcpol); + /** * The term conversion proof generator. * @@ -75,17 +88,23 @@ std::ostream& operator<<(std::ostream& out, TConvPolicy tcpol); class TConvProofGenerator : public ProofGenerator { public: - /** Constructor + /** + * Constructor, which notice does fixpoint rewriting (since this is the + * most common use case) and never caches. * * @param pnm The proof node manager for constructing ProofNode objects. * @param c The context that this class depends on. If none is provided, * this class is context-independent. * @param tpol The policy for applying rewrite steps of this class. For * details, see d_policy. + * @param cpol The caching policy for this generator. + * @param name The name of this generator (for debugging). */ TConvProofGenerator(ProofNodeManager* pnm, context::Context* c = nullptr, - TConvPolicy pol = TConvPolicy::FIXPOINT); + TConvPolicy pol = TConvPolicy::FIXPOINT, + TConvCachePolicy cpol = TConvCachePolicy::NEVER, + std::string name = "TConvProofGenerator"); ~TConvProofGenerator(); /** * Add rewrite step t --> s based on proof generator. @@ -136,6 +155,12 @@ class TConvProofGenerator : public ProofGenerator * f(a,c) = f(f(c),d) if d_policy is ONCE. */ TConvPolicy d_policy; + /** The cache policy */ + TConvCachePolicy d_cpolicy; + /** Name identifier */ + std::string d_name; + /** The cache for terms */ + std::map<Node, std::shared_ptr<ProofNode> > d_cache; /** * Adds a proof of t = t' to the proof pf where t' is the result of rewriting * t based on the rewrite steps registered to this class. This method then @@ -147,6 +172,8 @@ class TConvProofGenerator : public ProofGenerator * and a rewrite step has not already been registered for t. */ Node registerRewriteStep(Node t, Node s); + /** cache that r is the rewritten form of cur, pf can provide a proof */ + void doCache(Node cur, Node r, LazyCDProof& pf); }; } // namespace CVC4 |