Add (context-dependent) Proof (#4323)

A (context-dependent) collection of proof steps that are linked to together to form a ProofNode dag.

Note that the name "Proof" is currently taken. I am calling this class "CDProof", although it is optionally context dependent.

3 files changed, 360 insertions, 0 deletions

diff --git a/src/expr/CMakeLists.txt b/src/expr/CMakeLists.txt
index f21241ef5..41df85455 100644
--- a/src/expr/CMakeLists.txt
+++ b/src/expr/CMakeLists.txt
@@ -33,6 +33,8 @@ libcvc4_add_sources(
   node_value.cpp
   node_value.h
   node_visitor.h
+  proof.cpp
+  proof.h
   proof_checker.cpp
   proof_checker.h
   proof_node.cpp
diff --git a/src/expr/proof.cpp b/src/expr/proof.cpp
new file mode 100644
index 000000000..6d2d70543
--- /dev/null
+++ b/src/expr/proof.cpp
@@ -0,0 +1,162 @@
+/*********************                                                        */
+/*! \file 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 proof
+ **/
+
+#include "expr/proof.h"
+
+using namespace CVC4::kind;
+
+namespace CVC4 {
+
+CDProof::CDProof(ProofNodeManager* pnm, context::Context* c)
+    : d_manager(pnm), d_context(), d_nodes(c ? c : &d_context)
+{
+}
+
+CDProof::~CDProof() {}
+
+std::shared_ptr<ProofNode> CDProof::getProof(Node fact) const
+{
+  NodeProofNodeMap::iterator it = d_nodes.find(fact);
+  if (it != d_nodes.end())
+  {
+    return (*it).second;
+  }
+  return nullptr;
+}
+
+bool CDProof::addStep(Node expected,
+                      PfRule id,
+                      const std::vector<Node>& children,
+                      const std::vector<Node>& args,
+                      bool ensureChildren,
+                      bool forceOverwrite)
+{
+  // we must provide expected
+  Assert(!expected.isNull());
+
+  NodeProofNodeMap::iterator it = d_nodes.find(expected);
+  if (it != d_nodes.end())
+  {
+    if (!forceOverwrite
+        && ((*it).second->getId() != PfRule::ASSUME || id == PfRule::ASSUME))
+    {
+      // we do not overwrite if forceOverwrite is false and the previously
+      // provided step was not an assumption, or if the currently provided step
+      // is a (duplicate) assumption
+      return true;
+    }
+    // we will overwrite the existing proof node by updating its contents below
+  }
+
+  // collect the child proofs, for each premise
+  std::vector<std::shared_ptr<ProofNode>> pchildren;
+  for (const Node& c : children)
+  {
+    std::shared_ptr<ProofNode> pc = getProof(c);
+    if (pc == nullptr)
+    {
+      if (ensureChildren)
+      {
+        // failed to get a proof for a child, fail
+        return false;
+      }
+      // otherwise, we initialize it as an assumption
+      std::vector<Node> pcargs = {c};
+      std::vector<std::shared_ptr<ProofNode>> pcassume;
+      pc = d_manager->mkNode(PfRule::ASSUME, pcassume, pcargs, c);
+      // assumptions never fail to check
+      Assert(pc != nullptr);
+      d_nodes.insert(c, pc);
+    }
+    pchildren.push_back(pc);
+  }
+
+  // create or update it
+  std::shared_ptr<ProofNode> pthis;
+  if (it == d_nodes.end())
+  {
+    pthis = d_manager->mkNode(id, pchildren, args, expected);
+    if (pthis == nullptr)
+    {
+      // failed to construct the node, perhaps due to a proof checking failure
+      return false;
+    }
+    d_nodes.insert(expected, pthis);
+  }
+  else
+  {
+    // update its value
+    pthis = (*it).second;
+    d_manager->updateNode(pthis.get(), id, pchildren, args);
+  }
+  // the result of the proof node should be expected
+  Assert(pthis->getResult() == expected);
+  return true;
+}
+
+bool CDProof::addProof(ProofNode* pn, bool forceOverwrite)
+{
+  std::unordered_map<ProofNode*, bool> visited;
+  std::unordered_map<ProofNode*, bool>::iterator it;
+  std::vector<ProofNode*> visit;
+  ProofNode* cur;
+  Node curFact;
+  visit.push_back(pn);
+  bool retValue = true;
+  do
+  {
+    cur = visit.back();
+    curFact = cur->getResult();
+    visit.pop_back();
+    it = visited.find(cur);
+    if (it == visited.end())
+    {
+      // visit the children
+      visited[cur] = false;
+      visit.push_back(cur);
+      const std::vector<std::shared_ptr<ProofNode>>& cs = cur->getChildren();
+      for (const std::shared_ptr<ProofNode>& c : cs)
+      {
+        visit.push_back(c.get());
+      }
+    }
+    else if (!it->second)
+    {
+      // we always call addStep, which may or may not overwrite the
+      // current step
+      std::vector<Node> pexp;
+      const std::vector<std::shared_ptr<ProofNode>>& cs = cur->getChildren();
+      for (const std::shared_ptr<ProofNode>& c : cs)
+      {
+        Assert(!c->getResult().isNull());
+        pexp.push_back(c->getResult());
+      }
+      // can ensure children at this point
+      bool res = addStep(curFact,
+                         cur->getId(),
+                         pexp,
+                         cur->getArguments(),
+                         true,
+                         forceOverwrite);
+      // should always succeed
+      Assert(res);
+      retValue = retValue && res;
+      visited[cur] = true;
+    }
+  } while (!visit.empty());
+
+  return retValue;
+}
+
+}  // namespace CVC4
diff --git a/src/expr/proof.h b/src/expr/proof.h
new file mode 100644
index 000000000..c3b9698ca
--- /dev/null
+++ b/src/expr/proof.h
@@ -0,0 +1,196 @@
+/*********************                                                        */
+/*! \file 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 Proof utility
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef CVC4__EXPR__PROOF_H
+#define CVC4__EXPR__PROOF_H
+
+#include <map>
+#include <vector>
+
+#include "context/cdhashmap.h"
+#include "expr/node.h"
+#include "expr/proof_node.h"
+#include "expr/proof_node_manager.h"
+
+namespace CVC4 {
+
+/**
+ * A (context-dependent) proof.
+ *
+ * This maintains a context-dependent map from formulas to ProofNode shared
+ * pointers. When a step is added, it internally uses mutable ProofNode pointers
+ * to link the steps in the proof together.
+ *
+ * It is important to note that the premises of proof steps given to this class
+ * are *Node* not *ProofNode*. In other words, the user of this class does
+ * not have to manage ProofNode pointers while using this class. Instead,
+ * ProofNode is the final product of this class, via the getProof interface,
+ * which returns a ProofNode object that has linked together the proof steps
+ * added to this object.
+ *
+ * Its main interface is the function addStep, which registers a single
+ * step in the proof. Its interface is:
+ *   addStep( <conclusion>, <rule>, <premises>, <args>, ...<options>... )
+ * where conclusion is what to be proven, rule is an identifier, premises
+ * are the formulas that imply conclusion, and args are additional arguments to
+ * the proof rule application. The options include whether we ensure children
+ * proofs already exist for the premises and our policty for overwriting
+ * existing steps.
+ *
+ * As an example, let A, B, C, D be formulas represented by Nodes. If we
+ * call:
+ * - addStep( A, ID_A, { B, C }, {} )
+ * - addStep( B, ID_B, { D }, {} )
+ * - addStep( E, ID_E, {}, {} )
+ * with default options, then getProof( A ) returns the ProofNode of the form:
+ *   ID_A( ID_B( ASSUME( D ) ), ASSUME( C ) )
+ * Notice that the above calls to addStep can be made in either order. The
+ * proof step for E was not involved in the proof of A.
+ *
+ * If the user wants to combine proofs, then a addProof interface is
+ * available. The method addProof can be seen as syntax sugar for making
+ * multiple calls to addStep. Continuing the above example, if we call:
+ * - addProof( F, ID_F( ASSUME( A ), ASSUME( E ) ) )
+ * is the same as calling steps corresponding the steps in the provided proof
+ * bottom-up, starting from the leaves.
+ * --- addStep( A, ASSUME, {}, {}, true )
+ * --- addStep( E, ASSUME, {}, {}, true )
+ * --- addStep( F, ID_F, { A, E }, {}, true )
+ * The fifth argument provided indicates that we want to ensure child proofs
+ * are already available for the step (see ensureChildren in addStep below).
+ * This will result in getProof( F ) returning:
+ *   ID_F( ID_A( ID_B( ASSUME( D ) ), ASSUME( C ) ), ID_E() )
+ * Notice that the proof of A by ID_A was not overwritten by ASSUME in the
+ * addStep call above.
+ *
+ * The policy for overwriting proof steps gives ASSUME a special status. An
+ * ASSUME step can be seen as a step whose justification has not yet been
+ * provided. Thus, it is always overwritten. Other proof rules are never
+ * overwritten, unless the argument forceOverwrite is true.
+ *
+ * As an another example, say that we call:
+ * - addStep( B, ID_B1 {}, {} )
+ * - addStep( A, ID_A1, {B, C}, {} )
+ * At this point, getProof( A ) returns:
+ *   ID_A1( ID_B1(), ASSUME(C) )
+ * Now, assume an additional call is made to addProof, where notice
+ * forceOverwrite is false by default:
+ * - addProof( D, ID_D( ID_A2( ID_B2(), ID_C() ) ) )
+ * where assume ID_B2() and ID_C() prove B and C respectively. This call is
+ * equivalent to calling:
+ * --- addStep( B, ID_B2, {}, {}, true )
+ * --- addStep( C, ID_C, {}, {}, true )
+ * --- addStep( A, ID_A2, {B, C}, {}, true )
+ * --- addStep( D, ID_D, {A}, {}, true )
+ * Afterwards, getProof( D ) returns:
+ *   ID_D( ID_A1( ID_B1(), ID_C() ) )
+ * Notice that the steps with ID_A1 and ID_B1 were not overwritten by this call,
+ * whereas the assumption of C was overwritten by the proof ID_C(). Notice that
+ * the proof of D was completely traversed in addProof, despite encountering
+ * formulas, A and B, that were already given proof steps.
+ *
+ * This class requires a ProofNodeManager object, which is a trusted way of
+ * allocating ProofNode pointers. This manager may have an underlying checker,
+ * although this is not required. It also (optionally) takes a context c.
+ * If no context is provided, then this proof is context-independent. This
+ * is implemented internally by using a dummy context that is never pushed
+ * or popped. The map from Nodes to ProofNodes is context-dependent and is
+ * backtracked when its context backtracks.
+ *
+ * An important invariant of this object is that there exists (at most) one
+ * proof step for each Node. Thus, the ProofNode objects returned by this
+ * class share proofs for common subformulas, as guaranteed by the fact that
+ * Node objects have perfect sharing.
+ */
+class CDProof
+{
+  typedef context::CDHashMap<Node, std::shared_ptr<ProofNode>, NodeHashFunction>
+      NodeProofNodeMap;
+
+ public:
+  CDProof(ProofNodeManager* pnm, context::Context* c = nullptr);
+  ~CDProof();
+  /**
+   * Get proof for fact, or nullptr if it does not exist. Notice that this call
+   * does *not* clone the ProofNode object. Hence, the returned proof may
+   * be updated by further calls to this class. The caller should call
+   * ProofNode::clone if they want to own it.
+   */
+  std::shared_ptr<ProofNode> getProof(Node fact) const;
+  /** Add step
+   *
+   * @param expected The intended conclusion of this proof step. This must be
+   * non-null.
+   * @param id The identifier for the proof step.
+   * @param children The antecendants of the proof step. Each children[i] should
+   * be a fact previously added as a conclusion of an addStep call when
+   * ensureChildren is true.
+   * @param args The arguments of the proof step.
+   * @param ensureChildren Whether we wish to ensure steps have been added
+   * for all nodes in children
+   * @param forceOverwrite Whether we wish to overwrite if a step for expected
+   * was already provided (via a previous call to addStep)
+   * @return The true if indeed the proof step proves expected, or
+   * false otherwise. The latter can happen if the proof has a different (or
+   * invalid) conclusion, or if one of the children does not have a proof and
+   * ensureChildren is true.
+   *
+   * This method may create proofs justified by ASSUME of the facts in
+   * children that have not already been proven when ensureChildren is false.
+   * Notice that ensureChildren should be true if the proof is being
+   * constructed is a strictly eager fashion (bottom up from its leaves), while
+   * ensureChildren should be false if the steps are added lazily or out
+   * of order.
+   *
+   * This method only overwrites proofs for facts that were added as
+   * steps with id ASSUME when forceOverwrite is false, and otherwise always
+   * overwrites an existing step if one was provided when forceOverwrite is
+   * true.
+   */
+  bool addStep(Node expected,
+               PfRule id,
+               const std::vector<Node>& children,
+               const std::vector<Node>& args,
+               bool ensureChildren = false,
+               bool forceOverwrite = false);
+  /** Add proof
+   *
+   * @param pn The proof of the given fact.
+   * @param forceOverwrite Whether we wish to force overwriting if a step was
+   * already provided, for each node in the proof.
+   * @return true if all steps were successfully added to this class. If it
+   * returns true, it registers a copy of all of the subnodes of pn to this
+   * proof class.
+   *
+   * This method is implemented by calling addStep above for all subnodes
+   * of pn, traversed as a dag. This means that fresh ProofNode objects may be
+   * generated by this call, and further modifications to pn does not impact the
+   * internal data of this class.
+   */
+  bool addProof(ProofNode* pn, bool forceOverwrite = false);
+
+ protected:
+  /** The proof manager, used for allocating new ProofNode objects */
+  ProofNodeManager* d_manager;
+  /** A dummy context used by this class if none is provided */
+  context::Context d_context;
+  /** The nodes of the proof */
+  NodeProofNodeMap d_nodes;
+};
+
+}  // namespace CVC4
+
+#endif /* CVC4__EXPR__PROOF_MANAGER_H */