diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-05-23 07:00:40 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2018-05-23 07:00:40 -0500 |
| commit | 8de9510b8aa818f555294ebe88d9733cc10ff8b9 (patch) | |
| tree | dd4fae3e483be9d9ec0176f3122d58b0df957389 /test/regress/regress1/nl | |
| parent | 4576b47b4acbae79c0ea76ebdc103f4c3155c4ab (diff) | |
Generalize check-model in NonLinearExtension for quadratic equations (#1892)
Diffstat (limited to 'test/regress/regress1/nl')
| -rw-r--r-- | test/regress/regress1/nl/approx-sqrt-unsat.smt2 | 11 | ||||
| -rw-r--r-- | test/regress/regress1/nl/approx-sqrt.smt2 | 11 | ||||
| -rw-r--r-- | test/regress/regress1/nl/cos1-tc.smt2 | 2 | ||||
| -rw-r--r-- | test/regress/regress1/nl/solve-eq-small-qf-nra.smt2 | 17 |
4 files changed, 40 insertions, 1 deletions
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) |