diff options
author | Morgan Deters <mdeters@gmail.com> | 2012-09-28 17:29:01 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2012-09-28 17:29:01 +0000 |
commit | 65f720aac2d497c6e829d9c76638073a10060e7d (patch) | |
tree | 357035797e31f96a37dce30cb97ddb0aaf8f3bb7 /src/parser/smt2 | |
parent | c0c351a89871e0a6881668fa1a8d87349ab8af8e (diff) |
Public interface review items:
* Internal uses of CheckArgument changed to AssertArgument/AlwaysAssertArgument()
* Make util/Assert.h cvc4_private instead of public, so AssertionException and friends are now internal-only
* CheckArgument() throws non-AssertionException
* things outside the core library (parsers, driver) use regular C-style assert,
or a public exception type.
* auto-generated documentation for Smt options and internal options
Also, a small fix to SMT-LIBv1 QF_ABV and QF_AUFBV definitions, which were nonstandard.
Diffstat (limited to 'src/parser/smt2')
-rw-r--r-- | src/parser/smt2/Smt2.g | 10 | ||||
-rw-r--r-- | src/parser/smt2/smt2.cpp | 4 | ||||
-rw-r--r-- | src/parser/smt2/smt2_input.cpp | 8 | ||||
-rw-r--r-- | src/parser/smt2/smt2_input.h | 4 |
4 files changed, 15 insertions, 11 deletions
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index fb97d5d1e..1b778f87a 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -587,7 +587,7 @@ term[CVC4::Expr& expr, CVC4::Expr& expr2] args.size() == 1) { /* Unary AND/OR can be replaced with the argument. It just so happens expr should already by the only argument. */ - Assert( expr == args[0] ); + assert( expr == args[0] ); } else if( CVC4::kind::isAssociative(kind) && args.size() > EXPR_MANAGER->maxArity(kind) ) { /* Special treatment for associative operators with lots of children */ @@ -778,12 +778,12 @@ term[CVC4::Expr& expr, CVC4::Expr& expr2] } | HEX_LITERAL - { Assert( AntlrInput::tokenText($HEX_LITERAL).find("#x") == 0 ); + { assert( AntlrInput::tokenText($HEX_LITERAL).find("#x") == 0 ); std::string hexString = AntlrInput::tokenTextSubstr($HEX_LITERAL, 2); expr = MK_CONST( BitVector(hexString, 16) ); } | BINARY_LITERAL - { Assert( AntlrInput::tokenText($BINARY_LITERAL).find("#b") == 0 ); + { assert( AntlrInput::tokenText($BINARY_LITERAL).find("#b") == 0 ); std::string binString = AntlrInput::tokenTextSubstr($BINARY_LITERAL, 2); expr = MK_CONST( BitVector(binString, 2) ); } @@ -1055,7 +1055,9 @@ sortSymbol[CVC4::Type& t, CVC4::parser::DeclarationCheck check] } t = EXPR_MANAGER->mkBitVectorType(numerals.front()); } else { - Unhandled(name); + std::stringstream ss; + ss << "unknown indexed symbol `" << name << "'"; + PARSER_STATE->parseError(ss.str()); } } | LPAREN_TOK symbol[name,CHECK_NONE,SYM_SORT] sortList[args] RPAREN_TOK diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index ca7697810..45caf94a8 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -88,7 +88,9 @@ void Smt2::addTheory(Theory theory) { break; default: - Unhandled(theory); + std::stringstream ss; + ss << "internal error: unsupported theory " << theory; + throw ParserException(ss.str()); } } diff --git a/src/parser/smt2/smt2_input.cpp b/src/parser/smt2/smt2_input.cpp index 8f43b0acf..dd90598bb 100644 --- a/src/parser/smt2/smt2_input.cpp +++ b/src/parser/smt2/smt2_input.cpp @@ -34,7 +34,7 @@ namespace parser { Smt2Input::Smt2Input(AntlrInputStream& inputStream) : AntlrInput(inputStream, 2) { pANTLR3_INPUT_STREAM input = inputStream.getAntlr3InputStream(); - AlwaysAssert( input != NULL ); + assert( input != NULL ); d_pSmt2Lexer = Smt2LexerNew(input); if( d_pSmt2Lexer == NULL ) { @@ -44,7 +44,7 @@ Smt2Input::Smt2Input(AntlrInputStream& inputStream) : setAntlr3Lexer( d_pSmt2Lexer->pLexer ); pANTLR3_COMMON_TOKEN_STREAM tokenStream = getTokenStream(); - AlwaysAssert( tokenStream != NULL ); + assert( tokenStream != NULL ); d_pSmt2Parser = Smt2ParserNew(tokenStream); if( d_pSmt2Parser == NULL ) { @@ -61,12 +61,12 @@ Smt2Input::~Smt2Input() { } Command* Smt2Input::parseCommand() - throw (ParserException, TypeCheckingException, AssertionException) { + throw (ParserException, TypeCheckingException) { return d_pSmt2Parser->parseCommand(d_pSmt2Parser); } Expr Smt2Input::parseExpr() - throw (ParserException, TypeCheckingException, AssertionException) { + throw (ParserException, TypeCheckingException) { return d_pSmt2Parser->parseExpr(d_pSmt2Parser); } diff --git a/src/parser/smt2/smt2_input.h b/src/parser/smt2/smt2_input.h index 05a62c30d..2e36b218e 100644 --- a/src/parser/smt2/smt2_input.h +++ b/src/parser/smt2/smt2_input.h @@ -78,7 +78,7 @@ protected: * @throws ParserException if an error is encountered during parsing. */ Command* parseCommand() - throw(ParserException, TypeCheckingException, AssertionException); + throw(ParserException, TypeCheckingException); /** * Parse an expression from the input. Returns a null @@ -87,7 +87,7 @@ protected: * @throws ParserException if an error is encountered during parsing. */ Expr parseExpr() - throw(ParserException, TypeCheckingException, AssertionException); + throw(ParserException, TypeCheckingException); };/* class Smt2Input */ |