diff options
Diffstat (limited to 'examples')
-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/datatypes-new.cpp | 2 | ||||
-rw-r--r-- | examples/api/extract-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 |
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); |