(proof-new) Add proof generator for CAD solver (#5964)

This PR adds a proof generator for the CAD solver, including two new proof rules. The code is not yet used, but will be integrated into the CAD solver itself in another PR.

7 files changed, 542 insertions, 0 deletions

diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index 5a44df141..deb20ab70 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -347,6 +347,10 @@ libcvc4_add_sources(
   theory/arith/nl/cad/constraints.h
   theory/arith/nl/cad/projections.cpp
   theory/arith/nl/cad/projections.h
+  theory/arith/nl/cad/proof_checker.cpp
+  theory/arith/nl/cad/proof_checker.h
+  theory/arith/nl/cad/proof_generator.cpp
+  theory/arith/nl/cad/proof_generator.h
   theory/arith/nl/cad/variable_ordering.cpp
   theory/arith/nl/cad/variable_ordering.h
   theory/arith/nl/ext/constraint.cpp
diff --git a/src/expr/proof_rule.cpp b/src/expr/proof_rule.cpp
index 85463d2d9..bead7397a 100644
--- a/src/expr/proof_rule.cpp
+++ b/src/expr/proof_rule.cpp
@@ -188,6 +188,8 @@ const char* toString(PfRule id)
       return "ARITH_TRANS_SINE_APPROX_BELOW_NEG";
     case PfRule::ARITH_TRANS_SINE_APPROX_BELOW_POS:
       return "ARITH_TRANS_SINE_APPROX_BELOW_POS";
+    case PfRule::ARITH_NL_CAD_DIRECT: return "ARITH_NL_CAD_DIRECT";
+    case PfRule::ARITH_NL_CAD_RECURSIVE: return "ARITH_NL_CAD_RECURSIVE";
     //================================================= Unknown rule
     case PfRule::UNKNOWN: return "UNKNOWN";
     default: return "?";
diff --git a/src/expr/proof_rule.h b/src/expr/proof_rule.h
index 917db4088..d42175fab 100644
--- a/src/expr/proof_rule.h
+++ b/src/expr/proof_rule.h
@@ -1277,6 +1277,41 @@ enum class PfRule : uint32_t
   // secant of p from l to u.
   ARITH_TRANS_SINE_APPROX_BELOW_POS,
 
+  // ================ CAD Lemmas
+  // We use IRP for IndexedRootPredicate.
+  //
+  // A formula "Interval" describes that a variable (xn is none is given) is
+  // within a particular interval whose bounds are given as IRPs. It is either
+  // an open interval or a point interval:
+  //   (IRP k poly) < xn < (IRP k poly)
+  //   xn == (IRP k poly)
+  //
+  // A formula "Cell" describes a portion
+  // of the real space in the following form:
+  //   Interval(x1) and Interval(x2) and ...
+  // We implicitly assume a Cell to go up to n-1 (and can be empty).
+  //
+  // A formula "Covering" is a set of Intervals, implying that xn can be in
+  // neither of these intervals. To be a covering (of the real line), the union
+  // of these intervals should be the real numbers.
+  // ======== CAD direct conflict
+  // Children (Cell, A)
+  // ---------------------
+  // Conclusion: (false)
+  // A direct interval is generated from an assumption A (in variables x1...xn)
+  // over a Cell (in variables x1...xn). It derives that A evaluates to false
+  // over the Cell. In the actual algorithm, it means that xn can not be in the
+  // topmost interval of the Cell.
+  ARITH_NL_CAD_DIRECT,
+  // ======== CAD recursive interval
+  // Children (Cell, Covering)
+  // ---------------------
+  // Conclusion: (false)
+  // A recursive interval is generated from a Covering (for xn) over a Cell
+  // (in variables x1...xn-1). It generates the conclusion that no xn exists
+  // that extends the Cell and satisfies all assumptions.
+  ARITH_NL_CAD_RECURSIVE,
+
   //================================================= Unknown rule
   UNKNOWN,
 };
diff --git a/src/theory/arith/nl/cad/proof_checker.cpp b/src/theory/arith/nl/cad/proof_checker.cpp
new file mode 100644
index 000000000..24c4b813c
--- /dev/null
+++ b/src/theory/arith/nl/cad/proof_checker.cpp
@@ -0,0 +1,61 @@
+/*********************                                                        */
+/*! \file proof_checker.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 CAD proof checker
+ **/
+
+#include "theory/arith/nl/cad/proof_checker.h"
+
+#include "expr/sequence.h"
+#include "theory/rewriter.h"
+
+using namespace CVC4::kind;
+
+namespace CVC4 {
+namespace theory {
+namespace arith {
+namespace nl {
+namespace cad {
+
+void CADProofRuleChecker::registerTo(ProofChecker* pc)
+{
+  // trusted rules
+  pc->registerTrustedChecker(PfRule::ARITH_NL_CAD_DIRECT, this, 2);
+  pc->registerTrustedChecker(PfRule::ARITH_NL_CAD_RECURSIVE, this, 2);
+}
+
+Node CADProofRuleChecker::checkInternal(PfRule id,
+                                        const std::vector<Node>& children,
+                                        const std::vector<Node>& args)
+{
+  Trace("nl-cad-checker") << "Checking " << id << std::endl;
+  for (const auto& c : children)
+  {
+    Trace("nl-cad-checker") << "\t" << c << std::endl;
+  }
+  if (id == PfRule::ARITH_NL_CAD_DIRECT)
+  {
+    Assert(args.size() == 1);
+    return args[0];
+  }
+  if (id == PfRule::ARITH_NL_CAD_RECURSIVE)
+  {
+    Assert(args.size() == 1);
+    return args[0];
+  }
+  return Node::null();
+}
+
+}  // namespace cad
+}  // namespace nl
+}  // namespace arith
+}  // namespace theory
+}  // namespace CVC4
diff --git a/src/theory/arith/nl/cad/proof_checker.h b/src/theory/arith/nl/cad/proof_checker.h
new file mode 100644
index 000000000..d10ce2e1b
--- /dev/null
+++ b/src/theory/arith/nl/cad/proof_checker.h
@@ -0,0 +1,59 @@
+/*********************                                                        */
+/*! \file proof_checker.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 CAD proof checker utility
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef CVC4__THEORY__ARITH__NL__CAD__PROOF_CHECKER_H
+#define CVC4__THEORY__ARITH__NL__CAD__PROOF_CHECKER_H
+
+#include "expr/node.h"
+#include "expr/proof_checker.h"
+#include "expr/proof_node.h"
+
+namespace CVC4 {
+namespace theory {
+namespace arith {
+namespace nl {
+namespace cad {
+
+/**
+ * A checker for CAD proofs
+ *
+ * This proof checker takes care of the two CAD proof rules ARITH_NL_CAD_DIRECT
+ * and ARITH_NL_CAD_RECURSIVE. It does not do any actual proof checking yet, but
+ * considers them to be trusted rules.
+ */
+class CADProofRuleChecker : public ProofRuleChecker
+{
+ public:
+  CADProofRuleChecker() {}
+  ~CADProofRuleChecker() {}
+
+  /** Register all rules owned by this rule checker in pc. */
+  void registerTo(ProofChecker* pc) override;
+
+ protected:
+  /** Return the conclusion of the given proof step, or null if it is invalid */
+  Node checkInternal(PfRule id,
+                     const std::vector<Node>& children,
+                     const std::vector<Node>& args) override;
+};
+
+}  // namespace cad
+}  // namespace nl
+}  // namespace arith
+}  // namespace theory
+}  // namespace CVC4
+
+#endif /* CVC4__THEORY__STRINGS__PROOF_CHECKER_H */
diff --git a/src/theory/arith/nl/cad/proof_generator.cpp b/src/theory/arith/nl/cad/proof_generator.cpp
new file mode 100644
index 000000000..ebf1ab25e
--- /dev/null
+++ b/src/theory/arith/nl/cad/proof_generator.cpp
@@ -0,0 +1,232 @@
+/*********************                                                        */
+/*! \file 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 CAD proof generator
+ **/
+
+#include "theory/arith/nl/cad/proof_generator.h"
+
+#ifdef CVC4_POLY_IMP
+
+namespace CVC4 {
+namespace theory {
+namespace arith {
+namespace nl {
+namespace cad {
+
+namespace {
+/**
+ * Retrieves the root indices of the sign-invariant region of v.
+ *
+ * We assume that roots holds a sorted list of roots from one polynomial.
+ * If v is equal to one of these roots, we return (id,id) where id is the index
+ * of this root within roots. Otherwise, we return the id of the largest root
+ * below v and the id of the smallest root above v. To make sure a smaller root
+ * and a larger root always exist, we implicitly extend the roots by -infty and
+ * infty.
+ *
+ * ATTENTION: if we return id, the corresponding root is:
+ *   - id = 0: -infty
+ *   - 0 < id <= roots.size(): roots[id-1]
+ *   - id = roots.size() + 1: infty
+ */
+std::pair<std::size_t, std::size_t> getRootIDs(
+    const std::vector<poly::Value>& roots, const poly::Value& v)
+{
+  for (std::size_t i = 0; i < roots.size(); ++i)
+  {
+    if (roots[i] == v)
+    {
+      return {i + 1, i + 1};
+    }
+    if (roots[i] > v)
+    {
+      return {i, i + 1};
+    }
+  }
+  return {roots.size(), roots.size() + 1};
+}
+
+/**
+ * Constructs an IndexedRootExpression:
+ *   var ~rel~ root_k(poly)
+ * where root_k(poly) is "the k'th root of the polynomial".
+ *
+ * @param var The variable that is bounded
+ * @param rel The relation for this constraint
+ * @param zero A node representing Rational(0)
+ * @param k The index of the root (starting with 1)
+ * @param poly The polynomial whose root shall be considered
+ * @param vm A variable mapper from CVC4 to libpoly variables
+ */
+Node mkIRP(const Node& var,
+           Kind rel,
+           const Node& zero,
+           std::size_t k,
+           const poly::Polynomial& poly,
+           VariableMapper& vm)
+{
+  auto* nm = NodeManager::currentNM();
+  auto op = nm->mkConst<IndexedRootPredicate>(IndexedRootPredicate(k));
+  return nm->mkNode(Kind::INDEXED_ROOT_PREDICATE,
+                    op,
+                    nm->mkNode(rel, var, zero),
+                    as_cvc_polynomial(poly, vm));
+}
+
+}  // namespace
+
+CADProofGenerator::CADProofGenerator(context::Context* ctx,
+                                     ProofNodeManager* pnm)
+    : d_pnm(pnm), d_proofs(pnm, ctx), d_current(nullptr)
+{
+  d_false = NodeManager::currentNM()->mkConst<bool>(false);
+  d_zero = NodeManager::currentNM()->mkConst<Rational>(0);
+}
+
+void CADProofGenerator::startNewProof()
+{
+  d_current = d_proofs.allocateProof();
+}
+void CADProofGenerator::startRecursive() { d_current->openChild(); }
+void CADProofGenerator::endRecursive()
+{
+  d_current->setCurrent(PfRule::ARITH_NL_CAD_RECURSIVE, {}, {d_false}, d_false);
+  d_current->closeChild();
+}
+void CADProofGenerator::startScope()
+{
+  d_current->openChild();
+  d_current->getCurrent().d_rule = PfRule::SCOPE;
+}
+void CADProofGenerator::endScope(const std::vector<Node>& args)
+{
+  d_current->setCurrent(PfRule::SCOPE, {}, args, d_false);
+  d_current->closeChild();
+}
+
+ProofGenerator* CADProofGenerator::getProofGenerator() const
+{
+  return d_current;
+}
+
+void CADProofGenerator::addDirect(Node var,
+                                  VariableMapper& vm,
+                                  const poly::Polynomial& poly,
+                                  const poly::Assignment& a,
+                                  poly::SignCondition& sc,
+                                  const poly::Interval& interval,
+                                  Node constraint)
+{
+  if (is_minus_infinity(get_lower(interval))
+      && is_plus_infinity(get_upper(interval)))
+  {
+    // "Full conflict", constraint excludes (-inf,inf)
+    d_current->openChild();
+    d_current->setCurrent(
+        PfRule::ARITH_NL_CAD_DIRECT, {constraint}, {d_false}, d_false);
+    d_current->closeChild();
+    return;
+  }
+  std::vector<Node> res;
+  auto roots = poly::isolate_real_roots(poly, a);
+  if (get_lower(interval) == get_upper(interval))
+  {
+    // Excludes a single point only
+    auto ids = getRootIDs(roots, get_lower(interval));
+    Assert(ids.first == ids.second);
+    res.emplace_back(mkIRP(var, Kind::EQUAL, d_zero, ids.first, poly, vm));
+  }
+  else
+  {
+    // Excludes an open interval
+    if (!is_minus_infinity(get_lower(interval)))
+    {
+      // Interval has lower bound that is not -inf
+      auto ids = getRootIDs(roots, get_lower(interval));
+      Assert(ids.first == ids.second);
+      Kind rel = poly::get_lower_open(interval) ? Kind::GT : Kind::GEQ;
+      res.emplace_back(mkIRP(var, rel, d_zero, ids.first, poly, vm));
+    }
+    if (!is_plus_infinity(get_upper(interval)))
+    {
+      // Interval has upper bound that is not inf
+      auto ids = getRootIDs(roots, get_upper(interval));
+      Assert(ids.first == ids.second);
+      Kind rel = poly::get_upper_open(interval) ? Kind::LT : Kind::LEQ;
+      res.emplace_back(mkIRP(var, rel, d_zero, ids.first, poly, vm));
+    }
+  }
+  // Add to proof manager
+  startScope();
+  d_current->openChild();
+  d_current->setCurrent(
+      PfRule::ARITH_NL_CAD_DIRECT, {constraint}, {d_false}, d_false);
+  d_current->closeChild();
+  endScope(res);
+}
+
+std::vector<Node> CADProofGenerator::constructCell(Node var,
+                                                   const CACInterval& i,
+                                                   const poly::Assignment& a,
+                                                   const poly::Value& s,
+                                                   VariableMapper& vm)
+{
+  if (is_minus_infinity(get_lower(i.d_interval))
+      && is_plus_infinity(get_upper(i.d_interval)))
+  {
+    // "Full conflict", constraint excludes (-inf,inf)
+    return {};
+  }
+
+  std::vector<Node> res;
+
+  // Just use bounds for all polynomials
+  for (const auto& poly : i.d_mainPolys)
+  {
+    auto roots = poly::isolate_real_roots(poly, a);
+    auto ids = getRootIDs(roots, s);
+    if (ids.first == ids.second)
+    {
+      // Excludes a single point only
+      res.emplace_back(mkIRP(var, Kind::EQUAL, d_zero, ids.first, poly, vm));
+    }
+    else
+    {
+      // Excludes an open interval
+      if (ids.first > 0)
+      {
+        // Interval has lower bound that is not -inf
+        res.emplace_back(mkIRP(var, Kind::GT, d_zero, ids.first, poly, vm));
+      }
+      if (ids.second <= roots.size())
+      {
+        // Interval has upper bound that is not inf
+        res.emplace_back(mkIRP(var, Kind::LT, d_zero, ids.first, poly, vm));
+      }
+    }
+  }
+
+  return res;
+}
+
+std::ostream& operator<<(std::ostream& os, const CADProofGenerator& proof)
+{
+  return os << *proof.d_current;
+}
+
+}  // namespace cad
+}  // namespace nl
+}  // namespace arith
+}  // namespace theory
+}  // namespace CVC4
+
+#endif
diff --git a/src/theory/arith/nl/cad/proof_generator.h b/src/theory/arith/nl/cad/proof_generator.h
new file mode 100644
index 000000000..fd2458271
--- /dev/null
+++ b/src/theory/arith/nl/cad/proof_generator.h
@@ -0,0 +1,149 @@
+/*********************                                                        */
+/*! \file 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 Implements the proof generator for CAD
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef CVC4__THEORY__ARITH__NL__CAD__PROOF_GENERATOR_H
+#define CVC4__THEORY__ARITH__NL__CAD__PROOF_GENERATOR_H
+
+#include "util/real_algebraic_number.h"
+
+#ifdef CVC4_POLY_IMP
+
+#include <poly/polyxx.h>
+
+#include <vector>
+
+#include "context/cdlist.h"
+#include "expr/node.h"
+#include "expr/proof_generator.h"
+#include "expr/proof_set.h"
+#include "theory/arith/nl/cad/cdcac_utils.h"
+#include "theory/arith/nl/poly_conversion.h"
+#include "theory/lazy_tree_proof_generator.h"
+
+namespace CVC4 {
+namespace theory {
+namespace arith {
+namespace nl {
+namespace cad {
+
+/**
+ * This class manages the proof creation during a run of the CAD solver.
+ *
+ * Though it implements the ProofGenerator interface getProofFor(Node), it only
+ * gives a proof for a single node.
+ *
+ * It uses a LazyTreeProofGenerator internally to manage the tree-based proof
+ * construction.
+ */
+class CADProofGenerator
+{
+ public:
+  friend std::ostream& operator<<(std::ostream& os,
+                                  const CADProofGenerator& proof);
+  CADProofGenerator(context::Context* ctx, ProofNodeManager* pnm);
+
+  /** Start a new proof in this proof generator */
+  void startNewProof();
+  /** Start a new recursive call */
+  void startRecursive();
+  /** Finish the current recursive call */
+  void endRecursive();
+  /** Start a new scope, corresponding to a guess in CDCAC */
+  void startScope();
+  /** Finish a scope and add the (generalized) sample that was refuted */
+  void endScope(const std::vector<Node>& args);
+  /** Return the current proof generator */
+  ProofGenerator* getProofGenerator() const;
+
+  /**
+   * Calls LazyTreeProofGenerator::pruneChildren(f), but decorates the
+   * predicate such that f only accepts the index.
+   * @param f A Callable bool(std::size_t)
+   */
+  template <typename F>
+  void pruneChildren(F&& f)
+  {
+    d_current->pruneChildren(
+        [&f](std::size_t i, const detail::TreeProofNode& tpn) { return f(i); });
+  }
+
+  /**
+   * Add a direct interval conflict as generated in getUnsatIntervals().
+   * Its meaning is:
+   *   over the partial assignment a, var is not in interval because p~sc~0
+   *   and the origin of this is constraint.
+   *
+   * @param var The variable for which the interval is excluded
+   * @param vm A variable mapper between CVC4 and libpoly variables
+   * @param p The polynomial of the constraint
+   * @param a The current partial assignment
+   * @param sc The sign condition of the constraint
+   * @param interval The concrete interval that is excluded
+   * @param constraint The assumption that yields p and sc
+   */
+  void addDirect(Node var,
+                 VariableMapper& vm,
+                 const poly::Polynomial& p,
+                 const poly::Assignment& a,
+                 poly::SignCondition& sc,
+                 const poly::Interval& interval,
+                 Node constraint);
+
+  /**
+   * Constructs the (generalized) interval that is to be excluded from a
+   * CACInterval. It should be called after the recursive call to construct the
+   * generalized sample necessary for endScope().
+   *
+   * @param var The variable for which the interval is excluded
+   * @param i The concrete interval that is excluded
+   * @param a The current partial assignment
+   * @param s The sample point that is refuted for var
+   * @param vm A variable mapper between CVC4 and libpoly variables
+   */
+  std::vector<Node> constructCell(Node var,
+                                  const CACInterval& i,
+                                  const poly::Assignment& a,
+                                  const poly::Value& s,
+                                  VariableMapper& vm);
+
+ private:
+  /** The proof node manager used for the proofs */
+  ProofNodeManager* d_pnm;
+  /** The list of generated proofs */
+  CDProofSet<LazyTreeProofGenerator> d_proofs;
+  /** The current proof */
+  LazyTreeProofGenerator* d_current;
+
+  /** Constant false */
+  Node d_false;
+  /** Constant zero */
+  Node d_zero;
+};
+
+/**
+ * Prints the underlying LazyTreeProofGenerator. Please check the documentation
+ * of std::ostream& operator<<(std::ostream&, const LazyTreeProofGenerator&)
+ */
+std::ostream& operator<<(std::ostream& os, const CADProofGenerator& proof);
+
+}  // namespace cad
+}  // namespace nl
+}  // namespace arith
+}  // namespace theory
+}  // namespace CVC4
+
+#endif
+#endif