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