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