diff options
Diffstat (limited to 'src/expr/term_conversion_proof_generator.h')
| -rw-r--r-- | src/expr/term_conversion_proof_generator.h | 70 |
1 files changed, 61 insertions, 9 deletions
diff --git a/src/expr/term_conversion_proof_generator.h b/src/expr/term_conversion_proof_generator.h index e634b8a83..faee2b9e3 100644 --- a/src/expr/term_conversion_proof_generator.h +++ b/src/expr/term_conversion_proof_generator.h @@ -21,6 +21,7 @@ #include "expr/lazy_proof.h" #include "expr/proof_generator.h" #include "expr/proof_node_manager.h" +#include "expr/term_context.h" namespace CVC4 { @@ -84,6 +85,35 @@ std::ostream& operator<<(std::ostream& out, TConvCachePolicy tcpol); * addRewriteStep. In particular, notice that in the above example, we realize * that f(a) --> c at pre-rewrite instead of post-rewriting a --> b and then * ending with f(a)=f(b). + * + * This class may additionally be used for term-context-sensitive rewrite + * systems. An example is the term formula removal pass which rewrites + * terms dependending on whether they occur in a "term position", for details + * see RtfTermContext in expr/term_context.h. To use this class in a way + * that takes into account term contexts, the user of the term conversion + * proof generator should: + * (1) Provide a term context callback to the constructor of this class (tccb), + * (2) Register rewrite steps that indicate the term context identifier of + * the rewrite, which is a uint32_t. + * + * For example, RtfTermContext uses hash value 2 to indicate we are in a "term + * position". Say the user of this class calls: + * addRewriteStep( (and A B), BOOLEAN_TERM_VARIABLE_1, pg, true, 2) + * This indicates that (and A B) should rewrite to BOOLEAN_TERM_VARIABLE_1 if + * (and A B) occurs in a term position, where pg is a proof generator that can + * provide a closed proof of: + * (= (and A B) BOOLEAN_TERM_VARIABLE_1) + * Subsequently, this class may respond to a call to getProofFor on: + * (= + * (or (and A B) (P (and A B))) + * (or (and A B) (P BOOLEAN_TERM_VARIABLE_1))) + * where P is a predicate Bool -> Bool. The proof returned by this class + * involves congruence and pg's proof of the equivalence above. In particular, + * assuming its proof of the equivalence is P1, this proof is: + * (CONG{=} (CONG{or} (REFL (and A B)) (CONG{P} P1))) + * Notice the callback provided to this class ensures that the rewrite is + * replayed in the expected way, e.g. the occurrence of (and A B) that is not + * in term position is not rewritten. */ class TConvProofGenerator : public ProofGenerator { @@ -99,32 +129,48 @@ class TConvProofGenerator : public ProofGenerator * details, see d_policy. * @param cpol The caching policy for this generator. * @param name The name of this generator (for debugging). + * @param tccb The term context callback that this class depends on. If this + * is non-null, then this class stores a term-context-sensitive rewrite + * system. The rewrite steps should be given term context identifiers. */ TConvProofGenerator(ProofNodeManager* pnm, context::Context* c = nullptr, TConvPolicy pol = TConvPolicy::FIXPOINT, TConvCachePolicy cpol = TConvCachePolicy::NEVER, - std::string name = "TConvProofGenerator"); + std::string name = "TConvProofGenerator", + TermContext* tccb = nullptr); ~TConvProofGenerator(); /** * Add rewrite step t --> s based on proof generator. + * + * @param isClosed whether to expect that pg can provide a closed proof for + * this fact. + * @param tctx The term context identifier for the rewrite step. This + * value should correspond to one generated by the term context callback + * class provided in the argument tccb provided to the constructor of this + * class. */ - void addRewriteStep(Node t, Node s, ProofGenerator* pg); + void addRewriteStep(Node t, + Node s, + ProofGenerator* pg, + bool isClosed = true, + uint32_t tctx = 0); /** Same as above, for a single step */ - void addRewriteStep(Node t, Node s, ProofStep ps); + void addRewriteStep(Node t, Node s, ProofStep ps, uint32_t tctx = 0); /** Same as above, with explicit arguments */ void addRewriteStep(Node t, Node s, PfRule id, const std::vector<Node>& children, - const std::vector<Node>& args); + const std::vector<Node>& args, + uint32_t tctx = 0); /** Has rewrite step for term t */ - bool hasRewriteStep(Node t) const; + bool hasRewriteStep(Node t, uint32_t tctx = 0) const; /** * Get rewrite step for term t, returns the s provided in a call to * addRewriteStep if one exists, or null otherwise. */ - Node getRewriteStep(Node t) const; + Node getRewriteStep(Node t, uint32_t tctx = 0) const; /** * Get the proof for formula f. It should be the case that f is of the form * t = t', where t' is the result of rewriting t based on the rewrite steps @@ -161,19 +207,25 @@ class TConvProofGenerator : public ProofGenerator std::string d_name; /** The cache for terms */ std::map<Node, std::shared_ptr<ProofNode> > d_cache; + /** An (optional) term context object */ + TermContext* d_tcontext; + /** Get rewrite step for (hash value of) term. */ + Node getRewriteStepInternal(Node thash) const; /** * 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 * returns the proved equality t = t'. */ - Node getProofForRewriting(Node t, LazyCDProof& pf); + Node getProofForRewriting(Node t, LazyCDProof& pf, TermContext* tc = nullptr); /** * Register rewrite step, returns the equality t=s if t is distinct from s * and a rewrite step has not already been registered for t. */ - Node registerRewriteStep(Node t, Node s); + Node registerRewriteStep(Node t, Node s, uint32_t tctx); /** cache that r is the rewritten form of cur, pf can provide a proof */ - void doCache(Node cur, Node r, LazyCDProof& pf); + void doCache(Node curHash, Node cur, Node r, LazyCDProof& pf); + /** get debug information on this generator */ + std::string toStringDebug() const; }; } // namespace CVC4 |