diff options
-rw-r--r-- | examples/api/bitvectors-new.cpp | 10 | ||||
-rw-r--r-- | examples/api/bitvectors_and_arrays-new.cpp | 2 | ||||
-rw-r--r-- | examples/api/combination-new.cpp | 8 | ||||
-rw-r--r-- | examples/api/extract-new.cpp | 2 | ||||
-rw-r--r-- | examples/api/helloworld-new.cpp | 2 | ||||
-rw-r--r-- | examples/api/linear_arith-new.cpp | 4 | ||||
-rw-r--r-- | examples/api/sets-new.cpp | 10 | ||||
-rw-r--r-- | examples/api/strings-new.cpp | 10 | ||||
-rw-r--r-- | src/api/cvc4cpp.cpp | 20 | ||||
-rw-r--r-- | src/api/cvc4cpp.h | 11 | ||||
-rw-r--r-- | src/parser/smt2/Smt2.g | 4 | ||||
-rw-r--r-- | test/unit/api/solver_black.h | 28 | ||||
-rw-r--r-- | test/unit/api/term_black.h | 64 |
13 files changed, 77 insertions, 98 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); diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp index 9d56bb88a..032326c26 100644 --- a/src/api/cvc4cpp.cpp +++ b/src/api/cvc4cpp.cpp @@ -2392,27 +2392,13 @@ Term Solver::mkFloatingPoint(uint32_t exp, uint32_t sig, Term val) const /* Create variables */ /* -------------------------------------------------------------------------- */ -Term Solver::mkVar(const std::string& symbol, Sort sort) const +Term Solver::mkVar(Sort sort, const std::string& symbol) 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()); - } -} - -Term Solver::mkVar(Sort sort) const -{ - try - { - CVC4_API_ARG_CHECK_EXPECTED(!sort.isNull(), sort) << "non-null sort"; - Term res = d_exprMgr->mkVar(*sort.d_type); + Term res = symbol.empty() ? d_exprMgr->mkVar(*sort.d_type) + : d_exprMgr->mkVar(symbol, *sort.d_type); (void)res.d_expr->getType(true); /* kick off type checking */ return res; } diff --git a/src/api/cvc4cpp.h b/src/api/cvc4cpp.h index 2c266b11d..3999dd2ed 100644 --- a/src/api/cvc4cpp.h +++ b/src/api/cvc4cpp.h @@ -2167,18 +2167,11 @@ class CVC4_PUBLIC Solver /** * Create variable. - * @param symbol the name of the variable - * @param sort the sort of the variable - * @return the variable - */ - Term mkVar(const std::string& symbol, Sort sort) const; - - /** - * Create variable. * @param sort the sort of the variable + * @param symbol the name of the variable * @return the variable */ - Term mkVar(Sort sort) const; + Term mkVar(Sort sort, const std::string& symbol = std::string()) const; /** * Create bound variable. diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index c72a4f99b..81f01c138 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -2306,8 +2306,8 @@ termAtomic[CVC4::api::Term& atomTerm] sortSymbol[type,CHECK_DECLARED] sortSymbol[type2,CHECK_DECLARED] { - api::Term v1 = SOLVER->mkVar("_emp1", api::Sort(type)); - api::Term v2 = SOLVER->mkVar("_emp2", api::Sort(type2)); + api::Term v1 = SOLVER->mkVar(api::Sort(type), "_emp1"); + api::Term v2 = SOLVER->mkVar(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 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); |