(proof-new) Term conversion proof generator utility (#4603)

This utility is used for constructing any proof where a term is "converted" into another by small step rewrites. This utility will be used to construct the skeleton of the proofs of rewrites, preprocessing steps, expand definitions, results of substitutions, and so on.

3 files changed, 375 insertions, 0 deletions

diff --git a/src/expr/CMakeLists.txt b/src/expr/CMakeLists.txt
index 3d74d0bad..00eeaecea 100644
--- a/src/expr/CMakeLists.txt
+++ b/src/expr/CMakeLists.txt
@@ -61,6 +61,8 @@ libcvc4_add_sources(
   symbol_table.h
   term_canonize.cpp
   term_canonize.h
+  term_conversion_proof_generator.cpp
+  term_conversion_proof_generator.h
   type.cpp
   type.h
   type_checker.h
diff --git a/src/expr/term_conversion_proof_generator.cpp b/src/expr/term_conversion_proof_generator.cpp
new file mode 100644
index 000000000..59faaf632
--- /dev/null
+++ b/src/expr/term_conversion_proof_generator.cpp
@@ -0,0 +1,250 @@
+/*********************                                                        */
+/*! \file term_conversion_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 term conversion proof generator utility
+ **/
+
+#include "expr/term_conversion_proof_generator.h"
+
+using namespace CVC4::kind;
+
+namespace CVC4 {
+
+TConvProofGenerator::TConvProofGenerator(ProofNodeManager* pnm,
+                                         context::Context* c)
+    : d_proof(pnm, nullptr, c), d_rewriteMap(c ? c : &d_context)
+{
+}
+
+TConvProofGenerator::~TConvProofGenerator() {}
+
+void TConvProofGenerator::addRewriteStep(Node t, Node s, ProofGenerator* pg)
+{
+  // should not rewrite term more than once
+  Assert(!hasRewriteStep(t));
+  Node eq = t.eqNode(s);
+  d_proof.addLazyStep(eq, pg);
+  d_rewriteMap[t] = s;
+}
+
+void TConvProofGenerator::addRewriteStep(Node t, Node s, ProofStep ps)
+{
+  // should not rewrite term more than once
+  Assert(!hasRewriteStep(t));
+  Node eq = t.eqNode(s);
+  d_proof.addStep(eq, ps);
+  d_rewriteMap[t] = s;
+}
+
+void TConvProofGenerator::addRewriteStep(Node t,
+                                         Node s,
+                                         PfRule id,
+                                         const std::vector<Node>& children,
+                                         const std::vector<Node>& args)
+{
+  // should not rewrite term more than once
+  Assert(!hasRewriteStep(t));
+  Node eq = t.eqNode(s);
+  d_proof.addStep(eq, id, children, args);
+  d_rewriteMap[t] = s;
+}
+
+bool TConvProofGenerator::hasRewriteStep(Node t) const
+{
+  return !getRewriteStep(t).isNull();
+}
+
+std::shared_ptr<ProofNode> TConvProofGenerator::getProofFor(Node f)
+{
+  Trace("tconv-pf-gen") << "TConvProofGenerator::getProofFor: " << f
+                        << std::endl;
+  if (f.getKind() != EQUAL)
+  {
+    Trace("tconv-pf-gen") << "... fail, non-equality" << std::endl;
+    Assert(false);
+    return nullptr;
+  }
+  std::shared_ptr<ProofNode> pf = getProofForRewriting(f[0]);
+  if (pf == nullptr)
+  {
+    // failed to generate proof
+    Trace("tconv-pf-gen") << "...failed to get proof" << std::endl;
+    Assert(false);
+    return pf;
+  }
+  if (pf->getResult() != f)
+  {
+    Trace("tconv-pf-gen") << "...failed, mismatch: returned proof concludes "
+                          << pf->getResult() << std::endl;
+    Assert(false);
+    return nullptr;
+  }
+  Trace("tconv-pf-gen") << "... success" << std::endl;
+  return pf;
+}
+
+std::shared_ptr<ProofNode> TConvProofGenerator::getProofForRewriting(Node t)
+{
+  // we use the existing proofs
+  PRefProofGenerator prg(&d_proof);
+  LazyCDProof pf(d_proof.getManager(), &prg);
+  NodeManager* nm = NodeManager::currentNM();
+  // Invariant: if visited[t] = s or rewritten[t] = s and t,s are distinct,
+  // then pf is able to generate a proof of t=s.
+  // the final rewritten form of terms
+  std::unordered_map<TNode, Node, TNodeHashFunction> visited;
+  // the rewritten form of terms we have processed so far
+  std::unordered_map<TNode, Node, TNodeHashFunction> rewritten;
+  std::unordered_map<TNode, Node, TNodeHashFunction>::iterator it;
+  std::unordered_map<TNode, Node, TNodeHashFunction>::iterator itr;
+  std::vector<TNode> visit;
+  TNode cur;
+  visit.push_back(t);
+  do
+  {
+    cur = visit.back();
+    visit.pop_back();
+    it = visited.find(cur);
+
+    if (it == visited.end())
+    {
+      visited[cur] = Node::null();
+      // did we rewrite the current node (possibly at pre-rewrite)?
+      Node rcur = getRewriteStep(cur);
+      if (!rcur.isNull())
+      {
+        // d_proof should have a proof of cur = rcur. Hence there is nothing
+        // to do here, as pf will reference prg to get the proof from d_proof.
+        // It may be the case that rcur also rewrites, thus we cannot assign
+        // the final rewritten form for cur yet. Instead we revisit cur after
+        // finishing visiting rcur.
+        rewritten[cur] = rcur;
+        visit.push_back(cur);
+        visit.push_back(rcur);
+      }
+      else
+      {
+        visit.push_back(cur);
+        visit.insert(visit.end(), cur.begin(), cur.end());
+      }
+    }
+    else if (it->second.isNull())
+    {
+      itr = rewritten.find(cur);
+      if (itr != rewritten.end())
+      {
+        // if it was rewritten, check the status of the rewritten node,
+        // which should be finished now
+        Node rcur = itr->second;
+        Assert(cur != rcur);
+        // the final rewritten form of cur is the final form of rcur
+        Node rcurFinal = visited[rcur];
+        if (rcurFinal != rcur)
+        {
+          // must connect via TRANS
+          std::vector<Node> pfChildren;
+          pfChildren.push_back(cur.eqNode(rcur));
+          pfChildren.push_back(rcur.eqNode(rcurFinal));
+          Node result = cur.eqNode(rcurFinal);
+          pf.addStep(result, PfRule::TRANS, pfChildren, {});
+        }
+        visited[cur] = rcurFinal;
+      }
+      else
+      {
+        Node ret = cur;
+        bool childChanged = false;
+        std::vector<Node> children;
+        if (cur.getMetaKind() == metakind::PARAMETERIZED)
+        {
+          children.push_back(cur.getOperator());
+        }
+        for (const Node& cn : cur)
+        {
+          it = visited.find(cn);
+          Assert(it != visited.end());
+          Assert(!it->second.isNull());
+          childChanged = childChanged || cn != it->second;
+          children.push_back(it->second);
+        }
+        if (childChanged)
+        {
+          ret = nm->mkNode(cur.getKind(), children);
+          rewritten[cur] = ret;
+          // congruence to show (cur = ret)
+          std::vector<Node> pfChildren;
+          for (size_t i = 0, size = cur.getNumChildren(); i < size; i++)
+          {
+            if (cur[i] == ret[i])
+            {
+              // ensure REFL proof for unchanged children
+              pf.addStep(cur[i].eqNode(cur[i]), PfRule::REFL, {}, {cur[i]});
+            }
+            pfChildren.push_back(cur[i].eqNode(ret[i]));
+          }
+          std::vector<Node> pfArgs;
+          Kind k = cur.getKind();
+          if (kind::metaKindOf(k) == kind::metakind::PARAMETERIZED)
+          {
+            pfArgs.push_back(cur.getOperator());
+          }
+          else
+          {
+            pfArgs.push_back(nm->operatorOf(k));
+          }
+          Node result = cur.eqNode(ret);
+          pf.addStep(result, PfRule::CONG, pfChildren, pfArgs);
+        }
+        // did we rewrite ret (at post-rewrite)?
+        Node rret = getRewriteStep(ret);
+        if (!rret.isNull())
+        {
+          if (cur != ret)
+          {
+            visit.push_back(cur);
+          }
+          // d_proof should have a proof of ret = rret, hence nothing to do
+          // here, for the same reasons as above. It also may be the case that
+          // rret rewrites, hence we must revisit ret.
+          rewritten[ret] = rret;
+          visit.push_back(ret);
+          visit.push_back(rret);
+        }
+        else
+        {
+          // it is final
+          visited[cur] = ret;
+        }
+      }
+    }
+  } while (!visit.empty());
+  Assert(visited.find(t) != visited.end());
+  Assert(!visited.find(t)->second.isNull());
+  // make the overall proof
+  Node teq = t.eqNode(visited[t]);
+  return pf.mkProof(teq);
+}
+
+Node TConvProofGenerator::getRewriteStep(Node t) const
+{
+  NodeNodeMap::const_iterator it = d_rewriteMap.find(t);
+  if (it == d_rewriteMap.end())
+  {
+    return Node::null();
+  }
+  return (*it).second;
+}
+std::string TConvProofGenerator::identify() const
+{
+  return "TConvProofGenerator";
+}
+
+}  // namespace CVC4
diff --git a/src/expr/term_conversion_proof_generator.h b/src/expr/term_conversion_proof_generator.h
new file mode 100644
index 000000000..2af4250d2
--- /dev/null
+++ b/src/expr/term_conversion_proof_generator.h
@@ -0,0 +1,123 @@
+/*********************                                                        */
+/*! \file term_conversion_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 Term conversion proof generator utility
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef CVC4__EXPR__TERM_CONVERSION_PROOF_GENERATOR_H
+#define CVC4__EXPR__TERM_CONVERSION_PROOF_GENERATOR_H
+
+#include "context/cdhashmap.h"
+#include "expr/lazy_proof.h"
+#include "expr/proof_generator.h"
+#include "expr/proof_node_manager.h"
+
+namespace CVC4 {
+
+/**
+ * The term conversion proof generator.
+ *
+ * This class is used for proofs of t = t', where t' is obtained from t by
+ * applying (context-free) small step rewrites on subterms of t. Its main
+ * interface functions are:
+ * (1) addRewriteStep(t,s,<justification>) which notifies this class that t
+ * rewrites to s, where justification is either a proof generator or proof
+ * step,
+ * (2) getProofFor(f) where f is any equality that can be justified by the
+ * rewrite steps given above.
+ *
+ * For example, say we make the following calls:
+ *   addRewriteStep(a,b,P1)
+ *   addRewriteStep(f(a),c,P2)
+ *   addRewriteStep(c,d,P3)
+ * where P1 and P2 are proof steps. Afterwards, this class may justify any
+ * equality t = s where s is obtained by applying the rewrites a->b, f(a)->c,
+ * c->d, based on the strategy outlined below [***]. For example, the call to:
+ *   getProofFor(g(f(a),h(a),f(e)) = g(d,h(b),f(e)))
+ * will return the proof:
+ *   CONG(
+ *     TRANS(P2,P3),     ; f(a)=d
+ *     CONG(P1 :args h), ; h(a)=h(b)
+ *     REFL(:args f(e))  ; f(e)=f(e)
+ *   :args g)
+ *
+ * [***] This class traverses the left hand side of a given equality-to-prove
+ * (the term g(f(a),h(a),e) in the above example) and "replays" the rewrite
+ * steps to obtain its rewritten form. To do so, it applies any available
+ * rewrite step both at pre-rewrite (pre-order traversal) and post-rewrite
+ * (post-order traversal). It thus does not require the user of this class to
+ * distinguish whether a rewrite is a pre-rewrite or a post-rewrite during
+ * addRewriteStep. In particular, notice that in the above example, we realize
+ * that f(a) --> c at pre-rewrite instead of post-rewriting a --> b and then
+ * ending with f(a)=f(b).
+ */
+class TConvProofGenerator : public ProofGenerator
+{
+ public:
+  /** Constructor
+   *
+   * @param pnm The proof node manager for constructing ProofNode objects.
+   * @param c The context that this class depends on. If none is provided,
+   * this class is context-independent.
+   */
+  TConvProofGenerator(ProofNodeManager* pnm, context::Context* c = nullptr);
+  ~TConvProofGenerator();
+  /**
+   * Add rewrite step t --> s based on proof generator.
+   */
+  void addRewriteStep(Node t, Node s, ProofGenerator* pg);
+  /** Same as above, for a single step */
+  void addRewriteStep(Node t, Node s, ProofStep ps);
+  /** Same as above, with explicit arguments */
+  void addRewriteStep(Node t,
+                      Node s,
+                      PfRule id,
+                      const std::vector<Node>& children,
+                      const std::vector<Node>& args);
+  /** Has rewrite step for term t */
+  bool hasRewriteStep(Node t) const;
+  /** 
+   * Get rewrite step for term t, returns the s provided in a call to
+   * addRewriteStep if one exists, or null otherwise.
+   */
+  Node getRewriteStep(Node t) const;
+  /**
+   * Get the proof for formula f. It should be the case that f is of the form
+   * t = t', where t' is the result of rewriting t based on the rewrite steps
+   * registered to this class.
+   *
+   * @param f The fact to get the proof for.
+   * @return The proof for f.
+   */
+  std::shared_ptr<ProofNode> getProofFor(Node f) override;
+  /** Identify this generator (for debugging, etc..) */
+  std::string identify() const override;
+
+ protected:
+  typedef context::CDHashMap<Node, Node, NodeHashFunction> NodeNodeMap;
+  /** A dummy context used by this class if none is provided */
+  context::Context d_context;
+  /** The (lazy) context dependent proof object. */
+  LazyCDProof d_proof;
+  /** map to rewritten forms */
+  NodeNodeMap d_rewriteMap;
+  /**
+   * Get the proof for term t. Returns a proof of t = t' where t' is the
+   * result of rewriting t based on the rewrite steps registered to this class.
+   */
+  std::shared_ptr<ProofNode> getProofForRewriting(Node t);
+};
+
+}  // namespace CVC4
+
+#endif /* CVC4__EXPR__TERM_CONVERSION_PROOF_GENERATOR_H */