void AntlrInput::setParser(pANTLR3_PARSER pParser) {
d_parser = pParser;
// ANTLR isn't using super, AFAICT.
+ // We could also use @parser::context to add a field to the generated parser, but then
+ // it would have to be declared separately in every input's grammar and we'd have to
+ // pass it in as an address anyway.
d_parser->super = this;
d_parser->rec->reportError = &reportError;
}
* Wrapper for an ANTLR parser that includes convenience methods to set up input and token streams.
*/
class AntlrInput : public Input {
-
+ /** The token lookahead used to lex and parse the input. This should usually be equal to
+ * <code>K</code> for an LL(k) grammar. */
unsigned int d_lookahead;
+
+ /** The ANTLR3 lexer associated with this input. This will be <code>NULL</code> initially. It
+ * must be set by a call to <code>setLexer</code>, preferably in the subclass constructor. */
pANTLR3_LEXER d_lexer;
+
+ /** The ANTLR3 parser associated with this input. This will be <code>NULL</code> initially. It
+ * must be set by a call to <code>setParser</code>, preferably in the subclass constructor.
+ * The <code>super</code> field of <code>d_parser</code> will be set to <code>this</code> and
+ * <code>reportError</code> will be set to <code>AntlrInput::reportError</code>. */
pANTLR3_PARSER d_parser;
+
+ /** The ANTLR3 token stream associated with this input. We only need this so we can free it on exit.
+ * This is set by <code>setLexer</code>.
+ * NOTE: We assume that we <em>can</em> free it on exit. No sharing! */
pANTLR3_COMMON_TOKEN_STREAM d_tokenStream;
+
+ /** The ANTLR3 token stream associated with this input. We only need this so we can free it on exit.
+ * NOTE: We assume that we <em>can</em> free it on exit. No sharing! */
pANTLR3_INPUT_STREAM d_input;
+ /** Turns an ANTLR3 exception into a message for the user and calls <code>parseError</code>. */
static void reportError(pANTLR3_BASE_RECOGNIZER recognizer);
public:
+
+ /** Create a file input.
+ *
+ * @param exprManager the manager to use when building expressions from the input
+ * @param filename the path of the file to read
+ * @param lookahead the lookahead needed to parse the input (i.e., k for an LL(k) grammar)
+ * @param useMmap <code>true</code> if the input should use memory-mapped I/O; otherwise, the
+ * input will use the standard ANTLR3 I/O implementation.
+ */
AntlrInput(ExprManager* exprManager, const std::string& filename, unsigned int lookahead, bool useMmap);
+
+ /** Create an input from an istream. */
// AntlrParser(ExprManager* em, std::istream& input, const std::string& name, unsigned int lookahead);
+
+ /** Create a string input.
+ *
+ * @param exprManager the manager to use when building expressions from the input
+ * @param input the string to read
+ * @param name the "filename" to use when reporting errors
+ * @param lookahead the lookahead needed to parse the input (i.e., k for an LL(k) grammar)
+ */
AntlrInput(ExprManager* exprManager, const std::string& input, const std::string& name, unsigned int lookahead);
+
+ /** Destructor. Frees the token stream and closes the input. */
~AntlrInput();
+ /** Retrieve the text associated with a token. */
inline static std::string tokenText(pANTLR3_COMMON_TOKEN token);
protected:
/**
- * Throws a semantic exception with the given message.
+ * Throws a <code>ParserException</code> with the given message.
*/
void parseError(const std::string& msg) throw (ParserException);
- /** Get the lexer */
- pANTLR3_LEXER getLexer();
/** Retrieve the input stream for this parser. */
pANTLR3_INPUT_STREAM getInputStream();
- /** Retrieve the token stream for this parser. Must not be called before <code>setLexer()</code>. */
+ /** Retrieve the token stream for this parser. Must not be called before
+ * <code>setLexer()</code>. */
pANTLR3_COMMON_TOKEN_STREAM getTokenStream();
+
/** Set the ANTLR lexer for this parser. */
void setLexer(pANTLR3_LEXER pLexer);
+
/** Set the ANTLR parser implementation for this parser. */
void setParser(pANTLR3_PARSER pParser);
};
std::string AntlrInput::tokenText(pANTLR3_COMMON_TOKEN token) {
ANTLR3_MARKER start = token->getStartIndex(token);
ANTLR3_MARKER end = token->getStopIndex(token);
+ /* start and end are boundary pointers. The text is a string
+ * of (end-start+1) bytes beginning at start. */
std::string txt( (const char *)start, end-start+1 );
Debug("parser-extra") << "tokenText: start=" << start << std::endl
<< "end=" << end << std::endl
}
@lexer::includes {
+/** This suppresses warnings about the redefinition of token symbols between different
+ * parsers. The redefinitions should be harmless as long as no client: (a) #include's
+ * the lexer headers for two grammars AND (b) uses the token symbol definitions. */
+#pragma GCC system_header
+
/* This improves performance by ~10 percent on big inputs.
* This option is only valid if we know the input is ASCII (or some 8-bit encoding).
* If we know the input is UTF-16, we can use ANTLR3_INLINE_INPUT_UTF16.
@parser::includes {
#include "expr/command.h"
-#include "parser/input.h"
namespace CVC4 {
class Expr;
-namespace parser {
- class CvcInput;
-}
}
-
-extern
-void SetCvcInput(CVC4::parser::CvcInput* input);
-
}
@parser::postinclude {
#include "expr/expr.h"
#include "expr/kind.h"
#include "expr/type.h"
-#include "parser/input.h"
#include "parser/cvc/cvc_input.h"
#include "util/output.h"
#include <vector>
using namespace CVC4;
using namespace CVC4::parser;
-}
-
-@members {
-static CVC4::parser::CvcInput *input;
-extern
-void SetCvcInput(CVC4::parser::CvcInput* _input) {
- input = _input;
-}
+#undef CVC_INPUT
+#define CVC_INPUT ((CvcInput*)(PARSER->super))
}
/**
: ASSERT_TOK formula[f] SEMICOLON { cmd = new AssertCommand(f); }
| QUERY_TOK formula[f] SEMICOLON { cmd = new QueryCommand(f); }
| CHECKSAT_TOK formula[f] SEMICOLON { cmd = new CheckSatCommand(f); }
- | CHECKSAT_TOK SEMICOLON { cmd = new CheckSatCommand(input->getTrueExpr()); }
+ | CHECKSAT_TOK SEMICOLON { cmd = new CheckSatCommand(CVC_INPUT->getTrueExpr()); }
| PUSH_TOK SEMICOLON { cmd = new PushCommand(); }
| POP_TOK SEMICOLON { cmd = new PopCommand(); }
| declaration[cmd]
Debug("parser-extra") << "declType: " << AntlrInput::tokenText(LT(1)) << std::endl;
}
: /* A sort declaration (e.g., "T : TYPE") */
- TYPE_TOK { input->newSorts(idList); t = input->kindType(); }
+ TYPE_TOK { CVC_INPUT->newSorts(idList); t = CVC_INPUT->kindType(); }
| /* A variable declaration */
- type[t] { input->mkVars(idList,t); }
+ type[t] { CVC_INPUT->mkVars(idList,t); }
;
/**
| /* Single-parameter function type */
baseType[t] { typeList.push_back(t); }
ARROW_TOK baseType[t]
- { t = input->functionType(typeList,t); }
+ { t = CVC_INPUT->functionType(typeList,t); }
| /* Multi-parameter function type */
LPAREN baseType[t]
{ typeList.push_back(t); }
(COMMA baseType[t] { typeList.push_back(t); } )+
RPAREN ARROW_TOK baseType[t]
- { t = input->functionType(typeList,t); }
+ { t = CVC_INPUT->functionType(typeList,t); }
;
/**
CVC4::parser::SymbolType type]
: IDENTIFIER
{ id = AntlrInput::tokenText($IDENTIFIER);
- input->checkDeclaration(id, check, type); }
+ CVC_INPUT->checkDeclaration(id, check, type); }
;
/**
std::string id;
Debug("parser-extra") << "base type: " << AntlrInput::tokenText(LT(1)) << std::endl;
}
- : BOOLEAN_TOK { t = input->booleanType(); }
+ : BOOLEAN_TOK { t = CVC_INPUT->booleanType(); }
| typeSymbol[t]
;
Debug("parser-extra") << "type symbol: " << AntlrInput::tokenText(LT(1)) << std::endl;
}
: identifier[id,CHECK_DECLARED,SYM_SORT]
- { t = input->getSort(id); }
+ { t = CVC_INPUT->getSort(id); }
;
/**
: impliesFormula[f]
( IFF_TOK
iffFormula[e]
- { f = input->mkExpr(CVC4::kind::IFF, f, e); }
+ { f = CVC_INPUT->mkExpr(CVC4::kind::IFF, f, e); }
)?
;
}
: orFormula[f]
( IMPLIES_TOK impliesFormula[e]
- { f = input->mkExpr(CVC4::kind::IMPLIES, f, e); }
+ { f = CVC_INPUT->mkExpr(CVC4::kind::IMPLIES, f, e); }
)?
;
xorFormula[f] { exprs.push_back(f); } )*
{
if( exprs.size() > 0 ) {
- f = input->mkExpr(CVC4::kind::OR, exprs);
+ f = CVC_INPUT->mkExpr(CVC4::kind::OR, exprs);
}
}
;
}
: andFormula[f]
( XOR_TOK andFormula[e]
- { f = input->mkExpr(CVC4::kind::XOR,f, e); }
+ { f = CVC_INPUT->mkExpr(CVC4::kind::XOR,f, e); }
)*
;
notFormula[f] { exprs.push_back(f); } )*
{
if( exprs.size() > 0 ) {
- f = input->mkExpr(CVC4::kind::AND, exprs);
+ f = CVC_INPUT->mkExpr(CVC4::kind::AND, exprs);
}
}
;
}
: /* negation */
NOT_TOK notFormula[f]
- { f = input->mkExpr(CVC4::kind::NOT, f); }
+ { f = CVC_INPUT->mkExpr(CVC4::kind::NOT, f); }
| /* a boolean atom */
predFormula[f]
;
}
: term[f]
(EQUAL_TOK term[e]
- { f = input->mkExpr(CVC4::kind::EQUAL, f, e); }
+ { f = CVC_INPUT->mkExpr(CVC4::kind::EQUAL, f, e); }
)?
; // TODO: lt, gt, etc.
{ args.push_back( f ); }
LPAREN formulaList[args] RPAREN
// TODO: check arity
- { f = input->mkExpr(CVC4::kind::APPLY_UF, args); }
+ { f = CVC_INPUT->mkExpr(CVC4::kind::APPLY_UF, args); }
| /* if-then-else */
iteTerm[f]
LPAREN formula[f] RPAREN
/* constants */
- | TRUE_TOK { f = input->getTrueExpr(); }
- | FALSE_TOK { f = input->getFalseExpr(); }
+ | TRUE_TOK { f = CVC_INPUT->getTrueExpr(); }
+ | FALSE_TOK { f = CVC_INPUT->getFalseExpr(); }
| /* variable */
identifier[name,CHECK_DECLARED,SYM_VARIABLE]
- { f = input->getVariable(name); }
+ { f = CVC_INPUT->getVariable(name); }
;
/**
THEN_TOK formula[f] { args.push_back(f); }
iteElseTerm[f] { args.push_back(f); }
ENDIF_TOK
- { f = input->mkExpr(CVC4::kind::ITE, args); }
+ { f = CVC_INPUT->mkExpr(CVC4::kind::ITE, args); }
;
/**
| ELSEIF_TOK iteCondition = formula[f] { args.push_back(f); }
THEN_TOK iteThen = formula[f] { args.push_back(f); }
iteElse = iteElseTerm[f] { args.push_back(f); }
- { f = input->mkExpr(CVC4::kind::ITE, args); }
+ { f = CVC_INPUT->mkExpr(CVC4::kind::ITE, args); }
;
/**
std::string name;
}
: identifier[name,CHECK_DECLARED,SYM_FUNCTION]
- { input->checkFunction(name);
- f = input->getFunction(name); }
+ { CVC_INPUT->checkFunction(name);
+ f = CVC_INPUT->getFunction(name); }
;
}
setParser(d_pCvcParser->pParser);
- SetCvcInput(this);
}
return d_pCvcParser->parseExpr(d_pCvcParser);
}
+/*
pANTLR3_LEXER CvcInput::getLexer() {
return d_pCvcLexer->pLexer;
}
+*/
} // namespace parser
namespace parser {
class CvcInput : public AntlrInput {
+ /** The ANTLR3 CVC lexer for the input. */
+ pCvcLexer d_pCvcLexer;
+
+ /** The ANTLR3 CVC parser for the input. */
+ pCvcParser d_pCvcParser;
+
public:
+
+ /** Create a file input.
+ *
+ * @param exprManager the manager to use when building expressions from the input
+ * @param filename the path of the file to read
+ * @param useMmap <code>true</code> if the input should use memory-mapped
+ * I/O; otherwise, the input will use the standard ANTLR3 I/O implementation.
+ */
CvcInput(ExprManager* exprManager, const std::string& filename, bool useMmap);
- CvcInput(ExprManager* exprManager, const std::string& input, const std::string& name);
+
+ /** Create a string input.
+ *
+ * @param exprManager the manager to use when building expressions from the input
+ * @param input the string to read
+ * @param name the "filename" to use when reporting errors
+ */
+ CvcInput(ExprManager* exprManager, const std::string& input,
+ const std::string& name);
+
+ /* Destructor. Frees the lexer and the parser. */
~CvcInput();
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* doParseCommand() throw(ParserException);
+
+ /** 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 doParseExpr() throw(ParserException);
- pANTLR3_LEXER getLexer();
- pANTLR3_LEXER createLexer(pANTLR3_INPUT_STREAM input);
- pANTLR3_PARSER createParser(pANTLR3_COMMON_TOKEN_STREAM tokenStream);
private:
+
+ /** Initialize the class. Called from the constructors once the input stream
+ * is initialized. */
void init();
- pCvcLexer d_pCvcLexer;
- pCvcParser d_pCvcParser;
+
}; // class CvcInput
} // namespace parser
*/
class CVC4_PUBLIC Input {
+ /** Whether to de-allocate the input */
+// bool d_deleteInput;
+
+ /** The expression manager */
+ ExprManager* d_exprManager;
+
+ /** The symbol table lookup */
+ SymbolTable<Expr> d_varSymbolTable;
+
+ /** The sort table */
+ SymbolTable<Type*> d_sortTable;
+
+ /** The name of the input file. */
+ std::string d_filename;
+
+ /** Are we done */
+ bool d_done;
+
+ /** Are semantic checks enabled during parsing? */
+ bool d_checksEnabled;
+
public:
+
+ /**
+ * Create a new parser for the given file.
+ * @param exprManager the ExprManager to use
+ * @param filename the path of the file to parse
+ */
+ Input(ExprManager* exprManager, const std::string& filename);
+
+ /**
+ * Destructor.
+ */
+ ~Input();
+
/** Create a parser for the given file.
*
* @param exprManager the ExprManager for creating expressions from the input
*/
static Input* newStringParser(ExprManager* exprManager, InputLanguage lang, const std::string& input, const std::string& name);
- /**
- * Destructor.
- */
- ~Input();
-
/**
* Parse the next command of the input. If EOF is encountered a EmptyCommand
* is returned and done flag is set.
+ *
+ * @throws ParserException if an error is encountered during parsing.
*/
Command* parseNextCommand() throw(ParserException);
* Parse the next expression of the stream. If EOF is encountered a null
* expression is returned and done flag is set.
* @return the parsed expression
+ * @throws ParserException if an error is encountered during parsing.
*/
Expr parseNextExpression() throw(ParserException);
/** Returns the maximum arity of the given kind. */
static unsigned int maxArity(Kind kind);
+ /** Throws a <code>ParserException</code> with the given error message.
+ * Implementations should fill in the <code>ParserException</code> with
+ * line number information, etc. */
virtual void parseError(const std::string& msg) throw (ParserException) = 0;
protected:
- virtual Command* doParseCommand() throw(ParserException) = 0;
- virtual Expr doParseExpr() throw(ParserException) = 0;
- /**
- * Create a new parser for the given file.
- * @param exprManager the ExprManager to use
- * @param filename the path of the file to parse
- */
- Input(ExprManager* exprManager, const std::string& filename);
+ /** Called by <code>parseNextCommand</code> to actually parse a command from
+ * the input by invoking the implementation-specific parsing method. Returns
+ * <code>NULL</code> if there is no command there to parse.
+ *
+ * @throws ParserException if an error is encountered during parsing.
+ */
+ virtual Command* doParseCommand() throw(ParserException) = 0;
+
+ /** Called by <code>parseNextExpression</code> to actually parse an
+ * expression from the input by invoking the implementation-specific
+ * parsing method. Returns a null <code>Expr</code> if there is no
+ * expression there to parse.
+ *
+ * @throws ParserException if an error is encountered during parsing.
+ */
+ virtual Expr doParseExpr() throw(ParserException) = 0;
private:
/** Lookup a symbol in the given namespace. */
Expr getSymbol(const std::string& var_name, SymbolType type);
- /** Whether to de-allocate the input */
-// bool d_deleteInput;
-
- /** The expression manager */
- ExprManager* d_exprManager;
-
- /** The symbol table lookup */
- SymbolTable<Expr> d_varSymbolTable;
-
- /** The sort table */
- SymbolTable<Type*> d_sortTable;
-
- /** The name of the input file. */
- std::string d_filename;
-
- /** Are we done */
- bool d_done;
-
- /** Are semantic checks enabled during parsing? */
- bool d_checksEnabled;
-
}; // end of class Parser
}/* CVC4::parser namespace */
}
@lexer::includes {
+/** This suppresses warnings about the redefinition of token symbols between different
+ * parsers. The redefinitions should be harmless as long as no client: (a) #include's
+ * the lexer headers for two grammars AND (b) uses the token symbol definitions. */
+#pragma GCC system_header
+
/* This improves performance by ~10 percent on big inputs.
* This option is only valid if we know the input is ASCII (or some 8-bit encoding).
* If we know the input is UTF-16, we can use ANTLR3_INLINE_INPUT_UTF16.
@parser::includes {
#include "expr/command.h"
-#include "parser/input.h"
namespace CVC4 {
class Expr;
-namespace parser {
- class SmtInput;
-}
}
-
-extern
-void SetSmtInput(CVC4::parser::SmtInput* smt);
-
}
@parser::postinclude {
#include "expr/expr.h"
#include "expr/kind.h"
#include "expr/type.h"
-#include "parser/input.h"
#include "parser/smt/smt_input.h"
#include "util/output.h"
#include <vector>
using namespace CVC4;
using namespace CVC4::parser;
-}
-
-@members {
-static CVC4::parser::SmtInput *input;
-extern
-void SetSmtInput(CVC4::parser::SmtInput* _input) {
- input = _input;
-}
+#undef SMT_INPUT
+#define SMT_INPUT ((SmtInput*)(PARSER->super))
}
/**
Expr expr;
}
: LOGIC_TOK identifier[name,CHECK_NONE,SYM_VARIABLE]
- { input->setLogic(name);
+ { SMT_INPUT->setLogic(name);
smt_command = new SetBenchmarkLogicCommand(name); }
| ASSUMPTION_TOK annotatedFormula[expr]
{ smt_command = new AssertCommand(expr); }
}
: /* a built-in operator application */
LPAREN_TOK builtinOp[kind] annotatedFormulas[args,expr] RPAREN_TOK
- { input->checkArity(kind, args.size());
+ { SMT_INPUT->checkArity(kind, args.size());
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. */
Assert( expr == args[0] );
} else {
- expr = input->mkExpr(kind, args);
+ expr = SMT_INPUT->mkExpr(kind, args);
}
}
{ args.push_back(expr); }
annotatedFormulas[args,expr] RPAREN_TOK
// TODO: check arity
- { expr = input->mkExpr(CVC4::kind::APPLY_UF,args); }
+ { expr = SMT_INPUT->mkExpr(CVC4::kind::APPLY_UF,args); }
| /* An ite expression */
LPAREN_TOK (ITE_TOK | IF_THEN_ELSE_TOK)
annotatedFormula[expr]
{ args.push_back(expr); }
RPAREN_TOK
- { expr = input->mkExpr(CVC4::kind::ITE, args); }
+ { expr = SMT_INPUT->mkExpr(CVC4::kind::ITE, args); }
| /* a let/flet binding */
LPAREN_TOK
(LET_TOK LPAREN_TOK var_identifier[name,CHECK_UNDECLARED]
| FLET_TOK LPAREN_TOK fun_identifier[name,CHECK_UNDECLARED] )
annotatedFormula[expr] RPAREN_TOK
- { input->defineVar(name,expr); }
+ { SMT_INPUT->defineVar(name,expr); }
annotatedFormula[expr]
RPAREN_TOK
- { input->undefineVar(name); }
+ { SMT_INPUT->undefineVar(name); }
| /* a variable */
( identifier[name,CHECK_DECLARED,SYM_VARIABLE]
| var_identifier[name,CHECK_DECLARED]
| fun_identifier[name,CHECK_DECLARED] )
- { expr = input->getVariable(name); }
+ { expr = SMT_INPUT->getVariable(name); }
/* constants */
- | TRUE_TOK { expr = input->getTrueExpr(); }
- | FALSE_TOK { expr = input->getFalseExpr(); }
+ | TRUE_TOK { expr = SMT_INPUT->getTrueExpr(); }
+ | FALSE_TOK { expr = SMT_INPUT->getFalseExpr(); }
/* TODO: let, flet, quantifiers, arithmetic constants */
;
std::string name;
}
: functionName[name,CHECK_DECLARED]
- { input->checkFunction(name);
- fun = input->getFunction(name); }
+ { SMT_INPUT->checkFunction(name);
+ fun = SMT_INPUT->getFunction(name); }
;
/**
t = sortSymbol // require at least one sort
{ sorts.push_back(t); }
sortList[sorts] RPAREN_TOK
- { t = input->functionType(sorts);
- input->mkVar(name, t); }
+ { t = SMT_INPUT->functionType(sorts);
+ SMT_INPUT->mkVar(name, t); }
;
/**
std::vector<Type*> p_sorts;
}
: LPAREN_TOK predicateName[name,CHECK_UNDECLARED] sortList[p_sorts] RPAREN_TOK
- { Type *t = input->predicateType(p_sorts);
- input->mkVar(name, t); }
+ { Type *t = SMT_INPUT->predicateType(p_sorts);
+ SMT_INPUT->mkVar(name, t); }
;
sortDeclaration
}
: sortName[name,CHECK_UNDECLARED]
{ Debug("parser") << "sort decl: '" << name << "'" << std::endl;
- input->newSort(name); }
+ SMT_INPUT->newSort(name); }
;
/**
std::string name;
}
: sortName[name,CHECK_NONE]
- { $t = input->getSort(name); }
+ { $t = SMT_INPUT->getSort(name); }
;
/**
Debug("parser") << "identifier: " << id
<< " check? " << toString(check)
<< " type? " << toString(type) << std::endl;
- input->checkDeclaration(id, check, type); }
+ SMT_INPUT->checkDeclaration(id, check, type); }
;
/**
{ id = AntlrInput::tokenText($VAR_IDENTIFIER);
Debug("parser") << "var_identifier: " << id
<< " check? " << toString(check) << std::endl;
- input->checkDeclaration(id, check, SYM_VARIABLE); }
+ SMT_INPUT->checkDeclaration(id, check, SYM_VARIABLE); }
;
/**
{ id = AntlrInput::tokenText($FUN_IDENTIFIER);
Debug("parser") << "fun_identifier: " << id
<< " check? " << toString(check) << std::endl;
- input->checkDeclaration(id, check, SYM_FUNCTION); }
+ SMT_INPUT->checkDeclaration(id, check, SYM_FUNCTION); }
;
namespace parser {
/* Use lookahead=2 */
-SmtInput::SmtInput(ExprManager* exprManager, const std::string& filename, bool useMmap) :
- AntlrInput(exprManager,filename,2,useMmap) {
+SmtInput::SmtInput(ExprManager* exprManager, const std::string& filename,
+ bool useMmap) :
+ AntlrInput(exprManager, filename, 2, useMmap) {
init();
}
-SmtInput::SmtInput(ExprManager* exprManager, const std::string& input, const std::string& name) :
- AntlrInput(exprManager,input,name,2) {
+SmtInput::SmtInput(ExprManager* exprManager, const std::string& input,
+ const std::string& name) :
+ AntlrInput(exprManager, input, name, 2) {
init();
}
}
setParser(d_pSmtParser->pParser);
- SetSmtInput(this);
}
return d_pSmtParser->parseExpr(d_pSmtParser);
}
-pANTLR3_LEXER SmtInput::getLexer() {
- return d_pSmtLexer->pLexer;
-}
-
} // namespace parser
} // namespace CVC4
namespace parser {
class SmtInput : public AntlrInput {
+
+ /** The ANTLR3 SMT lexer for the input. */
+ pSmtLexer d_pSmtLexer;
+
+ /** The ANTLR3 CVC parser for the input. */
+ pSmtParser d_pSmtParser;
+
public:
+
+ /** Create a file input.
+ *
+ * @param exprManager the manager to use when building expressions from the input
+ * @param filename the path of the file to read
+ * @param useMmap <code>true</code> if the input should use memory-mapped
+ * I/O; otherwise, the input will use the standard ANTLR3 I/O implementation.
+ */
SmtInput(ExprManager* exprManager, const std::string& filename, bool useMmap);
+
+ /** Create a string input.
+ *
+ * @param exprManager the manager to use when building expressions from the input
+ * @param input the string to read
+ * @param name the "filename" to use when reporting errors
+ */
SmtInput(ExprManager* exprManager, const std::string& input, const std::string& name);
+
+ /* Destructor. Frees the lexer and the parser. */
~SmtInput();
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* doParseCommand() throw(ParserException);
+
+ /** 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 doParseExpr() throw(ParserException);
- pANTLR3_LEXER getLexer();
- pANTLR3_LEXER createLexer(pANTLR3_INPUT_STREAM input);
- pANTLR3_PARSER createParser(pANTLR3_COMMON_TOKEN_STREAM tokenStream);
private:
+
+ /** Initialize the class. Called from the constructors once the input stream
+ * is initialized. */
void init();
- pSmtLexer d_pSmtLexer;
- pSmtParser d_pSmtParser;
+
}; // class SmtInput
+
} // namespace parser
} // namespace CVC4
projects / cvc5.git / commitdiff