sets cvc parser

diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g
index 18f9dd8717015508289e751e256b58d305b23efd..12a3fa6f2ec03aaee3acd1b1f9dca5a3fd9c218c 100644 (file)
--- a/src/parser/cvc/Cvc.g
+++ b/src/parser/cvc/Cvc.g
@@ -104,6 +104,7 @@ tokens {
   WITH_TOK = 'WITH';
 
   SUBTYPE_TOK = 'SUBTYPE';
+  SET_TOK = 'SET';
 
   FORALL_TOK = 'FORALL';
   EXISTS_TOK = 'EXISTS';
@@ -326,6 +327,7 @@ Kind getOperatorKind(int type, bool& negate) {
   case GEQ_TOK: return kind::GEQ;
   case LT_TOK: return kind::LT;
   case LEQ_TOK: return kind::LEQ;
+  case IN_TOK: return kind::MEMBER;
 
     // arithmeticBinop
   case PLUS_TOK: return kind::PLUS;
@@ -388,12 +390,23 @@ Expr createPrecedenceTree(Parser* parser, ExprManager* em,
   Kind k = getOperatorKind(operators[pivot], negate);
   Expr lhs = createPrecedenceTree(parser, em, expressions, operators, startIndex, pivot);
   Expr rhs = createPrecedenceTree(parser, em, expressions, operators, pivot + 1, stopIndex);
-  if(k == kind::EQUAL && lhs.getType().isBoolean()) {
-    if(parser->strictModeEnabled()) {
-      WarningOnce() << "Warning: in strict parsing mode, will not convert BOOL = BOOL to BOOL <=> BOOL" << std::endl;
-    } else {
-      k = kind::IFF;
+
+  switch(k) {
+  case kind::EQUAL: {
+    if(lhs.getType().isBoolean()) {
+      if(parser->strictModeEnabled()) {
+        WarningOnce() << "Warning: in strict parsing mode, will not convert BOOL = BOOL to BOOL <=> BOOL" << std::endl;
+      } else {
+        k = kind::IFF;
+      }
     }
+    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;
+  case kind::BITVECTOR_OR : if(lhs.getType().isSet()) { k = kind::UNION; } break;
+  default: break;
   }
   Expr e = em->mkExpr(k, lhs, rhs);
   return negate ? em->mkExpr(kind::NOT, e) : e;
@@ -1146,6 +1159,8 @@ restrictedTypePossiblyFunctionLHS[CVC4::Type& t,
     /* array types */
   | ARRAY_TOK restrictedType[t,check] OF_TOK restrictedType[t2,check]
     { t = EXPR_MANAGER->mkArrayType(t, t2); }
+  | SET_TOK OF_TOK restrictedType[t,check]
+    { t = EXPR_MANAGER->mkSetType(t); }
 
     /* subtypes */
   | SUBTYPE_TOK LPAREN
@@ -1427,6 +1442,7 @@ comparisonBinop[unsigned& op]
   | GEQ_TOK
   | LT_TOK
   | LEQ_TOK
+  | IN_TOK
   ;
 
 term[CVC4::Expr& f]
@@ -1701,6 +1717,8 @@ postfixTerm[CVC4::Expr& f]
                                MK_CONST(AscriptionType(dtc.getSpecializedConstructorType(t))), f.getOperator() ));
           v.insert(v.end(), f.begin(), f.end());
           f = MK_EXPR(CVC4::kind::APPLY_CONSTRUCTOR, v);
+        } else if(f.getKind() == CVC4::kind::EMPTYSET && t.isSet()) {
+          f = MK_CONST(CVC4::EmptySet(t));
         } else {
           if(f.getType() != t) {
             PARSER_STATE->parseError("Type ascription not satisfied.");
@@ -1908,6 +1926,20 @@ simpleTerm[CVC4::Expr& f]
       f = MK_EXPR(kind::RECORD, MK_CONST(t.getRecord()), std::vector<Expr>());
     }
 
+
+    /* empty set literal */
+  | LBRACE RBRACE
+    { f = MK_CONST(EmptySet(Type())); }
+
+    /* finite set literal */
+  | LBRACE formula[f] { args.push_back(f); }
+    ( COMMA formula[f] { args.push_back(f); } )* RBRACE
+    { f = MK_EXPR(kind::SINGLETON, args[0]);
+      for(size_t i = 1; i < args.size(); ++i) {
+        f = MK_EXPR(kind::UNION, f, MK_EXPR(kind::SINGLETON, args[i]));
+      }
+    }
+
     /* boolean literals */
   | TRUE_TOK  { f = MK_CONST(bool(true)); }
   | FALSE_TOK { f = MK_CONST(bool(false)); }

diff --git a/test/regress/regress0/sets/Makefile.am b/test/regress/regress0/sets/Makefile.am
index 9536dfac1d5a748321a7ad896d68d17690cd00a7..19f6313fbb614a127329b1486f70b4a4d2c9b3b9 100644 (file)
--- a/test/regress/regress0/sets/Makefile.am
+++ b/test/regress/regress0/sets/Makefile.am
@@ -40,6 +40,7 @@ TESTS =       \
        mar2014/UniqueZipper.hs.1030minimized2.cvc4.smt2 \
        mar2014/UniqueZipper.hs.1030minimized.cvc4.smt2 \
        copy_check_heap_access_33_4.smt2 \
+       cvc-sample.cvc \
        emptyset.smt2 \
        error1.smt2 \
        error2.smt2 \

diff --git a/test/regress/regress0/sets/cvc-sample.cvc b/test/regress/regress0/sets/cvc-sample.cvc
new file mode 100644 (file)
index 0000000..c6fb95a
--- /dev/null
+++ b/test/regress/regress0/sets/cvc-sample.cvc
@@ -0,0 +1,57 @@
+% EXPECT: unsat
+% EXPECT: unsat
+% EXPECT: unsat
+% EXPECT: unsat
+% EXPECT: unsat
+% EXPECT: valid
+OPTION "incremental" true;
+OPTION "logic" "ALL_SUPPORTED";
+SetInt : TYPE = SET OF INT;
+x : SET OF INT;
+y : SET OF INT;
+z : SET OF INT;
+e1 : INT;
+e2 : INT;
+PUSH;
+a : SET OF INT;
+b : SET OF INT;
+c : SET OF INT;
+e : INT;
+ASSERT a = {5};
+ASSERT c = (a | b);
+ASSERT NOT(c = (a & b));
+ASSERT c = (a - b);
+ASSERT a <= b;
+ASSERT e IN c;
+ASSERT e IN a;
+ASSERT e IN (a & b);
+CHECKSAT TRUE;
+POP;
+PUSH;
+ASSERT x = y;
+ASSERT NOT((x | z) = (y | z));
+CHECKSAT TRUE;
+POP;
+PUSH;
+ASSERT x = y;
+ASSERT e1 = e2;
+ASSERT e1 IN x;
+ASSERT NOT(e2 IN y);
+CHECKSAT TRUE;
+POP;
+PUSH;
+ASSERT x = y;
+ASSERT e1 = e2;
+ASSERT e1 IN (x | z);
+ASSERT NOT(e2 IN (y | z));
+CHECKSAT TRUE;
+POP;
+PUSH;
+ASSERT 5 IN ({1, 2, 3, 4} | {5});
+ASSERT 5 IN ({1, 2, 3, 4} | {} :: SET OF INT);
+CHECKSAT TRUE;
+POP;
+PUSH;
+QUERY LET v_0 = e1 IN z
+IN NOT (v_0 AND NOT v_0);
+POP;

diff --git a/test/regress/regress0/sets/cvc-sample.smt2 b/test/regress/regress0/sets/cvc-sample.smt2
deleted file mode 100644 (file)
index 6f8b9f4..0000000
--- a/test/regress/regress0/sets/cvc-sample.smt2
+++ /dev/null
@@ -1,53 +0,0 @@
-OPTION "logic" "ALL_SUPPORTED";
-SetInt : TYPE = SET OF INT;
-PUSH;
-a : SET OF INT;
-b : SET OF INT;
-c : SET OF INT;
-e : INT;
-ASSERT a = {5};
-ASSERT c = (a | b);
-ASSERT NOT(c = (a & b));
-ASSERT c = (a - b);
-ASSERT a <= b;
-ASSERT e IN c;
-ASSERT e IN a;
-ASSERT e IN (a & b);
-CHECKSAT TRUE;
-POP;
-PUSH;
-x : SET OF INT;
-y : SET OF INT;
-z : SET OF INT;
-ASSERT x = y;
-ASSERT NOT((x | z) = (y | z));
-CHECKSAT TRUE;
-POP;
-PUSH;
-x : SET OF INT;
-y : SET OF INT;
-e1 : INT;
-e2 : INT;
-ASSERT x = y;
-ASSERT e1 = e2;
-ASSERT e1 IN x;
-ASSERT NOT(e2 IN y);
-CHECKSAT TRUE;
-POP;
-PUSH;
-x : SET OF INT;
-y : SET OF INT;
-z : SET OF INT;
-e1 : INT;
-e2 : INT;
-ASSERT x = y;
-ASSERT e1 = e2;
-ASSERT e1 IN (x | z);
-ASSERT NOT(e2 IN (y | z));
-CHECKSAT TRUE;
-POP;
-PUSH;
-ASSERT 5 IN ({1, 2, 3, 4} | {5});
-ASSERT 5 IN ({1, 2, 3, 4} | {} :: SET OF INT);
-CHECKSAT TRUE;
-