sets cvc printer

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)