diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2016-10-26 16:23:58 -0500 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2016-10-26 16:23:58 -0500 |
commit | 031722bee8682005bd4c8700ef78b5f893fc48fe (patch) | |
tree | 46a936a1bd20ea2cc588df0d3205cf7eb0fd4177 /src/parser | |
parent | e79e64329ce7d6df0003cab28dadb9b8bcc6f9ca (diff) |
New implementation of sets+cardinality. Merge Paul Meng's relation solver as extension of sets solver, add regressions.
Diffstat (limited to 'src/parser')
-rw-r--r-- | src/parser/cvc/Cvc.g | 47 |
1 files changed, 40 insertions, 7 deletions
diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g index 4c0516eb6..e6d7f9d86 100644 --- a/src/parser/cvc/Cvc.g +++ b/src/parser/cvc/Cvc.g @@ -109,6 +109,8 @@ tokens { SUBTYPE_TOK = 'SUBTYPE'; SET_TOK = 'SET'; + + TUPLE_TOK = 'TUPLE'; FORALL_TOK = 'FORALL'; EXISTS_TOK = 'EXISTS'; @@ -201,6 +203,12 @@ tokens { BVSGT_TOK = 'BVSGT'; BVSLE_TOK = 'BVSLE'; BVSGE_TOK = 'BVSGE'; + + // Relations + JOIN_TOK = 'JOIN'; + TRANSPOSE_TOK = 'TRANSPOSE'; + PRODUCT_TOK = 'PRODUCT'; + TRANSCLOSURE_TOK = 'TCLOSURE'; // Strings @@ -307,9 +315,14 @@ int getOperatorPrecedence(int type) { case STAR_TOK: case INTDIV_TOK: case DIV_TOK: + case TUPLE_TOK: case MOD_TOK: return 23; case PLUS_TOK: - case MINUS_TOK: return 24; + case MINUS_TOK: + case JOIN_TOK: + case TRANSPOSE_TOK: + case PRODUCT_TOK: + case TRANSCLOSURE_TOK: return 24; case LEQ_TOK: case LT_TOK: case GEQ_TOK: @@ -346,6 +359,9 @@ Kind getOperatorKind(int type, bool& negate) { case OR_TOK: return kind::OR; case XOR_TOK: return kind::XOR; case AND_TOK: return kind::AND; + + case PRODUCT_TOK: return kind::PRODUCT; + case JOIN_TOK: return kind::JOIN; // comparisonBinop case EQUAL_TOK: return kind::EQUAL; @@ -1222,8 +1238,8 @@ restrictedTypePossiblyFunctionLHS[CVC4::Type& t, | 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); } - + { t = EXPR_MANAGER->mkSetType(t); } + /* subtypes */ | SUBTYPE_TOK LPAREN /* A bit tricky: this LAMBDA expression cannot refer to constants @@ -1472,6 +1488,8 @@ booleanBinop[unsigned& op] | OR_TOK | XOR_TOK | AND_TOK + | JOIN_TOK + | PRODUCT_TOK ; comparison[CVC4::Expr& f] @@ -1651,6 +1669,20 @@ bvNegTerm[CVC4::Expr& f] /* BV neg */ : BVNEG_TOK bvNegTerm[f] { f = MK_EXPR(CVC4::kind::BITVECTOR_NOT, f); } + | TRANSPOSE_TOK bvNegTerm[f] + { f = MK_EXPR(CVC4::kind::TRANSPOSE, f); } + | TRANSCLOSURE_TOK bvNegTerm[f] + { f = MK_EXPR(CVC4::kind::TCLOSURE, f); } + | TUPLE_TOK LPAREN bvNegTerm[f] RPAREN + { std::vector<Type> types; + std::vector<Expr> args; + args.push_back(f); + types.push_back(f.getType()); + DatatypeType t = EXPR_MANAGER->mkTupleType(types); + const Datatype& dt = t.getDatatype(); + args.insert( args.begin(), dt[0].getConstructor() ); + f = MK_EXPR(kind::APPLY_CONSTRUCTOR, args); + } | postfixTerm[f] ; @@ -1969,8 +2001,8 @@ simpleTerm[CVC4::Expr& f] Type t, t2; } /* if-then-else */ - : iteTerm[f] - + : iteTerm[f] + /* parenthesized sub-formula / tuple literals */ | LPAREN formula[f] { args.push_back(f); } ( COMMA formula[f] { args.push_back(f); } )* RPAREN @@ -1987,14 +2019,15 @@ simpleTerm[CVC4::Expr& f] args.insert( args.begin(), dt[0].getConstructor() ); f = MK_EXPR(kind::APPLY_CONSTRUCTOR, args); } - } + } /* empty tuple literal */ | LPAREN RPAREN { std::vector<Type> types; DatatypeType t = EXPR_MANAGER->mkTupleType(types); const Datatype& dt = t.getDatatype(); - f = MK_EXPR(kind::APPLY_CONSTRUCTOR, dt[0].getConstructor()); } + f = MK_EXPR(kind::APPLY_CONSTRUCTOR, dt[0].getConstructor()); } + /* empty record literal */ | PARENHASH HASHPAREN { DatatypeType t = EXPR_MANAGER->mkRecordType(std::vector< std::pair<std::string, Type> >()); |