From e099e59f544d204ff74b2a8f26994795a2d6fb3e Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Fri, 4 Mar 2022 18:47:13 -0600 Subject: [PATCH] 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. --- src/options/arith_options.toml | 2 +- test/regress/CMakeLists.txt | 7 +++++++ .../proofs/proj-issue326-nl-bounds-check.smt2 | 3 ++- test/regress/regress1/nl/proj-issue215.smt2 | 12 ++++++++++++ test/regress/regress1/nl/proj-issue279.smt2 | 5 +++++ test/regress/regress1/nl/proj-issue291.smt2 | 6 ++++++ test/regress/regress1/nl/proj-issue292.smt2 | 7 +++++++ test/regress/regress1/nl/proj-issue294.smt2 | 5 +++++ test/regress/regress1/nl/proj-issue297.smt2 | 6 ++++++ test/regress/regress1/nl/proj-issue302.smt2 | 6 ++++++ 10 files changed, 57 insertions(+), 2 deletions(-) create mode 100644 test/regress/regress1/nl/proj-issue215.smt2 create mode 100644 test/regress/regress1/nl/proj-issue279.smt2 create mode 100644 test/regress/regress1/nl/proj-issue291.smt2 create mode 100644 test/regress/regress1/nl/proj-issue292.smt2 create mode 100644 test/regress/regress1/nl/proj-issue294.smt2 create mode 100644 test/regress/regress1/nl/proj-issue297.smt2 create mode 100644 test/regress/regress1/nl/proj-issue302.smt2 diff --git a/src/options/arith_options.toml b/src/options/arith_options.toml index d76f6c973..0061b316e 100644 --- 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 ea5bc37cd..50969c740 100644 --- 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 bc10e9cac..9b7074307 100644 --- 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 index 000000000..24951890e --- /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 index 000000000..09ae1d378 --- /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 index 000000000..2a43414c4 --- /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 index 000000000..fc43486ac --- /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 index 000000000..c468f7e7c --- /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 index 000000000..9e34fe8b3 --- /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 index 000000000..44939c12b --- /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) -- 2.30.2