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/input.h | |
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/input.h')
-rw-r--r-- | src/parser/input.h | 13 |
1 files changed, 6 insertions, 7 deletions
diff --git a/src/parser/input.h b/src/parser/input.h index d47ca4d12..6f30724d1 100644 --- a/src/parser/input.h +++ b/src/parser/input.h @@ -29,7 +29,6 @@ #include "expr/expr.h" #include "expr/expr_manager.h" #include "parser/parser_exception.h" -#include "util/Assert.h" #include "util/language.h" namespace CVC4 { @@ -111,7 +110,7 @@ public: static Input* newFileInput(InputLanguage lang, const std::string& filename, bool useMmap = false) - throw (InputStreamException, AssertionException); + throw (InputStreamException); /** Create an input for the given stream. * @@ -126,7 +125,7 @@ public: std::istream& input, const std::string& name, bool lineBuffered = false) - throw (InputStreamException, AssertionException); + throw (InputStreamException); /** Create an input for the given string * @@ -137,7 +136,7 @@ public: static Input* newStringInput(InputLanguage lang, const std::string& input, const std::string& name) - throw (InputStreamException, AssertionException); + throw (InputStreamException); /** Destructor. Frees the input stream and closes the input. */ @@ -172,7 +171,7 @@ protected: * @throws ParserException if an error is encountered during parsing. */ virtual Command* parseCommand() - throw (ParserException, TypeCheckingException, AssertionException) = 0; + throw (ParserException, TypeCheckingException) = 0; /** * Issue a warning to the user, with source file, line, and column info. @@ -183,7 +182,7 @@ protected: * Throws a <code>ParserException</code> with the given message. */ virtual void parseError(const std::string& msg) - throw (ParserException, AssertionException) = 0; + throw (ParserException) = 0; /** Parse an expression from the input by invoking the * implementation-specific parsing method. Returns a null @@ -192,7 +191,7 @@ protected: * @throws ParserException if an error is encountered during parsing. */ virtual Expr parseExpr() - throw (ParserException, TypeCheckingException, AssertionException) = 0; + throw (ParserException, TypeCheckingException) = 0; /** Set the Parser object for this input. */ virtual void setParser(Parser& parser) = 0; |