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}
examples/api/java/Datatypes.java
1/******************************************************************************
2 * Top contributors (to current version):
3 * Mudathir Mohamed, Morgan Deters, Aina Niemetz
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
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 // 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 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 = slv.mkTerm(Kind.APPLY_CONSTRUCTOR,
38 consList.getConstructor("cons").getTerm(),
39 slv.mkInteger(0),
40 slv.mkTerm(Kind.APPLY_CONSTRUCTOR, consList.getConstructor("nil").getTerm()));
41
42 System.out.println("t is " + t + "\n"
43 + "sort of cons is " + consList.getConstructor("cons").getTerm().getSort() + "\n"
44 + "sort of nil is " + consList.getConstructor("nil").getTerm().getSort());
45
46 // t2 = head(cons 0 nil), and of course this can be evaluated
47 //
48 // Here we first get the DatatypeConstructor for cons (with
49 // consList["cons"]) in order to get the "head" selector symbol
50 // to apply.
51 Term t2 = slv.mkTerm(
52 Kind.APPLY_SELECTOR, consList.getConstructor("cons").getSelector("head").getTerm(), t);
53
54 System.out.println("t2 is " + t2 + "\n"
55 + "simplify(t2) is " + slv.simplify(t2) + "\n");
56
57 // You can also iterate over a Datatype to get all its constructors,
58 // and over a DatatypeConstructor to get all its "args" (selectors)
59
60 for (Iterator<DatatypeConstructor> i = consList.iterator(); i.hasNext();)
61 {
62 DatatypeConstructor constructor = i.next();
63 System.out.println("ctor: " + constructor);
64 for (Iterator<DatatypeSelector> j = constructor.iterator(); j.hasNext();)
65 {
66 System.out.println(" + arg: " + j.next());
67 }
68 }
69 System.out.println();
70
71 // Alternatively, you can use for each loops.
72 for (DatatypeConstructor c : consList)
73 {
74 System.out.println("ctor: " + c);
75 for (DatatypeSelector s : c)
76 {
77 System.out.println(" + arg: " + s);
78 }
79 }
80 System.out.println();
81
82 // You can also define a tester term for constructor 'cons': (_ is cons)
83 Term t_is_cons =
84 slv.mkTerm(Kind.APPLY_TESTER, consList.getConstructor("cons").getTesterTerm(), t);
85 System.out.println("t_is_cons is " + t_is_cons + "\n");
86 slv.assertFormula(t_is_cons);
87 // Updating t at 'head' with value 1 is defined as follows:
88 Term t_updated = slv.mkTerm(Kind.APPLY_UPDATER,
89 consList.getConstructor("cons").getSelector("head").getUpdaterTerm(),
90 t,
91 slv.mkInteger(1));
92 System.out.println("t_updated is " + t_updated + "\n");
93 slv.assertFormula(slv.mkTerm(Kind.DISTINCT, t, t_updated));
94
95 // You can also define parameterized datatypes.
96 // This example builds a simple parameterized list of sort T, with one
97 // constructor "cons".
98 Sort sort = slv.mkParamSort("T");
99 DatatypeDecl paramConsListSpec =
100 slv.mkDatatypeDecl("paramlist", new Sort[] {sort}); // give the datatype a name
101 DatatypeConstructorDecl paramCons = slv.mkDatatypeConstructorDecl("cons");
102 DatatypeConstructorDecl paramNil = slv.mkDatatypeConstructorDecl("nil");
103 paramCons.addSelector("head", sort);
104 paramCons.addSelectorSelf("tail");
105 paramConsListSpec.addConstructor(paramCons);
106 paramConsListSpec.addConstructor(paramNil);
107
108 Sort paramConsListSort = slv.mkDatatypeSort(paramConsListSpec);
109 Sort paramConsIntListSort = paramConsListSort.instantiate(new Sort[] {slv.getIntegerSort()});
110
111 Datatype paramConsList = paramConsListSort.getDatatype();
112
113 System.out.println("parameterized datatype sort is ");
114 for (DatatypeConstructor ctor : paramConsList)
115 {
116 System.out.println("ctor: " + ctor);
117 for (DatatypeSelector stor : ctor)
118 {
119 System.out.println(" + arg: " + stor);
120 }
121 }
122
123 Term a = slv.mkConst(paramConsIntListSort, "a");
124 System.out.println("term " + a + " is of sort " + a.getSort());
125
126 Term head_a = slv.mkTerm(
127 Kind.APPLY_SELECTOR, paramConsList.getConstructor("cons").getSelector("head").getTerm(), a);
128 System.out.println("head_a is " + head_a + " of sort " + head_a.getSort() + "\n"
129 + "sort of cons is " + paramConsList.getConstructor("cons").getTerm().getSort() + "\n");
130 Term assertion = slv.mkTerm(Kind.GT, head_a, slv.mkInteger(50));
131 System.out.println("Assert " + assertion);
132 slv.assertFormula(assertion);
133 System.out.println("Expect sat.");
134 System.out.println("cvc5: " + slv.checkSat());
135 }
136
137 public static void main(String[] args) throws CVC5ApiException
138 {
139 Solver slv = new Solver();
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 = slv.mkDatatypeDecl("list"); // give the datatype a name
150 DatatypeConstructorDecl cons = slv.mkDatatypeConstructorDecl("cons");
151 cons.addSelector("head", slv.getIntegerSort());
152 cons.addSelectorSelf("tail");
153 consListSpec.addConstructor(cons);
154 DatatypeConstructorDecl nil = slv.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 = slv.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 = slv.mkDatatypeConstructorDecl("cons");
175 cons2.addSelector("head", slv.getIntegerSort());
176 cons2.addSelectorSelf("tail");
177 DatatypeConstructorDecl nil2 = slv.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# Top contributors (to current version):
3# Alex Ozdemir
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##
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-2024 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)