New C++ API: Clean up API: mkVar vs mkConst vs mkBoundVar. (#2977)

This cleans up naming of API functions to create first-order constants and variables.

mkVar -> mkConst
mkBoundVar -> mkVar
declareConst is redundant (= mkConst) and thus, in an effort to avoid redundancy, removed.

Note that we want to avoid redundancy in order to reduce code duplication and maintenance
overhead (we do not allow nested API calls, since this is problematic when tracing API calls).

8 files changed, 24 insertions, 24 deletions

diff --git a/examples/api/bitvectors-new.cpp b/examples/api/bitvectors-new.cpp
index 6aea56163..d0c26f134 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(bitvector32, "x");
-  Term a = slv.mkVar(bitvector32, "a");
-  Term b = slv.mkVar(bitvector32, "b");
+  Term x = slv.mkConst(bitvector32, "x");
+  Term a = slv.mkConst(bitvector32, "a");
+  Term b = slv.mkConst(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(bitvector32, "new_x");  // x after executing code (0)
+  Term new_x = slv.mkConst(bitvector32, "new_x");  // x after executing code (0)
   Term new_x_ =
-      slv.mkVar(bitvector32, "new_x_");  // x after executing code (1) or (2)
+      slv.mkConst(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 f0883d634..955a83cff 100644
--- a/examples/api/bitvectors_and_arrays-new.cpp
+++ b/examples/api/bitvectors_and_arrays-new.cpp
@@ -53,7 +53,7 @@ int main()
   Sort arraySort = slv.mkArraySort(indexSort, elementSort);
 
   // Variables
-  Term current_array = slv.mkVar(arraySort, "current_array");
+  Term current_array = slv.mkConst(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 a3ff4421f..e78e8919f 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(u, "x");
-  Term y = slv.mkVar(u, "y");
+  Term x = slv.mkConst(u, "x");
+  Term y = slv.mkConst(u, "y");
 
   // Functions
-  Term f = slv.mkVar(uToInt, "f");
-  Term p = slv.mkVar(intPred, "p");
+  Term f = slv.mkConst(uToInt, "f");
+  Term p = slv.mkConst(intPred, "p");
 
   // Constants
   Term zero = slv.mkReal(0);
diff --git a/examples/api/datatypes-new.cpp b/examples/api/datatypes-new.cpp
index c499fa111..08918fc87 100644
--- a/examples/api/datatypes-new.cpp
+++ b/examples/api/datatypes-new.cpp
@@ -116,7 +116,7 @@ void test(Solver& slv, Sort& consListSort)
     }
   }
 
-  Term a = slv.declareConst("a", paramConsIntListSort);
+  Term a = slv.mkConst(paramConsIntListSort, "a");
   std::cout << "term " << a << " is of sort " << a.getSort() << std::endl;
 
   Term head_a = slv.mkTerm(
diff --git a/examples/api/extract-new.cpp b/examples/api/extract-new.cpp
index aad9e0fb5..cb7d96fa5 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(bitvector32, "a");
+  Term x = slv.mkConst(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/linear_arith-new.cpp b/examples/api/linear_arith-new.cpp
index aae2fa67e..2edcaf71e 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(integer, "x");
-  Term y = slv.mkVar(real, "y");
+  Term x = slv.mkConst(integer, "x");
+  Term y = slv.mkConst(real, "y");
 
   // Constants
   Term three = slv.mkReal(3);
diff --git a/examples/api/sets-new.cpp b/examples/api/sets-new.cpp
index 6c0352302..60df7a82f 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(set, "A");
-    Term B = slv.mkVar(set, "B");
-    Term C = slv.mkVar(set, "C");
+    Term A = slv.mkConst(set, "A");
+    Term B = slv.mkConst(set, "B");
+    Term C = slv.mkConst(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(set, "A");
+    Term A = slv.mkConst(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(integer, "x");
+    Term x = slv.mkConst(integer, "x");
 
     Term e = slv.mkTerm(MEMBER, x, intersection);
 
diff --git a/examples/api/strings-new.cpp b/examples/api/strings-new.cpp
index a9c6dd491..42630dc0e 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(string, "x");
-  Term y = slv.mkVar(string, "y");
-  Term z = slv.mkVar(string, "z");
+  Term x = slv.mkConst(string, "x");
+  Term y = slv.mkConst(string, "y");
+  Term z = slv.mkConst(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(string, "s1");
-  Term s2 = slv.mkVar(string, "s2");
+  Term s1 = slv.mkConst(string, "s1");
+  Term s2 = slv.mkConst(string, "s2");
   // String concatenation: s1.s2
   Term s = slv.mkTerm(STRING_CONCAT, s1, s2);