diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-10-18 19:37:11 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2018-10-18 19:37:11 -0500 |
| commit | 547bd91e189b28da9950e12037d1e88079157479 (patch) | |
| tree | 7f225e6df081071028c9e6102c902a6224179edf /test | |
| parent | 10707e3ec6f2cab793919f2d1a159e13cdd032a9 (diff) | |
Non-implied mode for model cores (#2653)
Diffstat (limited to 'test')
| -rw-r--r-- | test/regress/CMakeLists.txt | 1 | ||||
| -rw-r--r-- | test/regress/regress0/model-core.smt2 | 3 | ||||
| -rw-r--r-- | test/regress/regress1/nl/pinto-model-core-ni.smt2 | 22 |
3 files changed, 25 insertions, 1 deletions
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index a41108a71..cd98a8917 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -1183,6 +1183,7 @@ set(regress_1_tests regress1/nl/nl-unk-quant.smt2 regress1/nl/nl_uf_lalt.smt2 regress1/nl/ones.smt2 + regress1/nl/pinto-model-core-ni.smt2 regress1/nl/poly-1025.smt2 regress1/nl/quant-nl.smt2 regress1/nl/red-exp.smt2 diff --git a/test/regress/regress0/model-core.smt2 b/test/regress/regress0/model-core.smt2 index 6729cb5e0..fca80a960 100644 --- a/test/regress/regress0/model-core.smt2 +++ b/test/regress/regress0/model-core.smt2 @@ -1,4 +1,5 @@ -; COMMAND-LINE: --produce-model-cores +; COMMAND-LINE: --produce-models --model-cores=simple +; COMMAND-LINE: --produce-models --model-core=non-implied ; EXPECT: sat (set-logic QF_UFLIA) (declare-fun x () Int) diff --git a/test/regress/regress1/nl/pinto-model-core-ni.smt2 b/test/regress/regress1/nl/pinto-model-core-ni.smt2 new file mode 100644 index 000000000..1e09f8439 --- /dev/null +++ b/test/regress/regress1/nl/pinto-model-core-ni.smt2 @@ -0,0 +1,22 @@ +; COMMAND-LINE: --nl-ext-tplanes --produce-models --model-core=non-implied +; EXPECT: sat +(set-logic ALL) +(declare-fun i1 () Real) +(declare-fun i2 () Real) +(declare-fun n () Int) +(declare-fun x () Int) +(declare-fun y () Int) +(declare-fun i11 () Real) +(declare-fun i21 () Real) + +(assert (>= n 1)) +(assert (and (<= 1 x)(<= x n))) +(assert (and (<= 1 y)(<= y n))) +(assert (or (= (/ (* (- 1) x) n) i1)(= i1 (/ x n)))) +(assert (or (= (/ (* (- 1) y) n) i2)(= i2 (/ y n)))) + +(assert (and (= i1 i11) (= i2 i21) )) + +(assert (not (and (or (= (- 1) i11 )(= i11 1)) (or (= (- 1) i21)(= i21 1)) ))) + +(check-sat) |