From 02b88b7665df5a6b1a2bce231d7567efdcc4b20a Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Tue, 19 May 2020 14:51:19 -0500 Subject: 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 ++- 4 files changed, 24 insertions(+), 22 deletions(-) (limited to 'src/options') 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\ -- cgit v1.2.3