Revision 9cab57c9
Added by Pierre-Loïc Garoche almost 10 years ago
| src/horn_backend.ml | ||
|---|---|---|
| 268 | 268 |
(Utils.fprintf_list ~sep:"@ " (pp_instr false m.mname.node_id)) m.mstep.step_instrs |
| 269 | 269 |
m.mname.node_id |
| 270 | 270 |
(Utils.fprintf_list ~sep:" " pp_var) (step_vars machines m); |
| 271 |
|
|
| 272 |
() |
|
| 273 |
) |
|
| 271 |
|
|
| 272 |
match m.mspec with |
|
| 273 |
None -> () (* No node spec; we do nothing *) |
|
| 274 |
| Some {requires = []; ensures = [EnsuresExpr e]; behaviors = []} ->
|
|
| 275 |
( |
|
| 276 |
(* For the moment, we only deal with simple case: single ensures, no other parameters *) |
|
| 277 |
() |
|
| 278 |
|
|
| 279 |
) |
|
| 280 |
| _ -> () (* Other cases give nothing *) |
|
| 281 |
) |
|
| 282 |
|
|
| 283 |
|
|
| 274 | 284 |
|
| 275 | 285 |
let main_print machines fmt = |
| 276 | 286 |
if !Options.main_node <> "" then |
| 277 | 287 |
begin |
| 278 | 288 |
let node = !Options.main_node in |
| 279 | 289 |
let machine = get_machine machines node in |
| 280 |
Format.fprintf fmt "; Collecting semantics with main node %s@.@." node; |
|
| 290 |
|
|
| 291 |
Format.fprintf fmt "; Collecting semantics for node %s@.@." node; |
|
| 281 | 292 |
(* We print the types of the main node "memory tree" TODO: add the output *) |
| 293 |
let main_output = |
|
| 294 |
rename_machine_list machine.mname.node_id machine.mstep.step_outputs |
|
| 295 |
in |
|
| 282 | 296 |
let main_memory_next = |
| 283 |
(rename_next_list (* machine.mname.node_id *) (full_memory_vars machines machine)) |
|
| 297 |
(rename_next_list (* machine.mname.node_id *) (full_memory_vars machines machine)) @ |
|
| 298 |
main_output |
|
| 284 | 299 |
in |
| 285 | 300 |
let main_memory_current = |
| 286 |
(rename_current_list (* machine.mname.node_id *) (full_memory_vars machines machine)) |
|
| 301 |
(rename_current_list (* machine.mname.node_id *) (full_memory_vars machines machine)) @ |
|
| 302 |
main_output |
|
| 287 | 303 |
in |
| 288 |
Format.fprintf fmt "(declare-rel MAIN (%a Bool))@."
|
|
| 304 |
Format.fprintf fmt "(declare-rel MAIN (%a))@." |
|
| 289 | 305 |
(Utils.fprintf_list ~sep:" " pp_type) |
| 290 | 306 |
(List.map (fun v -> v.var_type) main_memory_next); |
| 291 | 307 |
|
| 292 | 308 |
Format.fprintf fmt "; Initial set@."; |
| 293 | 309 |
Format.fprintf fmt "(declare-rel INIT_STATE ())@."; |
| 294 | 310 |
Format.fprintf fmt "(rule INIT_STATE)@."; |
| 295 |
Format.fprintf fmt "@[<v 2>(rule (=> @ (and @[<v 0>INIT_STATE@ (@[<v 0>%s_init %a@])@]@ )@ (MAIN %a top.OK)@]@.))@.@."
|
|
| 311 |
Format.fprintf fmt "@[<v 2>(rule (=> @ (and @[<v 0>INIT_STATE@ (@[<v 0>%s_init %a@])@]@ )@ (MAIN %a)@]@.))@.@." |
|
| 296 | 312 |
node |
| 297 | 313 |
(Utils.fprintf_list ~sep:" " pp_var) (init_vars machines machine) |
| 298 |
(Utils.fprintf_list ~sep:" " pp_var) main_memory_next; |
|
| 314 |
(Utils.fprintf_list ~sep:" " pp_var) main_memory_next ;
|
|
| 299 | 315 |
|
| 300 | 316 |
Format.fprintf fmt "; Inductive def@."; |
| 301 | 317 |
Format.fprintf fmt "(declare-var dummy Bool)@."; |
| 302 | 318 |
Format.fprintf fmt |
| 303 |
"@[<v 2>(rule (=> @ (and @[<v 0>(MAIN %a dummy)@ (@[<v 0>%s_step %a@])@]@ )@ (MAIN %a top.OK)@]@.))@.@."
|
|
| 319 |
"@[<v 2>(rule (=> @ (and @[<v 0>(MAIN %a dummy)@ (@[<v 0>%s_step %a@])@]@ )@ (MAIN %a)@]@.))@.@." |
|
| 304 | 320 |
(Utils.fprintf_list ~sep:" " pp_var) main_memory_current |
| 305 | 321 |
node |
| 306 | 322 |
(Utils.fprintf_list ~sep:" " pp_var) (step_vars machines machine) |
| 307 |
(Utils.fprintf_list ~sep:" " pp_var) main_memory_next; |
|
| 323 |
(Utils.fprintf_list ~sep:" " pp_var) main_memory_next ;
|
|
| 308 | 324 |
|
| 309 | 325 |
Format.fprintf fmt "; Property def@."; |
| 310 | 326 |
Format.fprintf fmt "(declare-rel ERR ())@."; |
| 311 | 327 |
Format.fprintf fmt "@[<v 2>(rule (=> @ (and @[<v 0>(not (= top.OK true))@ (MAIN %a)@])@ ERR))@." |
| 312 |
(Utils.fprintf_list ~sep:" " pp_var) main_memory_current; |
|
| 328 |
(Utils.fprintf_list ~sep:" " pp_var) main_memory_current |
|
| 329 |
; |
|
| 313 | 330 |
Format.fprintf fmt "(query ERR)@."; |
| 314 | 331 |
|
| 315 | 332 |
() |
| ... | ... | |
| 318 | 335 |
|
| 319 | 336 |
let translate fmt basename prog machines = |
| 320 | 337 |
List.iter (print_machine machines fmt) (List.rev machines); |
| 338 |
|
|
| 321 | 339 |
main_print machines fmt |
| 322 | 340 |
|
| 323 | 341 |
|
Also available in: Unified diff
...
git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/branches/horn_encoding@151 041b043f-8d7c-46b2-b46e-ef0dd855326e