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-2025 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}
1/******************************************************************************
2 * Top contributors (to current version):
3 * Aina Niemetz, Morgan Deters, Haniel Barbosa
4 *
5 * This file is part of the cvc5 project.
6 *
7 * Copyright (c) 2009-2025 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/c/cvc5.h>
17#include <stdio.h>
18
19void test(Cvc5TermManager* tm, Cvc5* slv, Cvc5Sort cons_list_sort)
20{
21 // Now our old "cons_list_decl" is useless--the relevant information
22 // has been copied out, so we can throw that spec away. We can get
23 // the complete spec for the datatype from the DatatypeSort, and
24 // this Datatype object has constructor symbols (and others) filled in.
25
26 Cvc5Datatype cons_list = cvc5_sort_get_datatype(cons_list_sort);
27
28 // t = cons 0 nil
29 //
30 // Here, cvc5_dt_cons_get_constructor_by_name(cons_list, "cons") gives you
31 // the Cvc5DatatypeConstructor. Note that "nil" is a constructor too, so it
32 // needs to be applied with CVC5_KIND_APPLY_CONSTRUCTOR, even though it has
33 // no arguments.
34 Cvc5Term nil_term =
35 cvc5_dt_cons_get_term(cvc5_dt_get_constructor_by_name(cons_list, "nil"));
36 Cvc5DatatypeConstructor cons =
37 cvc5_dt_get_constructor_by_name(cons_list, "cons");
38 Cvc5Term cons_term = cvc5_dt_cons_get_term(cons);
39 Cvc5Term args1[1] = {nil_term};
40 Cvc5Term args3[3] = {cons_term,
41 cvc5_mk_integer_int64(tm, 0),
42 cvc5_mk_term(tm, CVC5_KIND_APPLY_CONSTRUCTOR, 1, args1)};
43 Cvc5Term t = cvc5_mk_term(tm, CVC5_KIND_APPLY_CONSTRUCTOR, 3, args3);
44
45 printf("t is %s\n", cvc5_term_to_string(t));
46 printf("sort of cons is %s\n",
47 cvc5_sort_to_string(cvc5_term_get_sort(cons_term)));
48 printf("sort of nil is %s\n",
49 cvc5_sort_to_string(cvc5_term_get_sort(nil_term)));
50
51 // t2 = head(cons 0 nil), and of course this can be evaluated
52 //
53 // Here we first get the DatatypeConstructor for cons (with
54 // cvc5_dt_cons_get_constructor_by_name(cons_list, "cons") in order to get
55 // the "head" selector symbol to apply.
56 Cvc5DatatypeSelector head = cvc5_dt_cons_get_selector_by_name(cons, "head");
57 Cvc5Term args2[2] = {cvc5_dt_sel_get_term(head), t};
58 Cvc5Term t2 = cvc5_mk_term(tm, CVC5_KIND_APPLY_SELECTOR, 2, args2);
59
60 printf("t2 is %s\n", cvc5_term_to_string(t2));
61 printf("simplify(t2) is %s\n\n",
62 cvc5_term_to_string(cvc5_simplify(slv, t2, false)));
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 (size_t i = 0, n = cvc5_dt_get_num_constructors(cons_list); i < n; ++i)
67 {
68 Cvc5DatatypeConstructor dtcons = cvc5_dt_get_constructor(cons_list, i);
69 printf("ctor: %s\n", cvc5_dt_cons_to_string(dtcons));
70 for (size_t j = 0, m = cvc5_dt_cons_get_num_selectors(dtcons); j < m; ++j)
71 {
72 Cvc5DatatypeSelector dtsel = cvc5_dt_cons_get_selector(dtcons, j);
73 printf(" + arg: %s\n", cvc5_dt_sel_to_string(dtsel));
74 }
75 }
76 printf("\n");
77
78 // You can also define a tester term for constructor 'cons': (_ is cons)
79 args2[0] = cvc5_dt_cons_get_tester_term(cons);
80 args2[1] = t;
81 Cvc5Term t_is_cons = cvc5_mk_term(tm, CVC5_KIND_APPLY_TESTER, 2, args2);
82 printf("t_is_cons is %s\n\n", cvc5_term_to_string(t_is_cons));
83 cvc5_assert_formula(slv, t_is_cons);
84 // Updating t at 'head' with value 1 is defined as follows:
85 args3[0] = cvc5_dt_sel_get_updater_term(head);
86 args3[1] = t;
87 args3[2] = cvc5_mk_integer_int64(tm, 1);
88 Cvc5Term t_updated = cvc5_mk_term(tm, CVC5_KIND_APPLY_UPDATER, 3, args3);
89 printf("t_updated is %s\n\n", cvc5_term_to_string(t_updated));
90 args2[0] = t;
91 args2[1] = t_updated;
92 cvc5_assert_formula(slv, cvc5_mk_term(tm, CVC5_KIND_DISTINCT, 2, args2));
93
94 // You can also define parameterized datatypes.
95 // This example builds a simple parameterized list of sort T, with one
96 // constructor "cons".
97 Cvc5Sort sort = cvc5_mk_param_sort(tm, "T");
98 Cvc5Sort sorts[1] = {sort};
99 Cvc5DatatypeDecl param_cons_list_decl =
100 cvc5_mk_dt_decl_with_params(tm, "paramlist", 1, sorts, false);
101 Cvc5DatatypeConstructorDecl param_cons = cvc5_mk_dt_cons_decl(tm, "cons");
102 Cvc5DatatypeConstructorDecl param_nil = cvc5_mk_dt_cons_decl(tm, "nil");
103 cvc5_dt_cons_decl_add_selector(param_cons, "head", sort);
104 cvc5_dt_cons_decl_add_selector_self(param_cons, "tail");
105 cvc5_dt_decl_add_constructor(param_cons_list_decl, param_cons);
106 cvc5_dt_decl_add_constructor(param_cons_list_decl, param_nil);
107
108 Cvc5Sort param_cons_list_sort = cvc5_mk_dt_sort(tm, param_cons_list_decl);
109 sorts[0] = cvc5_get_integer_sort(tm);
110 Cvc5Sort param_cons_int_list_sort =
111 cvc5_sort_instantiate(param_cons_list_sort, 1, sorts);
112
113 Cvc5Datatype param_cons_list = cvc5_sort_get_datatype(param_cons_list_sort);
114
115 printf("parameterized datatype sort is\n");
116 for (size_t i = 0, n = cvc5_dt_get_num_constructors(param_cons_list); i < n;
117 ++i)
118 {
119 Cvc5DatatypeConstructor dtcons =
120 cvc5_dt_get_constructor(param_cons_list, i);
121 printf("ctor: %s\n", cvc5_dt_cons_to_string(dtcons));
122 for (size_t j = 0, m = cvc5_dt_cons_get_num_selectors(dtcons); j < m; ++j)
123 {
124 Cvc5DatatypeSelector dtsel = cvc5_dt_cons_get_selector(dtcons, j);
125 printf(" + arg: %s\n", cvc5_dt_sel_to_string(dtsel));
126 }
127 }
128
129 Cvc5Term a = cvc5_mk_const(tm, param_cons_int_list_sort, "a");
130 printf("term %s is of sort %s\n",
131 cvc5_term_to_string(a),
132 cvc5_sort_to_string(cvc5_term_get_sort(a)));
133
134 args2[0] = cvc5_dt_sel_get_term(cvc5_dt_cons_get_selector_by_name(
135 cvc5_dt_get_constructor_by_name(param_cons_list, "cons"), "head"));
136 args2[1] = a;
137 Cvc5Term head_a = cvc5_mk_term(tm, CVC5_KIND_APPLY_SELECTOR, 2, args2);
138
139 printf("head_a is %s of sort %s\n",
140 cvc5_term_to_string(head_a),
141 cvc5_sort_to_string(cvc5_term_get_sort(head_a)));
142 printf("sort of cons is %s\n\n",
143 cvc5_sort_to_string(cvc5_term_get_sort(cvc5_dt_cons_get_term(
144 cvc5_dt_get_constructor_by_name(param_cons_list, "cons")))));
145
146 args2[0] = head_a;
147 args2[1] = cvc5_mk_integer_int64(tm, 50);
148 Cvc5Term assertion = cvc5_mk_term(tm, CVC5_KIND_GT, 2, args2);
149 printf("Assert %s\n", cvc5_term_to_string(assertion));
150 cvc5_assert_formula(slv, assertion);
151 printf("Expect sat.\n");
152 printf("cvc5: %s\n", cvc5_result_to_string(cvc5_check_sat(slv)));
153}
154
155int main()
156{
157 Cvc5TermManager* tm = cvc5_term_manager_new();
158 Cvc5* slv = cvc5_new(tm);
159 // This example builds a simple "cons list" of integers, with
160 // two constructors, "cons" and "nil."
161
162 // Building a datatype consists of two steps.
163 // First, the datatype is specified.
164 // Second, it is "resolved" to an actual sort, at which point function
165 // symbols are assigned to its constructors, selectors, and testers.
166
167 Cvc5DatatypeDecl cons_list_decl = cvc5_mk_dt_decl(tm, "list", false);
168 Cvc5DatatypeConstructorDecl cons = cvc5_mk_dt_cons_decl(tm, "cons");
169 cvc5_dt_cons_decl_add_selector(cons, "head", cvc5_get_integer_sort(tm));
170 cvc5_dt_cons_decl_add_selector_self(cons, "tail");
171 cvc5_dt_decl_add_constructor(cons_list_decl, cons);
172 Cvc5DatatypeConstructorDecl nil = cvc5_mk_dt_cons_decl(tm, "nil");
173 cvc5_dt_decl_add_constructor(cons_list_decl, nil);
174
175 printf("spec is:\n");
176 printf("%s\n", cvc5_dt_decl_to_string(cons_list_decl));
177
178 // Keep in mind that "DatatypeDecl" is the specification class for
179 // datatypes---"DatatypeDecl" is not itself a cvc5 Sort.
180 // Now that our Datatype is fully specified, we can get a Sort for it.
181 // This step resolves the "SelfSort" reference and creates
182 // symbols for all the constructors, etc.
183
184 Cvc5Sort cons_list_sort = cvc5_mk_dt_sort(tm, cons_list_decl);
185
186 test(tm, slv, cons_list_sort);
187
188 printf("\n");
189 printf(">>> Alternatively, use cvc5_declare_dt\n\n");
190
191 Cvc5DatatypeConstructorDecl cons2 = cvc5_mk_dt_cons_decl(tm, "cons");
192 cvc5_dt_cons_decl_add_selector(cons2, "head", cvc5_get_integer_sort(tm));
193 cvc5_dt_cons_decl_add_selector_self(cons2, "tail");
194 Cvc5DatatypeConstructorDecl nil2 = cvc5_mk_dt_cons_decl(tm, "nil");
195 Cvc5DatatypeConstructorDecl ctors[2] = {cons2, nil2};
196 Cvc5Sort cons_list_sort2 = cvc5_declare_dt(slv, "list2", 2, ctors);
197 test(tm, slv, cons_list_sort2);
198
199 cvc5_delete(slv);
200 cvc5_term_manager_delete(tm);
201 return 0;
202}
examples/api/java/Datatypes.java
1/******************************************************************************
2 * Top contributors (to current version):
3 * Mudathir Mohamed, Daniel Larraz, Morgan Deters
4 *
5 * This file is part of the cvc5 project.
6 *
7 * Copyright (c) 2009-2025 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
16import io.github.cvc5.*;
17import java.util.Iterator;
18
19public class Datatypes
20{
21 private static void test(Solver slv, Sort consListSort) throws CVC5ApiException
22 {
23 TermManager tm = slv.getTermManager();
24
25 // Now our old "consListSpec" is useless--the relevant information
26 // has been copied out, so we can throw that spec away. We can get
27 // the complete spec for the datatype from the DatatypeSort, and
28 // this Datatype object has constructor symbols (and others) filled in.
29
30 Datatype consList = consListSort.getDatatype();
31
32 // t = cons 0 nil
33 //
34 // Here, consList["cons"] gives you the DatatypeConstructor. To get
35 // the constructor symbol for application, use .getConstructor("cons"),
36 // which is equivalent to consList["cons"].getConstructor(). Note that
37 // "nil" is a constructor too, so it needs to be applied with
38 // APPLY_CONSTRUCTOR, even though it has no arguments.
39 Term t = tm.mkTerm(Kind.APPLY_CONSTRUCTOR,
40 consList.getConstructor("cons").getTerm(),
41 tm.mkInteger(0),
42 tm.mkTerm(Kind.APPLY_CONSTRUCTOR, consList.getConstructor("nil").getTerm()));
43
44 System.out.println("t is " + t + "\n"
45 + "sort of cons is " + consList.getConstructor("cons").getTerm().getSort() + "\n"
46 + "sort of nil is " + consList.getConstructor("nil").getTerm().getSort());
47
48 // t2 = head(cons 0 nil), and of course this can be evaluated
49 //
50 // Here we first get the DatatypeConstructor for cons (with
51 // consList["cons"]) in order to get the "head" selector symbol
52 // to apply.
53 Term t2 = tm.mkTerm(
54 Kind.APPLY_SELECTOR, consList.getConstructor("cons").getSelector("head").getTerm(), t);
55
56 System.out.println("t2 is " + t2 + "\n"
57 + "simplify(t2) is " + slv.simplify(t2) + "\n");
58
59 // You can also iterate over a Datatype to get all its constructors,
60 // and over a DatatypeConstructor to get all its "args" (selectors)
61
62 for (Iterator<DatatypeConstructor> i = consList.iterator(); i.hasNext();)
63 {
64 DatatypeConstructor constructor = i.next();
65 System.out.println("ctor: " + constructor);
66 for (Iterator<DatatypeSelector> j = constructor.iterator(); j.hasNext();)
67 {
68 System.out.println(" + arg: " + j.next());
69 }
70 }
71 System.out.println();
72
73 // Alternatively, you can use for each loops.
74 for (DatatypeConstructor c : consList)
75 {
76 System.out.println("ctor: " + c);
77 for (DatatypeSelector s : c)
78 {
79 System.out.println(" + arg: " + s);
80 }
81 }
82 System.out.println();
83
84 // You can also define a tester term for constructor 'cons': (_ is cons)
85 Term t_is_cons =
86 tm.mkTerm(Kind.APPLY_TESTER, consList.getConstructor("cons").getTesterTerm(), t);
87 System.out.println("t_is_cons is " + t_is_cons + "\n");
88 slv.assertFormula(t_is_cons);
89 // Updating t at 'head' with value 1 is defined as follows:
90 Term t_updated = tm.mkTerm(Kind.APPLY_UPDATER,
91 consList.getConstructor("cons").getSelector("head").getUpdaterTerm(),
92 t,
93 tm.mkInteger(1));
94 System.out.println("t_updated is " + t_updated + "\n");
95 slv.assertFormula(tm.mkTerm(Kind.DISTINCT, t, t_updated));
96
97 // You can also define parameterized datatypes.
98 // This example builds a simple parameterized list of sort T, with one
99 // constructor "cons".
100 Sort sort = tm.mkParamSort("T");
101 DatatypeDecl paramConsListSpec =
102 tm.mkDatatypeDecl("paramlist", new Sort[] {sort}); // give the datatype a name
103 DatatypeConstructorDecl paramCons = tm.mkDatatypeConstructorDecl("cons");
104 DatatypeConstructorDecl paramNil = tm.mkDatatypeConstructorDecl("nil");
105 paramCons.addSelector("head", sort);
106 paramCons.addSelectorSelf("tail");
107 paramConsListSpec.addConstructor(paramCons);
108 paramConsListSpec.addConstructor(paramNil);
109
110 Sort paramConsListSort = tm.mkDatatypeSort(paramConsListSpec);
111 Sort paramConsIntListSort = paramConsListSort.instantiate(new Sort[] {tm.getIntegerSort()});
112
113 Datatype paramConsList = paramConsListSort.getDatatype();
114
115 System.out.println("parameterized datatype sort is ");
116 for (DatatypeConstructor ctor : paramConsList)
117 {
118 System.out.println("ctor: " + ctor);
119 for (DatatypeSelector stor : ctor)
120 {
121 System.out.println(" + arg: " + stor);
122 }
123 }
124
125 Term a = tm.mkConst(paramConsIntListSort, "a");
126 System.out.println("term " + a + " is of sort " + a.getSort());
127
128 Term head_a = tm.mkTerm(
129 Kind.APPLY_SELECTOR, paramConsList.getConstructor("cons").getSelector("head").getTerm(), a);
130 System.out.println("head_a is " + head_a + " of sort " + head_a.getSort() + "\n"
131 + "sort of cons is " + paramConsList.getConstructor("cons").getTerm().getSort() + "\n");
132 Term assertion = tm.mkTerm(Kind.GT, head_a, tm.mkInteger(50));
133 System.out.println("Assert " + assertion);
134 slv.assertFormula(assertion);
135 System.out.println("Expect sat.");
136 System.out.println("cvc5: " + slv.checkSat());
137 }
138
139 public static void main(String[] args) throws CVC5ApiException
140 {
141 TermManager tm = new TermManager();
142 Solver slv = new Solver(tm);
143 {
144 // This example builds a simple "cons list" of integers, with
145 // two constructors, "cons" and "nil."
146
147 // Building a datatype consists of two steps.
148 // First, the datatype is specified.
149 // Second, it is "resolved" to an actual sort, at which point function
150 // symbols are assigned to its constructors, selectors, and testers.
151
152 DatatypeDecl consListSpec = tm.mkDatatypeDecl("list"); // give the datatype a name
153 DatatypeConstructorDecl cons = tm.mkDatatypeConstructorDecl("cons");
154 cons.addSelector("head", tm.getIntegerSort());
155 cons.addSelectorSelf("tail");
156 consListSpec.addConstructor(cons);
157 DatatypeConstructorDecl nil = tm.mkDatatypeConstructorDecl("nil");
158 consListSpec.addConstructor(nil);
159
160 System.out.println("spec is:"
161 + "\n" + consListSpec);
162
163 // Keep in mind that "DatatypeDecl" is the specification class for
164 // datatypes---"DatatypeDecl" is not itself a cvc5 Sort.
165 // Now that our Datatype is fully specified, we can get a Sort for it.
166 // This step resolves the "SelfSort" reference and creates
167 // symbols for all the constructors, etc.
168
169 Sort consListSort = tm.mkDatatypeSort(consListSpec);
170
171 test(slv, consListSort);
172
173 System.out.println("\n"
174 + ">>> Alternatively, use declareDatatype");
175 System.out.println();
176
177 DatatypeConstructorDecl cons2 = tm.mkDatatypeConstructorDecl("cons");
178 cons2.addSelector("head", tm.getIntegerSort());
179 cons2.addSelectorSelf("tail");
180 DatatypeConstructorDecl nil2 = tm.mkDatatypeConstructorDecl("nil");
181 DatatypeConstructorDecl[] ctors = new DatatypeConstructorDecl[] {cons2, nil2};
182 Sort consListSort2 = slv.declareDatatype("list2", ctors);
183 test(slv, consListSort2);
184 }
185 Context.deletePointers();
186 }
187}
examples/api/python/pythonic/datatypes.py
1###############################################################################
2# Top contributors (to current version):
3# Alex Ozdemir
4#
5# This file is part of the cvc5 project.
6#
7# Copyright (c) 2009-2025 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##
15from cvc5.pythonic import *
16
17if __name__ == '__main__':
18 # This example builds a simple "cons list" of integers, with
19 # two constructors, "cons" and "nil."
20
21 # Building a datatype consists of two steps.
22 # First, the datatype is specified.
23 # Second, it is "resolved" to an actual sort, at which point function
24 # symbols are assigned to its constructors, selectors, and testers.
25
26 decl = Datatype("list")
27 decl.declare("cons", ("head", IntSort()), ("tail", decl))
28 decl.declare("nil")
29 List = decl.create()
30
31 # Using constructors and selectors:
32 t = List.cons(0, List.nil)
33 print("t is:", t)
34 print("head of t is:", List.head(t))
35 print("after simplify:", simplify(List.head(t)))
36 print()
37
38 # You can iterate over constructors and selectors
39 for i in range(List.num_constructors()):
40 ctor = List.constructor(i)
41 print("ctor:", ctor)
42 for j in range(ctor.arity()):
43 print(" + arg:", ctor.domain(j))
44 print(" + selector:", List.accessor(i, j))
45 print()
46
47 # You can use testers
48 print("t is a 'cons':", simplify(List.is_cons(t)))
49 print()
50
51 # This Python API does not support type parameters or updators for
52 # datatypes. See the base Python API for those features, or construct them
53 # using Python functions/classes.
54
55 a = Int('a')
56 solve(List.head(List.cons(a, List.nil)) > 50)
57
58 prove(Not(List.is_nil(List.cons(a, List.nil))))
examples/api/python/datatypes.py
1#!/usr/bin/env python
2###############################################################################
3# Top contributors (to current version):
4# Makai Mann, Aina Niemetz, Andrew Reynolds
5#
6# This file is part of the cvc5 project.
7#
8# Copyright (c) 2009-2025 by the authors listed in the file AUTHORS
9# in the top-level source directory and their institutional affiliations.
10# All rights reserved. See the file COPYING in the top-level source
11# directory for licensing information.
12# #############################################################################
13#
14# A simple demonstration of the solving capabilities of the cvc5 datatypes
15# solver through the Python API. This is a direct translation of
16# datatypes-new.cpp.
17##
18
19import cvc5
20from cvc5 import Kind
21
22def test(slv, consListSort):
23 # Now our old "consListSpec" is useless--the relevant information
24 # has been copied out, so we can throw that spec away. We can get
25 # the complete spec for the datatype from the DatatypeSort, and
26 # this Datatype object has constructor symbols (and others) filled in.
27
28 tm = slv.getTermManager()
29
30 consList = consListSort.getDatatype()
31
32 # t = cons 0 nil
33 #
34 # Here, consList["cons"] gives you the DatatypeConstructor. To get
35 # the constructor symbol for application, use .getConstructor("cons"),
36 # which is equivalent to consList["cons"].getConstructor(). Note that
37 # "nil" is a constructor too
38
39 t = tm.mkTerm(
40 Kind.APPLY_CONSTRUCTOR,
41 consList.getConstructor("cons").getTerm(),
42 tm.mkInteger(0),
43 tm.mkTerm(
44 Kind.APPLY_CONSTRUCTOR,
45 consList.getConstructor("nil").getTerm()))
46
47 print("t is {}\nsort of cons is {}\n sort of nil is {}".format(
48 t,
49 consList.getConstructor("cons").getTerm().getSort(),
50 consList.getConstructor("nil").getTerm().getSort()))
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
58 t2 = tm.mkTerm(
59 Kind.APPLY_SELECTOR,
60 consList["cons"].getSelector("head").getTerm(),
61 t)
62
63 print("t2 is {}\nsimplify(t2) is {}\n\n".format(t2, slv.simplify(t2)))
64
65 # You can also iterate over a Datatype to get all its constructors,
66 # and over a DatatypeConstructor to get all its "args" (selectors)
67 for i in consList:
68 print("ctor:", i)
69 for j in i:
70 print(" + args:", j)
71 print()
72
73 # You can also define a tester term for constructor 'cons': (_ is cons)
74 t_is_cons = tm.mkTerm(
75 Kind.APPLY_TESTER, consList["cons"].getTesterTerm(), t)
76 print("t_is_cons is {}\n\n".format(t_is_cons))
77 slv.assertFormula(t_is_cons)
78 # Updating t at 'head' with value 1 is defined as follows:
79 t_updated = tm.mkTerm(Kind.APPLY_UPDATER,
80 consList["cons"]["head"].getUpdaterTerm(),
81 t,
82 tm.mkInteger(1))
83 print("t_updated is {}\n\n".format(t_updated))
84 slv.assertFormula(tm.mkTerm(Kind.DISTINCT, t, t_updated))
85
86 # You can also define parameterized datatypes.
87 # This example builds a simple parameterized list of sort T, with one
88 # constructor "cons".
89 sort = tm.mkParamSort("T")
90 paramConsListSpec = tm.mkDatatypeDecl("paramlist", [sort])
91 paramCons = tm.mkDatatypeConstructorDecl("cons")
92 paramNil = tm.mkDatatypeConstructorDecl("nil")
93 paramCons.addSelector("head", sort)
94 paramCons.addSelectorSelf("tail")
95 paramConsListSpec.addConstructor(paramCons)
96 paramConsListSpec.addConstructor(paramNil)
97
98 paramConsListSort = tm.mkDatatypeSort(paramConsListSpec)
99 paramConsIntListSort = paramConsListSort.instantiate([tm.getIntegerSort()])
100 paramConsList = paramConsListSort.getDatatype()
101
102 a = tm.mkConst(paramConsIntListSort, "a")
103 print("term {} is of sort {}".format(a, a.getSort()))
104
105 head_a = tm.mkTerm(
106 Kind.APPLY_SELECTOR,
107 paramConsList["cons"].getSelector("head").getTerm(),
108 a)
109 print("head_a is {} of sort {}".format(head_a, head_a.getSort()))
110 print("sort of cons is",
111 paramConsList.getConstructor("cons").getTerm().getSort())
112
113 assertion = tm.mkTerm(Kind.GT, head_a, tm.mkInteger(50))
114 print("Assert", assertion)
115 slv.assertFormula(assertion)
116 print("Expect sat.")
117 print("cvc5:", slv.checkSat())
118
119
120if __name__ == "__main__":
121 tm = cvc5.TermManager()
122 slv = cvc5.Solver(tm)
123
124 # This example builds a simple "cons list" of integers, with
125 # two constructors, "cons" and "nil."
126
127 # Building a datatype consists of two steps.
128 # First, the datatype is specified.
129 # Second, it is "resolved" to an actual sort, at which point function
130 # symbols are assigned to its constructors, selectors, and testers.
131
132 consListSpec = tm.mkDatatypeDecl("list") # give the datatype a name
133 cons = tm.mkDatatypeConstructorDecl("cons")
134 cons.addSelector("head", tm.getIntegerSort())
135 cons.addSelectorSelf("tail")
136 consListSpec.addConstructor(cons)
137 nil = tm.mkDatatypeConstructorDecl("nil")
138 consListSpec.addConstructor(nil)
139
140 print("spec is {}".format(consListSpec))
141
142 # Keep in mind that "DatatypeDecl" is the specification class for
143 # datatypes---"DatatypeDecl" is not itself a cvc5 Sort.
144 # Now that our Datatype is fully specified, we can get a Sort for it.
145 # This step resolves the "SelfSort" reference and creates
146 # symbols for all the constructors, etc.
147
148 consListSort = tm.mkDatatypeSort(consListSpec)
149 test(slv, consListSort)
150
151 print("### Alternatively, use declareDatatype")
152
153 cons2 = tm.mkDatatypeConstructorDecl("cons")
154 cons2.addSelector("head", tm.getIntegerSort())
155 cons2.addSelectorSelf("tail")
156 nil2 = tm.mkDatatypeConstructorDecl("nil")
157 consListSort2 = slv.declareDatatype("list2", cons2, nil2)
158 test(slv, consListSort2)
examples/api/smtlib/datatypes.smt2
1(set-logic QF_UFDTLIA)
2
3; declaring a List datatype and defining List terms
4(declare-datatype List ((cons (head Int) (tail List)) (nil)))
5
6(define-const t List (cons 0 nil))
7(define-const t2 Int (head t))
8
9; declaring a parameterized datatype. We need the general
10; declare-datatypes command since the singular version is a macro for
11; the (declare-datatypes ((<type> 0)) <declaration>)
12(declare-datatypes ((ParList 1))
13 ((par (T) ((cons (parHead T) (parTail (ParList T))) (nil)))))
14
15(define-sort ParListInt () (ParList Int))
16(declare-const a ParListInt)
17(define-const aHead Int (parHead a))
18
19(assert (< aHead 50))
20(check-sat)