summaryrefslogtreecommitdiff
path: root/src/parser/smt2/smt2.h
diff options
context:
space:
mode:
Diffstat (limited to 'src/parser/smt2/smt2.h')
-rw-r--r--src/parser/smt2/smt2.h14
1 files changed, 6 insertions, 8 deletions
diff --git a/src/parser/smt2/smt2.h b/src/parser/smt2/smt2.h
index e9e36e78c..09f7a5696 100644
--- a/src/parser/smt2/smt2.h
+++ b/src/parser/smt2/smt2.h
@@ -153,7 +153,7 @@ public:
const LogicInfo& getLogic() const { return d_logic; }
bool v2_0() const {
- return getInput()->getLanguage() == language::input::LANG_SMTLIB_V2_0;
+ return getLanguage() == language::input::LANG_SMTLIB_V2_0;
}
/**
* Are we using smtlib 2.5 or above? If exact=true, then this method returns
@@ -161,7 +161,7 @@ public:
*/
bool v2_5(bool exact = false) const
{
- return language::isInputLang_smt2_5(getInput()->getLanguage(), exact);
+ return language::isInputLang_smt2_5(getLanguage(), exact);
}
/**
* Are we using smtlib 2.6 or above? If exact=true, then this method returns
@@ -169,13 +169,9 @@ public:
*/
bool v2_6(bool exact = false) const
{
- return language::isInputLang_smt2_6(getInput()->getLanguage(), exact);
+ return language::isInputLang_smt2_6(getLanguage(), exact);
}
- bool sygus() const {
- return getInput()->getLanguage() == language::input::LANG_SYGUS;
- }
-
- void setLanguage(InputLanguage lang);
+ bool sygus() const { return getLanguage() == language::input::LANG_SYGUS; }
void setInfo(const std::string& flag, const SExpr& sexpr);
@@ -396,6 +392,8 @@ private:
void addFloatingPointOperators();
void addSepOperators();
+
+ InputLanguage getLanguage() const;
};/* class Smt2 */
}/* CVC4::parser namespace */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback