fixed cvc4 parser for set complement

diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g
index d72e1526e9b2e15393de4d7b09ea0c3631b41277..a5d5febe93c9c71962d7919724ad01b851cdc211 100644 (file)
--- 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 981e88a5cc78ff90872bb36d7c57f5ca975574d2..c9a80d24796d9f8ebbb0ad231131fc95bd23a271 100644 (file)
--- 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 06bd6cbf11205bb6d040eedfd51e337befb9b1a8..4c65f3a6ac98de6da6ba2069c645e489dcc9b3d2 100644 (file)
--- 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 6181cbee72762c0c6705cb2f84b83414406e7578..73eeb2cbd1775b6316035e324b0a4fb6a456943f 100644 (file)
--- 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 6802065f1c949ff08197b2482c34e69f724cd83c..22dde0338eb0fb727d13dbaf9f2caa55f75ad814 100644 (file)
--- 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;\r
 c : Atom;\r
 \r
-ASSERT a = NOT(a);\r
+ASSERT a = ~(a);\r
 ASSERT c IS_IN a;\r
 \r
 CHECKSAT;\r

diff --git a/test/regress/regress0/sets/complement3.cvc b/test/regress/regress0/sets/complement3.cvc
new file mode 100644 (file)
index 0000000..ff527a9
--- /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