summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/options/language.cpp23
-rw-r--r--src/options/language.h16
-rw-r--r--src/options/language.i4
-rw-r--r--src/options/options_template.cpp3
-rw-r--r--src/parser/antlr_input.cpp2
-rw-r--r--src/parser/parser_builder.cpp2
-rw-r--r--src/parser/smt2/smt2.cpp4
-rw-r--r--src/printer/printer.cpp2
-rw-r--r--src/printer/smt2/smt2_printer.cpp6
-rw-r--r--src/util/result.cpp2
-rw-r--r--src/util/sexpr.cpp2
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> Printer::makePrinter(OutputLanguage lang)
return unique_ptr<Printer>(
new printer::smt2::Smt2Printer(printer::smt2::z3str_variant));
- case LANG_SYGUS:
+ case LANG_SYGUS_V1:
return unique_ptr<Printer>(
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:
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback