Enable NL tangent planes by default (#8233)

Fixes cvc5/cvc5-projects#215
Fixes cvc5/cvc5-projects#291
Fixes cvc5/cvc5-projects#292
Fixes cvc5/cvc5-projects#294
Fixes cvc5/cvc5-projects#297

Previously the concern was that this would interfere with e.g. quantifiers + non-linear. However, our strategy is now fair wrt other theories as we send lemmas at LAST_CALL effort, and is properly restricted by the nl-ext mode.

Moreover, this option increases our ability to solve problems (instead of saying "unknown") significantly, even for quantified logics like UFNIA.

diff --git a/src/options/arith_options.toml b/src/options/arith_options.toml
index d76f6c97368f52ee8942178014004a7a3b14f251..0061b316e0d1677c5e4efc1b837a70ea1bd45f09 100644 (file)
--- a/src/options/arith_options.toml
+++ b/src/options/arith_options.toml
@@ -398,7 +398,7 @@ name   = "Arithmetic Theory"
   category   = "regular"
   long       = "nl-ext-tplanes"
   type       = "bool"
-  default    = "false"
+  default    = "true"
   help       = "use non-terminating tangent plane strategy for non-linear incremental linearization solver"
 
 [[option]]

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index ea5bc37cdc6883a6ce724177e4d9f2e0a8772ee2..50969c740b727a50079ba8a3bd709c7d1faaed6c 100644 (file)
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -1958,14 +1958,21 @@ set(regress_1_tests
   regress1/nl/pinto-model-core-ni.smt2
   regress1/nl/poly-1025.smt2
   regress1/nl/proj-365-is-int-pi.smt2
+  regress1/nl/proj-issue215.smt2
   regress1/nl/proj-issue231.smt2
   regress1/nl/proj-issue232.smt2
   regress1/nl/proj-issue251.smt2
   regress1/nl/proj-issue253.smt2
+  regress1/nl/proj-issue279.smt2
   regress1/nl/proj-issue280.smt2
   regress1/nl/proj-issue282.smt2
   regress1/nl/proj-issue286.smt2
   regress1/nl/proj-issue290.smt2
+  regress1/nl/proj-issue291.smt2
+  regress1/nl/proj-issue292.smt2
+  regress1/nl/proj-issue294.smt2
+  regress1/nl/proj-issue297.smt2
+  regress1/nl/proj-issue302.smt2
   regress1/nl/quant-nl.smt2
   regress1/nl/red-exp.smt2
   regress1/nl/rewriting-sums.smt2

diff --git a/test/regress/regress0/proofs/proj-issue326-nl-bounds-check.smt2 b/test/regress/regress0/proofs/proj-issue326-nl-bounds-check.smt2
index bc10e9cac008d11e6f8361a37eecdb75a61c8135..9b7074307f080243d899a9294adbf33e9743fc32 100644 (file)
--- a/test/regress/regress0/proofs/proj-issue326-nl-bounds-check.smt2
+++ b/test/regress/regress0/proofs/proj-issue326-nl-bounds-check.smt2
@@ -1,4 +1,5 @@
-; EXPECT: unknown
+; COMMAND-LINE: -q
+; EXPECT: sat
 (set-logic ALL)
 (set-option :check-proofs true)
 (set-option :proof-check eager)

diff --git a/test/regress/regress1/nl/proj-issue215.smt2 b/test/regress/regress1/nl/proj-issue215.smt2
new file mode 100644 (file)
index 0000000..2495189
--- /dev/null
+++ b/test/regress/regress1/nl/proj-issue215.smt2
@@ -0,0 +1,12 @@
+(set-logic ALL)
+(set-info :status sat)
+(declare-fun a () Real)
+(declare-fun b () Real)
+(declare-fun c () Real)
+(declare-fun d () Real)
+(declare-fun f () Real)
+(declare-fun g () Real)
+(assert (= (* c f c) a (- d f)))
+(assert (= d (/ a f)))
+(assert (distinct f 0 (/ b g) g))
+(check-sat)

diff --git a/test/regress/regress1/nl/proj-issue279.smt2 b/test/regress/regress1/nl/proj-issue279.smt2
new file mode 100644 (file)
index 0000000..09ae1d3
--- /dev/null
+++ b/test/regress/regress1/nl/proj-issue279.smt2
@@ -0,0 +1,5 @@
+(set-logic ALL)
+(set-info :status sat)
+(declare-const s Real)
+(assert (or (or false (= 0.0 s)) (< (* s (+ 6 (* s 12))) (- 1))))
+(check-sat)

diff --git a/test/regress/regress1/nl/proj-issue291.smt2 b/test/regress/regress1/nl/proj-issue291.smt2
new file mode 100644 (file)
index 0000000..2a43414
--- /dev/null
+++ b/test/regress/regress1/nl/proj-issue291.smt2
@@ -0,0 +1,6 @@
+(set-logic ALL)
+(set-info :status sat)
+(declare-const x1 Real)
+(declare-fun s () Real)
+(assert (and (> (* x1 s x1) 1) (exists ((x Bool)) (=> (not true) false))))
+(check-sat)

diff --git a/test/regress/regress1/nl/proj-issue292.smt2 b/test/regress/regress1/nl/proj-issue292.smt2
new file mode 100644 (file)
index 0000000..fc43486
--- /dev/null
+++ b/test/regress/regress1/nl/proj-issue292.smt2
@@ -0,0 +1,7 @@
+(set-logic ALL)
+(set-info :status sat)
+(declare-const x Real)
+(declare-const u Real)
+(declare-const v Real)
+(assert (exists ((t Real)) (and (>= x (- 1.0)) (not (or (< t 0.0) (= t (* u t v)))))))
+(check-sat)

diff --git a/test/regress/regress1/nl/proj-issue294.smt2 b/test/regress/regress1/nl/proj-issue294.smt2
new file mode 100644 (file)
index 0000000..c468f7e
--- /dev/null
+++ b/test/regress/regress1/nl/proj-issue294.smt2
@@ -0,0 +1,5 @@
+(set-logic ALL)
+(set-info :status sat)
+(declare-fun c () Int)
+(assert (= (> c 1) (= 6 (* c c))))
+(check-sat)

diff --git a/test/regress/regress1/nl/proj-issue297.smt2 b/test/regress/regress1/nl/proj-issue297.smt2
new file mode 100644 (file)
index 0000000..9e34fe8
--- /dev/null
+++ b/test/regress/regress1/nl/proj-issue297.smt2
@@ -0,0 +1,6 @@
+(set-logic ALL)
+(set-info :status sat)
+(declare-const x1 Bool)
+(declare-const x Int)
+(assert (ite (= 3 (* x (ite (< x 1) x 0))) true x1))
+(check-sat)

diff --git a/test/regress/regress1/nl/proj-issue302.smt2 b/test/regress/regress1/nl/proj-issue302.smt2
new file mode 100644 (file)
index 0000000..44939c1
--- /dev/null
+++ b/test/regress/regress1/nl/proj-issue302.smt2
@@ -0,0 +1,6 @@
+(set-logic ALL)
+(set-info :status sat)
+(declare-fun s () Real)
+(declare-fun k () Real)
+(assert (>= (* s k) 1))
+(check-sat)