diff options
Diffstat (limited to 'src')
-rw-r--r-- | src/api/cvc4cpp.cpp | 4 | ||||
-rw-r--r-- | src/options/language.cpp | 16 | ||||
-rw-r--r-- | src/options/language.h | 10 | ||||
-rw-r--r-- | src/options/language.i | 2 | ||||
-rw-r--r-- | src/options/options_template.cpp | 6 | ||||
-rw-r--r-- | src/parser/parser.cpp | 3 | ||||
-rw-r--r-- | src/parser/parser.h | 2 | ||||
-rw-r--r-- | src/parser/smt2/smt2.cpp | 6 | ||||
-rw-r--r-- | src/printer/printer.cpp | 6 | ||||
-rw-r--r-- | src/printer/smt2/smt2_printer.cpp | 23 | ||||
-rw-r--r-- | src/printer/smt2/smt2_printer.h | 13 | ||||
-rw-r--r-- | src/smt/smt_engine.cpp | 4 |
12 files changed, 27 insertions, 68 deletions
diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp index 24cd762a1..b27cc48b4 100644 --- a/src/api/cvc4cpp.cpp +++ b/src/api/cvc4cpp.cpp @@ -4384,9 +4384,9 @@ void Solver::setInfo(const std::string& keyword, const std::string& value) const "'notes', 'smt-lib-version' or 'status'"; CVC4_API_ARG_CHECK_EXPECTED(keyword != "smt-lib-version" || value == "2" || value == "2.0" || value == "2.5" - || value == "2.6" || value == "2.6.1", + || value == "2.6", value) - << "'2.0', '2.5', '2.6' or '2.6.1'"; + << "'2.0', '2.5', '2.6'"; CVC4_API_ARG_CHECK_EXPECTED(keyword != "status" || value == "sat" || value == "unsat" || value == "unknown", value) diff --git a/src/options/language.cpp b/src/options/language.cpp index 8c6f8421f..52263567b 100644 --- a/src/options/language.cpp +++ b/src/options/language.cpp @@ -21,10 +21,10 @@ namespace language { /** define the end points of smt2 languages */ namespace input { -Language LANG_SMTLIB_V2_END = LANG_SMTLIB_V2_6_1; +Language LANG_SMTLIB_V2_END = LANG_SMTLIB_V2_6; } namespace output { -Language LANG_SMTLIB_V2_END = LANG_SMTLIB_V2_6_1; +Language LANG_SMTLIB_V2_END = LANG_SMTLIB_V2_6; } bool isInputLang_smt2(InputLanguage lang) @@ -83,7 +83,6 @@ InputLanguage toInputLanguage(OutputLanguage language) { 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: @@ -106,7 +105,6 @@ 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: @@ -152,11 +150,6 @@ OutputLanguage toOutputLanguage(std::string language) { || language == "LANG_SMTLIB_V2") { 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" || @@ -197,11 +190,6 @@ 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 3a9ebf9d5..7866becd3 100644 --- a/src/options/language.h +++ b/src/options/language.h @@ -48,12 +48,10 @@ enum CVC4_PUBLIC Language LANG_SMTLIB_V2_0 = 0, /** The SMTLIB v2.5 input language */ LANG_SMTLIB_V2_5, - /** The SMTLIB v2.6 input language */ + /** The SMTLIB v2.6 input language, with support for the strings standard */ 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 */ @@ -87,7 +85,6 @@ 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; @@ -129,12 +126,10 @@ enum CVC4_PUBLIC Language LANG_SMTLIB_V2_0 = input::LANG_SMTLIB_V2_0, /** The SMTLIB v2.5 output language */ LANG_SMTLIB_V2_5 = input::LANG_SMTLIB_V2_5, - /** The SMTLIB v2.6 output language */ + /** The SMTLIB v2.6 output language, with support for the strings standard */ 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 */ @@ -168,7 +163,6 @@ inline std::ostream& operator<<(std::ostream& out, Language lang) { 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; diff --git a/src/options/language.i b/src/options/language.i index f61359d4e..acda19aec 100644 --- a/src/options/language.i +++ b/src/options/language.i @@ -23,7 +23,6 @@ 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,7 +35,6 @@ 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 8a227a2e7..fe742adfc 100644 --- a/src/options/options_template.cpp +++ b/src/options/options_template.cpp @@ -416,8 +416,7 @@ Languages currently supported as arguments to the -L / --lang option:\n\ smt | smtlib | smt2 |\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\ + smt2.6 | smtlib2.6 SMT-LIB format 2.6 with support for the strings standard\n\ tptp TPTP format (cnf, fof and tff)\n\ sygus | sygus2 SyGuS version 1.0 and 2.0 formats\n\ \n\ @@ -428,8 +427,7 @@ Languages currently supported as arguments to the --output-lang option:\n\ smt | smtlib | smt2 |\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\ + smt2.6 | smtlib2.6 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\ diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp index 5dca92370..c860d14c7 100644 --- a/src/parser/parser.cpp +++ b/src/parser/parser.cpp @@ -895,8 +895,7 @@ std::vector<unsigned> Parser::processAdHocStringEsc(const std::string& s) Expr Parser::mkStringConstant(const std::string& s) { ExprManager* em = d_solver->getExprManager(); - if (em->getOptions().getInputLanguage() - == language::input::LANG_SMTLIB_V2_6_1) + if (language::isInputLang_smt2_6(em->getOptions().getInputLanguage())) { return d_solver->mkString(s, true).getExpr(); } diff --git a/src/parser/parser.h b/src/parser/parser.h index cd4105cd0..7941cfdd5 100644 --- a/src/parser/parser.h +++ b/src/parser/parser.h @@ -842,7 +842,7 @@ public: * * This makes the string constant based on the string s. This may involve * processing ad-hoc escape sequences (if the language is not - * SMT-LIB 2.6.1 or higher), or otherwise calling the solver to construct + * SMT-LIB 2.6 or higher), or otherwise calling the solver to construct * the string. */ Expr mkStringConstant(const std::string& s); diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index 6cba1ce19..3c30f5c49 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -166,8 +166,8 @@ void Smt2::addStringOperators() { addOperator(api::STRING_SUFFIX, "str.suffixof"); addOperator(api::STRING_FROM_CODE, "str.from_code"); addOperator(api::STRING_IS_DIGIT, "str.is_digit"); - // at the moment, we only use this syntax for smt2.6.1 - if (getLanguage() == language::input::LANG_SMTLIB_V2_6_1 + // at the moment, we only use this syntax for smt2.6 + if (getLanguage() == language::input::LANG_SMTLIB_V2_6 || getLanguage() == language::input::LANG_SYGUS_V2) { addOperator(api::STRING_ITOS, "str.from_int"); @@ -682,7 +682,7 @@ Command* Smt2::setLogic(std::string name, bool fromCommand) defineType("RegLan", d_solver->getRegExpSort()); defineType("Int", d_solver->getIntegerSort()); - if (getLanguage() == language::input::LANG_SMTLIB_V2_6_1 + if (getLanguage() == language::input::LANG_SMTLIB_V2_6 || getLanguage() == language::input::LANG_SYGUS_V2) { defineVar("re.none", d_solver->mkRegexpEmpty()); diff --git a/src/printer/printer.cpp b/src/printer/printer.cpp index 886be0cfa..085a32c43 100644 --- a/src/printer/printer.cpp +++ b/src/printer/printer.cpp @@ -46,10 +46,6 @@ unique_ptr<Printer> Printer::makePrinter(OutputLanguage lang) return unique_ptr<Printer>( new printer::smt2::Smt2Printer(printer::smt2::smt2_6_variant)); - case LANG_SMTLIB_V2_6_1: - return unique_ptr<Printer>( - new printer::smt2::Smt2Printer(printer::smt2::smt2_6_1_variant)); - case LANG_TPTP: return unique_ptr<Printer>(new printer::tptp::TptpPrinter()); @@ -68,7 +64,7 @@ unique_ptr<Printer> Printer::makePrinter(OutputLanguage lang) // sygus version 2.0 does not have discrepancies with smt2, hence we use // a normal smt2 variant here. return unique_ptr<Printer>( - new printer::smt2::Smt2Printer(printer::smt2::smt2_6_1_variant)); + new printer::smt2::Smt2Printer(printer::smt2::smt2_6_variant)); case LANG_AST: return unique_ptr<Printer>(new printer::ast::AstPrinter()); diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index 4013cbd08..fbccd26ed 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -48,10 +48,7 @@ static OutputLanguage variantToLanguage(Variant v); static string smtKindString(Kind k, Variant v); /** returns whether the variant is smt-lib 2.6 or greater */ -bool isVariant_2_6(Variant v) -{ - return v == smt2_6_variant || v == smt2_6_1_variant; -} +bool isVariant_2_6(Variant v) { return v == smt2_6_variant; } static void toStreamRational(std::ostream& out, const Rational& r, @@ -1203,8 +1200,7 @@ static string smtKindString(Kind k, Variant v) case kind::STRING_CHARAT: return "str.at" ; case kind::STRING_STRIDOF: return "str.indexof" ; case kind::STRING_STRREPL: return "str.replace" ; - case kind::STRING_STRREPLALL: - return v == smt2_6_1_variant ? "str.replace_all" : "str.replaceall"; + case kind::STRING_STRREPLALL: return "str.replace_all"; case kind::STRING_TOLOWER: return "str.tolower"; case kind::STRING_TOUPPER: return "str.toupper"; case kind::STRING_REV: return "str.rev"; @@ -1213,16 +1209,11 @@ static string smtKindString(Kind k, Variant v) case kind::STRING_LEQ: return "str.<="; case kind::STRING_LT: return "str.<"; case kind::STRING_FROM_CODE: return "str.from_code"; - case kind::STRING_TO_CODE: - return v == smt2_6_1_variant ? "str.to_code" : "str.code"; - case kind::STRING_ITOS: - return v == smt2_6_1_variant ? "str.from_int" : "int.to.str"; - case kind::STRING_STOI: - return v == smt2_6_1_variant ? "str.to_int" : "str.to.int"; - case kind::STRING_IN_REGEXP: - return v == smt2_6_1_variant ? "str.in_re" : "str.in.re"; - case kind::STRING_TO_REGEXP: - return v == smt2_6_1_variant ? "str.to_re" : "str.to.re"; + case kind::STRING_TO_CODE: return "str.to_code"; + case kind::STRING_ITOS: return "str.from_int"; + case kind::STRING_STOI: return "str.to_int"; + case kind::STRING_IN_REGEXP: return "str.in_re"; + case kind::STRING_TO_REGEXP: return "str.to_re"; case kind::REGEXP_EMPTY: return "re.nostr"; case kind::REGEXP_SIGMA: return "re.allchar"; case kind::REGEXP_CONCAT: return "re.++"; diff --git a/src/printer/smt2/smt2_printer.h b/src/printer/smt2/smt2_printer.h index 579231364..b34acacbb 100644 --- a/src/printer/smt2/smt2_printer.h +++ b/src/printer/smt2/smt2_printer.h @@ -30,13 +30,12 @@ namespace smt2 { enum Variant { no_variant, - smt2_0_variant, // old-style 2.0 syntax, when it makes a difference - smt2_6_variant, // new-style 2.6 syntax, when it makes a difference - smt2_6_1_variant, // new-style 2.6 syntax, when it makes a difference, with - // support for the string standard - z3str_variant, // old-style 2.0 and also z3str syntax - sygus_variant // variant for sygus -}; /* enum Variant */ + smt2_0_variant, // old-style 2.0 syntax, when it makes a difference + smt2_6_variant, // new-style 2.6 syntax, when it makes a difference, with + // support for the string standard + z3str_variant, // old-style 2.0 and also z3str syntax + sygus_variant // variant for sygus +}; /* enum Variant */ class Smt2Printer : public CVC4::Printer { public: Smt2Printer(Variant variant = no_variant) : d_variant(variant) { } diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 990ffd04d..d4e83c672 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -990,10 +990,6 @@ void SmtEngine::setInfo(const std::string& key, const CVC4::SExpr& value) value.getValue() == "2.6" ) { ilang = language::input::LANG_SMTLIB_V2_6; } - else if (value.getValue() == "2.6.1") - { - ilang = language::input::LANG_SMTLIB_V2_6_1; - } else { Warning() << "Warning: unsupported smt-lib-version: " << value << endl; |