Add the LazyTreeProofGenerator. (#5948)

This PR adds a new proof utility to construct tree-shaped proofs in a lazy fashion.
The LazyTreeProofGenerator is currently intended to be used for CAD proofs, where we need to construct proofs that consist of nested case-splits, but the exact split (in a form suitable for proof construction) is only known when the whole subtree is finished.
We thus store the proof in a tree structure similar to proof nodes, and transform the whole proof to a proper proof node once all data is available.

3 files changed, 368 insertions, 0 deletions

diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index 3bfb248a4..5a44df141 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -612,6 +612,8 @@ libcvc4_add_sources(
   theory/inference_id.h
   theory/inference_manager_buffered.cpp
   theory/inference_manager_buffered.h
+  theory/lazy_tree_proof_generator.cpp
+  theory/lazy_tree_proof_generator.h
   theory/logic_info.cpp
   theory/logic_info.h
   theory/model_manager.cpp
diff --git a/src/theory/lazy_tree_proof_generator.cpp b/src/theory/lazy_tree_proof_generator.cpp
new file mode 100644
index 000000000..126ce60b9
--- /dev/null
+++ b/src/theory/lazy_tree_proof_generator.cpp
@@ -0,0 +1,144 @@
+/*********************                                                        */
+/*! \file lazy_tree_proof_generator.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Gereon Kremer
+ ** 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 the lazy tree proof generator class
+ **/
+
+#include "theory/lazy_tree_proof_generator.h"
+
+#include <iostream>
+
+#include "expr/node.h"
+#include "expr/proof_generator.h"
+#include "expr/proof_node_manager.h"
+
+namespace CVC4 {
+namespace theory {
+
+LazyTreeProofGenerator::LazyTreeProofGenerator(ProofNodeManager* pnm,
+                                               const std::string& name)
+    : d_pnm(pnm), d_name(name)
+{
+  d_stack.emplace_back(&d_proof);
+}
+void LazyTreeProofGenerator::openChild()
+{
+  detail::TreeProofNode& pn = getCurrent();
+  pn.d_children.emplace_back();
+  d_stack.emplace_back(&pn.d_children.back());
+}
+void LazyTreeProofGenerator::closeChild()
+{
+  Assert(getCurrent().d_rule != PfRule::UNKNOWN);
+  d_stack.pop_back();
+}
+detail::TreeProofNode& LazyTreeProofGenerator::getCurrent()
+{
+  Assert(!d_stack.empty()) << "Proof construction has already been finished.";
+  return *d_stack.back();
+}
+void LazyTreeProofGenerator::setCurrent(PfRule rule,
+                                        const std::vector<Node>& premise,
+                                        std::vector<Node> args,
+                                        Node proven)
+{
+  detail::TreeProofNode& pn = getCurrent();
+  pn.d_rule = rule;
+  pn.d_premise = premise;
+  pn.d_args = args;
+  pn.d_proven = proven;
+}
+std::shared_ptr<ProofNode> LazyTreeProofGenerator::getProof() const
+{
+  // Check cache
+  if (d_cached) return d_cached;
+  Assert(d_stack.empty()) << "Proof construction has not yet been finished.";
+  std::vector<std::shared_ptr<ProofNode>> scope;
+  d_cached = getProof(scope, d_proof);
+  return d_cached;
+}
+
+std::shared_ptr<ProofNode> LazyTreeProofGenerator::getProofFor(Node f)
+{
+  Assert(hasProofFor(f));
+  return getProof();
+}
+
+bool LazyTreeProofGenerator::hasProofFor(Node f)
+{
+  return f == getProof()->getResult();
+}
+
+std::shared_ptr<ProofNode> LazyTreeProofGenerator::getProof(
+    std::vector<std::shared_ptr<ProofNode>>& scope,
+    const detail::TreeProofNode& pn) const
+{
+  // Store scope size to reset scope afterwards
+  std::size_t before = scope.size();
+  std::vector<std::shared_ptr<ProofNode>> children;
+  if (pn.d_rule == PfRule::SCOPE)
+  {
+    // Extend scope for all but the root node
+    if (&pn != &d_proof)
+    {
+      for (const auto& a : pn.d_args)
+      {
+        scope.emplace_back(d_pnm->mkAssume(a));
+      }
+    }
+  }
+  else
+  {
+    // Initialize the children with the scope
+    children = scope;
+  }
+  for (auto& c : pn.d_children)
+  {
+    // Recurse into tree
+    children.emplace_back(getProof(scope, c));
+  }
+  for (const auto& p : pn.d_premise)
+  {
+    // Add premises as assumptions
+    children.emplace_back(d_pnm->mkAssume(p));
+  }
+  // Reset scope
+  scope.resize(before);
+  return d_pnm->mkNode(pn.d_rule, children, pn.d_args);
+}
+
+void LazyTreeProofGenerator::print(std::ostream& os,
+                                   const std::string& prefix,
+                                   const detail::TreeProofNode& pn) const
+{
+  os << prefix << pn.d_rule << ": ";
+  container_to_stream(os, pn.d_premise);
+  os << " ==> " << pn.d_proven << std::endl;
+  if (!pn.d_args.empty())
+  {
+    os << prefix << ":args ";
+    container_to_stream(os, pn.d_args);
+    std::cout << std::endl;
+  }
+  for (const auto& c : pn.d_children)
+  {
+    print(os, prefix + '\t', c);
+  }
+}
+
+std::ostream& operator<<(std::ostream& os, const LazyTreeProofGenerator& ltpg)
+{
+  ltpg.print(os, "", ltpg.d_proof);
+  return os;
+}
+
+}  // namespace theory
+}  // namespace CVC4
\ No newline at end of file
diff --git a/src/theory/lazy_tree_proof_generator.h b/src/theory/lazy_tree_proof_generator.h
new file mode 100644
index 000000000..980d6d6bb
--- /dev/null
+++ b/src/theory/lazy_tree_proof_generator.h
@@ -0,0 +1,222 @@
+/*********************                                                        */
+/*! \file lazy_tree_proof_generator.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Gereon Kremer
+ ** 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 The lazy tree proof generator class
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef CVC4__THEORY__LAZY_TREE_PROOF_GENERATOR_H
+#define CVC4__THEORY__LAZY_TREE_PROOF_GENERATOR_H
+
+#include <iostream>
+
+#include "expr/node.h"
+#include "expr/proof_generator.h"
+#include "expr/proof_node_manager.h"
+
+namespace CVC4 {
+namespace theory {
+namespace detail {
+/**
+ * A single node in the proof tree created by the LazyTreeProofGenerator.
+ * A node directly represents a ProofNode that is eventually constructed from
+ * it. The Nodes of the additional field d_premise are added to d_children as
+ * new assumptions via ASSUME.
+ */
+struct TreeProofNode
+{
+  /** The proof rule */
+  PfRule d_rule = PfRule::UNKNOWN;
+  /** Assumptions used as premise for this proof step */
+  std::vector<Node> d_premise;
+  /** Arguments for this proof step */
+  std::vector<Node> d_args;
+  /** Conclusion of this proof step */
+  Node d_proven;
+  /** Children of this proof step */
+  std::vector<TreeProofNode> d_children;
+};
+}  // namespace detail
+
+/**
+ * This class supports the lazy creation of a tree-shaped proof.
+ * The core idea is that the lazy creation is necessary because proof rules
+ * depend on assumptions that are only known after the whole subtree has been
+ * finished.
+ *
+ * We indend to argue about proofs that roughly go as follows:
+ * - we assume a set of assumptions
+ * - we do a case split
+ * - for every case, we derive false, possibly by nested case splits
+ *
+ * Every case is represented by a SCOPE whose child derives false. When
+ * composing the final proof, we explicitly extend the premise of every proof
+ * step with the scope (the currently selected case) that this proof step lives
+ * in. When doing this, we ignore the outermost scope (which assumes the
+ * assertion set) to allow for having conflicts that are only a subset of the
+ * assertion set.
+ *
+ * Consider the example  x*x<1 and x>2  and the intended proof
+ *  (SCOPE
+ *    (ARITH_NL_CAD_SPLIT
+ *      (SCOPE
+ *        (ARITH_NL_CAD_DIRECT  (x<=2  and  x>2) ==> false)
+ *        :args [x<=2]
+ *      )
+ *      (SCOPE
+ *        (ARITH_NL_CAD_DIRECT  (x>=1  and  x*x<1) ==> false)
+ *        :args [x>=1]
+ *      )
+ *    )
+ *    :args [ x*x<1, x>2 ]
+ *  )
+ * We obtain this proof in a way that (in general) gives us the assumptions
+ * for the scopes (x<=2, x>=1) only when the scope children have been fully
+ * computed. Thus, we store the proof in an intermediate form and add the scope
+ * arguments when we learn them. Once we have completed the proof, we can easily
+ * transform it into proper ProofNodes.
+ *
+ * This class is stateful in the sense that the interface (in particular
+ * openChild() and closeChild()) navigates the proof tree (and creating it
+ * on-the-fly). Initially, and after reset() has been called, the proof consists
+ * of one empty proof node (with proof rule UNKNOWN). It stores the current
+ * position in the proof tree internally to make the interface easier to use.
+ *
+ * THIS MAKES THIS CLASS INHERENTLY NOT THREAD-SAFE!
+ *
+ * To construct the above proof, use this class roughly as follows:
+ *  setCurrent(SCOPE, {}, assertions, false);
+ *  openChild();
+ *  // First nested scope
+ *  openChild();
+ *  setCurrent(SCOPE, {}, {}, false);
+ *  openChild();
+ *  setCurrent(CAD_DIRECT, {x>2}, {}, false);
+ *  closeChild();
+ *  getCurrent().args = {x<=2};
+ *  closeChild();
+ *  // Second nested scope
+ *  openChild();
+ *  setCurrent(SCOPE, {}, {}, false);
+ *  openChild();
+ *  setCurrent(CAD_DIRECT, {x*x<1}, {}, false);
+ *  closeChild();
+ *  getCurrent().args = {x>=1};
+ *  closeChild();
+ *  // Finish split
+ *  setCurrent(CAD_SPLIT, {}, {}, false);
+ *  closeChild();
+ *  closeChild();
+ *
+ * To explicitly finish proof construction, we need to call closeChild() one
+ * additional time.
+ */
+class LazyTreeProofGenerator : public ProofGenerator
+{
+ public:
+  friend std::ostream& operator<<(std::ostream& os,
+                                  const LazyTreeProofGenerator& ltpg);
+
+  LazyTreeProofGenerator(ProofNodeManager* pnm,
+                         const std::string& name = "LazyTreeProofGenerator");
+
+  std::string identify() const override { return d_name; }
+  /** Create a new child and make it the current node */
+  void openChild();
+  /**
+   * Finish the current node and return to its parent
+   * Checks that the current node has a proof rule different from UNKNOWN.
+   * When called on the root node, this finishes the proof construction: we can
+   * no longer call getCurrent(), setCurrent() openChild() and closeChild(), but
+   * instead can call getProof() now.
+   */
+  void closeChild();
+  /**
+   * Return a reference to the current node
+   */
+  detail::TreeProofNode& getCurrent();
+  /** Set the current node / proof step */
+  void setCurrent(PfRule rule,
+                  const std::vector<Node>& premise,
+                  std::vector<Node> args,
+                  Node proven);
+  /** Construct the proof as a ProofNode */
+  std::shared_ptr<ProofNode> getProof() const;
+  /** Return the constructed proof. Checks that we have proven f */
+  std::shared_ptr<ProofNode> getProofFor(Node f) override;
+  /** Checks whether we have proven f */
+  bool hasProofFor(Node f) override;
+
+  /**
+   * Removes children from the current node based on the given predicate.
+   * It can be used for cases where facts (and their proofs) are eagerly
+   * generated and then later pruned, for example to produce smaller conflicts.
+   * The predicate is given as a Callable f that is called for every child with
+   * the id of the child and the child itself.
+   * f should return true if the child should be kept, fals if the child should
+   * be removed.
+   * @param f a Callable bool(std::size_t, const detail::TreeProofNode&)
+   */
+  template <typename F>
+  void pruneChildren(F&& f)
+  {
+    auto& children = getCurrent().d_children;
+    std::size_t cur = 0;
+    std::size_t pos = 0;
+    for (std::size_t size = children.size(); cur < size; ++cur)
+    {
+      if (f(cur, children[pos]))
+      {
+        if (cur != pos)
+        {
+          children[pos] = std::move(children[cur]);
+        }
+        ++pos;
+      }
+    }
+    children.resize(pos);
+  }
+
+ private:
+  /** recursive proof construction used by getProof() */
+  std::shared_ptr<ProofNode> getProof(
+      std::vector<std::shared_ptr<ProofNode>>& scope,
+      const detail::TreeProofNode& pn) const;
+
+  /** recursive debug printing used by operator<<() */
+  void print(std::ostream& os,
+             const std::string& prefix,
+             const detail::TreeProofNode& pn) const;
+
+  /** The ProofNodeManager used for constructing ProofNodes */
+  ProofNodeManager* d_pnm;
+  /** The trace to the current node */
+  std::vector<detail::TreeProofNode*> d_stack;
+  /** The root node of the proof tree */
+  detail::TreeProofNode d_proof;
+  /** Caches the result of getProof() */
+  mutable std::shared_ptr<ProofNode> d_cached;
+  /** Name of this proof generator */
+  std::string d_name;
+};
+
+/**
+ * Prints the current state of a LazyTreeProofGenerator. Can also be used on a
+ * partially constructed proof. It is intended for debugging only and attempts
+ * to pretty-print itself using indentation.
+ */
+std::ostream& operator<<(std::ostream& os, const LazyTreeProofGenerator& ltpg);
+
+}  // namespace theory
+}  // namespace CVC4
+
+#endif