summaryrefslogtreecommitdiff
path: root/src/parser
diff options
context:
space:
mode:
Diffstat (limited to 'src/parser')
-rw-r--r--src/parser/antlr_input.cpp9
-rw-r--r--src/parser/antlr_input.h9
-rw-r--r--src/parser/bounded_token_buffer.cpp2
-rw-r--r--src/parser/cvc/Cvc.g6
-rw-r--r--src/parser/cvc/cvc_input.cpp6
-rw-r--r--src/parser/cvc/cvc_input.h6
-rw-r--r--src/parser/input.h6
-rw-r--r--src/parser/memory_mapped_input_buffer.cpp17
-rw-r--r--src/parser/parser.cpp16
-rw-r--r--src/parser/smt1/Smt1.g107
-rw-r--r--src/parser/smt1/smt1_input.cpp6
-rw-r--r--src/parser/smt1/smt1_input.h6
-rw-r--r--src/parser/smt2/Smt2.g6
-rw-r--r--src/parser/smt2/smt2_input.cpp6
-rw-r--r--src/parser/smt2/smt2_input.h8
-rw-r--r--src/parser/tptp/Tptp.g6
-rw-r--r--src/parser/tptp/tptp.cpp2
-rw-r--r--src/parser/tptp/tptp_input.cpp6
-rw-r--r--src/parser/tptp/tptp_input.h6
19 files changed, 138 insertions, 98 deletions
diff --git a/src/parser/antlr_input.cpp b/src/parser/antlr_input.cpp
index 8987a7572..fbf2b8650 100644
--- a/src/parser/antlr_input.cpp
+++ b/src/parser/antlr_input.cpp
@@ -63,8 +63,13 @@ AntlrInputStream*
AntlrInputStream::newFileInputStream(const std::string& name,
bool useMmap)
throw (InputStreamException) {
+#ifdef _WIN32
+ if(useMmap) {
+ useMmap = false;
+ }
+#endif
pANTLR3_INPUT_STREAM input = NULL;
- if( useMmap ) {
+ if(useMmap) {
input = MemoryMappedInputBufferNew(name);
} else {
// libantlr3c v3.2 isn't source-compatible with v3.4
@@ -74,7 +79,7 @@ AntlrInputStream::newFileInputStream(const std::string& name,
input = antlr3FileStreamNew((pANTLR3_UINT8) name.c_str(), ANTLR3_ENC_8BIT);
#endif /* CVC4_ANTLR3_OLD_INPUT_STREAM */
}
- if( input == NULL ) {
+ if(input == NULL) {
throw InputStreamException("Couldn't open file: " + name);
}
return new AntlrInputStream( name, input );
diff --git a/src/parser/antlr_input.h b/src/parser/antlr_input.h
index 68a62274d..a2fe99f52 100644
--- a/src/parser/antlr_input.h
+++ b/src/parser/antlr_input.h
@@ -285,7 +285,14 @@ inline Rational AntlrInput::tokenToRational(pANTLR3_COMMON_TOKEN token) {
inline BitVector AntlrInput::tokenToBitvector(pANTLR3_COMMON_TOKEN number, pANTLR3_COMMON_TOKEN size) {
std::string number_str = tokenTextSubstr(number, 2);
- return BitVector(tokenToUnsigned(size), Integer(number_str));
+ unsigned sz = tokenToUnsigned(size);
+ Integer val(number_str);
+ if(val.modByPow2(sz) != val) {
+ std::stringstream ss;
+ ss << "Overflow in bitvector construction (specified bitvector size " << sz << " too small to hold value " << tokenText(number) << ")";
+ throw std::invalid_argument(ss.str());
+ }
+ return BitVector(sz, val);
}
}/* CVC4::parser namespace */
diff --git a/src/parser/bounded_token_buffer.cpp b/src/parser/bounded_token_buffer.cpp
index 904f9a7fa..6a6ae8609 100644
--- a/src/parser/bounded_token_buffer.cpp
+++ b/src/parser/bounded_token_buffer.cpp
@@ -512,7 +512,7 @@ static pANTLR3_COMMON_TOKEN nextToken(pBOUNDED_TOKEN_BUFFER buffer) {
}
-/// Return a string that represents the name assoicated with the input source
+/// Return a string that represents the name associated with the input source
///
/// /param[in] is The ANTLR3_INT_STREAM interface that is representing this token stream.
///
diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g
index 1af4799be..b8ec160e8 100644
--- a/src/parser/cvc/Cvc.g
+++ b/src/parser/cvc/Cvc.g
@@ -416,10 +416,8 @@ Expr addNots(ExprManager* em, size_t n, Expr e) {
@header {
/**
- ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys)
- ** Courant Institute of Mathematical Sciences
- ** New York University
+ ** This file is part of CVC4.
+ ** Copyright (c) 2009-2013 New York University and The University of Iowa
** See the file COPYING in the top-level source directory for licensing
** information.
**/
diff --git a/src/parser/cvc/cvc_input.cpp b/src/parser/cvc/cvc_input.cpp
index 52fadae66..8328306be 100644
--- a/src/parser/cvc/cvc_input.cpp
+++ b/src/parser/cvc/cvc_input.cpp
@@ -56,13 +56,11 @@ CvcInput::~CvcInput() {
d_pCvcParser->free(d_pCvcParser);
}
-Command* CvcInput::parseCommand()
- throw (ParserException, TypeCheckingException) {
+Command* CvcInput::parseCommand() {
return d_pCvcParser->parseCommand(d_pCvcParser);
}
-Expr CvcInput::parseExpr()
- throw (ParserException, TypeCheckingException) {
+Expr CvcInput::parseExpr() {
return d_pCvcParser->parseExpr(d_pCvcParser);
}
diff --git a/src/parser/cvc/cvc_input.h b/src/parser/cvc/cvc_input.h
index 398ac4bd0..973e1c173 100644
--- a/src/parser/cvc/cvc_input.h
+++ b/src/parser/cvc/cvc_input.h
@@ -63,16 +63,14 @@ protected:
*
* @throws ParserException if an error is encountered during parsing.
*/
- Command* parseCommand()
- throw(ParserException, TypeCheckingException);
+ Command* parseCommand();
/** Parse an expression from the input. Returns a null <code>Expr</code>
* if there is no expression there to parse.
*
* @throws ParserException if an error is encountered during parsing.
*/
- Expr parseExpr()
- throw(ParserException, TypeCheckingException);
+ Expr parseExpr();
private:
diff --git a/src/parser/input.h b/src/parser/input.h
index 0203ed806..f4b36469b 100644
--- a/src/parser/input.h
+++ b/src/parser/input.h
@@ -168,8 +168,7 @@ protected:
*
* @throws ParserException if an error is encountered during parsing.
*/
- virtual Command* parseCommand()
- throw (ParserException, TypeCheckingException) = 0;
+ virtual Command* parseCommand() = 0;
/**
* Issue a warning to the user, with source file, line, and column info.
@@ -188,8 +187,7 @@ protected:
*
* @throws ParserException if an error is encountered during parsing.
*/
- virtual Expr parseExpr()
- throw (ParserException, TypeCheckingException) = 0;
+ virtual Expr parseExpr() = 0;
/** Set the Parser object for this input. */
virtual void setParser(Parser& parser) = 0;
diff --git a/src/parser/memory_mapped_input_buffer.cpp b/src/parser/memory_mapped_input_buffer.cpp
index 9f72ac51c..f110b1145 100644
--- a/src/parser/memory_mapped_input_buffer.cpp
+++ b/src/parser/memory_mapped_input_buffer.cpp
@@ -18,10 +18,15 @@
#include <stdio.h>
#include <stdint.h>
+#include <antlr3input.h>
+
+#ifndef _WIN32
+
#include <cerrno>
#include <sys/mman.h>
#include <sys/stat.h>
-#include <antlr3input.h>
+
+#endif /* _WIN32 */
#include "parser/memory_mapped_input_buffer.h"
#include "util/exception.h"
@@ -31,6 +36,14 @@ namespace parser {
extern "C" {
+#ifdef _WIN32
+
+pANTLR3_INPUT_STREAM MemoryMappedInputBufferNew(const std::string& filename) {
+ return 0;
+}
+
+#else /* ! _WIN32 */
+
static ANTLR3_UINT32
MemoryMapFile(pANTLR3_INPUT_STREAM input, const std::string& filename);
@@ -112,6 +125,8 @@ void UnmapFile(pANTLR3_INPUT_STREAM input) {
input->close(input);
}
+#endif /* _WIN32 */
+
}/* extern "C" */
}/* CVC4::parser namespace */
diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp
index 65d46220b..8b77362b2 100644
--- a/src/parser/parser.cpp
+++ b/src/parser/parser.cpp
@@ -462,15 +462,9 @@ Command* Parser::nextCommand() throw(ParserException) {
} catch(ParserException& e) {
setDone();
throw;
- } catch(Exception& e) {
+ } catch(exception& e) {
setDone();
- stringstream ss;
- // set the language of the stream, otherwise if it contains
- // Exprs or Types it prints in the AST language
- OutputLanguage outlang =
- language::toOutputLanguage(d_input->getLanguage());
- ss << Expr::setlanguage(outlang) << e;
- parseError( ss.str() );
+ parseError(e.what());
}
}
}
@@ -490,11 +484,9 @@ Expr Parser::nextExpression() throw(ParserException) {
} catch(ParserException& e) {
setDone();
throw;
- } catch(Exception& e) {
+ } catch(exception& e) {
setDone();
- stringstream ss;
- ss << e;
- parseError( ss.str() );
+ parseError(e.what());
}
}
Debug("parser") << "nextExpression() => " << result << std::endl;
diff --git a/src/parser/smt1/Smt1.g b/src/parser/smt1/Smt1.g
index 6dade9530..f8331c899 100644
--- a/src/parser/smt1/Smt1.g
+++ b/src/parser/smt1/Smt1.g
@@ -31,10 +31,8 @@ options {
@header {
/**
- ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys)
- ** Courant Institute of Mathematical Sciences
- ** New York University
+ ** This file is part of CVC4.
+ ** Copyright (c) 2009-2013 New York University and The University of Iowa
** See the file COPYING in the top-level source directory for licensing
** information.
**/
@@ -235,10 +233,10 @@ annotatedFormula[CVC4::Expr& expr]
Expr op; /* Operator expression FIXME: move away kill it */
}
: /* a built-in operator application */
- LPAREN_TOK builtinOp[kind] annotatedFormulas[args,expr] RPAREN_TOK
+ LPAREN_TOK builtinOp[kind] annotatedFormulas[args,expr]
{ if((kind == CVC4::kind::AND || kind == CVC4::kind::OR) && args.size() == 1) {
/* Unary AND/OR can be replaced with the argument.
- It just so happens expr should already by the only argument. */
+ * It just so happens expr should already be the only argument. */
assert( expr == args[0] );
} else if( CVC4::kind::isAssociative(kind) &&
args.size() > EXPR_MANAGER->maxArity(kind) ) {
@@ -253,6 +251,7 @@ annotatedFormula[CVC4::Expr& expr]
expr = MK_EXPR(kind, args);
}
}
+ termAnnotation[expr]* RPAREN_TOK
| /* A quantifier */
LPAREN_TOK
@@ -261,12 +260,13 @@ annotatedFormula[CVC4::Expr& expr]
( LPAREN_TOK let_identifier[name,CHECK_NONE] t=sortSymbol RPAREN_TOK
{ args.push_back(PARSER_STATE->mkBoundVar(name, t)); }
)+
- annotatedFormula[expr] RPAREN_TOK
+ annotatedFormula[expr]
{ args2.push_back( MK_EXPR( kind::BOUND_VAR_LIST, args ) );
args2.push_back(expr);
expr = MK_EXPR(kind, args2);
- PARSER_STATE->popScope();
}
+ termAnnotation[expr]* RPAREN_TOK
+ { PARSER_STATE->popScope(); }
| /* A non-built-in function application */
@@ -275,9 +275,10 @@ annotatedFormula[CVC4::Expr& expr]
// { isFunction(LT(2)->getText()) }?
LPAREN_TOK
parameterizedOperator[op]
- annotatedFormulas[args,expr] RPAREN_TOK
+ annotatedFormulas[args,expr]
// TODO: check arity
{ expr = MK_EXPR(op,args); }
+ termAnnotation[expr]* RPAREN_TOK
| /* An ite expression */
LPAREN_TOK ITE_TOK
@@ -286,9 +287,9 @@ annotatedFormula[CVC4::Expr& expr]
annotatedFormula[expr]
{ args.push_back(expr); }
annotatedFormula[expr]
- { args.push_back(expr); }
- RPAREN_TOK
- { expr = MK_EXPR(CVC4::kind::ITE, args); }
+ { args.push_back(expr);
+ expr = MK_EXPR(CVC4::kind::ITE, args); }
+ termAnnotation[expr]* RPAREN_TOK
| /* a let/flet binding */
LPAREN_TOK
@@ -298,7 +299,7 @@ annotatedFormula[CVC4::Expr& expr]
{ PARSER_STATE->pushScope();
PARSER_STATE->defineVar(name,expr); }
annotatedFormula[expr]
- RPAREN_TOK
+ termAnnotation[expr]* RPAREN_TOK
{ PARSER_STATE->popScope(); }
/* constants */
@@ -310,7 +311,7 @@ annotatedFormula[CVC4::Expr& expr]
{ // FIXME: This doesn't work because an SMT rational is not a
// valid GMP rational string
expr = MK_CONST( AntlrInput::tokenToRational($RATIONAL_TOK) ); }
- | n = BITVECTOR_BV_CONST '[' size = NUMERAL_TOK ']'
+ | n = BITVECTOR_BV_CONST '[' size = NUMERAL_TOK ']'
{ expr = MK_CONST( AntlrInput::tokenToBitvector($n, $size) ); }
// NOTE: Theory constants go here
/* TODO: quantifiers, arithmetic constants */
@@ -320,7 +321,6 @@ annotatedFormula[CVC4::Expr& expr]
| let_identifier[name,CHECK_DECLARED]
| flet_identifier[name,CHECK_DECLARED] )
{ expr = PARSER_STATE->getVariable(name); }
-
;
/**
@@ -458,7 +458,7 @@ functionSymbol[CVC4::Expr& fun]
* Matches an attribute name from the input (:attribute_name).
*/
attribute[std::string& s]
- : ATTR_IDENTIFIER
+ : ATTR_IDENTIFIER
{ s = AntlrInput::tokenText($ATTR_IDENTIFIER); }
;
@@ -555,28 +555,56 @@ status[ CVC4::BenchmarkStatus& status ]
/**
* Matches an annotation, which is an attribute name, with an optional user
+ * value.
*/
annotation[CVC4::Command*& smt_command]
@init {
- std::string key;
+ std::string key, value;
smt_command = NULL;
+ std::vector<Expr> pats;
+ Expr pat;
}
- : attribute[key]
- ( USER_VALUE
- { std::string value = AntlrInput::tokenText($USER_VALUE);
- assert(*value.begin() == '{');
- assert(*value.rbegin() == '}');
- // trim whitespace
- value.erase(value.begin(), value.begin() + 1);
- value.erase(value.begin(), std::find_if(value.begin(), value.end(), std::not1(std::ptr_fun<int, int>(std::isspace))));
- value.erase(value.end() - 1);
- value.erase(std::find_if(value.rbegin(), value.rend(), std::not1(std::ptr_fun<int, int>(std::isspace))).base(), value.end());
- smt_command = new SetInfoCommand(key.c_str() + 1, value); }
- )?
- { if(smt_command == NULL) {
- smt_command = new EmptyCommand(std::string("annotation: ") + key);
+ : PATTERN_ANNOTATION_BEGIN
+ { PARSER_STATE->warning(":pat not supported here; ignored"); }
+ annotatedFormulas[pats,pat] '}'
+ | attribute[key]
+ ( userValue[value]
+ { smt_command = new SetInfoCommand(key.c_str() + 1, value); }
+ | { smt_command = new EmptyCommand(std::string("annotation: ") + key); }
+ )
+ ;
+
+/**
+ * Matches an annotation, which is an attribute name, with an optional user
+ * value.
+ */
+termAnnotation[CVC4::Expr& expr]
+@init {
+ std::string key, value;
+ std::vector<Expr> pats;
+ Expr pat;
+}
+ : PATTERN_ANNOTATION_BEGIN annotatedFormulas[pats,pat] '}'
+ { if(expr.getKind() == kind::FORALL || expr.getKind() == kind::EXISTS) {
+ pat = MK_EXPR(kind::INST_PATTERN, pats);
+ if(expr.getNumChildren() == 3) {
+ // we have other user patterns attached to the quantifier
+ // already; add this one to the existing list
+ pats = expr[2].getChildren();
+ pats.push_back(pat);
+ expr = MK_EXPR(expr.getKind(), expr[0], expr[1], MK_EXPR(kind::INST_PATTERN_LIST, pats));
+ } else {
+ // this is the only user pattern for the quantifier
+ expr = MK_EXPR(expr.getKind(), expr[0], expr[1], MK_EXPR(kind::INST_PATTERN_LIST, pat));
+ }
+ } else {
+ PARSER_STATE->warning(":pat only supported on quantifiers");
}
}
+ | ':pat'
+ { PARSER_STATE->warning("expected an instantiation pattern after :pat"); }
+ | attribute[key] userValue[value]?
+ { PARSER_STATE->attributeNotSupported(key); }
;
/**
@@ -752,6 +780,23 @@ FLET_IDENTIFIER
* only constraint imposed on a user-defined value is that it start
* with an open brace and end with closed brace.
*/
+userValue[std::string& s]
+ : USER_VALUE
+ { s = AntlrInput::tokenText($USER_VALUE);
+ assert(*s.begin() == '{');
+ assert(*s.rbegin() == '}');
+ // trim whitespace
+ s.erase(s.begin(), s.begin() + 1);
+ s.erase(s.begin(), std::find_if(s.begin(), s.end(), std::not1(std::ptr_fun<int, int>(std::isspace))));
+ s.erase(s.end() - 1);
+ s.erase(std::find_if(s.rbegin(), s.rend(), std::not1(std::ptr_fun<int, int>(std::isspace))).base(), s.end());
+ }
+ ;
+
+PATTERN_ANNOTATION_BEGIN
+ : ':pat' (' ' | '\t' | '\f' | '\r' | '\n')* '{'
+ ;
+
USER_VALUE
: '{' ('\\{' | '\\}' | ~('{' | '}'))* '}'
;
diff --git a/src/parser/smt1/smt1_input.cpp b/src/parser/smt1/smt1_input.cpp
index 156ca083f..2dae4ef66 100644
--- a/src/parser/smt1/smt1_input.cpp
+++ b/src/parser/smt1/smt1_input.cpp
@@ -57,13 +57,11 @@ Smt1Input::~Smt1Input() {
d_pSmt1Parser->free(d_pSmt1Parser);
}
-Command* Smt1Input::parseCommand()
- throw (ParserException, TypeCheckingException) {
+Command* Smt1Input::parseCommand() {
return d_pSmt1Parser->parseCommand(d_pSmt1Parser);
}
-Expr Smt1Input::parseExpr()
- throw (ParserException, TypeCheckingException) {
+Expr Smt1Input::parseExpr() {
return d_pSmt1Parser->parseExpr(d_pSmt1Parser);
}
diff --git a/src/parser/smt1/smt1_input.h b/src/parser/smt1/smt1_input.h
index ce5c8284c..11110e78a 100644
--- a/src/parser/smt1/smt1_input.h
+++ b/src/parser/smt1/smt1_input.h
@@ -66,8 +66,7 @@ protected:
*
* @throws ParserException if an error is encountered during parsing.
*/
- Command* parseCommand()
- throw(ParserException, TypeCheckingException);
+ Command* parseCommand();
/**
* Parse an expression from the input. Returns a null
@@ -75,8 +74,7 @@ protected:
*
* @throws ParserException if an error is encountered during parsing.
*/
- Expr parseExpr()
- throw(ParserException, TypeCheckingException);
+ Expr parseExpr();
private:
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index 648666091..1ee288aa4 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -31,10 +31,8 @@ options {
@header {
/**
- ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009-2012 The Analysis of Computer Systems Group (ACSys)
- ** Courant Institute of Mathematical Sciences
- ** New York University
+ ** This file is part of CVC4.
+ ** Copyright (c) 2009-2013 New York University and The University of Iowa
** See the file COPYING in the top-level source directory for licensing
** information.
**/
diff --git a/src/parser/smt2/smt2_input.cpp b/src/parser/smt2/smt2_input.cpp
index 2ed8d6966..9b423dcad 100644
--- a/src/parser/smt2/smt2_input.cpp
+++ b/src/parser/smt2/smt2_input.cpp
@@ -58,13 +58,11 @@ Smt2Input::~Smt2Input() {
d_pSmt2Parser->free(d_pSmt2Parser);
}
-Command* Smt2Input::parseCommand()
- throw (ParserException, TypeCheckingException) {
+Command* Smt2Input::parseCommand() {
return d_pSmt2Parser->parseCommand(d_pSmt2Parser);
}
-Expr Smt2Input::parseExpr()
- throw (ParserException, TypeCheckingException) {
+Expr Smt2Input::parseExpr() {
return d_pSmt2Parser->parseExpr(d_pSmt2Parser);
}
diff --git a/src/parser/smt2/smt2_input.h b/src/parser/smt2/smt2_input.h
index 62ed33632..9b271a2c0 100644
--- a/src/parser/smt2/smt2_input.h
+++ b/src/parser/smt2/smt2_input.h
@@ -41,7 +41,7 @@ class Smt2Input : public AntlrInput {
/** The ANTLR3 SMT2 lexer for the input. */
pSmt2Lexer d_pSmt2Lexer;
- /** The ANTLR3 CVC parser for the input. */
+ /** The ANTLR3 SMT2 parser for the input. */
pSmt2Parser d_pSmt2Parser;
/**
@@ -75,8 +75,7 @@ protected:
*
* @throws ParserException if an error is encountered during parsing.
*/
- Command* parseCommand()
- throw(ParserException, TypeCheckingException);
+ Command* parseCommand();
/**
* Parse an expression from the input. Returns a null
@@ -84,8 +83,7 @@ protected:
*
* @throws ParserException if an error is encountered during parsing.
*/
- Expr parseExpr()
- throw(ParserException, TypeCheckingException);
+ Expr parseExpr();
};/* class Smt2Input */
diff --git a/src/parser/tptp/Tptp.g b/src/parser/tptp/Tptp.g
index 2180255ca..ec6868c5b 100644
--- a/src/parser/tptp/Tptp.g
+++ b/src/parser/tptp/Tptp.g
@@ -32,10 +32,8 @@ options {
@header {
/**
- ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys)
- ** Courant Institute of Mathematical Sciences
- ** New York University
+ ** This file is part of CVC4.
+ ** Copyright (c) 2009-2013 New York University and The University of Iowa
** See the file COPYING in the top-level source directory for licensing
** information.
**/
diff --git a/src/parser/tptp/tptp.cpp b/src/parser/tptp/tptp.cpp
index 1e40ea63f..59b1d205b 100644
--- a/src/parser/tptp/tptp.cpp
+++ b/src/parser/tptp/tptp.cpp
@@ -151,7 +151,7 @@ void Tptp::includeFile(std::string fileName){
if( d_tptpDir.empty() ){
parseError("Couldn't open included file: " + fileName
- + " at " + currentDirFileName + " and the TPTP directory is not specified (environnement variable TPTP)");
+ + " at " + currentDirFileName + " and the TPTP directory is not specified (environment variable TPTP)");
};
std::string tptpDirFileName = d_tptpDir + fileName;
diff --git a/src/parser/tptp/tptp_input.cpp b/src/parser/tptp/tptp_input.cpp
index 40231853f..d52c7f597 100644
--- a/src/parser/tptp/tptp_input.cpp
+++ b/src/parser/tptp/tptp_input.cpp
@@ -58,13 +58,11 @@ TptpInput::~TptpInput() {
d_pTptpParser->free(d_pTptpParser);
}
-Command* TptpInput::parseCommand()
- throw (ParserException, TypeCheckingException) {
+Command* TptpInput::parseCommand() {
return d_pTptpParser->parseCommand(d_pTptpParser);
}
-Expr TptpInput::parseExpr()
- throw (ParserException, TypeCheckingException) {
+Expr TptpInput::parseExpr() {
return d_pTptpParser->parseExpr(d_pTptpParser);
}
diff --git a/src/parser/tptp/tptp_input.h b/src/parser/tptp/tptp_input.h
index da9c67e31..13aa358cd 100644
--- a/src/parser/tptp/tptp_input.h
+++ b/src/parser/tptp/tptp_input.h
@@ -75,8 +75,7 @@ protected:
*
* @throws ParserException if an error is encountered during parsing.
*/
- Command* parseCommand()
- throw(ParserException, TypeCheckingException);
+ Command* parseCommand();
/**
* Parse an expression from the input. Returns a null
@@ -84,8 +83,7 @@ protected:
*
* @throws ParserException if an error is encountered during parsing.
*/
- Expr parseExpr()
- throw(ParserException, TypeCheckingException);
+ Expr parseExpr();
};/* class TptpInput */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback