(proof-new) Add abstract proof generator class (#4574)

Also adds a commonly used proof generator: the proof reference proof generator.

diff --git a/src/expr/CMakeLists.txt b/src/expr/CMakeLists.txt
index 6415e21323db8e3b875a3fb26642d5b927a715f6..2e02586ce8d27f814821bf4553871046668082c5 100644 (file)
--- a/src/expr/CMakeLists.txt
+++ b/src/expr/CMakeLists.txt
@@ -41,6 +41,8 @@ libcvc4_add_sources(
   proof.h
   proof_checker.cpp
   proof_checker.h
+  proof_generator.cpp
+  proof_generator.h
   proof_node.cpp
   proof_node.h
   proof_node_to_sexpr.cpp

diff --git a/src/expr/proof_generator.cpp b/src/expr/proof_generator.cpp
new file mode 100644 (file)
index 0000000..d59c8b5
--- /dev/null
+++ b/src/expr/proof_generator.cpp
@@ -0,0 +1,77 @@
+/*********************                                                        */
+/*! \file proof_generator.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief Implementation of proof generator utility
+ **/
+
+#include "expr/proof_generator.h"
+
+#include "expr/proof.h"
+
+namespace CVC4 {
+
+ProofGenerator::ProofGenerator() {}
+
+ProofGenerator::~ProofGenerator() {}
+
+std::shared_ptr<ProofNode> ProofGenerator::getProofFor(Node f)
+{
+  Unreachable() << "ProofGenerator::getProofFor: " << identify()
+                << " has no implementation" << std::endl;
+  return nullptr;
+}
+
+bool ProofGenerator::addProofTo(Node f, CDProof* pf, CDPOverwrite opolicy)
+{
+  Trace("pfgen") << "ProofGenerator::addProofTo: " << f << "..." << std::endl;
+  Assert(pf != nullptr);
+  // plug in the proof provided by the generator, if it exists
+  std::shared_ptr<ProofNode> apf = getProofFor(f);
+  if (apf != nullptr)
+  {
+    if (Trace.isOn("pfgen"))
+    {
+      std::stringstream ss;
+      apf->printDebug(ss);
+      Trace("pfgen") << "...got proof " << ss.str() << std::endl;
+    }
+    // Add the proof, without deep copying.
+    if (pf->addProof(apf, opolicy, false))
+    {
+      Trace("pfgen") << "...success!" << std::endl;
+      return true;
+    }
+    Trace("pfgen") << "...failed to add proof" << std::endl;
+  }
+  else
+  {
+    Trace("pfgen") << "...failed, no proof" << std::endl;
+    Assert(false) << "Failed to get proof from generator for fact " << f;
+  }
+  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
new file mode 100644 (file)
index 0000000..7de53fe
--- /dev/null
+++ b/src/expr/proof_generator.h
@@ -0,0 +1,117 @@
+/*********************                                                        */
+/*! \file proof_generator.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief The abstract proof generator class
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef CVC4__EXPR__PROOF_GENERATOR_H
+#define CVC4__EXPR__PROOF_GENERATOR_H
+
+#include "expr/node.h"
+#include "expr/proof.h"
+#include "expr/proof_node.h"
+
+namespace CVC4 {
+
+/**
+ * An abstract proof generator class.
+ *
+ * A proof generator is intended to be used as a utility e.g. in theory
+ * solvers for constructing and storing proofs internally. A theory may have
+ * multiple instances of ProofGenerator objects, e.g. if it has more than one
+ * way of justifying lemmas or conflicts.
+ *
+ * A proof generator has two main interfaces for generating proofs:
+ * (1) getProofFor, and (2) addProofTo. The latter is optional.
+ *
+ * The addProofTo method can be used as an optimization for avoiding
+ * the construction of the ProofNode for a given fact.
+ *
+ * If no implementation of addProofTo is provided, then addProofTo(f, pf)
+ * calls getProofFor(f) and links the topmost ProofNode of the returned proof
+ * into pf. Note this top-most ProofNode can be avoided in the addProofTo
+ * method.
+ */
+class ProofGenerator
+{
+ public:
+  ProofGenerator();
+  virtual ~ProofGenerator();
+  /** Get the proof for formula f
+   *
+   * This forces the proof generator to construct a proof for formula f and
+   * return it. If this is an "eager" proof generator, this function is expected
+   * to be implemented as a map lookup. If this is a "lazy" proof generator,
+   * this function is expected to invoke a proof producing procedure of the
+   * generator.
+   *
+   * It should be the case that hasProofFor(f) is true.
+   *
+   * @param f The fact to get the proof for.
+   * @return The proof for f.
+   */
+  virtual std::shared_ptr<ProofNode> getProofFor(Node f);
+  /**
+   * Add the proof for formula f to proof pf. The proof of f is overwritten in
+   * pf based on the policy opolicy.
+   *
+   * @param f The fact to get the proof for.
+   * @param pf The CDProof object to add the proof to.
+   * @param opolicy The overwrite policy for adding to pf.
+   * @return True if this call was sucessful.
+   */
+  virtual bool addProofTo(Node f,
+                          CDProof* pf,
+                          CDPOverwrite opolicy = CDPOverwrite::ASSUME_ONLY);
+  /**
+   * Can we give the proof for formula f? This is used for debugging. This
+   * returns false if the generator cannot provide a proof of formula f.
+   *
+   * Also notice that this function does not require the proof for f to be
+   * constructed at the time of this call. Thus, if this is a "lazy" proof
+   * generator, it is expected that this call is implemented as a map lookup
+   * into the bookkeeping maintained by the generator only.
+   *
+   * Notice the default return value is true. In other words, a proof generator
+   * may choose to override this function to verify the construction, although
+   * we do not insist this is the case.
+   */
+  virtual bool hasProofFor(Node f) { return true; }
+  /** Identify this generator (for debugging, etc..) */
+  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 */