Fix cvc parser for set compliment.

diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g
index 0655359a9ab16b0c73668ee8c98aa681241e899f..267fe303ec47fb6ef3533865bb06686a5b8de5c2 100644 (file)
--- a/src/parser/cvc/Cvc.g
+++ b/src/parser/cvc/Cvc.g
@@ -441,7 +441,6 @@ Expr createPrecedenceTree(Parser* parser, ExprManager* em,
   Expr rhs = createPrecedenceTree(parser, em, expressions, operators, pivot + 1, stopIndex);
 
   switch(k) {
-  case kind::NOT          : if(lhs.getType().isSet()) { k = kind::COMPLIMENT; } break;
   case kind::LEQ          : if(lhs.getType().isSet()) { k = kind::SUBSET; } break;
   case kind::MINUS        : if(lhs.getType().isSet()) { k = kind::SETMINUS; } break;
   case kind::BITVECTOR_AND: if(lhs.getType().isSet()) { k = kind::INTERSECTION; } break;
@@ -449,7 +448,7 @@ Expr createPrecedenceTree(Parser* parser, ExprManager* em,
   default: break;
   }
   Expr e = em->mkExpr(k, lhs, rhs);
-  return negate ? em->mkExpr(kind::NOT, e) : e;
+  return negate ? em->mkExpr(e.getType().isSet() ? kind::COMPLIMENT : kind::NOT, e) : e;
 }/* createPrecedenceTree() recursive variant */
 
 Expr createPrecedenceTree(Parser* parser, ExprManager* em,
@@ -475,8 +474,9 @@ 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::COMPLIMENT : kind::NOT;
   while(n-- > 0) {
-    e = em->mkExpr(kind::NOT, e);
+    e = em->mkExpr(k, e);
   }
   return e;
 }/* addNots() */

diff --git a/test/regress/regress0/sets/Makefile.am b/test/regress/regress0/sets/Makefile.am
index a92c534a121cd758b95aafe442dc977196cb603d..629e8a8a07ab23414f937bbd2b2349bd8de2046b 100644 (file)
--- a/test/regress/regress0/sets/Makefile.am
+++ b/test/regress/regress0/sets/Makefile.am
@@ -75,7 +75,8 @@ TESTS =       \
        abt-min.smt2 \
        abt-te-exh.smt2 \
        abt-te-exh2.smt2 \
-       univset-simp.smt2
+       univset-simp.smt2 \
+       compliment.cvc
 
 EXTRA_DIST = $(TESTS)
 

diff --git a/test/regress/regress0/sets/compliment.cvc b/test/regress/regress0/sets/compliment.cvc
new file mode 100644 (file)
index 0000000..6181cbe
--- /dev/null
+++ b/test/regress/regress0/sets/compliment.cvc
@@ -0,0 +1,9 @@
+% EXPECT: sat
+OPTION "logic" "ALL_SUPPORTED";
+Atom: TYPE;
+a : SET OF [Atom];
+b : SET OF [Atom];
+
+ASSERT a = (NOT b);
+
+CHECKSAT;