From 211304a663417c69552ea9efc43aaef855d7cd70 Mon Sep 17 00:00:00 2001
From: Kshitij Bansal <kshitij@cs.nyu.edu>
Date: Wed, 9 Jul 2014 15:58:40 -0400
Subject: sets cvc parser

---
 test/regress/regress0/sets/Makefile.am     |  1 +
 test/regress/regress0/sets/cvc-sample.cvc  | 57 ++++++++++++++++++++++++++++++
 test/regress/regress0/sets/cvc-sample.smt2 | 53 ---------------------------
 3 files changed, 58 insertions(+), 53 deletions(-)
 create mode 100644 test/regress/regress0/sets/cvc-sample.cvc
 delete mode 100644 test/regress/regress0/sets/cvc-sample.smt2

(limited to 'test')

diff --git a/test/regress/regress0/sets/Makefile.am b/test/regress/regress0/sets/Makefile.am
index 9536dfac1..19f6313fb 100644
--- a/test/regress/regress0/sets/Makefile.am
+++ b/test/regress/regress0/sets/Makefile.am
@@ -40,6 +40,7 @@ TESTS =	\
 	mar2014/UniqueZipper.hs.1030minimized2.cvc4.smt2 \
 	mar2014/UniqueZipper.hs.1030minimized.cvc4.smt2 \
 	copy_check_heap_access_33_4.smt2 \
+	cvc-sample.cvc \
 	emptyset.smt2 \
 	error1.smt2 \
 	error2.smt2 \
diff --git a/test/regress/regress0/sets/cvc-sample.cvc b/test/regress/regress0/sets/cvc-sample.cvc
new file mode 100644
index 000000000..c6fb95a77
--- /dev/null
+++ b/test/regress/regress0/sets/cvc-sample.cvc
@@ -0,0 +1,57 @@
+% EXPECT: unsat
+% EXPECT: unsat
+% EXPECT: unsat
+% EXPECT: unsat
+% EXPECT: unsat
+% EXPECT: valid
+OPTION "incremental" true;
+OPTION "logic" "ALL_SUPPORTED";
+SetInt : TYPE = SET OF INT;
+x : SET OF INT;
+y : SET OF INT;
+z : SET OF INT;
+e1 : INT;
+e2 : 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;
+ASSERT x = y;
+ASSERT NOT((x | z) = (y | z));
+CHECKSAT TRUE;
+POP;
+PUSH;
+ASSERT x = y;
+ASSERT e1 = e2;
+ASSERT e1 IN x;
+ASSERT NOT(e2 IN y);
+CHECKSAT TRUE;
+POP;
+PUSH;
+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;
+POP;
+PUSH;
+QUERY LET v_0 = e1 IN z
+IN NOT (v_0 AND NOT v_0);
+POP;
diff --git a/test/regress/regress0/sets/cvc-sample.smt2 b/test/regress/regress0/sets/cvc-sample.smt2
deleted file mode 100644
index 6f8b9f48b..000000000
--- a/test/regress/regress0/sets/cvc-sample.smt2
+++ /dev/null
@@ -1,53 +0,0 @@
-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;
-
-- 
cgit v1.2.3