diff options
author | Aina Niemetz <aina.niemetz@gmail.com> | 2018-07-23 12:29:03 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2018-07-23 12:29:03 -0700 |
commit | 35c39b2cdc3905af8ad4739c20971d8b35889582 (patch) | |
tree | d2e6a6c647b3f3404aac7006eaf9497d1161d353 /examples | |
parent | 416f6d2d55fb24fea63bd13537b24a6a88509344 (diff) |
New C++ API: declare-datatype. (#2166)
Diffstat (limited to 'examples')
-rw-r--r-- | examples/api/datatypes-new.cpp | 75 |
1 files changed, 44 insertions, 31 deletions
diff --git a/examples/api/datatypes-new.cpp b/examples/api/datatypes-new.cpp index 9ec679f8e..0989d3c48 100644 --- a/examples/api/datatypes-new.cpp +++ b/examples/api/datatypes-new.cpp @@ -20,38 +20,8 @@ #include "api/cvc4cpp.h" using namespace CVC4::api; -int main() +void test(Solver& slv, Sort& consListSort) { - Solver slv; - // This example builds a simple "cons list" of integers, with - // two constructors, "cons" and "nil." - - // Building a datatype consists of two steps. - // First, the datatype is specified. - // 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 - DatatypeConstructorDecl cons("cons"); - DatatypeSelectorDecl head("head", slv.getIntegerSort()); - DatatypeSelectorDecl tail("tail", DatatypeDeclSelfSort()); - cons.addSelector(head); - cons.addSelector(tail); - consListSpec.addConstructor(cons); - DatatypeConstructorDecl nil("nil"); - consListSpec.addConstructor(nil); - - 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. - // Now that our Datatype is fully specified, we can get a Sort for it. - // This step resolves the "SelfSort" reference and creates - // symbols for all the constructors, etc. - - Sort consListSort = slv.mkDatatypeSort(consListSpec); - // Now our old "consListSpec" is useless--the relevant information // has been copied out, so we can throw that spec away. We can get // the complete spec for the datatype from the DatatypeSort, and @@ -160,6 +130,49 @@ int main() slv.assertFormula(assertion); std::cout << "Expect sat." << std::endl; std::cout << "CVC4: " << slv.checkSat() << std::endl; +} + +int main() +{ + Solver slv; + // This example builds a simple "cons list" of integers, with + // two constructors, "cons" and "nil." + + // Building a datatype consists of two steps. + // First, the datatype is specified. + // 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 + DatatypeConstructorDecl cons("cons"); + DatatypeSelectorDecl head("head", slv.getIntegerSort()); + DatatypeSelectorDecl tail("tail", DatatypeDeclSelfSort()); + cons.addSelector(head); + cons.addSelector(tail); + consListSpec.addConstructor(cons); + DatatypeConstructorDecl nil("nil"); + consListSpec.addConstructor(nil); + + 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. + // Now that our Datatype is fully specified, we can get a Sort for it. + // This step resolves the "SelfSort" reference and creates + // symbols for all the constructors, etc. + + Sort consListSort = slv.mkDatatypeSort(consListSpec); + + test(slv, consListSort); + + std::cout << std::endl << ">>> Alternatively, use declareDatatype" << std::endl; + std::cout << std::endl; + + std::vector<DatatypeConstructorDecl> ctors = { cons, nil }; + Sort consListSort2 = slv.declareDatatype("list2", ctors); + test(slv, consListSort2); + return 0; } |