From 00c03533135d14d0aaaf607fde8874f346af7dbc Mon Sep 17 00:00:00 2001
From: Paul Meng <baolmeng@gmail.com>
Date: Mon, 20 Mar 2017 13:49:31 -0500
Subject: [PATCH] fixed cvc4 parser for set complement

---
 src/parser/cvc/Cvc.g                       | 11 ++++-------
 src/printer/cvc/cvc_printer.cpp            |  2 +-
 test/regress/regress0/sets/Makefile.am     |  3 ++-
 test/regress/regress0/sets/complement.cvc  |  2 +-
 test/regress/regress0/sets/complement2.cvc |  2 +-
 test/regress/regress0/sets/complement3.cvc | 14 ++++++++++++++
 6 files changed, 23 insertions(+), 11 deletions(-)
 create mode 100644 test/regress/regress0/sets/complement3.cvc

diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g
index d72e1526e..a5d5febe9 100644
--- a/src/parser/cvc/Cvc.g
+++ b/src/parser/cvc/Cvc.g
@@ -448,7 +448,7 @@ Expr createPrecedenceTree(Parser* parser, ExprManager* em,
   default: break;
   }
   Expr e = em->mkExpr(k, lhs, rhs);
-  return negate ? em->mkExpr(e.getType().isSet() ? kind::COMPLEMENT : kind::NOT, e) : e;
+  return negate ? em->mkExpr(kind::NOT, e) : e;
 }/* createPrecedenceTree() recursive variant */
 
 Expr createPrecedenceTree(Parser* parser, ExprManager* em,
@@ -474,9 +474,8 @@ Expr createPrecedenceTree(Parser* parser, ExprManager* em,
 
 /** Add n NOTs to the front of e and return the result. */
 Expr addNots(ExprManager* em, size_t n, Expr e) {
-  Kind k = e.getType().isSet() ? kind::COMPLEMENT : kind::NOT;
   while(n-- > 0) {
-    e = em->mkExpr(k, e);
+    e = em->mkExpr(kind::NOT, e);
   }
   return e;
 }/* addNots() */
@@ -1688,15 +1687,13 @@ bvBinop[unsigned& op]
 bvNegTerm[CVC4::Expr& f]
     /* BV neg */
   : BVNEG_TOK bvNegTerm[f]
-    { f = MK_EXPR(CVC4::kind::BITVECTOR_NOT, f); }
+    { f = f.getType().isSet() ? MK_EXPR(CVC4::kind::COMPLEMENT, f) : MK_EXPR(CVC4::kind::BITVECTOR_NOT, f); }
   | relationTerm[f]
   ;
 
 relationTerm[CVC4::Expr& f]
     /* relation terms */
-  : NOT_TOK relationTerm[f]
-    { f = MK_EXPR(CVC4::kind::COMPLEMENT, f); } 
-  | TRANSPOSE_TOK relationTerm[f]
+  : TRANSPOSE_TOK relationTerm[f]
     { f = MK_EXPR(CVC4::kind::TRANSPOSE, f); } 
   | TRANSCLOSURE_TOK relationTerm[f]
     { f = MK_EXPR(CVC4::kind::TCLOSURE, f); }
diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp
index 981e88a5c..c9a80d247 100644
--- a/src/printer/cvc/cvc_printer.cpp
+++ b/src/printer/cvc/cvc_printer.cpp
@@ -783,7 +783,7 @@ void CvcPrinter::toStream(std::ostream& out, TNode n, int depth, bool types, boo
       opType = INFIX;
       break;
     case kind::COMPLEMENT:
-      op << "NOT";
+      op << "~";
       opType = PREFIX;
       break;
     case kind::PRODUCT:
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
-- 
2.30.2