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).

diff --git a/examples/api/bitvectors-new.cpp b/examples/api/bitvectors-new.cpp
index 6aea561639a278b2228e5191298eb72b95962144..d0c26f13441f88687a7dc64e110038e40b9a693b 100644 (file)
--- 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 f0883d6345c804262512e3dcf575f20c8198b22c..955a83cffdf366bf5fd9c42cfff6a80d8cd2e9af 100644 (file)
--- 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 a3ff4421f052e81d5d46bae23988986e59f436ad..e78e8919f61eb5a6bca933de7b780b751ccaa235 100644 (file)
--- 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 c499fa111326e56661f4fad53ac014b1921b630a..08918fc87cc45cd49a6594818d1694bfa28d2b83 100644 (file)
--- 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 aad9e0fb59798e0eb9a32c3ba29f703a42c6da23..cb7d96fa5083f6f56ac53a7f67c7d8e4aa1054fb 100644 (file)
--- 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 aae2fa67ecb46e8caa9946c707fb1e6c22332e43..2edcaf71e6f7e31473e766f1347c418b422ff44d 100644 (file)
--- 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 6c0352302c35786235e2677095f11be8cc828e70..60df7a82fbf316f360ad313f2f87338ec040284e 100644 (file)
--- 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 a9c6dd49172b085756abbc37a15f59fc760db6d3..42630dc0ec30359fad31c25bd5a6ed9d4564b68e 100644 (file)
--- 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);
 

diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp
index 86072d601ee8bf50e4378504849280f9cba920c9..4cd9f49237cf1be97be1f6efe01d50a3794e25a8 100644 (file)
--- a/src/api/cvc4cpp.cpp
+++ b/src/api/cvc4cpp.cpp
@@ -56,8 +56,8 @@ const static std::unordered_map<Kind, CVC4::Kind, KindHashFunction> s_kinds{
     {APPLY, CVC4::Kind::APPLY},
     {EQUAL, CVC4::Kind::EQUAL},
     {DISTINCT, CVC4::Kind::DISTINCT},
-    {VARIABLE, CVC4::Kind::VARIABLE},
-    {BOUND_VARIABLE, CVC4::Kind::BOUND_VARIABLE},
+    {CONSTANT, CVC4::Kind::VARIABLE},
+    {VARIABLE, CVC4::Kind::BOUND_VARIABLE},
     {LAMBDA, CVC4::Kind::LAMBDA},
     {CHOICE, CVC4::Kind::CHOICE},
     {CHAIN, CVC4::Kind::CHAIN},
@@ -304,8 +304,8 @@ const static std::unordered_map<CVC4::Kind, Kind, CVC4::kind::KindHashFunction>
         {CVC4::Kind::APPLY, APPLY},
         {CVC4::Kind::EQUAL, EQUAL},
         {CVC4::Kind::DISTINCT, DISTINCT},
-        {CVC4::Kind::VARIABLE, VARIABLE},
-        {CVC4::Kind::BOUND_VARIABLE, BOUND_VARIABLE},
+        {CVC4::Kind::VARIABLE, CONSTANT},
+        {CVC4::Kind::BOUND_VARIABLE, VARIABLE},
         {CVC4::Kind::LAMBDA, LAMBDA},
         {CVC4::Kind::CHOICE, CHOICE},
         {CVC4::Kind::CHAIN, CHAIN},
@@ -1970,7 +1970,7 @@ Term Solver::mkPi() const
 }
 
 template <typename T>
