New C++: Remove redundant mkVar function.

s

8 files changed, 24 insertions, 24 deletions

diff --git a/examples/api/bitvectors-new.cpp b/examples/api/bitvectors-new.cpp
index 7070f6748..102cc2314 100644
--- a/examples/api/bitvectors-new.cpp
+++ b/examples/api/bitvectors-new.cpp
@@ -50,9 +50,9 @@ int main()
   Sort bitvector32 = slv.mkBitVectorSort(32);
 
   // Variables
-  Term x = slv.mkVar("x", bitvector32);
-  Term a = slv.mkVar("a", bitvector32);
-  Term b = slv.mkVar("b", bitvector32);
+  Term x = slv.mkVar(bitvector32, "x");
+  Term a = slv.mkVar(bitvector32, "a");
+  Term b = slv.mkVar(bitvector32, "b");
 
   // First encode the assumption that x must be equal to a or b
   Term x_eq_a = slv.mkTerm(EQUAL, x, a);
@@ -63,9 +63,9 @@ int main()
   slv.assertFormula(assumption);
 
   // Introduce a new variable for the new value of x after assignment.
-  Term new_x = slv.mkVar("new_x", bitvector32);  // x after executing code (0)
+  Term new_x = slv.mkVar(bitvector32, "new_x");  // x after executing code (0)
   Term new_x_ =
-      slv.mkVar("new_x_", bitvector32);  // x after executing code (1) or (2)
+      slv.mkVar(bitvector32, "new_x_");  // x after executing code (1) or (2)
 
   // Encoding code (0)
   // new_x = x == a ? b : a;
diff --git a/examples/api/bitvectors_and_arrays-new.cpp b/examples/api/bitvectors_and_arrays-new.cpp
index 3d4e6bca0..294cf66c0 100644
--- a/examples/api/bitvectors_and_arrays-new.cpp
+++ b/examples/api/bitvectors_and_arrays-new.cpp
@@ -52,7 +52,7 @@ int main()
   Sort arraySort = slv.mkArraySort(indexSort, elementSort);
 
   // Variables
-  Term current_array = slv.mkVar("current_array", arraySort);
+  Term current_array = slv.mkVar(arraySort, "current_array");
 
   // Making a bit-vector constant
   Term zero = slv.mkBitVector(index_size, 0u);
diff --git a/examples/api/combination-new.cpp b/examples/api/combination-new.cpp
index 8c968c95e..24ed32ad5 100644
--- a/examples/api/combination-new.cpp
+++ b/examples/api/combination-new.cpp
@@ -51,12 +51,12 @@ int main()
   Sort intPred = slv.mkFunctionSort(integer, boolean);
 
   // Variables
-  Term x = slv.mkVar("x", u);
-  Term y = slv.mkVar("y", u);
+  Term x = slv.mkVar(u, "x");
+  Term y = slv.mkVar(u, "y");
 
   // Functions
-  Term f = slv.mkVar("f", uToInt);
-  Term p = slv.mkVar("p", intPred);
+  Term f = slv.mkVar(uToInt, "f");
+  Term p = slv.mkVar(intPred, "p");
 
   // Constants
   Term zero = slv.mkReal(0);
diff --git a/examples/api/extract-new.cpp b/examples/api/extract-new.cpp
index 96961458e..05be327b9 100644
--- a/examples/api/extract-new.cpp
+++ b/examples/api/extract-new.cpp
@@ -29,7 +29,7 @@ int main()
 
   Sort bitvector32 = slv.mkBitVectorSort(32);
 
-  Term x = slv.mkVar("a", bitvector32);
+  Term x = slv.mkVar(bitvector32, "a");
 
   OpTerm ext_31_1 = slv.mkOpTerm(BITVECTOR_EXTRACT_OP, 31, 1);
   Term x_31_1 = slv.mkTerm(BITVECTOR_EXTRACT, ext_31_1, x);
