(proof-new) Adding API for converting EqProof into ProofNode (#4747)

Also puts EqProof into its own module. Next will come the implementation of the API.

5 files changed, 475 insertions, 92 deletions

diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index 28d943ced..a19580c00 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -785,6 +785,8 @@ libcvc4_add_sources(
   theory/uf/equality_engine.cpp
   theory/uf/equality_engine.h
   theory/uf/equality_engine_types.h
+  theory/uf/eq_proof.cpp
+  theory/uf/eq_proof.h
   theory/uf/proof_checker.cpp
   theory/uf/proof_checker.h
   theory/uf/ho_extension.cpp
diff --git a/src/theory/uf/eq_proof.cpp b/src/theory/uf/eq_proof.cpp
new file mode 100644
index 000000000..3a60d246e
--- /dev/null
+++ b/src/theory/uf/eq_proof.cpp
@@ -0,0 +1,129 @@
+/*********************                                                        */
+/*! \file eq_proof.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Haniel Barbosa
+ ** 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 Implementation of a proof as produced by the equality engine.
+ **
+ **/
+
+#include "theory/uf/eq_proof.h"
+
+#include "expr/proof.h"
+
+namespace CVC4 {
+namespace theory {
+namespace eq {
+
+void EqProof::debug_print(const char* c,
+                          unsigned tb,
+                          PrettyPrinter* prettyPrinter) const
+{
+  std::stringstream ss;
+  debug_print(ss, tb, prettyPrinter);
+  Debug(c) << ss.str();
+}
+
+void EqProof::debug_print(std::ostream& os,
+                          unsigned tb,
+                          PrettyPrinter* prettyPrinter) const
+{
+  for (unsigned i = 0; i < tb; i++)
+  {
+    os << "  ";
+  }
+
+  if (prettyPrinter)
+  {
+    os << prettyPrinter->printTag(d_id);
+  }
+  else
+  {
+    os << static_cast<MergeReasonType>(d_id);
+  }
+  os << "(";
+  if (d_children.empty() && d_node.isNull())
+  {
+    os << ")";
+    return;
+  }
+  if (!d_node.isNull())
+  {
+    os << std::endl;
+    for (unsigned i = 0; i < tb + 1; ++i)
+    {
+      os << "  ";
+    }
+    os << d_node << (!d_children.empty() ? "," : "");
+  }
+  unsigned size = d_children.size();
+  for (unsigned i = 0; i < size; ++i)
+  {
+    os << std::endl;
+    d_children[i]->debug_print(os, tb + 1, prettyPrinter);
+    if (i < size - 1)
+    {
+      for (unsigned j = 0; j < tb + 1; ++j)
+      {
+        os << "  ";
+      }
+      os << ",";
+    }
+  }
+  if (size > 0)
+  {
+    for (unsigned i = 0; i < tb; ++i)
+    {
+      os << "  ";
+    }
+  }
+  os << ")" << std::endl;
+}
+
+void EqProof::cleanReflPremises(std::vector<Node>& premises) const {}
+
+bool EqProof::expandTransitivityForDisequalities(
+    Node conclusion,
+    std::vector<Node>& premises,
+    CDProof* p,
+    std::unordered_set<Node, NodeHashFunction>& assumptions) const
+{
+  return false;
+}
+
+bool EqProof::buildTransitivityChain(Node conclusion,
+                                     std::vector<Node>& premises) const
+{
+  return false;
+}
+
+void EqProof::reduceNestedCongruence(
+    unsigned i,
+    Node conclusion,
+    std::vector<std::vector<Node>>& transitivityMatrix,
+    CDProof* p,
+    std::unordered_map<Node, Node, NodeHashFunction>& visited,
+    std::unordered_set<Node, NodeHashFunction>& assumptions,
+    bool isNary) const
+{
+}
+
+Node EqProof::addToProof(CDProof* p) const { return Node::null(); }
+
+Node EqProof::addToProof(
+    CDProof* p,
+    std::unordered_map<Node, Node, NodeHashFunction>& visited,
+    std::unordered_set<Node, NodeHashFunction>& assumptions) const
+{
+  return Node::null();
+}
+
+}  // namespace eq
+}  // Namespace theory
+}  // Namespace CVC4
diff --git a/src/theory/uf/eq_proof.h b/src/theory/uf/eq_proof.h
new file mode 100644
index 000000000..c396da313
--- /dev/null
+++ b/src/theory/uf/eq_proof.h
@@ -0,0 +1,340 @@
+/*********************                                                        */
+/*! \file eq_proof.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Haniel Barbosa
+ ** 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 A proof as produced by the equality engine.
+ **
+ **/
+
+#include "cvc4_private.h"
+#include "expr/node.h"
+#include "theory/uf/equality_engine_types.h"
+
+namespace CVC4 {
+
+class CDProof;
+
+namespace theory {
+namespace eq {
+
+/**
+ * An equality proof.
+ *
+ * This represents the reasoning performed by the Equality Engine to derive
+ * facts, represented in terms of the rules in MergeReasonType. Each proof step
+ * is annotated with the rule id, the conclusion node and a vector of proofs of
+ * the rule's premises.
+ **/
+class EqProof
+{
+ public:
+  /** A custom pretty printer used for custom rules being those in
+   * MergeReasonType. */
+  class PrettyPrinter
+  {
+   public:
+    virtual ~PrettyPrinter() {}
+    virtual std::string printTag(unsigned tag) = 0;
+  };
+
+  EqProof() : d_id(MERGED_THROUGH_REFLEXIVITY) {}
+  /** The proof rule for concluding d_node */
+  unsigned d_id;
+  /** The conclusion of this EqProof */
+  Node d_node;
+  /** The proofs of the premises for deriving d_node with d_id */
+  std::vector<std::shared_ptr<EqProof>> d_children;
+  /**
+   * Debug print this proof on debug trace c with tabulation tb and pretty
+   * printer prettyPrinter.
+   */
+  void debug_print(const char* c,
+                   unsigned tb = 0,
+                   PrettyPrinter* prettyPrinter = nullptr) const;
+  /**
+   * Debug print this proof on output stream os with tabulation tb and pretty
+   * printer prettyPrinter.
+   */
+  void debug_print(std::ostream& os,
+                   unsigned tb = 0,
+                   PrettyPrinter* prettyPrinter = nullptr) const;
+
+  /** Add to proof
+   *
+   * Converts EqProof into ProofNode via a series of steps to be stored in
+   * CDProof* p.
+   *
+   * This method can be seen as a best-effort solution until the EqualityEngine
+   * is updated to produce ProofNodes directly, if ever. Note that since the
+   * original EqProof steps can be coarse-grained (e.g. without proper order,
+   * implicit inferences related to disequelaties) and are phrased over curried
+   * terms, the transformation requires significant, although cheap (mostly
+   * linear on the DAG-size of EqProof), post-processing.
+   *
+   * An important invariant of the resulting ProofNode is that neither its
+   * assumptions nor its conclusion are predicate equalities, i.e. of the form
+   * (= t true/false), modulo symmetry. This is so that users of the converted
+   * ProofNode don't need to do case analysis on whether assumptions/conclusion
+   * are either t or (= t true/false).
+   *
+   * @param p a pointer to a CDProof to store the conversion of this EqProof
+   * @return the node that is the conclusion of the proof as added to p.
+   */
+  Node addToProof(CDProof* p) const;
+
+ private:
+  /**
+   * As above, but with a cache of previously processed nodes and their results
+   * (for DAG traversal). The caching is in terms of the original conclusions of
+   * EqProof.
+   *
+   * @param p a pointer to a CDProof to store the conversion of this EqProof
+   * @param visited a cache of the original EqProof conclusions and the
+   * resulting conclusion after conversion.
+   * @param assumptions the assumptions of the original EqProof (and their
+   * variations in terms of symmetry and conversion to/from predicate
+   * equalities)
+   * @return the node that is the conclusion of the proof as added to p.
+   */
+  Node addToProof(
+      CDProof* p,
+      std::unordered_map<Node, Node, NodeHashFunction>& visited,
+      std::unordered_set<Node, NodeHashFunction>& assumptions) const;
+
+  /** Removes all reflexivity steps, i.e. (= t t), from premises. */
+  void cleanReflPremises(std::vector<Node>& premises) const;
+
+  /** Expand coarse-grained transitivity steps for disequalities
+   *
+   * Currently the equality engine can represent disequality reasoning in a
+   * rather coarse-grained manner with EqProof. This is always the case when the
+   * transitivity step contains a disequality, (= (= t t') false) or its
+   * symmetric.
+   *
+   * There are two cases. In the simplest one the general shape of the EqProof
+   * is
+   *  (= t1 t2) (= t3 t2) (= (t1 t3) false)
+   *  ------------------------------------- EQP::TR
+   *             false = true
+   *
+   * which is expanded into
+   *                                          (= t3 t2)
+   *                                          --------- SYMM
+   *                                (= t1 t2) (= t2 t3)
+   *                                ------------------- TRANS
+   *   (= (= t1 t3) false)                (= t1 t3)
+   *  --------------------- SYMM    ------------------ TRUE_INTRO
+   *   (= false (= t1 t3))         (= (= t1 t3) true)
+   *  ----------------------------------------------- TRANS
+   *             false = true
+   *
+   * by explicitly adding the transitivity step for inferring (= t1 t3) and its
+   * predicate equality. Note that we differentiate (from now on) the EqProof
+   * rules ids from those of ProofRule by adding the prefix EQP:: to the former.
+   *
+   * In the other case, the general shape of the EqProof is
+   *
+   *  (= (= t1 t2) false) (= t1 x1) ... (= xn t3) (= t2 y1) ... (= ym t4)
+   * ------------------------------------------------------------------- EQP::TR
+   *         (= (= t4 t3) false)
+   *
+   * which is converted into
+   *
+   *   (= t1 x1) ... (= xn t3)      (= t2 y1) ... (= ym t4)
+   *  ------------------------ TR  ------------------------ TR
+   *   (= t1 t3)                    (= t2 t4)
+   *  ----------- SYMM             ----------- SYMM
+   *   (= t3 t1)                    (= t4 t2)
+   *  ---------------------------------------- CONG
+   *   (= (= t3 t4) (= t1 t2))                         (= (= t1 t2) false)
+   *  --------------------------------------------------------------------- TR
+   *           (= (= t3 t4) false)
+   *          --------------------- MACRO_SR_PRED_TRANSFORM
+   *           (= (= t4 t3) false)
+   *
+   * whereas the last step is only necessary if the conclusion has the arguments
+   * in reverse order than expected. Note that the original step represents two
+   * substitutions happening on the disequality, from t1->t3 and t2->t4, which
+   * are implicitly justified by transitivity steps that need to be made
+   * explicity. Since there is no sense of ordering among which premisis (other
+   * than (= (= t1 t2) false)) are used for which substitution, the transitivity
+   * proofs are built greedly by searching the sets of premises.
+   *
+   * If in either of the above cases then the conclusion is directly derived
+   * in the call, so only in the other cases we try to build a transitivity
+   * step below
+   *
+   * @param conclusion the conclusion of the (possibly) coarse-grained
+   * transitivity step
+   * @param premises the premises of the (possibly) coarse-grained
+   * transitivity step
+   * @param p a pointer to a CDProof to store the conversion of this EqProof
+   * @param assumptions the assumptions (and variants) of the original
+   * EqProof. These are necessary to avoid cyclic proofs, which could be
+   * generated by creating transitivity steps for assumptions (which depend on
+   * themselves).
+   */
+  bool expandTransitivityForDisequalities(
+      Node conclusion,
+      std::vector<Node>& premises,
+      CDProof* p,
+      std::unordered_set<Node, NodeHashFunction>& assumptions) const;
+
+  /** Builds a transitivity chain from equalities to derive a conclusion
+   *
+   * Given an equality (= t1 tn), and a list of equalities premises, attempts to
+   * build a chain (= t1 t2) ... (= tn-1 tn) from premises. This is done in a
+   * greedy manner by finding one "link" in the chain at a time, updating the
+   * conclusion to be the next link and the premises by removing the used
+   * premise, and searching recursively.
+   *
+   * Consider for example
+   * - conclusion: (= t1 t4)
+   * - premises:   (= t4 t2), (= t2 t3), (= t2 t1), (= t3 t4)
+   *
+   * It proceeds by searching for t1 in an equality in the premises, in order,
+   * which is found in the equality (= t2 t1). Since t2 != t4, it attempts to
+   * build a chain with
+   * - conclusion (= t2 t4)
+   * - premises (= t4 t2), (= t2 t3), (= t3 t4)
+   *
+   * In the first equality it finds t2 and also t4, which closes the chain, so
+   * that premises is updated to (= t2 t4) and the method returns true. Since
+   * the recursive call was successful, the original conclusion (= t1 t4) is
+   * justified with (= t1 t2) plus the chain built in the recursive call,
+   * i.e. (= t1 t2), (= t2 t4).
+   *
+   * Note that not all the premises were necessary to build a successful
+   * chain. Moreover, note that building a successful chain can depend on the
+   * order in which the equalities are chosen. When a recursive call fails to
+   * close a chain, the chosen equality is dismissed and another is searched for
+   * among the remaining ones.
+   *
+   * This method assumes that premises does not contain reflexivity premises.
+   * This is without loss of generality since such premises are spurious for a
+   * transitivity step.
+   *
+   * @param conclusion the conclusion of the transitivity chain of equalities
+   * @param premises the list of equalities to build a chain with
+   * @return whether premises successfully build a transitivity chain for the
+   * conclusion
+   */
+  bool buildTransitivityChain(Node conclusion,
+                              std::vector<Node>& premises) const;
+
+  /** Reduce the a congruence EqProof into a transitivity matrix
+   *
+   * Given a congruence EqProof of (= (f a0 ... an-1) (f b0 ... bn-1)), reduce
+   * its justification into a matrix
+   *
+   *   [0]   -> p_{0,0} ... p_{m_0,0}
+   *   ...
+   *   [n-1] -> p_{0,n} ... p_{m_n-1,n-1}
+   *
+   * where f has arity n and each p_{0,i} ... p_{m_i, i} is a transitivity chain
+   * (modulo ordering) justifying (= ai bi).
+   *
+   * Congruence steps in EqProof are binary, representing reasoning over curried
+   * applications. In the simplest case the general shape of a congruence
+   * EqProof is:
+   *                                     P0
+   *              ------- EQP::REFL  ----------
+   *       P1        []               (= a0 b0)
+   *  ---------   ----------------------- EQP::CONG
+   *  (= a1 b1)             []                        P2
+   *  ------------------------- EQP::CONG        -----------
+   *             []                               (= a2 b2)
+   *          ------------------------------------------------ EQP::CONG
+   *                  (= (f a0 a1 a2) (f b0 b1 b2))
+   *
+   * where [] stands for the null node, symbolizing "equality between partial
+   * applications".
+   *
+   * The reduction of such a proof is done by
+   * - converting the proof of the second CONG premise (via addToProof) and
+   *   adding the resulting node to row i of the matrix
+   * - recursively reducing the first proof with i-1
+   *
+   * In the above case the transitivity matrix would thus be
+   *   [0] -> (= a0 b0)
+   *   [1] -> (= a1 b1)
+   *   [2] -> (= a2 b2)
+   *
+   * The more complex case of congruence proofs has transitivity steps as the
+   * first child of CONG steps. For example
+   *                                     P0
+   *              ------- EQP::REFL  ----------
+   *     P'          []            (= a0 c)
+   *  ---------   ----------------------------- EQP::CONG
+   *  (= b0 c)             []                               P1
+   * ------------------------- EQP::TRANS             -----------
+   *            []                                     (= a1 b1)
+   *         ----------------------------------------------------- EQP::CONG
+   *                          (= (f a0 a1) (f b0 b1))
+   *
+   * where when the first child of CONG is a transitivity step
+   * - the premises that are CONG steps are recursively reduced with *the same*
+       argument i
+   * - the other premises are processed with addToProof and added to the i row
+   *   in the matrix
+   *
+   * In the above example the to which the transitivity matrix is
+   *   [0] -> (= a0 c), (= b0 c)
+   *   [1] -> (= a1 b1)
+   *
+   * The remaining complication is that when conclusion is an equality of n-ary
+   * applications of *different* arities, there is, necessarily, a transitivity
+   * step as a first child a CONG step whose conclusion is an equality of n-ary
+   * applications of different arities. For example
+   *             P0                              P1
+   * -------------------------- EQP::TRANS  -----------
+   *     (= (f a0 a1) (f b0))                (= a2 b1)
+   * -------------------------------------------------- EQP::CONG
+   *              (= (f a0 a1 a2) (f b0 b1))
+   *
+   * will be first reduced with i = 2 (maximal arity amorg the original
+   * conclusion's applications), adding (= a2 b1) to row 2 after processing
+   * P1. The first child is reduced with i = 1. Since it is a TRANS step whose
+   * conclusion is an equality of n-ary applications with mismatching arity, P0
+   * is processed with addToProof and the result is added to row 1. Thus the
+   * transitivity matrix is
+   *   [0] ->
+   *   [1] -> (= (f a0 a1) (f b0))
+   *   [2] -> (= a2 b1)
+   *
+   * The empty row 0 is used by the original caller of reduceNestedCongruence to
+   * compute that the above congruence proof's conclusion is
+   *   (= (f (f a0 a1) a2) (f (f b0) b1))
+   *
+   * @param i the i-th argument of the congruent applications, initially being
+   * the maximal arity among conclusion's applications.
+   * @param conclusion the original congruence conclusion
+   * @param transitivityMatrix a matrix of equalities with each row justifying
+   * an equality between the congruent applications
+   * @param p a pointer to a CDProof to store the conversion of this EqProof
+   * @param visited a cache of the original EqProof conclusions and the
+   * resulting conclusion after conversion.
+   * @param assumptions the assumptions (and variants) of the original EqProof
+   * @param isNary whether conclusion is an equality of n-ary applications
+   */
+  void reduceNestedCongruence(
+      unsigned i,
+      Node conclusion,
+      std::vector<std::vector<Node>>& transitivityMatrix,
+      CDProof* p,
+      std::unordered_map<Node, Node, NodeHashFunction>& visited,
+      std::unordered_set<Node, NodeHashFunction>& assumptions,
+      bool isNary) const;
+
+}; /* class EqProof */
+
+}  // Namespace eq
+}  // Namespace theory
+}  // Namespace CVC4
diff --git a/src/theory/uf/equality_engine.cpp b/src/theory/uf/equality_engine.cpp
index 1dd9ba8b6..b532bcfa5 100644
--- a/src/theory/uf/equality_engine.cpp
+++ b/src/theory/uf/equality_engine.cpp
@@ -2412,67 +2412,6 @@ bool EqClassIterator::isFinished() const {
   return d_current == null_id;
 }
 
-void EqProof::debug_print(const char* c, unsigned tb, PrettyPrinter* prettyPrinter) const {
-  std::stringstream ss;
-  debug_print(ss, tb, prettyPrinter);
-  Debug(c) << ss.str();
-}
-void EqProof::debug_print(std::ostream& os,
-                          unsigned tb,
-                          PrettyPrinter* prettyPrinter) const
-{
-  for (unsigned i = 0; i < tb; i++)
-  {
-    os << "  ";
-  }
-
-  if (prettyPrinter)
-  {
-    os << prettyPrinter->printTag(d_id);
-  }
-  else
-  {
-    os << static_cast<MergeReasonType>(d_id);
-  }
-  os << "(";
-  if (d_children.empty() && d_node.isNull())
-  {
-    os << ")";
-    return;
-  }
-  if (!d_node.isNull())
-  {
-    os << std::endl;
-    for (unsigned i = 0; i < tb + 1; ++i)
-    {
-      os << "  ";
-    }
-    os << d_node << (!d_children.empty() ? "," : "");
-  }
-  unsigned size = d_children.size();
-  for (unsigned i = 0; i < size; ++i)
-  {
-    os << std::endl;
-    d_children[i]->debug_print(os, tb + 1, prettyPrinter);
-    if (i < size - 1)
-    {
-      for (unsigned j = 0; j < tb + 1; ++j)
-      {
-        os << "  ";
-      }
-      os << ",";
-    }
-  }
-  if (size > 0)
-  {
-    for (unsigned i = 0; i < tb; ++i)
-    {
-      os << "  ";
-    }
-  }
-  os << ")" << std::endl;
-}
-
 } // Namespace uf
 } // Namespace theory
 } // Namespace CVC4
