New C++: Remove redundant mkVar function.

s

2 files changed, 46 insertions, 46 deletions

diff --git a/test/unit/api/solver_black.h b/test/unit/api/solver_black.h
index c42854fce..f64751d01 100644
--- a/test/unit/api/solver_black.h
+++ b/test/unit/api/solver_black.h
@@ -510,7 +510,7 @@ void SolverBlack::testMkReal()
 void SolverBlack::testMkRegexpEmpty()
 {
   Sort strSort = d_solver->getStringSort();
-  Term s = d_solver->mkVar("s", strSort);
+  Term s = d_solver->mkVar(strSort, "s");
   TS_ASSERT_THROWS_NOTHING(
       d_solver->mkTerm(STRING_IN_REGEXP, s, d_solver->mkRegexpEmpty()));
 }
@@ -518,7 +518,7 @@ void SolverBlack::testMkRegexpEmpty()
 void SolverBlack::testMkRegexpSigma()
 {
   Sort strSort = d_solver->getStringSort();
-  Term s = d_solver->mkVar("s", strSort);
+  Term s = d_solver->mkVar(strSort, "s");
   TS_ASSERT_THROWS_NOTHING(
       d_solver->mkTerm(STRING_IN_REGEXP, s, d_solver->mkRegexpSigma()));
 }
