From 716ce9168d846ea991f8404a78aeb1ccccfbce14 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Wed, 2 May 2018 20:25:09 -0500 Subject: Initial support for string standard in smt lib 2.6 (#1848) --- src/main/interactive_shell.cpp | 28 +++++----- src/main/main.cpp | 5 +- src/options/language.cpp | 61 ++++++++++++++++++++ src/options/language.h | 34 ++++++++++-- src/options/language.i | 2 + src/options/options_template.cpp | 5 +- src/parser/antlr_input.cpp | 20 ++++--- src/parser/parser_builder.cpp | 14 +++-- src/parser/smt2/Smt2.g | 4 +- src/parser/smt2/smt2.cpp | 20 +++++-- src/parser/smt2/smt2.h | 21 ++++--- src/parser/smt2/smt2_input.cpp | 4 +- src/printer/printer.cpp | 4 ++ src/printer/smt2/smt2_printer.cpp | 113 ++++++++++++++++++++++---------------- src/printer/smt2/smt2_printer.h | 16 +++--- src/smt/smt_engine.cpp | 56 +++++++++---------- src/util/result.cpp | 19 +++---- src/util/sexpr.cpp | 7 +-- 18 files changed, 279 insertions(+), 154 deletions(-) (limited to 'src') diff --git a/src/main/interactive_shell.cpp b/src/main/interactive_shell.cpp index 4761ba07e..e58c5319a 100644 --- a/src/main/interactive_shell.cpp +++ b/src/main/interactive_shell.cpp @@ -125,22 +125,25 @@ InteractiveShell::InteractiveShell(ExprManager& exprManager, commandsBegin = smt1_commands; commandsEnd = smt1_commands + sizeof(smt1_commands) / sizeof(*smt1_commands); break; - case output::LANG_SMTLIB_V2_0: - case output::LANG_SMTLIB_V2_5: - case output::LANG_SMTLIB_V2_6: - d_historyFilename = string(getenv("HOME")) + "/.cvc4_history_smtlib2"; - commandsBegin = smt2_commands; - commandsEnd = smt2_commands + sizeof(smt2_commands) / sizeof(*smt2_commands); - break; case output::LANG_TPTP: d_historyFilename = string(getenv("HOME")) + "/.cvc4_history_tptp"; commandsBegin = tptp_commands; commandsEnd = tptp_commands + sizeof(tptp_commands) / sizeof(*tptp_commands); break; default: - std::stringstream ss; - ss << "internal error: unhandled language " << lang; - throw Exception(ss.str()); + if (language::isOutputLang_smt2(lang)) + { + d_historyFilename = string(getenv("HOME")) + "/.cvc4_history_smtlib2"; + commandsBegin = smt2_commands; + commandsEnd = + smt2_commands + sizeof(smt2_commands) / sizeof(*smt2_commands); + } + else + { + std::stringstream ss; + ss << "internal error: unhandled language " << lang; + throw Exception(ss.str()); + } } d_usingReadline = true; int err = ::read_history(d_historyFilename.c_str()); @@ -333,9 +336,8 @@ restart: line += "\n"; goto restart; } catch(ParserException& pe) { - if(d_options.getOutputLanguage() == output::LANG_SMTLIB_V2_0 || - d_options.getOutputLanguage() == output::LANG_SMTLIB_V2_5 || - d_options.getOutputLanguage() == output::LANG_SMTLIB_V2_6) { + if (language::isOutputLang_smt2(d_options.getOutputLanguage())) + { d_out << "(error \"" << pe << "\")" << endl; } else { d_out << pe << endl; diff --git a/src/main/main.cpp b/src/main/main.cpp index 758d10af8..29d720b90 100644 --- a/src/main/main.cpp +++ b/src/main/main.cpp @@ -64,9 +64,8 @@ int main(int argc, char* argv[]) { #ifdef CVC4_COMPETITION_MODE *opts.getOut() << "unknown" << endl; #endif - if(opts.getOutputLanguage() == output::LANG_SMTLIB_V2_0 || - opts.getOutputLanguage() == output::LANG_SMTLIB_V2_5 || - opts.getOutputLanguage() == output::LANG_SMTLIB_V2_6) { + if (language::isOutputLang_smt2(opts.getOutputLanguage())) + { *opts.getOut() << "(error \"" << e << "\")" << endl; } else { *opts.getErr() << "CVC4 Error:" << endl << e << endl; 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\ diff --git a/src/parser/antlr_input.cpp b/src/parser/antlr_input.cpp index a4bab5a8d..1e5d62ef8 100644 --- a/src/parser/antlr_input.cpp +++ b/src/parser/antlr_input.cpp @@ -254,12 +254,6 @@ AntlrInput* AntlrInput::newInput(InputLanguage lang, AntlrInputStream& inputStre input = new Smt1Input(inputStream); break; - case LANG_SMTLIB_V2_0: - case LANG_SMTLIB_V2_5: - case LANG_SMTLIB_V2_6: - input = new Smt2Input(inputStream, lang); - break; - case LANG_SYGUS: input = new SygusInput(inputStream); break; @@ -269,9 +263,17 @@ AntlrInput* AntlrInput::newInput(InputLanguage lang, AntlrInputStream& inputStre break; default: - std::stringstream ss; - ss << "internal error: unhandled language " << lang << " in AntlrInput::newInput"; - throw InputStreamException(ss.str()); + if (language::isInputLang_smt2(lang)) + { + input = new Smt2Input(inputStream, lang); + } + else + { + std::stringstream ss; + ss << "internal error: unhandled language " << lang + << " in AntlrInput::newInput"; + throw InputStreamException(ss.str()); + } } return input; diff --git a/src/parser/parser_builder.cpp b/src/parser/parser_builder.cpp index ceda2ba47..9f161b830 100644 --- a/src/parser/parser_builder.cpp +++ b/src/parser/parser_builder.cpp @@ -91,11 +91,6 @@ Parser* ParserBuilder::build() case language::input::LANG_SMTLIB_V1: parser = new Smt1(d_exprManager, input, d_strictMode, d_parseOnly); break; - case language::input::LANG_SMTLIB_V2_0: - case language::input::LANG_SMTLIB_V2_5: - case language::input::LANG_SMTLIB_V2_6: - parser = new Smt2(d_exprManager, input, d_strictMode, d_parseOnly); - break; case language::input::LANG_SYGUS: parser = new Smt2(d_exprManager, input, d_strictMode, d_parseOnly); break; @@ -103,7 +98,14 @@ Parser* ParserBuilder::build() parser = new Tptp(d_exprManager, input, d_strictMode, d_parseOnly); break; default: - parser = new Parser(d_exprManager, input, d_strictMode, d_parseOnly); + if (language::isInputLang_smt2(d_lang)) + { + parser = new Smt2(d_exprManager, input, d_strictMode, d_parseOnly); + } + else + { + parser = new Parser(d_exprManager, input, d_strictMode, d_parseOnly); + } break; } diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index ae9d304f1..74f8e71d3 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -3103,7 +3103,7 @@ GET_PROOF_TOK : 'get-proof'; GET_UNSAT_ASSUMPTIONS_TOK : 'get-unsat-assumptions'; GET_UNSAT_CORE_TOK : 'get-unsat-core'; EXIT_TOK : 'exit'; -RESET_TOK : { PARSER_STATE->v2_5(false) }? 'reset'; +RESET_TOK : { PARSER_STATE->v2_5() }? 'reset'; RESET_ASSERTIONS_TOK : 'reset-assertions'; ITE_TOK : 'ite'; LET_TOK : { !PARSER_STATE->sygus() }? 'let'; @@ -3362,7 +3362,7 @@ STRING_LITERAL_2_0 * will be part of the token text. Use the str[] parser rule instead. */ STRING_LITERAL_2_5 - : { PARSER_STATE->v2_5(false) || PARSER_STATE->sygus() }?=> + : { PARSER_STATE->v2_5() || PARSER_STATE->sygus() }?=> '"' (~('"') | '""')* '"' ; diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index 332c66be1..1d66ab0c1 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -129,10 +129,22 @@ void Smt2::addStringOperators() { addOperator(kind::STRING_STRREPL, "str.replace" ); addOperator(kind::STRING_PREFIX, "str.prefixof" ); addOperator(kind::STRING_SUFFIX, "str.suffixof" ); - addOperator(kind::STRING_ITOS, "int.to.str" ); - addOperator(kind::STRING_STOI, "str.to.int" ); - addOperator(kind::STRING_IN_REGEXP, "str.in.re"); - addOperator(kind::STRING_TO_REGEXP, "str.to.re"); + // at the moment, we only use this syntax for smt2.6.1 + if (getInput()->getLanguage() == language::input::LANG_SMTLIB_V2_6_1) + { + addOperator(kind::STRING_ITOS, "str.from-int"); + addOperator(kind::STRING_STOI, "str.to-int"); + addOperator(kind::STRING_IN_REGEXP, "str.in-re"); + addOperator(kind::STRING_TO_REGEXP, "str.to-re"); + } + else + { + addOperator(kind::STRING_ITOS, "int.to.str"); + addOperator(kind::STRING_STOI, "str.to.int"); + addOperator(kind::STRING_IN_REGEXP, "str.in.re"); + addOperator(kind::STRING_TO_REGEXP, "str.to.re"); + } + addOperator(kind::REGEXP_CONCAT, "re.++"); addOperator(kind::REGEXP_UNION, "re.union"); addOperator(kind::REGEXP_INTER, "re.inter"); 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; diff --git a/src/parser/smt2/smt2_input.cpp b/src/parser/smt2/smt2_input.cpp index 0958e9d6c..b7ffe6991 100644 --- a/src/parser/smt2/smt2_input.cpp +++ b/src/parser/smt2/smt2_input.cpp @@ -66,9 +66,7 @@ Smt2Input::~Smt2Input() { } void Smt2Input::setLanguage(InputLanguage lang) { - CheckArgument(lang == language::input::LANG_SMTLIB_V2_0 || - lang == language::input::LANG_SMTLIB_V2_5 || - lang == language::input::LANG_SMTLIB_V2_6, lang); + CheckArgument(language::isInputLang_smt2(lang), lang); d_lang = lang; } diff --git a/src/printer/printer.cpp b/src/printer/printer.cpp index e8ebadeb8..f9486f017 100644 --- a/src/printer/printer.cpp +++ b/src/printer/printer.cpp @@ -50,6 +50,10 @@ unique_ptr Printer::makePrinter(OutputLanguage lang) return unique_ptr( new printer::smt2::Smt2Printer(printer::smt2::smt2_6_variant)); + case LANG_SMTLIB_V2_6_1: + return unique_ptr( + new printer::smt2::Smt2Printer(printer::smt2::smt2_6_1_variant)); + case LANG_TPTP: return unique_ptr(new printer::tptp::TptpPrinter()); diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index 8c9680a74..5d2b8972d 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -42,7 +42,13 @@ namespace smt2 { static OutputLanguage variantToLanguage(Variant v); -static string smtKindString(Kind k); +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; +} static void printBvParameterizedOp(std::ostream& out, TNode n); static void printFpParameterizedOp(std::ostream& out, TNode n); @@ -191,10 +197,10 @@ void Smt2Printer::toStream(std::ostream& out, out << (n.getConst() ? "true" : "false"); break; case kind::BUILTIN: - out << smtKindString(n.getConst()); + out << smtKindString(n.getConst(), d_variant); break; case kind::CHAIN_OP: - out << smtKindString(n.getConst().getOperator()); + out << smtKindString(n.getConst().getOperator(), d_variant); break; case kind::CONST_RATIONAL: { const Rational& r = n.getConst(); @@ -323,7 +329,8 @@ void Smt2Printer::toStream(std::ostream& out, if (force_nt.isReal()) { out << "(" << smtKindString(force_nt.isInteger() ? kind::TO_INTEGER - : kind::TO_REAL) + : kind::TO_REAL, + d_variant) << " "; toStream(out, n, toDepth, types, TypeNode::null()); out << ")"; @@ -385,8 +392,8 @@ void Smt2Printer::toStream(std::ostream& out, // builtin theory case kind::APPLY: break; case kind::EQUAL: - case kind::DISTINCT: - out << smtKindString(k) << " "; + case kind::DISTINCT: + out << smtKindString(k, d_variant) << " "; parametricTypeChildren = true; break; case kind::CHAIN: break; @@ -407,14 +414,16 @@ void Smt2Printer::toStream(std::ostream& out, case kind::IMPLIES: case kind::OR: case kind::XOR: - case kind::ITE: out << smtKindString(k) << " "; break; + case kind::ITE: + out << smtKindString(k, d_variant) << " "; + break; - // uf theory + // uf theory case kind::APPLY_UF: typeChildren = true; break; // higher-order case kind::HO_APPLY: break; case kind::LAMBDA: - out << smtKindString(k) << " "; + out << smtKindString(k, d_variant) << " "; break; // arith theory @@ -453,7 +462,7 @@ void Smt2Printer::toStream(std::ostream& out, case kind::TO_REAL: case kind::POW: parametricTypeChildren = true; - out << smtKindString(k) << " "; + out << smtKindString(k, d_variant) << " "; break; case kind::DIVISIBLE: @@ -466,9 +475,11 @@ void Smt2Printer::toStream(std::ostream& out, case kind::STORE: typeChildren = true; case kind::PARTIAL_SELECT_0: case kind::PARTIAL_SELECT_1: - case kind::ARRAY_TYPE: out << smtKindString(k) << " "; break; + case kind::ARRAY_TYPE: + out << smtKindString(k, d_variant) << " "; + break; - // string theory + // string theory case kind::STRING_CONCAT: if(d_variant == z3str_variant) { out << "Concat "; @@ -499,30 +510,30 @@ void Smt2Printer::toStream(std::ostream& out, out << ")"; return; } - out << "str.in.re "; + out << smtKindString(k, d_variant) << " "; break; } - case kind::STRING_LENGTH: out << (d_variant == z3str_variant ? "Length " : "str.len "); break; - case kind::STRING_SUBSTR: out << "str.substr "; break; - case kind::STRING_CHARAT: out << "str.at "; break; - case kind::STRING_STRCTN: out << "str.contains "; break; - case kind::STRING_STRIDOF: out << "str.indexof "; break; - case kind::STRING_STRREPL: out << "str.replace "; break; - case kind::STRING_PREFIX: out << "str.prefixof "; break; - case kind::STRING_SUFFIX: out << "str.suffixof "; break; - case kind::STRING_ITOS: out << "int.to.str "; break; - case kind::STRING_STOI: out << "str.to.int "; break; - case kind::STRING_TO_REGEXP: out << "str.to.re "; break; - case kind::REGEXP_CONCAT: out << "re.++ "; break; - case kind::REGEXP_UNION: out << "re.union "; break; - case kind::REGEXP_INTER: out << "re.inter "; break; - case kind::REGEXP_STAR: out << "re.* "; break; - case kind::REGEXP_PLUS: out << "re.+ "; break; - case kind::REGEXP_OPT: out << "re.opt "; break; - case kind::REGEXP_RANGE: out << "re.range "; break; - case kind::REGEXP_LOOP: out << "re.loop "; break; - case kind::REGEXP_EMPTY: out << "re.nostr "; break; - case kind::REGEXP_SIGMA: out << "re.allchar "; break; + case kind::STRING_LENGTH: + case kind::STRING_SUBSTR: + case kind::STRING_CHARAT: + case kind::STRING_STRCTN: + case kind::STRING_STRIDOF: + case kind::STRING_STRREPL: + case kind::STRING_PREFIX: + case kind::STRING_SUFFIX: + case kind::STRING_ITOS: + case kind::STRING_STOI: + case kind::STRING_TO_REGEXP: + case kind::REGEXP_CONCAT: + case kind::REGEXP_UNION: + case kind::REGEXP_INTER: + case kind::REGEXP_STAR: + case kind::REGEXP_PLUS: + case kind::REGEXP_OPT: + case kind::REGEXP_RANGE: + case kind::REGEXP_LOOP: + case kind::REGEXP_EMPTY: + case kind::REGEXP_SIGMA: out << smtKindString(k, d_variant) << " "; break; case kind::CARDINALITY_CONSTRAINT: out << "fmf.card "; break; case kind::CARDINALITY_VALUE: out << "fmf.card.val "; break; @@ -586,12 +597,12 @@ void Smt2Printer::toStream(std::ostream& out, case kind::TRANSPOSE: case kind::TCLOSURE: parametricTypeChildren = true; - out << smtKindString(k) << " "; + out << smtKindString(k, d_variant) << " "; break; case kind::MEMBER: typeChildren = true; case kind::SET_TYPE: case kind::SINGLETON: - case kind::COMPLEMENT:out << smtKindString(k) << " "; break; + case kind::COMPLEMENT: out << smtKindString(k, d_variant) << " "; break; case kind::UNIVERSE_SET:out << "(as univset " << n.getType() << ")";break; // fp theory @@ -621,7 +632,8 @@ void Smt2Printer::toStream(std::ostream& out, case kind::FLOATINGPOINT_ISNEG: case kind::FLOATINGPOINT_ISPOS: case kind::FLOATINGPOINT_TO_REAL: - out << smtKindString(k) << ' '; break; + out << smtKindString(k, d_variant) << ' '; + break; case kind::FLOATINGPOINT_TO_FP_IEEE_BITVECTOR: case kind::FLOATINGPOINT_TO_FP_FLOATINGPOINT: @@ -681,7 +693,7 @@ void Smt2Printer::toStream(std::ostream& out, case kind::SEP_EMP: case kind::SEP_PTO: case kind::SEP_STAR: - case kind::SEP_WAND: out << smtKindString(k) << " "; break; + case kind::SEP_WAND: out << smtKindString(k, d_variant) << " "; break; case kind::SEP_NIL: out << "(as sep.nil " << n.getType() << ")"; @@ -773,7 +785,8 @@ void Smt2Printer::toStream(std::ostream& out, }else if( n.getKind()==kind::APPLY_TESTER ){ unsigned cindex = Datatype::indexOf(n.getOperator().toExpr()); const Datatype& dt = Datatype::datatypeOf(n.getOperator().toExpr()); - if( d_variant==smt2_6_variant ){ + if (isVariant_2_6(d_variant)) + { out << "(_ is "; toStream(out, Node::fromExpr(dt[cindex].getConstructor()), toDepth < 0 ? toDepth : toDepth - 1, types, TypeNode::null()); out << ")"; @@ -856,7 +869,7 @@ void Smt2Printer::toStream(std::ostream& out, if(forceBinary && i < n.getNumChildren() - 1) { // not going to work properly for parameterized kinds! Assert(n.getMetaKind() != kind::metakind::PARAMETERIZED); - out << " (" << smtKindString(n.getKind()) << ' '; + out << " (" << smtKindString(n.getKind(), d_variant) << ' '; parens << ')'; ++c; } else { @@ -869,7 +882,7 @@ void Smt2Printer::toStream(std::ostream& out, } }/* Smt2Printer::toStream(TNode) */ -static string smtKindString(Kind k) +static string smtKindString(Kind k, Variant v) { switch(k) { // builtin theory @@ -1039,7 +1052,7 @@ static string smtKindString(Kind k) //string theory case kind::STRING_CONCAT: return "str.++"; - case kind::STRING_LENGTH: return "str.len"; + case kind::STRING_LENGTH: return v == z3str_variant ? "Length" : "str.len"; case kind::STRING_SUBSTR: return "str.substr" ; case kind::STRING_STRCTN: return "str.contains" ; case kind::STRING_CHARAT: return "str.at" ; @@ -1047,10 +1060,14 @@ static string smtKindString(Kind k) case kind::STRING_STRREPL: return "str.replace" ; case kind::STRING_PREFIX: return "str.prefixof" ; case kind::STRING_SUFFIX: return "str.suffixof" ; - case kind::STRING_ITOS: return "int.to.str" ; - 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::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::REGEXP_CONCAT: return "re.++"; case kind::REGEXP_UNION: return "re.union"; case kind::REGEXP_INTER: return "re.inter"; @@ -1310,7 +1327,7 @@ void DeclareTypeCommandToStream(std::ostream& out, const std::vector* type_refs = model.getRepSet()->getTypeRepsOrNull(tn); if (options::modelUninterpDtEnum() && tn.isSort() && type_refs != nullptr) { - if (variant == smt2_6_variant) + if (isVariant_2_6(variant)) { out << "(declare-datatypes ((" << command.getSymbol() << " 0)) ("; } @@ -1893,7 +1910,7 @@ static void toStream(std::ostream& out, out << "co"; } out << "datatypes"; - if (v == smt2_6_variant) + if (isVariant_2_6(v)) { out << " ("; for (vector::const_iterator i = datatypes.begin(), diff --git a/src/printer/smt2/smt2_printer.h b/src/printer/smt2/smt2_printer.h index 922b69a9e..1d281aed4 100644 --- a/src/printer/smt2/smt2_printer.h +++ b/src/printer/smt2/smt2_printer.h @@ -27,14 +27,16 @@ namespace CVC4 { namespace printer { namespace smt2 { -enum Variant { +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 - 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 + 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 */ 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 97e3f0215..ca01ccd8e 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -1304,8 +1304,8 @@ void SmtEngine::setDefaults() { // Language-based defaults if (!options::bitvectorDivByZeroConst.wasSetByUser()) { - options::bitvectorDivByZeroConst.set(options::inputLanguage() - == language::input::LANG_SMTLIB_V2_6); + options::bitvectorDivByZeroConst.set( + language::isInputLang_smt2_6(options::inputLanguage())); } if (options::inputLanguage() == language::input::LANG_SYGUS) { @@ -2262,44 +2262,40 @@ void SmtEngine::setInfo(const std::string& key, const CVC4::SExpr& value) d_filename = value.getValue(); return; } else if(key == "smt-lib-version") { + language::input::Language ilang = language::input::LANG_AUTO; if( (value.isInteger() && value.getIntegerValue() == Integer(2)) || (value.isRational() && value.getRationalValue() == Rational(2)) || value.getValue() == "2" || value.getValue() == "2.0" ) { - options::inputLanguage.set(language::input::LANG_SMTLIB_V2_0); - - // supported SMT-LIB version - if(!options::outputLanguage.wasSetByUser() && - ( options::outputLanguage() == language::output::LANG_SMTLIB_V2_5 || options::outputLanguage() == language::output::LANG_SMTLIB_V2_6 )) { - options::outputLanguage.set(language::output::LANG_SMTLIB_V2_0); - *options::out() << language::SetLanguage(language::output::LANG_SMTLIB_V2_0); - } - return; + ilang = language::input::LANG_SMTLIB_V2_0; } else if( (value.isRational() && value.getRationalValue() == Rational(5, 2)) || value.getValue() == "2.5" ) { - options::inputLanguage.set(language::input::LANG_SMTLIB_V2_5); - - // supported SMT-LIB version - if(!options::outputLanguage.wasSetByUser() && - options::outputLanguage() == language::output::LANG_SMTLIB_V2_0) { - options::outputLanguage.set(language::output::LANG_SMTLIB_V2_5); - *options::out() << language::SetLanguage(language::output::LANG_SMTLIB_V2_5); - } - return; + ilang = language::input::LANG_SMTLIB_V2_5; } else if( (value.isRational() && value.getRationalValue() == Rational(13, 5)) || value.getValue() == "2.6" ) { - options::inputLanguage.set(language::input::LANG_SMTLIB_V2_6); - - // supported SMT-LIB version - if(!options::outputLanguage.wasSetByUser() && - options::outputLanguage() == language::output::LANG_SMTLIB_V2_0) { - options::outputLanguage.set(language::output::LANG_SMTLIB_V2_6); - *options::out() << language::SetLanguage(language::output::LANG_SMTLIB_V2_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; + throw UnrecognizedOptionException(); + } + options::inputLanguage.set(ilang); + // also update the output language + if (!options::outputLanguage.wasSetByUser()) + { + language::output::Language olang = language::toOutputLanguage(ilang); + if (options::outputLanguage() != olang) + { + options::outputLanguage.set(olang); + *options::out() << language::SetLanguage(olang); } - return; } - Warning() << "Warning: unsupported smt-lib-version: " << value << endl; - throw UnrecognizedOptionException(); + return; } else if(key == "status") { string s; if(value.isAtom()) { diff --git a/src/util/result.cpp b/src/util/result.cpp index 27d82bb6f..dfcd74ff7 100644 --- a/src/util/result.cpp +++ b/src/util/result.cpp @@ -349,24 +349,21 @@ void Result::toStreamTptp(std::ostream& out) const { void Result::toStream(std::ostream& out, OutputLanguage language) const { switch (language) { - case language::output::LANG_SMTLIB_V2_0: - case language::output::LANG_SMTLIB_V2_5: - case language::output::LANG_SMTLIB_V2_6: case language::output::LANG_SYGUS: - case language::output::LANG_Z3STR: toStreamSmt2(out); break; case language::output::LANG_TPTP: toStreamTptp(out); break; - case language::output::LANG_AST: - case language::output::LANG_AUTO: - case language::output::LANG_CVC3: - case language::output::LANG_CVC4: - case language::output::LANG_MAX: - case language::output::LANG_SMTLIB_V1: default: - toStreamDefault(out); + if (language::isOutputLang_smt2(language)) + { + toStreamSmt2(out); + } + else + { + toStreamDefault(out); + } break; }; } diff --git a/src/util/sexpr.cpp b/src/util/sexpr.cpp index 504d58b0e..fbc8802d6 100644 --- a/src/util/sexpr.cpp +++ b/src/util/sexpr.cpp @@ -273,18 +273,13 @@ void SExpr::toStreamRec(std::ostream& out, const SExpr& sexpr, bool SExpr::languageQuotesKeywords(OutputLanguage language) { switch (language) { case language::output::LANG_SMTLIB_V1: - case language::output::LANG_SMTLIB_V2_0: - case language::output::LANG_SMTLIB_V2_5: - case language::output::LANG_SMTLIB_V2_6: case language::output::LANG_SYGUS: case language::output::LANG_TPTP: - case language::output::LANG_Z3STR: return true; case language::output::LANG_AST: case language::output::LANG_CVC3: case language::output::LANG_CVC4: - default: - return false; + default: return language::isOutputLang_smt2(language); }; } -- cgit v1.2.3