diff options
author | Kshitij Bansal <kshitij@cs.nyu.edu> | 2014-07-09 14:33:31 -0400 |
---|---|---|
committer | Kshitij Bansal <kshitij@cs.nyu.edu> | 2014-07-09 14:33:31 -0400 |
commit | b3c76399db741d8d616a75242345710dc1c1b81c (patch) | |
tree | 5f2ac2af2b52229a28d3e72f93dd2f0b89d548ed /test/regress | |
parent | e926fd162c6cee95d31044305e3b4df90b59f9fc (diff) |
sets cvc printer
Diffstat (limited to 'test/regress')
-rw-r--r-- | test/regress/regress0/sets/cvc-sample.smt2 | 53 | ||||
-rw-r--r-- | test/regress/regress0/sets/sets-sample.smt2 | 8 |
2 files changed, 60 insertions, 1 deletions
diff --git a/test/regress/regress0/sets/cvc-sample.smt2 b/test/regress/regress0/sets/cvc-sample.smt2 new file mode 100644 index 000000000..6f8b9f48b --- /dev/null +++ b/test/regress/regress0/sets/cvc-sample.smt2 @@ -0,0 +1,53 @@ +OPTION "logic" "ALL_SUPPORTED"; +SetInt : TYPE = SET OF INT; +PUSH; +a : SET OF INT; +b : SET OF INT; +c : SET OF INT; +e : INT; +ASSERT a = {5}; +ASSERT c = (a | b); +ASSERT NOT(c = (a & b)); +ASSERT c = (a - b); +ASSERT a <= b; +ASSERT e IN c; +ASSERT e IN a; +ASSERT e IN (a & b); +CHECKSAT TRUE; +POP; +PUSH; +x : SET OF INT; +y : SET OF INT; +z : SET OF INT; +ASSERT x = y; +ASSERT NOT((x | z) = (y | z)); +CHECKSAT TRUE; +POP; +PUSH; +x : SET OF INT; +y : SET OF INT; +e1 : INT; +e2 : INT; +ASSERT x = y; +ASSERT e1 = e2; +ASSERT e1 IN x; +ASSERT NOT(e2 IN y); +CHECKSAT TRUE; +POP; +PUSH; +x : SET OF INT; +y : SET OF INT; +z : SET OF INT; +e1 : INT; +e2 : INT; +ASSERT x = y; +ASSERT e1 = e2; +ASSERT e1 IN (x | z); +ASSERT NOT(e2 IN (y | z)); +CHECKSAT TRUE; +POP; +PUSH; +ASSERT 5 IN ({1, 2, 3, 4} | {5}); +ASSERT 5 IN ({1, 2, 3, 4} | {} :: SET OF INT); +CHECKSAT TRUE; + diff --git a/test/regress/regress0/sets/sets-sample.smt2 b/test/regress/regress0/sets/sets-sample.smt2 index a040b0bec..3bc2da065 100644 --- a/test/regress/regress0/sets/sets-sample.smt2 +++ b/test/regress/regress0/sets/sets-sample.smt2 @@ -3,6 +3,7 @@ ; EXPECT: unsat ; EXPECT: unsat ; EXPECT: unsat +; EXPECT: unsat (set-logic ALL_SUPPORTED) (define-sort SetInt () (Set Int)) @@ -59,6 +60,11 @@ (assert (not (member e2 (union y z)))) (check-sat) (pop 1) + +; test all the other kinds for completeness +(push 1) +(assert (member 5 (insert 1 2 3 4 (singleton 5)))) +(assert (member 5 (insert 1 2 3 4 (as emptyset (Set Int))))) +(check-sat) (exit) -(exit) |