summaryrefslogtreecommitdiff
path: root/src/parser/smt2/smt2.h
diff options
context:
space:
mode:
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>2018-05-02 20:25:09 -0500
committerAndres Noetzli <andres.noetzli@gmail.com>2018-05-02 18:25:09 -0700
commit716ce9168d846ea991f8404a78aeb1ccccfbce14 (patch)
tree5a617909b7d82ed2265693461f4f9f0a4c811f56 /src/parser/smt2/smt2.h
parentd3f4ac852146c41341e485d9035f3631993e3fa5 (diff)
Initial support for string standard in smt lib 2.6 (#1848)
Diffstat (limited to 'src/parser/smt2/smt2.h')
-rw-r--r--src/parser/smt2/smt2.h21
1 files changed, 14 insertions, 7 deletions
diff --git a/src/parser/smt2/smt2.h b/src/parser/smt2/smt2.h
index 71aa32492..e9e36e78c 100644
--- a/src/parser/smt2/smt2.h
+++ b/src/parser/smt2/smt2.h
@@ -155,14 +155,21 @@ public:
bool v2_0() const {
return getInput()->getLanguage() == language::input::LANG_SMTLIB_V2_0;
}
- // 2.6 is a superset of 2.5, use exact=false to query whether smt lib 2.5 or above
- bool v2_5( bool exact = true ) const {
- return exact ? getInput()->getLanguage() == language::input::LANG_SMTLIB_V2_5 :
- ( getInput()->getLanguage() >= language::input::LANG_SMTLIB_V2_5 &&
- getInput()->getLanguage() <= language::input::LANG_SMTLIB_V2 );
+ /**
+ * Are we using smtlib 2.5 or above? If exact=true, then this method returns
+ * false if the input language is not exactly SMT-LIB 2.5.
+ */
+ bool v2_5(bool exact = false) const
+ {
+ return language::isInputLang_smt2_5(getInput()->getLanguage(), exact);
}
- bool v2_6() const {
- return getInput()->getLanguage() == language::input::LANG_SMTLIB_V2_6;
+ /**
+ * Are we using smtlib 2.6 or above? If exact=true, then this method returns
+ * false if the input language is not exactly SMT-LIB 2.6.
+ */
+ bool v2_6(bool exact = false) const
+ {
+ return language::isInputLang_smt2_6(getInput()->getLanguage(), exact);
}
bool sygus() const {
return getInput()->getLanguage() == language::input::LANG_SYGUS;
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback