diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2017-04-21 09:26:04 -0500 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2017-04-21 09:26:19 -0500 |
commit | a33dac29d9cc8520f62b6e4f4f9138ea4e3fbcd4 (patch) | |
tree | b92bc3f34aca16a4b4ed6d42b2c2ae909dff17d4 /test | |
parent | 8a0d2b0577e174d2078026129dd01ea46f7f984a (diff) |
Handle subtypes in sets. Bug fixes for tuples with subtypes.
Diffstat (limited to 'test')
-rw-r--r-- | test/regress/regress0/datatypes/Makefile.am | 3 | ||||
-rw-r--r-- | test/regress/regress0/datatypes/tuple-no-clash.cvc | 11 | ||||
-rw-r--r-- | test/regress/regress0/rels/atom_univ2.cvc | 1 | ||||
-rw-r--r-- | test/regress/regress0/sets/Makefile.am | 7 | ||||
-rw-r--r-- | test/regress/regress0/sets/complement.cvc | 1 | ||||
-rw-r--r-- | test/regress/regress0/sets/complement2.cvc | 1 | ||||
-rw-r--r-- | test/regress/regress0/sets/complement3.cvc | 3 | ||||
-rw-r--r-- | test/regress/regress0/sets/int-real-univ-unsat.smt2 | 16 | ||||
-rw-r--r-- | test/regress/regress0/sets/int-real-univ.smt2 | 16 | ||||
-rw-r--r-- | test/regress/regress0/sets/nonvar-univ.smt2 | 2 | ||||
-rw-r--r-- | test/regress/regress0/sets/pre-proc-univ.smt2 | 2 | ||||
-rw-r--r-- | test/regress/regress0/sets/sets-poly-int-real.smt2 | 17 | ||||
-rw-r--r-- | test/regress/regress0/sets/sets-poly-nonint.smt2 | 11 | ||||
-rw-r--r-- | test/regress/regress0/sets/sets-tuple-poly.cvc | 18 | ||||
-rw-r--r-- | test/regress/regress0/sets/univset-simp.smt2 | 2 |
15 files changed, 108 insertions, 3 deletions
diff --git a/test/regress/regress0/datatypes/Makefile.am b/test/regress/regress0/datatypes/Makefile.am index d9db39b40..caf1fc61c 100644 --- a/test/regress/regress0/datatypes/Makefile.am +++ b/test/regress/regress0/datatypes/Makefile.am @@ -79,7 +79,8 @@ TESTS = \ dt-sel-2.6.smt2 \ dt-param-2.6.smt2 \ dt-color-2.6.smt2 \ - dt-match-pat-param-2.6.smt2 + dt-match-pat-param-2.6.smt2 \ + tuple-no-clash.cvc FAILING_TESTS = \ datatype-dump.cvc diff --git a/test/regress/regress0/datatypes/tuple-no-clash.cvc b/test/regress/regress0/datatypes/tuple-no-clash.cvc new file mode 100644 index 000000000..4d7345a54 --- /dev/null +++ b/test/regress/regress0/datatypes/tuple-no-clash.cvc @@ -0,0 +1,11 @@ +% EXPECT: sat +OPTION "logic" "ALL_SUPPORTED"; + +x : [ REAL, REAL ]; +y : REAL; +z : REAL; + +ASSERT x = (y, z) OR x = (z, y); +ASSERT x = (0,0) OR x = (1,1); + +CHECKSAT; diff --git a/test/regress/regress0/rels/atom_univ2.cvc b/test/regress/regress0/rels/atom_univ2.cvc index 9901ce630..e01d99dee 100644 --- a/test/regress/regress0/rels/atom_univ2.cvc +++ b/test/regress/regress0/rels/atom_univ2.cvc @@ -1,4 +1,5 @@ % EXPECT: unsat
+OPTION "sets-ext";
OPTION "logic" "ALL_SUPPORTED";
Atom: TYPE;
diff --git a/test/regress/regress0/sets/Makefile.am b/test/regress/regress0/sets/Makefile.am index 9413dfba3..5ff24f1ff 100644 --- a/test/regress/regress0/sets/Makefile.am +++ b/test/regress/regress0/sets/Makefile.am @@ -81,7 +81,12 @@ TESTS = \ complement3.cvc \ sharing-simp.smt2 \ pre-proc-univ.smt2 \ - nonvar-univ.smt2 + nonvar-univ.smt2 \ + sets-poly-int-real.smt2 \ + sets-poly-nonint.smt2 \ + int-real-univ.smt2 \ + int-real-univ-unsat.smt2 \ + sets-tuple-poly.cvc EXTRA_DIST = $(TESTS) diff --git a/test/regress/regress0/sets/complement.cvc b/test/regress/regress0/sets/complement.cvc index 73eeb2cbd..91388a56c 100644 --- a/test/regress/regress0/sets/complement.cvc +++ b/test/regress/regress0/sets/complement.cvc @@ -1,4 +1,5 @@ % EXPECT: sat +OPTION "sets-ext"; OPTION "logic" "ALL_SUPPORTED"; Atom: TYPE; a : SET OF [Atom]; diff --git a/test/regress/regress0/sets/complement2.cvc b/test/regress/regress0/sets/complement2.cvc index 22dde0338..b8100bf5f 100644 --- a/test/regress/regress0/sets/complement2.cvc +++ b/test/regress/regress0/sets/complement2.cvc @@ -1,4 +1,5 @@ % EXPECT: unsat
+OPTION "sets-ext";
OPTION "logic" "ALL_SUPPORTED";
Atom: TYPE;
a : SET OF Atom;
diff --git a/test/regress/regress0/sets/complement3.cvc b/test/regress/regress0/sets/complement3.cvc index ff527a9b3..fa0a31e40 100644 --- a/test/regress/regress0/sets/complement3.cvc +++ b/test/regress/regress0/sets/complement3.cvc @@ -1,4 +1,5 @@ % EXPECT: sat +OPTION "sets-ext"; OPTION "logic" "ALL_SUPPORTED"; Atom : TYPE; C32 : SET OF [Atom]; @@ -11,4 +12,4 @@ ASSERT TUPLE(V1) IS_IN ~(C32); ASSERT ATOM_UNIV = UNIVERSE :: SET OF [Atom]; ASSERT TUPLE(V1) IS_IN ATOM_UNIV; ASSERT TUPLE(V1) IS_IN ~(C2); -CHECKSAT;
\ No newline at end of file +CHECKSAT; diff --git a/test/regress/regress0/sets/int-real-univ-unsat.smt2 b/test/regress/regress0/sets/int-real-univ-unsat.smt2 new file mode 100644 index 000000000..56f7e8c5e --- /dev/null +++ b/test/regress/regress0/sets/int-real-univ-unsat.smt2 @@ -0,0 +1,16 @@ +; COMMAND-LINE: --sets-ext +; EXPECT: unsat +(set-logic ALL) +(set-info :status unsat) + +(declare-fun a () (Set Real)) + +(declare-fun x () Real) + +(assert (= (as univset (Set Real)) (as univset (Set Int)))) + +(assert (member x a)) + +(assert (and (<= 5.5 x) (< x 5.8))) + +(check-sat) diff --git a/test/regress/regress0/sets/int-real-univ.smt2 b/test/regress/regress0/sets/int-real-univ.smt2 new file mode 100644 index 000000000..afe20b92f --- /dev/null +++ b/test/regress/regress0/sets/int-real-univ.smt2 @@ -0,0 +1,16 @@ +; COMMAND-LINE: --sets-ext +; EXPECT: sat +(set-logic ALL) +(set-info :status sat) + +(declare-fun a () (Set Real)) + +(declare-fun x () Real) + +(assert (= (as univset (Set Real)) (as univset (Set Int)))) + +(assert (member x a)) + +(assert (and (<= 5.5 x) (< x 6.1))) + +(check-sat) diff --git a/test/regress/regress0/sets/nonvar-univ.smt2 b/test/regress/regress0/sets/nonvar-univ.smt2 index c71c984a2..5c3bc567c 100644 --- a/test/regress/regress0/sets/nonvar-univ.smt2 +++ b/test/regress/regress0/sets/nonvar-univ.smt2 @@ -1,3 +1,5 @@ +; COMMAND-LINE: --sets-ext +; EXPECT: sat (set-logic ALL) (set-info :status sat) (declare-fun x () (Set Int)) diff --git a/test/regress/regress0/sets/pre-proc-univ.smt2 b/test/regress/regress0/sets/pre-proc-univ.smt2 index 1b4bf8b41..f184ebf92 100644 --- a/test/regress/regress0/sets/pre-proc-univ.smt2 +++ b/test/regress/regress0/sets/pre-proc-univ.smt2 @@ -1,3 +1,5 @@ +; COMMAND-LINE: --sets-ext +; EXPECT: unsat (set-logic ALL) (set-info :status unsat) (declare-fun x () (Set Int)) diff --git a/test/regress/regress0/sets/sets-poly-int-real.smt2 b/test/regress/regress0/sets/sets-poly-int-real.smt2 new file mode 100644 index 000000000..407e95d3c --- /dev/null +++ b/test/regress/regress0/sets/sets-poly-int-real.smt2 @@ -0,0 +1,17 @@ +(set-logic QF_UFLIRAFS) +(set-info :status sat) +(declare-fun s () (Set Real)) +(declare-fun t1 () (Set Real)) +(declare-fun t2 () (Set Real)) +(declare-fun t3 () (Set Real)) +(declare-fun r1 () (Set Int)) +(declare-fun r2 () (Set Int)) +(declare-fun r3 () (Set Int)) +(assert (and (member 1.5 s) (member 0 s))) +(assert (= t1 (union s (singleton 2.5)))) +(assert (= t2 (union s (singleton 2)))) +(assert (= t3 (union r3 (singleton 2.5)))) +(assert (= (intersection r1 r2) (intersection s (singleton 0)))) +(assert (not (= r1 (as emptyset (Set Real))))) + +(check-sat) diff --git a/test/regress/regress0/sets/sets-poly-nonint.smt2 b/test/regress/regress0/sets/sets-poly-nonint.smt2 new file mode 100644 index 000000000..441716dcf --- /dev/null +++ b/test/regress/regress0/sets/sets-poly-nonint.smt2 @@ -0,0 +1,11 @@ +(set-logic QF_UFLIRAFS) +(set-info :status unsat) +(declare-fun s () (Set Int)) +(declare-fun t () (Set Real)) +(declare-fun r () (Set Real)) +(declare-fun u () (Set Real)) +(assert (member 1.5 t)) +(assert (member 2.5 r)) +(assert (member 3.5 u)) +(assert (or (member 4.5 s) (= s t) (= s r) (= s u) (= s (singleton 6.5)))) +(check-sat) diff --git a/test/regress/regress0/sets/sets-tuple-poly.cvc b/test/regress/regress0/sets/sets-tuple-poly.cvc new file mode 100644 index 000000000..8d87345f6 --- /dev/null +++ b/test/regress/regress0/sets/sets-tuple-poly.cvc @@ -0,0 +1,18 @@ +% EXPECT: sat +OPTION "sets-ext"; +OPTION "logic" "ALL_SUPPORTED"; + +a : SET OF [REAL, INT]; +b : SET OF [INT, REAL]; + +x : [ REAL, REAL ]; + + +ASSERT NOT x = (0,0); + +ASSERT x IS_IN a; +ASSERT x IS_IN b; + +ASSERT NOT x.0 = x.1; + +CHECKSAT; diff --git a/test/regress/regress0/sets/univset-simp.smt2 b/test/regress/regress0/sets/univset-simp.smt2 index ec9750776..a8875cc41 100644 --- a/test/regress/regress0/sets/univset-simp.smt2 +++ b/test/regress/regress0/sets/univset-simp.smt2 @@ -1,3 +1,5 @@ +; COMMAND-LINE: --sets-ext +; EXPECT: sat (set-logic ALL) (set-info :status sat) |