Revision 07ceae4c
Added by Pierre-Loïc Garoche almost 6 years ago
| src/backends/Horn/horn_backend_printers.ml | ||
|---|---|---|
| 36 | 36 |
(* Used to print boolean constants *) |
| 37 | 37 |
let pp_horn_tag fmt t = |
| 38 | 38 |
pp_print_string fmt (if t = tag_true then "true" else if t = tag_false then "false" else t) |
| 39 |
|
|
| 39 |
|
|
| 40 | 40 |
(* Prints a constant value *) |
| 41 | 41 |
let rec pp_horn_const fmt c = |
| 42 | 42 |
match c with |
| ... | ... | |
| 276 | 276 |
end |
| 277 | 277 |
with Not_found -> ( (* stateless node instance *) |
| 278 | 278 |
let (n,_) = List.assoc i m.mcalls in |
| 279 |
fprintf fmt "(%s @[<v 0>%a%t%a)@]"
|
|
| 280 |
(node_name n) |
|
| 279 |
fprintf fmt "(%a @[<v 0>%a%t%a)@]"
|
|
| 280 |
pp_machine_stateless_name (node_name n)
|
|
| 281 | 281 |
(Utils.fprintf_list ~sep:"@ " (pp_horn_val self (pp_horn_var m))) |
| 282 | 282 |
inputs |
| 283 | 283 |
(Utils.pp_final_char_if_non_empty "@ " inputs) |
| ... | ... | |
| 327 | 327 |
let self = m.mname.node_id in |
| 328 | 328 |
let pp_branch fmt (tag, instrs) = |
| 329 | 329 |
fprintf fmt |
| 330 |
"@[<v 3>(or (not (= %a %s))@ "
|
|
| 330 |
"@[<v 3>(or (not (= %a %a))@ "
|
|
| 331 | 331 |
(*"@[<v 3>(=> (= %a %s)@ "*) (* Issues with some versions of Z3. It |
| 332 | 332 |
seems that => within Horn predicate |
| 333 | 333 |
may cause trouble. I have hard time |
| 334 | 334 |
producing a MWE, so I'll just keep the |
| 335 | 335 |
fix here as (not a) or b *) |
| 336 | 336 |
(pp_horn_val self (pp_horn_var m)) g |
| 337 |
tag; |
|
| 337 |
pp_horn_tag tag;
|
|
| 338 | 338 |
let _ (* rs *) = pp_machine_instrs machines reset_instances m fmt instrs in |
| 339 | 339 |
fprintf fmt "@])"; |
| 340 | 340 |
() (* rs *) |
Also available in: Unified diff
[HORN] Protect names of stateless nodes with a _fun suffix. This was conflicting with existing names in Z3, ie. "abs".
[HORN] Better treatment of stateless nodes collecting semantics
Fixes issue #13 on github: https://github.com/coco-team/lustrec/issues/13