Revision 07ceae4c
Added by Pierre-Loïc Garoche almost 6 years ago
| src/backends/Horn/horn_backend_collecting_sem.ml | ||
|---|---|---|
| 41 | 41 |
main_output_dummy |
| 42 | 42 |
in |
| 43 | 43 |
|
| 44 |
(* Special case when the main node is stateless *) |
|
| 45 |
let reset_name, step_name = |
|
| 46 |
if is_stateless machine then |
|
| 47 |
pp_machine_stateless_name, pp_machine_stateless_name |
|
| 48 |
else |
|
| 49 |
pp_machine_reset_name, pp_machine_step_name |
|
| 50 |
in |
|
| 51 |
|
|
| 52 | 44 |
fprintf fmt "(declare-rel MAIN (%a))@." |
| 53 | 45 |
(Utils.fprintf_list ~sep:" " pp_type) |
| 54 | 46 |
(List.map (fun v -> v.var_type) main_memory_next); |
| 55 | 47 |
|
| 56 |
fprintf fmt "; Initial set: Reset(c,m) + One Step(m,x) @."; |
|
| 57 |
fprintf fmt "(declare-rel INIT_STATE ())@."; |
|
| 58 |
fprintf fmt "(rule INIT_STATE)@."; |
|
| 59 |
fprintf fmt "@[<v 2>(rule (=> @ (and @[<v 0>"; |
|
| 60 |
fprintf fmt "INIT_STATE@ "; |
|
| 61 |
fprintf fmt "(@[<v 0>%a %a@])@ " |
|
| 62 |
reset_name node |
|
| 63 |
(Utils.fprintf_list ~sep:" " (pp_horn_var machine)) (reset_vars machines machine); |
|
| 64 |
fprintf fmt "(@[<v 0>%a %a@])" |
|
| 65 |
step_name node |
|
| 66 |
(Utils.fprintf_list ~sep:" " (pp_horn_var machine)) (step_vars_m_x machines machine); |
|
| 67 |
|
|
| 68 |
fprintf fmt "@]@ )@ "; |
|
| 69 |
fprintf fmt "(MAIN %a)@]@.))@.@." |
|
| 70 |
(Utils.fprintf_list ~sep:" " (pp_horn_var machine)) main_memory_next ; |
|
| 48 |
|
|
| 49 |
(* Init case *) |
|
| 50 |
let _ = |
|
| 51 |
(* Special case when the main node is stateless *) |
|
| 52 |
if is_stateless machine then ( |
|
| 53 |
let step_name = pp_machine_stateless_name in |
|
| 54 |
fprintf fmt "; Initial set: One Step(m,x) -- Stateless node! @."; |
|
| 55 |
fprintf fmt "(declare-rel INIT_STATE ())@."; |
|
| 56 |
fprintf fmt "(rule INIT_STATE)@."; |
|
| 57 |
fprintf fmt "@[<v 2>(rule (=> @ (and @[<v 0>"; |
|
| 58 |
fprintf fmt "INIT_STATE@ "; |
|
| 59 |
fprintf fmt "(@[<v 0>%a %a@])" |
|
| 60 |
step_name node |
|
| 61 |
(Utils.fprintf_list ~sep:" " (pp_horn_var machine)) (step_vars_m_x machines machine); |
|
| 62 |
fprintf fmt "@]@ )@ "; |
|
| 63 |
fprintf fmt "(MAIN %a)@]@.))@.@." |
|
| 64 |
(Utils.fprintf_list ~sep:" " (pp_horn_var machine)) main_memory_next ; |
|
| 65 |
) |
|
| 66 |
else ( |
|
| 67 |
let reset_name, step_name = |
|
| 68 |
pp_machine_reset_name, pp_machine_step_name |
|
| 69 |
in |
|
| 70 |
fprintf fmt "; Initial set: Reset(c,m) + One Step(m,x) @."; |
|
| 71 |
fprintf fmt "(declare-rel INIT_STATE ())@."; |
|
| 72 |
fprintf fmt "(rule INIT_STATE)@."; |
|
| 73 |
fprintf fmt "@[<v 2>(rule (=> @ (and @[<v 0>"; |
|
| 74 |
fprintf fmt "INIT_STATE@ "; |
|
| 75 |
fprintf fmt "(@[<v 0>%a %a@])@ " |
|
| 76 |
reset_name node |
|
| 77 |
(Utils.fprintf_list ~sep:" " (pp_horn_var machine)) (reset_vars machines machine); |
|
| 78 |
fprintf fmt "(@[<v 0>%a %a@])" |
|
| 79 |
step_name node |
|
| 80 |
(Utils.fprintf_list ~sep:" " (pp_horn_var machine)) (step_vars_m_x machines machine); |
|
| 81 |
|
|
| 82 |
fprintf fmt "@]@ )@ "; |
|
| 83 |
fprintf fmt "(MAIN %a)@]@.))@.@." |
|
| 84 |
(Utils.fprintf_list ~sep:" " (pp_horn_var machine)) main_memory_next ; |
|
| 85 |
) |
|
| 86 |
in |
|
| 71 | 87 |
|
| 88 |
let step_name = |
|
| 89 |
if is_stateless machine then |
|
| 90 |
pp_machine_stateless_name |
|
| 91 |
else |
|
| 92 |
pp_machine_step_name |
|
| 93 |
in |
|
| 94 |
|
|
| 72 | 95 |
fprintf fmt "; Inductive def@."; |
| 73 | 96 |
(Utils.fprintf_list ~sep:" " (fun fmt v -> fprintf fmt "%a@." pp_decl_var v)) fmt main_output_dummy; |
| 74 | 97 |
fprintf fmt |
| src/backends/Horn/horn_backend_common.ml | ||
|---|---|---|
| 16 | 16 |
|
| 17 | 17 |
let pp_machine_reset_name fmt id = fprintf fmt "%s_reset" id |
| 18 | 18 |
let pp_machine_step_name fmt id = fprintf fmt "%s_step" id |
| 19 |
let pp_machine_stateless_name fmt id = fprintf fmt "%s" id |
|
| 19 |
let pp_machine_stateless_name fmt id = fprintf fmt "%s_fun" id
|
|
| 20 | 20 |
|
| 21 | 21 |
let rec pp_type fmt t = |
| 22 | 22 |
match (Types.repr t).Types.tdesc with |
| 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