summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--examples/api/combination.cpp8
-rw-r--r--examples/api/python/combination.py6
-rw-r--r--src/options/language.cpp20
-rw-r--r--src/options/language.h5
-rw-r--r--src/options/options_template.cpp5
-rw-r--r--src/printer/printer.cpp4
-rw-r--r--test/api/ouroborous.cpp24
7 files changed, 31 insertions, 41 deletions
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> Printer::makePrinter(OutputLanguage lang)
case LANG_AST:
return unique_ptr<Printer>(new printer::ast::AstPrinter());
- case LANG_CVC3:
- return unique_ptr<Printer>(
- 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;
}
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback