diff options
Diffstat (limited to 'examples/api/datatypes.cpp')
-rw-r--r-- | examples/api/datatypes.cpp | 189 |
1 files changed, 109 insertions, 80 deletions
diff --git a/examples/api/datatypes.cpp b/examples/api/datatypes.cpp index a749f0a0f..dd2c2695d 100644 --- a/examples/api/datatypes.cpp +++ b/examples/api/datatypes.cpp @@ -2,9 +2,9 @@ /*! \file datatypes.cpp ** \verbatim ** Top contributors (to current version): - ** Morgan Deters, Aina Niemetz + ** Aina Niemetz, Andrew Reynolds, Makai Mann ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim @@ -16,135 +16,164 @@ #include <iostream> -#include <cvc4/cvc4.h> +#include <cvc4/api/cvc4cpp.h> -using namespace CVC4; - -int main() { - ExprManager em; - SmtEngine smt(&em); - - // 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"---at which point function - // symbols are assigned to its constructors, selectors, and testers. - - Datatype consListSpec(&em, "list"); // give the datatype a name - DatatypeConstructor cons("cons"); - cons.addArg("head", em.integerType()); - cons.addArg("tail", DatatypeSelfType()); // a list - consListSpec.addConstructor(cons); - DatatypeConstructor nil("nil"); - consListSpec.addConstructor(nil); - - std::cout << "spec is:" << std::endl - << consListSpec << std::endl; - - // Keep in mind that "Datatype" is the specification class for - // datatypes---"Datatype" is not itself a CVC4 Type. Now that - // our Datatype is fully specified, we can get a Type for it. - // This step resolves the "SelfType" reference and creates - // symbols for all the constructors, etc. - - DatatypeType consListType = em.mkDatatypeType(consListSpec); +using namespace CVC4::api; +void test(Solver& slv, Sort& consListSort) +{ // 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 DatatypeType, and + // the complete spec for the datatype from the DatatypeSort, and // this Datatype object has constructor symbols (and others) filled in. - const Datatype& consList = consListType.getDatatype(); + const Datatype& consList = consListSort.getDatatype(); - // e = cons 0 nil + // t = cons 0 nil // // Here, consList["cons"] gives you the DatatypeConstructor. To get // the constructor symbol for application, use .getConstructor("cons"), // which is equivalent to consList["cons"].getConstructor(). Note that // "nil" is a constructor too, so it needs to be applied with // APPLY_CONSTRUCTOR, even though it has no arguments. - Expr e = em.mkExpr(kind::APPLY_CONSTRUCTOR, - consList.getConstructor("cons"), - em.mkConst(Rational(0)), - em.mkExpr(kind::APPLY_CONSTRUCTOR, - consList.getConstructor("nil"))); - - std::cout << "e is " << e << std::endl - << "type of cons is " << consList.getConstructor("cons").getType() - << std::endl - << "type of nil is " << consList.getConstructor("nil").getType() + Term t = slv.mkTerm( + APPLY_CONSTRUCTOR, + consList.getConstructorTerm("cons"), + slv.mkReal(0), + slv.mkTerm(APPLY_CONSTRUCTOR, consList.getConstructorTerm("nil"))); + + std::cout << "t is " << t << std::endl + << "sort of cons is " + << consList.getConstructorTerm("cons").getSort() << std::endl + << "sort of nil is " << consList.getConstructorTerm("nil").getSort() << std::endl; - // e2 = head(cons 0 nil), and of course this can be evaluated + // t2 = head(cons 0 nil), and of course this can be evaluated // // Here we first get the DatatypeConstructor for cons (with // consList["cons"]) in order to get the "head" selector symbol // to apply. - Expr e2 = em.mkExpr(kind::APPLY_SELECTOR, - consList["cons"].getSelector("head"), - e); + Term t2 = + slv.mkTerm(APPLY_SELECTOR, consList["cons"].getSelectorTerm("head"), t); - std::cout << "e2 is " << e2 << std::endl - << "simplify(e2) is " << smt.simplify(e2) - << std::endl << std::endl; + std::cout << "t2 is " << t2 << 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::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::iterator j = (*i).begin(); j != (*i).end(); ++j) { + for (DatatypeConstructor::const_iterator j = (*i).begin(); j != (*i).end(); + ++j) + { std::cout << " + arg: " << *j << std::endl; } } std::cout << std::endl; + // Alternatively, you can use for each loops. + for (const auto& c : consList) + { + std::cout << "ctor: " << c << std::endl; + for (const auto& s : c) + { + std::cout << " + arg: " << s << std::endl; + } + } + std::cout << std::endl; + // You can also define parameterized datatypes. // This example builds a simple parameterized list of sort T, with one // constructor "cons". - Type sort = em.mkSort("T", ExprManager::SORT_FLAG_PLACEHOLDER); - Datatype paramConsListSpec(&em, "list", std::vector<Type>{sort}); - DatatypeConstructor paramCons("cons"); - DatatypeConstructor paramNil("nil"); - paramCons.addArg("head", sort); - paramCons.addArg("tail", DatatypeSelfType()); + Sort sort = slv.mkParamSort("T"); + DatatypeDecl paramConsListSpec = + slv.mkDatatypeDecl("paramlist", + sort); // give the datatype a name + DatatypeConstructorDecl paramCons = slv.mkDatatypeConstructorDecl("cons"); + DatatypeConstructorDecl paramNil = slv.mkDatatypeConstructorDecl("nil"); + paramCons.addSelector("head", sort); + paramCons.addSelectorSelf("tail"); paramConsListSpec.addConstructor(paramCons); paramConsListSpec.addConstructor(paramNil); - DatatypeType paramConsListType = em.mkDatatypeType(paramConsListSpec); - Type paramConsIntListType = paramConsListType.instantiate(std::vector<Type>{em.integerType()}); + Sort paramConsListSort = slv.mkDatatypeSort(paramConsListSpec); + Sort paramConsIntListSort = + paramConsListSort.instantiate(std::vector<Sort>{slv.getIntegerSort()}); - const Datatype& paramConsList = paramConsListType.getDatatype(); + const Datatype& paramConsList = paramConsListSort.getDatatype(); std::cout << "parameterized datatype sort is " << std::endl; for (const DatatypeConstructor& ctor : paramConsList) { std::cout << "ctor: " << ctor << std::endl; - for (const DatatypeConstructorArg& stor : ctor) + for (const DatatypeSelector& stor : ctor) { std::cout << " + arg: " << stor << std::endl; } } - Expr a = em.mkVar("a", paramConsIntListType); - std::cout << "Expr " << a << " is of type " << a.getType() << std::endl; + Term a = slv.mkConst(paramConsIntListSort, "a"); + std::cout << "term " << a << " is of sort " << a.getSort() << std::endl; - Expr head_a = em.mkExpr( - kind::APPLY_SELECTOR, - paramConsList["cons"].getSelector("head"), - a); - std::cout << "head_a is " << head_a << " of type " << head_a.getType() + 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::endl - << "type of cons is " - << paramConsList.getConstructor("cons").getType() << std::endl + << "sort of cons is " + << paramConsList.getConstructorTerm("cons").getSort() << std::endl << std::endl; - - Expr assertion = em.mkExpr(kind::GT, head_a, em.mkConst(Rational(50))); + Term assertion = slv.mkTerm(GT, head_a, slv.mkReal(50)); std::cout << "Assert " << assertion << std::endl; - smt.assertFormula(assertion); - + slv.assertFormula(assertion); std::cout << "Expect sat." << std::endl; - std::cout << "CVC4: " << smt.checkSat()<< 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 = + slv.mkDatatypeDecl("list"); // give the datatype a name + DatatypeConstructorDecl cons = slv.mkDatatypeConstructorDecl("cons"); + cons.addSelector("head", slv.getIntegerSort()); + cons.addSelectorSelf("tail"); + consListSpec.addConstructor(cons); + DatatypeConstructorDecl nil = slv.mkDatatypeConstructorDecl("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; + + DatatypeConstructorDecl cons2 = slv.mkDatatypeConstructorDecl("cons"); + cons2.addSelector("head", slv.getIntegerSort()); + cons2.addSelectorSelf("tail"); + DatatypeConstructorDecl nil2 = slv.mkDatatypeConstructorDecl("nil"); + std::vector<DatatypeConstructorDecl> ctors = {cons2, nil2}; + Sort consListSort2 = slv.declareDatatype("list2", ctors); + test(slv, consListSort2); return 0; } |