From 59bbcb5aa51b2ae9689e69afb05b017ee4fcb43a Mon Sep 17 00:00:00 2001 From: Haniel Barbosa Date: Tue, 15 Jun 2021 15:29:08 -0300 Subject: CVC4 -> cvc5 in cpp API examples (#6746) --- examples/api/cpp/bitvectors.cpp | 22 +++++++++++----------- examples/api/cpp/bitvectors_and_arrays.cpp | 6 +++--- examples/api/cpp/datatypes.cpp | 6 +++--- examples/api/cpp/extract.cpp | 4 ++-- examples/api/cpp/helloworld.cpp | 2 +- examples/api/cpp/linear_arith.cpp | 14 +++++++------- examples/api/cpp/sequences.cpp | 4 ++-- examples/api/cpp/sets.cpp | 6 +++--- examples/api/cpp/strings.cpp | 4 ++-- 9 files changed, 34 insertions(+), 34 deletions(-) diff --git a/examples/api/cpp/bitvectors.cpp b/examples/api/cpp/bitvectors.cpp index 8768bd996..51f438a2d 100644 --- a/examples/api/cpp/bitvectors.cpp +++ b/examples/api/cpp/bitvectors.cpp @@ -10,7 +10,7 @@ * directory for licensing information. * **************************************************************************** * - * A simple demonstration of the solving capabilities of the CVC4 + * A simple demonstration of the solving capabilities of the cvc5 * bit-vector solver. * */ @@ -43,7 +43,7 @@ int main() // //(2) x = a + b - x; // - // We will use CVC4 to prove that the three pieces of code above are all + // We will use cvc5 to prove that the three pieces of code above are all // equivalent by encoding the problem in the bit-vector theory. // Creating a bit-vector type of width 32 @@ -73,7 +73,7 @@ int main() Term assignment0 = slv.mkTerm(EQUAL, new_x, ite); // Assert the encoding of code (0) - cout << "Asserting " << assignment0 << " to CVC4 " << endl; + cout << "Asserting " << assignment0 << " to cvc5 " << endl; slv.assertFormula(assignment0); cout << "Pushing a new context." << endl; slv.push(); @@ -83,14 +83,14 @@ int main() Term a_xor_b_xor_x = slv.mkTerm(BITVECTOR_XOR, a, b, x); Term assignment1 = slv.mkTerm(EQUAL, new_x_, a_xor_b_xor_x); - // Assert encoding to CVC4 in current context; - cout << "Asserting " << assignment1 << " to CVC4 " << endl; + // Assert encoding to cvc5 in current context; + cout << "Asserting " << assignment1 << " to cvc5 " << endl; slv.assertFormula(assignment1); Term new_x_eq_new_x_ = slv.mkTerm(EQUAL, new_x, new_x_); cout << " Check entailment assuming: " << new_x_eq_new_x_ << endl; cout << " Expect ENTAILED. " << endl; - cout << " CVC4: " << slv.checkEntailed(new_x_eq_new_x_) << endl; + cout << " cvc5: " << slv.checkEntailed(new_x_eq_new_x_) << endl; cout << " Popping context. " << endl; slv.pop(); @@ -100,19 +100,19 @@ int main() Term a_plus_b_minus_x = slv.mkTerm(BITVECTOR_SUB, a_plus_b, x); Term assignment2 = slv.mkTerm(EQUAL, new_x_, a_plus_b_minus_x); - // Assert encoding to CVC4 in current context; - cout << "Asserting " << assignment2 << " to CVC4 " << endl; + // Assert encoding to cvc5 in current context; + cout << "Asserting " << assignment2 << " to cvc5 " << endl; slv.assertFormula(assignment2); cout << " Check entailment assuming: " << new_x_eq_new_x_ << endl; cout << " Expect ENTAILED. " << endl; - cout << " CVC4: " << slv.checkEntailed(new_x_eq_new_x_) << endl; + cout << " cvc5: " << slv.checkEntailed(new_x_eq_new_x_) << endl; Term x_neq_x = slv.mkTerm(EQUAL, x, x).notTerm(); std::vector v{new_x_eq_new_x_, x_neq_x}; cout << " Check entailment assuming: " << v << endl; cout << " Expect NOT_ENTAILED. " << endl; - cout << " CVC4: " << slv.checkEntailed(v) << endl; + cout << " cvc5: " << slv.checkEntailed(v) << endl; // Assert that a is odd Op extract_op = slv.mkOp(BITVECTOR_EXTRACT, 0, 0); @@ -123,6 +123,6 @@ int main() cout << "Check satisfiability." << endl; slv.assertFormula(a_odd); cout << " Expect sat. " << endl; - cout << " CVC4: " << slv.checkSat() << endl; + cout << " cvc5: " << slv.checkSat() << endl; return 0; } diff --git a/examples/api/cpp/bitvectors_and_arrays.cpp b/examples/api/cpp/bitvectors_and_arrays.cpp index 547b294a0..6b58daf1b 100644 --- a/examples/api/cpp/bitvectors_and_arrays.cpp +++ b/examples/api/cpp/bitvectors_and_arrays.cpp @@ -10,7 +10,7 @@ * directory for licensing information. * **************************************************************************** * - * A simple demonstration of the solving capabilities of the CVC4 + * A simple demonstration of the solving capabilities of the cvc5 * bit-vector and array solvers. * */ @@ -84,10 +84,10 @@ int main() Term query = slv.mkTerm(NOT, slv.mkTerm(AND, assertions)); - cout << "Asserting " << query << " to CVC4 " << endl; + cout << "Asserting " << query << " to cvc5 " << endl; slv.assertFormula(query); cout << "Expect sat. " << endl; - cout << "CVC4: " << slv.checkSatAssuming(slv.mkTrue()) << endl; + cout << "cvc5: " << slv.checkSatAssuming(slv.mkTrue()) << endl; // Getting the model cout << "The satisfying model is: " << endl; diff --git a/examples/api/cpp/datatypes.cpp b/examples/api/cpp/datatypes.cpp index 76c6da0f0..1ba9beaf1 100644 --- a/examples/api/cpp/datatypes.cpp +++ b/examples/api/cpp/datatypes.cpp @@ -10,7 +10,7 @@ * directory for licensing information. * **************************************************************************** * - * An example of using inductive datatypes in CVC4. + * An example of using inductive datatypes in cvc5. */ #include @@ -127,7 +127,7 @@ void test(Solver& slv, Sort& consListSort) std::cout << "Assert " << assertion << std::endl; slv.assertFormula(assertion); std::cout << "Expect sat." << std::endl; - std::cout << "CVC4: " << slv.checkSat() << std::endl; + std::cout << "cvc5: " << slv.checkSat() << std::endl; } int main() @@ -153,7 +153,7 @@ int main() std::cout << "spec is:" << std::endl << consListSpec << std::endl; // Keep in mind that "DatatypeDecl" is the specification class for - // datatypes---"DatatypeDecl" is not itself a CVC4 Sort. + // datatypes---"DatatypeDecl" is not itself a cvc5 Sort. // Now that our Datatype is fully specified, we can get a Sort for it. // This step resolves the "SelfSort" reference and creates // symbols for all the constructors, etc. diff --git a/examples/api/cpp/extract.cpp b/examples/api/cpp/extract.cpp index d21c59d59..b5de58d26 100644 --- a/examples/api/cpp/extract.cpp +++ b/examples/api/cpp/extract.cpp @@ -10,7 +10,7 @@ * directory for licensing information. * **************************************************************************** * - * A simple demonstration of the solving capabilities of the CVC4 + * A simple demonstration of the solving capabilities of the cvc5 * bit-vector solver. * */ @@ -50,7 +50,7 @@ int main() Term eq2 = slv.mkTerm(EQUAL, x_31_31, x_0_0); cout << " Check entailment assuming: " << eq2 << endl; cout << " Expect ENTAILED. " << endl; - cout << " CVC4: " << slv.checkEntailed(eq2) << endl; + cout << " cvc5: " << slv.checkEntailed(eq2) << endl; return 0; } diff --git a/examples/api/cpp/helloworld.cpp b/examples/api/cpp/helloworld.cpp index 21eb8e8fc..3d11d1bd0 100644 --- a/examples/api/cpp/helloworld.cpp +++ b/examples/api/cpp/helloworld.cpp @@ -10,7 +10,7 @@ * directory for licensing information. * **************************************************************************** * - * A very simple CVC4 example. + * A very simple cvc5 example. */ #include diff --git a/examples/api/cpp/linear_arith.cpp b/examples/api/cpp/linear_arith.cpp index 02ddd956c..979959d21 100644 --- a/examples/api/cpp/linear_arith.cpp +++ b/examples/api/cpp/linear_arith.cpp @@ -11,7 +11,7 @@ * **************************************************************************** * * A simple demonstration of the linear arithmetic solving capabilities and - * the push pop of CVC4. This also gives an example option. + * the push pop of cvc5. This also gives an example option. */ #include @@ -60,9 +60,9 @@ int main() slv.push(); Term diff_leq_two_thirds = slv.mkTerm(LEQ, diff, two_thirds); - cout << "Prove that " << diff_leq_two_thirds << " with CVC4." << endl; - cout << "CVC4 should report ENTAILED." << endl; - cout << "Result from CVC4 is: " << slv.checkEntailed(diff_leq_two_thirds) + cout << "Prove that " << diff_leq_two_thirds << " with cvc5." << endl; + cout << "cvc5 should report ENTAILED." << endl; + cout << "Result from cvc5 is: " << slv.checkEntailed(diff_leq_two_thirds) << endl; slv.pop(); @@ -72,9 +72,9 @@ int main() Term diff_is_two_thirds = slv.mkTerm(EQUAL, diff, two_thirds); slv.assertFormula(diff_is_two_thirds); cout << "Show that the assertions are consistent with " << endl; - cout << diff_is_two_thirds << " with CVC4." << endl; - cout << "CVC4 should report SAT." << endl; - cout << "Result from CVC4 is: " << slv.checkSat() << endl; + cout << diff_is_two_thirds << " with cvc5." << endl; + cout << "cvc5 should report SAT." << endl; + cout << "Result from cvc5 is: " << slv.checkSat() << endl; slv.pop(); cout << "Thus the maximum value of (y - x) is 2/3."<< endl; diff --git a/examples/api/cpp/sequences.cpp b/examples/api/cpp/sequences.cpp index 5ee66048f..40cacf5c7 100644 --- a/examples/api/cpp/sequences.cpp +++ b/examples/api/cpp/sequences.cpp @@ -10,7 +10,7 @@ * directory for licensing information. * **************************************************************************** * - * A simple demonstration of reasoning about sequences with CVC4 via C++ API. + * A simple demonstration of reasoning about sequences with cvc5 via C++ API. */ #include @@ -57,7 +57,7 @@ int main() // check sat Result result = slv.checkSatAssuming(q); - std::cout << "CVC4 reports: " << q << " is " << result << "." << std::endl; + std::cout << "cvc5 reports: " << q << " is " << result << "." << std::endl; if (result.isSat()) { diff --git a/examples/api/cpp/sets.cpp b/examples/api/cpp/sets.cpp index c1eded4a4..1f3a1683c 100644 --- a/examples/api/cpp/sets.cpp +++ b/examples/api/cpp/sets.cpp @@ -51,7 +51,7 @@ int main() Term theorem = slv.mkTerm(EQUAL, lhs, rhs); - cout << "CVC4 reports: " << theorem << " is " << slv.checkEntailed(theorem) + cout << "cvc5 reports: " << theorem << " is " << slv.checkEntailed(theorem) << "." << endl; } @@ -62,7 +62,7 @@ int main() Term theorem = slv.mkTerm(SUBSET, emptyset, A); - cout << "CVC4 reports: " << theorem << " is " << slv.checkEntailed(theorem) + cout << "cvc5 reports: " << theorem << " is " << slv.checkEntailed(theorem) << "." << endl; } @@ -84,7 +84,7 @@ int main() Term e = slv.mkTerm(MEMBER, x, intersection); Result result = slv.checkSatAssuming(e); - cout << "CVC4 reports: " << e << " is " << result << "." << endl; + cout << "cvc5 reports: " << e << " is " << result << "." << endl; if (result.isSat()) { diff --git a/examples/api/cpp/strings.cpp b/examples/api/cpp/strings.cpp index a952b31d1..01e384ee7 100644 --- a/examples/api/cpp/strings.cpp +++ b/examples/api/cpp/strings.cpp @@ -10,7 +10,7 @@ * directory for licensing information. * **************************************************************************** * - * A simple demonstration of reasoning about strings with CVC4 via C++ API. + * A simple demonstration of reasoning about strings with cvc5 via C++ API. */ #include @@ -84,7 +84,7 @@ int main() // check sat Result result = slv.checkSatAssuming(q); - std::cout << "CVC4 reports: " << q << " is " << result << "." << std::endl; + std::cout << "cvc5 reports: " << q << " is " << result << "." << std::endl; if(result.isSat()) { -- cgit v1.2.3