summaryrefslogtreecommitdiff
path: root/src/parser/smt/smt_input.h
diff options
context:
space:
mode:
Diffstat (limited to 'src/parser/smt/smt_input.h')
-rw-r--r--src/parser/smt/smt_input.h9
1 files changed, 7 insertions, 2 deletions
diff --git a/src/parser/smt/smt_input.h b/src/parser/smt/smt_input.h
index c5b147b71..0ab382c73 100644
--- a/src/parser/smt/smt_input.h
+++ b/src/parser/smt/smt_input.h
@@ -55,6 +55,11 @@ public:
/** Destructor. Frees the lexer and the parser. */
~SmtInput();
+ /** Get the language that this Input is reading. */
+ InputLanguage getLanguage() const throw() {
+ return language::input::LANG_SMTLIB;
+ }
+
protected:
/**
@@ -63,7 +68,7 @@ protected:
*
* @throws ParserException if an error is encountered during parsing.
*/
- Command* parseCommand()
+ Command* parseCommand()
throw(ParserException, TypeCheckingException, AssertionException);
/**
@@ -72,7 +77,7 @@ protected:
*
* @throws ParserException if an error is encountered during parsing.
*/
- Expr parseExpr()
+ Expr parseExpr()
throw(ParserException, TypeCheckingException, AssertionException);
private:
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback