Generalize check-model in NonLinearExtension for quadratic equations (#1892)

6 files changed, 45 insertions, 3 deletions

diff --git a/test/regress/Makefile.tests b/test/regress/Makefile.tests
index 4324171a8..bd5002921 100644
--- a/test/regress/Makefile.tests
+++ b/test/regress/Makefile.tests
@@ -1106,6 +1106,8 @@ REG1_TESTS = \
 	regress1/lemmas/pursuit-safety-8.smt \
 	regress1/lemmas/simple_startup_9nodes.abstract.base.smt \
 	regress1/nl/NAVIGATION2.smt2 \
+	regress1/nl/approx-sqrt.smt2 \
+	regress1/nl/approx-sqrt-unsat.smt2 \
 	regress1/nl/arctan2-expdef.smt2 \
 	regress1/nl/arrowsmith-050317.smt2 \
 	regress1/nl/bad-050217.smt2 \
@@ -1151,6 +1153,7 @@ REG1_TESTS = \
 	regress1/nl/sin1-ub.smt2 \
 	regress1/nl/sin2-lb.smt2 \
 	regress1/nl/sin2-ub.smt2 \
+	regress1/nl/solve-eq-small-qf-nra.smt2 \
 	regress1/nl/sqrt-problem-1.smt2 \
 	regress1/nl/sugar-ident-2.smt2 \
 	regress1/nl/sugar-ident-3.smt2 \
diff --git a/test/regress/regress1/nl/approx-sqrt-unsat.smt2 b/test/regress/regress1/nl/approx-sqrt-unsat.smt2
new file mode 100644
index 000000000..af3eda65a
--- /dev/null
+++ b/test/regress/regress1/nl/approx-sqrt-unsat.smt2
@@ -0,0 +1,11 @@
+(set-logic QF_NRA)
+(set-info :status unsat)
+(declare-fun x () Real)
+(assert (= (* x x) 2))
+(assert (> x 0))
+(assert (or 
+(> (+ (* x x) (* (- 2.8) x)) (- 1.95))
+(> (+ (* x x) (* (- 2.8284271247) x)) (- 1.999999))
+(> (+ (* x x) (* (- 2.82842712475) x)) (- 2.0000000000000000000000000001))
+))
+(check-sat)
diff --git a/test/regress/regress1/nl/approx-sqrt.smt2 b/test/regress/regress1/nl/approx-sqrt.smt2
new file mode 100644
index 000000000..4ff659bc1
--- /dev/null
+++ b/test/regress/regress1/nl/approx-sqrt.smt2
@@ -0,0 +1,11 @@
+; COMMAND-LINE: --no-check-models
+; EXPECT: sat
+(set-logic QF_NRA)
+(set-info :status sat)
+(declare-fun x () Real)
+(assert (= (* x x) 2))
+(assert (> x 0))
+(assert (> (+ (* x x) (* (- 2.8) x)) (- 1.9598)))
+(assert (> (+ (* x x) (* (- 2.8284271247) x)) (- 1.9999999999999)))
+(assert (> (+ (* x x) (* (- 2.82842712475) x)) (- 2.00000001)))
+(check-sat)
diff --git a/test/regress/regress1/nl/cos1-tc.smt2 b/test/regress/regress1/nl/cos1-tc.smt2
index f910f0c58..3bf15c384 100644
--- a/test/regress/regress1/nl/cos1-tc.smt2
+++ b/test/regress/regress1/nl/cos1-tc.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --nl-ext --no-nl-ext-tf-tplanes --no-nl-ext-tf-inc-prec
+; COMMAND-LINE: --nl-ext --no-nl-ext-tf-tplanes --no-nl-ext-inc-prec
 ; EXPECT: unknown
 (set-logic UFNRA)
 (declare-fun f (Real) Real)
diff --git a/test/regress/regress1/nl/solve-eq-small-qf-nra.smt2 b/test/regress/regress1/nl/solve-eq-small-qf-nra.smt2
new file mode 100644
index 000000000..fe4625af7
--- /dev/null
+++ b/test/regress/regress1/nl/solve-eq-small-qf-nra.smt2
@@ -0,0 +1,17 @@
+; COMMAND-LINE: --no-check-models
+; EXPECT: sat
+(set-info :smt-lib-version 2.6)
+(set-logic QF_NRA)
+(set-info :status sat)
+(declare-fun skoS3 () Real)
+(declare-fun skoSX () Real)
+(declare-fun skoX () Real)
+(assert (and 
+(not (= (* skoX (* skoX (- 80))) (+ 75 (* skoSX (* skoSX (- 1)))))) 
+(= (* skoS3 skoS3) 3) 
+(not (<= skoX 0)) 
+(not (<= skoSX 0)) 
+(not (<= skoS3 0))
+))
+; cannot construct an exact model, but can reason that this is SAT based on approximation
+(check-sat)
diff --git a/test/regress/regress1/sqrt2-sort-inf-unk.smt2 b/test/regress/regress1/sqrt2-sort-inf-unk.smt2
index f4b15020a..d9489eee7 100644
--- a/test/regress/regress1/sqrt2-sort-inf-unk.smt2
+++ b/test/regress/regress1/sqrt2-sort-inf-unk.smt2
@@ -1,5 +1,5 @@
-; COMMAND-LINE: --sort-inference
-; EXPECT: unknown
+; COMMAND-LINE: --sort-inference --no-check-models
+; EXPECT: sat
 (set-logic QF_NRA)
 (declare-fun x () Real)
 (assert (= (* x x) 2.0))