diff options
Diffstat (limited to 'src/parser/smt2/smt2.cpp')
| -rw-r--r-- | src/parser/smt2/smt2.cpp | 14 |
1 files changed, 8 insertions, 6 deletions
diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index e0769f88a..cdb799864 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -15,8 +15,8 @@ **/ #include "parser/smt2/smt2.h" - #include "expr/type.h" +#include "options/options.h" #include "parser/antlr_input.h" #include "parser/parser.h" #include "parser/smt1/smt1.h" @@ -42,10 +42,6 @@ Smt2::Smt2(ExprManager* exprManager, Input* input, bool strictMode, bool parseOn } } -void Smt2::setLanguage(InputLanguage lang) { - ((Smt2Input*) getInput())->setLanguage(lang); -} - void Smt2::addArithmeticOperators() { Parser::addOperator(kind::PLUS); Parser::addOperator(kind::MINUS); @@ -130,7 +126,7 @@ void Smt2::addStringOperators() { addOperator(kind::STRING_PREFIX, "str.prefixof" ); addOperator(kind::STRING_SUFFIX, "str.suffixof" ); // at the moment, we only use this syntax for smt2.6.1 - if (getInput()->getLanguage() == language::input::LANG_SMTLIB_V2_6_1) + if (getLanguage() == language::input::LANG_SMTLIB_V2_6_1) { addOperator(kind::STRING_ITOS, "str.from-int"); addOperator(kind::STRING_STOI, "str.to-int"); @@ -1250,5 +1246,11 @@ const void Smt2::addSygusFunSymbol( Type t, Expr synth_fun ){ preemptCommand(cattr); } +InputLanguage Smt2::getLanguage() const +{ + ExprManager* em = getExprManager(); + return em->getOptions().getInputLanguage(); +} + }/* CVC4::parser namespace */ }/* CVC4 namespace */ |