(proof-new) CDProof inherits from ProofGenerator (#4622)

This design simplifies a number of issues and makes the PRefProofGenerator class obsolete.

diff --git a/src/expr/lazy_proof.cpp b/src/expr/lazy_proof.cpp
index 400ce2cf0ba2d1afb10a492fb4b4602ec39ead2d..3980a3cb39cd7a6b06fdb485fdeb8c37b8d02835 100644 (file)
--- 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<ProofNode> LazyCDProof::mkProof(Node fact)
+std::shared_ptr<ProofNode> 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<ProofNode> opf = CDProof::mkProof(fact);
+  std::shared_ptr<ProofNode> 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 1f7487a6b87046254c7c4c6c69cf4608b328ad88..c802de39e85cc51356e746f9167328ae54ebcf86 100644 (file)
--- 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<ProofNode> mkProof(Node fact) override;
+  std::shared_ptr<ProofNode> 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<Node, ProofGenerator*, NodeHashFunction>

diff --git a/src/expr/proof.cpp b/src/expr/proof.cpp
index 1c879ef0ba96986e29a92af5fc35bc9134f5c6cf..20e8e29e2a2f2cf3f11685c9a5c6bb24e0111126 100644 (file)
--- 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<ProofNode> CDProof::mkProof(Node fact)
+std::shared_ptr<ProofNode> CDProof::getProofFor(Node fact)
 {
   std::shared_ptr<ProofNode> 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 194b35bfb2521f8cf94f6caa1c6fe2c7f5d66a75..ff6b8bbf159e522734162394ba3b28dacf82a8da 100644 (file)
--- 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<ProofNode> mkProof(Node fact);
+  std::shared_ptr<ProofNode> 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<Node, std::shared_ptr<ProofNode>, NodeHashFunction>

diff --git a/src/expr/proof_generator.cpp b/src/expr/proof_generator.cpp
index 0e3c258187a3254cc7abd6d011de52a000f3980a..fd8f50415acf40ec8ee5b802e083a8d4531357c2 100644 (file)
--- 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<ProofNode> 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 1375541a30c51b782912b491e2eeac70f9399a52..35f94194fb287463f39172af205306dad52b48b3 100644 (file)
--- 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<ProofNode> 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 94bff5b8ca2e1b99082e3887da8c595ab4139456..70b42951073229517f5b914eeb8f2d9bfe68d9d0 100644 (file)
--- a/src/expr/term_conversion_proof_generator.cpp
+++ b/src/expr/term_conversion_proof_generator.cpp
@@ -94,8 +94,7 @@ std::shared_ptr<ProofNode> TConvProofGenerator::getProofFor(Node f)
 std::shared_ptr<ProofNode> 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<ProofNode> 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