(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.

1 files changed, 23 insertions, 8 deletions

diff --git a/src/theory/arith/nl/cad_solver.cpp b/src/theory/arith/nl/cad_solver.cpp
index 83ceb1182..74c0457a8 100644
--- 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 "