From e8000a4693ecc1f8418c80726032ef6937e36241 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Fri, 19 Jun 2020 18:55:19 -0500 Subject: [PATCH] (proof-new) CDProof inherits from ProofGenerator (#4622) This design simplifies a number of issues and makes the PRefProofGenerator class obsolete. --- src/expr/lazy_proof.cpp | 6 ++-- src/expr/lazy_proof.h | 6 ++-- src/expr/proof.cpp | 16 ++------- src/expr/proof.h | 20 +++-------- src/expr/proof_generator.cpp | 27 +++++++------- src/expr/proof_generator.h | 37 ++++++++------------ src/expr/term_conversion_proof_generator.cpp | 5 ++- 7 files changed, 45 insertions(+), 72 deletions(-) diff --git a/src/expr/lazy_proof.cpp b/src/expr/lazy_proof.cpp index 400ce2cf0..3980a3cb3 100644 --- a/src/expr/lazy_proof.cpp +++ b/src/expr/lazy_proof.cpp @@ -27,12 +27,12 @@ LazyCDProof::LazyCDProof(ProofNodeManager* pnm, LazyCDProof::~LazyCDProof() {} -std::shared_ptr LazyCDProof::mkProof(Node fact) +std::shared_ptr LazyCDProof::getProofFor(Node fact) { Trace("lazy-cdproof") << "LazyCDProof::mkLazyProof " << fact << std::endl; // make the proof, which should always be non-null, since we construct an // assumption in the worst case. - std::shared_ptr opf = CDProof::mkProof(fact); + std::shared_ptr opf = CDProof::getProofFor(fact); Assert(opf != nullptr); if (!hasGenerators()) { @@ -176,4 +176,6 @@ bool LazyCDProof::hasGenerator(Node fact) const return it != d_gens.end(); } +std::string LazyCDProof::identify() const { return "LazyCDProof"; } + } // namespace CVC4 diff --git a/src/expr/lazy_proof.h b/src/expr/lazy_proof.h index 1f7487a6b..c802de39e 100644 --- a/src/expr/lazy_proof.h +++ b/src/expr/lazy_proof.h @@ -52,7 +52,7 @@ class LazyCDProof : public CDProof * additionally call proof generators to generate proofs for ASSUME nodes that * don't yet have a concrete proof. */ - std::shared_ptr mkProof(Node fact) override; + std::shared_ptr getProofFor(Node fact) override; /** Add step by generator * * This method stores that expected can be proven by proof generator pg if @@ -62,7 +62,7 @@ class LazyCDProof : public CDProof * It is important to note that pg is asked to provide a proof for expected * only when no other call for the fact expected is provided via the addStep * method of this class. In particular, pg is asked to prove expected when it - * appears as the conclusion of an ASSUME leaf within CDProof::mkProof. + * appears as the conclusion of an ASSUME leaf within CDProof::getProofFor. * * @param expected The fact that can be proven. * @param pg The generator that can proof expected. @@ -80,6 +80,8 @@ class LazyCDProof : public CDProof bool hasGenerators() const; /** Does the given fact have an explicitly provided generator? */ bool hasGenerator(Node fact) const; + /** identify */ + std::string identify() const override; protected: typedef context::CDHashMap diff --git a/src/expr/proof.cpp b/src/expr/proof.cpp index 1c879ef0b..20e8e29e2 100644 --- a/src/expr/proof.cpp +++ b/src/expr/proof.cpp @@ -18,18 +18,6 @@ using namespace CVC4::kind; namespace CVC4 { -std::ostream& operator<<(std::ostream& out, CDPOverwrite opol) -{ - switch (opol) - { - case CDPOverwrite::ALWAYS: out << "ALWAYS"; break; - case CDPOverwrite::ASSUME_ONLY: out << "ASSUME_ONLY"; break; - case CDPOverwrite::NEVER: out << "NEVER"; break; - default: out << "CDPOverwrite:unknown"; break; - } - return out; -} - CDProof::CDProof(ProofNodeManager* pnm, context::Context* c) : d_manager(pnm), d_context(), d_nodes(c ? c : &d_context) { @@ -37,7 +25,7 @@ CDProof::CDProof(ProofNodeManager* pnm, context::Context* c) CDProof::~CDProof() {} -std::shared_ptr CDProof::mkProof(Node fact) +std::shared_ptr CDProof::getProofFor(Node fact) { std::shared_ptr pf = getProofSymm(fact); if (pf != nullptr) @@ -436,4 +424,6 @@ Node CDProof::getSymmFact(TNode f) return polarity ? symFact : symFact.notNode(); } +std::string CDProof::identify() const { return "CDProof"; } + } // namespace CVC4 diff --git a/src/expr/proof.h b/src/expr/proof.h index 194b35bfb..ff6b8bbf1 100644 --- a/src/expr/proof.h +++ b/src/expr/proof.h @@ -22,25 +22,13 @@ #include "context/cdhashmap.h" #include "expr/node.h" +#include "expr/proof_generator.h" #include "expr/proof_node.h" #include "expr/proof_node_manager.h" #include "expr/proof_step_buffer.h" namespace CVC4 { -/** An overwrite policy for CDProof below */ -enum class CDPOverwrite : uint32_t -{ - // always overwrite an existing step. - ALWAYS, - // overwrite ASSUME with non-ASSUME steps. - ASSUME_ONLY, - // never overwrite an existing step. - NEVER, -}; -/** Writes a overwrite policy name to a stream. */ -std::ostream& operator<<(std::ostream& out, CDPOverwrite opol); - /** * A (context-dependent) proof. * @@ -143,7 +131,7 @@ std::ostream& operator<<(std::ostream& out, CDPOverwrite opol); * of ID_2. More generally, CDProof::isSame(F,G) returns true if F and G are * essentially the same formula according to this class. */ -class CDProof +class CDProof : public ProofGenerator { public: CDProof(ProofNodeManager* pnm, context::Context* c = nullptr); @@ -161,7 +149,7 @@ class CDProof * returned proof may be updated by further calls to this class. The caller * should call ProofNode::clone if they want to own it. */ - virtual std::shared_ptr mkProof(Node fact); + std::shared_ptr getProofFor(Node fact) override; /** Add step * * @param expected The intended conclusion of this proof step. This must be @@ -241,6 +229,8 @@ class CDProof * null if none exist. */ static Node getSymmFact(TNode f); + /** identify */ + std::string identify() const override; protected: typedef context::CDHashMap, NodeHashFunction> diff --git a/src/expr/proof_generator.cpp b/src/expr/proof_generator.cpp index 0e3c25818..fd8f50415 100644 --- a/src/expr/proof_generator.cpp +++ b/src/expr/proof_generator.cpp @@ -18,6 +18,18 @@ namespace CVC4 { +std::ostream& operator<<(std::ostream& out, CDPOverwrite opol) +{ + switch (opol) + { + case CDPOverwrite::ALWAYS: out << "ALWAYS"; break; + case CDPOverwrite::ASSUME_ONLY: out << "ASSUME_ONLY"; break; + case CDPOverwrite::NEVER: out << "NEVER"; break; + default: out << "CDPOverwrite:unknown"; break; + } + return out; +} + ProofGenerator::ProofGenerator() {} ProofGenerator::~ProofGenerator() {} @@ -59,19 +71,4 @@ bool ProofGenerator::addProofTo(Node f, CDProof* pf, CDPOverwrite opolicy) return false; } -PRefProofGenerator::PRefProofGenerator(CDProof* cd) : d_proof(cd) {} - -PRefProofGenerator::~PRefProofGenerator() {} - -std::shared_ptr PRefProofGenerator::getProofFor(Node f) -{ - Trace("pfgen") << "PRefProofGenerator::getProofFor: " << f << std::endl; - return d_proof->mkProof(f); -} - -std::string PRefProofGenerator::identify() const -{ - return "PRefProofGenerator"; -} - } // namespace CVC4 diff --git a/src/expr/proof_generator.h b/src/expr/proof_generator.h index 1375541a3..35f94194f 100644 --- a/src/expr/proof_generator.h +++ b/src/expr/proof_generator.h @@ -18,11 +18,25 @@ #define CVC4__EXPR__PROOF_GENERATOR_H #include "expr/node.h" -#include "expr/proof.h" #include "expr/proof_node.h" namespace CVC4 { +class CDProof; + +/** An overwrite policy for CDProof */ +enum class CDPOverwrite : uint32_t +{ + // always overwrite an existing step. + ALWAYS, + // overwrite ASSUME with non-ASSUME steps. + ASSUME_ONLY, + // never overwrite an existing step. + NEVER, +}; +/** Writes a overwrite policy name to a stream. */ +std::ostream& operator<<(std::ostream& out, CDPOverwrite opol); + /** * An abstract proof generator class. * @@ -91,27 +105,6 @@ class ProofGenerator virtual std::string identify() const = 0; }; -class CDProof; - -/** - * A "copy on demand" proof generator which returns proof nodes based on a - * reference to another CDProof. - */ -class PRefProofGenerator : public ProofGenerator -{ - public: - PRefProofGenerator(CDProof* cd); - ~PRefProofGenerator(); - /** Get proof for */ - std::shared_ptr getProofFor(Node f) override; - /** Identify this generator (for debugging, etc..) */ - std::string identify() const override; - - protected: - /** The reference proof */ - CDProof* d_proof; -}; - } // namespace CVC4 #endif /* CVC4__EXPR__PROOF_GENERATOR_H */ diff --git a/src/expr/term_conversion_proof_generator.cpp b/src/expr/term_conversion_proof_generator.cpp index 94bff5b8c..70b429510 100644 --- a/src/expr/term_conversion_proof_generator.cpp +++ b/src/expr/term_conversion_proof_generator.cpp @@ -94,8 +94,7 @@ std::shared_ptr TConvProofGenerator::getProofFor(Node f) std::shared_ptr TConvProofGenerator::getProofForRewriting(Node t) { // we use the existing proofs - PRefProofGenerator prg(&d_proof); - LazyCDProof pf(d_proof.getManager(), &prg); + LazyCDProof pf(d_proof.getManager(), &d_proof); NodeManager* nm = NodeManager::currentNM(); // Invariant: if visited[t] = s or rewritten[t] = s and t,s are distinct, // then pf is able to generate a proof of t=s. @@ -230,7 +229,7 @@ std::shared_ptr TConvProofGenerator::getProofForRewriting(Node t) Assert(!visited.find(t)->second.isNull()); // make the overall proof Node teq = t.eqNode(visited[t]); - return pf.mkProof(teq); + return pf.getProofFor(teq); } Node TConvProofGenerator::getRewriteStep(Node t) const -- 2.30.2