From: Haniel Barbosa <hanielbbarbosa@gmail.com>
Date: Tue, 15 Jun 2021 18:29:08 +0000 (-0300)
Subject: CVC4 -> cvc5 in cpp API examples (#6746)
X-Git-Tag: cvc5-1.0.0~1602
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=59bbcb5aa51b2ae9689e69afb05b017ee4fcb43a;p=cvc5.git

CVC4 -> cvc5 in cpp API examples (#6746)
---

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<Term> 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 <cvc5/cvc5.h>
@@ -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 <cvc5/cvc5.h>
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 <iostream>
@@ -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 <cvc5/cvc5.h>
@@ -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 <cvc5/cvc5.h>
@@ -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())
   {