Revision 4e809854
Added by Pierre-Loïc Garoche about 5 years ago
| src/backends/Horn/horn_backend_printers.ml | ||
|---|---|---|
| 245 | 245 |
in |
| 246 | 246 |
pp_conj pp_branch fmt hl; |
| 247 | 247 |
reset_instances |
| 248 |
|
|
| 248 |
| MComment _ -> [] |
|
| 249 |
|
|
| 249 | 250 |
and pp_machine_instrs machines reset_instances m fmt instrs = |
| 250 | 251 |
let ppi rs fmt i = pp_machine_instr machines rs m fmt i in |
| 251 | 252 |
match instrs with |
| ... | ... | |
| 296 | 297 |
fprintf fmt "@]@ )" |
| 297 | 298 |
|
| 298 | 299 |
|
| 299 |
|
|
| 300 | 300 |
(**************************************************************) |
| 301 | 301 |
|
| 302 | 302 |
let is_stateless m = m.minstances = [] && m.mmemory = [] |
| ... | ... | |
| 375 | 375 |
end |
| 376 | 376 |
| assertsl -> |
| 377 | 377 |
begin |
| 378 |
let pp_val = pp_horn_val ~is_lhs:true m.mname.node_id (pp_horn_var m) in
|
|
| 378 |
let pp_val = pp_horn_val ~is_lhs:true m.mname.node_id (pp_horn_var m) in
|
|
| 379 | 379 |
(* print_string pp_val; *) |
| 380 | 380 |
fprintf fmt "; with Assertions @."; |
| 381 | 381 |
|
| 382 | 382 |
(*Rule for step*) |
| 383 | 383 |
fprintf fmt "@[<v 2>(rule (=> @ (and @ "; |
| 384 | 384 |
ignore (pp_machine_instrs machines [] m fmt m.mstep.step_instrs); |
| 385 |
fprintf fmt "@. %a)(%a @[<v 0>%a)@]@]@.))@.@." (pp_conj pp_val) assertsl |
|
| 385 |
fprintf fmt "@. %a)" (pp_conj pp_val) assertsl; |
|
| 386 |
fprintf fmt "(%a @[<v 0>%a)@]@]@.))@.@." |
|
| 386 | 387 |
pp_machine_step_name m.mname.node_id |
| 387 | 388 |
(Utils.fprintf_list ~sep:" " (pp_horn_var m)) (step_vars machines m); |
| 388 | 389 |
end |
Also available in: Unified diff
Cosmetic changes