@@ -542,8 +542,8 @@ void SolverBlack::testMkString()
 void SolverBlack::testMkTerm()
 {
   Sort bv32 = d_solver->mkBitVectorSort(32);
-  Term a = d_solver->mkVar("a", bv32);
-  Term b = d_solver->mkVar("b", bv32);
+  Term a = d_solver->mkVar(bv32, "a");
+  Term b = d_solver->mkVar(bv32, "b");
   std::vector<Term> v1 = {a, b};
   std::vector<Term> v2 = {a, Term()};
   std::vector<Term> v3 = {a, d_solver->mkTrue()};
@@ -595,8 +595,8 @@ void SolverBlack::testMkTerm()
 void SolverBlack::testMkTermFromOpTerm()
 {
   Sort bv32 = d_solver->mkBitVectorSort(32);
-  Term a = d_solver->mkVar("a", bv32);
-  Term b = d_solver->mkVar("b", bv32);
+  Term a = d_solver->mkVar(bv32, "a");
+  Term b = d_solver->mkVar(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 = {};
@@ -731,12 +731,12 @@ void SolverBlack::testMkVar()
   Sort boolSort = d_solver->getBooleanSort();
   Sort intSort = d_solver->getIntegerSort();
   Sort funSort = d_solver->mkFunctionSort(intSort, boolSort);
-  TS_ASSERT_THROWS(d_solver->mkVar(Sort()), CVC4ApiException&);
   TS_ASSERT_THROWS_NOTHING(d_solver->mkVar(boolSort));
   TS_ASSERT_THROWS_NOTHING(d_solver->mkVar(funSort));
-  TS_ASSERT_THROWS(d_solver->mkVar("a", Sort()), CVC4ApiException&);
-  TS_ASSERT_THROWS_NOTHING(d_solver->mkVar(std::string("b"), 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()
@@ -801,7 +801,7 @@ void SolverBlack::testDefineFun()
   Term b3 = d_solver->mkBoundVar("b3", funSort2);
   Term v1 = d_solver->mkBoundVar("v1", bvSort);
   Term v2 = d_solver->mkBoundVar("v2", d_solver->getIntegerSort());
-  Term v3 = d_solver->mkVar("v3", funSort2);
+  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);
@@ -833,7 +833,7 @@ void SolverBlack::testDefineFunRec()
   Term b3 = d_solver->mkBoundVar("b3", funSort2);
   Term v1 = d_solver->mkBoundVar("v1", bvSort);
   Term v2 = d_solver->mkBoundVar("v2", d_solver->getIntegerSort());
-  Term v3 = d_solver->mkVar("v3", funSort2);
+  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);
@@ -868,8 +868,8 @@ void SolverBlack::testDefineFunsRec()
   Term b4 = d_solver->mkBoundVar("b4", uSort);
   Term v1 = d_solver->mkBoundVar("v1", bvSort);
   Term v2 = d_solver->mkBoundVar("v2", d_solver->getIntegerSort());
-  Term v3 = d_solver->mkVar("v3", funSort2);
-  Term v4 = d_solver->mkVar("v4", uSort);
+  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);
diff --git a/test/unit/api/term_black.h b/test/unit/api/term_black.h
index a7f735651..5bb99ff2a 100644
--- a/test/unit/api/term_black.h
+++ b/test/unit/api/term_black.h
@@ -45,8 +45,8 @@ class TermBlack : public CxxTest::TestSuite
 void TermBlack::testEq()
 {
   Sort uSort = d_solver.mkUninterpretedSort("u");
-  Term x = d_solver.mkVar("x", uSort);
-  Term y = d_solver.mkVar("y", uSort);
+  Term x = d_solver.mkVar(uSort, "x");
+  Term y = d_solver.mkVar(uSort, "y");
   Term z;
 
   TS_ASSERT(x == x);
@@ -67,14 +67,14 @@ void TermBlack::testGetKind()
 
   Term n;
   TS_ASSERT_THROWS(n.getKind(), CVC4ApiException&);
-  Term x = d_solver.mkVar("x", uSort);
+  Term x = d_solver.mkVar(uSort, "x");
   TS_ASSERT_THROWS_NOTHING(x.getKind());
-  Term y = d_solver.mkVar("y", uSort);
+  Term y = d_solver.mkVar(uSort, "y");
   TS_ASSERT_THROWS_NOTHING(y.getKind());
 
-  Term f = d_solver.mkVar("f", funSort1);
+  Term f = d_solver.mkVar(funSort1, "f");
   TS_ASSERT_THROWS_NOTHING(f.getKind());
-  Term p = d_solver.mkVar("p", funSort2);
+  Term p = d_solver.mkVar(funSort2, "p");
   TS_ASSERT_THROWS_NOTHING(p.getKind());
 
   Term zero = d_solver.mkReal(0);
@@ -102,17 +102,17 @@ void TermBlack::testGetSort()
 
   Term n;
   TS_ASSERT_THROWS(n.getSort(), CVC4ApiException&);
-  Term x = d_solver.mkVar("x", bvSort);
+  Term x = d_solver.mkVar(bvSort, "x");
   TS_ASSERT_THROWS_NOTHING(x.getSort());
   TS_ASSERT(x.getSort() == bvSort);
-  Term y = d_solver.mkVar("y", bvSort);
+  Term y = d_solver.mkVar(bvSort, "y");
   TS_ASSERT_THROWS_NOTHING(y.getSort());
   TS_ASSERT(y.getSort() == bvSort);
 
-  Term f = d_solver.mkVar("f", funSort1);
+  Term f = d_solver.mkVar(funSort1, "f");
   TS_ASSERT_THROWS_NOTHING(f.getSort());
   TS_ASSERT(f.getSort() == funSort1);
-  Term p = d_solver.mkVar("p", funSort2);
+  Term p = d_solver.mkVar(funSort2, "p");
   TS_ASSERT_THROWS_NOTHING(p.getSort());
   TS_ASSERT(p.getSort() == funSort2);
 
@@ -141,7 +141,7 @@ void TermBlack::testIsNull()
 {
   Term x;
   TS_ASSERT(x.isNull());
-  x = d_solver.mkVar("x", d_solver.mkBitVectorSort(4));
+  x = d_solver.mkVar(d_solver.mkBitVectorSort(4), "x");
   TS_ASSERT(!x.isNull());
 }
 
@@ -155,11 +155,11 @@ void TermBlack::testNotTerm()
 
   Term b = d_solver.mkTrue();
   TS_ASSERT_THROWS_NOTHING(b.notTerm());
-  Term x = d_solver.mkVar("x", d_solver.mkBitVectorSort(8));
+  Term x = d_solver.mkVar(d_solver.mkBitVectorSort(8), "x");
   TS_ASSERT_THROWS(x.notTerm(), CVC4ApiException&);
-  Term f = d_solver.mkVar("f", funSort1);
+  Term f = d_solver.mkVar(funSort1, "f");
   TS_ASSERT_THROWS(f.notTerm(), CVC4ApiException&);
-  Term p = d_solver.mkVar("p", funSort2);
+  Term p = d_solver.mkVar(funSort2, "p");
   TS_ASSERT_THROWS(p.notTerm(), CVC4ApiException&);
   Term zero = d_solver.mkReal(0);
   TS_ASSERT_THROWS(zero.notTerm(), CVC4ApiException&);
@@ -183,14 +183,14 @@ void TermBlack::testAndTerm()
 
   Term b = d_solver.mkTrue();
   TS_ASSERT_THROWS_NOTHING(b.andTerm(b));
-  Term x = d_solver.mkVar("x", d_solver.mkBitVectorSort(8));
+  Term x = d_solver.mkVar(d_solver.mkBitVectorSort(8), "x");
   TS_ASSERT_THROWS(x.andTerm(b), CVC4ApiException&);
   TS_ASSERT_THROWS(x.andTerm(x), CVC4ApiException&);
-  Term f = d_solver.mkVar("f", funSort1);
+  Term f = d_solver.mkVar(funSort1, "f");
   TS_ASSERT_THROWS(f.andTerm(b), CVC4ApiException&);
   TS_ASSERT_THROWS(f.andTerm(x), CVC4ApiException&);
   TS_ASSERT_THROWS(f.andTerm(f), CVC4ApiException&);
-  Term p = d_solver.mkVar("p", funSort2);
+  Term p = d_solver.mkVar(funSort2, "p");
   TS_ASSERT_THROWS(p.andTerm(b), CVC4ApiException&);
   TS_ASSERT_THROWS(p.andTerm(x), CVC4ApiException&);
   TS_ASSERT_THROWS(p.andTerm(f), CVC4ApiException&);
@@ -247,14 +247,14 @@ void TermBlack::testOrTerm()
 
   Term b = d_solver.mkTrue();
   TS_ASSERT_THROWS_NOTHING(b.orTerm(b));
-  Term x = d_solver.mkVar("x", d_solver.mkBitVectorSort(8));
+  Term x = d_solver.mkVar(d_solver.mkBitVectorSort(8), "x");
   TS_ASSERT_THROWS(x.orTerm(b), CVC4ApiException&);
   TS_ASSERT_THROWS(x.orTerm(x), CVC4ApiException&);
-  Term f = d_solver.mkVar("f", funSort1);
+  Term f = d_solver.mkVar(funSort1, "f");
   TS_ASSERT_THROWS(f.orTerm(b), CVC4ApiException&);
   TS_ASSERT_THROWS(f.orTerm(x), CVC4ApiException&);
   TS_ASSERT_THROWS(f.orTerm(f), CVC4ApiException&);
-  Term p = d_solver.mkVar("p", funSort2);
+  Term p = d_solver.mkVar(funSort2, "p");
   TS_ASSERT_THROWS(p.orTerm(b), CVC4ApiException&);
   TS_ASSERT_THROWS(p.orTerm(x), CVC4ApiException&);
   TS_ASSERT_THROWS(p.orTerm(f), CVC4ApiException&);
@@ -311,14 +311,14 @@ void TermBlack::testXorTerm()
 
   Term b = d_solver.mkTrue();
   TS_ASSERT_THROWS_NOTHING(b.xorTerm(b));
-  Term x = d_solver.mkVar("x", d_solver.mkBitVectorSort(8));
+  Term x = d_solver.mkVar(d_solver.mkBitVectorSort(8), "x");
   TS_ASSERT_THROWS(x.xorTerm(b), CVC4ApiException&);
   TS_ASSERT_THROWS(x.xorTerm(x), CVC4ApiException&);
-  Term f = d_solver.mkVar("f", funSort1);
+  Term f = d_solver.mkVar(funSort1, "f");
   TS_ASSERT_THROWS(f.xorTerm(b), CVC4ApiException&);
   TS_ASSERT_THROWS(f.xorTerm(x), CVC4ApiException&);
   TS_ASSERT_THROWS(f.xorTerm(f), CVC4ApiException&);
-  Term p = d_solver.mkVar("p", funSort2);
+  Term p = d_solver.mkVar(funSort2, "p");
   TS_ASSERT_THROWS(p.xorTerm(b), CVC4ApiException&);
   TS_ASSERT_THROWS(p.xorTerm(x), CVC4ApiException&);
   TS_ASSERT_THROWS(p.xorTerm(f), CVC4ApiException&);
@@ -375,14 +375,14 @@ void TermBlack::testEqTerm()
 
   Term b = d_solver.mkTrue();
   TS_ASSERT_THROWS_NOTHING(b.eqTerm(b));
-  Term x = d_solver.mkVar("x", d_solver.mkBitVectorSort(8));
+  Term x = d_solver.mkVar(d_solver.mkBitVectorSort(8), "x");
   TS_ASSERT_THROWS(x.eqTerm(b), CVC4ApiException&);
   TS_ASSERT_THROWS_NOTHING(x.eqTerm(x));
-  Term f = d_solver.mkVar("f", funSort1);
+  Term f = d_solver.mkVar(funSort1, "f");
   TS_ASSERT_THROWS(f.eqTerm(b), CVC4ApiException&);
   TS_ASSERT_THROWS(f.eqTerm(x), CVC4ApiException&);
   TS_ASSERT_THROWS_NOTHING(f.eqTerm(f));
-  Term p = d_solver.mkVar("p", funSort2);
+  Term p = d_solver.mkVar(funSort2, "p");
   TS_ASSERT_THROWS(p.eqTerm(b), CVC4ApiException&);
   TS_ASSERT_THROWS(p.eqTerm(x), CVC4ApiException&);
   TS_ASSERT_THROWS(p.eqTerm(f), CVC4ApiException&);
@@ -439,14 +439,14 @@ void TermBlack::testImpTerm()
 
   Term b = d_solver.mkTrue();
   TS_ASSERT_THROWS_NOTHING(b.impTerm(b));
-  Term x = d_solver.mkVar("x", d_solver.mkBitVectorSort(8));
+  Term x = d_solver.mkVar(d_solver.mkBitVectorSort(8), "x");
   TS_ASSERT_THROWS(x.impTerm(b), CVC4ApiException&);
   TS_ASSERT_THROWS(x.impTerm(x), CVC4ApiException&);
-  Term f = d_solver.mkVar("f", funSort1);
+  Term f = d_solver.mkVar(funSort1, "f");
   TS_ASSERT_THROWS(f.impTerm(b), CVC4ApiException&);
   TS_ASSERT_THROWS(f.impTerm(x), CVC4ApiException&);
   TS_ASSERT_THROWS(f.impTerm(f), CVC4ApiException&);
-  Term p = d_solver.mkVar("p", funSort2);
+  Term p = d_solver.mkVar(funSort2, "p");
   TS_ASSERT_THROWS(p.impTerm(b), CVC4ApiException&);
   TS_ASSERT_THROWS(p.impTerm(x), CVC4ApiException&);
   TS_ASSERT_THROWS(p.impTerm(f), CVC4ApiException&);
@@ -503,16 +503,16 @@ void TermBlack::testIteTerm()
 
   Term b = d_solver.mkTrue();
   TS_ASSERT_THROWS_NOTHING(b.iteTerm(b, b));
-  Term x = d_solver.mkVar("x", d_solver.mkBitVectorSort(8));
+  Term x = d_solver.mkVar(d_solver.mkBitVectorSort(8), "x");
   TS_ASSERT_THROWS_NOTHING(b.iteTerm(x, x));
   TS_ASSERT_THROWS_NOTHING(b.iteTerm(b, b));
   TS_ASSERT_THROWS(b.iteTerm(x, b), CVC4ApiException&);
   TS_ASSERT_THROWS(x.iteTerm(x, x), CVC4ApiException&);
   TS_ASSERT_THROWS(x.iteTerm(x, b), CVC4ApiException&);
-  Term f = d_solver.mkVar("f", funSort1);
+  Term f = d_solver.mkVar(funSort1, "f");
   TS_ASSERT_THROWS(f.iteTerm(b, b), CVC4ApiException&);
   TS_ASSERT_THROWS(x.iteTerm(b, x), CVC4ApiException&);
-  Term p = d_solver.mkVar("p", funSort2);
+  Term p = d_solver.mkVar(funSort2, "p");
   TS_ASSERT_THROWS(p.iteTerm(b, b), CVC4ApiException&);
   TS_ASSERT_THROWS(p.iteTerm(x, b), CVC4ApiException&);
   Term zero = d_solver.mkReal(0);