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-2022 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 // Now our old "consListSpec" is useless--the relevant information
25 // has been copied out, so we can throw that spec away. We can get
26 // the complete spec for the datatype from the DatatypeSort, and
27 // this Datatype object has constructor symbols (and others) filled in.
28
29 const Datatype& consList = consListSort.getDatatype();
30
31 // t = cons 0 nil
32 //
33 // Here, consList["cons"] gives you the DatatypeConstructor. To get
34 // the constructor symbol for application, use .getConstructor("cons"),
35 // which is equivalent to consList["cons"].getConstructor(). Note that
36 // "nil" is a constructor too, so it needs to be applied with
37 // APPLY_CONSTRUCTOR, even though it has no arguments.
38 Term t = slv.mkTerm(APPLY_CONSTRUCTOR,
39 {consList.getConstructor("cons").getTerm(),
40 slv.mkInteger(0),
41 slv.mkTerm(APPLY_CONSTRUCTOR,
42 {consList.getConstructor("nil").getTerm()})});
43
44 std::cout << "t is " << t << std::endl
45 << "sort of cons is "
46 << consList.getConstructor("cons").getTerm().getSort() << std::endl
47 << "sort of nil is "
48 << consList.getConstructor("nil").getTerm().getSort() << std::endl;
49
50 // t2 = head(cons 0 nil), and of course this can be evaluated
51 //
52 // Here we first get the DatatypeConstructor for cons (with
53 // consList["cons"]) in order to get the "head" selector symbol
54 // to apply.
55 Term t2 = slv.mkTerm(APPLY_SELECTOR,
56 {consList["cons"].getSelector("head").getTerm(), t});
57
58 std::cout << "t2 is " << t2 << std::endl
59 << "simplify(t2) is " << slv.simplify(t2) << std::endl
60 << std::endl;
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 (Datatype::const_iterator i = consList.begin(); i != consList.end(); ++i)
65 {
66 std::cout << "ctor: " << *i << std::endl;
67 for (DatatypeConstructor::const_iterator j = (*i).begin(); j != (*i).end();
68 ++j)
69 {
70 std::cout << " + arg: " << *j << std::endl;
71 }
72 }
73 std::cout << std::endl;
74
75 // Alternatively, you can use for each loops.
76 for (const auto& c : consList)
77 {
78 std::cout << "ctor: " << c << std::endl;
79 for (const auto& s : c)
80 {
81 std::cout << " + arg: " << s << std::endl;
82 }
83 }
84 std::cout << std::endl;
85
86 // You can also define a tester term for constructor 'cons': (_ is cons)
87 Term t_is_cons =
88 slv.mkTerm(APPLY_TESTER, {consList["cons"].getTesterTerm(), t});
89 std::cout << "t_is_cons is " << t_is_cons << std::endl << std::endl;
90 slv.assertFormula(t_is_cons);
91 // Updating t at 'head' with value 1 is defined as follows:
92 Term t_updated = slv.mkTerm(
93 APPLY_UPDATER,
94 {consList["cons"]["head"].getUpdaterTerm(), t, slv.mkInteger(1)});
95 std::cout << "t_updated is " << t_updated << std::endl << std::endl;
96 slv.assertFormula(slv.mkTerm(DISTINCT, {t, t_updated}));
97
98 // You can also define parameterized datatypes.
99 // This example builds a simple parameterized list of sort T, with one
100 // constructor "cons".
101 Sort sort = slv.mkParamSort("T");
102 DatatypeDecl paramConsListSpec =
103 slv.mkDatatypeDecl("paramlist", {sort}); // give the datatype a name
104 DatatypeConstructorDecl paramCons = slv.mkDatatypeConstructorDecl("cons");
105 DatatypeConstructorDecl paramNil = slv.mkDatatypeConstructorDecl("nil");
106 paramCons.addSelector("head", sort);
107 paramCons.addSelectorSelf("tail");
108 paramConsListSpec.addConstructor(paramCons);
109 paramConsListSpec.addConstructor(paramNil);
110
111 Sort paramConsListSort = slv.mkDatatypeSort(paramConsListSpec);
112 Sort paramConsIntListSort =
113 paramConsListSort.instantiate(std::vector<Sort>{slv.getIntegerSort()});
114
115 const Datatype& paramConsList = paramConsListSort.getDatatype();
116
117 std::cout << "parameterized datatype sort is " << std::endl;
118 for (const DatatypeConstructor& ctor : paramConsList)
119 {
120 std::cout << "ctor: " << ctor << std::endl;
121 for (const DatatypeSelector& stor : ctor)
122 {
123 std::cout << " + arg: " << stor << std::endl;
124 }
125 }
126
127 Term a = slv.mkConst(paramConsIntListSort, "a");
128 std::cout << "term " << a << " is of sort " << a.getSort() << std::endl;
129
130 Term head_a = slv.mkTerm(
131 APPLY_SELECTOR, {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 = slv.mkTerm(GT, {head_a, slv.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 Solver slv;
149 // This example builds a simple "cons list" of integers, with
150 // two constructors, "cons" and "nil."
151
152 // Building a datatype consists of two steps.
153 // First, the datatype is specified.
154 // Second, it is "resolved" to an actual sort, at which point function
155 // symbols are assigned to its constructors, selectors, and testers.
156
157 DatatypeDecl consListSpec =
158 slv.mkDatatypeDecl("list"); // give the datatype a name
159 DatatypeConstructorDecl cons = slv.mkDatatypeConstructorDecl("cons");
160 cons.addSelector("head", slv.getIntegerSort());
161 cons.addSelectorSelf("tail");
162 consListSpec.addConstructor(cons);
163 DatatypeConstructorDecl nil = slv.mkDatatypeConstructorDecl("nil");
164 consListSpec.addConstructor(nil);
165
166 std::cout << "spec is:" << std::endl << consListSpec << std::endl;
167
168 // Keep in mind that "DatatypeDecl" is the specification class for
169 // datatypes---"DatatypeDecl" is not itself a cvc5 Sort.
170 // Now that our Datatype is fully specified, we can get a Sort for it.
171 // This step resolves the "SelfSort" reference and creates
172 // symbols for all the constructors, etc.
173
174 Sort consListSort = slv.mkDatatypeSort(consListSpec);
175
176 test(slv, consListSort);
177
178 std::cout << std::endl
179 << ">>> Alternatively, use declareDatatype" << std::endl;
180 std::cout << std::endl;
181
182 DatatypeConstructorDecl cons2 = slv.mkDatatypeConstructorDecl("cons");
183 cons2.addSelector("head", slv.getIntegerSort());
184 cons2.addSelectorSelf("tail");
185 DatatypeConstructorDecl nil2 = slv.mkDatatypeConstructorDecl("nil");
186 std::vector<DatatypeConstructorDecl> ctors = {cons2, nil2};
187 Sort consListSort2 = slv.declareDatatype("list2", ctors);
188 test(slv, consListSort2);
189
190 return 0;
191}
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-2022 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 }
183}
examples/api/python/pythonic/datatypes.py
1from cvc5.pythonic import *
2
3if __name__ == '__main__':
4 # This example builds a simple "cons list" of integers, with
5 # two constructors, "cons" and "nil."
6
7 # Building a datatype consists of two steps.
8 # First, the datatype is specified.
9 # Second, it is "resolved" to an actual sort, at which point function
10 # symbols are assigned to its constructors, selectors, and testers.
11
12 decl = Datatype("list")
13 decl.declare("cons", ("head", IntSort()), ("tail", decl))
14 decl.declare("nil")
15 List = decl.create()
16
17 # Using constructors and selectors:
18 t = List.cons(0, List.nil)
19 print("t is:", t)
20 print("head of t is:", List.head(t))
21 print("after simplify:", simplify(List.head(t)))
22 print()
23
24 # You can iterate over constructors and selectors
25 for i in range(List.num_constructors()):
26 ctor = List.constructor(i)
27 print("ctor:", ctor)
28 for j in range(ctor.arity()):
29 print(" + arg:", ctor.domain(j))
30 print(" + selector:", List.accessor(i, j))
31 print()
32
33 # You can use testers
34 print("t is a 'cons':", simplify(List.is_cons(t)))
35 print()
36
37 # This Python API does not support type parameters or updators for
38 # datatypes. See the base Python API for those features, or construct them
39 # using Python functions/classes.
40
41 a = Int('a')
42 solve(List.head(List.cons(a, List.nil)) > 50)
43
44 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-2022 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 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
36
37 t = slv.mkTerm(
38 Kind.APPLY_CONSTRUCTOR,
39 consList.getConstructor("cons").getTerm(),
40 slv.mkInteger(0),
41 slv.mkTerm(
42 Kind.APPLY_CONSTRUCTOR,
43 consList.getConstructor("nil").getTerm()))
44
45 print("t is {}\nsort of cons is {}\n sort of nil is {}".format(
46 t,
47 consList.getConstructor("cons").getTerm().getSort(),
48 consList.getConstructor("nil").getTerm().getSort()))
49
50 # t2 = head(cons 0 nil), and of course this can be evaluated
51 #
52 # Here we first get the DatatypeConstructor for cons (with
53 # consList["cons"]) in order to get the "head" selector symbol
54 # to apply.
55
56 t2 = slv.mkTerm(
57 Kind.APPLY_SELECTOR,
58 consList["cons"].getSelector("head").getTerm(),
59 t)
60
61 print("t2 is {}\nsimplify(t2) is {}\n\n".format(t2, slv.simplify(t2)))
62
63 # You can also iterate over a Datatype to get all its constructors,
64 # and over a DatatypeConstructor to get all its "args" (selectors)
65 for i in consList:
66 print("ctor:", i)
67 for j in i:
68 print(" + args:", j)
69 print()
70
71 # You can also define a tester term for constructor 'cons': (_ is cons)
72 t_is_cons = slv.mkTerm(
73 Kind.APPLY_TESTER, consList["cons"].getTesterTerm(), t)
74 print("t_is_cons is {}\n\n".format(t_is_cons))
75 slv.assertFormula(t_is_cons)
76 # Updating t at 'head' with value 1 is defined as follows:
77 t_updated = slv.mkTerm(Kind.APPLY_UPDATER,
78 consList["cons"]["head"].getUpdaterTerm(),
79 t,
80 slv.mkInteger(1))
81 print("t_updated is {}\n\n".format(t_updated))
82 slv.assertFormula(slv.mkTerm(Kind.DISTINCT, t, t_updated))
83
84 # You can also define parameterized datatypes.
85 # This example builds a simple parameterized list of sort T, with one
86 # constructor "cons".
87 sort = slv.mkParamSort("T")
88 paramConsListSpec = slv.mkDatatypeDecl("paramlist", [sort])
89 paramCons = slv.mkDatatypeConstructorDecl("cons")
90 paramNil = slv.mkDatatypeConstructorDecl("nil")
91 paramCons.addSelector("head", sort)
92 paramCons.addSelectorSelf("tail")
93 paramConsListSpec.addConstructor(paramCons)
94 paramConsListSpec.addConstructor(paramNil)
95
96 paramConsListSort = slv.mkDatatypeSort(paramConsListSpec)
97 paramConsIntListSort = paramConsListSort.instantiate([slv.getIntegerSort()])
98 paramConsList = paramConsListSort.getDatatype()
99
100 a = slv.mkConst(paramConsIntListSort, "a")
101 print("term {} is of sort {}".format(a, a.getSort()))
102
103 head_a = slv.mkTerm(
104 Kind.APPLY_SELECTOR,
105 paramConsList["cons"].getSelector("head").getTerm(),
106 a)
107 print("head_a is {} of sort {}".format(head_a, head_a.getSort()))
108 print("sort of cons is",
109 paramConsList.getConstructor("cons").getTerm().getSort())
110
111 assertion = slv.mkTerm(Kind.GT, head_a, slv.mkInteger(50))
112 print("Assert", assertion)
113 slv.assertFormula(assertion)
114 print("Expect sat.")
115 print("cvc5:", slv.checkSat())
116
117
118if __name__ == "__main__":
119 slv = cvc5.Solver()
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 = slv.mkDatatypeDecl("list") # give the datatype a name
130 cons = slv.mkDatatypeConstructorDecl("cons")
131 cons.addSelector("head", slv.getIntegerSort())
132 cons.addSelectorSelf("tail")
133 consListSpec.addConstructor(cons)
134 nil = slv.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 = slv.mkDatatypeSort(consListSpec)
146 test(slv, consListSort)
147
148 print("### Alternatively, use declareDatatype")
149
150 cons2 = slv.mkDatatypeConstructorDecl("cons")
151 cons2.addSelector("head", slv.getIntegerSort())
152 cons2.addSelectorSelf("tail")
153 nil2 = slv.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)