From 267858307741675cb78e829270e619f57cf21a27 Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Mon, 18 Apr 2011 18:05:39 +0000 Subject: mostly CVC presentation language parsing and printing --- src/parser/cvc/Cvc.g | 881 ++++++++++++++++++++++++++++++++++++------------- src/parser/smt2/Smt2.g | 1 + 2 files changed, 655 insertions(+), 227 deletions(-) (limited to 'src/parser') diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g index 33e576a32..96a8346b0 100644 --- a/src/parser/cvc/Cvc.g +++ b/src/parser/cvc/Cvc.g @@ -24,6 +24,323 @@ options { k = 2; } +tokens { + // Keywords + + AND_TOK = 'AND'; + ASSERT_TOK = 'ASSERT'; + BOOLEAN_TOK = 'BOOLEAN'; + CHECKSAT_TOK = 'CHECKSAT'; + ECHO_TOK = 'ECHO'; + ELSEIF_TOK = 'ELSIF'; + ELSE_TOK = 'ELSE'; + ENDIF_TOK = 'ENDIF'; + FALSE_TOK = 'FALSE'; + IF_TOK = 'IF'; + IN_TOK = 'IN'; + INT_TOK = 'INT'; + LET_TOK = 'LET'; + NOT_TOK = 'NOT'; + OPTION_TOK = 'OPTION'; + OR_TOK = 'OR'; + POPTO_TOK = 'POPTO'; + POP_TOK = 'POP'; + PRINT_TOK = 'PRINT'; + PUSH_TOK = 'PUSH'; + QUERY_TOK = 'QUERY'; + REAL_TOK = 'REAL'; + THEN_TOK = 'THEN'; + TRUE_TOK = 'TRUE'; + TYPE_TOK = 'TYPE'; + XOR_TOK = 'XOR'; + + DATATYPE_TOK = 'DATATYPE'; + END_TOK = 'END'; + + ARRAY_TOK = 'ARRAY'; + OF_TOK = 'OF'; + WITH_TOK = 'WITH'; + + FORALL_TOK = 'FORALL'; + EXISTS_TOK = 'EXISTS'; + + // Symbols + + COLON = ':'; + COMMA = ','; + LPAREN = '('; + RPAREN = ')'; + LBRACE = '{'; + RBRACE = '}'; + LBRACKET = '['; + RBRACKET = ']'; + SEMICOLON = ';'; + BAR = '|'; + DOT = '.'; + + SQHASH = '[#'; + HASHSQ = '#]'; + PARENHASH = '(#'; + HASHPAREN = '#)'; + + // Operators + + ARROW_TOK = '->'; + DIV_TOK = '/'; + EQUAL_TOK = '='; + DISEQUAL_TOK = '/='; + EXP_TOK = '^'; + GT_TOK = '>'; + GEQ_TOK = '>='; + IFF_TOK = '<=>'; + IMPLIES_TOK = '=>'; + LT_TOK = '<'; + LEQ_TOK = '<='; + MINUS_TOK = '-'; + PLUS_TOK = '+'; + STAR_TOK = '*'; + ASSIGN_TOK = ':='; + MOD_TOK = 'MOD'; + INTDIV_TOK = 'DIV'; + FLOOR_TOK = 'FLOOR'; + + //IS_INTEGER_TOK = 'IS_INTEGER'; + + // Bitvectors + + BITVECTOR_TOK = 'BITVECTOR'; + LEFTSHIFT_TOK = '<<'; + RIGHTSHIFT_TOK = '>>'; + BVPLUS_TOK = 'BVPLUS'; + BVSUB_TOK = 'BVSUB'; + BVUDIV_TOK = 'BVUDIV'; + BVSDIV_TOK = 'BVSDIV'; + BVUREM_TOK = 'BVUREM'; + BVSREM_TOK = 'BVSREM'; + BVSMOD_TOK = 'BVSMOD'; + BVSHL_TOK = 'BVSHL'; + BVASHR_TOK = 'BVASHR'; + BVLSHR_TOK = 'BVLSHR'; + BVUMINUS_TOK = 'BVUMINUS'; + BVMULT_TOK = 'BVMULT'; + BVNEG_TOK = '~'; + BVAND_TOK = '&'; + BVXOR_TOK = 'BVXOR'; + BVNAND_TOK = 'BVNAND'; + BVNOR_TOK = 'BVNOR'; + BVCOMP_TOK = 'BVCOMP'; + BVXNOR_TOK = 'BVXNOR'; + CONCAT_TOK = '@'; + BVTOINT_TOK = 'BVTOINT'; + INTTOBV_TOK = 'INTTOBV'; + BOOLEXTRACT_TOK = 'BOOLEXTRACT'; + BVLT_TOK = 'BVLT'; + BVGT_TOK = 'BVGT'; + BVLE_TOK = 'BVLE'; + BVGE_TOK = 'BVGE'; + SX_TOK = 'SX'; + BVZEROEXTEND_TOK = 'BVZEROEXTEND'; + BVREPEAT_TOK = 'BVREPEAT'; + BVROTL_TOK = 'BVROTL'; + BVROTR_TOK = 'BVROTR'; + BVSLT_TOK = 'BVSLT'; + BVSGT_TOK = 'BVSGT'; + BVSLE_TOK = 'BVSLE'; + BVSGE_TOK = 'BVSGE'; +} + +@parser::members { + +// Idea and code guidance from Sam Harwell, +// http://www.antlr.org/wiki/display/ANTLR3/Operator+precedence+parser + +bool isRightToLeft(int type) { + // return true here for any operators that are right-to-left associative + switch(type) { + case IMPLIES_TOK: return true; + default: return false; + } +} + +int getOperatorPrecedence(int type) { + switch(type) { + case BITVECTOR_TOK: return 1; + case DOT: + case LPAREN: + case LBRACE: return 2; + case LBRACKET: return 3; + case ARROW_TOK: return 4; + //case IS_INTEGER_TOK: return 5; + case BVSLT_TOK: + case BVSLE_TOK: + case BVSGT_TOK: + case BVSGE_TOK: return 6; + case BVLT_TOK: + case BVLE_TOK: + case BVGT_TOK: + case BVGE_TOK: return 7; + case LEFTSHIFT_TOK: + case RIGHTSHIFT_TOK: return 8; + case SX_TOK: + case BVZEROEXTEND_TOK: + case BVREPEAT_TOK: + case BVROTL_TOK: + case BVROTR_TOK: return 9; + case BVUDIV_TOK: + case BVSDIV_TOK: + case BVUREM_TOK: + case BVSREM_TOK: + case BVSMOD_TOK: + case BVSHL_TOK: + case BVASHR_TOK: + case BVLSHR_TOK: return 10; + case BVUMINUS_TOK: + case BVPLUS_TOK: + case BVSUB_TOK: return 11; + case BVNEG_TOK: return 12; + case BVXNOR_TOK: return 13; + case BVNOR_TOK: + case BVCOMP_TOK: return 14; + case BVNAND_TOK: return 15; + case BVXOR_TOK: return 16; + case BVAND_TOK: return 17; + case BAR: return 18; + case CONCAT_TOK: return 19; +//case UMINUS_TOK: return 20; + case WITH_TOK: return 21; + case EXP_TOK: return 22; + case STAR_TOK: + case INTDIV_TOK: + case DIV_TOK: + case MOD_TOK: return 23; + case PLUS_TOK: + case MINUS_TOK: return 24; + case LEQ_TOK: + case LT_TOK: + case GEQ_TOK: + case GT_TOK: + case FLOOR_TOK: return 25; + case EQUAL_TOK: + case DISEQUAL_TOK: return 26; + case NOT_TOK: return 27; + case AND_TOK: return 28; + case OR_TOK: + case XOR_TOK: return 29; + case IMPLIES_TOK: return 30;// right-to-left + case IFF_TOK: return 31; + case FORALL_TOK: + case EXISTS_TOK: return 32; + case ASSIGN_TOK: + case IN_TOK: return 33; + + default: + Unhandled(CvcParserTokenNames[type]); + } +} + +Kind getOperatorKind(int type, bool& negate) { + negate = false; + + switch(type) { + // booleanBinop + case IFF_TOK: return kind::IFF; + case IMPLIES_TOK: return kind::IMPLIES; + case OR_TOK: return kind::OR; + case XOR_TOK: return kind::XOR; + case AND_TOK: return kind::AND; + + // comparisonBinop + case EQUAL_TOK: return kind::EQUAL; + case DISEQUAL_TOK: negate = true; return kind::EQUAL; + case GT_TOK: return kind::GT; + case GEQ_TOK: return kind::GEQ; + case LT_TOK: return kind::LT; + case LEQ_TOK: return kind::LEQ; + + // arithmeticBinop + case PLUS_TOK: return kind::PLUS; + case MINUS_TOK: return kind::MINUS; + case STAR_TOK: return kind::MULT; + case INTDIV_TOK: Unhandled(CvcParserTokenNames[type]); + case DIV_TOK: return kind::DIVISION; + case EXP_TOK: Unhandled(CvcParserTokenNames[type]); + + // concatBitwiseBinop + case CONCAT_TOK: return kind::BITVECTOR_CONCAT; + case BAR: return kind::BITVECTOR_OR; + case BVAND_TOK: return kind::BITVECTOR_AND; + + default: + Unhandled(CvcParserTokenNames[type]); + } +} + +unsigned findPivot(const std::vector& operators, + unsigned startIndex, unsigned stopIndex) { + unsigned pivot = startIndex; + unsigned pivotRank = getOperatorPrecedence(operators[pivot]); + /*Debug("prec") << "initial pivot at " << pivot + << "(" << CvcParserTokenNames[operators[pivot]] << ") " + << "level " << pivotRank << std::endl;*/ + for(unsigned i = startIndex + 1; i <= stopIndex; ++i) { + unsigned current = getOperatorPrecedence(operators[i]); + bool rtl = isRightToLeft(operators[i]); + if(current > pivotRank || (current == pivotRank && !rtl)) { + /*Debug("prec") << "new pivot at " << i + << "(" << CvcParserTokenNames[operators[i]] << ") " + << "level " << current << " rtl == " << rtl << std::endl;*/ + pivot = i; + pivotRank = current; + } + } + return pivot; +} + +Expr createPrecedenceTree(ExprManager* em, + const std::vector& expressions, + const std::vector& operators, + unsigned startIndex, unsigned stopIndex) { + Assert(expressions.size() == operators.size() + 1); + Assert(startIndex < expressions.size()); + Assert(stopIndex < expressions.size()); + Assert(startIndex <= stopIndex); + + if(stopIndex == startIndex) { + return expressions[startIndex]; + } + + unsigned pivot = findPivot(operators, startIndex, stopIndex - 1); + //Debug("prec") << "pivot[" << startIndex << "," << stopIndex - 1 << "] at " << pivot << std::endl; + bool negate; + Expr e = em->mkExpr(getOperatorKind(operators[pivot], negate), + createPrecedenceTree(em, expressions, operators, startIndex, pivot), + createPrecedenceTree(em, expressions, operators, pivot + 1, stopIndex)); + return negate ? em->mkExpr(kind::NOT, e) : e; +} + +Expr createPrecedenceTree(ExprManager* em, + const std::vector& expressions, + const std::vector& operators) { + if(Debug.isOn("prec") && operators.size() > 1) { + for(unsigned i = 0; i < expressions.size(); ++i) { + Debug("prec") << expressions[i]; + if(operators.size() > i) { + Debug("prec") << ' ' << CvcParserTokenNames[operators[i]] << ' '; + } + } + Debug("prec") << std::endl; + } + + Expr e = createPrecedenceTree(em, expressions, operators, 0, expressions.size() - 1); + if(Debug.isOn("prec") && operators.size() > 1) { + Expr::setlanguage::Scope ls(Debug("prec"), language::output::LANG_AST); + Debug("prec") << "=> " << e << std::endl; + } + return e; +} + +}/* @parser::members */ + @header { /** ** This file is part of the CVC4 prototype. @@ -178,21 +495,41 @@ declaration[CVC4::Command*& cmd] Debug("parser-extra") << "declaration: " << AntlrInput::tokenText(LT(1)) << std::endl; } : // FIXME: These could be type or function declarations, if that matters. - identifierList[ids, CHECK_UNDECLARED, SYM_VARIABLE] COLON declType[t,ids] SEMICOLON - { cmd = new DeclarationCommand(ids,t); } + identifierList[ids, CHECK_UNDECLARED, SYM_VARIABLE] COLON declType[t, ids] SEMICOLON + { cmd = new DeclarationCommand(ids, t); } ; /** Match the right-hand side of a declaration. Returns the type. */ declType[CVC4::Type& t, std::vector& idList] @init { + Expr f; Debug("parser-extra") << "declType: " << AntlrInput::tokenText(LT(1)) << std::endl; } : /* A sort declaration (e.g., "T : TYPE") */ TYPE_TOK { PARSER_STATE->mkSorts(idList); t = EXPR_MANAGER->kindType(); } + | /* A type alias */ + TYPE_TOK EQUAL_TOK type[t] + { for(std::vector::const_iterator i = idList.begin(); + i != idList.end(); + ++i) { + PARSER_STATE->defineType(*i, t); + } + t = EXPR_MANAGER->kindType(); } | /* A variable declaration */ - type[t] { PARSER_STATE->mkVars(idList,t); } + type[t] ( EQUAL_TOK formula[f] )? + { if(f.isNull()) { + PARSER_STATE->mkVars(idList, t); + } else { + for(std::vector::const_iterator i = idList.begin(), + i_end = idList.end(); + i != i_end; + ++i) { + PARSER_STATE->defineFunction(*i, f); + } + } + } ; /** @@ -206,16 +543,16 @@ type[CVC4::Type& t] Debug("parser-extra") << "type: " << AntlrInput::tokenText(LT(1)) << std::endl; } : /* Simple type */ - baseType[t] + bitvectorType[t] | /* Single-parameter function type */ baseType[t] ARROW_TOK baseType[t2] - { t = EXPR_MANAGER->mkFunctionType(t,t2); } + { t = EXPR_MANAGER->mkFunctionType(t, t2); } | /* Multi-parameter function type */ LPAREN baseType[t] { typeList.push_back(t); } - (COMMA baseType[t] { typeList.push_back(t); } )+ + ( COMMA baseType[t] { typeList.push_back(t); } )* RPAREN ARROW_TOK baseType[t] - { t = EXPR_MANAGER->mkFunctionType(typeList,t); } + { t = EXPR_MANAGER->mkFunctionType(typeList, t); } ; /** @@ -246,6 +583,24 @@ identifier[std::string& id, PARSER_STATE->checkDeclaration(id, check, type); } ; +/** + * Matches a bitvector type. + */ +bitvectorType[CVC4::Type& t] + : arrayType[t] + | BITVECTOR_TOK LPAREN INTEGER_LITERAL RPAREN + { t = EXPR_MANAGER->mkBitVectorType(AntlrInput::tokenToUnsigned($INTEGER_LITERAL)); } + ; + +arrayType[CVC4::Type& t] +@init { + Type t2; +} + : baseType[t] + | ARRAY_TOK baseType[t] OF_TOK baseType[t2] + { t = EXPR_MANAGER->mkArrayType(t, t2); } + ; + /** * Matches a type (which MUST be already declared). * @@ -262,9 +617,7 @@ baseType[CVC4::Type& t] * CHECK_DECLARED and the type is not declared, an exception is * thrown. * - * @return the type identifier - * - * @TODO parse more types + * @return the type identifier in 't', and the id (where applicable) in 'id' */ maybeUndefinedBaseType[CVC4::Type& t, CVC4::parser::DeclarationCheck check] returns [CVC4::parser::cvc::mystring id] @@ -336,7 +689,7 @@ letBinding[CVC4::Expr& f] letDecls IN_TOK letBinding[f] { PARSER_STATE->popScope(); } - | iffFormula[f] + | booleanFormula[f] ; /** @@ -359,193 +712,305 @@ letDecl { PARSER_STATE->defineVar(name, e); } ; -/** - * Matches a Boolean IFF formula (right-associative) - */ -iffFormula[CVC4::Expr& f] +booleanFormula[CVC4::Expr& f] @init { - Expr e; - Debug("parser-extra") << "<=> formula: " << AntlrInput::tokenText(LT(1)) << std::endl; + std::vector expressions; + std::vector operators; + unsigned op; + unsigned notCount = 0; } - : impliesFormula[f] - ( IFF_TOK - iffFormula[e] - { f = MK_EXPR(CVC4::kind::IFF, f, e); } - )? + : ( NOT_TOK { ++notCount; } )* comparison[f] + { while(notCount > 0) { + --notCount; + f = EXPR_MANAGER->mkExpr(kind::NOT, f); + } + expressions.push_back(f); } + ( booleanBinop[op] ( NOT_TOK { ++notCount; } )* comparison[f] + { operators.push_back(op); + while(notCount > 0) { + --notCount; + f = EXPR_MANAGER->mkExpr(kind::NOT, f); + } + expressions.push_back(f); + } + )* + { f = createPrecedenceTree(EXPR_MANAGER, expressions, operators); } ; -/** - * Matches a Boolean IMPLIES formula (right-associative) - */ -impliesFormula[CVC4::Expr& f] +booleanBinop[unsigned& op] @init { - Expr e; - Debug("parser-extra") << "=> Formula: " << AntlrInput::tokenText(LT(1)) << std::endl; + op = LT(1)->getType(LT(1)); } - : orFormula[f] - ( IMPLIES_TOK impliesFormula[e] - { f = MK_EXPR(CVC4::kind::IMPLIES, f, e); } - )? + : IFF_TOK + | IMPLIES_TOK + | OR_TOK + | XOR_TOK + | AND_TOK ; -/** - * Matches a Boolean OR formula (left-associative) - */ -orFormula[CVC4::Expr& f] +comparison[CVC4::Expr& f] @init { - std::vector exprs; - Debug("parser-extra") << "OR Formula: " << AntlrInput::tokenText(LT(1)) << std::endl; + std::vector expressions; + std::vector operators; + unsigned op; } - : xorFormula[f] - ( OR_TOK { exprs.push_back(f); } - xorFormula[f] { exprs.push_back(f); } )* - { - if( exprs.size() > 0 ) { - f = MK_EXPR(CVC4::kind::OR, exprs); - } - } + : term[f] { expressions.push_back(f); } + ( comparisonBinop[op] term[f] + { operators.push_back(op); expressions.push_back(f); } )* + { f = createPrecedenceTree(EXPR_MANAGER, expressions, operators); } ; -/** - * Matches a Boolean XOR formula (left-associative) - */ -xorFormula[CVC4::Expr& f] +comparisonBinop[unsigned& op] @init { - Expr e; - Debug("parser-extra") << "XOR formula: " << AntlrInput::tokenText(LT(1)) << std::endl; + op = LT(1)->getType(LT(1)); } - : andFormula[f] - ( XOR_TOK andFormula[e] - { f = MK_EXPR(CVC4::kind::XOR,f, e); } - )* + : EQUAL_TOK + | DISEQUAL_TOK + | GT_TOK + | GEQ_TOK + | LT_TOK + | LEQ_TOK ; -/** - * Matches a Boolean AND formula (left-associative) - */ -andFormula[CVC4::Expr& f] +term[CVC4::Expr& f] @init { - std::vector exprs; - Debug("parser-extra") << "AND Formula: " << AntlrInput::tokenText(LT(1)) << std::endl; + std::vector expressions; + std::vector operators; + unsigned op; } - : notFormula[f] - ( AND_TOK { exprs.push_back(f); } - notFormula[f] { exprs.push_back(f); } )* - { - if( exprs.size() > 0 ) { - f = MK_EXPR(CVC4::kind::AND, exprs); - } - } + : storeTerm[f] { expressions.push_back(f); } + ( arithmeticBinop[op] storeTerm[f] { operators.push_back(op); expressions.push_back(f); } )* + { f = createPrecedenceTree(EXPR_MANAGER, expressions, operators); } ; -/** - * Parses a NOT formula. - * @return the expression representing the formula - */ -notFormula[CVC4::Expr& f] +arithmeticBinop[unsigned& op] @init { - Debug("parser-extra") << "NOT formula: " << AntlrInput::tokenText(LT(1)) << std::endl; + op = LT(1)->getType(LT(1)); } - : /* negation */ - NOT_TOK notFormula[f] - { f = MK_EXPR(CVC4::kind::NOT, f); } - | /* a boolean atom */ - comparisonFormula[f] + : PLUS_TOK + | MINUS_TOK + | STAR_TOK + | INTDIV_TOK + | DIV_TOK + | EXP_TOK ; -/** Parses a comparison formula (non-associative). - NOTE: equality should technically have higher precedence than - greater-than, less-than, etc., but I don't think this will ever - be relevant in a well-typed formula. -*/ -comparisonFormula[CVC4::Expr& f] +/** Parses an array store term. */ +storeTerm[CVC4::Expr& f] @init { - Expr e; - Kind op; - bool negate; - Debug("parser-extra") << "predicate formula: " << AntlrInput::tokenText(LT(1)) << std::endl; -} - : plusTerm[f] - ( ( EQUAL_TOK { op = CVC4::kind::EQUAL; negate = false; } - | DISEQUAL_TOK { op = CVC4::kind::EQUAL; negate = true; } - | GT_TOK { op = CVC4::kind::GT; negate = false; } - | GEQ_TOK { op = CVC4::kind::GEQ; negate = false; } - | LT_TOK { op = CVC4::kind::LT; negate = false; } - | LEQ_TOK { op = CVC4::kind::LEQ; negate = false; }) - plusTerm[e] - { f = MK_EXPR(op, f, e); - if(negate) { - f = MK_EXPR(CVC4::kind::NOT, f); - } + Expr f2, f3; +} + : uminusTerm[f] ( WITH_TOK + LBRACKET formula[f2] RBRACKET ASSIGN_TOK uminusTerm[f3] + { f = MK_EXPR(CVC4::kind::STORE, f, f2, f3); } + ( COMMA LBRACKET formula[f2] RBRACKET ASSIGN_TOK uminusTerm[f3] + { f = MK_EXPR(CVC4::kind::STORE, f, f2, f3); } )* )* + ; + +/** Parses a unary minus term. */ +uminusTerm[CVC4::Expr& f] +@init { + unsigned minusCount = 0; +} + : /* Unary minus */ +// (MINUS_TOK { ++minusCount; })* concatBitwiseTerm[f] + (MINUS_TOK { ++minusCount; })+ concatBitwiseTerm[f] + { while(minusCount > 0) { --minusCount; f = MK_EXPR(CVC4::kind::UMINUS, f); } } + | concatBitwiseTerm[f] + ; + +/** Parses bitvectors. */ + +concatBitwiseTerm[CVC4::Expr& f] +@init { + std::vector expressions; + std::vector operators; + unsigned op; +} + : bitwiseXorTerm[f] { expressions.push_back(f); } + ( concatBitwiseBinop[op] bitwiseXorTerm[f] { operators.push_back(op); expressions.push_back(f); } )* + { f = createPrecedenceTree(EXPR_MANAGER, expressions, operators); } + ; +concatBitwiseBinop[unsigned& op] +@init { + op = LT(1)->getType(LT(1)); +} + : CONCAT_TOK + | BAR + | BVAND_TOK + ; + +bitwiseXorTerm[CVC4::Expr& f] +@init { + Expr f2; +} + : /* BV xor */ + BVXOR_TOK LPAREN formula[f] COMMA formula[f] RPAREN + { f = MK_EXPR(CVC4::kind::BITVECTOR_XOR, f, f2); } + | BVNAND_TOK LPAREN formula[f] COMMA formula[f] RPAREN + { f = MK_EXPR(CVC4::kind::BITVECTOR_NAND, f, f2); } + | BVNOR_TOK LPAREN formula[f] COMMA formula[f] RPAREN + { f = MK_EXPR(CVC4::kind::BITVECTOR_NOR, f, f2); } + | BVCOMP_TOK LPAREN formula[f] COMMA formula[f] RPAREN + { f = MK_EXPR(CVC4::kind::BITVECTOR_COMP, f, f2); } + | BVXNOR_TOK LPAREN formula[f] COMMA formula[f] RPAREN + { f = MK_EXPR(CVC4::kind::BITVECTOR_XNOR, f, f2); } + | bvNegTerm[f] + ; +bvNegTerm[CVC4::Expr& f] + : /* BV neg */ + BVNEG_TOK bvNegTerm[f] + { f = MK_EXPR(CVC4::kind::BITVECTOR_NOT, f); } + | bvUminusTerm[f] + ; +bvUminusTerm[CVC4::Expr& f] +@init { + Expr f2; +} + : /* BV unary minus */ + BVUMINUS_TOK LPAREN formula[f] RPAREN + { f = MK_EXPR(CVC4::kind::BITVECTOR_NEG, f); } + | BVPLUS_TOK LPAREN INTEGER_LITERAL COMMA formula[f] + ( COMMA formula[f2] { f = MK_EXPR(CVC4::kind::BITVECTOR_PLUS, f, f2); } )+ RPAREN + { unsigned size = BitVectorType(f.getType()).getSize(); + unsigned k = AntlrInput::tokenToUnsigned($INTEGER_LITERAL); + if(k == 0) { + PARSER_STATE->parseError("BVPLUS(k,_,_,...) must have k > 0"); } - )? + if(k > size) { + f = MK_EXPR(MK_CONST(BitVectorZeroExtend(k)), f); + } else if(k < size) { + f = MK_EXPR(MK_CONST(BitVectorExtract(0, k - 1)), f); + } + } + | BVSUB_TOK LPAREN INTEGER_LITERAL COMMA formula[f] COMMA formula[f2] RPAREN + { f = MK_EXPR(CVC4::kind::BITVECTOR_SUB, f, f2); + unsigned k = AntlrInput::tokenToUnsigned($INTEGER_LITERAL); + if(k == 0) { + PARSER_STATE->parseError("BVSUB(k,_,_) must have k > 0"); + } + unsigned size = BitVectorType(f.getType()).getSize(); + if(k > size) { + f = MK_EXPR(MK_CONST(BitVectorZeroExtend(k)), f); + } else if(k < size) { + f = MK_EXPR(MK_CONST(BitVectorExtract(0, k - 1)), f); + } + } + | BVMULT_TOK LPAREN INTEGER_LITERAL COMMA formula[f] COMMA formula[f2] RPAREN + { MK_EXPR(CVC4::kind::BITVECTOR_MULT, f, f2); + unsigned k = AntlrInput::tokenToUnsigned($INTEGER_LITERAL); + if(k == 0) { + PARSER_STATE->parseError("BVMULT(k,_,_) must have k > 0"); + } + unsigned size = BitVectorType(f.getType()).getSize(); + if(k > size) { + f = MK_EXPR(MK_CONST(BitVectorZeroExtend(k)), f); + } else if(k < size) { + f = MK_EXPR(MK_CONST(BitVectorExtract(0, k - 1)), f); + } + } + | BVUDIV_TOK LPAREN formula[f] COMMA formula[f2] RPAREN + { f = MK_EXPR(CVC4::kind::BITVECTOR_UDIV, f, f2); } + | BVSDIV_TOK LPAREN formula[f] COMMA formula[f2] RPAREN + { f = MK_EXPR(CVC4::kind::BITVECTOR_SDIV, f, f2); } + | BVUREM_TOK LPAREN formula[f] COMMA formula[f2] RPAREN + { f = MK_EXPR(CVC4::kind::BITVECTOR_UREM, f, f2); } + | BVSREM_TOK LPAREN formula[f] COMMA formula[f2] RPAREN + { f = MK_EXPR(CVC4::kind::BITVECTOR_SREM, f, f2); } + | BVSMOD_TOK LPAREN formula[f] COMMA formula[f2] RPAREN + { f = MK_EXPR(CVC4::kind::BITVECTOR_SMOD, f, f2); } + | BVSHL_TOK LPAREN formula[f] COMMA formula[f2] RPAREN + { f = MK_EXPR(CVC4::kind::BITVECTOR_SHL, f, f2); } + | BVASHR_TOK LPAREN formula[f] COMMA formula[f2] RPAREN + { f = MK_EXPR(CVC4::kind::BITVECTOR_ASHR, f, f2); } + | BVLSHR_TOK LPAREN formula[f] COMMA formula[f2] RPAREN + { f = MK_EXPR(CVC4::kind::BITVECTOR_LSHR, f, f2); } + | SX_TOK LPAREN formula[f] COMMA INTEGER_LITERAL RPAREN + { unsigned k = AntlrInput::tokenToUnsigned($INTEGER_LITERAL); + f = MK_EXPR(MK_CONST(BitVectorSignExtend(k)), f); } + | BVZEROEXTEND_TOK LPAREN formula[f] COMMA INTEGER_LITERAL RPAREN + { unsigned k = AntlrInput::tokenToUnsigned($INTEGER_LITERAL); + f = MK_EXPR(MK_CONST(BitVectorSignExtend(k)), f); } + | BVREPEAT_TOK LPAREN formula[f] COMMA INTEGER_LITERAL RPAREN + { unsigned k = AntlrInput::tokenToUnsigned($INTEGER_LITERAL); + f = MK_EXPR(MK_CONST(BitVectorRepeat(k)), f); } + | BVROTR_TOK LPAREN formula[f] COMMA INTEGER_LITERAL RPAREN + { unsigned k = AntlrInput::tokenToUnsigned($INTEGER_LITERAL); + f = MK_EXPR(MK_CONST(BitVectorSignExtend(k)), f); } + | BVROTL_TOK LPAREN formula[f] COMMA INTEGER_LITERAL RPAREN + { unsigned k = AntlrInput::tokenToUnsigned($INTEGER_LITERAL); + f = MK_EXPR(MK_CONST(BitVectorRotateLeft(k)), f); } + | bvShiftTerm[f] ; -/** Parses a plus/minus term (left-associative). - TODO: This won't take advantage of n-ary PLUS's. */ -plusTerm[CVC4::Expr& f] +bvShiftTerm[CVC4::Expr& f] @init { - Expr e; - Kind op; - std::vector exprs; - Debug("parser-extra") << "plus term: " << AntlrInput::tokenText(LT(1)) << std::endl; -} - : multTerm[f] - ( ( PLUS_TOK { op = CVC4::kind::PLUS; } - | MINUS_TOK { op = CVC4::kind::MINUS; } ) - multTerm[e] - { f = MK_EXPR(op, f, e); } - )* + std::vector expressions; + std::vector operators; + unsigned op; +} + : bvComparison[f] + ( ( LEFTSHIFT_TOK | RIGHTSHIFT_TOK) INTEGER_LITERAL + { unsigned k = AntlrInput::tokenToUnsigned($INTEGER_LITERAL); + f = MK_EXPR(MK_CONST(BitVectorRotateLeft(k)), f); } + )? ; -/** Parses a multiply/divide term (left-associative). - TODO: This won't take advantage of n-ary MULT's. */ -multTerm[CVC4::Expr& f] +bvComparison[CVC4::Expr& f] @init { - Expr e; - Kind op; - Debug("parser-extra") << "multiplication term: " << AntlrInput::tokenText(LT(1)) << std::endl; -} - : expTerm[f] - ( ( STAR_TOK { op = CVC4::kind::MULT; } - | DIV_TOK { op = CVC4::kind::DIVISION; } ) - expTerm[e] - { f = MK_EXPR(op, f, e); } - )* + Expr f2; +} + : /* BV comparison */ + BVLT_TOK LPAREN formula[f] COMMA formula[f2] RPAREN + { f = MK_EXPR(CVC4::kind::BITVECTOR_ULT, f, f2); } + | BVLE_TOK LPAREN formula[f] COMMA formula[f2] RPAREN + { f = MK_EXPR(CVC4::kind::BITVECTOR_ULE, f, f2); } + | BVGT_TOK LPAREN formula[f] COMMA formula[f2] RPAREN + { f = MK_EXPR(CVC4::kind::BITVECTOR_UGT, f, f2); } + | BVGE_TOK LPAREN formula[f] COMMA formula[f2] RPAREN + { f = MK_EXPR(CVC4::kind::BITVECTOR_UGE, f, f2); } + | BVSLT_TOK LPAREN formula[f] COMMA formula[f2] RPAREN + { f = MK_EXPR(CVC4::kind::BITVECTOR_SLT, f, f2); } + | BVSLE_TOK LPAREN formula[f] COMMA formula[f2] RPAREN + { f = MK_EXPR(CVC4::kind::BITVECTOR_SLE, f, f2); } + | BVSGT_TOK LPAREN formula[f] COMMA formula[f2] RPAREN + { f = MK_EXPR(CVC4::kind::BITVECTOR_SGT, f, f2); } + | BVSGE_TOK LPAREN formula[f] COMMA formula[f2] RPAREN + { f = MK_EXPR(CVC4::kind::BITVECTOR_SGE, f, f2); } + /* + | IS_INTEGER_TOK LPAREN formula[f] RPAREN + { f = MK_EXPR(CVC4::kind::BITVECTOR_IS_INTEGER, f); } + */ + | selectExtractTerm[f] ; -/** - * Parses an exponential term (left-associative). - * NOTE that the exponent must be a nonnegative integer constant - * (for now). - */ -expTerm[CVC4::Expr& f] +/** Parses an array select. */ +selectExtractTerm[CVC4::Expr& f] @init { - Expr e; - Debug("parser-extra") << "exponential term: " << AntlrInput::tokenText(LT(1)) << std::endl; -} - : unaryTerm[f] - ( EXP_TOK INTEGER_LITERAL - { Integer n = AntlrInput::tokenToInteger($INTEGER_LITERAL); - if(n == 0) { - f = MK_CONST( Integer(1) ); - } else if(n == 1) { - /* f remains the same */ - } else { - std::vector v; - for(Integer i = 0; i < n; i = i + 1) { - v.push_back(f); + Expr f2; + bool extract; +} + : /* array select / bitvector extract */ + simpleTerm[f] + ( { extract = false; } + LBRACKET formula[f2] ( COLON INTEGER_LITERAL { extract = true; } )? RBRACKET + { if(extract) { + if(f2.getKind() != kind::CONST_INTEGER) { + PARSER_STATE->parseError("bitvector extraction requires [INTEGER_LITERAL:INTEGER_LITERAL] range"); } - f = MK_EXPR(CVC4::kind::MULT, v); + unsigned k1 = f2.getConst().getLong(); + unsigned k2 = AntlrInput::tokenToUnsigned($INTEGER_LITERAL); + f = MK_EXPR(MK_CONST(BitVectorExtract(k1, k2)), f); + } else { + f = MK_EXPR(CVC4::kind::SELECT, f, f2); } } )* + ; -/** - * Parses a unary term. - */ -unaryTerm[CVC4::Expr& f] +/** Parses a simple term. */ +simpleTerm[CVC4::Expr& f] @init { std::string name; std::vector args; @@ -574,18 +1039,22 @@ unaryTerm[CVC4::Expr& f] | /* if-then-else */ iteTerm[f] - | /* Unary minus */ - MINUS_TOK unaryTerm[f] { f = MK_EXPR(CVC4::kind::UMINUS, f); } - | /* parenthesized sub-formula */ LPAREN formula[f] RPAREN /* constants */ | TRUE_TOK { f = MK_CONST(true); } | FALSE_TOK { f = MK_CONST(false); } - | INTEGER_LITERAL { f = MK_CONST( AntlrInput::tokenToInteger($INTEGER_LITERAL) ); } | DECIMAL_LITERAL { f = MK_CONST( AntlrInput::tokenToRational($DECIMAL_LITERAL) ); } + | HEX_LITERAL + { Assert( AntlrInput::tokenText($HEX_LITERAL).find("0hex") == 0 ); + std::string hexString = AntlrInput::tokenTextSubstr($HEX_LITERAL, 4); + f = MK_CONST( BitVector(hexString, 16) ); } + | BINARY_LITERAL + { Assert( AntlrInput::tokenText($BINARY_LITERAL).find("0bin") == 0 ); + std::string binString = AntlrInput::tokenTextSubstr($BINARY_LITERAL, 4); + f = MK_CONST( BitVector(binString, 2) ); } | /* variable */ identifier[name,CHECK_DECLARED,SYM_VARIABLE] @@ -653,7 +1122,7 @@ datatypeDef[std::vector& datatypes] : identifier[id,CHECK_UNDECLARED,SYM_SORT] { datatypes.push_back(Datatype(id)); } EQUAL_TOK constructorDef[datatypes.back()] - ( BAR_TOK constructorDef[datatypes.back()] )* + ( BAR constructorDef[datatypes.back()] )* ; /** @@ -689,7 +1158,13 @@ selector[CVC4::Datatype::Constructor& ctor] std::string id; Type type; } - : identifier[id,CHECK_UNDECLARED,SYM_SORT] COLON maybeUndefinedBaseType[type,CHECK_NONE] + : identifier[id,CHECK_UNDECLARED,SYM_SORT] COLON + maybeUndefinedBaseType[type,CHECK_NONE] + // TODO: this doesn't permit datatype fields of ARRAY or BITVECTOR + // type. This will be problematic, since, after all, you could + // have something nasty like this: + // + // DATATYPE list = cons(car:ARRAY list OF list, cdr:list) | nil END; { if(type.isNull()) { ctor.addArg(id, Datatype::UnresolvedType($maybeUndefinedBaseType.id)); } else { @@ -699,70 +1174,6 @@ selector[CVC4::Datatype::Constructor& ctor] } ; -// Keywords - -AND_TOK : 'AND'; -ASSERT_TOK : 'ASSERT'; -BOOLEAN_TOK : 'BOOLEAN'; -CHECKSAT_TOK : 'CHECKSAT'; -ECHO_TOK : 'ECHO'; -ELSEIF_TOK : 'ELSIF'; -ELSE_TOK : 'ELSE'; -ENDIF_TOK : 'ENDIF'; -FALSE_TOK : 'FALSE'; -IF_TOK : 'IF'; -IN_TOK : 'IN'; -INT_TOK : 'INT'; -LET_TOK : 'LET'; -NOT_TOK : 'NOT'; -OPTION_TOK : 'OPTION'; -OR_TOK : 'OR'; -POPTO_TOK : 'POPTO'; -POP_TOK : 'POP'; -PRINT_TOK : 'PRINT'; -PUSH_TOK : 'PUSH'; -QUERY_TOK : 'QUERY'; -REAL_TOK : 'REAL'; -THEN_TOK : 'THEN'; -TRUE_TOK : 'TRUE'; -TYPE_TOK : 'TYPE'; -XOR_TOK : 'XOR'; - -DATATYPE_TOK : 'DATATYPE'; -END_TOK : 'END'; -BAR_TOK : '|'; - -ARRAY_TOK : 'ARRAY'; -OF_TOK : 'OF'; -WITH_TOK : 'WITH'; - -BITVECTOR_TOK : 'BITVECTOR'; - -// Symbols - -COLON : ':'; -COMMA : ','; -LPAREN : '('; -RPAREN : ')'; -SEMICOLON : ';'; - -// Operators - -ARROW_TOK : '->'; -DIV_TOK : '/'; -EQUAL_TOK : '='; -DISEQUAL_TOK : '/='; -EXP_TOK : '^'; -GT_TOK : '>'; -GEQ_TOK : '>='; -IFF_TOK : '<=>'; -IMPLIES_TOK : '=>'; -LT_TOK : '<'; -LEQ_TOK : '<='; -MINUS_TOK : '-'; -PLUS_TOK : '+'; -STAR_TOK : '*'; - /** * Matches an identifier from the input. An identifier is a sequence of letters, * digits and "_", "'", "." symbols, starting with a letter. @@ -779,6 +1190,20 @@ INTEGER_LITERAL: DIGIT+; */ DECIMAL_LITERAL: DIGIT+ '.' DIGIT+; +/** + * Matches a hexadecimal constant. + */ +HEX_LITERAL + : '0hex' HEX_DIGIT+ + ; + +/** + * Matches a binary constant. + */ +BINARY_LITERAL + : '0bin' ('0' | '1')+ + ; + /** * Matches a double quoted string literal. Escaping is supported, and * escape character '\' has to be escaped. @@ -795,6 +1220,8 @@ fragment ALPHA : 'a'..'z' | 'A'..'Z'; */ fragment DIGIT : '0'..'9'; +fragment HEX_DIGIT : DIGIT | 'a'..'f' | 'A'..'F'; + /** * Matches and skips whitespace in the input and ignores it. */ diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index a5a633e48..d27abc735 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -448,6 +448,7 @@ term[CVC4::Expr& expr] { Assert( AntlrInput::tokenText($BINARY_LITERAL).find("#b") == 0 ); std::string binString = AntlrInput::tokenTextSubstr($BINARY_LITERAL, 2); expr = MK_CONST( BitVector(binString, 2) ); } + // NOTE: Theory constants go here ; -- cgit v1.2.3