diff options
Diffstat (limited to 'src/parser/cvc/Cvc.g')
| -rw-r--r-- | src/parser/cvc/Cvc.g | 103 |
1 files changed, 45 insertions, 58 deletions
diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g index c79da40a0..038c1f1d0 100644 --- a/src/parser/cvc/Cvc.g +++ b/src/parser/cvc/Cvc.g @@ -531,35 +531,6 @@ Expr addNots(ExprManager* em, size_t n, Expr e) { namespace CVC4 { class Expr; - - namespace parser { - namespace cvc { - /** - * This class is just here to get around an unfortunate bit of Antlr. - * We use strings below as return values from rules, which require - * them to be constructible by a void*. So we derive the string - * class to provide just such a conversion. - */ - class myString : public std::string { - public: - myString(const std::string& s) : std::string(s) {} - myString(void*) : std::string() {} - myString() : std::string() {} - };/* class myString */ - - /** - * Just exists to give us the void* construction that - * ANTLR requires. - */ - struct myExpr : public CVC4::Expr { - myExpr() : CVC4::Expr() {} - myExpr(void*) : CVC4::Expr() {} - myExpr(const Expr& e) : CVC4::Expr(e) {} - myExpr(const myExpr& e) : CVC4::Expr(e) {} - };/* struct myExpr */ - - }/* CVC4::parser::cvc namespace */ - }/* CVC4::parser namespace */ }/* CVC4 namespace */ }/* @parser::includes */ @@ -645,7 +616,7 @@ parseCommand returns [CVC4::Command* cmd_return = NULL] if(s == "benchmark") { PARSER_STATE->parseError( "In CVC4 presentation language mode, but SMT-LIBv1 format " - "detected. Use --lang smt1 for SMT-LIBv1 support."); + "detected, which is not supported anymore."); } else if(s == "set" || s == "get" || s == "declare" || s == "define" || s == "assert") { PARSER_STATE->parseError( @@ -1153,7 +1124,7 @@ declareVariables[std::unique_ptr<CVC4::Command>* cmd, CVC4::Type& t, Debug("parser") << "making " << *i << " : " << t << " = " << f << std::endl; PARSER_STATE->checkDeclaration(*i, CHECK_UNDECLARED, SYM_VARIABLE); Expr func = EXPR_MANAGER->mkVar(*i, t, ExprManager::VAR_FLAG_GLOBAL | ExprManager::VAR_FLAG_DEFINED); - PARSER_STATE->defineFunction(*i, f); + PARSER_STATE->defineVar(*i, f); Command* decl = new DefineFunctionCommand(*i, func, f); seq->addCommand(decl); } @@ -1552,9 +1523,6 @@ booleanBinop[unsigned& op] | OR_TOK | XOR_TOK | AND_TOK - | JOIN_TOK - | PRODUCT_TOK - | JOIN_IMAGE_TOK ; comparison[CVC4::Expr& f] @@ -1705,9 +1673,8 @@ uminusTerm[CVC4::Expr& f] unsigned minusCount = 0; } /* Unary minus */ - : (MINUS_TOK { ++minusCount; })+ bvBinaryOpTerm[f] + : (MINUS_TOK { ++minusCount; })* bvBinaryOpTerm[f] { while(minusCount > 0) { --minusCount; f = MK_EXPR(CVC4::kind::UMINUS, f); } } - | bvBinaryOpTerm[f] ; /** Parses bitvectors. Starts with binary operators @, &, and |. */ @@ -1734,28 +1701,27 @@ bvNegTerm[CVC4::Expr& f] /* BV neg */ : BVNEG_TOK bvNegTerm[f] { f = f.getType().isSet() ? MK_EXPR(CVC4::kind::COMPLEMENT, f) : MK_EXPR(CVC4::kind::BITVECTOR_NOT, f); } - | relationTerm[f] + | relationBinopTerm[f] ; -relationTerm[CVC4::Expr& f] - /* relation terms */ - : TRANSPOSE_TOK relationTerm[f] - { f = MK_EXPR(CVC4::kind::TRANSPOSE, f); } - | TRANSCLOSURE_TOK relationTerm[f] - { f = MK_EXPR(CVC4::kind::TCLOSURE, f); } - | TUPLE_TOK LPAREN relationTerm[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); - } - | IDEN_TOK relationTerm[f] - { f = MK_EXPR(CVC4::kind::IDEN, f); } - | postfixTerm[f] +relationBinop[unsigned& op] +@init { + op = LT(1)->getType(LT(1)); +} + : JOIN_TOK + | PRODUCT_TOK + | JOIN_IMAGE_TOK + ; + +relationBinopTerm[CVC4::Expr& f] +@init { + std::vector<CVC4::Expr> expressions; + std::vector<unsigned> operators; + unsigned op; +} + : postfixTerm[f] { expressions.push_back(f); } + ( relationBinop[op] postfixTerm[f] { operators.push_back(op); expressions.push_back(f); } )* + { f = createPrecedenceTree(PARSER_STATE, EXPR_MANAGER, expressions, operators); } ; /** @@ -1775,7 +1741,7 @@ postfixTerm[CVC4::Expr& f] std::string id; Type t; } - : ( bvTerm[f] + : ( relationTerm[f] ( /* array select / bitvector extract */ LBRACKET ( formula[f2] { extract = false; } @@ -1883,7 +1849,28 @@ postfixTerm[CVC4::Expr& f] } )? ; - + +relationTerm[CVC4::Expr& f] + /* relation terms */ + : TRANSPOSE_TOK LPAREN formula[f] RPAREN + { f = MK_EXPR(CVC4::kind::TRANSPOSE, f); } + | TRANSCLOSURE_TOK LPAREN formula[f] RPAREN + { f = MK_EXPR(CVC4::kind::TCLOSURE, f); } + | TUPLE_TOK LPAREN formula[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); + } + | IDEN_TOK LPAREN formula[f] RPAREN + { f = MK_EXPR(CVC4::kind::IDEN, f); } + | bvTerm[f] + ; + bvTerm[CVC4::Expr& f] @init { Expr f2; |