diff --git a/src/theory/uf/equality_engine.h b/src/theory/uf/equality_engine.h
index cf6eabfb7..6b1f3b6aa 100644
--- a/src/theory/uf/equality_engine.h
+++ b/src/theory/uf/equality_engine.h
@@ -32,6 +32,7 @@
 #include "expr/node.h"
 #include "theory/rewriter.h"
 #include "theory/theory.h"
+#include "theory/uf/eq_proof.h"
 #include "theory/uf/equality_engine_types.h"
 #include "util/statistics_registry.h"
 
@@ -757,9 +758,9 @@ public:
   }
 
   /**
-   * Add a kind to treat as function applications. 
-   * When extOperator is true, this equality engine will treat the operators of this kind 
-   * as "external" e.g. not internal nodes (see d_isInternal). This means that we will 
+   * Add a kind to treat as function applications.
+   * When extOperator is true, this equality engine will treat the operators of this kind
+   * as "external" e.g. not internal nodes (see d_isInternal). This means that we will
    * consider equivalence classes containing the operators of such terms, and "hasTerm" will
    * return true.
    */
@@ -951,34 +952,6 @@ public:
   bool isFinished() const;
 };/* class EqClassIterator */
 
-class EqProof
-{
-public:
-  class PrettyPrinter {
-  public:
-    virtual ~PrettyPrinter() {}
-    virtual std::string printTag(unsigned tag) = 0;
-  };
-
-  EqProof() : d_id(MERGED_THROUGH_REFLEXIVITY){}
-  unsigned d_id;
-  Node d_node;
-  std::vector<std::shared_ptr<EqProof>> d_children;
-  /**
-   * Debug print this proof on debug trace c with tabulation tb and pretty
-   * printer prettyPrinter.
-   */
-  void debug_print(const char* c, unsigned tb = 0,
-                   PrettyPrinter* prettyPrinter = nullptr) const;
-  /**
-   * Debug print this proof on output stream os with tabulation tb and pretty
-   * printer prettyPrinter.
-   */
-  void debug_print(std::ostream& os,
-                   unsigned tb = 0,
-                   PrettyPrinter* prettyPrinter = nullptr) const;
-};/* class EqProof */
-
 } // Namespace eq
 } // Namespace theory
 } // Namespace CVC4