Add CAD-based solver (#4834)

Based on #4774, this PR adds a new CadSolver class that allows the NonlinearExtension to actually employ the CAD-based method. In more detail:

add --nl-cad option
add CadSolver class that wraps cad::CDCAC with support for checks, model construction and conflict generation
add new Inference types for the NlLemma class
use CadSolver in NonlinearExtension (if --nl-cad is given)

1 files changed, 19 insertions, 1 deletions

diff --git a/src/theory/arith/nl/nonlinear_extension.cpp b/src/theory/arith/nl/nonlinear_extension.cpp
index 4cb1c9fe6..9dbb95d93 100644
--- a/src/theory/arith/nl/nonlinear_extension.cpp
+++ b/src/theory/arith/nl/nonlinear_extension.cpp
@@ -42,6 +42,7 @@ NonlinearExtension::NonlinearExtension(TheoryArith& containing,
       d_model(containing.getSatContext()),
       d_trSlv(d_model),
       d_nlSlv(containing, d_model),
+      d_cadSlv(containing, d_model),
       d_iandSlv(containing, d_model),
       d_builtModel(containing.getSatContext(), false)
 {
@@ -406,6 +407,10 @@ bool NonlinearExtension::checkModel(const std::vector<Node>& assertions,
       return false;
     }
   }
+  if (options::nlCad())
+  {
+    d_cadSlv.constructModelIfAvailable(passertions);
+  }
 
   Trace("nl-ext-cm") << "-----" << std::endl;
   unsigned tdegree = d_trSlv.getTaylorDegree();
@@ -433,7 +438,11 @@ int NonlinearExtension::checkLastCall(const std::vector<Node>& assertions,
     // process lemmas that may have been generated by the transcendental solver
     filterLemmas(lemmas, lems);
   }
-  
+  if (options::nlCad())
+  {
+    d_cadSlv.initLastCall(assertions);
+  }
+
   // init last call with IAND
   d_iandSlv.initLastCall(assertions, false_asserts, xts);
   
@@ -594,6 +603,15 @@ int NonlinearExtension::checkLastCall(const std::vector<Node>& assertions,
       filterLemmas(lemmas, wlems);
     }
   }
+  if (options::nlCad())
+  {
+    lemmas = d_cadSlv.checkFull();
+    if (lemmas.empty())
+    {
+      Trace("nl-cad") << "nl-cad found SAT!" << std::endl;
+    }
+    filterLemmas(lemmas, wlems);
+  }
   // run the full refinement in the IAND solver
   lemmas = d_iandSlv.checkFullRefine();
   filterLemmas(lemmas, wlems);