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.

1 files changed, 162 insertions, 0 deletions

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