Theory of Datatypes

examples/api/cpp/datatypes.cpp

  1/******************************************************************************
  2 * Top contributors (to current version):
  3 *   Aina Niemetz, Morgan Deters, Andrew Reynolds
  4 *
  5 * This file is part of the cvc5 project.
  6 *
  7 * Copyright (c) 2009-2024 by the authors listed in the file AUTHORS
  8 * in the top-level source directory and their institutional affiliations.
  9 * All rights reserved.  See the file COPYING in the top-level source
 10 * directory for licensing information.
 11 * ****************************************************************************
 12 *
 13 * An example of using inductive datatypes in cvc5.
 14 */
 15
 16#include <cvc5/cvc5.h>
 17
 18#include <iostream>
 19
 20using namespace cvc5;
 21
 22void test(Solver& slv, Sort& consListSort)
 23{
 24  TermManager& tm = slv.getTermManager();
 25
 26  // Now our old "consListSpec" is useless--the relevant information
 27  // has been copied out, so we can throw that spec away.  We can get
 28  // the complete spec for the datatype from the DatatypeSort, and
 29  // this Datatype object has constructor symbols (and others) filled in.
 30
 31  const Datatype& consList = consListSort.getDatatype();
 32
 33  // t = cons 0 nil
 34  //
 35  // Here, consList["cons"] gives you the DatatypeConstructor.  To get
 36  // the constructor symbol for application, use .getConstructor("cons"),
 37  // which is equivalent to consList["cons"].getConstructor().  Note that
 38  // "nil" is a constructor too, so it needs to be applied with
 39  // APPLY_CONSTRUCTOR, even though it has no arguments.
 40  Term t = tm.mkTerm(Kind::APPLY_CONSTRUCTOR,
 41                     {consList.getConstructor("cons").getTerm(),
 42                      tm.mkInteger(0),
 43                      tm.mkTerm(Kind::APPLY_CONSTRUCTOR,
 44                                {consList.getConstructor("nil").getTerm()})});
 45
 46  std::cout << "t is " << t << std::endl
 47            << "sort of cons is "
 48            << consList.getConstructor("cons").getTerm().getSort() << std::endl
 49            << "sort of nil is "
 50            << consList.getConstructor("nil").getTerm().getSort() << std::endl;
 51
 52  // t2 = head(cons 0 nil), and of course this can be evaluated
 53  //
 54  // Here we first get the DatatypeConstructor for cons (with
 55  // consList["cons"]) in order to get the "head" selector symbol
 56  // to apply.
 57  Term t2 = tm.mkTerm(Kind::APPLY_SELECTOR,
 58                      {consList["cons"].getSelector("head").getTerm(), t});
 59
 60  std::cout << "t2 is " << t2 << std::endl
 61            << "simplify(t2) is " << slv.simplify(t2) << std::endl
 62            << std::endl;
 63
 64  // You can also iterate over a Datatype to get all its constructors,
 65  // and over a DatatypeConstructor to get all its "args" (selectors)
 66  for (Datatype::const_iterator i = consList.begin(); i != consList.end(); ++i)
 67  {
 68    std::cout << "ctor: " << *i << std::endl;
 69    for (DatatypeConstructor::const_iterator j = (*i).begin(); j != (*i).end();
 70         ++j)
 71    {
 72      std::cout << " + arg: " << *j << std::endl;
 73    }
 74  }
 75  std::cout << std::endl;
 76
 77  // Alternatively, you can use for each loops.
 78  for (const auto& c : consList)
 79  {
 80    std::cout << "ctor: " << c << std::endl;
 81    for (const auto& s : c)
 82    {
 83      std::cout << " + arg: " << s << std::endl;
 84    }
 85  }
 86  std::cout << std::endl;
 87
 88  // You can also define a tester term for constructor 'cons': (_ is cons)
 89  Term t_is_cons =
 90      tm.mkTerm(Kind::APPLY_TESTER, {consList["cons"].getTesterTerm(), t});
 91  std::cout << "t_is_cons is " << t_is_cons << std::endl << std::endl;
 92  slv.assertFormula(t_is_cons);
 93  // Updating t at 'head' with value 1 is defined as follows:
 94  Term t_updated = tm.mkTerm(
 95      Kind::APPLY_UPDATER,
 96      {consList["cons"]["head"].getUpdaterTerm(), t, tm.mkInteger(1)});
 97  std::cout << "t_updated is " << t_updated << std::endl << std::endl;
 98  slv.assertFormula(tm.mkTerm(Kind::DISTINCT, {t, t_updated}));
 99
100  // You can also define parameterized datatypes.
101  // This example builds a simple parameterized list of sort T, with one
102  // constructor "cons".
103  Sort sort = tm.mkParamSort("T");
104  DatatypeDecl paramConsListSpec =
105      tm.mkDatatypeDecl("paramlist", {sort});  // give the datatype a name
106  DatatypeConstructorDecl paramCons = tm.mkDatatypeConstructorDecl("cons");
107  DatatypeConstructorDecl paramNil = tm.mkDatatypeConstructorDecl("nil");
108  paramCons.addSelector("head", sort);
109  paramCons.addSelectorSelf("tail");
110  paramConsListSpec.addConstructor(paramCons);
111  paramConsListSpec.addConstructor(paramNil);
112
113  Sort paramConsListSort = tm.mkDatatypeSort(paramConsListSpec);
114  Sort paramConsIntListSort =
115      paramConsListSort.instantiate(std::vector<Sort>{tm.getIntegerSort()});
116
117  const Datatype& paramConsList = paramConsListSort.getDatatype();
118
119  std::cout << "parameterized datatype sort is" << std::endl;
120  for (const DatatypeConstructor& ctor : paramConsList)
121  {
122    std::cout << "ctor: " << ctor << std::endl;
123    for (const DatatypeSelector& stor : ctor)
124    {
125      std::cout << " + arg: " << stor << std::endl;
126    }
127  }
128
129  Term a = tm.mkConst(paramConsIntListSort, "a");
130  std::cout << "term " << a << " is of sort " << a.getSort() << std::endl;
131
132  Term head_a =
133      tm.mkTerm(Kind::APPLY_SELECTOR,
134                {paramConsList["cons"].getSelector("head").getTerm(), a});
135  std::cout << "head_a is " << head_a << " of sort " << head_a.getSort()
136            << std::endl
137            << "sort of cons is "
138            << paramConsList.getConstructor("cons").getTerm().getSort()
139            << std::endl
140            << std::endl;
141
142  Term assertion = tm.mkTerm(Kind::GT, {head_a, tm.mkInteger(50)});
143  std::cout << "Assert " << assertion << std::endl;
144  slv.assertFormula(assertion);
145  std::cout << "Expect sat." << std::endl;
146  std::cout << "cvc5: " << slv.checkSat() << std::endl;
147}
148
149int main()
150{
151  TermManager tm;
152  Solver slv(tm);
153  // This example builds a simple "cons list" of integers, with
154  // two constructors, "cons" and "nil."
155
156  // Building a datatype consists of two steps.
157  // First, the datatype is specified.
158  // Second, it is "resolved" to an actual sort, at which point function
159  // symbols are assigned to its constructors, selectors, and testers.
160
161  DatatypeDecl consListSpec =
162      tm.mkDatatypeDecl("list");  // give the datatype a name
163  DatatypeConstructorDecl cons = tm.mkDatatypeConstructorDecl("cons");
164  cons.addSelector("head", tm.getIntegerSort());
165  cons.addSelectorSelf("tail");
166  consListSpec.addConstructor(cons);
167  DatatypeConstructorDecl nil = tm.mkDatatypeConstructorDecl("nil");
168  consListSpec.addConstructor(nil);
169
170  std::cout << "spec is:" << std::endl << consListSpec << std::endl;
171
172  // Keep in mind that "DatatypeDecl" is the specification class for
173  // datatypes---"DatatypeDecl" is not itself a cvc5 Sort.
174  // Now that our Datatype is fully specified, we can get a Sort for it.
175  // This step resolves the "SelfSort" reference and creates
176  // symbols for all the constructors, etc.
177
178  Sort consListSort = tm.mkDatatypeSort(consListSpec);
179
180  test(slv, consListSort);
181
182  std::cout << std::endl
183            << ">>> Alternatively, use declareDatatype" << std::endl;
184  std::cout << std::endl;
185
186  DatatypeConstructorDecl cons2 = tm.mkDatatypeConstructorDecl("cons");
187  cons2.addSelector("head", tm.getIntegerSort());
188  cons2.addSelectorSelf("tail");
189  DatatypeConstructorDecl nil2 = tm.mkDatatypeConstructorDecl("nil");
190  std::vector<DatatypeConstructorDecl> ctors = {cons2, nil2};
191  Sort consListSort2 = slv.declareDatatype("list2", ctors);
192  test(slv, consListSort2);
193
194  return 0;
195}