From 02b88b7665df5a6b1a2bce231d7567efdcc4b20a Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Tue, 19 May 2020 14:51:19 -0500 Subject: [PATCH] Update enum and option names for sygus languages (#4388) This ensures sygus is interpreted as sygus version 2; sygus1 must be used to specify sygus version 1. Required for the 1.8 release. --- src/options/language.cpp | 23 ++++++++++++++--------- src/options/language.h | 16 ++++++---------- src/options/language.i | 4 ++-- src/options/options_template.cpp | 3 ++- src/parser/antlr_input.cpp | 2 +- src/parser/parser_builder.cpp | 2 +- src/parser/smt2/smt2.cpp | 4 ++-- src/printer/printer.cpp | 2 +- src/printer/smt2/smt2_printer.cpp | 6 ++---- src/util/result.cpp | 2 +- src/util/sexpr.cpp | 2 +- 11 files changed, 33 insertions(+), 33 deletions(-) diff --git a/src/options/language.cpp b/src/options/language.cpp index 52263567b..885549b43 100644 --- a/src/options/language.cpp +++ b/src/options/language.cpp @@ -70,12 +70,12 @@ bool isOutputLang_smt2_6(OutputLanguage lang, bool exact) bool isInputLangSygus(InputLanguage lang) { - return lang == input::LANG_SYGUS || lang == input::LANG_SYGUS_V2; + return lang == input::LANG_SYGUS_V1 || lang == input::LANG_SYGUS_V2; } bool isOutputLangSygus(OutputLanguage lang) { - return lang == output::LANG_SYGUS || lang == output::LANG_SYGUS_V2; + return lang == output::LANG_SYGUS_V1 || lang == output::LANG_SYGUS_V2; } InputLanguage toInputLanguage(OutputLanguage language) { @@ -86,7 +86,7 @@ InputLanguage toInputLanguage(OutputLanguage language) { case output::LANG_TPTP: case output::LANG_CVC4: case output::LANG_Z3STR: - case output::LANG_SYGUS: + case output::LANG_SYGUS_V1: case output::LANG_SYGUS_V2: // these entries directly correspond (by design) return InputLanguage(int(language)); @@ -108,7 +108,7 @@ OutputLanguage toOutputLanguage(InputLanguage language) { case input::LANG_TPTP: case input::LANG_CVC4: case input::LANG_Z3STR: - case input::LANG_SYGUS: + case input::LANG_SYGUS_V1: case input::LANG_SYGUS_V2: // these entries directly correspond (by design) return OutputLanguage(int(language)); @@ -155,10 +155,13 @@ OutputLanguage toOutputLanguage(std::string language) { } else if(language == "z3str" || language == "z3-str" || language == "LANG_Z3STR") { return output::LANG_Z3STR; - } else if(language == "sygus" || language == "LANG_SYGUS") { - return output::LANG_SYGUS; } - else if (language == "sygus2" || language == "LANG_SYGUS_V2") + else if (language == "sygus1" || language == "LANG_SYGUS_V1") + { + return output::LANG_SYGUS_V1; + } + else if (language == "sygus" || language == "LANG_SYGUS" + || language == "sygus2" || language == "LANG_SYGUS_V2") { return output::LANG_SYGUS_V2; } @@ -195,8 +198,10 @@ InputLanguage toInputLanguage(std::string language) { } else if(language == "z3str" || language == "z3-str" || language == "LANG_Z3STR") { return input::LANG_Z3STR; - } else if(language == "sygus" || language == "LANG_SYGUS") { - return input::LANG_SYGUS; + } + else if (language == "sygus1" || language == "LANG_SYGUS_V1") + { + return input::LANG_SYGUS_V1; } else if (language == "sygus2" || language == "LANG_SYGUS_V2") { diff --git a/src/options/language.h b/src/options/language.h index 7866becd3..d0bdc6e77 100644 --- a/src/options/language.h +++ b/src/options/language.h @@ -58,8 +58,8 @@ enum CVC4_PUBLIC Language LANG_CVC4, /** The Z3-str input language */ LANG_Z3STR, - /** The SyGuS input language */ - LANG_SYGUS, + /** The SyGuS input language version 1.0 */ + LANG_SYGUS_V1, /** The SyGuS input language version 2.0 */ LANG_SYGUS_V2, @@ -94,9 +94,7 @@ inline std::ostream& operator<<(std::ostream& out, Language lang) { case LANG_Z3STR: out << "LANG_Z3STR"; break; - case LANG_SYGUS: - out << "LANG_SYGUS"; - break; + case LANG_SYGUS_V1: out << "LANG_SYGUS_V1"; break; case LANG_SYGUS_V2: out << "LANG_SYGUS_V2"; break; default: out << "undefined_input_language"; @@ -136,8 +134,8 @@ enum CVC4_PUBLIC Language LANG_CVC4 = input::LANG_CVC4, /** The Z3-str output language */ LANG_Z3STR = input::LANG_Z3STR, - /** The sygus output language */ - LANG_SYGUS = input::LANG_SYGUS, + /** The sygus output language version 1.0 */ + LANG_SYGUS_V1 = input::LANG_SYGUS_V1, /** The sygus output language version 2.0 */ LANG_SYGUS_V2 = input::LANG_SYGUS_V2, @@ -172,9 +170,7 @@ inline std::ostream& operator<<(std::ostream& out, Language lang) { case LANG_Z3STR: out << "LANG_Z3STR"; break; - case LANG_SYGUS: - out << "LANG_SYGUS"; - break; + case LANG_SYGUS_V1: out << "LANG_SYGUS_V1"; break; case LANG_SYGUS_V2: out << "LANG_SYGUS_V2"; break; case LANG_AST: out << "LANG_AST"; diff --git a/src/options/language.i b/src/options/language.i index acda19aec..639cb0bda 100644 --- a/src/options/language.i +++ b/src/options/language.i @@ -27,7 +27,7 @@ namespace CVC4 { %rename(INPUT_LANG_CVC4) CVC4::language::input::LANG_CVC4; %rename(INPUT_LANG_MAX) CVC4::language::input::LANG_MAX; %rename(INPUT_LANG_Z3STR) CVC4::language::input::LANG_Z3STR; -%rename(INPUT_LANG_SYGUS) CVC4::language::input::LANG_SYGUS; +%rename(INPUT_LANG_SYGUS_V1) CVC4::language::input::LANG_SYGUS_V1; %rename(INPUT_LANG_SYGUS_V2) CVC4::language::input::LANG_SYGUS_V2; %rename(OUTPUT_LANG_AUTO) CVC4::language::output::LANG_AUTO; @@ -40,7 +40,7 @@ namespace CVC4 { %rename(OUTPUT_LANG_AST) CVC4::language::output::LANG_AST; %rename(OUTPUT_LANG_MAX) CVC4::language::output::LANG_MAX; %rename(OUTPUT_LANG_Z3STR) CVC4::language::output::LANG_Z3STR; -%rename(OUTPUT_LANG_SYGUS) CVC4::language::output::LANG_SYGUS; +%rename(OUTPUT_LANG_SYGUS_V1) CVC4::language::output::LANG_SYGUS_V1; %rename(OUTPUT_LANG_SYGUS_V2) CVC4::language::output::LANG_SYGUS_V2; %include "options/language.h" diff --git a/src/options/options_template.cpp b/src/options/options_template.cpp index fe742adfc..a6489fcc4 100644 --- a/src/options/options_template.cpp +++ b/src/options/options_template.cpp @@ -418,7 +418,8 @@ Languages currently supported as arguments to the -L / --lang option:\n\ smt2.5 | smtlib2.5 SMT-LIB format 2.5\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\ + sygus1 SyGuS version 1.0 \n\ + sygus | sygus2 SyGuS version 2.0\n\ \n\ Languages currently supported as arguments to the --output-lang option:\n\ auto match output language to input language\n\ diff --git a/src/parser/antlr_input.cpp b/src/parser/antlr_input.cpp index 3157ab6e5..6dc26d439 100644 --- a/src/parser/antlr_input.cpp +++ b/src/parser/antlr_input.cpp @@ -247,7 +247,7 @@ AntlrInput* AntlrInput::newInput(InputLanguage lang, AntlrInputStream& inputStre break; } - case LANG_SYGUS: + case LANG_SYGUS_V1: case LANG_SYGUS_V2: input = new SygusInput(inputStream); break; case LANG_TPTP: diff --git a/src/parser/parser_builder.cpp b/src/parser/parser_builder.cpp index 28a965278..651dd560c 100644 --- a/src/parser/parser_builder.cpp +++ b/src/parser/parser_builder.cpp @@ -89,7 +89,7 @@ Parser* ParserBuilder::build() Parser* parser = NULL; switch (d_lang) { - case language::input::LANG_SYGUS: + case language::input::LANG_SYGUS_V1: case language::input::LANG_SYGUS_V2: parser = new Smt2(d_solver, input, d_strictMode, d_parseOnly); break; diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index 3c30f5c49..437f5aa2f 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -743,13 +743,13 @@ Command* Smt2::setLogic(std::string name, bool fromCommand) bool Smt2::sygus() const { InputLanguage ilang = getLanguage(); - return ilang == language::input::LANG_SYGUS + return ilang == language::input::LANG_SYGUS_V1 || ilang == language::input::LANG_SYGUS_V2; } bool Smt2::sygus_v1() const { - return getLanguage() == language::input::LANG_SYGUS; + return getLanguage() == language::input::LANG_SYGUS_V1; } bool Smt2::sygus_v2() const diff --git a/src/printer/printer.cpp b/src/printer/printer.cpp index 085a32c43..f8d62a8be 100644 --- a/src/printer/printer.cpp +++ b/src/printer/printer.cpp @@ -56,7 +56,7 @@ unique_ptr Printer::makePrinter(OutputLanguage lang) return unique_ptr( new printer::smt2::Smt2Printer(printer::smt2::z3str_variant)); - case LANG_SYGUS: + case LANG_SYGUS_V1: return unique_ptr( new printer::smt2::Smt2Printer(printer::smt2::sygus_variant)); diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index fbccd26ed..9edc73acd 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -2276,11 +2276,9 @@ static OutputLanguage variantToLanguage(Variant variant) return language::output::LANG_SMTLIB_V2_0; case z3str_variant: return language::output::LANG_Z3STR; - case sygus_variant: - return language::output::LANG_SYGUS; + case sygus_variant: return language::output::LANG_SYGUS_V1; case no_variant: - default: - return language::output::LANG_SMTLIB_V2_5; + default: return language::output::LANG_SMTLIB_V2_6; } } diff --git a/src/util/result.cpp b/src/util/result.cpp index 916e16b4f..01d5b052e 100644 --- a/src/util/result.cpp +++ b/src/util/result.cpp @@ -374,7 +374,7 @@ void Result::toStreamTptp(std::ostream& out) const { void Result::toStream(std::ostream& out, OutputLanguage language) const { switch (language) { - case language::output::LANG_SYGUS: + case language::output::LANG_SYGUS_V1: case language::output::LANG_SYGUS_V2: toStreamSmt2(out); break; case language::output::LANG_TPTP: toStreamTptp(out); diff --git a/src/util/sexpr.cpp b/src/util/sexpr.cpp index b2dcbbc8e..24ec700bc 100644 --- a/src/util/sexpr.cpp +++ b/src/util/sexpr.cpp @@ -272,7 +272,7 @@ void SExpr::toStreamRec(std::ostream& out, const SExpr& sexpr, bool SExpr::languageQuotesKeywords(OutputLanguage language) { switch (language) { - case language::output::LANG_SYGUS: + case language::output::LANG_SYGUS_V1: case language::output::LANG_TPTP: return true; case language::output::LANG_AST: -- 2.30.2