Merge branch 'master' into issue6453issue6453

1 files changed, 258 insertions, 0 deletions

diff --git a/src/proof/proof_node_updater.cpp b/src/proof/proof_node_updater.cpp
new file mode 100644
index 000000000..2bdb54a45
--- /dev/null
+++ b/src/proof/proof_node_updater.cpp
@@ -0,0 +1,258 @@
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Andrew Reynolds, Haniel Barbosa
+ *
+ * This file is part of the cvc5 project.
+ *
+ * Copyright (c) 2009-2021 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.
+ * ****************************************************************************
+ *
+ * Implementation of a utility for updating proof nodes.
+ */
+
+#include "proof/proof_node_updater.h"
+
+#include "proof/lazy_proof.h"
+#include "proof/proof_ensure_closed.h"
+#include "proof/proof_node_algorithm.h"
+#include "proof/proof_node_manager.h"
+
+namespace cvc5 {
+
+ProofNodeUpdaterCallback::ProofNodeUpdaterCallback() {}
+ProofNodeUpdaterCallback::~ProofNodeUpdaterCallback() {}
+
+bool ProofNodeUpdaterCallback::update(Node res,
+                                      PfRule id,
+                                      const std::vector<Node>& children,
+                                      const std::vector<Node>& args,
+                                      CDProof* cdp,
+                                      bool& continueUpdate)
+{
+  return false;
+}
+
+ProofNodeUpdater::ProofNodeUpdater(ProofNodeManager* pnm,
+                                   ProofNodeUpdaterCallback& cb,
+                                   bool mergeSubproofs,
+                                   bool autoSym)
+    : d_pnm(pnm),
+      d_cb(cb),
+      d_debugFreeAssumps(false),
+      d_mergeSubproofs(mergeSubproofs),
+      d_autoSym(autoSym)
+{
+}
+
+void ProofNodeUpdater::process(std::shared_ptr<ProofNode> pf)
+{
+  if (d_debugFreeAssumps)
+  {
+    if (Trace.isOn("pfnu-debug"))
+    {
+      Trace("pfnu-debug2") << "Initial proof: " << *pf.get() << std::endl;
+      Trace("pfnu-debug") << "ProofNodeUpdater::process" << std::endl;
+      Trace("pfnu-debug") << "Expected free assumptions: " << std::endl;
+      for (const Node& fa : d_freeAssumps)
+      {
+        Trace("pfnu-debug") << "- " << fa << std::endl;
+      }
+      std::vector<Node> assump;
+      expr::getFreeAssumptions(pf.get(), assump);
+      Trace("pfnu-debug") << "Current free assumptions: " << std::endl;
+      for (const Node& fa : assump)
+      {
+        Trace("pfnu-debug") << "- " << fa << std::endl;
+      }
+    }
+  }
+  std::vector<std::shared_ptr<ProofNode>> traversing;
+  processInternal(pf, d_freeAssumps, traversing);
+}
+
+void ProofNodeUpdater::processInternal(
+    std::shared_ptr<ProofNode> pf,
+    const std::vector<Node>& fa,
+    std::vector<std::shared_ptr<ProofNode>>& traversing)
+{
+  Trace("pf-process") << "ProofNodeUpdater::process" << std::endl;
+  std::unordered_map<std::shared_ptr<ProofNode>, bool> visited;
+  std::unordered_map<std::shared_ptr<ProofNode>, bool>::iterator it;
+  std::vector<std::shared_ptr<ProofNode>> visit;
+  std::shared_ptr<ProofNode> cur;
+  visit.push_back(pf);
+  std::map<Node, std::shared_ptr<ProofNode>>::iterator itc;
+  // A cache from formulas to proof nodes that are in the current scope.
+  // Notice that we make a fresh recursive call to process if the current
+  // rule is SCOPE below.
+  std::map<Node, std::shared_ptr<ProofNode>> resCache;
+  Node res;
+  do
+  {
+    cur = visit.back();
+    visit.pop_back();
+    it = visited.find(cur);
+    res = cur->getResult();
+    if (it == visited.end())
+    {
+      if (d_mergeSubproofs)
+      {
+        itc = resCache.find(res);
+        if (itc != resCache.end())
+        {
+          // already have a proof, merge it into this one
+          visited[cur] = true;
+          d_pnm->updateNode(cur.get(), itc->second.get());
+          continue;
+        }
+      }
+      // run update to a fixed point
+      bool continueUpdate = true;
+      while (runUpdate(cur, fa, continueUpdate) && continueUpdate)
+      {
+        Trace("pf-process-debug") << "...updated proof." << std::endl;
+      }
+      visited[cur] = !continueUpdate;
+      if (!continueUpdate)
+      {
+        // no further changes should be made to cur according to the callback
+        Trace("pf-process-debug")
+            << "...marked to not continue update." << std::endl;
+        runFinalize(cur, fa, resCache);
+        continue;
+      }
+      traversing.push_back(cur);
+      visit.push_back(cur);
+      // If we are not the top-level proof, we were a scope, or became a scope
+      // after updating, we do a separate recursive call to this method. This
+      // allows us to properly track the assumptions in scope, which is
+      // important for example to merge or to determine updates based on free
+      // assumptions.
+      if (cur->getRule() == PfRule::SCOPE && cur != pf)
+      {
+        std::vector<Node> nfa;
+        nfa.insert(nfa.end(), fa.begin(), fa.end());
+        const std::vector<Node>& args = cur->getArguments();
+        nfa.insert(nfa.end(), args.begin(), args.end());
+        Trace("pfnu-debug2") << "Process new scope with " << args << std::endl;
+        // Process in new call separately
+        processInternal(cur, nfa, traversing);
+        continue;
+      }
+      const std::vector<std::shared_ptr<ProofNode>>& ccp = cur->getChildren();
+      // now, process children
+      for (const std::shared_ptr<ProofNode>& cp : ccp)
+      {
+        if (std::find(traversing.begin(), traversing.end(), cp)
+            != traversing.end())
+        {
+          Unhandled()
+              << "ProofNodeUpdater::processInternal: cyclic proof! (use "
+                 "--proof-eager-checking)"
+              << std::endl;
+        }
+        visit.push_back(cp);
+      }
+    }
+    else if (!it->second)
+    {
+      Assert(!traversing.empty());
+      traversing.pop_back();
+      visited[cur] = true;
+      // finalize the node
+      runFinalize(cur, fa, resCache);
+    }
+  } while (!visit.empty());
+  Trace("pf-process") << "ProofNodeUpdater::process: finished" << std::endl;
+}
+
+bool ProofNodeUpdater::runUpdate(std::shared_ptr<ProofNode> cur,
+                                 const std::vector<Node>& fa,
+                                 bool& continueUpdate)
+{
+  // should it be updated?
+  if (!d_cb.shouldUpdate(cur, fa, continueUpdate))
+  {
+    return false;
+  }
+  PfRule id = cur->getRule();
+  // use CDProof to open a scope for which the callback updates
+  CDProof cpf(d_pnm, nullptr, "ProofNodeUpdater::CDProof", d_autoSym);
+  const std::vector<std::shared_ptr<ProofNode>>& cc = cur->getChildren();
+  std::vector<Node> ccn;
+  for (const std::shared_ptr<ProofNode>& cp : cc)
+  {
+    Node cpres = cp->getResult();
+    ccn.push_back(cpres);
+    // store in the proof
+    cpf.addProof(cp);
+  }
+  Node res = cur->getResult();
+  Trace("pf-process-debug")
+      << "Updating (" << cur->getRule() << "): " << res << std::endl;
+  // only if the callback updated the node
+  if (d_cb.update(res, id, ccn, cur->getArguments(), &cpf, continueUpdate))
+  {
+    std::shared_ptr<ProofNode> npn = cpf.getProofFor(res);
+    std::vector<Node> fullFa;
+    if (d_debugFreeAssumps)
+    {
+      expr::getFreeAssumptions(cur.get(), fullFa);
+      Trace("pfnu-debug") << "Original proof : " << *cur << std::endl;
+    }
+    // then, update the original proof node based on this one
+    Trace("pf-process-debug") << "Update node..." << std::endl;
+    d_pnm->updateNode(cur.get(), npn.get());
+    Trace("pf-process-debug") << "...update node finished." << std::endl;
+    if (d_debugFreeAssumps)
+    {
+      fullFa.insert(fullFa.end(), fa.begin(), fa.end());
+      // We have that npn is a node we occurring the final updated version of
+      // the proof. We can now debug based on the expected set of free
+      // assumptions.
+      Trace("pfnu-debug") << "Ensure update closed..." << std::endl;
+      pfnEnsureClosedWrt(
+          npn.get(), fullFa, "pfnu-debug", "ProofNodeUpdater:postupdate");
+    }
+    Trace("pf-process-debug") << "..finished" << std::endl;
+    return true;
+  }
+  Trace("pf-process-debug") << "..finished" << std::endl;
+  return false;
+}
+
+void ProofNodeUpdater::runFinalize(
+    std::shared_ptr<ProofNode> cur,
+    const std::vector<Node>& fa,
+    std::map<Node, std::shared_ptr<ProofNode>>& resCache)
+{
+  if (d_mergeSubproofs)
+  {
+    Node res = cur->getResult();
+    // cache result if we are merging subproofs
+    resCache[res] = cur;
+  }
+  if (d_debugFreeAssumps)
+  {
+    // We have that npn is a node we occurring the final updated version of
+    // the proof. We can now debug based on the expected set of free
+    // assumptions.
+    Trace("pfnu-debug") << "Ensure update closed..." << std::endl;
+    pfnEnsureClosedWrt(
+        cur.get(), fa, "pfnu-debug", "ProofNodeUpdater:finalize");
+  }
+}
+
+void ProofNodeUpdater::setDebugFreeAssumptions(
+    const std::vector<Node>& freeAssumps)
+{
+  d_freeAssumps.clear();
+  d_freeAssumps.insert(
+      d_freeAssumps.end(), freeAssumps.begin(), freeAssumps.end());
+  d_debugFreeAssumps = true;
+}
+
+}  // namespace cvc5