summaryrefslogtreecommitdiff
path: root/examples/api/datatypes.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'examples/api/datatypes.cpp')
-rw-r--r--examples/api/datatypes.cpp189
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;
}
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback