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
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
[@@@ocaml.warning "-33"]
open Options
module Rel1 : Sig_rel.RELATION = IntervalCalculus
module Rel2 : Sig_rel.RELATION = Records_rel
module Rel3 : Sig_rel.RELATION = Bitv_rel
module Rel4 : Sig_rel.RELATION = Arrays_rel
module Rel5 : Sig_rel.RELATION = Enum_rel
module Rel6 : Sig_rel.RELATION = Adt_rel
module Rel7 : Sig_rel.RELATION = Ite_rel
open Sig_rel
type t = {
r1: Rel1.t;
r2: Rel2.t;
r3: Rel3.t;
r4: Rel4.t;
r5: Rel5.t;
r6: Rel6.t;
r7: Rel7.t;
}
let empty classes = {
r1=Rel1.empty classes;
r2=Rel2.empty classes;
r3=Rel3.empty classes;
r4=Rel4.empty classes;
r5=Rel5.empty classes;
r6=Rel6.empty classes;
r7=Rel7.empty classes;
}
let (|@|) l1 l2 =
if l1 == [] then l2
else if l2 == [] then l1
else List.rev_append l1 l2
let assume env uf sa =
Options.exec_thread_yield ();
let env1, { assume = a1; remove = rm1} =
Rel1.assume env.r1 uf sa in
let env2, { assume = a2; remove = rm2} =
Rel2.assume env.r2 uf sa in
let env3, { assume = a3; remove = rm3} =
Rel3.assume env.r3 uf sa in
let env4, { assume = a4; remove = rm4} =
Rel4.assume env.r4 uf sa in
let env5, { assume = a5; remove = rm5} =
Rel5.assume env.r5 uf sa in
let env6, { assume = a6; remove = rm6} =
Rel6.assume env.r6 uf sa in
let env7, { assume = a7; remove = rm7} =
Rel7.assume env.r7 uf sa in
{r1=env1; r2=env2; r3=env3; r4=env4; r5=env5; r6=env6; r7=env7},
{ assume = a1 |@| a2 |@| a3 |@| a4 |@| a5 |@| a6 |@| a7;
remove = rm1 |@| rm2 |@| rm3 |@| rm4 |@| rm5 |@| rm6 |@| rm7}
let assume_th_elt env th_elt dep =
Options.exec_thread_yield ();
let env1 = Rel1.assume_th_elt env.r1 th_elt dep in
let env2 = Rel2.assume_th_elt env.r2 th_elt dep in
let env3 = Rel3.assume_th_elt env.r3 th_elt dep in
let env4 = Rel4.assume_th_elt env.r4 th_elt dep in
let env5 = Rel5.assume_th_elt env.r5 th_elt dep in
let env6 = Rel6.assume_th_elt env.r6 th_elt dep in
let env7 = Rel7.assume_th_elt env.r7 th_elt dep in
{r1=env1; r2=env2; r3=env3; r4=env4; r5=env5; r6=env6; r7=env7}
let query env uf a =
Options.exec_thread_yield ();
match Rel1.query env.r1 uf a with
| Some _ as ans -> ans
| None ->
match Rel2.query env.r2 uf a with
| Some _ as ans -> ans
| None ->
match Rel3.query env.r3 uf a with
| Some _ as ans -> ans
| None ->
match Rel4.query env.r4 uf a with
| Some _ as ans -> ans
| None ->
match Rel5.query env.r5 uf a with
| Some _ as ans -> ans
| None ->
match Rel6.query env.r6 uf a with
| Some _ as ans -> ans
| None -> Rel7.query env.r7 uf a
let case_split env uf ~for_model =
Options.exec_thread_yield ();
let seq1 = Rel1.case_split env.r1 uf ~for_model in
let seq2 = Rel2.case_split env.r2 uf ~for_model in
let seq3 = Rel3.case_split env.r3 uf ~for_model in
let seq4 = Rel4.case_split env.r4 uf ~for_model in
let seq5 = Rel5.case_split env.r5 uf ~for_model in
let seq6 = Rel6.case_split env.r6 uf ~for_model in
let seq7 = Rel7.case_split env.r7 uf ~for_model in
let l = seq1 |@| seq2 |@| seq3 |@| seq4 |@| seq5 |@| seq6 |@| seq7 in
List.sort
(fun (_,_,sz1) (_,_,sz2) ->
match sz1, sz2 with
| Th_util.CS(_,sz1), Th_util.CS(_,sz2) -> Numbers.Q.compare sz1 sz2
| _ -> assert false
)l
let add env uf r t =
Options.exec_thread_yield ();
{r1=Rel1.add env.r1 uf r t;
r2=Rel2.add env.r2 uf r t;
r3=Rel3.add env.r3 uf r t;
r4=Rel4.add env.r4 uf r t;
r5=Rel5.add env.r5 uf r t;
r6=Rel6.add env.r6 uf r t;
r7=Rel7.add env.r7 uf r t;
}
let instantiate ~do_syntactic_matching t_match env uf selector =
Options.exec_thread_yield ();
let r1, l1 =
Rel1.instantiate ~do_syntactic_matching t_match env.r1 uf selector in
let r2, l2 =
Rel2.instantiate ~do_syntactic_matching t_match env.r2 uf selector in
let r3, l3 =
Rel3.instantiate ~do_syntactic_matching t_match env.r3 uf selector in
let r4, l4 =
Rel4.instantiate ~do_syntactic_matching t_match env.r4 uf selector in
let r5, l5 =
Rel5.instantiate ~do_syntactic_matching t_match env.r5 uf selector in
let r6, l6 =
Rel6.instantiate ~do_syntactic_matching t_match env.r6 uf selector in
let r7, l7 =
Rel7.instantiate ~do_syntactic_matching t_match env.r7 uf selector in
{r1=r1; r2=r2; r3=r3; r4=r4; r5=r5; r6=r6; r7=r7},
l7 |@| l6 |@| l5 |@| l4 |@| l3 |@| l2 |@| l1
let print_model fmt env rs =
Rel1.print_model fmt env.r1 rs;
Rel2.print_model fmt env.r2 rs;
Rel3.print_model fmt env.r3 rs;
Rel4.print_model fmt env.r4 rs;
Rel5.print_model fmt env.r5 rs;
Rel6.print_model fmt env.r6 rs;
Rel7.print_model fmt env.r7 rs
let new_terms env =
let t1 = Rel1.new_terms env.r1 in
let t2 = Rel2.new_terms env.r2 in
let t3 = Rel3.new_terms env.r3 in
let t4 = Rel4.new_terms env.r4 in
let t5 = Rel5.new_terms env.r5 in
let t6 = Rel6.new_terms env.r6 in
let t7 = Rel7.new_terms env.r7 in
Expr.Set.union t1
(Expr.Set.union t2
(Expr.Set.union t3
(Expr.Set.union t4
(Expr.Set.union t5
(Expr.Set.union t6 t7)) )))