From: ajreynol <andrew.j.reynolds@gmail.com>
Date: Tue, 7 Mar 2017 15:11:33 +0000 (-0600)
Subject: Fix cvc parser for set compliment.
X-Git-Tag: cvc5-1.0.0~5898
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=105cae4ed94f0ce13b0525a348b29d2fc7d5af72;p=cvc5.git

Fix cvc parser for set compliment.
---

diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g
index 0655359a9..267fe303e 100644
--- 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 a92c534a1..629e8a8a0 100644
--- 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
index 000000000..6181cbee7
--- /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;