From: Gereon Kremer <gkremer@cs.stanford.edu>
Date: Fri, 1 Apr 2022 22:24:16 +0000 (+0200)
Subject: Prevent using the coverings solver with extended operators (#8523)
X-Git-Tag: cvc5-1.0.0~51
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=0a58942a2eb87fd7e10d0cf2b54f2e7d0b9e5c26;p=cvc5.git

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 74a2caa06..4461a69df 100644
--- 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 b3a8007a1..9f3ffa98d 100644
--- 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 3b1742688..6a0810adb 100644
--- 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 c58f0948d..f06d6a913 100644
--- 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
index 000000000..523650ab9
--- /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
index 000000000..5304efacf
--- /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)