diff options
Diffstat (limited to 'test/regress')
-rw-r--r-- | test/regress/regress0/fmf/quant_real_univ.cvc | 1 | ||||
-rw-r--r-- | test/regress/regress0/rels/joinImg_0.cvc | 1 | ||||
-rw-r--r-- | test/regress/regress0/rels/joinImg_0_1.cvc | 1 | ||||
-rw-r--r-- | test/regress/regress0/rels/joinImg_1.cvc | 1 | ||||
-rw-r--r-- | test/regress/regress0/rels/joinImg_1_1.cvc | 1 | ||||
-rw-r--r-- | test/regress/regress0/rels/joinImg_2.cvc | 1 | ||||
-rw-r--r-- | test/regress/regress0/rels/joinImg_2_1.cvc | 3 | ||||
-rw-r--r-- | test/regress/regress0/sets/Makefile.am | 4 | ||||
-rw-r--r-- | test/regress/regress0/sets/arjun-set-univ.cvc | 8 | ||||
-rw-r--r-- | test/regress/regress0/sets/univ-set-uf-elim.smt2 | 16 |
10 files changed, 35 insertions, 2 deletions
diff --git a/test/regress/regress0/fmf/quant_real_univ.cvc b/test/regress/regress0/fmf/quant_real_univ.cvc index c3cefd767..c3dbb2cd6 100644 --- a/test/regress/regress0/fmf/quant_real_univ.cvc +++ b/test/regress/regress0/fmf/quant_real_univ.cvc @@ -1,5 +1,6 @@ % EXPECT: sat
OPTION "fmf-bound";
+OPTION "sets-ext";
Atom : TYPE;
REAL_UNIVERSE : SET OF [REAL];
ATOM_UNIVERSE : SET OF [Atom];
diff --git a/test/regress/regress0/rels/joinImg_0.cvc b/test/regress/regress0/rels/joinImg_0.cvc index e36c6a647..297898a81 100644 --- a/test/regress/regress0/rels/joinImg_0.cvc +++ b/test/regress/regress0/rels/joinImg_0.cvc @@ -1,5 +1,6 @@ % EXPECT: unsat OPTION "logic" "ALL_SUPPORTED"; +OPTION "sets-ext"; IntPair: TYPE = [INT, INT]; x : SET OF IntPair; y : SET OF IntPair; diff --git a/test/regress/regress0/rels/joinImg_0_1.cvc b/test/regress/regress0/rels/joinImg_0_1.cvc index 602c4fe3f..4e69394bd 100644 --- a/test/regress/regress0/rels/joinImg_0_1.cvc +++ b/test/regress/regress0/rels/joinImg_0_1.cvc @@ -1,5 +1,6 @@ % EXPECT: sat OPTION "logic" "ALL_SUPPORTED"; +OPTION "sets-ext"; IntPair: TYPE = [INT, INT]; x : SET OF IntPair; y : SET OF IntPair; diff --git a/test/regress/regress0/rels/joinImg_1.cvc b/test/regress/regress0/rels/joinImg_1.cvc index 47e57c1fb..81f208fc4 100644 --- a/test/regress/regress0/rels/joinImg_1.cvc +++ b/test/regress/regress0/rels/joinImg_1.cvc @@ -1,5 +1,6 @@ % EXPECT: unsat OPTION "logic" "ALL_SUPPORTED"; +OPTION "sets-ext"; Atom: TYPE; x : SET OF [Atom, Atom]; y : SET OF [Atom, Atom]; diff --git a/test/regress/regress0/rels/joinImg_1_1.cvc b/test/regress/regress0/rels/joinImg_1_1.cvc index a7927f7e2..003770a1b 100644 --- a/test/regress/regress0/rels/joinImg_1_1.cvc +++ b/test/regress/regress0/rels/joinImg_1_1.cvc @@ -1,5 +1,6 @@ % EXPECT: sat OPTION "logic" "ALL_SUPPORTED"; +OPTION "sets-ext"; Atom: TYPE; x : SET OF [Atom, Atom]; y : SET OF [Atom, Atom]; diff --git a/test/regress/regress0/rels/joinImg_2.cvc b/test/regress/regress0/rels/joinImg_2.cvc index bbf57629b..a4acfe6c6 100644 --- a/test/regress/regress0/rels/joinImg_2.cvc +++ b/test/regress/regress0/rels/joinImg_2.cvc @@ -1,5 +1,6 @@ % EXPECT: unsat OPTION "logic" "ALL_SUPPORTED"; +OPTION "sets-ext"; Atom: TYPE; x : SET OF [Atom, Atom]; y : SET OF [Atom, Atom]; diff --git a/test/regress/regress0/rels/joinImg_2_1.cvc b/test/regress/regress0/rels/joinImg_2_1.cvc index b38bfab06..03f88be37 100644 --- a/test/regress/regress0/rels/joinImg_2_1.cvc +++ b/test/regress/regress0/rels/joinImg_2_1.cvc @@ -1,5 +1,6 @@ % EXPECT: sat OPTION "logic" "ALL_SUPPORTED"; +OPTION "sets-ext"; Atom: TYPE; x : SET OF [Atom, Atom]; y : SET OF [Atom, Atom]; @@ -21,4 +22,4 @@ ASSERT y = {(f, g), (b, c), (d, e), (c, e)}; ASSERT x = {(f, g), (b, c), (d, e), (c, e)}; ASSERT (NOT(a = b)) OR (NOT(a = f)); -CHECKSAT;
\ No newline at end of file +CHECKSAT; diff --git a/test/regress/regress0/sets/Makefile.am b/test/regress/regress0/sets/Makefile.am index c8e416a42..de2170768 100644 --- a/test/regress/regress0/sets/Makefile.am +++ b/test/regress/regress0/sets/Makefile.am @@ -86,7 +86,9 @@ TESTS = \ sets-poly-nonint.smt2 \ int-real-univ.smt2 \ int-real-univ-unsat.smt2 \ - sets-tuple-poly.cvc + sets-tuple-poly.cvc \ + arjun-set-univ.cvc \ + univ-set-uf-elim.smt2 EXTRA_DIST = $(TESTS) diff --git a/test/regress/regress0/sets/arjun-set-univ.cvc b/test/regress/regress0/sets/arjun-set-univ.cvc new file mode 100644 index 000000000..3c35a62a5 --- /dev/null +++ b/test/regress/regress0/sets/arjun-set-univ.cvc @@ -0,0 +1,8 @@ +% EXPECT: Extended set operators are not supported in default mode, try --sets-ext. +% EXIT: 1 +OPTION "produce-models" true; +x,y,z : SET OF BOOLEAN; +ASSERT x = {TRUE}; +ASSERT y = {FALSE}; +CHECKSAT z = ~ y; +COUNTERMODEL; diff --git a/test/regress/regress0/sets/univ-set-uf-elim.smt2 b/test/regress/regress0/sets/univ-set-uf-elim.smt2 new file mode 100644 index 000000000..a22f2a44f --- /dev/null +++ b/test/regress/regress0/sets/univ-set-uf-elim.smt2 @@ -0,0 +1,16 @@ +; EXPECT: (error "Extended set operators are not supported in default mode, try --sets-ext.") +; EXIT: 1 +(set-logic ALL) +(declare-fun a () Int) +(declare-fun f ((Set Bool)) Int) +(declare-fun s () (Set Bool)) + +(assert (member true s)) +(assert (member false s)) +(assert (= a (f (as univset (Set Bool))))) + +(assert (= (f (as emptyset (Set Bool))) 1)) +(assert (= (f (singleton true)) 2)) +(assert (= (f (singleton false)) 3)) +(assert (= (f (union (singleton true) (singleton false))) 4)) +(check-sat) |