-Term Solver::mkConstHelper(T t) const
+Term Solver::mkValHelper(T t) const
 {
   try
   {
@@ -1997,7 +1997,7 @@ Term Solver::mkRealFromStrHelper(std::string s) const
     CVC4::Rational r = s.find('/') != std::string::npos
                            ? CVC4::Rational(s)
                            : CVC4::Rational::fromDecimal(s);
-    return mkConstHelper<CVC4::Rational>(r);
+    return mkValHelper<CVC4::Rational>(r);
   }
   catch (const std::invalid_argument& e)
   {
@@ -2020,7 +2020,7 @@ Term Solver::mkReal(int32_t val) const
 {
   try
   {
-    return mkConstHelper<CVC4::Rational>(CVC4::Rational(val));
+    return mkValHelper<CVC4::Rational>(CVC4::Rational(val));
   }
   catch (const std::invalid_argument& e)
   {
@@ -2032,7 +2032,7 @@ Term Solver::mkReal(int64_t val) const
 {
   try
   {
-    return mkConstHelper<CVC4::Rational>(CVC4::Rational(val));
+    return mkValHelper<CVC4::Rational>(CVC4::Rational(val));
   }
   catch (const std::invalid_argument& e)
   {
@@ -2044,7 +2044,7 @@ Term Solver::mkReal(uint32_t val) const
 {
   try
   {
-    return mkConstHelper<CVC4::Rational>(CVC4::Rational(val));
+    return mkValHelper<CVC4::Rational>(CVC4::Rational(val));
   }
   catch (const std::invalid_argument& e)
   {
@@ -2056,7 +2056,7 @@ Term Solver::mkReal(uint64_t val) const
 {
   try
   {
-    return mkConstHelper<CVC4::Rational>(CVC4::Rational(val));
+    return mkValHelper<CVC4::Rational>(CVC4::Rational(val));
   }
   catch (const std::invalid_argument& e)
   {
@@ -2068,7 +2068,7 @@ Term Solver::mkReal(int32_t num, int32_t den) const
 {
   try
   {
-    return mkConstHelper<CVC4::Rational>(CVC4::Rational(num, den));
+    return mkValHelper<CVC4::Rational>(CVC4::Rational(num, den));
   }
   catch (const std::invalid_argument& e)
   {
@@ -2080,7 +2080,7 @@ Term Solver::mkReal(int64_t num, int64_t den) const
 {
   try
   {
-    return mkConstHelper<CVC4::Rational>(CVC4::Rational(num, den));
+    return mkValHelper<CVC4::Rational>(CVC4::Rational(num, den));
   }
   catch (const std::invalid_argument& e)
   {
@@ -2092,7 +2092,7 @@ Term Solver::mkReal(uint32_t num, uint32_t den) const
 {
   try
   {
-    return mkConstHelper<CVC4::Rational>(CVC4::Rational(num, den));
+    return mkValHelper<CVC4::Rational>(CVC4::Rational(num, den));
   }
   catch (const std::invalid_argument& e)
   {
@@ -2104,7 +2104,7 @@ Term Solver::mkReal(uint64_t num, uint64_t den) const
 {
   try
   {
-    return mkConstHelper<CVC4::Rational>(CVC4::Rational(num, den));
+    return mkValHelper<CVC4::Rational>(CVC4::Rational(num, den));
   }
   catch (const std::invalid_argument& e)
   {
@@ -2146,7 +2146,7 @@ Term Solver::mkEmptySet(Sort s) const
 {
   CVC4_API_ARG_CHECK_EXPECTED(s.isNull() || s.isSet(), s)
       << "null sort or set sort";
-  return mkConstHelper<CVC4::EmptySet>(CVC4::EmptySet(*s.d_type));
+  return mkValHelper<CVC4::EmptySet>(CVC4::EmptySet(*s.d_type));
 }
 
 Term Solver::mkSepNil(Sort sort) const
@@ -2166,22 +2166,22 @@ Term Solver::mkSepNil(Sort sort) const
 
 Term Solver::mkString(const char* s, bool useEscSequences) const
 {
-  return mkConstHelper<CVC4::String>(CVC4::String(s, useEscSequences));
+  return mkValHelper<CVC4::String>(CVC4::String(s, useEscSequences));
 }
 
 Term Solver::mkString(const std::string& s, bool useEscSequences) const
 {
-  return mkConstHelper<CVC4::String>(CVC4::String(s, useEscSequences));
+  return mkValHelper<CVC4::String>(CVC4::String(s, useEscSequences));
 }
 
 Term Solver::mkString(const unsigned char c) const
 {
-  return mkConstHelper<CVC4::String>(CVC4::String(std::string(1, c)));
+  return mkValHelper<CVC4::String>(CVC4::String(std::string(1, c)));
 }
 
 Term Solver::mkString(const std::vector<unsigned>& s) const
 {
-  return mkConstHelper<CVC4::String>(CVC4::String(s));
+  return mkValHelper<CVC4::String>(CVC4::String(s));
 }
 
 Term Solver::mkUniverseSet(Sort sort) const
@@ -2207,7 +2207,7 @@ Term Solver::mkBVFromIntHelper(uint32_t size, uint64_t val) const
   CVC4_API_ARG_CHECK_EXPECTED(size > 0, size) << "a bit-width > 0";
   try
   {
-    return mkConstHelper<CVC4::BitVector>(CVC4::BitVector(size, val));
+    return mkValHelper<CVC4::BitVector>(CVC4::BitVector(size, val));
   }
   catch (const std::invalid_argument& e)
   {
@@ -2228,7 +2228,7 @@ Term Solver::mkBVFromStrHelper(std::string s, uint32_t base) const
       << "base 2, 10, or 16";
   try
   {
-    return mkConstHelper<CVC4::BitVector>(CVC4::BitVector(s, base));
+    return mkValHelper<CVC4::BitVector>(CVC4::BitVector(s, base));
   }
   catch (const std::invalid_argument& e)
   {
@@ -2249,7 +2249,7 @@ Term Solver::mkBVFromStrHelper(uint32_t size,
     CVC4_API_CHECK(val.modByPow2(size) == val)
         << "Overflow in bitvector construction (specified bitvector size "
         << size << " too small to hold value " << s << ")";
-    return mkConstHelper<CVC4::BitVector>(CVC4::BitVector(size, val));
+    return mkValHelper<CVC4::BitVector>(CVC4::BitVector(size, val));
   }
   catch (const std::invalid_argument& e)
   {
@@ -2283,7 +2283,7 @@ Term Solver::mkPosInf(uint32_t exp, uint32_t sig) const
 {
   CVC4_API_CHECK(Configuration::isBuiltWithSymFPU())
       << "Expected CVC4 to be compiled with SymFPU support";
-  return mkConstHelper<CVC4::FloatingPoint>(
+  return mkValHelper<CVC4::FloatingPoint>(
       FloatingPoint::makeInf(FloatingPointSize(exp, sig), false));
 }
 
@@ -2291,7 +2291,7 @@ Term Solver::mkNegInf(uint32_t exp, uint32_t sig) const
 {
   CVC4_API_CHECK(Configuration::isBuiltWithSymFPU())
       << "Expected CVC4 to be compiled with SymFPU support";
-  return mkConstHelper<CVC4::FloatingPoint>(
+  return mkValHelper<CVC4::FloatingPoint>(
       FloatingPoint::makeInf(FloatingPointSize(exp, sig), true));
 }
 
@@ -2299,7 +2299,7 @@ Term Solver::mkNaN(uint32_t exp, uint32_t sig) const
 {
   CVC4_API_CHECK(Configuration::isBuiltWithSymFPU())
       << "Expected CVC4 to be compiled with SymFPU support";
-  return mkConstHelper<CVC4::FloatingPoint>(
+  return mkValHelper<CVC4::FloatingPoint>(
       FloatingPoint::makeNaN(FloatingPointSize(exp, sig)));
 }
 
@@ -2307,7 +2307,7 @@ Term Solver::mkPosZero(uint32_t exp, uint32_t sig) const
 {
   CVC4_API_CHECK(Configuration::isBuiltWithSymFPU())
       << "Expected CVC4 to be compiled with SymFPU support";
-  return mkConstHelper<CVC4::FloatingPoint>(
+  return mkValHelper<CVC4::FloatingPoint>(
       FloatingPoint::makeZero(FloatingPointSize(exp, sig), false));
 }
 
@@ -2315,19 +2315,19 @@ Term Solver::mkNegZero(uint32_t exp, uint32_t sig) const
 {
   CVC4_API_CHECK(Configuration::isBuiltWithSymFPU())
       << "Expected CVC4 to be compiled with SymFPU support";
-  return mkConstHelper<CVC4::FloatingPoint>(
+  return mkValHelper<CVC4::FloatingPoint>(
       FloatingPoint::makeZero(FloatingPointSize(exp, sig), true));
 }
 
 Term Solver::mkRoundingMode(RoundingMode rm) const
 {
-  return mkConstHelper<CVC4::RoundingMode>(s_rmodes.at(rm));
+  return mkValHelper<CVC4::RoundingMode>(s_rmodes.at(rm));
 }
 
 Term Solver::mkUninterpretedConst(Sort sort, int32_t index) const
 {
   CVC4_API_ARG_CHECK_EXPECTED(!sort.isNull(), sort) << "non-null sort";
-  return mkConstHelper<CVC4::UninterpretedConstant>(
+  return mkValHelper<CVC4::UninterpretedConstant>(
       CVC4::UninterpretedConstant(*sort.d_type, index));
 }
 
@@ -2385,14 +2385,14 @@ Term Solver::mkFloatingPoint(uint32_t exp, uint32_t sig, Term val) const
   CVC4_API_ARG_CHECK_EXPECTED(
       val.getSort().isBitVector() && val.d_expr->isConst(), val)
       << "bit-vector constant";
-  return mkConstHelper<CVC4::FloatingPoint>(
+  return mkValHelper<CVC4::FloatingPoint>(
       CVC4::FloatingPoint(exp, sig, val.d_expr->getConst<BitVector>()));
 }
 
-/* Create variables                                                           */
+/* Create constants                                                           */
 /* -------------------------------------------------------------------------- */
 
-Term Solver::mkVar(Sort sort, const std::string& symbol) const
+Term Solver::mkConst(Sort sort, const std::string& symbol) const
 {
   try
   {
@@ -2408,7 +2408,10 @@ Term Solver::mkVar(Sort sort, const std::string& symbol) const
   }
 }
 
-Term Solver::mkBoundVar(Sort sort, const std::string& symbol) const
+/* Create variables                                                           */
+/* -------------------------------------------------------------------------- */
+
+Term Solver::mkVar(Sort sort, const std::string& symbol) const
 {
   try
   {
@@ -2436,8 +2439,9 @@ void Solver::checkMkTerm(Kind kind, uint32_t nchildren) const
       mk == kind::metakind::PARAMETERIZED || mk == kind::metakind::OPERATOR,
       kind)
       << "Only operator-style terms are created with mkTerm(), "
-         "to create variables and constants see mkVar(), mkBoundVar(), "
-         "and mkConst().";
+         "to create variables, constants and values see mkVar(), mkConst() "
+         "and the respective theory-specific functions to create values, "
+         "e.g., mkBitVector().";
   CVC4_API_KIND_CHECK_EXPECTED(
       nchildren >= minArity(kind) && nchildren <= maxArity(kind), kind)
       << "Terms with kind " << kindToString(kind) << " must have at least "
@@ -2729,15 +2733,14 @@ std::vector<Expr> Solver::termVectorToExprs(
 OpTerm Solver::mkOpTerm(Kind kind, Kind k)
 {
   CVC4_API_KIND_CHECK_EXPECTED(kind == CHAIN_OP, kind) << "CHAIN_OP";
-  return *mkConstHelper<CVC4::Chain>(CVC4::Chain(extToIntKind(k))).d_expr.get();
+  return *mkValHelper<CVC4::Chain>(CVC4::Chain(extToIntKind(k))).d_expr.get();
 }
 
 OpTerm Solver::mkOpTerm(Kind kind, const std::string& arg)
 {
   CVC4_API_KIND_CHECK_EXPECTED(kind == RECORD_UPDATE_OP, kind)
       << "RECORD_UPDATE_OP";
-  return *mkConstHelper<CVC4::RecordUpdate>(CVC4::RecordUpdate(arg))
-              .d_expr.get();
+  return *mkValHelper<CVC4::RecordUpdate>(CVC4::RecordUpdate(arg)).d_expr.get();
 }
 
 OpTerm Solver::mkOpTerm(Kind kind, uint32_t arg)
@@ -2747,59 +2750,59 @@ OpTerm Solver::mkOpTerm(Kind kind, uint32_t arg)
   switch (kind)
   {
     case DIVISIBLE_OP:
-      res = *mkConstHelper<CVC4::Divisible>(CVC4::Divisible(arg)).d_expr.get();
+      res = *mkValHelper<CVC4::Divisible>(CVC4::Divisible(arg)).d_expr.get();
       break;
     case BITVECTOR_REPEAT_OP:
-      res = *mkConstHelper<CVC4::BitVectorRepeat>(CVC4::BitVectorRepeat(arg))
+      res = *mkValHelper<CVC4::BitVectorRepeat>(CVC4::BitVectorRepeat(arg))
                  .d_expr.get();
       break;
     case BITVECTOR_ZERO_EXTEND_OP:
-      res = *mkConstHelper<CVC4::BitVectorZeroExtend>(
+      res = *mkValHelper<CVC4::BitVectorZeroExtend>(
                  CVC4::BitVectorZeroExtend(arg))
                  .d_expr.get();
       break;
     case BITVECTOR_SIGN_EXTEND_OP:
-      res = *mkConstHelper<CVC4::BitVectorSignExtend>(
+      res = *mkValHelper<CVC4::BitVectorSignExtend>(
                  CVC4::BitVectorSignExtend(arg))
                  .d_expr.get();
       break;
     case BITVECTOR_ROTATE_LEFT_OP:
-      res = *mkConstHelper<CVC4::BitVectorRotateLeft>(
+      res = *mkValHelper<CVC4::BitVectorRotateLeft>(
                  CVC4::BitVectorRotateLeft(arg))
                  .d_expr.get();
       break;
     case BITVECTOR_ROTATE_RIGHT_OP:
-      res = *mkConstHelper<CVC4::BitVectorRotateRight>(
+      res = *mkValHelper<CVC4::BitVectorRotateRight>(
                  CVC4::BitVectorRotateRight(arg))
                  .d_expr.get();
       break;
     case INT_TO_BITVECTOR_OP:
-      res = *mkConstHelper<CVC4::IntToBitVector>(CVC4::IntToBitVector(arg))
+      res = *mkValHelper<CVC4::IntToBitVector>(CVC4::IntToBitVector(arg))
                  .d_expr.get();
       break;
     case FLOATINGPOINT_TO_UBV_OP:
-      res = *mkConstHelper<CVC4::FloatingPointToUBV>(
-                 CVC4::FloatingPointToUBV(arg))
-                 .d_expr.get();
+      res =
+          *mkValHelper<CVC4::FloatingPointToUBV>(CVC4::FloatingPointToUBV(arg))
+               .d_expr.get();
       break;
     case FLOATINGPOINT_TO_UBV_TOTAL_OP:
-      res = *mkConstHelper<CVC4::FloatingPointToUBVTotal>(
+      res = *mkValHelper<CVC4::FloatingPointToUBVTotal>(
                  CVC4::FloatingPointToUBVTotal(arg))
                  .d_expr.get();
       break;
     case FLOATINGPOINT_TO_SBV_OP:
-      res = *mkConstHelper<CVC4::FloatingPointToSBV>(
-                 CVC4::FloatingPointToSBV(arg))
-                 .d_expr.get();
+      res =
+          *mkValHelper<CVC4::FloatingPointToSBV>(CVC4::FloatingPointToSBV(arg))
+               .d_expr.get();
       break;
     case FLOATINGPOINT_TO_SBV_TOTAL_OP:
-      res = *mkConstHelper<CVC4::FloatingPointToSBVTotal>(
+      res = *mkValHelper<CVC4::FloatingPointToSBVTotal>(
                  CVC4::FloatingPointToSBVTotal(arg))
                  .d_expr.get();
       break;
     case TUPLE_UPDATE_OP:
-      res = *mkConstHelper<CVC4::TupleUpdate>(CVC4::TupleUpdate(arg))
-                 .d_expr.get();
+      res =
+          *mkValHelper<CVC4::TupleUpdate>(CVC4::TupleUpdate(arg)).d_expr.get();
       break;
     default:
       CVC4_API_KIND_CHECK_EXPECTED(false, kind)
@@ -2816,37 +2819,37 @@ OpTerm Solver::mkOpTerm(Kind kind, uint32_t arg1, uint32_t arg2)
   switch (kind)
   {
     case BITVECTOR_EXTRACT_OP:
-      res = *mkConstHelper<CVC4::BitVectorExtract>(
+      res = *mkValHelper<CVC4::BitVectorExtract>(
                  CVC4::BitVectorExtract(arg1, arg2))
                  .d_expr.get();
       break;
     case FLOATINGPOINT_TO_FP_IEEE_BITVECTOR_OP:
-      res = *mkConstHelper<CVC4::FloatingPointToFPIEEEBitVector>(
+      res = *mkValHelper<CVC4::FloatingPointToFPIEEEBitVector>(
                  CVC4::FloatingPointToFPIEEEBitVector(arg1, arg2))
                  .d_expr.get();
       break;
     case FLOATINGPOINT_TO_FP_FLOATINGPOINT_OP:
-      res = *mkConstHelper<CVC4::FloatingPointToFPFloatingPoint>(
+      res = *mkValHelper<CVC4::FloatingPointToFPFloatingPoint>(
                  CVC4::FloatingPointToFPFloatingPoint(arg1, arg2))
                  .d_expr.get();
       break;
     case FLOATINGPOINT_TO_FP_REAL_OP:
-      res = *mkConstHelper<CVC4::FloatingPointToFPReal>(
+      res = *mkValHelper<CVC4::FloatingPointToFPReal>(
                  CVC4::FloatingPointToFPReal(arg1, arg2))
                  .d_expr.get();
       break;
     case FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR_OP:
-      res = *mkConstHelper<CVC4::FloatingPointToFPSignedBitVector>(
+      res = *mkValHelper<CVC4::FloatingPointToFPSignedBitVector>(
                  CVC4::FloatingPointToFPSignedBitVector(arg1, arg2))
                  .d_expr.get();
       break;
     case FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR_OP:
-      res = *mkConstHelper<CVC4::FloatingPointToFPUnsignedBitVector>(
+      res = *mkValHelper<CVC4::FloatingPointToFPUnsignedBitVector>(
                  CVC4::FloatingPointToFPUnsignedBitVector(arg1, arg2))
                  .d_expr.get();
       break;
     case FLOATINGPOINT_TO_FP_GENERIC_OP:
-      res = *mkConstHelper<CVC4::FloatingPointToFPGeneric>(
+      res = *mkValHelper<CVC4::FloatingPointToFPGeneric>(
                  CVC4::FloatingPointToFPGeneric(arg1, arg2))
                  .d_expr.get();
       break;
@@ -2939,24 +2942,6 @@ Result Solver::checkSatAssuming(const std::vector<Term>& assumptions) const
   return Result(r);
 }
 
-/**
- *  ( declare-const <symbol> <sort> )
- */
-Term Solver::declareConst(const std::string& symbol, Sort sort) const
-{
-  try
-  {
-    CVC4_API_ARG_CHECK_EXPECTED(!sort.isNull(), sort) << "non-null sort";
-    Term res = d_exprMgr->mkVar(symbol, *sort.d_type);
-    (void)res.d_expr->getType(true); /* kick off type checking */
-    return res;
-  }
-  catch (const CVC4::TypeCheckingException& e)
-  {
-    throw CVC4ApiException(e.getMessage());
-  }
-}
-
 /**
  *  ( declare-datatype <symbol> <datatype_decl> )
  */

diff --git a/src/api/cvc4cpp.h b/src/api/cvc4cpp.h
index 203586066d995fae3126b3abce1d5f66d66bdaf5..c13c7919e1fd845870471061319f2fb9080e3cc4 100644 (file)
--- a/src/api/cvc4cpp.h
+++ b/src/api/cvc4cpp.h
@@ -2166,20 +2166,23 @@ class CVC4_PUBLIC Solver
   /* .................................................................... */
 
   /**
-   * Create variable.
-   * @param sort the sort of the variable
-   * @param symbol the name of the variable
-   * @return the variable
+   * Create (first-order) constant (0-arity function symbol).
+   * SMT-LIB: ( declare-const <symbol> <sort> )
+   * SMT-LIB: ( declare-fun <symbol> ( ) <sort> )
+   *
+   * @param sort the sort of the constant
+   * @param symbol the name of the constant
+   * @return the first-order constant
    */
-  Term mkVar(Sort sort, const std::string& symbol = std::string()) const;
+  Term mkConst(Sort sort, const std::string& symbol = std::string()) const;
 
   /**
-   * Create bound variable.
+   * Create (bound) variable.
    * @param sort the sort of the variable
    * @param symbol the name of the variable
    * @return the variable
    */
-  Term mkBoundVar(Sort sort, const std::string& symbol = std::string()) const;
+  Term mkVar(Sort sort, const std::string& symbol = std::string()) const;
 
   /* .................................................................... */
   /* Formula Handling                                                     */
@@ -2245,17 +2248,6 @@ class CVC4_PUBLIC Solver
    */
   Result checkValidAssuming(const std::vector<Term>& assumptions) const;
 
-  /**
-   * Declare first-order constant (0-arity function symbol).
-   * SMT-LIB: ( declare-const <symbol> <sort> )
-   * SMT-LIB: ( declare-fun <symbol> ( ) <sort> )
-   * This command corresponds to mkVar().
-   * @param symbol the name of the first-order constant
-   * @param sort the sort of the first-order constant
-   * @return the first-order constant
-   */
-  Term declareConst(const std::string& symbol, Sort sort) const;
-
   /**
    * Create datatype sort.
    * SMT-LIB: ( declare-datatype <symbol> <datatype_decl> )
@@ -2303,7 +2295,7 @@ class CVC4_PUBLIC Solver
   /**
    * Define n-ary function.
    * SMT-LIB: ( define-fun <function_def> )
-   * Create parameter 'fun' with mkVar().
+   * Create parameter 'fun' with mkConst().
    * @param fun the sorted function
    * @param bound_vars the parameters to this function
    * @param term the function body
@@ -2330,7 +2322,7 @@ class CVC4_PUBLIC Solver
   /**
    * Define recursive function.
    * SMT-LIB: ( define-fun-rec <function_def> )
-   * Create parameter 'fun' with mkVar().
+   * Create parameter 'fun' with mkConst().
    * @param fun the sorted function
    * @param bound_vars the parameters to this function
    * @param term the function body
@@ -2343,7 +2335,7 @@ class CVC4_PUBLIC Solver
   /**
    * Define recursive functions.
    * SMT-LIB: ( define-funs-rec ( <function_decl>^{n+1} ) ( <term>^{n+1} ) )
-   * Create elements of parameter 'funs' with mkVar().
+   * Create elements of parameter 'funs' with mkConst().
    * @param funs the sorted functions
    * @param bound_vars the list of parameters to the functions
    * @param term the list of function bodies of the functions
@@ -2506,7 +2498,7 @@ class CVC4_PUBLIC Solver
   void checkMkTerm(Kind kind, uint32_t nchildren) const;
   /* Helper for mk-functions that call d_exprMgr->mkConst(). */
   template <typename T>
-  Term mkConstHelper(T t) const;
+  Term mkValHelper(T t) const;
   /* Helper for mkReal functions that take a string as argument. */
   Term mkRealFromStrHelper(std::string s) const;
   /* Helper for mkBitVector functions that take a string as argument. */

diff --git a/src/api/cvc4cppkind.h b/src/api/cvc4cppkind.h
index 3aba6cebbd20c01dcd53b9bdfa152ca12d677b3b..d4f6880f9a4d26fcec1d6ad482832422e7611911 100644 (file)
--- a/src/api/cvc4cppkind.h
+++ b/src/api/cvc4cppkind.h
@@ -123,25 +123,25 @@ enum CVC4_PUBLIC Kind : int32_t
    */
   DISTINCT,
   /**
-   * Variable.
+   * First-order constant.
    * Not permitted in bindings (forall, exists, ...).
    * Parameters:
-   *   See mkVar().
+   *   See mkConst().
    * Create with:
-   *   mkVar(const std::string& symbol, Sort sort)
-   *   mkVar(Sort sort)
+   *   mkConst(const std::string& symbol, Sort sort)
+   *   mkConst(Sort sort)
    */
-  VARIABLE,
+  CONSTANT,
   /**
-   * Bound variable.
+   * (Bound) variable.
    * Permitted in bindings and in the lambda and quantifier bodies only.
    * Parameters:
-   *   See mkBoundVar().
+   *   See mkVar().
    * Create with:
-   *   mkBoundVar(const std::string& symbol, Sort sort)
-   *   mkBoundVar(Sort sort)
+   *   mkVar(const std::string& symbol, Sort sort)
+   *   mkVar(Sort sort)
    */
-  BOUND_VARIABLE,
+  VARIABLE,
 #if 0
   /* Skolem variable (internal only) */
   SKOLEM,

diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index 00f2e944d6ce1de6525ac3d944fcd33904960d9f..75df38637c05981aa0085492b3f3518b88fff743 100644 (file)
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -2307,8 +2307,8 @@ termAtomic[CVC4::api::Term& atomTerm]
       sortSymbol[type,CHECK_DECLARED]
       sortSymbol[type2,CHECK_DECLARED]
       {
-        api::Term v1 = SOLVER->mkVar(api::Sort(type), "_emp1");
-        api::Term v2 = SOLVER->mkVar(api::Sort(type2), "_emp2");
+        api::Term v1 = SOLVER->mkConst(api::Sort(type), "_emp1");
+        api::Term v2 = SOLVER->mkConst(api::Sort(type2), "_emp2");
         atomTerm = SOLVER->mkTerm(api::SEP_EMP, v1, v2);
       }
 

diff --git a/test/unit/api/solver_black.h b/test/unit/api/solver_black.h
index a5d927812b4be1a8051614e46ff473a36f1363df..289fc26f02d417cfe4f206c9071c60585007f78d 100644 (file)
--- a/test/unit/api/solver_black.h
+++ b/test/unit/api/solver_black.h
@@ -76,7 +76,6 @@ class SolverBlack : public CxxTest::TestSuite
   void testMkUniverseSet();
   void testMkVar();
 
-  void testDeclareConst();
   void testDeclareDatatype();
   void testDeclareFun();
   void testDeclareSort();
@@ -295,12 +294,12 @@ void SolverBlack::testMkBoundVar()
   Sort boolSort = d_solver->getBooleanSort();
   Sort intSort = d_solver->getIntegerSort();
   Sort funSort = d_solver->mkFunctionSort(intSort, boolSort);
-  TS_ASSERT_THROWS_NOTHING(d_solver->mkBoundVar(boolSort));
-  TS_ASSERT_THROWS_NOTHING(d_solver->mkBoundVar(funSort));
-  TS_ASSERT_THROWS_NOTHING(d_solver->mkBoundVar(boolSort, std::string("b")));
-  TS_ASSERT_THROWS_NOTHING(d_solver->mkBoundVar(funSort, ""));
-  TS_ASSERT_THROWS(d_solver->mkBoundVar(Sort()), CVC4ApiException&);
-  TS_ASSERT_THROWS(d_solver->mkBoundVar(Sort(), "a"), CVC4ApiException&);
+  TS_ASSERT_THROWS_NOTHING(d_solver->mkVar(boolSort));
+  TS_ASSERT_THROWS_NOTHING(d_solver->mkVar(funSort));
+  TS_ASSERT_THROWS_NOTHING(d_solver->mkVar(boolSort, std::string("b")));
+  TS_ASSERT_THROWS_NOTHING(d_solver->mkVar(funSort, ""));
+  TS_ASSERT_THROWS(d_solver->mkVar(Sort()), CVC4ApiException&);
+  TS_ASSERT_THROWS(d_solver->mkVar(Sort(), "a"), CVC4ApiException&);
 }
 
 void SolverBlack::testMkBoolean()
@@ -512,7 +511,7 @@ void SolverBlack::testMkReal()
 void SolverBlack::testMkRegexpEmpty()
 {
   Sort strSort = d_solver->getStringSort();
-  Term s = d_solver->mkVar(strSort, "s");
+  Term s = d_solver->mkConst(strSort, "s");
   TS_ASSERT_THROWS_NOTHING(
       d_solver->mkTerm(STRING_IN_REGEXP, s, d_solver->mkRegexpEmpty()));
 }
@@ -520,7 +519,7 @@ void SolverBlack::testMkRegexpEmpty()
 void SolverBlack::testMkRegexpSigma()
 {
   Sort strSort = d_solver->getStringSort();
-  Term s = d_solver->mkVar(strSort, "s");
+  Term s = d_solver->mkConst(strSort, "s");
   TS_ASSERT_THROWS_NOTHING(
       d_solver->mkTerm(STRING_IN_REGEXP, s, d_solver->mkRegexpSigma()));
 }
@@ -544,8 +543,8 @@ void SolverBlack::testMkString()
 void SolverBlack::testMkTerm()
 {
   Sort bv32 = d_solver->mkBitVectorSort(32);
-  Term a = d_solver->mkVar(bv32, "a");
-  Term b = d_solver->mkVar(bv32, "b");
+  Term a = d_solver->mkConst(bv32, "a");
+  Term b = d_solver->mkConst(bv32, "b");
   std::vector<Term> v1 = {a, b};
   std::vector<Term> v2 = {a, Term()};
   std::vector<Term> v3 = {a, d_solver->mkTrue()};
@@ -597,8 +596,8 @@ void SolverBlack::testMkTerm()
 void SolverBlack::testMkTermFromOpTerm()
 {
   Sort bv32 = d_solver->mkBitVectorSort(32);
-  Term a = d_solver->mkVar(bv32, "a");
-  Term b = d_solver->mkVar(bv32, "b");
+  Term a = d_solver->mkConst(bv32, "a");
+  Term b = d_solver->mkConst(bv32, "b");
   std::vector<Term> v1 = {d_solver->mkReal(1), d_solver->mkReal(2)};
   std::vector<Term> v2 = {d_solver->mkReal(1), Term()};
   std::vector<Term> v3 = {};
@@ -620,7 +619,7 @@ void SolverBlack::testMkTermFromOpTerm()
   Sort listSort = d_solver->mkDatatypeSort(listDecl);
   Sort intListSort =
       listSort.instantiate(std::vector<Sort>{d_solver->getIntegerSort()});
-  Term c = d_solver->declareConst("c", intListSort);
+  Term c = d_solver->mkConst(intListSort, "c");
   Datatype list = listSort.getDatatype();
   // list datatype constructor and selector operator terms
   OpTerm consTerm1 = list.getConstructorTerm("cons");
@@ -733,24 +732,14 @@ void SolverBlack::testMkVar()
   Sort boolSort = d_solver->getBooleanSort();
   Sort intSort = d_solver->getIntegerSort();
   Sort funSort = d_solver->mkFunctionSort(intSort, boolSort);
-  TS_ASSERT_THROWS_NOTHING(d_solver->mkVar(boolSort));
-  TS_ASSERT_THROWS_NOTHING(d_solver->mkVar(funSort));
-  TS_ASSERT_THROWS_NOTHING(d_solver->mkVar(boolSort, std::string("b")));
-  TS_ASSERT_THROWS_NOTHING(d_solver->mkVar(funSort, ""));
-  TS_ASSERT_THROWS(d_solver->mkVar(Sort()), CVC4ApiException&);
-  TS_ASSERT_THROWS(d_solver->mkVar(Sort(), "a"), CVC4ApiException&);
-}
-
-void SolverBlack::testDeclareConst()
-{
-  Sort boolSort = d_solver->getBooleanSort();
-  Sort intSort = d_solver->getIntegerSort();
-  Sort funSort = d_solver->mkFunctionSort(intSort, boolSort);
-  TS_ASSERT_THROWS_NOTHING(d_solver->declareConst(std::string("b"), boolSort));
-  TS_ASSERT_THROWS_NOTHING(d_solver->declareConst(std::string("i"), intSort));
-  TS_ASSERT_THROWS_NOTHING(d_solver->declareConst("f", funSort));
-  TS_ASSERT_THROWS_NOTHING(d_solver->declareConst("", funSort));
-  TS_ASSERT_THROWS(d_solver->declareConst("a", Sort()), CVC4ApiException&);
+  TS_ASSERT_THROWS_NOTHING(d_solver->mkConst(boolSort));
+  TS_ASSERT_THROWS_NOTHING(d_solver->mkConst(funSort));
+  TS_ASSERT_THROWS_NOTHING(d_solver->mkConst(boolSort, std::string("b")));
+  TS_ASSERT_THROWS_NOTHING(d_solver->mkConst(intSort, std::string("i")));
+  TS_ASSERT_THROWS_NOTHING(d_solver->mkConst(funSort, "f"));
+  TS_ASSERT_THROWS_NOTHING(d_solver->mkConst(funSort, ""));
+  TS_ASSERT_THROWS(d_solver->mkConst(Sort()), CVC4ApiException&);
+  TS_ASSERT_THROWS(d_solver->mkConst(Sort(), "a"), CVC4ApiException&);
 }
 
 void SolverBlack::testDeclareDatatype()
@@ -797,16 +786,16 @@ void SolverBlack::testDefineFun()
   Sort funSort1 = d_solver->mkFunctionSort({bvSort, bvSort}, bvSort);
   Sort funSort2 = d_solver->mkFunctionSort(d_solver->mkUninterpretedSort("u"),
                                            d_solver->getIntegerSort());
-  Term b1 = d_solver->mkBoundVar(bvSort, "b1");
-  Term b11 = d_solver->mkBoundVar(bvSort, "b1");
-  Term b2 = d_solver->mkBoundVar(d_solver->getIntegerSort(), "b2");
-  Term b3 = d_solver->mkBoundVar(funSort2, "b3");
-  Term v1 = d_solver->mkBoundVar(bvSort, "v1");
-  Term v2 = d_solver->mkBoundVar(d_solver->getIntegerSort(), "v2");
-  Term v3 = d_solver->mkVar(funSort2, "v3");
-  Term f1 = d_solver->declareConst("f1", funSort1);
-  Term f2 = d_solver->declareConst("f2", funSort2);
-  Term f3 = d_solver->declareConst("f3", bvSort);
+  Term b1 = d_solver->mkVar(bvSort, "b1");
+  Term b11 = d_solver->mkVar(bvSort, "b1");
+  Term b2 = d_solver->mkVar(d_solver->getIntegerSort(), "b2");
+  Term b3 = d_solver->mkVar(funSort2, "b3");
+  Term v1 = d_solver->mkVar(bvSort, "v1");
+  Term v2 = d_solver->mkVar(d_solver->getIntegerSort(), "v2");
+  Term v3 = d_solver->mkConst(funSort2, "v3");
+  Term f1 = d_solver->mkConst(funSort1, "f1");
+  Term f2 = d_solver->mkConst(funSort2, "f2");
+  Term f3 = d_solver->mkConst(bvSort, "f3");
   TS_ASSERT_THROWS_NOTHING(d_solver->defineFun("f", {}, bvSort, v1));
   TS_ASSERT_THROWS_NOTHING(d_solver->defineFun("ff", {b1, b2}, bvSort, v1));
   TS_ASSERT_THROWS_NOTHING(d_solver->defineFun(f1, {b1, b11}, v1));
@@ -829,16 +818,16 @@ void SolverBlack::testDefineFunRec()
   Sort funSort1 = d_solver->mkFunctionSort({bvSort, bvSort}, bvSort);
   Sort funSort2 = d_solver->mkFunctionSort(d_solver->mkUninterpretedSort("u"),
                                            d_solver->getIntegerSort());
-  Term b1 = d_solver->mkBoundVar(bvSort, "b1");
-  Term b11 = d_solver->mkBoundVar(bvSort, "b1");
-  Term b2 = d_solver->mkBoundVar(d_solver->getIntegerSort(), "b2");
-  Term b3 = d_solver->mkBoundVar(funSort2, "b3");
-  Term v1 = d_solver->mkBoundVar(bvSort, "v1");
-  Term v2 = d_solver->mkBoundVar(d_solver->getIntegerSort(), "v2");
-  Term v3 = d_solver->mkVar(funSort2, "v3");
-  Term f1 = d_solver->declareConst("f1", funSort1);
-  Term f2 = d_solver->declareConst("f2", funSort2);
-  Term f3 = d_solver->declareConst("f3", bvSort);
+  Term b1 = d_solver->mkVar(bvSort, "b1");
+  Term b11 = d_solver->mkVar(bvSort, "b1");
+  Term b2 = d_solver->mkVar(d_solver->getIntegerSort(), "b2");
+  Term b3 = d_solver->mkVar(funSort2, "b3");
+  Term v1 = d_solver->mkVar(bvSort, "v1");
+  Term v2 = d_solver->mkVar(d_solver->getIntegerSort(), "v2");
+  Term v3 = d_solver->mkConst(funSort2, "v3");
+  Term f1 = d_solver->mkConst(funSort1, "f1");
+  Term f2 = d_solver->mkConst(funSort2, "f2");
+  Term f3 = d_solver->mkConst(bvSort, "f3");
   TS_ASSERT_THROWS_NOTHING(d_solver->defineFunRec("f", {}, bvSort, v1));
   TS_ASSERT_THROWS_NOTHING(d_solver->defineFunRec("ff", {b1, b2}, bvSort, v1));
   TS_ASSERT_THROWS_NOTHING(d_solver->defineFunRec(f1, {b1, b11}, v1));
@@ -863,18 +852,18 @@ void SolverBlack::testDefineFunsRec()
   Sort bvSort = d_solver->mkBitVectorSort(32);
   Sort funSort1 = d_solver->mkFunctionSort({bvSort, bvSort}, bvSort);
   Sort funSort2 = d_solver->mkFunctionSort(uSort, d_solver->getIntegerSort());
-  Term b1 = d_solver->mkBoundVar(bvSort, "b1");
-  Term b11 = d_solver->mkBoundVar(bvSort, "b1");
-  Term b2 = d_solver->mkBoundVar(d_solver->getIntegerSort(), "b2");
-  Term b3 = d_solver->mkBoundVar(funSort2, "b3");
-  Term b4 = d_solver->mkBoundVar(uSort, "b4");
-  Term v1 = d_solver->mkBoundVar(bvSort, "v1");
-  Term v2 = d_solver->mkBoundVar(d_solver->getIntegerSort(), "v2");
-  Term v3 = d_solver->mkVar(funSort2, "v3");
-  Term v4 = d_solver->mkVar(uSort, "v4");
-  Term f1 = d_solver->declareConst("f1", funSort1);
-  Term f2 = d_solver->declareConst("f2", funSort2);
-  Term f3 = d_solver->declareConst("f3", bvSort);
+  Term b1 = d_solver->mkVar(bvSort, "b1");
+  Term b11 = d_solver->mkVar(bvSort, "b1");
+  Term b2 = d_solver->mkVar(d_solver->getIntegerSort(), "b2");
+  Term b3 = d_solver->mkVar(funSort2, "b3");
+  Term b4 = d_solver->mkVar(uSort, "b4");
+  Term v1 = d_solver->mkVar(bvSort, "v1");
+  Term v2 = d_solver->mkVar(d_solver->getIntegerSort(), "v2");
+  Term v3 = d_solver->mkConst(funSort2, "v3");
+  Term v4 = d_solver->mkConst(uSort, "v4");
+  Term f1 = d_solver->mkConst(funSort1, "f1");
+  Term f2 = d_solver->mkConst(funSort2, "f2");
+  Term f3 = d_solver->mkConst(bvSort, "f3");
   TS_ASSERT_THROWS_NOTHING(
       d_solver->defineFunsRec({f1, f2}, {{b1, b11}, {b4}}, {v1, v2}));
   TS_ASSERT_THROWS(