diff options
author | Aina Niemetz <aina.niemetz@gmail.com> | 2019-01-29 11:47:04 -0800 |
---|---|---|
committer | GitHub <noreply@github.com> | 2019-01-29 11:47:04 -0800 |
commit | d4870775e67c7878c32c17f10b1217c14dc5869b (patch) | |
tree | 8e2bcd1a731eab54041724bb9310e1c7aaaf3e4c /examples/api | |
parent | 1eaf6cf987fa1452528dc0598ca7235be735ba3b (diff) |
New C++ API: Fix checks for mkTerm. (#2820)
This required fixing the OpTerm handling for mkTerm functions in the API.
Diffstat (limited to 'examples/api')
-rw-r--r-- | examples/api/bitvectors-new.cpp | 12 | ||||
-rw-r--r-- | examples/api/datatypes-new.cpp | 27 | ||||
-rw-r--r-- | examples/api/extract-new.cpp | 8 |
3 files changed, 22 insertions, 25 deletions
diff --git a/examples/api/bitvectors-new.cpp b/examples/api/bitvectors-new.cpp index cd34a5130..7070f6748 100644 --- a/examples/api/bitvectors-new.cpp +++ b/examples/api/bitvectors-new.cpp @@ -24,9 +24,8 @@ using namespace CVC4::api; int main() { - Solver slv; - slv.setLogic("QF_BV"); // Set the logic + slv.setLogic("QF_BV"); // Set the logic // The following example has been adapted from the book A Hacker's Delight by // Henry S. Warren. @@ -64,8 +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("new_x_", bitvector32); // x after executing code (1) or (2) + Term new_x = slv.mkVar("new_x", bitvector32); // x after executing code (0) + Term new_x_ = + slv.mkVar("new_x_", bitvector32); // x after executing code (1) or (2) // Encoding code (0) // new_x = x == a ? b : a; @@ -114,9 +114,9 @@ int main() cout << " Expect invalid. " << endl; cout << " CVC4: " << slv.checkValidAssuming(v) << endl; - // Assert that a is odd + // Assert that a is odd OpTerm extract_op = slv.mkOpTerm(BITVECTOR_EXTRACT_OP, 0, 0); - Term lsb_of_a = slv.mkTerm(extract_op, a); + Term lsb_of_a = slv.mkTerm(BITVECTOR_EXTRACT, extract_op, a); cout << "Sort of " << lsb_of_a << " is " << lsb_of_a.getSort() << endl; Term a_odd = slv.mkTerm(EQUAL, lsb_of_a, slv.mkBitVector(1u, 1u)); cout << "Assert " << a_odd << endl; diff --git a/examples/api/datatypes-new.cpp b/examples/api/datatypes-new.cpp index 48560e894..14ddcd383 100644 --- a/examples/api/datatypes-new.cpp +++ b/examples/api/datatypes-new.cpp @@ -57,18 +57,15 @@ void test(Solver& slv, Sort& consListSort) slv.mkTerm(APPLY_SELECTOR, consList["cons"].getSelectorTerm("head"), t); std::cout << "t2 is " << t2 << std::endl - << "simplify(t2) is " << slv.simplify(t2) - << std::endl << std::endl; + << "simplify(t2) is " << slv.simplify(t2) << std::endl + << std::endl; // You can also iterate over a Datatype to get all its constructors, // and over a DatatypeConstructor to get all its "args" (selectors) - for (Datatype::const_iterator i = consList.begin(); - i != consList.end(); - ++i) + for (Datatype::const_iterator i = consList.begin(); i != consList.end(); ++i) { std::cout << "ctor: " << *i << std::endl; - for (DatatypeConstructor::const_iterator j = (*i).begin(); - j != (*i).end(); + for (DatatypeConstructor::const_iterator j = (*i).begin(); j != (*i).end(); ++j) { std::cout << " + arg: " << *j << std::endl; @@ -91,7 +88,8 @@ void test(Solver& slv, Sort& consListSort) // This example builds a simple parameterized list of sort T, with one // constructor "cons". Sort sort = slv.mkParamSort("T"); - DatatypeDecl paramConsListSpec("paramlist", sort); // give the datatype a name + DatatypeDecl paramConsListSpec("paramlist", + sort); // give the datatype a name DatatypeConstructorDecl paramCons("cons"); DatatypeConstructorDecl paramNil("nil"); DatatypeSelectorDecl paramHead("head", sort); @@ -122,7 +120,7 @@ void test(Solver& slv, Sort& consListSort) Term head_a = slv.mkTerm( APPLY_SELECTOR, paramConsList["cons"].getSelectorTerm("head"), a); - std::cout << "head_a is " << head_a << " of sort " << head_a.getSort() + std::cout << "head_a is " << head_a << " of sort " << head_a.getSort() << std::endl << "sort of cons is " << paramConsList.getConstructorTerm("cons").getSort() << std::endl @@ -145,7 +143,7 @@ int main() // Second, it is "resolved" to an actual sort, at which point function // symbols are assigned to its constructors, selectors, and testers. - DatatypeDecl consListSpec("list"); // give the datatype a name + DatatypeDecl consListSpec("list"); // give the datatype a name DatatypeConstructorDecl cons("cons"); DatatypeSelectorDecl head("head", slv.getIntegerSort()); DatatypeSelectorDecl tail("tail", DatatypeDeclSelfSort()); @@ -155,8 +153,7 @@ int main() DatatypeConstructorDecl nil("nil"); consListSpec.addConstructor(nil); - std::cout << "spec is:" << std::endl - << consListSpec << std::endl; + std::cout << "spec is:" << std::endl << consListSpec << std::endl; // Keep in mind that "DatatypeDecl" is the specification class for // datatypes---"DatatypeDecl" is not itself a CVC4 Sort. @@ -168,13 +165,13 @@ int main() test(slv, consListSort); - std::cout << std::endl << ">>> Alternatively, use declareDatatype" << std::endl; + std::cout << std::endl + << ">>> Alternatively, use declareDatatype" << std::endl; std::cout << std::endl; - std::vector<DatatypeConstructorDecl> ctors = { cons, nil }; + std::vector<DatatypeConstructorDecl> ctors = {cons, nil}; Sort consListSort2 = slv.declareDatatype("list2", ctors); test(slv, consListSort2); - return 0; } diff --git a/examples/api/extract-new.cpp b/examples/api/extract-new.cpp index 8d31c1b12..96961458e 100644 --- a/examples/api/extract-new.cpp +++ b/examples/api/extract-new.cpp @@ -32,16 +32,16 @@ int main() Term x = slv.mkVar("a", bitvector32); OpTerm ext_31_1 = slv.mkOpTerm(BITVECTOR_EXTRACT_OP, 31, 1); - Term x_31_1 = slv.mkTerm(ext_31_1, x); + Term x_31_1 = slv.mkTerm(BITVECTOR_EXTRACT, ext_31_1, x); OpTerm ext_30_0 = slv.mkOpTerm(BITVECTOR_EXTRACT_OP, 30, 0); - Term x_30_0 = slv.mkTerm(ext_30_0, x); + Term x_30_0 = slv.mkTerm(BITVECTOR_EXTRACT, ext_30_0, x); OpTerm ext_31_31 = slv.mkOpTerm(BITVECTOR_EXTRACT_OP, 31, 31); - Term x_31_31 = slv.mkTerm(ext_31_31, x); + Term x_31_31 = slv.mkTerm(BITVECTOR_EXTRACT, ext_31_31, x); OpTerm ext_0_0 = slv.mkOpTerm(BITVECTOR_EXTRACT_OP, 0, 0); - Term x_0_0 = slv.mkTerm(ext_0_0, x); + Term x_0_0 = slv.mkTerm(BITVECTOR_EXTRACT, ext_0_0, x); Term eq = slv.mkTerm(EQUAL, x_31_1, x_30_0); cout << " Asserting: " << eq << endl; |