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
#[test]
fn test_adt() {
run()
}
fn run() {
use rsmt2::{
print::{AdtDecl, AdtVariant, AdtVariantField},
Solver,
};
let mut solver = Solver::default_z3(()).unwrap();
// Alright, so we're going to declared two mutually recursive sorts. It is easier to pack the
// sort-declaration data in custom types. If you want to declare a sort, you most likely
// already have a representation for it, so working on custom types is reasonable.
// Notice that the `AdtDecl`, `AdtVariantField` and `AdtVariant` traits from `rsmt2::print::_`
// are in scope. This is what our custom types will need to generate to declare the sort.
// We'll use static string slices for simplicity as `&str` implements all printing traits.
type Sym = &'static str;
type Sort = &'static str;
// Let's start with the top-level sort type.
struct MyAdt {
// Name of the sort, for instance `List`.
sym: Sym,
// Symbol(s) for the type parameter(s), for instance `T` for `List<T>`. Must be a collection
// of known length, because rsmt2 needs to access the arity (number of type parameters).
args: Vec<Sym>,
// Body of the sort: its variants. For instance the `nil` and `cons` variants for `List<T>`.
variants: Vec<Variant>,
}
impl MyAdt {
// This thing build the actual declaration expected by rsmt2. Its output is something that
// implements `AdtDecl` and can only live as long as the input ref to `self`.
fn as_decl<'me>(&'me self) -> impl AdtDecl + 'me {
// Check out rsmt2's documentation and you'll see that `AdtDecl` is already implemented for
// certain triplets.
(
// Symbol.
&self.sym,
// Sized collection of type-parameter symbols.
&self.args,
// Variant, collection of iterator over `impl AdtVariant` (see below).
self.variants.iter().map(Variant::as_decl),
)
}
fn tree() -> Self {
Self {
sym: "Tree",
args: vec!["T"],
variants: vec![Variant::tree_leaf(), Variant::tree_node()],
}
}
}
// Next up, variants. A variant is a symbol (*e.g.* `nil` or `cons` for `List<T>`) and some
// fields which describe the data stored in the variant.
struct Variant {
sym: Sym,
fields: Vec<Field>,
}
impl Variant {
// Variant declaration; again, `AdtVariant` is implemented for certain types of pairs.
fn as_decl<'me>(&'me self) -> impl AdtVariant + 'me {
(
// Symbol.
self.sym,
// Iterator over field declarations.
self.fields.iter().map(Field::as_decl),
)
}
fn tree_leaf() -> Self {
Self {
sym: "leaf",
fields: vec![],
}
}
fn tree_node() -> Self {
Self {
sym: "node",
fields: vec![Field::tree_node_value(), Field::tree_node_children()],
}
}
}
// A symbol and a sort: describes a piece of data in a variant with a symbol to retrieve it,
// *i.e.* the name of the field.
struct Field {
sym: Sym,
sort: Sort,
}
impl Field {
// As usual, `AdtVariantField` is implemented for certain pairs.
fn as_decl(&self) -> impl AdtVariantField {
(self.sym, self.sort)
}
fn tree_node_value() -> Self {
Self {
sym: "value",
sort: "T",
}
}
fn tree_node_children() -> Self {
Self {
sym: "children",
sort: "(TreeList T)",
}
}
}
let tree = MyAdt::tree();
// Now this `tree` uses an non-existing `(TreeList T)` sort to store its children, let's declare
// it now.
let nil = Variant {
sym: "nil",
fields: vec![],
};
let cons = Variant {
sym: "cons",
fields: vec![
Field {
sym: "car",
sort: "(Tree T)",
},
Field {
sym: "cdr",
sort: "(TreeList T)",
},
],
};
let tree_list = MyAdt {
sym: "TreeList",
args: vec!["T"],
variants: vec![nil, cons],
};
println!("declaring ADTs `Tree<T>` and `TreeList<T>`");
solver
// These sort are mutually recursive, `Solver::declare_datatypes` needs to declare them at the
// same time.
.declare_datatypes(&[tree.as_decl(), tree_list.as_decl()])
.unwrap();
// That's it! Solver now knows these sorts and we can use them.
println!("declaring two `Tree<_>` values");
solver.declare_const("t1", "(Tree Int)").unwrap();
solver.declare_const("t2", "(Tree Bool)").unwrap();
println!("asserting some stuff");
solver.assert("(> (value t1) 20)").unwrap();
solver.assert("(not (is-leaf t2))").unwrap();
solver.assert("(not (value t2))").unwrap();
println!("check-sat, should be sat");
let sat = solver.check_sat().unwrap();
assert!(sat);
println!("it is!");
}
fn main() {
run();
println!("everything is fine");
}