diff options
| author | Aina Niemetz <aina.niemetz@gmail.com> | 2021-04-20 13:25:10 -0700 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-04-20 20:25:10 +0000 |
| commit | eee194ba0e228d28aa8bdd40a360b98fc3d0613f (patch) | |
| tree | 73013077dbfdf0cad49291abe851d1ed2cc54370 /examples/api | |
| parent | 54c3b8f716b4313f967c91ca9f55d2385a21e28c (diff) | |
Remove support for CVC3 language. (#6369)
Diffstat (limited to 'examples/api')
| -rw-r--r-- | examples/api/combination.cpp | 8 | ||||
| -rw-r--r-- | examples/api/python/combination.py | 6 |
2 files changed, 7 insertions, 7 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))) |