ICP-based solver for nonlinear arithmetic (#5017)

This PR adds a new icp-based solver to be integrated into the nonlinear extension.
It is not meant to be used as a stand-alone ICP solver. It does not implement splits (only propagations) and implements a rather aggressive budget mechanism that aims to quickly stop propagation to allow other solvers to take over. Additionally, it enforces a maximum bit size to avoid divergence.

1 files changed, 17 insertions, 1 deletions

diff --git a/src/theory/arith/nl/nonlinear_extension.cpp b/src/theory/arith/nl/nonlinear_extension.cpp
index df3a304be..05442a566 100644
--- a/src/theory/arith/nl/nonlinear_extension.cpp
+++ b/src/theory/arith/nl/nonlinear_extension.cpp
@@ -47,6 +47,7 @@ NonlinearExtension::NonlinearExtension(TheoryArith& containing,
       d_trSlv(d_im, d_model),
       d_nlSlv(containing, d_model),
       d_cadSlv(d_im, d_model),
+      d_icpSlv(d_im),
       d_iandSlv(containing, d_model),
       d_builtModel(containing.getSatContext(), false)
 {
@@ -381,6 +382,21 @@ int NonlinearExtension::checkLastCall(const std::vector<Node>& assertions,
     }
   }
 
+  if (options::nlICP())
+  {
+    d_icpSlv.reset(assertions);
+    d_icpSlv.check();
+
+    if (d_im.hasUsed())
+    {
+      Trace("nl-ext") << "  ...finished with "
+                      << d_im.numPendingLemmas() + d_im.numSentLemmas()
+                      << " new lemmas from ICP." << std::endl;
+      return d_im.numPendingLemmas() + d_im.numSentLemmas();
+    }
+    Trace("nl-ext") << "Done with ICP" << std::endl;
+  }
+
   if (options::nlExt())
   {
     // initialize the non-linear solver
@@ -758,7 +774,7 @@ bool NonlinearExtension::modelBasedRefinement(std::vector<NlLemma>& mlems)
         d_builtModel = true;
       }
       filterLemmas(lemmas, mlems);
-      if (!mlems.empty())
+      if (!mlems.empty() || d_im.hasPendingLemma())
       {
         return true;
       }