diff options
author | Morgan Deters <mdeters@gmail.com> | 2012-10-09 20:22:01 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2012-10-09 20:22:01 +0000 |
commit | dba60e91f02ae9ca3c3126c76d79a09c95f95a45 (patch) | |
tree | 6fbc624797feec4e934ff3dca2c6038416d999f7 /src/parser | |
parent | 24ef270bb13fc36de9bea4fb92449f5ad8d0770d (diff) |
* make Model class private (as discussed at meeting today)
* fix minor issue with s-expr parsing in CVC and SMT grammars
* other minor things
(this commit was certified error- and warning-free by the test-and-commit script.)
Diffstat (limited to 'src/parser')
-rw-r--r-- | src/parser/cvc/Cvc.g | 17 | ||||
-rw-r--r-- | src/parser/smt2/Smt2.g | 17 |
2 files changed, 20 insertions, 14 deletions
diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g index 22459037d..40f35093f 100644 --- a/src/parser/cvc/Cvc.g +++ b/src/parser/cvc/Cvc.g @@ -320,7 +320,7 @@ Kind getOperatorKind(int type, bool& negate) { case INTDIV_TOK: return kind::INTS_DIVISION; case MOD_TOK: return kind::INTS_MODULUS; case DIV_TOK: return kind::DIVISION; - case EXP_TOK: break; + case EXP_TOK: return kind::POW; // bvBinop case CONCAT_TOK: return kind::BITVECTOR_CONCAT; @@ -570,8 +570,9 @@ parseCommand returns [CVC4::Command* cmd = NULL] { std::string s = AntlrInput::tokenText($IDENTIFIER); if(s == "benchmark") { PARSER_STATE->parseError("In CVC4 presentation language mode, but SMT-LIBv1 format detected. Use --lang smt1 for SMT-LIBv1 support."); - } else if(s == "set" || s == "get") { - PARSER_STATE->parseError("In CVC4 presentation language mode, but SMT-LIBv2 format detected. Use --lang smt2 for SMT-LIBv2 support."); + } else if(s == "set" || s == "get" || s == "declare" || + s == "define" || s == "assert") { + PARSER_STATE->parseError("In CVC4 presentation language mode, but SMT-LIB format detected. Use --lang smt for SMT-LIB support."); } else { PARSER_STATE->parseError("A CVC4 presentation language command cannot begin with a parenthesis; expected command name."); } @@ -782,7 +783,9 @@ simpleSymbolicExpr[CVC4::SExpr& sexpr] CVC4::Rational r; } : INTEGER_LITERAL - { sexpr = SExpr(AntlrInput::tokenToInteger($INTEGER_LITERAL)); } + { sexpr = SExpr(Integer(AntlrInput::tokenText($INTEGER_LITERAL))); } + | MINUS_TOK INTEGER_LITERAL + { sexpr = SExpr(-Integer(AntlrInput::tokenText($INTEGER_LITERAL))); } | DECIMAL_LITERAL { sexpr = SExpr(AntlrInput::tokenToRational($DECIMAL_LITERAL)); } | HEX_LITERAL @@ -1784,15 +1787,15 @@ bvTerm[CVC4::Expr& f] /* BV sign extension */ | SX_TOK LPAREN formula[f] COMMA k=numeral RPAREN { unsigned n = BitVectorType(f.getType()).getSize(); - // Sign extension in TheoryBitVector is defined as in SMT-LIBv2 + // Sign extension in TheoryBitVector is defined as in SMT-LIB // which is different than in the CVC language // SX(BITVECTOR(k), n) in CVC language extends to n bits - // In SMT-LIBv2, such a thing expands to k + n bits + // In SMT-LIB, such a thing expands to k + n bits f = MK_EXPR(MK_CONST(BitVectorSignExtend(k - n)), f); } /* BV zero extension */ | BVZEROEXTEND_TOK LPAREN formula[f] COMMA k=numeral RPAREN { unsigned n = BitVectorType(f.getType()).getSize(); - // Zero extension in TheoryBitVector is defined as in SMT-LIBv2 + // Zero extension in TheoryBitVector is defined as in SMT-LIB // which is the same as in CVC3, but different than SX! // SX(BITVECTOR(k), n) in CVC language extends to n bits // BVZEROEXTEND(BITVECTOR(k), n) in CVC language extends to k + n bits diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index dbefc0305..a49ae35c5 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -5,7 +5,7 @@ ** Major contributors: mdeters ** Minor contributors (to current version): taking ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009-2012 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing @@ -34,7 +34,7 @@ options { @header { /** ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009-2012 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing @@ -124,8 +124,9 @@ namespace CVC4 { using namespace CVC4; using namespace CVC4::parser; -/* These need to be macros so they can refer to the PARSER macro, which will be defined - * by ANTLR *after* this section. (If they were functions, PARSER would be undefined.) */ +/* These need to be macros so they can refer to the PARSER macro, which + * will be defined by ANTLR *after* this section. (If they were functions, + * PARSER would be undefined.) */ #undef PARSER_STATE #define PARSER_STATE ((Smt2*)PARSER->super) #undef EXPR_MANAGER @@ -140,7 +141,8 @@ using namespace CVC4::parser; /** * Parses an expression. - * @return the parsed expression, or the Null Expr if we've reached the end of the input + * @return the parsed expression, or the Null Expr if we've reached the + * end of the input */ parseExpr returns [CVC4::parser::smt2::myExpr expr] @declarations { @@ -160,7 +162,8 @@ parseCommand returns [CVC4::Command* cmd = NULL] ; /** - * Parse the internal portion of the command, ignoring the surrounding parentheses. + * Parse the internal portion of the command, ignoring the surrounding + * parentheses. */ command returns [CVC4::Command* cmd = NULL] @declarations { @@ -631,7 +634,7 @@ simpleSymbolicExpr[CVC4::SExpr& sexpr] std::string s; } : INTEGER_LITERAL - { sexpr = SExpr(AntlrInput::tokenToInteger($INTEGER_LITERAL)); } + { sexpr = SExpr(Integer(AntlrInput::tokenText($INTEGER_LITERAL))); } | DECIMAL_LITERAL { sexpr = SExpr(AntlrInput::tokenToRational($DECIMAL_LITERAL)); } | str[s] |