diff options
| author | Andres Noetzli <andres.noetzli@gmail.com> | 2018-05-29 05:43:20 -0700 |
|---|---|---|
| committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-05-29 07:43:20 -0500 |
| commit | 6059866b361d0852d0b70d484b0cb397f3cc5bf4 (patch) | |
| tree | a06379fe4b368addd94db16261b4ff6004e3b482 /src/parser/smt2/smt2.cpp | |
| parent | 74c1ad7e4a8e93316b7555ac8a1b88ee777335e2 (diff) | |
Track input language in a single place (#2003)
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 */ |