Revision a0c92fa8 src/tools/zustre/zustre_common.ml
src/tools/zustre/zustre_common.ml | ||
---|---|---|
5 | 5 |
(* open Horn_backend_common |
6 | 6 |
* open Horn_backend *) |
7 | 7 |
open Zustre_data |
8 |
|
|
8 |
|
|
9 |
let report = Log.report ~plugin:"z3 interface" |
|
10 |
|
|
9 | 11 |
module HBC = Horn_backend_common |
10 | 12 |
let node_name = HBC.node_name |
11 | 13 |
|
... | ... | |
111 | 113 |
let get_fdecl id = |
112 | 114 |
try |
113 | 115 |
Hashtbl.find decls id |
114 |
with Not_found -> (Format.eprintf "Unable to find func_decl %s@.@?" id; raise Not_found)
|
|
116 |
with Not_found -> (report ~level:3 (fun fmt -> Format.fprintf fmt "Unable to find func_decl %s@.@?" id); raise Not_found)
|
|
115 | 117 |
|
116 | 118 |
let pp_fdecls fmt = |
117 | 119 |
Format.fprintf fmt "Registered fdecls: @[%a@]@ " |
... | ... | |
124 | 126 |
register_fdecl id.var_id fdecl; |
125 | 127 |
fdecl |
126 | 128 |
|
129 |
(* Declaring the function used in expr *) |
|
130 |
let decl_fun op args typ = |
|
131 |
let args = List.map type_to_sort args in |
|
132 |
let fdecl = Z3.FuncDecl.mk_func_decl_s !ctx op args (type_to_sort typ) in |
|
133 |
register_fdecl op fdecl; |
|
134 |
fdecl |
|
135 |
|
|
127 | 136 |
let idx_sort = int_sort |
128 | 137 |
let uid_sort = Z3.Z3List.mk_sort !ctx (Z3.Symbol.mk_string !ctx "uid_list") int_sort |
129 | 138 |
let uid_conc = |
... | ... | |
242 | 251 |
|
243 | 252 |
(* Conversion of basic library functions *) |
244 | 253 |
|
245 |
let horn_basic_app i val_to_expr vl =
|
|
254 |
let horn_basic_app i vl (vltyp, typ) =
|
|
246 | 255 |
match i, vl with |
247 |
| "ite", [v1; v2; v3] -> |
|
248 |
Z3.Boolean.mk_ite |
|
249 |
!ctx |
|
250 |
(val_to_expr v1) |
|
251 |
(val_to_expr v2) |
|
252 |
(val_to_expr v3) |
|
253 |
|
|
254 |
| "uminus", [v] -> |
|
255 |
Z3.Arithmetic.mk_unary_minus |
|
256 |
!ctx |
|
257 |
(val_to_expr v) |
|
256 |
| "ite", [v1; v2; v3] -> Z3.Boolean.mk_ite !ctx v1 v2 v3 |
|
257 |
| "uminus", [v] -> Z3.Arithmetic.mk_unary_minus |
|
258 |
!ctx v |
|
258 | 259 |
| "not", [v] -> |
259 | 260 |
Z3.Boolean.mk_not |
260 |
!ctx |
|
261 |
(val_to_expr v) |
|
261 |
!ctx v |
|
262 | 262 |
| "=", [v1; v2] -> |
263 | 263 |
Z3.Boolean.mk_eq |
264 |
!ctx |
|
265 |
(val_to_expr v1) |
|
266 |
(val_to_expr v2) |
|
264 |
!ctx v1 v2 |
|
267 | 265 |
| "&&", [v1; v2] -> |
268 | 266 |
Z3.Boolean.mk_and |
269 | 267 |
!ctx |
270 |
[val_to_expr v1; |
|
271 |
val_to_expr v2] |
|
268 |
[v1; v2] |
|
272 | 269 |
| "||", [v1; v2] -> |
273 | 270 |
Z3.Boolean.mk_or |
274 | 271 |
!ctx |
275 |
[val_to_expr v1;
|
|
276 |
val_to_expr v2]
|
|
272 |
[v1; |
|
273 |
v2] |
|
277 | 274 |
|
278 | 275 |
| "impl", [v1; v2] -> |
279 | 276 |
Z3.Boolean.mk_implies |
280 |
!ctx |
|
281 |
(val_to_expr v1) |
|
282 |
(val_to_expr v2) |
|
277 |
!ctx v1 v2 |
|
283 | 278 |
| "mod", [v1; v2] -> |
284 | 279 |
Z3.Arithmetic.Integer.mk_mod |
285 |
!ctx |
|
286 |
(val_to_expr v1) |
|
287 |
(val_to_expr v2) |
|
280 |
!ctx v1 v2 |
|
288 | 281 |
| "equi", [v1; v2] -> |
289 | 282 |
Z3.Boolean.mk_eq |
290 | 283 |
!ctx |
291 |
(val_to_expr v1) |
|
292 |
(val_to_expr v2) |
|
284 |
v1 v2 |
|
293 | 285 |
| "xor", [v1; v2] -> |
294 | 286 |
Z3.Boolean.mk_xor |
295 |
!ctx |
|
296 |
(val_to_expr v1) |
|
297 |
(val_to_expr v2) |
|
287 |
!ctx v1 v2 |
|
298 | 288 |
| "!=", [v1; v2] -> |
299 | 289 |
Z3.Boolean.mk_not |
300 | 290 |
!ctx |
301 | 291 |
( |
302 | 292 |
Z3.Boolean.mk_eq |
303 |
!ctx |
|
304 |
(val_to_expr v1) |
|
305 |
(val_to_expr v2) |
|
293 |
!ctx v1 v2 |
|
306 | 294 |
) |
307 | 295 |
| "/", [v1; v2] -> |
308 | 296 |
Z3.Arithmetic.mk_div |
309 |
!ctx |
|
310 |
(val_to_expr v1) |
|
311 |
(val_to_expr v2) |
|
297 |
!ctx v1 v2 |
|
312 | 298 |
|
313 | 299 |
| "+", [v1; v2] -> |
314 | 300 |
Z3.Arithmetic.mk_add |
315 | 301 |
!ctx |
316 |
[val_to_expr v1; val_to_expr v2] |
|
317 |
|
|
302 |
[v1; v2] |
|
318 | 303 |
| "-", [v1; v2] -> |
319 | 304 |
Z3.Arithmetic.mk_sub |
320 | 305 |
!ctx |
321 |
[val_to_expr v1 ; val_to_expr v2]
|
|
306 |
[v1 ; v2]
|
|
322 | 307 |
|
323 | 308 |
| "*", [v1; v2] -> |
324 | 309 |
Z3.Arithmetic.mk_mul |
325 | 310 |
!ctx |
326 |
[val_to_expr v1; val_to_expr v2]
|
|
311 |
[ v1; v2]
|
|
327 | 312 |
|
328 | 313 |
|
329 | 314 |
| "<", [v1; v2] -> |
330 | 315 |
Z3.Arithmetic.mk_lt |
331 |
!ctx |
|
332 |
(val_to_expr v1) |
|
333 |
(val_to_expr v2) |
|
334 |
|
|
316 |
!ctx v1 v2 |
|
335 | 317 |
| "<=", [v1; v2] -> |
336 | 318 |
Z3.Arithmetic.mk_le |
337 |
!ctx |
|
338 |
(val_to_expr v1) |
|
339 |
(val_to_expr v2) |
|
340 |
|
|
319 |
!ctx v1 v2 |
|
341 | 320 |
| ">", [v1; v2] -> |
342 | 321 |
Z3.Arithmetic.mk_gt |
343 |
!ctx |
|
344 |
(val_to_expr v1) |
|
345 |
(val_to_expr v2) |
|
346 |
|
|
322 |
!ctx v1 v2 |
|
347 | 323 |
| ">=", [v1; v2] -> |
348 | 324 |
Z3.Arithmetic.mk_ge |
349 |
!ctx |
|
350 |
(val_to_expr v1) |
|
351 |
(val_to_expr v2) |
|
352 |
|
|
325 |
!ctx v1 v2 |
|
353 | 326 |
| "int_to_real", [v1] -> |
354 | 327 |
Z3.Arithmetic.Integer.mk_int2real |
355 |
!ctx |
|
356 |
(val_to_expr v1) |
|
357 |
|
|
328 |
!ctx v1 |
|
329 |
| _ -> |
|
330 |
let fd = |
|
331 |
try |
|
332 |
get_fdecl i |
|
333 |
with Not_found -> begin |
|
334 |
report ~level:3 (fun fmt -> Format.fprintf fmt "Registering function %s as uninterpreted function in Z3@.%s: (%a) -> %a" i i (Utils.fprintf_list ~sep:"," Types.print_ty) vltyp Types.print_ty typ); |
|
335 |
decl_fun i vltyp typ |
|
336 |
end |
|
337 |
in |
|
338 |
Z3.FuncDecl.apply fd vl |
|
358 | 339 |
|
340 |
|
|
359 | 341 |
(* | _, [v1; v2] -> Z3.Boolean.mk_and |
360 | 342 |
* !ctx |
361 | 343 |
* (val_to_expr v1) |
362 | 344 |
* (val_to_expr v2) |
363 | 345 |
* |
364 | 346 |
* Format.fprintf fmt "(%s %a %a)" i val_to_exprr v1 val_to_expr v2 *) |
365 |
| _ -> ( |
|
366 |
let msg fmt = Format.fprintf fmt |
|
367 |
"internal error: zustre unkown function %s (nb args = %i)@." |
|
368 |
i (List.length vl) |
|
369 |
in |
|
370 |
raise (UnknownFunction(i, msg)) |
|
371 |
) |
|
347 |
|
|
348 |
(* | _ -> ( |
|
349 |
* let msg fmt = Format.fprintf fmt |
|
350 |
* "internal error: zustre unkown function %s (nb args = %i)@." |
|
351 |
* i (List.length vl) |
|
352 |
* in |
|
353 |
* raise (UnknownFunction(i, msg)) |
|
354 |
* ) *) |
|
372 | 355 |
|
373 | 356 |
|
374 | 357 |
(* Convert a value expression [v], with internal function calls only. [pp_var] |
... | ... | |
376 | 359 |
may be added for array variables |
377 | 360 |
*) |
378 | 361 |
let rec horn_val_to_expr ?(is_lhs=false) m self v = |
362 |
(* Format.eprintf "h_v2e %a@." (Machine_code_common.pp_val m) v ; *) |
|
379 | 363 |
match v.value_desc with |
380 | 364 |
| Cst c -> horn_const_to_expr c |
381 | 365 |
|
... | ... | |
425 | 409 |
(rename_machine |
426 | 410 |
self |
427 | 411 |
v) |
428 |
| Fun (n, vl) -> horn_basic_app n (horn_val_to_expr m self) vl
|
|
412 |
| Fun (n, vl) -> horn_basic_app n (List.map (horn_val_to_expr m self) vl) (List.map (fun v -> v.value_type) vl, v.value_type)
|
|
429 | 413 |
|
430 | 414 |
let no_reset_to_exprs machines m i = |
431 | 415 |
let (n,_) = List.assoc i m.minstances in |
Also available in: Unified diff