From: Aina Niemetz Date: Tue, 20 Apr 2021 20:25:10 +0000 (-0700) Subject: Remove support for CVC3 language. (#6369) X-Git-Tag: cvc5-1.0.0~1880 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=eee194ba0e228d28aa8bdd40a360b98fc3d0613f;p=cvc5.git Remove support for CVC3 language. (#6369) --- diff --git a/examples/api/combination.cpp b/examples/api/combination.cpp index c4b99a56a..d47897a7c 100644 --- a/examples/api/combination.cpp +++ b/examples/api/combination.cpp @@ -10,7 +10,7 @@ * directory for licensing information. * **************************************************************************** * - * A simple demonstration of the capabilities of CVC4 + * A simple demonstration of the capabilities of cvc5 * * A simple demonstration of how to use uninterpreted functions, combining this * with arithmetic, and extracting a model at the end of a satisfiable query. @@ -38,7 +38,7 @@ int main() { Solver slv; slv.setOption("produce-models", "true"); // Produce Models - slv.setOption("output-language", "cvc4"); // Set the output-language to CVC's + slv.setOption("output-language", "cvc"); // Set the output-language to CVC's slv.setOption("dag-thresh", "0"); // Disable dagifying the output slv.setOption("output-language", "smt2"); // use smt-lib v2 as output language slv.setLogic(string("QF_UFLIRA")); @@ -84,13 +84,13 @@ int main() << assertions << endl << endl; cout << "Prove x /= y is entailed. " << endl - << "CVC4: " << slv.checkEntailed(slv.mkTerm(DISTINCT, x, y)) << "." + << "cvc5: " << slv.checkEntailed(slv.mkTerm(DISTINCT, x, y)) << "." << endl << endl; cout << "Call checkSat to show that the assertions are satisfiable. " << endl - << "CVC4: " + << "cvc5: " << slv.checkSat() << "."<< endl << endl; cout << "Call slv.getValue(...) on terms of interest." diff --git a/examples/api/python/combination.py b/examples/api/python/combination.py index eb40f6ba3..adeba3a3c 100644 --- a/examples/api/python/combination.py +++ b/examples/api/python/combination.py @@ -27,7 +27,7 @@ def prefixPrintGetValue(slv, t, level=0): if __name__ == "__main__": slv = pycvc4.Solver() slv.setOption("produce-models", "true") # Produce Models - slv.setOption("output-language", "cvc4") # Set the output-language to CVC's + slv.setOption("output-language", "cvc") # Set the output-language to CVC's slv.setOption("dag-thresh", "0") # Disable dagifying the output slv.setOption("output-language", "smt2") # use smt-lib v2 as output language slv.setLogic("QF_UFLIRA") @@ -71,11 +71,11 @@ if __name__ == "__main__": slv.assertFormula(assertions) print("Given the following assertions:", assertions, "\n") - print("Prove x /= y is entailed.\nCVC4: ", + print("Prove x /= y is entailed.\ncvc5: ", slv.checkEntailed(slv.mkTerm(kinds.Distinct, x, y)), "\n") print("Call checkSat to show that the assertions are satisfiable") - print("CVC4:", slv.checkSat(), "\n") + print("cvc5:", slv.checkSat(), "\n") print("Call slv.getValue(...) on terms of interest") print("slv.getValue({}): {}".format(f_x, slv.getValue(f_x))) diff --git a/src/options/language.cpp b/src/options/language.cpp index 13384164a..bf17e91f9 100644 --- a/src/options/language.cpp +++ b/src/options/language.cpp @@ -111,23 +111,22 @@ OutputLanguage toOutputLanguage(InputLanguage language) { }/* switch(language) */ }/* toOutputLanguage() */ -OutputLanguage toOutputLanguage(std::string language) { - if (language == "cvc4" || language == "pl" || language == "presentation" +OutputLanguage toOutputLanguage(std::string language) +{ + if (language == "cvc" || language == "pl" || language == "presentation" || language == "native" || language == "LANG_CVC") { return output::LANG_CVC; } - else if (language == "cvc3" || language == "LANG_CVC3") - { - return output::LANG_CVC3; - } else if (language == "smtlib" || language == "smt" || language == "smtlib2" || language == "smt2" || language == "smtlib2.6" || language == "smt2.6" || language == "LANG_SMTLIB_V2_6" || language == "LANG_SMTLIB_V2") { return output::LANG_SMTLIB_V2_6; - } else if(language == "tptp" || language == "LANG_TPTP") { + } + else if (language == "tptp" || language == "LANG_TPTP") + { return output::LANG_TPTP; } else if (language == "sygus" || language == "LANG_SYGUS" @@ -144,11 +143,12 @@ OutputLanguage toOutputLanguage(std::string language) { return output::LANG_AUTO; } - throw OptionException(std::string("unknown output language `" + language + "'")); -}/* toOutputLanguage() */ + throw OptionException( + std::string("unknown output language `" + language + "'")); +} InputLanguage toInputLanguage(std::string language) { - if (language == "cvc4" || language == "pl" || language == "presentation" + if (language == "cvc" || language == "pl" || language == "presentation" || language == "native" || language == "LANG_CVC") { return input::LANG_CVC; diff --git a/src/options/language.h b/src/options/language.h index 413ef59ed..54e0e9dfa 100644 --- a/src/options/language.h +++ b/src/options/language.h @@ -114,8 +114,6 @@ enum CVC4_EXPORT Language /** The AST output language */ LANG_AST = 10, - /** The CVC3-compatibility output language */ - LANG_CVC3, /** LANG_MAX is > any valid OutputLanguage id */ LANG_MAX @@ -133,9 +131,6 @@ inline std::ostream& operator<<(std::ostream& out, Language lang) { case LANG_AST: out << "LANG_AST"; break; - case LANG_CVC3: - out << "LANG_CVC3"; - break; default: out << "undefined_output_language"; } diff --git a/src/options/options_template.cpp b/src/options/options_template.cpp index c06a7aab3..91d06dec2 100644 --- a/src/options/options_template.cpp +++ b/src/options/options_template.cpp @@ -290,7 +290,7 @@ 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 cvc5 presentation language\n\ + cvc | presentation | pl CVC presentation language\n\ smt | smtlib | smt2 |\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\ @@ -298,8 +298,7 @@ Languages currently supported as arguments to the -L / --lang option:\n\ \n\ Languages currently supported as arguments to the --output-lang option:\n\ auto match output language to input language\n\ - cvc4 | presentation | pl cvc5 presentation language\n\ - cvc3 CVC3 presentation language\n\ + cvc | presentation | pl CVC presentation language\n\ smt | smtlib | smt2 |\n\ smt2.6 | smtlib2.6 SMT-LIB format 2.6 with support for the strings standard\n\ tptp TPTP format\n\ diff --git a/src/printer/printer.cpp b/src/printer/printer.cpp index 6237c8744..6ab419b85 100644 --- a/src/printer/printer.cpp +++ b/src/printer/printer.cpp @@ -56,10 +56,6 @@ unique_ptr Printer::makePrinter(OutputLanguage lang) case LANG_AST: return unique_ptr(new printer::ast::AstPrinter()); - case LANG_CVC3: - return unique_ptr( - new printer::cvc::CvcPrinter(/* cvc3-mode = */ true)); - default: Unhandled() << lang; } } diff --git a/test/api/ouroborous.cpp b/test/api/ouroborous.cpp index 3f1fa6733..b51982d59 100644 --- a/test/api/ouroborous.cpp +++ b/test/api/ouroborous.cpp @@ -10,10 +10,10 @@ * directory for licensing information. * **************************************************************************** * - * "Ouroborous" test: does CVC4 read its own output? + * "Ouroborous" test: does cvc5 read its own output? * * The "Ouroborous" test, named after the serpent that swallows its - * own tail, ensures that CVC4 can parse some input, output it again + * own tail, ensures that cvc5 can parse some input, output it again * (in any of its languages) and then parse it again. The result of * the first parse must be equal to the result of the second parse; * both strings and expressions are compared for equality. @@ -57,7 +57,7 @@ int main() } catch (...) { - std::cerr << "non-cvc4 exception thrown" << std::endl; + std::cerr << "non-cvc5 exception thrown" << std::endl; } return 1; } @@ -66,8 +66,8 @@ std::string parse(std::string instr, std::string input_language, std::string output_language) { - assert(input_language == "smt2" || input_language == "cvc4"); - assert(output_language == "smt2" || output_language == "cvc4"); + assert(input_language == "smt2" || input_language == "cvc"); + assert(output_language == "smt2" || output_language == "cvc"); std::string declarations; @@ -125,8 +125,8 @@ std::string translate(std::string instr, std::string input_language, std::string output_language) { - assert(input_language == "smt2" || input_language == "cvc4"); - assert(output_language == "smt2" || output_language == "cvc4"); + assert(input_language == "smt2" || input_language == "cvc"); + assert(output_language == "smt2" || output_language == "cvc"); std::cout << "==============================================" << std::endl << "translating from " @@ -159,9 +159,9 @@ void runTestString(std::string instr, std::string instr_language) << " in language " << input::LANG_SMTLIB_V2 << std::endl; std::string smt2str = translate(instr, instr_language, "smt2"); std::cout << "in SMT2 : " << smt2str << std::endl; - std::string cvcstr = translate(smt2str, "smt2", "cvc4"); + std::string cvcstr = translate(smt2str, "smt2", "cvc"); std::cout << "in CVC : " << cvcstr << std::endl; - std::string outstr = translate(cvcstr, "cvc4", "smt2"); + std::string outstr = translate(cvcstr, "cvc", "smt2"); std::cout << "back to SMT2 : " << outstr << std::endl << std::endl; assert(outstr == smt2str); // differences in output @@ -170,8 +170,8 @@ void runTestString(std::string instr, std::string instr_language) int32_t runTest() { runTestString("(= (f (f y)) x)", "smt2"); - runTestString("~BVPLUS(3, 0bin00, 0bin11)[2:1] = 0bin10", "cvc4"); - runTestString("~BVPLUS(3, BVMULT(2, 0bin01, 0bin11), 0bin11)[2:0]", "cvc4"); - runTestString("a[x][y] = a[y][x]", "cvc4"); + runTestString("~BVPLUS(3, 0bin00, 0bin11)[2:1] = 0bin10", "cvc"); + runTestString("~BVPLUS(3, BVMULT(2, 0bin01, 0bin11), 0bin11)[2:0]", "cvc"); + runTestString("a[x][y] = a[y][x]", "cvc"); return 0; }