fixed cvc4 parser for set complement

4 files changed, 18 insertions, 3 deletions

diff --git a/test/regress/regress0/sets/Makefile.am b/test/regress/regress0/sets/Makefile.am
index 06bd6cbf1..4c65f3a6a 100644
--- a/test/regress/regress0/sets/Makefile.am
+++ b/test/regress/regress0/sets/Makefile.am
@@ -77,7 +77,8 @@ TESTS =	\
 	abt-te-exh2.smt2 \
 	univset-simp.smt2 \
 	complement.cvc \
-	complement2.cvc
+	complement2.cvc \
+    complement3.cvc
 
 EXTRA_DIST = $(TESTS)
 
diff --git a/test/regress/regress0/sets/complement.cvc b/test/regress/regress0/sets/complement.cvc
index 6181cbee7..73eeb2cbd 100644
--- a/test/regress/regress0/sets/complement.cvc
+++ b/test/regress/regress0/sets/complement.cvc
@@ -4,6 +4,6 @@ Atom: TYPE;
 a : SET OF [Atom];
 b : SET OF [Atom];
 
-ASSERT a = (NOT b);
+ASSERT a = (~ b);
 
 CHECKSAT;
diff --git a/test/regress/regress0/sets/complement2.cvc b/test/regress/regress0/sets/complement2.cvc
index 6802065f1..22dde0338 100644
--- a/test/regress/regress0/sets/complement2.cvc
+++ b/test/regress/regress0/sets/complement2.cvc
@@ -5,7 +5,7 @@ a : SET OF Atom;
 b : SET OF Atom;

 c : Atom;

 

-ASSERT a = NOT(a);

+ASSERT a = ~(a);

 ASSERT c IS_IN a;

 

 CHECKSAT;

diff --git a/test/regress/regress0/sets/complement3.cvc b/test/regress/regress0/sets/complement3.cvc
new file mode 100644
index 000000000..ff527a9b3
--- /dev/null
+++ b/test/regress/regress0/sets/complement3.cvc
@@ -0,0 +1,14 @@
+% EXPECT: sat
+OPTION "logic" "ALL_SUPPORTED";
+Atom : TYPE;
+C32 : SET OF [Atom];
+C2 : SET OF [Atom];
+C4 : SET OF [Atom];
+ATOM_UNIV : SET OF [Atom];
+V1 : Atom;
+ASSERT C32 = (~C2) & (~C4);											
+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