(proof-new) Add lazy proof utility (#4589)

Adds an extension of CDProof where facts can be mapped to (lazy) proof generators.

diff --git a/src/expr/CMakeLists.txt b/src/expr/CMakeLists.txt
index 2e02586ce8d27f814821bf4553871046668082c5..3d74d0badc558104532340a4671c00e5fa52b3c8 100644 (file)
--- a/src/expr/CMakeLists.txt
+++ b/src/expr/CMakeLists.txt
@@ -15,6 +15,8 @@ libcvc4_add_sources(
   expr_sequence.cpp
   expr_sequence.h
   kind_map.h
+  lazy_proof.cpp
+  lazy_proof.h
   match_trie.cpp
   match_trie.h
   node.cpp

diff --git a/src/expr/lazy_proof.cpp b/src/expr/lazy_proof.cpp
new file mode 100644 (file)
index 0000000..ae0ddbb
--- /dev/null
+++ b/src/expr/lazy_proof.cpp
@@ -0,0 +1,179 @@
+/*********************                                                        */
+/*! \file lazy_proof.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 lazy proof utility
+ **/
+
+#include "expr/lazy_proof.h"
+
+using namespace CVC4::kind;
+
+namespace CVC4 {
+
+LazyCDProof::LazyCDProof(ProofNodeManager* pnm,
+                         ProofGenerator* dpg,
+                         context::Context* c)
+    : CDProof(pnm, c), d_gens(c ? c : &d_context), d_defaultGen(dpg)
+{
+}
+
+LazyCDProof::~LazyCDProof() {}
+
+std::shared_ptr<ProofNode> LazyCDProof::mkProof(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);
+  Assert(opf != nullptr);
+  if (!hasGenerators())
+  {
+    Trace("lazy-cdproof") << "...no generators, finished" << std::endl;
+    // optimization: no generators, we are done
+    return opf;
+  }
+  // otherwise, we traverse the proof opf and fill in the ASSUME leafs that
+  // have generators
+  std::unordered_set<ProofNode*> visited;
+  std::unordered_set<ProofNode*>::iterator it;
+  std::vector<ProofNode*> visit;
+  ProofNode* cur;
+  visit.push_back(opf.get());
+  do
+  {
+    cur = visit.back();
+    visit.pop_back();
+    it = visited.find(cur);
+
+    if (it == visited.end())
+    {
+      visited.insert(cur);
+      if (cur->getRule() == PfRule::ASSUME)
+      {
+        Node afact = cur->getResult();
+        bool isSym = false;
+        ProofGenerator* pg = getGeneratorFor(afact, isSym);
+        if (pg != nullptr)
+        {
+          Trace("lazy-cdproof") << "LazyCDProof: Call generator for assumption "
+                                << afact << std::endl;
+          Node afactGen = isSym ? CDProof::getSymmFact(afact) : afact;
+          Assert(!afactGen.isNull());
+          // use the addProofTo interface
+          if (!pg->addProofTo(afactGen, this))
+          {
+            Trace("lazy-cdproof") << "LazyCDProof: Failed added fact for "
+                                  << afactGen << std::endl;
+            Assert(false) << "Proof generator " << pg->identify()
+                          << " could not add proof for fact " << afactGen
+                          << std::endl;
+          }
+          else
+          {
+            Trace("lazy-cdproof") << "LazyCDProof: Successfully added fact for "
+                                  << afactGen << std::endl;
+          }
+        }
+        else
+        {
+          Trace("lazy-cdproof")
+              << "LazyCDProof: No generator for " << afact << std::endl;
+        }
+        // Notice that we do not traverse the proofs that have been generated
+        // lazily by the proof generators here.  In other words, we assume that
+        // the proofs from provided proof generators are final and need
+        // no further modification by this class.
+      }
+      else
+      {
+        const std::vector<std::shared_ptr<ProofNode>>& cc = cur->getChildren();
+        for (const std::shared_ptr<ProofNode>& cp : cc)
+        {
+          visit.push_back(cp.get());
+        }
+      }
+    }
+  } while (!visit.empty());
+  // we have now updated the ASSUME leafs of opf, return it
+  Trace("lazy-cdproof") << "...finished" << std::endl;
+  return opf;
+}
+
+void LazyCDProof::addLazyStep(Node expected,
+                              ProofGenerator* pg,
+                              bool forceOverwrite)
+{
+  Assert(pg != nullptr);
+  if (!forceOverwrite)
+  {
+    NodeProofGeneratorMap::const_iterator it = d_gens.find(expected);
+    if (it != d_gens.end())
+    {
+      // don't overwrite something that is already there
+      return;
+    }
+  }
+  // just store now
+  d_gens.insert(expected, pg);
+}
+
+ProofGenerator* LazyCDProof::getGeneratorFor(Node fact,
+                                             bool& isSym)
+{
+  isSym = false;
+  NodeProofGeneratorMap::const_iterator it = d_gens.find(fact);
+  if (it != d_gens.end())
+  {
+    return (*it).second;
+  }
+  Node factSym = CDProof::getSymmFact(fact);
+  // could be symmetry
+  if (factSym.isNull())
+  {
+    // can't be symmetry, return the default generator
+    return d_defaultGen;
+  }
+  it = d_gens.find(factSym);
+  if (it != d_gens.end())
+  {
+    isSym = true;
+    return (*it).second;
+  }
+  // return the default generator
+  return d_defaultGen;
+}
+
+bool LazyCDProof::hasGenerators() const
+{
+  return !d_gens.empty() || d_defaultGen != nullptr;
+}
+
+bool LazyCDProof::hasGenerator(Node fact) const
+{
+  if (d_defaultGen != nullptr)
+  {
+    return true;
+  }
+  NodeProofGeneratorMap::const_iterator it = d_gens.find(fact);
+  if (it != d_gens.end())
+  {
+    return true;
+  }
+  // maybe there is a symmetric fact?
+  Node factSym = CDProof::getSymmFact(fact);
+  if (!factSym.isNull())
+  {
+    it = d_gens.find(factSym);
+  }
+  return it != d_gens.end();
+}
+
+}  // namespace CVC4

diff --git a/src/expr/lazy_proof.h b/src/expr/lazy_proof.h
new file mode 100644 (file)
index 0000000..d12aa1a
--- /dev/null
+++ b/src/expr/lazy_proof.h
@@ -0,0 +1,101 @@
+/*********************                                                        */
+/*! \file lazy_proof.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 Lazy proof utility
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef CVC4__EXPR__LAZY_PROOF_H
+#define CVC4__EXPR__LAZY_PROOF_H
+
+#include <unordered_map>
+#include <vector>
+
+#include "expr/proof.h"
+#include "expr/proof_generator.h"
+#include "expr/proof_node_manager.h"
+
+namespace CVC4 {
+
+/**
+ * A (context-dependent) lazy proof. This class is an extension of CDProof
+ * that additionally maps facts to proof generators in a context-dependent
+ * manner. It extends CDProof with an additional method, addLazyStep for adding
+ * steps to a proof via a given proof generator.
+ */
+class LazyCDProof : public CDProof
+{
+ public:
+  /** Constructor
+   *
+   * @param pnm The proof node manager for constructing ProofNode objects.
+   * @param dpg The (optional) default proof generator, which is called
+   * for facts that have no explicitly provided generator.
+   * @param c The context that this class depends on. If none is provided,
+   * this class is context-independent.
+   */
+  LazyCDProof(ProofNodeManager* pnm,
+              ProofGenerator* dpg = nullptr,
+              context::Context* c = nullptr);
+  ~LazyCDProof();
+  /**
+   * Get lazy proof for fact, or nullptr if it does not exist. This may
+   * 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;
+  /** Add step by generator
+   *
+   * This method stores that expected can be proven by proof generator pg if
+   * it is required to do so. This mapping is maintained in the remainder of
+   * the current context (according to the context c provided to this class).
+   *
+   * 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.
+   *
+   * @param expected The fact that can be proven.
+   * @param pg The generator that can proof expected.
+   * @param forceOverwrite If this flag is true, then this call overwrites
+   * an existing proof generator provided for expected, if one was provided
+   * via a previous call to addLazyStep in the current context.
+   */
+  void addLazyStep(Node expected,
+                   ProofGenerator* pg,
+                   bool forceOverwrite = false);
+  /**
+   * Does this have any proof generators? This method always returns true
+   * if the default is non-null.
+   */
+  bool hasGenerators() const;
+  /** Does the given fact have an explicitly provided generator? */
+  bool hasGenerator(Node fact) const;
+
+ protected:
+  typedef context::CDHashMap<Node, ProofGenerator*, NodeHashFunction>
+      NodeProofGeneratorMap;
+  /** Maps facts that can be proven to generators */
+  NodeProofGeneratorMap d_gens;
+  /** The default proof generator */
+  ProofGenerator* d_defaultGen;
+  /**
+   * Get generator for fact, or nullptr if it doesnt exist. This method is
+   * robust to symmetry of (dis)equality. It updates isSym to true if a
+   * proof generator for the symmetric form of fact was provided.
+   */
+  ProofGenerator* getGeneratorFor(Node fact, bool& isSym);
+};
+
+}  // namespace CVC4
+
+#endif /* CVC4__EXPR__LAZY_PROOF_H */