Prevent using the coverings solver with extended operators (#8523)

The way we construct the model within the nonlinear extension makes using multiple subsolvers that contribute to the model potentially unsound. This PR prevent the coverings solver from being used if extended operators are present, unless --nl-cov-force is given.
Fixes #8515. Fixes #8516.

diff --git a/src/options/arith_options.toml b/src/options/arith_options.toml
index 74a2caa06b8bc067b20370764be8bbc0ee6fa3e8..4461a69df2cddebe6baab8a48f1d33cbbf92de3a 100644 (file)
--- a/src/options/arith_options.toml
+++ b/src/options/arith_options.toml
@@ -500,6 +500,14 @@ name   = "Arithmetic Theory"
   default    = "false"
   help       = "whether to use the cylindrical algebraic coverings solver for non-linear arithmetic"
 
+[[option]]
+  name       = "nlCovForce"
+  category   = "expert"
+  long       = "nl-cov-force"
+  type       = "bool"
+  default    = "false"
+  help       = "forces using the cylindrical algebraic coverings solver, even in cases where it is possibly not safe to do so"
+
 [[option]]
   name       = "nlCovVarElim"
   category   = "expert"

diff --git a/src/smt/set_defaults.cpp b/src/smt/set_defaults.cpp
index b3a8007a13ae792eb0c4a103b8084953d59adc52..9f3ffa98d959283c3b74ac6e89fc6185c59b5a32 100644 (file)
--- a/src/smt/set_defaults.cpp
+++ b/src/smt/set_defaults.cpp
@@ -815,7 +815,8 @@ void SetDefaults::setDefaultsPost(const LogicInfo& logic, Options& opts) const
     }
   }
   else if (logic.isQuantified() && logic.isTheoryEnabled(theory::THEORY_ARITH)
-           && logic.areRealsUsed() && !logic.areIntegersUsed())
+           && logic.areRealsUsed() && !logic.areIntegersUsed()
+           && !logic.areTranscendentalsUsed())
   {
     if (!opts.arith.nlCov && !opts.arith.nlCovWasSetByUser)
     {

diff --git a/src/theory/arith/nl/nonlinear_extension.cpp b/src/theory/arith/nl/nonlinear_extension.cpp
index 3b17426884d80d26c5fe59259d32c2a7f40050e4..6a0810adbce6dd213d7c3873146e58556b5ec079 100644 (file)
--- a/src/theory/arith/nl/nonlinear_extension.cpp
+++ b/src/theory/arith/nl/nonlinear_extension.cpp
@@ -102,6 +102,17 @@ void NonlinearExtension::preRegisterTerm(TNode n)
       throw LogicException(ss.str());
     }
   }
+  if (isTranscendentalKind(k) || k == Kind::IAND || k == Kind::POW2)
+  {
+    if (options().arith.nlCov && !options().arith.nlCovForce)
+    {
+      std::stringstream ss;
+      ss << "Term of kind " << printer::smt2::Smt2Printer::smtKindString(k)
+         << " is not compatible with using the coverings-based solver. If you know what you are doing, "
+          "you can try --nl-cov-force, but expect crashes or incorrect results.";
+      throw LogicException(ss.str());
+    }
+  }
 }
 
 void NonlinearExtension::processSideEffect(const NlLemma& se)

diff --git a/test/regress/cli/CMakeLists.txt b/test/regress/cli/CMakeLists.txt
index c58f0948d9cd561a19f1c7c18374e2a2414d98ac..f06d6a91316a6b413cb0bbbdf439693f7f29315a 100644 (file)
--- a/test/regress/cli/CMakeLists.txt
+++ b/test/regress/cli/CMakeLists.txt
@@ -797,6 +797,8 @@ set(regress_0_tests
   regress0/nl/issue8161-var-elim.smt2
   regress0/nl/issue8226-ran-refinement.smt2
   regress0/nl/issue8414-ran-rational.smt2
+  regress0/nl/issue8515-cov-iand.smt2
+  regress0/nl/issue8516-cov-sin.smt2
   regress0/nl/lazard-spurious-root.smt2
   regress0/nl/magnitude-wrong-1020-m.smt2
   regress0/nl/mult-po.smt2

diff --git a/test/regress/cli/regress0/nl/issue8515-cov-iand.smt2 b/test/regress/cli/regress0/nl/issue8515-cov-iand.smt2
new file mode 100644 (file)
index 0000000..523650a
--- /dev/null
+++ b/test/regress/cli/regress0/nl/issue8515-cov-iand.smt2
@@ -0,0 +1,12 @@
+; REQUIRES: poly
+; SCRUBBER: grep -o "Term of kind iand is not compatible"
+; EXPECT: Term of kind iand is not compatible
+; EXIT: 1
+(set-logic ALL)
+(set-option :nl-cov true)
+(set-option :check-models true)
+(declare-fun v () Int)
+(declare-fun a () Int)
+(declare-fun va () Int)
+(assert (and (= 1 (div 0 va)) (> 0 ((_ iand 1) v a))))
+(check-sat)

diff --git a/test/regress/cli/regress0/nl/issue8516-cov-sin.smt2 b/test/regress/cli/regress0/nl/issue8516-cov-sin.smt2
new file mode 100644 (file)
index 0000000..5304efa
--- /dev/null
+++ b/test/regress/cli/regress0/nl/issue8516-cov-sin.smt2
@@ -0,0 +1,8 @@
+; REQUIRES: poly
+; SCRUBBER: grep -o "Term of kind sin is not compatible"
+; EXPECT: Term of kind sin is not compatible
+; EXIT: 1
+(set-logic NRAT)
+(set-option :nl-cov true)
+(assert (exists ((r Real)) (distinct 0.0 (sin 1.0))))
+(check-sat)