AntlrInputStream*
AntlrInputStream::newFileInputStream(const std::string& name,
bool useMmap)
- throw (InputStreamException) {
+{
#ifdef _WIN32
if(useMmap) {
useMmap = false;
AntlrInputStream::newStreamInputStream(std::istream& input,
const std::string& name,
bool lineBuffered)
- throw (InputStreamException) {
-
+{
pANTLR3_INPUT_STREAM inputStream = NULL;
pANTLR3_UINT8 inputStringCopy = NULL;
LineBuffer* line_buffer = NULL;
AntlrInputStream*
AntlrInputStream::newStringInputStream(const std::string& input,
const std::string& name)
- throw (InputStreamException) {
-
+{
size_t input_size = input.size();
assert(input_size <= std::numeric_limits<uint32_t>::max());
}
void AntlrInput::parseError(const std::string& message, bool eofException)
- throw (ParserException) {
-
+{
string updatedMessage = parseErrorHelper((const char*)d_antlr3InputStream->getLineBuf(d_antlr3InputStream),
d_lexer->getCharPositionInLine(d_lexer),
message);
* input will use the standard ANTLR3 I/O implementation.
*/
static AntlrInputStream* newFileInputStream(const std::string& name,
- bool useMmap = false)
- throw (InputStreamException);
+ bool useMmap = false);
/** Create an input from an istream. */
static AntlrInputStream* newStreamInputStream(std::istream& input,
const std::string& name,
- bool lineBuffered = false)
- throw (InputStreamException);
+ bool lineBuffered = false);
/** Create a string input.
* NOTE: the new AntlrInputStream will take ownership of input over
* @param name the "filename" to use when reporting errors
*/
static AntlrInputStream* newStringInputStream(const std::string& input,
- const std::string& name)
- throw (InputStreamException);
+ const std::string& name);
};/* class AntlrInputStream */
class Parser;
/**
* Issue a non-fatal warning to the user with file, line, and column info.
*/
- void warning(const std::string& msg);
+ void warning(const std::string& msg) override;
/**
* Throws a <code>ParserException</code> with the given message.
*/
- void parseError(const std::string& msg, bool eofException = false)
- throw (ParserException);
+ void parseError(const std::string& msg, bool eofException = false) override;
/** Set the ANTLR3 lexer for this input. */
void setAntlr3Lexer(pANTLR3_LEXER pLexer);
/** The ANTLR3 CVC parser for the input. */
pCvcParser d_pCvcParser;
-public:
-
+ public:
/** Create an input.
*
* @param inputStream the input to parse
virtual ~CvcInput();
/** Get the language that this Input is reading. */
- InputLanguage getLanguage() const throw() {
+ InputLanguage getLanguage() const override
+ {
return language::input::LANG_CVC4;
}
-protected:
-
+ protected:
/** Parse a command from the input. Returns <code>NULL</code> if there is
* no command there to parse.
*
* @throws ParserException if an error is encountered during parsing.
*/
- Command* parseCommand();
+ Command* parseCommand() override;
/** Parse an expression from the input. Returns a null <code>Expr</code>
* if there is no expression there to parse.
*/
Expr parseExpr();
-private:
-
+ private:
/** Initialize the class. Called from the constructors once the input stream
* is initialized. */
void init();
Input* Input::newFileInput(InputLanguage lang,
const std::string& filename,
bool useMmap)
- throw (InputStreamException) {
+{
AntlrInputStream *inputStream =
AntlrInputStream::newFileInputStream(filename, useMmap);
return AntlrInput::newInput(lang, *inputStream);
std::istream& input,
const std::string& name,
bool lineBuffered)
- throw (InputStreamException) {
+{
AntlrInputStream *inputStream =
AntlrInputStream::newStreamInputStream(input, name, lineBuffered);
return AntlrInput::newInput(lang, *inputStream);
Input* Input::newStringInput(InputLanguage lang,
const std::string& str,
const std::string& name)
- throw (InputStreamException) {
+{
AntlrInputStream *inputStream = AntlrInputStream::newStringInputStream(str, name);
return AntlrInput::newInput(lang, *inputStream);
}
namespace parser {
class CVC4_PUBLIC InputStreamException : public Exception {
-
-public:
+ public:
InputStreamException(const std::string& msg);
- virtual ~InputStreamException() throw() { }
};
/** Wrapper around an input stream. */
* delete on exit. */
bool d_fileIsTemporary;
-protected:
-
+ protected:
/** Initialize the input stream with a name. */
InputStream(std::string name, bool isTemporary=false) :
d_name(name),
d_fileIsTemporary(isTemporary) {
}
-public:
-
+ public:
/** Destructor. */
virtual ~InputStream() {
if( d_fileIsTemporary ) {
Input(const Input& input) CVC4_UNDEFINED;
Input& operator=(const Input& input) CVC4_UNDEFINED;
-public:
-
+ public:
/** Create an input for the given file.
*
* @param lang the input language
*/
static Input* newFileInput(InputLanguage lang,
const std::string& filename,
- bool useMmap = false)
- throw (InputStreamException);
+ bool useMmap = false);
/** Create an input for the given stream.
*
static Input* newStreamInput(InputLanguage lang,
std::istream& input,
const std::string& name,
- bool lineBuffered = false)
- throw (InputStreamException);
+ bool lineBuffered = false);
/** Create an input for the given string
*
*/
static Input* newStringInput(InputLanguage lang,
const std::string& input,
- const std::string& name)
- throw (InputStreamException);
-
+ const std::string& name);
/** Destructor. Frees the input stream and closes the input. */
virtual ~Input();
/** Get the language that this Input is reading. */
- virtual InputLanguage getLanguage() const throw() = 0;
+ virtual InputLanguage getLanguage() const = 0;
/** Retrieve the name of the input stream */
- const std::string getInputStreamName(){
- return getInputStream()->getName();
- }
-
-protected:
-
+ const std::string getInputStreamName() { return getInputStream()->getName(); }
+ protected:
/** Create an input.
*
* @param inputStream the input stream
/**
* Throws a <code>ParserException</code> with the given message.
*/
- virtual void parseError(const std::string& msg, bool eofException = false)
- throw (ParserException) = 0;
+ virtual void parseError(const std::string& msg,
+ bool eofException = false) = 0;
/** Parse an expression from the input by invoking the
* implementation-specific parsing method. Returns a null
}
void Parser::checkDeclaration(const std::string& varName,
- DeclarationCheck check, SymbolType type,
- std::string notes) throw(ParserException) {
+ DeclarationCheck check,
+ SymbolType type,
+ std::string notes)
+{
if (!d_checksEnabled) {
return;
}
}
}
-void Parser::checkFunctionLike(Expr fun) throw(ParserException) {
+void Parser::checkFunctionLike(Expr fun)
+{
if (d_checksEnabled && !isFunctionLike(fun)) {
stringstream ss;
ss << "Expecting function-like symbol, found '";
}
}
-void Parser::checkArity(Kind kind, unsigned numArgs) throw(ParserException) {
+void Parser::checkArity(Kind kind, unsigned numArgs)
+{
if (!d_checksEnabled) {
return;
}
}
}
-void Parser::checkOperator(Kind kind, unsigned numArgs) throw(ParserException) {
+void Parser::checkOperator(Kind kind, unsigned numArgs)
+{
if (d_strictMode && d_logicOperators.find(kind) == d_logicOperators.end()) {
parseError("Operator is not defined in the current logic: " +
kindToString(kind));
void Parser::addOperator(Kind kind) { d_logicOperators.insert(kind); }
void Parser::preemptCommand(Command* cmd) { d_commandQueue.push_back(cmd); }
-
-Command* Parser::nextCommand() throw(ParserException,
- UnsafeInterruptException) {
+Command* Parser::nextCommand()
+{
Debug("parser") << "nextCommand()" << std::endl;
Command* cmd = NULL;
if (!d_commandQueue.empty()) {
return cmd;
}
-Expr Parser::nextExpression() throw(ParserException, UnsafeInterruptException) {
+Expr Parser::nextExpression()
+{
Debug("parser") << "nextExpression()" << std::endl;
const Options& options = d_exprManager->getOptions();
d_resourceManager->spendResource(options.getParseStep());
* @param notes notes to add to a parse error (if one is generated)
* @throws ParserException if checks are enabled and the check fails
*/
- void checkDeclaration(const std::string& name, DeclarationCheck check,
+ void checkDeclaration(const std::string& name,
+ DeclarationCheck check,
SymbolType type = SYM_VARIABLE,
- std::string notes = "") throw(ParserException);
+ std::string notes = "");
/**
* Reserve a symbol at the assertion level.
* @throws ParserException if checks are enabled and fun is not
* a function
*/
- void checkFunctionLike(Expr fun) throw(ParserException);
+ void checkFunctionLike(Expr fun);
/**
* Check that <code>kind</code> can accept <code>numArgs</code> arguments.
* <code>kind</code> cannot be applied to <code>numArgs</code>
* arguments.
*/
- void checkArity(Kind kind, unsigned numArgs) throw(ParserException);
+ void checkArity(Kind kind, unsigned numArgs);
/**
* Check that <code>kind</code> is a legal operator in the current
* @throws ParserException if the parser mode is strict and the
* operator <code>kind</code> has not been enabled
*/
- void checkOperator(Kind kind, unsigned numArgs) throw(ParserException);
+ void checkOperator(Kind kind, unsigned numArgs);
/** Create a new CVC4 variable expression of the given type.
*
bool isPredicate(const std::string& name);
/** Parse and return the next command. */
- Command* nextCommand() throw(ParserException, UnsafeInterruptException);
+ Command* nextCommand();
/** Parse and return the next expression. */
- Expr nextExpression() throw(ParserException, UnsafeInterruptException);
+ Expr nextExpression();
/** Issue a warning to the user. */
- inline void warning(const std::string& msg) {
- d_input->warning(msg);
- }
-
+ void warning(const std::string& msg) { d_input->warning(msg); }
/** Issue a warning to the user, but only once per attribute. */
void attributeNotSupported(const std::string& attr);
/** Raise a parse error with the given message. */
- inline void parseError(const std::string& msg) throw(ParserException) {
- d_input->parseError(msg);
- }
-
+ inline void parseError(const std::string& msg) { d_input->parseError(msg); }
/** Unexpectedly encountered an EOF */
- inline void unexpectedEOF(const std::string& msg) throw(ParserException) {
+ inline void unexpectedEOF(const std::string& msg)
+ {
d_input->parseError(msg, true);
}
* support parsing quantifiers (just not doing anything with them).
* So this mechanism gives you a way to do it with --parse-only.
*/
- inline void unimplementedFeature(const std::string& msg) throw(ParserException) {
+ inline void unimplementedFeature(const std::string& msg)
+ {
if(!d_parseOnly) {
parseError("Unimplemented feature: " + msg);
}
}
Parser* ParserBuilder::build()
- throw (InputStreamException) {
+{
Input* input = NULL;
switch( d_inputType ) {
case FILE_INPUT:
const Options& options);
/** Build the parser, using the current settings. */
- Parser *build() throw (InputStreamException);
+ Parser* build();
/** Should semantic checks be enabled in the parser? (Default: yes) */
ParserBuilder& withChecks(bool flag = true);
virtual ~Smt1Input();
/** Get the language that this Input is reading. */
- InputLanguage getLanguage() const throw() {
+ InputLanguage getLanguage() const override
+ {
return language::input::LANG_SMTLIB_V1;
}
-protected:
-
+ protected:
/**
* Parse a command from the input. Returns <code>NULL</code> if
* there is no command there to parse.
*
* @throws ParserException if an error is encountered during parsing.
*/
- Command* parseCommand();
+ Command* parseCommand() override;
/**
* Parse an expression from the input. Returns a null
*/
Expr parseExpr();
-private:
-
+ private:
/**
* Initialize the class. Called from the constructors once the input
* stream is initialized.
* Smt2 parser provides its own checkDeclaration, which does the
* same as the base, but with some more helpful errors.
*/
- void checkDeclaration(const std::string& name, DeclarationCheck check,
+ void checkDeclaration(const std::string& name,
+ DeclarationCheck check,
SymbolType type = SYM_VARIABLE,
- std::string notes = "") throw(ParserException) {
+ std::string notes = "")
+ {
// if the symbol is something like "-1", we'll give the user a helpful
// syntax hint. (-1 is a valid identifier in SMT-LIB, NOT unary minus.)
if( check != CHECK_DECLARED ||
this->Parser::checkDeclaration(name, check, type, ss.str());
}
- void checkOperator(Kind kind, unsigned numArgs) throw(ParserException) {
+ void checkOperator(Kind kind, unsigned numArgs)
+ {
Parser::checkOperator(kind, numArgs);
// strict SMT-LIB mode enables extra checks for some bitvector operators
// that CVC4 permits as N-ary but the standard requires is binary
}
// Throw a ParserException with msg appended with the current logic.
- inline void parseErrorLogic(const std::string& msg) throw(ParserException) {
+ inline void parseErrorLogic(const std::string& msg)
+ {
const std::string withLogic = msg + getLogic().getLogicString();
parseError(withLogic);
}
*/
void init();
-public:
-
+ public:
/**
* Create an input.
*
virtual ~Smt2Input();
/** Get the language that this Input is reading. */
- InputLanguage getLanguage() const throw() {
- return d_lang;
- }
-
+ InputLanguage getLanguage() const override { return d_lang; }
/** Set the language that this Input is reading. */
void setLanguage(InputLanguage);
-protected:
-
+ protected:
/**
* Parse a command from the input. Returns <code>NULL</code> if
* there is no command there to parse.
*
* @throws ParserException if an error is encountered during parsing.
*/
- Command* parseCommand();
+ Command* parseCommand() override;
/**
* Parse an expression from the input. Returns a null
*/
void init();
-public:
-
+ public:
/**
* Create an input.
*
virtual ~SygusInput();
/** Get the language that this Input is reading. */
- InputLanguage getLanguage() const throw() {
+ InputLanguage getLanguage() const override
+ {
return language::input::LANG_SYGUS;
}
-protected:
-
+ protected:
/**
* Parse a command from the input. Returns <code>NULL</code> if
* there is no command there to parse.
*
* @throws ParserException if an error is encountered during parsing.
*/
- Command* parseCommand();
+ Command* parseCommand() override;
/**
* Parse an expression from the input. Returns a null
*/
void init();
-public:
-
+ public:
/**
* Create an input.
*
virtual ~TptpInput();
/** Get the language that this Input is reading. */
- InputLanguage getLanguage() const throw() {
+ InputLanguage getLanguage() const override
+ {
return language::input::LANG_TPTP;
}
-protected:
-
+ protected:
/**
* Parse a command from the input. Returns <code>NULL</code> if
* there is no command there to parse.
*
* @throws ParserException if an error is encountered during parsing.
*/
- Command* parseCommand();
+ Command* parseCommand() override;
/**
* Parse an expression from the input. Returns a null
projects / cvc5.git / commitdiff