diff --git a/examples/api/helloworld-new.cpp b/examples/api/helloworld-new.cpp
index 484995143..3e3c7426b 100644
--- a/examples/api/helloworld-new.cpp
+++ b/examples/api/helloworld-new.cpp
@@ -24,7 +24,7 @@ using namespace CVC4::api;
 int main()
 {
   Solver slv;
-  Term helloworld = slv.mkVar("Hello World!", slv.getBooleanSort());
+  Term helloworld = slv.mkVar(slv.getBooleanSort(), "Hello World!");
   std::cout << helloworld << " is " << slv.checkValidAssuming(helloworld)
             << std::endl;
   return 0;
diff --git a/examples/api/linear_arith-new.cpp b/examples/api/linear_arith-new.cpp
index d643b85bc..c194458ae 100644
--- a/examples/api/linear_arith-new.cpp
+++ b/examples/api/linear_arith-new.cpp
@@ -36,8 +36,8 @@ int main()
   Sort integer = slv.getIntegerSort();
 
   // Variables
-  Term x = slv.mkVar("x", integer);
-  Term y = slv.mkVar("y", real);
+  Term x = slv.mkVar(integer, "x");
+  Term y = slv.mkVar(real, "y");
 
   // Constants
   Term three = slv.mkReal(3);
diff --git a/examples/api/sets-new.cpp b/examples/api/sets-new.cpp
index 2dcfbbc02..95e1aa175 100644
--- a/examples/api/sets-new.cpp
+++ b/examples/api/sets-new.cpp
@@ -40,9 +40,9 @@ int main()
   // Verify union distributions over intersection
   // (A union B) intersection C = (A intersection C) union (B intersection C)
   {
-    Term A = slv.mkVar("A", set);
-    Term B = slv.mkVar("B", set);
-    Term C = slv.mkVar("C", set);
+    Term A = slv.mkVar(set, "A");
+    Term B = slv.mkVar(set, "B");
+    Term C = slv.mkVar(set, "C");
 
     Term unionAB = slv.mkTerm(UNION, A, B);
     Term lhs = slv.mkTerm(INTERSECTION, unionAB, C);
@@ -59,7 +59,7 @@ int main()
 
   // Verify emptset is a subset of any set
   {
-    Term A = slv.mkVar("A", set);
+    Term A = slv.mkVar(set, "A");
     Term emptyset = slv.mkEmptySet(set);
 
     Term theorem = slv.mkTerm(SUBSET, emptyset, A);
@@ -81,7 +81,7 @@ int main()
     Term two_three = slv.mkTerm(UNION, singleton_two, singleton_three);
     Term intersection = slv.mkTerm(INTERSECTION, one_two, two_three);
 
-    Term x = slv.mkVar("x", integer);
+    Term x = slv.mkVar(integer, "x");
 
     Term e = slv.mkTerm(MEMBER, x, intersection);
 
diff --git a/examples/api/strings-new.cpp b/examples/api/strings-new.cpp
index c88ccc9c0..d5f4312cd 100644
--- a/examples/api/strings-new.cpp
+++ b/examples/api/strings-new.cpp
@@ -43,9 +43,9 @@ int main()
   Term ab  = slv.mkString(str_ab);
   Term abc = slv.mkString("abc");
   // String variables
-  Term x = slv.mkVar("x", string);
-  Term y = slv.mkVar("y", string);
-  Term z = slv.mkVar("z", string);
+  Term x = slv.mkVar(string, "x");
+  Term y = slv.mkVar(string, "y");
+  Term z = slv.mkVar(string, "z");
 
   // String concatenation: x.ab.y
   Term lhs = slv.mkTerm(STRING_CONCAT, x, ab, y);
@@ -70,8 +70,8 @@ int main()
     slv.mkTerm(STRING_TO_REGEXP, slv.mkString("h")));
 
   // String variables
-  Term s1 = slv.mkVar("s1", string);
-  Term s2 = slv.mkVar("s2", string);
+  Term s1 = slv.mkVar(string, "s1");
+  Term s2 = slv.mkVar(string, "s2");
   // String concatenation: s1.s2
   Term s = slv.mkTerm(STRING_CONCAT, s1, s2);