diff options
Diffstat (limited to 'src/parser/cvc/Cvc.g')
-rw-r--r-- | src/parser/cvc/Cvc.g | 35 |
1 files changed, 20 insertions, 15 deletions
diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g index 4577b504c..b496aa91c 100644 --- a/src/parser/cvc/Cvc.g +++ b/src/parser/cvc/Cvc.g @@ -288,7 +288,9 @@ int getOperatorPrecedence(int type) { case IN_TOK: return 33; default: - Unhandled(CvcParserTokenNames[type]); + std::stringstream ss; + ss << "internal error: no entry in precedence table for operator " << CvcParserTokenNames[type]; + throw ParserException(ss.str()); } }/* getOperatorPrecedence() */ @@ -318,16 +320,18 @@ 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: Unhandled(CvcParserTokenNames[type]); + case EXP_TOK: break; // bvBinop case CONCAT_TOK: return kind::BITVECTOR_CONCAT; case BAR: return kind::BITVECTOR_OR; case BVAND_TOK: return kind::BITVECTOR_AND; - - default: - Unhandled(CvcParserTokenNames[type]); } + + std::stringstream ss; + ss << "internal error: no entry in operator-kind table for operator " << CvcParserTokenNames[type]; + throw ParserException(ss.str()); + }/* getOperatorKind() */ unsigned findPivot(const std::vector<unsigned>& operators, @@ -355,10 +359,10 @@ Expr createPrecedenceTree(Parser* parser, ExprManager* em, const std::vector<CVC4::Expr>& expressions, const std::vector<unsigned>& operators, unsigned startIndex, unsigned stopIndex) { - Assert(expressions.size() == operators.size() + 1); - Assert(startIndex < expressions.size()); - Assert(stopIndex < expressions.size()); - Assert(startIndex <= stopIndex); + assert(expressions.size() == operators.size() + 1); + assert(startIndex < expressions.size()); + assert(stopIndex < expressions.size()); + assert(startIndex <= stopIndex); if(stopIndex == startIndex) { return expressions[startIndex]; @@ -450,6 +454,7 @@ Expr addNots(ExprManager* em, size_t n, Expr e) { @parser::includes { #include <stdint.h> +#include <cassert> #include "expr/command.h" #include "parser/parser.h" #include "util/subrange_bound.h" @@ -1016,7 +1021,7 @@ type[CVC4::Type& t, /* a type, possibly a function */ : restrictedTypePossiblyFunctionLHS[t,check,lhs] { if(lhs) { - Assert(t.isTuple()); + assert(t.isTuple()); args = TupleType(t).getTypes(); } else { args.push_back(t); @@ -1430,7 +1435,7 @@ arrayStore[CVC4::Expr& f] } : ( LBRACKET formula[f2] { dims.push_back(f2); } RBRACKET )+ ASSIGN_TOK uminusTerm[f3] - { Assert(dims.size() >= 1); + { assert(dims.size() >= 1); // these loops are a bit complicated; they're only used for the // multidimensional ...WITH [a][b] :=... syntax for(unsigned i = 0; i < dims.size() - 1; ++i) { @@ -1630,7 +1635,7 @@ postfixTerm[CVC4::Expr& f] } else if(t.isTester()) { f = MK_EXPR(CVC4::kind::APPLY_TESTER, args); } else { - Unhandled(t); + PARSER_STATE->parseError("internal error: unhandled function application kind"); } } @@ -1864,18 +1869,18 @@ simpleTerm[CVC4::Expr& f] | INTEGER_LITERAL { f = MK_CONST(AntlrInput::tokenToInteger($INTEGER_LITERAL)); } /* bitvector literals */ | HEX_LITERAL - { Assert( AntlrInput::tokenText($HEX_LITERAL).find("0hex") == 0 ); + { 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 ); + { assert( AntlrInput::tokenText($BINARY_LITERAL).find("0bin") == 0 ); std::string binString = AntlrInput::tokenTextSubstr($BINARY_LITERAL, 4); f = MK_CONST( BitVector(binString, 2) ); } /* record literals */ | PARENHASH recordEntry[name,e] { names.push_back(name); args.push_back(e); } ( COMMA recordEntry[name,e] { names.push_back(name); args.push_back(e); } )* HASHPAREN { std::vector< std::pair<std::string, Type> > typeIds; - Assert(names.size() == args.size()); + assert(names.size() == args.size()); for(unsigned i = 0; i < names.size(); ++i) { typeIds.push_back(std::make_pair(names[i], args[i].getType())); } |