From 0a58942a2eb87fd7e10d0cf2b54f2e7d0b9e5c26 Mon Sep 17 00:00:00 2001
From: Gereon Kremer <gkremer@cs.stanford.edu>
Date: Sat, 2 Apr 2022 00:24:16 +0200
Subject: [PATCH] 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.
---
 src/options/arith_options.toml                       |  8 ++++++++
 src/smt/set_defaults.cpp                             |  3 ++-
 src/theory/arith/nl/nonlinear_extension.cpp          | 11 +++++++++++
 test/regress/cli/CMakeLists.txt                      |  2 ++
 test/regress/cli/regress0/nl/issue8515-cov-iand.smt2 | 12 ++++++++++++
 test/regress/cli/regress0/nl/issue8516-cov-sin.smt2  |  8 ++++++++
 6 files changed, 43 insertions(+), 1 deletion(-)
 create mode 100644 test/regress/cli/regress0/nl/issue8515-cov-iand.smt2
 create mode 100644 test/regress/cli/regress0/nl/issue8516-cov-sin.smt2

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)
-- 
2.30.2