From b9c38b2a878841a1288b1e2279b1ecb74727eeab Mon Sep 17 00:00:00 2001
From: Gereon Kremer <gereon.kremer@cs.rwth-aachen.de>
Date: Tue, 27 Oct 2020 13:57:55 +0100
Subject: [PATCH] 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.
---
 src/options/arith_options.toml                |  3 +-
 src/smt/set_defaults.cpp                      | 30 +++++++++++++++++++
 src/theory/arith/nl/cad_solver.cpp            | 18 ++++++++++-
 test/regress/regress1/nl/iand-native-1.smt2   |  4 +--
 .../nl/issue3300-approx-sqrt-witness.smt2     |  2 +-
 5 files changed, 51 insertions(+), 6 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 "
diff --git a/test/regress/regress1/nl/iand-native-1.smt2 b/test/regress/regress1/nl/iand-native-1.smt2
index e6a25bcc4..0f50dcaed 100644
--- a/test/regress/regress1/nl/iand-native-1.smt2
+++ b/test/regress/regress1/nl/iand-native-1.smt2
@@ -1,5 +1,5 @@
-; COMMAND-LINE: --iand-mode=value
-; COMMAND-LINE: --iand-mode=sum --bvand-integer-granularity=1 --finite-model-find
+; COMMAND-LINE: --iand-mode=value --no-check-models
+; COMMAND-LINE: --iand-mode=sum --bvand-integer-granularity=1 --finite-model-find --no-check-models
 ; EXPECT: sat
 (set-logic QF_NIA)
 (set-info :status sat)
diff --git a/test/regress/regress1/nl/issue3300-approx-sqrt-witness.smt2 b/test/regress/regress1/nl/issue3300-approx-sqrt-witness.smt2
index 3a4332176..512c8d2e1 100644
--- a/test/regress/regress1/nl/issue3300-approx-sqrt-witness.smt2
+++ b/test/regress/regress1/nl/issue3300-approx-sqrt-witness.smt2
@@ -1,4 +1,4 @@
-; SCRUBBER: sed -e 's/BOUND_VARIABLE_[0-9]*/BOUND_VARIABLE/; s/((x (witness ((BOUND_VARIABLE Real)) (or (= BOUND_VARIABLE.*/SUCCESS/'
+; SCRUBBER: sed -e 's/BOUND_VARIABLE_[0-9]*/BOUND_VARIABLE/; s/((x (witness ((BOUND_VARIABLE Real)) (.*/SUCCESS/'
 ; COMMAND-LINE: --produce-models --model-witness-value --no-check-models
 ; EXPECT: sat
 ; EXPECT: SUCCESS
-- 
2.30.2