Enable --nl-cad by default (#5345)

This PR enables `--nl-cad` for QF_NRA (and QF_UFNRA) by default to improve nonlinear arithmetic solving.
Furthermore, it takes care of disabling it when libpoly is not available. It also adds a fix to the CadSolver that avoids incorrect SATs in the presence of theory combination.

3 files changed, 48 insertions, 3 deletions

diff --git a/src/options/arith_options.toml b/src/options/arith_options.toml
index fad1b3dcd..f99c8df90 100644
--- a/src/options/arith_options.toml
+++ b/src/options/arith_options.toml
@@ -433,7 +433,6 @@ header = "options/arith_options.h"
   long       = "nl-ext"
   type       = "bool"
   default    = "true"
-  read_only  = true
   help       = "incremental linearization approach to non-linear"
 
 [[option]]
@@ -564,7 +563,7 @@ header = "options/arith_options.h"
   category   = "regular"
   long       = "nl-cad"
   type       = "bool"
-  default    = "false"
+  default    = "true"
   help       = "whether to use the cylindrical algebraic decomposition solver for non-linear arithmetic"
 
 [[option]]
diff --git a/src/smt/set_defaults.cpp b/src/smt/set_defaults.cpp
index 27959a6bc..7a206e2aa 100644
--- a/src/smt/set_defaults.cpp
+++ b/src/smt/set_defaults.cpp
@@ -1437,6 +1437,36 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
   {
     throw OptionException("--proof-new is not yet supported.");
   }
+
+  if (logic == LogicInfo("QF_UFNRA"))
+  {
+#ifdef CVC4_USE_POLY
+    if (!options::nlCad() && !options::nlCad.wasSetByUser())
+    {
+      options::nlCad.set(true);
+      options::nlExt.set(false);
+      options::nlRlvMode.set(options::NlRlvMode::INTERLEAVE);
+    }
+#endif
+  }
+#ifndef CVC4_USE_POLY
+  if (options::nlCad())
+  {
+    if (options::nlCad.wasSetByUser())
+    {
+      std::stringstream ss;
+      ss << "Cannot use " << options::nlCad.getName() << " without configuring with --poly.";
+      throw OptionException(ss.str());
+    }
+    else
+    {
+      Notice() << "Cannot use --" << options::nlCad.getName()
+               << " without configuring with --poly." << std::endl;
+      options::nlCad.set(false);
+      options::nlExt.set(true);
+    }
+  }
+#endif
 }
 
 }  // namespace smt
diff --git a/src/theory/arith/nl/cad_solver.cpp b/src/theory/arith/nl/cad_solver.cpp
index b63a8398c..d12a861ac 100644
--- a/src/theory/arith/nl/cad_solver.cpp
+++ b/src/theory/arith/nl/cad_solver.cpp
@@ -18,6 +18,7 @@
 #include <poly/polyxx.h>
 #endif
 
+#include "options/arith_options.h"
 #include "theory/arith/inference_id.h"
 #include "theory/arith/nl/cad/cdcac.h"
 #include "theory/arith/nl/poly_conversion.h"
@@ -145,10 +146,15 @@ bool CadSolver::constructModelIfAvailable(std::vector<Node>& assertions)
   {
     return false;
   }
-  assertions.clear();
+  bool foundNonVariable = false;
   for (const auto& v : d_CAC.getVariableOrdering())
   {
     Node variable = d_CAC.getConstraints().varMapper()(v);
+    if (!variable.isVar())
+    {
+      Trace("nl-cad") << "Not a variable: " << variable << std::endl;
+      foundNonVariable = true;
+    }
     Node value = value_to_node(d_CAC.getModel().get(v), d_ranVariable);
     if (value.isConst())
     {
@@ -160,6 +166,16 @@ bool CadSolver::constructModelIfAvailable(std::vector<Node>& assertions)
     }
     Trace("nl-cad") << "-> " << v << " = " << value << std::endl;
   }
+  if (foundNonVariable)
+  {
+    Trace("nl-cad")
+        << "Some variable was an extended term, don't clear list of assertions."
+        << std::endl;
+    return false;
+  }
+  Trace("nl-cad") << "Constructed a full assignment, clear list of assertions."
+                  << std::endl;
+  assertions.clear();
   return true;
 #else
   Warning() << "Tried to use CadSolver but libpoly is not available. Compile "