Revision 8c934ccd
Added by Pierre-Loïc Garoche about 3 years ago
| src/tools/zustre/zustre_common.ml | ||
|---|---|---|
| 36 | 36 |
|
| 37 | 37 |
let preprocess = Horn_backend.preprocess |
| 38 | 38 |
|
| 39 |
|
|
| 39 |
|
|
| 40 |
exception UnknownFunction of (string * (Format.formatter -> unit)) |
|
| 40 | 41 |
(** Sorts |
| 41 | 42 |
|
| 42 | 43 |
A sort is introduced for each basic type and each enumerated type. |
| ... | ... | |
| 349 | 350 |
(val_to_expr v1) |
| 350 | 351 |
(val_to_expr v2) |
| 351 | 352 |
|
| 352 |
|
|
| 353 |
|
|
| 354 |
|
|
| 353 | 355 |
(* | _, [v1; v2] -> Z3.Boolean.mk_and |
| 354 | 356 |
* !ctx |
| 355 | 357 |
* (val_to_expr v1) |
| ... | ... | |
| 357 | 359 |
* |
| 358 | 360 |
* Format.fprintf fmt "(%s %a %a)" i val_to_exprr v1 val_to_expr v2 *) |
| 359 | 361 |
| _ -> ( |
| 360 |
Format.eprintf |
|
| 361 |
"internal error: zustre unkown function %s@." i; |
|
| 362 |
assert false) |
|
| 362 |
let msg fmt = Format.fprintf fmt |
|
| 363 |
"internal error: zustre unkown function %s (nb args = %i)@." |
|
| 364 |
i (List.length vl) |
|
| 365 |
in |
|
| 366 |
raise (UnknownFunction(i, msg)) |
|
| 367 |
) |
|
| 363 | 368 |
|
| 364 | 369 |
|
| 365 | 370 |
(* Convert a value expression [v], with internal function calls only. [pp_var] |
Also available in: Unified diff
lustrev seal: ongoing work on extraction as dynamical system. Still not working yet