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.

1 files changed, 17 insertions, 1 deletions

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 "