diff options
Diffstat (limited to 'examples')
| -rw-r--r-- | examples/api/combination-new.cpp | 4 | ||||
| -rw-r--r-- | examples/api/datatypes-new.cpp | 4 | ||||
| -rw-r--r-- | examples/api/linear_arith-new.cpp | 4 | ||||
| -rw-r--r-- | examples/api/sets-new.cpp | 6 | ||||
| -rw-r--r-- | examples/api/strings-new.cpp | 2 |
5 files changed, 10 insertions, 10 deletions
diff --git a/examples/api/combination-new.cpp b/examples/api/combination-new.cpp index 2956d76e6..8c968c95e 100644 --- a/examples/api/combination-new.cpp +++ b/examples/api/combination-new.cpp @@ -59,8 +59,8 @@ int main() Term p = slv.mkVar("p", intPred); // Constants - Term zero = slv.mkInteger(0); - Term one = slv.mkInteger(1); + Term zero = slv.mkReal(0); + Term one = slv.mkReal(1); // Terms Term f_x = slv.mkTerm(APPLY_UF, f, x); diff --git a/examples/api/datatypes-new.cpp b/examples/api/datatypes-new.cpp index b6a816db4..48560e894 100644 --- a/examples/api/datatypes-new.cpp +++ b/examples/api/datatypes-new.cpp @@ -39,7 +39,7 @@ void test(Solver& slv, Sort& consListSort) Term t = slv.mkTerm( APPLY_CONSTRUCTOR, consList.getConstructorTerm("cons"), - slv.mkInteger(0), + slv.mkReal(0), slv.mkTerm(APPLY_CONSTRUCTOR, consList.getConstructorTerm("nil"))); std::cout << "t is " << t << std::endl @@ -127,7 +127,7 @@ void test(Solver& slv, Sort& consListSort) << "sort of cons is " << paramConsList.getConstructorTerm("cons").getSort() << std::endl << std::endl; - Term assertion = slv.mkTerm(GT, head_a, slv.mkInteger(50)); + Term assertion = slv.mkTerm(GT, head_a, slv.mkReal(50)); std::cout << "Assert " << assertion << std::endl; slv.assertFormula(assertion); std::cout << "Expect sat." << std::endl; diff --git a/examples/api/linear_arith-new.cpp b/examples/api/linear_arith-new.cpp index ef8faade9..d643b85bc 100644 --- a/examples/api/linear_arith-new.cpp +++ b/examples/api/linear_arith-new.cpp @@ -40,8 +40,8 @@ int main() Term y = slv.mkVar("y", real); // Constants - Term three = slv.mkInteger(3); - Term neg2 = slv.mkInteger(-2); + Term three = slv.mkReal(3); + Term neg2 = slv.mkReal(-2); Term two_thirds = slv.mkReal(2, 3); // Terms diff --git a/examples/api/sets-new.cpp b/examples/api/sets-new.cpp index be35bcc21..2dcfbbc02 100644 --- a/examples/api/sets-new.cpp +++ b/examples/api/sets-new.cpp @@ -70,9 +70,9 @@ int main() // Find me an element in {1, 2} intersection {2, 3}, if there is one. { - Term one = slv.mkInteger(1); - Term two = slv.mkInteger(2); - Term three = slv.mkInteger(3); + Term one = slv.mkReal(1); + Term two = slv.mkReal(2); + Term three = slv.mkReal(3); Term singleton_one = slv.mkTerm(SINGLETON, one); Term singleton_two = slv.mkTerm(SINGLETON, two); diff --git a/examples/api/strings-new.cpp b/examples/api/strings-new.cpp index 2010c6909..c88ccc9c0 100644 --- a/examples/api/strings-new.cpp +++ b/examples/api/strings-new.cpp @@ -57,7 +57,7 @@ int main() // Length of y: |y| Term leny = slv.mkTerm(STRING_LENGTH, y); // |y| >= 0 - Term formula2 = slv.mkTerm(GEQ, leny, slv.mkInteger(0)); + Term formula2 = slv.mkTerm(GEQ, leny, slv.mkReal(0)); // Regular expression: (ab[c-e]*f)|g|h Term r = slv.mkTerm(REGEXP_UNION, |