(proof-new) Add the term conversion sequence generator (#5097)

This class will be used in the theory preprocessor and is planned to be used in other preprocessing passes that can be understood as sequences of rewrite systems.

5 files changed, 309 insertions, 0 deletions

diff --git a/src/expr/CMakeLists.txt b/src/expr/CMakeLists.txt
index 1cc4e9a33..8742612ad 100644
--- a/src/expr/CMakeLists.txt
+++ b/src/expr/CMakeLists.txt
@@ -75,6 +75,8 @@ libcvc4_add_sources(
   skolem_manager.h
   symbol_table.cpp
   symbol_table.h
+  tconv_seq_proof_generator.cpp
+  tconv_seq_proof_generator.h
   term_canonize.cpp
   term_canonize.h
   term_context.cpp
diff --git a/src/expr/proof_node_manager.cpp b/src/expr/proof_node_manager.cpp
index eb298cc83..9f60a49e4 100644
--- a/src/expr/proof_node_manager.cpp
+++ b/src/expr/proof_node_manager.cpp
@@ -56,6 +56,18 @@ std::shared_ptr<ProofNode> ProofNodeManager::mkAssume(Node fact)
   return mkNode(PfRule::ASSUME, {}, {fact}, fact);
 }
 
+std::shared_ptr<ProofNode> ProofNodeManager::mkTrans(
+    const std::vector<std::shared_ptr<ProofNode>>& children, Node expected)
+{
+  Assert(!children.empty());
+  if (children.size() == 1)
+  {
+    Assert(expected.isNull() || children[0]->getResult() == expected);
+    return children[0];
+  }
+  return mkNode(PfRule::TRANS, children, {}, expected);
+}
+
 std::shared_ptr<ProofNode> ProofNodeManager::mkScope(
     std::shared_ptr<ProofNode> pf,
     std::vector<Node>& assumps,
diff --git a/src/expr/proof_node_manager.h b/src/expr/proof_node_manager.h
index 47fdf3ebd..7d7993146 100644
--- a/src/expr/proof_node_manager.h
+++ b/src/expr/proof_node_manager.h
@@ -81,6 +81,15 @@ class ProofNodeManager
    */
   std::shared_ptr<ProofNode> mkAssume(Node fact);
   /**
+   * Make transitivity proof, where children contains one or more proofs of
+   * equalities that form an ordered chain. In other words, the vector children
+   * is a legal set of children for an application of TRANS.
+   */
+  std::shared_ptr<ProofNode> mkTrans(
+      const std::vector<std::shared_ptr<ProofNode>>& children,
+      Node expected = Node::null());
+
+  /**
    * Make scope having body pf and arguments (assumptions-to-close) assumps.
    * If ensureClosed is true, then this method throws an assertion failure if
    * the returned proof is not closed. This is the case if a free assumption
diff --git a/src/expr/tconv_seq_proof_generator.cpp b/src/expr/tconv_seq_proof_generator.cpp
new file mode 100644
index 000000000..b22170b38
--- /dev/null
+++ b/src/expr/tconv_seq_proof_generator.cpp
@@ -0,0 +1,167 @@
+/*********************                                                        */
+/*! \file tconv_seq_proof_generator.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2020 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 sequence proof generator utility
+ **/
+
+#include "expr/tconv_seq_proof_generator.h"
+
+namespace CVC4 {
+
+TConvSeqProofGenerator::TConvSeqProofGenerator(
+    ProofNodeManager* pnm,
+    const std::vector<ProofGenerator*>& ts,
+    context::Context* c,
+    std::string name)
+    : d_pnm(pnm), d_converted(c), d_name(name)
+{
+  d_tconvs.insert(d_tconvs.end(), ts.begin(), ts.end());
+  AlwaysAssert(!d_tconvs.empty())
+      << "TConvSeqProofGenerator::TConvSeqProofGenerator: expecting non-empty "
+         "sequence";
+}
+
+TConvSeqProofGenerator::~TConvSeqProofGenerator() {}
+
+void TConvSeqProofGenerator::registerConvertedTerm(Node t, Node s, size_t index)
+{
+  if (t == s)
+  {
+    // no need
+    return;
+  }
+  std::pair<Node, size_t> key = std::pair<Node, size_t>(t, index);
+  d_converted[key] = s;
+}
+
+std::shared_ptr<ProofNode> TConvSeqProofGenerator::getProofFor(Node f)
+{
+  Trace("tconv-seq-pf-gen")
+      << "TConvSeqProofGenerator::getProofFor: " << identify() << ": " << f
+      << std::endl;
+  return getSubsequenceProofFor(f, 0, d_tconvs.size() - 1);
+}
+
+std::shared_ptr<ProofNode> TConvSeqProofGenerator::getSubsequenceProofFor(
+    Node f, size_t start, size_t end)
+{
+  Assert(end < d_tconvs.size());
+  if (f.getKind() != kind::EQUAL)
+  {
+    std::stringstream serr;
+    serr << "TConvSeqProofGenerator::getProofFor: " << identify()
+         << ": fail, non-equality " << f;
+    Unhandled() << serr.str();
+    Trace("tconv-seq-pf-gen") << serr.str() << std::endl;
+    return nullptr;
+  }
+  // start with the left hand side of the equality
+  Node curr = f[0];
+  // proofs forming transitivity chain
+  std::vector<std::shared_ptr<ProofNode>> transChildren;
+  std::pair<Node, size_t> currKey;
+  NodeIndexNodeMap::iterator itc;
+  // convert the term in sequence
+  for (size_t i = start; i <= end; i++)
+  {
+    currKey = std::pair<Node, size_t>(curr, i);
+    itc = d_converted.find(currKey);
+    // if we provided a conversion at this index via registerConvertedTerm
+    if (itc != d_converted.end())
+    {
+      Node next = (*itc).second;
+      Trace("tconv-seq-pf-gen") << "...convert to " << next << std::endl;
+      Node eq = curr.eqNode(next);
+      std::shared_ptr<ProofNode> pf = d_tconvs[i]->getProofFor(eq);
+      transChildren.push_back(pf);
+      curr = next;
+    }
+  }
+  // should end up with the right hand side of the equality
+  if (curr != f[1])
+  {
+    // unexpected
+    std::stringstream serr;
+    serr << "TConvSeqProofGenerator::getProofFor: " << identify()
+         << ": failed, mismatch (see -t tconv-seq-pf-gen-debug for details)"
+         << std::endl;
+    serr << "                    source: " << f[0] << std::endl;
+    serr << "expected after conversions: " << f[1] << std::endl;
+    serr << "  actual after conversions: " << curr << std::endl;
+
+    if (Trace.isOn("tconv-seq-pf-gen-debug"))
+    {
+      Trace("tconv-pf-gen-debug")
+          << "Printing conversion steps..." << std::endl;
+      serr << "Conversions: " << std::endl;
+      for (NodeIndexNodeMap::const_iterator it = d_converted.begin();
+           it != d_converted.end();
+           ++it)
+      {
+        serr << "(" << (*it).first.first << ", " << (*it).first.second
+             << ") -> " << (*it).second << std::endl;
+      }
+    }
+    Unhandled() << serr.str();
+    return nullptr;
+  }
+  // otherwise, make transitivity
+  return d_pnm->mkTrans(transChildren, f);
+}
+
+theory::TrustNode TConvSeqProofGenerator::mkTrustRewriteSequence(
+    const std::vector<Node>& cterms)
+{
+  Assert(cterms.size() == d_tconvs.size() + 1);
+  if (cterms[0] == cterms[cterms.size() - 1])
+  {
+    return theory::TrustNode::null();
+  }
+  bool useThis = false;
+  ProofGenerator* pg = nullptr;
+  for (size_t i = 0, nconvs = d_tconvs.size(); i < nconvs; i++)
+  {
+    if (cterms[i] == cterms[i + 1])
+    {
+      continue;
+    }
+    else if (pg == nullptr)
+    {
+      // Maybe the i^th generator can explain it alone, which must be the case
+      // if there is only one position in the sequence where the term changes.
+      // We may overwrite pg with this class if another step is encountered in
+      // this loop.
+      pg = d_tconvs[i];
+    }
+    else
+    {
+      // need more than a single generator, use this class
+      useThis = true;
+      break;
+    }
+  }
+  if (useThis)
+  {
+    pg = this;
+    // if more than two steps, we must register each conversion step
+    for (size_t i = 0, nconvs = d_tconvs.size(); i < nconvs; i++)
+    {
+      registerConvertedTerm(cterms[i], cterms[i + 1], i);
+    }
+  }
+  Assert(pg != nullptr);
+  return theory::TrustNode::mkTrustRewrite(
+      cterms[0], cterms[cterms.size() - 1], pg);
+}
+
+std::string TConvSeqProofGenerator::identify() const { return d_name; }
+
+}  // namespace CVC4
diff --git a/src/expr/tconv_seq_proof_generator.h b/src/expr/tconv_seq_proof_generator.h
new file mode 100644
index 000000000..95499d6b8
--- /dev/null
+++ b/src/expr/tconv_seq_proof_generator.h
@@ -0,0 +1,119 @@
+/*********************                                                        */
+/*! \file tconv_seq_proof_generator.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2020 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 sequence proof generator utility
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef CVC4__EXPR__TCONV_SEQ_PROOF_GENERATOR_H
+#define CVC4__EXPR__TCONV_SEQ_PROOF_GENERATOR_H
+
+#include "context/cdhashmap.h"
+#include "expr/node.h"
+#include "expr/proof_generator.h"
+#include "expr/proof_node_manager.h"
+#include "theory/trust_node.h"
+
+namespace CVC4 {
+
+/**
+ * The term conversion sequence proof generator. This is used for maintaining
+ * a fixed sequence of proof generators that provide proofs for rewrites
+ * (equalities). We call these the "component generators" of this sequence,
+ * which are typically TConvProofGenerator.
+ */
+class TConvSeqProofGenerator : public ProofGenerator
+{
+ public:
+  /**
+   * @param pnm The proof node manager for constructing ProofNode objects.
+   * @param ts The list of component term conversion generators that are
+   * applied in sequence
+   * @param c The context that this class depends on. If none is provided,
+   * this class is context-independent.
+   * @param name The name of this generator (for debugging).
+   */
+  TConvSeqProofGenerator(ProofNodeManager* pnm,
+                         const std::vector<ProofGenerator*>& ts,
+                         context::Context* c = nullptr,
+                         std::string name = "TConvSeqProofGenerator");
+  ~TConvSeqProofGenerator();
+  /**
+   * Indicate that the index^th proof generator converts term t to s. This
+   * should be called for a unique s for each (t, index). It must be the
+   * case that d_tconv[index] can provide a proof for t = s in the remainder
+   * of the context maintained by this class.
+   */
+  void registerConvertedTerm(Node t, Node s, size_t index);
+  /**
+   * Get the proof for formula f. It should be the case that f is of the form
+   * t_0 = t_n, where it must be the case that t_n is obtained by the following:
+   * For each i=0, ... n, let t_{i+1} be the term such that
+   *   registerConvertedTerm(t_i, t_{i+1}, i)
+   * was called. Otherwise t_{i+1} = t_i.
+   * In other words, t_n is obtained by converting t_0, in order, based on the
+   * calls to registerConvertedTerm.
+   *
+   * @param f The equality fact to get the proof for.
+   * @return The proof for f.
+   */
+  std::shared_ptr<ProofNode> getProofFor(Node f) override;
+  /**
+   * Get subsequence proof for f, with given start and end steps (inclusive).
+   */
+  std::shared_ptr<ProofNode> getSubsequenceProofFor(Node f,
+                                                    size_t start,
+                                                    size_t end);
+  /** Identify this generator (for debugging, etc..) */
+  std::string identify() const override;
+
+  /**
+   * Make trust node from a sequence of converted terms. The number of
+   * terms in cterms should be 1 + the number of component proof generators
+   * maintained by this class. This selects a proof generator that is capable
+   * of proving cterms[0] = cterms[cterms.size()-1], which is either this
+   * generator, or one of the component proof generators, if only one step
+   * rewrote. In the former case, all steps are registered to this class.
+   * Using a component generator is an optimization that saves having to
+   * save the conversion steps or use this class. For example, if we have 2 
+   * term conversion components, and call this method on:
+   *   { a, b, c }
+   * then this method calls:
+   *   registerConvertedTerm( a, b, 0 )
+   *   registerConvertedTerm( b, c, 1 )
+   * and returns a trust node proving (= a c) with this class as the proof
+   * generator. On the other hand, if we call this method on:
+   *   { d, d, e }
+   * then we return a trust node proving (= d e) with the 2nd component proof
+   * generator, as it alone is capable of proving this equality.
+   */
+  theory::TrustNode mkTrustRewriteSequence(const std::vector<Node>& cterms);
+
+ protected:
+  using NodeIndexPairHashFunction =
+      PairHashFunction<Node, size_t, NodeHashFunction>;
+  typedef context::
+      CDHashMap<std::pair<Node, size_t>, Node, NodeIndexPairHashFunction>
+          NodeIndexNodeMap;
+  /** The proof node manager */
+  ProofNodeManager* d_pnm;
+  /** The term conversion generators */
+  std::vector<ProofGenerator*> d_tconvs;
+  /** the set of converted terms */
+  NodeIndexNodeMap d_converted;
+  /** Name identifier */
+  std::string d_name;
+};
+
+}  // namespace CVC4
+
+#endif /* CVC4__EXPR__TCONV_SEQ_PROOF_GENERATOR_H */