(proof-new) Add proofs for CAD solver (#5981)

This PR adds proofs for the CAD solver, based on the proof generator from the previous PR.
Note that the level of detail of these CAD proofs is significantly higher than for other proofs. Making these proofs more fine-grained and maybe at some point accessible to proof checkers is probably still quite a bit of work.
Thus, the CAD proof rules are both trusted rules for now.

diff --git a/src/theory/arith/nl/cad/cdcac.cpp b/src/theory/arith/nl/cad/cdcac.cpp
index d076438f59f1995f534ebd3758ae86fb60818ca3..df3ba37f3077aa9ba618233335991fdea4bbc746 100644 (file)
--- a/src/theory/arith/nl/cad/cdcac.cpp
+++ b/src/theory/arith/nl/cad/cdcac.cpp
@@ -39,11 +39,15 @@ namespace arith {
 namespace nl {
 namespace cad {
 
-CDCAC::CDCAC() {}
-
-CDCAC::CDCAC(const std::vector<poly::Variable>& ordering)
+CDCAC::CDCAC(context::Context* ctx,
+             ProofNodeManager* pnm,
+             const std::vector<poly::Variable>& ordering)
     : d_variableOrdering(ordering)
 {
+  if (pnm != nullptr)
+  {
+    d_proof.reset(new CADProofGenerator(ctx, pnm));
+  }
 }
 
 void CDCAC::reset()
@@ -120,6 +124,17 @@ std::vector<CACInterval> CDCAC::getUnsatIntervals(std::size_t cur_variable)
       if (!is_minus_infinity(get_lower(i))) l = m;
       if (!is_plus_infinity(get_upper(i))) u = m;
       res.emplace_back(CACInterval{i, l, u, m, d, {n}});
+      if (isProofEnabled())
+      {
+        d_proof->addDirect(
+            d_constraints.varMapper()(d_variableOrdering[cur_variable]),
+            d_constraints.varMapper(),
+            p,
+            d_assignment,
+            sc,
+            i,
+            n);
+      }
     }
   }
   pruneRedundantIntervals(res);
@@ -335,6 +350,10 @@ CACInterval CDCAC::intervalFromCharacterization(
 std::vector<CACInterval> CDCAC::getUnsatCover(std::size_t curVariable,
                                               bool returnFirstInterval)
 {
+  if (isProofEnabled())
+  {
+    d_proof->startRecursive();
+  }
   Trace("cdcac") << "Looking for unsat cover for "
                  << d_variableOrdering[curVariable] << std::endl;
   std::vector<CACInterval> intervals = getUnsatIntervals(curVariable);
@@ -373,6 +392,10 @@ std::vector<CACInterval> CDCAC::getUnsatCover(std::size_t curVariable,
       Trace("cdcac") << "Found full assignment: " << d_assignment << std::endl;
       return {};
     }
+    if (isProofEnabled())
+    {
+      d_proof->startScope();
+    }
     // Recurse to next variable
     auto cov = getUnsatCover(curVariable + 1);
     if (cov.empty())
@@ -391,6 +414,16 @@ std::vector<CACInterval> CDCAC::getUnsatCover(std::size_t curVariable,
         intervalFromCharacterization(characterization, curVariable, sample);
     newInterval.d_origins = collectConstraints(cov);
     intervals.emplace_back(newInterval);
+    if (isProofEnabled())
+    {
+      auto cell = d_proof->constructCell(
+          d_constraints.varMapper()(d_variableOrdering[curVariable]),
+          newInterval,
+          d_assignment,
+          sample,
+          d_constraints.varMapper());
+      d_proof->endScope(cell);
+    }
 
     if (returnFirstInterval)
     {
@@ -421,9 +454,31 @@ std::vector<CACInterval> CDCAC::getUnsatCover(std::size_t curVariable,
       Trace("cdcac") << "-> " << i.d_interval << std::endl;
     }
   }
+  if (isProofEnabled())
+  {
+    d_proof->endRecursive();
+  }
   return intervals;
 }
 
+void CDCAC::startNewProof()
+{
+  if (isProofEnabled())
+  {
+    d_proof->startNewProof();
+  }
+}
+
+ProofGenerator* CDCAC::closeProof(const std::vector<Node>& assertions)
+{
+  if (isProofEnabled())
+  {
+    d_proof->endScope(assertions);
+    return d_proof->getProofGenerator();
+  }
+  return nullptr;
+}
+
 bool CDCAC::checkIntegrality(std::size_t cur_variable, const poly::Value& value)
 {
   Node var = d_constraints.varMapper()(d_variableOrdering[cur_variable]);
@@ -470,7 +525,19 @@ bool CDCAC::hasRootBelow(const poly::Polynomial& p,
 
 void CDCAC::pruneRedundantIntervals(std::vector<CACInterval>& intervals)
 {
-  cleanIntervals(intervals);
+  if (isProofEnabled())
+  {
+    std::vector<CACInterval> allIntervals = intervals;
+    cleanIntervals(intervals);
+    d_proof->pruneChildren([&allIntervals, &intervals](std::size_t i) {
+      return std::find(intervals.begin(), intervals.end(), allIntervals[i])
+             != intervals.end();
+    });
+  }
+  else
+  {
+    cleanIntervals(intervals);
+  }
 }
 
 }  // namespace cad

diff --git a/src/theory/arith/nl/cad/cdcac.h b/src/theory/arith/nl/cad/cdcac.h
index f9294fdf18e1082cabbc5e8e5a22c2f1350f77da..4511d0c55e88d02e999a03ba23bf00564f949955 100644 (file)
--- a/src/theory/arith/nl/cad/cdcac.h
+++ b/src/theory/arith/nl/cad/cdcac.h
@@ -30,6 +30,7 @@
 
 #include "theory/arith/nl/cad/cdcac_utils.h"
 #include "theory/arith/nl/cad/constraints.h"
+#include "theory/arith/nl/cad/proof_generator.h"
 #include "theory/arith/nl/cad/variable_ordering.h"
 #include "theory/arith/nl/nl_model.h"
 
@@ -46,10 +47,10 @@ namespace cad {
 class CDCAC
 {
  public:
-  /** Initialize without a variable ordering. */
-  CDCAC();
   /** Initialize this method with the given variable ordering. */
-  CDCAC(const std::vector<poly::Variable>& ordering);
+  CDCAC(context::Context* ctx,
+        ProofNodeManager* pnm,
+        const std::vector<poly::Variable>& ordering = {});
 
   /** Reset this instance. */
   void reset();
@@ -138,7 +139,20 @@ class CDCAC
   std::vector<CACInterval> getUnsatCover(std::size_t curVariable = 0,
                                          bool returnFirstInterval = false);
 
+  void startNewProof();
+  /**
+   * Finish the generated proof (if proofs are enabled) with a scope over the
+   * given assertions.
+   */
+  ProofGenerator* closeProof(const std::vector<Node>& assertions);
+
+  /** Get the proof generator */
+  CADProofGenerator* getProof() { return d_proof.get(); }
+
  private:
+  /** Check whether proofs are enabled */
+  bool isProofEnabled() const { return d_proof != nullptr; }
+
   /**
    * Check whether the current sample satisfies the integrality condition of the
    * current variable. Returns true if the variable is not integral or the
@@ -187,6 +201,9 @@ class CDCAC
 
   /** The linear assignment used as an initial guess. */
   std::vector<poly::Value> d_initialAssignment;
+
+  /** The proof generator */
+  std::unique_ptr<CADProofGenerator> d_proof;
 };
 
 }  // namespace cad

diff --git a/src/theory/arith/nl/cad_solver.cpp b/src/theory/arith/nl/cad_solver.cpp
index 83ceb1182f481570d6be29734cbe325bd135e19f..74c0457a85fe9ae4a80af26dc8b7c30074874538 100644 (file)
--- a/src/theory/arith/nl/cad_solver.cpp
+++ b/src/theory/arith/nl/cad_solver.cpp
@@ -29,14 +29,31 @@ namespace theory {
 namespace arith {
 namespace nl {
 
-CadSolver::CadSolver(InferenceManager& im, NlModel& model)
-    : d_foundSatisfiability(false), d_im(im), d_model(model)
+CadSolver::CadSolver(InferenceManager& im,
+                     NlModel& model,
+                     context::Context* ctx,
+                     ProofNodeManager* pnm)
+    :
+#ifdef CVC4_POLY_IMP
+      d_CAC(ctx, pnm),
+#endif
+      d_foundSatisfiability(false),
+      d_im(im),
+      d_model(model)
 {
   d_ranVariable =
       NodeManager::currentNM()->mkSkolem("__z",
                                          NodeManager::currentNM()->realType(),
                                          "",
                                          NodeManager::SKOLEM_EXACT_NAME);
+#ifdef CVC4_POLY_IMP
+  ProofChecker* pc = pnm != nullptr ? pnm->getChecker() : nullptr;
+  if (pc != nullptr)
+  {
+    // add checkers
+    d_proofChecker.registerTo(pc);
+  }
+#endif
 }
 
 CadSolver::~CadSolver() {}
@@ -75,6 +92,7 @@ void CadSolver::checkFull()
     Trace("nl-cad") << "No constraints. Return." << std::endl;
     return;
   }
+  d_CAC.startNewProof();
   auto covering = d_CAC.getUnsatCover();
   if (covering.empty())
   {
@@ -88,12 +106,9 @@ void CadSolver::checkFull()
     Trace("nl-cad") << "Collected MIS: " << mis << std::endl;
     Assert(!mis.empty()) << "Infeasible subset can not be empty";
     Trace("nl-cad") << "UNSAT with MIS: " << mis << std::endl;
-    for (auto& n : mis)
-    {
-      n = n.negate();
-    }
-    d_im.addPendingLemma(NodeManager::currentNM()->mkOr(mis),
-                         InferenceId::ARITH_NL_CAD_CONFLICT);
+    Node lem = NodeManager::currentNM()->mkAnd(mis).negate();
+    ProofGenerator* proof = d_CAC.closeProof(mis);
+    d_im.addPendingLemma(lem, InferenceId::ARITH_NL_CAD_CONFLICT, proof);
   }
 #else
   Warning() << "Tried to use CadSolver but libpoly is not available. Compile "

diff --git a/src/theory/arith/nl/cad_solver.h b/src/theory/arith/nl/cad_solver.h
index 4d537213faf104a18d3f63dcd1720b0771bc2cca..21fbbab2e7489d37e46340aa1390642c3b509b48 100644 (file)
--- a/src/theory/arith/nl/cad_solver.h
+++ b/src/theory/arith/nl/cad_solver.h
@@ -20,6 +20,7 @@
 #include "expr/node.h"
 #include "theory/arith/inference_manager.h"
 #include "theory/arith/nl/cad/cdcac.h"
+#include "theory/arith/nl/cad/proof_checker.h"
 #include "theory/arith/nl/nl_model.h"
 
 namespace CVC4 {
@@ -34,7 +35,10 @@ namespace nl {
 class CadSolver
 {
  public:
-  CadSolver(InferenceManager& im, NlModel& model);
+  CadSolver(InferenceManager& im,
+            NlModel& model,
+            context::Context* ctx,
+            ProofNodeManager* pnm);
   ~CadSolver();
 
   /**
@@ -81,6 +85,8 @@ class CadSolver
    * The object implementing the actual decision procedure.
    */
   cad::CDCAC d_CAC;
+  /** The proof checker for cad proofs */
+  cad::CADProofRuleChecker d_proofChecker;
 #endif
   /**
    * Indicates whether we found satisfiability in the last call to

diff --git a/src/theory/arith/nl/nonlinear_extension.cpp b/src/theory/arith/nl/nonlinear_extension.cpp
index 4d29f1955f7278c10c4bfab095d28b890b855804..c46781e76ef1fed6f94f6ed651260efd2d94619a 100644 (file)
--- a/src/theory/arith/nl/nonlinear_extension.cpp
+++ b/src/theory/arith/nl/nonlinear_extension.cpp
@@ -54,7 +54,7 @@ NonlinearExtension::NonlinearExtension(TheoryArith& containing,
       d_monomialSlv(&d_extState),
       d_splitZeroSlv(&d_extState),
       d_tangentPlaneSlv(&d_extState),
-      d_cadSlv(d_im, d_model),
+      d_cadSlv(d_im, d_model, state.getUserContext(), pnm),
       d_icpSlv(d_im),
       d_iandSlv(d_im, state, d_model),
       d_builtModel(containing.getSatContext(), false)