diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-05-02 20:25:09 -0500 |
---|---|---|
committer | Andres Noetzli <andres.noetzli@gmail.com> | 2018-05-02 18:25:09 -0700 |
commit | 716ce9168d846ea991f8404a78aeb1ccccfbce14 (patch) | |
tree | 5a617909b7d82ed2265693461f4f9f0a4c811f56 /src/options | |
parent | d3f4ac852146c41341e485d9035f3631993e3fa5 (diff) |
Initial support for string standard in smt lib 2.6 (#1848)
Diffstat (limited to 'src/options')
-rw-r--r-- | src/options/language.cpp | 61 | ||||
-rw-r--r-- | src/options/language.h | 34 | ||||
-rw-r--r-- | src/options/language.i | 2 | ||||
-rw-r--r-- | src/options/options_template.cpp | 5 |
4 files changed, 97 insertions, 5 deletions
diff --git a/src/options/language.cpp b/src/options/language.cpp index 86beffd6d..f76893866 100644 --- a/src/options/language.cpp +++ b/src/options/language.cpp @@ -19,12 +19,62 @@ namespace CVC4 { namespace language { +/** define the end points of smt2 languages */ +namespace input { +Language LANG_SMTLIB_V2_END = LANG_SMTLIB_V2_6_1; +} +namespace output { +Language LANG_SMTLIB_V2_END = LANG_SMTLIB_V2_6_1; +} + +bool isInputLang_smt2(InputLanguage lang) +{ + return (lang >= input::LANG_SMTLIB_V2_0 && lang <= input::LANG_SMTLIB_V2_END) + || lang == input::LANG_Z3STR; +} + +bool isOutputLang_smt2(OutputLanguage lang) +{ + return (lang >= output::LANG_SMTLIB_V2_0 + && lang <= output::LANG_SMTLIB_V2_END) + || lang == output::LANG_Z3STR; +} + +bool isInputLang_smt2_5(InputLanguage lang, bool exact) +{ + return exact ? lang == input::LANG_SMTLIB_V2_5 + : (lang >= input::LANG_SMTLIB_V2_5 + && lang <= input::LANG_SMTLIB_V2_END); +} + +bool isOutputLang_smt2_5(OutputLanguage lang, bool exact) +{ + return exact ? lang == output::LANG_SMTLIB_V2_5 + : (lang >= output::LANG_SMTLIB_V2_5 + && lang <= output::LANG_SMTLIB_V2_END); +} + +bool isInputLang_smt2_6(InputLanguage lang, bool exact) +{ + return exact ? lang == input::LANG_SMTLIB_V2_6 + : (lang >= input::LANG_SMTLIB_V2_6 + && lang <= input::LANG_SMTLIB_V2_END); +} + +bool isOutputLang_smt2_6(OutputLanguage lang, bool exact) +{ + return exact ? lang == output::LANG_SMTLIB_V2_6 + : (lang >= output::LANG_SMTLIB_V2_6 + && lang <= output::LANG_SMTLIB_V2_END); +} + InputLanguage toInputLanguage(OutputLanguage language) { switch(language) { case output::LANG_SMTLIB_V1: case output::LANG_SMTLIB_V2_0: case output::LANG_SMTLIB_V2_5: case output::LANG_SMTLIB_V2_6: + case output::LANG_SMTLIB_V2_6_1: case output::LANG_TPTP: case output::LANG_CVC4: case output::LANG_Z3STR: @@ -47,6 +97,7 @@ OutputLanguage toOutputLanguage(InputLanguage language) { case input::LANG_SMTLIB_V2_0: case input::LANG_SMTLIB_V2_5: case input::LANG_SMTLIB_V2_6: + case input::LANG_SMTLIB_V2_6_1: case input::LANG_TPTP: case input::LANG_CVC4: case input::LANG_Z3STR: @@ -90,6 +141,11 @@ OutputLanguage toOutputLanguage(std::string language) { } else if(language == "smtlib2.6" || language == "smt2.6" || language == "LANG_SMTLIB_V2_6") { return output::LANG_SMTLIB_V2_6; + } + else if (language == "smtlib2.6.1" || language == "smt2.6.1" + || language == "LANG_SMTLIB_V2_6_1") + { + return output::LANG_SMTLIB_V2_6_1; } else if(language == "tptp" || language == "LANG_TPTP") { return output::LANG_TPTP; } else if(language == "z3str" || language == "z3-str" || @@ -125,6 +181,11 @@ InputLanguage toInputLanguage(std::string language) { language == "smtlib2.6" || language == "smt2.6" || language == "LANG_SMTLIB_V2_6" || language == "LANG_SMTLIB_V2") { return input::LANG_SMTLIB_V2_6; + } + else if (language == "smtlib2.6.1" || language == "smt2.6.1" + || language == "LANG_SMTLIB_V2_6_1") + { + return input::LANG_SMTLIB_V2_6_1; } else if(language == "tptp" || language == "LANG_TPTP") { return input::LANG_TPTP; } else if(language == "z3str" || language == "z3-str" || diff --git a/src/options/language.h b/src/options/language.h index f238e765d..2b2e7d5da 100644 --- a/src/options/language.h +++ b/src/options/language.h @@ -30,7 +30,8 @@ namespace language { namespace input { -enum CVC4_PUBLIC Language { +enum CVC4_PUBLIC Language +{ // SPECIAL "NON-LANGUAGE" LANGUAGES HAVE ENUM VALUE < 0 /** Auto-detect the language */ @@ -53,6 +54,8 @@ enum CVC4_PUBLIC Language { LANG_SMTLIB_V2_6, /** Backward-compatibility for enumeration naming */ LANG_SMTLIB_V2 = LANG_SMTLIB_V2_6, + /** The SMTLIB v2.6 input language, with support for the strings standard */ + LANG_SMTLIB_V2_6_1, /** The TPTP input language */ LANG_TPTP, /** The CVC4 input language */ @@ -67,7 +70,7 @@ enum CVC4_PUBLIC Language { /** LANG_MAX is > any valid InputLanguage id */ LANG_MAX -};/* enum Language */ +}; /* enum Language */ inline std::ostream& operator<<(std::ostream& out, Language lang) CVC4_PUBLIC; inline std::ostream& operator<<(std::ostream& out, Language lang) { @@ -87,6 +90,7 @@ inline std::ostream& operator<<(std::ostream& out, Language lang) { case LANG_SMTLIB_V2_6: out << "LANG_SMTLIB_V2_6"; break; + case LANG_SMTLIB_V2_6_1: out << "LANG_SMTLIB_V2_6_1"; break; case LANG_TPTP: out << "LANG_TPTP"; break; @@ -109,7 +113,8 @@ inline std::ostream& operator<<(std::ostream& out, Language lang) { namespace output { -enum CVC4_PUBLIC Language { +enum CVC4_PUBLIC Language +{ // SPECIAL "NON-LANGUAGE" LANGUAGES HAVE ENUM VALUE < 0 /** Match the output language to the input language */ @@ -132,6 +137,8 @@ enum CVC4_PUBLIC Language { LANG_SMTLIB_V2_6 = input::LANG_SMTLIB_V2_6, /** Backward-compatibility for enumeration naming */ LANG_SMTLIB_V2 = input::LANG_SMTLIB_V2, + /** The SMTLIB v2.6 output language */ + LANG_SMTLIB_V2_6_1 = input::LANG_SMTLIB_V2_6_1, /** The TPTP output language */ LANG_TPTP = input::LANG_TPTP, /** The CVC4 output language */ @@ -151,7 +158,7 @@ enum CVC4_PUBLIC Language { /** LANG_MAX is > any valid OutputLanguage id */ LANG_MAX -};/* enum Language */ +}; /* enum Language */ inline std::ostream& operator<<(std::ostream& out, Language lang) CVC4_PUBLIC; inline std::ostream& operator<<(std::ostream& out, Language lang) { @@ -165,6 +172,8 @@ inline std::ostream& operator<<(std::ostream& out, Language lang) { case LANG_SMTLIB_V2_5: out << "LANG_SMTLIB_V2_5"; break; + case LANG_SMTLIB_V2_6: out << "LANG_SMTLIB_V2_6"; break; + case LANG_SMTLIB_V2_6_1: out << "LANG_SMTLIB_V2_6_1"; break; case LANG_TPTP: out << "LANG_TPTP"; break; @@ -198,6 +207,23 @@ typedef language::output::Language OutputLanguage; namespace language { +/** Is the language a variant of the smtlib version 2 language? */ +bool isInputLang_smt2(InputLanguage lang) CVC4_PUBLIC; +bool isOutputLang_smt2(OutputLanguage lang) CVC4_PUBLIC; + +/** + * Is the language smtlib 2.5 or above? If exact=true, then this method returns + * false if the input language is not exactly SMT-LIB 2.6. + */ +bool isInputLang_smt2_5(InputLanguage lang, bool exact = false) CVC4_PUBLIC; +bool isOutputLang_smt2_5(OutputLanguage lang, bool exact = false) CVC4_PUBLIC; +/** + * Is the language 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 isInputLang_smt2_6(InputLanguage lang, bool exact = false) CVC4_PUBLIC; +bool isOutputLang_smt2_6(OutputLanguage lang, bool exact = false) CVC4_PUBLIC; + InputLanguage toInputLanguage(OutputLanguage language) CVC4_PUBLIC; OutputLanguage toOutputLanguage(InputLanguage language) CVC4_PUBLIC; InputLanguage toInputLanguage(std::string language) CVC4_PUBLIC; diff --git a/src/options/language.i b/src/options/language.i index 427e6c608..177e590f5 100644 --- a/src/options/language.i +++ b/src/options/language.i @@ -24,6 +24,7 @@ namespace CVC4 { %rename(INPUT_LANG_SMTLIB_V2_0) CVC4::language::input::LANG_SMTLIB_V2_0; %rename(INPUT_LANG_SMTLIB_V2_5) CVC4::language::input::LANG_SMTLIB_V2_5; %rename(INPUT_LANG_SMTLIB_V2_6) CVC4::language::input::LANG_SMTLIB_V2_6; +%rename(INPUT_LANG_SMTLIB_V2_6_1) CVC4::language::input::LANG_SMTLIB_V2_6_1; %rename(INPUT_LANG_TPTP) CVC4::language::input::LANG_TPTP; %rename(INPUT_LANG_CVC4) CVC4::language::input::LANG_CVC4; %rename(INPUT_LANG_MAX) CVC4::language::input::LANG_MAX; @@ -36,6 +37,7 @@ namespace CVC4 { %rename(OUTPUT_LANG_SMTLIB_V2_0) CVC4::language::output::LANG_SMTLIB_V2_0; %rename(OUTPUT_LANG_SMTLIB_V2_5) CVC4::language::output::LANG_SMTLIB_V2_5; %rename(OUTPUT_LANG_SMTLIB_V2_6) CVC4::language::output::LANG_SMTLIB_V2_6; +%rename(OUTPUT_LANG_SMTLIB_V2_6_1) CVC4::language::output::LANG_SMTLIB_V2_6_1; %rename(OUTPUT_LANG_TPTP) CVC4::language::output::LANG_TPTP; %rename(OUTPUT_LANG_CVC4) CVC4::language::output::LANG_CVC4; %rename(OUTPUT_LANG_AST) CVC4::language::output::LANG_AST; diff --git a/src/options/options_template.cpp b/src/options/options_template.cpp index 917dae687..4fdd477b9 100644 --- a/src/options/options_template.cpp +++ b/src/options/options_template.cpp @@ -423,7 +423,8 @@ static const std::string optionsFootnote = "\n\ sense of the option.\n\ "; -static const std::string languageDescription = "\ +static const std::string languageDescription = + "\ Languages currently supported as arguments to the -L / --lang option:\n\ auto attempt to automatically determine language\n\ cvc4 | presentation | pl CVC4 presentation language\n\ @@ -432,6 +433,7 @@ Languages currently supported as arguments to the -L / --lang option:\n\ smt2.0 | smtlib2 | smtlib2.0 SMT-LIB format 2.0\n\ smt2.5 | smtlib2.5 SMT-LIB format 2.5\n\ smt2.6 | smtlib2.6 SMT-LIB format 2.6\n\ + smt2.6.1 | smtlib2.6.1 SMT-LIB format 2.6 with support for the strings standard\n\ tptp TPTP format (cnf and fof)\n\ sygus SyGuS format\n\ \n\ @@ -444,6 +446,7 @@ Languages currently supported as arguments to the --output-lang option:\n\ smt2.0 | smtlib2.0 | smtlib2 SMT-LIB format 2.0\n\ smt2.5 | smtlib2.5 SMT-LIB format 2.5\n\ smt2.6 | smtlib2.6 SMT-LIB format 2.6\n\ + smt2.6.1 | smtlib2.6.1 SMT-LIB format 2.6 with support for the strings standard\n\ tptp TPTP format\n\ z3str SMT-LIB 2.0 with Z3-str string constraints\n\ ast internal format (simple syntax trees)\n\ |