From: Kshitij Bansal Date: Wed, 9 Jul 2014 19:58:40 +0000 (-0400) Subject: sets cvc parser X-Git-Tag: cvc5-1.0.0~6701^2~4 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=211304a663417c69552ea9efc43aaef855d7cd70;p=cvc5.git sets cvc parser --- diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g index 18f9dd871..12a3fa6f2 100644 --- 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()); } + + /* 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 9536dfac1..19f6313fb 100644 --- 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 index 000000000..c6fb95a77 --- /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 index 6f8b9f48b..000000000 --- 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; -