Revision 86ae18b7 src/backends/Horn/horn_backend_printers.ml
| src/backends/Horn/horn_backend_printers.ml | ||
|---|---|---|
| 21 | 21 |
open Machine_code |
| 22 | 22 |
|
| 23 | 23 |
open Horn_backend_common |
| 24 |
|
|
| 24 |
open Types |
|
| 25 | 25 |
|
| 26 | 26 |
(********************************************************************************************) |
| 27 | 27 |
(* Instruction Printing functions *) |
| 28 | 28 |
(********************************************************************************************) |
| 29 | 29 |
|
| 30 | 30 |
let pp_horn_var m fmt id = |
| 31 |
if Types.is_array_type id.var_type |
|
| 31 |
(*if Types.is_array_type id.var_type
|
|
| 32 | 32 |
then |
| 33 | 33 |
assert false (* no arrays in Horn output *) |
| 34 |
else |
|
| 34 |
else*)
|
|
| 35 | 35 |
fprintf fmt "%s" id.var_id |
| 36 | 36 |
|
| 37 | 37 |
(* Used to print boolean constants *) |
| ... | ... | |
| 46 | 46 |
| Const_tag t -> pp_horn_tag fmt t |
| 47 | 47 |
| _ -> assert false |
| 48 | 48 |
|
| 49 |
(* PL comment 2017/01/03: Useless code, the function existed before in typing.ml *) |
|
| 50 |
(* let rec get_type_cst c = *) |
|
| 51 |
(* match c with *) |
|
| 52 |
(* | Const_int(n) -> new_ty Tint *) |
|
| 53 |
(* | Const_real _ -> new_ty Treal *) |
|
| 54 |
(* (\* | Const_float _ -> new_ty Treal *\) *) |
|
| 55 |
(* | Const_array(l) -> new_ty (Tarray(Dimension.mkdim_int (Location.dummy_loc) (List.length l), *) |
|
| 56 |
(* get_type_cst (List.hd l))) *) |
|
| 57 |
(* | Const_tag(tag) -> new_ty Tbool *) |
|
| 58 |
(* | Const_string(str) -> assert false(\* used only for annotations *\) *) |
|
| 59 |
(* | Const_struct(l) -> new_ty (Tstruct(List.map (fun (label, t) -> (label, get_type_cst t)) l)) *) |
|
| 60 |
|
|
| 61 |
(* PL comment 2017/01/03: the following function get_type seems useless to me: it looks like computing the type of a machine code expression v while v.value_type should contain this information. The code is kept for the moment in case I missed something *) |
|
| 62 |
|
|
| 63 |
(* |
|
| 64 |
let rec get_type v = |
|
| 65 |
match v with |
|
| 66 |
| Cst c -> Typing.type_const Location.dummy_loc c (* get_type_cst c*) |
|
| 67 |
| Access(tab, index) -> begin |
|
| 68 |
let rec remove_link ltype = |
|
| 69 |
match (dynamic_type ltype).tdesc with |
|
| 70 |
| Tlink t -> t |
|
| 71 |
| _ -> ltype |
|
| 72 |
in |
|
| 73 |
match (dynamic_type (remove_link (get_type tab))).tdesc with |
|
| 74 |
| Tarray(size, t) -> remove_link t |
|
| 75 |
| Tvar -> Format.eprintf "Type of access is a variable... "; assert false |
|
| 76 |
| Tunivar -> Format.eprintf "Type of access is a variable... "; assert false |
|
| 77 |
| _ -> Format.eprintf "Type of access is not an array "; assert false |
|
| 78 |
end |
|
| 79 |
| Power(v, n) -> assert false |
|
| 80 |
| LocalVar v -> v.var_type |
|
| 81 |
| StateVar v -> v.var_type |
|
| 82 |
| Fun(n, vl) -> begin match n with |
|
| 83 |
| "+" |
|
| 84 |
| "-" |
|
| 85 |
| "*" -> get_type (List.hd vl) |
|
| 86 |
| _ -> Format.eprintf "Function undealt with : %s" n ;assert false |
|
| 87 |
end |
|
| 88 |
| Array(l) -> new_ty (Tarray(Dimension.mkdim_int |
|
| 89 |
(Location.dummy_loc) |
|
| 90 |
(List.length l), |
|
| 91 |
get_type (List.hd l))) |
|
| 92 |
| _ -> assert false |
|
| 93 |
*) |
|
| 94 |
|
|
| 95 |
(* Default value for each type, used when building arrays. Eg integer array |
|
| 96 |
[2;7] is defined as (store (store (0) 1 7) 0 2) where 0 is this default value |
|
| 97 |
for the type integer (arrays). |
|
| 98 |
*) |
|
| 99 |
let rec pp_default_val fmt t = |
|
| 100 |
match (dynamic_type t).tdesc with |
|
| 101 |
| Tint -> fprintf fmt "0" |
|
| 102 |
| Treal -> fprintf fmt "0" |
|
| 103 |
| Tbool -> fprintf fmt "true" |
|
| 104 |
| Tarray(dim, l) -> (* TODO PL: this strange code has to be (heavily) checked *) |
|
| 105 |
let valt = array_element_type t in |
|
| 106 |
fprintf fmt "((as const (Array Int %a)) %a)" |
|
| 107 |
pp_type valt |
|
| 108 |
pp_default_val valt |
|
| 109 |
| Tstruct(l) -> assert false |
|
| 110 |
| Ttuple(l) -> assert false |
|
| 111 |
|_ -> assert false |
|
| 112 |
|
|
| 113 |
|
|
| 49 | 114 |
(* Prints a value expression [v], with internal function calls only. |
| 50 | 115 |
[pp_var] is a printer for variables (typically [pp_c_var_read]), |
| 51 | 116 |
but an offset suffix may be added for array variables |
| 52 | 117 |
*) |
| 53 | 118 |
let rec pp_horn_val ?(is_lhs=false) self pp_var fmt v = |
| 54 | 119 |
match v.value_desc with |
| 55 |
| Cst c -> pp_horn_const fmt c |
|
| 56 |
| Array _ |
|
| 57 |
| Access _ -> assert false (* no arrays *) |
|
| 58 |
| Power (v, n) -> assert false |
|
| 59 |
| LocalVar v -> pp_var fmt (rename_machine self v) |
|
| 60 |
| StateVar v -> |
|
| 61 |
if Types.is_array_type v.var_type |
|
| 62 |
then assert false |
|
| 63 |
else pp_var fmt (rename_machine self ((if is_lhs then rename_next else rename_current) (* self *) v)) |
|
| 64 |
| Fun (n, vl) -> fprintf fmt "%a" (Basic_library.pp_horn n (pp_horn_val self pp_var)) vl |
|
| 120 |
| Cst c -> pp_horn_const fmt c |
|
| 121 |
|
|
| 122 |
(* Code specific for arrays *) |
|
| 123 |
| Array il -> |
|
| 124 |
(* An array definition: |
|
| 125 |
(store ( |
|
| 126 |
... |
|
| 127 |
(store ( |
|
| 128 |
store ( |
|
| 129 |
default_val |
|
| 130 |
) |
|
| 131 |
idx_n val_n |
|
| 132 |
) |
|
| 133 |
idx_n-1 val_n-1) |
|
| 134 |
... |
|
| 135 |
idx_1 val_1 |
|
| 136 |
) *) |
|
| 137 |
let rec print fmt (tab, x) = |
|
| 138 |
match tab with |
|
| 139 |
| [] -> pp_default_val fmt v.value_type(* (get_type v) *) |
|
| 140 |
| h::t -> |
|
| 141 |
fprintf fmt "(store %a %i %a)" |
|
| 142 |
print (t, (x+1)) |
|
| 143 |
x |
|
| 144 |
(pp_horn_val ~is_lhs:is_lhs self pp_var) h |
|
| 145 |
in |
|
| 146 |
print fmt (il, 0) |
|
| 147 |
|
|
| 148 |
| Access(tab,index) -> |
|
| 149 |
fprintf fmt "(select %a %a)" |
|
| 150 |
(pp_horn_val ~is_lhs:is_lhs self pp_var) tab |
|
| 151 |
(pp_horn_val ~is_lhs:is_lhs self pp_var) index |
|
| 152 |
|
|
| 153 |
(* Code specific for arrays *) |
|
| 154 |
|
|
| 155 |
| Power (v, n) -> assert false |
|
| 156 |
| LocalVar v -> pp_var fmt (rename_machine self v) |
|
| 157 |
| StateVar v -> |
|
| 158 |
if Types.is_array_type v.var_type |
|
| 159 |
then assert false |
|
| 160 |
else pp_var fmt (rename_machine self ((if is_lhs then rename_next else rename_current) (* self *) v)) |
|
| 161 |
| Fun (n, vl) -> fprintf fmt "%a" (Basic_library.pp_horn n (pp_horn_val self pp_var)) vl |
|
| 65 | 162 |
|
| 66 | 163 |
(* Prints a [value] indexed by the suffix list [loop_vars] *) |
| 67 | 164 |
let rec pp_value_suffix self pp_value fmt value = |
| ... | ... | |
| 79 | 176 |
*) |
| 80 | 177 |
let pp_assign m pp_var fmt var_name value = |
| 81 | 178 |
let self = m.mname.node_id in |
| 82 |
fprintf fmt "(= %a %a)"
|
|
| 179 |
fprintf fmt "(= %a %a)" |
|
| 83 | 180 |
(pp_horn_val ~is_lhs:true self pp_var) var_name |
| 84 | 181 |
(pp_value_suffix self pp_var) value |
| 85 |
|
|
| 182 |
|
|
| 86 | 183 |
|
| 87 | 184 |
(* In case of no reset call, we define mid_mem = current_mem *) |
| 88 | 185 |
let pp_no_reset machines m fmt i = |
| 89 | 186 |
let (n,_) = List.assoc i m.minstances in |
| 90 | 187 |
let target_machine = List.find (fun m -> m.mname.node_id = (node_name n)) machines in |
| 91 | 188 |
|
| 92 |
let m_list =
|
|
| 189 |
let m_list = |
|
| 93 | 190 |
rename_machine_list |
| 94 | 191 |
(concat m.mname.node_id i) |
| 95 | 192 |
(rename_mid_list (full_memory_vars machines target_machine)) |
| ... | ... | |
| 104 | 201 |
fprintf fmt "(= %a %a)" |
| 105 | 202 |
(pp_horn_var m) mhd |
| 106 | 203 |
(pp_horn_var m) chd |
| 107 |
|
|
| 204 |
|
|
| 108 | 205 |
| _ -> ( |
| 109 | 206 |
fprintf fmt "@[<v 0>(and @[<v 0>"; |
| 110 |
List.iter2 (fun mhd chd ->
|
|
| 207 |
List.iter2 (fun mhd chd -> |
|
| 111 | 208 |
fprintf fmt "(= %a %a)@ " |
| 112 | 209 |
(pp_horn_var m) mhd |
| 113 | 210 |
(pp_horn_var m) chd |
| ... | ... | |
| 120 | 217 |
let pp_instance_reset machines m fmt i = |
| 121 | 218 |
let (n,_) = List.assoc i m.minstances in |
| 122 | 219 |
let target_machine = List.find (fun m -> m.mname.node_id = (node_name n)) machines in |
| 123 |
|
|
| 220 |
|
|
| 124 | 221 |
fprintf fmt "(%a @[<v 0>%a)@]" |
| 125 | 222 |
pp_machine_reset_name (node_name n) |
| 126 |
(Utils.fprintf_list ~sep:"@ " (pp_horn_var m))
|
|
| 223 |
(Utils.fprintf_list ~sep:"@ " (pp_horn_var m)) |
|
| 127 | 224 |
( |
| 128 | 225 |
(rename_machine_list |
| 129 | 226 |
(concat m.mname.node_id i) |
| 130 | 227 |
(rename_current_list (full_memory_vars machines target_machine)) |
| 131 |
)
|
|
| 228 |
) |
|
| 132 | 229 |
@ |
| 133 | 230 |
(rename_machine_list |
| 134 | 231 |
(concat m.mname.node_id i) |
| ... | ... | |
| 146 | 243 |
if not (List.mem i reset_instances) then |
| 147 | 244 |
(* If not, declare mem_m = mem_c *) |
| 148 | 245 |
pp_no_reset machines m fmt i; |
| 149 |
|
|
| 246 |
|
|
| 150 | 247 |
let mems = full_memory_vars machines target_machine in |
| 151 | 248 |
let rename_mems f = rename_machine_list (concat m.mname.node_id i) (f mems) in |
| 152 | 249 |
let mid_mems = rename_mems rename_mid_list in |
| ... | ... | |
| 157 | 254 |
fprintf fmt "@[<v 5>(and "; |
| 158 | 255 |
fprintf fmt "(= %a (ite %a %a %a))" |
| 159 | 256 |
(pp_horn_val ~is_lhs:true self (pp_horn_var m)) (mk_val (LocalVar o) o.var_type) (* output var *) |
| 160 |
(pp_horn_var m) mem_m
|
|
| 257 |
(pp_horn_var m) mem_m |
|
| 161 | 258 |
(pp_horn_val self (pp_horn_var m)) i1 |
| 162 | 259 |
(pp_horn_val self (pp_horn_var m)) i2 |
| 163 | 260 |
; |
| ... | ... | |
| 175 | 272 |
(List.map (fun v -> mk_val (LocalVar v) v.var_type) outputs) |
| 176 | 273 |
(Utils.pp_final_char_if_non_empty "@ " outputs) |
| 177 | 274 |
(Utils.fprintf_list ~sep:"@ " (pp_horn_var m)) (mid_mems@next_mems) |
| 178 |
|
|
| 275 |
|
|
| 179 | 276 |
end |
| 180 | 277 |
end |
| 181 | 278 |
with Not_found -> ( (* stateless node instance *) |
| ... | ... | |
| 188 | 285 |
(Utils.fprintf_list ~sep:"@ " (pp_horn_val self (pp_horn_var m))) |
| 189 | 286 |
(List.map (fun v -> mk_val (LocalVar v) v.var_type) outputs) |
| 190 | 287 |
) |
| 191 |
|
|
| 192 |
|
|
| 288 |
|
|
| 289 |
|
|
| 193 | 290 |
(* Print the instruction and update the set of reset instances *) |
| 194 | 291 |
let rec pp_machine_instr machines reset_instances (m: machine_t) fmt instr : ident list = |
| 195 | 292 |
match instr with |
| ... | ... | |
| 230 | 327 |
statement. *) |
| 231 | 328 |
let self = m.mname.node_id in |
| 232 | 329 |
let pp_branch fmt (tag, instrs) = |
| 233 |
fprintf fmt
|
|
| 234 |
"@[<v 3>(or (not (= %a %s))@ "
|
|
| 330 |
fprintf fmt |
|
| 331 |
"@[<v 3>(or (not (= %a %s))@ " |
|
| 235 | 332 |
(*"@[<v 3>(=> (= %a %s)@ "*) (* Issues with some versions of Z3. It |
| 236 | 333 |
seems that => within Horn predicate |
| 237 | 334 |
may cause trouble. I have hard time |
| ... | ... | |
| 244 | 341 |
() (* rs *) |
| 245 | 342 |
in |
| 246 | 343 |
pp_conj pp_branch fmt hl; |
| 247 |
reset_instances
|
|
| 344 |
reset_instances |
|
| 248 | 345 |
|
| 249 |
and pp_machine_instrs machines reset_instances m fmt instrs =
|
|
| 346 |
and pp_machine_instrs machines reset_instances m fmt instrs = |
|
| 250 | 347 |
let ppi rs fmt i = pp_machine_instr machines rs m fmt i in |
| 251 | 348 |
match instrs with |
| 252 |
| [x] -> ppi reset_instances fmt x
|
|
| 349 |
| [x] -> ppi reset_instances fmt x |
|
| 253 | 350 |
| _::_ -> |
| 254 | 351 |
fprintf fmt "(and @[<v 0>"; |
| 255 |
let rs = List.fold_left (fun rs i ->
|
|
| 352 |
let rs = List.fold_left (fun rs i -> |
|
| 256 | 353 |
let rs = ppi rs fmt i in |
| 257 | 354 |
fprintf fmt "@ "; |
| 258 | 355 |
rs |
| 259 | 356 |
) |
| 260 |
reset_instances instrs
|
|
| 357 |
reset_instances instrs |
|
| 261 | 358 |
in |
| 262 | 359 |
fprintf fmt "@])"; |
| 263 | 360 |
rs |
| ... | ... | |
| 269 | 366 |
fprintf fmt "@[<v 5>(and @ "; |
| 270 | 367 |
|
| 271 | 368 |
(* print "x_m = x_c" for each local memory *) |
| 272 |
(Utils.fprintf_list ~sep:"@ " (fun fmt v ->
|
|
| 369 |
(Utils.fprintf_list ~sep:"@ " (fun fmt v -> |
|
| 273 | 370 |
fprintf fmt "(= %a %a)" |
| 274 | 371 |
(pp_horn_var m) (rename_mid v) |
| 275 | 372 |
(pp_horn_var m) (rename_current v) |
| ... | ... | |
| 281 | 378 |
*) |
| 282 | 379 |
(Utils.fprintf_list ~sep:"@ " (fun fmt (id, (n, _)) -> |
| 283 | 380 |
let name = node_name n in |
| 284 |
if name = "_arrow" then (
|
|
| 381 |
if name = "_arrow" then ( |
|
| 285 | 382 |
fprintf fmt "(= %s._arrow._first_m true)" |
| 286 |
(concat m.mname.node_id id)
|
|
| 383 |
(concat m.mname.node_id id) |
|
| 287 | 384 |
) else ( |
| 288 |
let machine_n = get_machine machines name in
|
|
| 289 |
fprintf fmt "(%s_reset @[<hov 0>%a@])"
|
|
| 385 |
let machine_n = get_machine machines name in |
|
| 386 |
fprintf fmt "(%s_reset @[<hov 0>%a@])" |
|
| 290 | 387 |
name |
| 291 |
(Utils.fprintf_list ~sep:"@ " (pp_horn_var m))
|
|
| 388 |
(Utils.fprintf_list ~sep:"@ " (pp_horn_var m)) |
|
| 292 | 389 |
(rename_machine_list (concat m.mname.node_id id) (reset_vars machines machine_n)) |
| 293 | 390 |
) |
| 294 | 391 |
)) fmt m.minstances; |
| ... | ... | |
| 314 | 411 |
else |
| 315 | 412 |
begin |
| 316 | 413 |
fprintf fmt "; %s@." m.mname.node_id; |
| 317 |
|
|
| 414 |
|
|
| 318 | 415 |
(* Printing variables *) |
| 319 | 416 |
Utils.fprintf_list ~sep:"@." pp_decl_var fmt |
| 320 | 417 |
( |
| ... | ... | |
| 358 | 455 |
|
| 359 | 456 |
(* Rule for reset *) |
| 360 | 457 |
fprintf fmt "@[<v 2>(rule (=> @ %a@ (%a @[<v 0>%a)@]@]@.))@.@." |
| 361 |
(pp_machine_reset machines) m
|
|
| 458 |
(pp_machine_reset machines) m |
|
| 362 | 459 |
pp_machine_reset_name m.mname.node_id |
| 363 | 460 |
(Utils.fprintf_list ~sep:"@ " (pp_horn_var m)) (reset_vars machines m); |
| 364 | 461 |
|
| ... | ... | |
| 373 | 470 |
pp_machine_step_name m.mname.node_id |
| 374 | 471 |
(Utils.fprintf_list ~sep:"@ " (pp_horn_var m)) (step_vars machines m); |
| 375 | 472 |
end |
| 376 |
| assertsl ->
|
|
| 473 |
| assertsl -> |
|
| 377 | 474 |
begin |
| 378 | 475 |
let pp_val = pp_horn_val ~is_lhs:true m.mname.node_id (pp_horn_var m) in |
| 379 | 476 |
(* print_string pp_val; *) |
| 380 | 477 |
fprintf fmt "; with Assertions @."; |
| 381 |
|
|
| 478 |
|
|
| 382 | 479 |
(*Rule for step*) |
| 383 | 480 |
fprintf fmt "@[<v 2>(rule (=> @ (and @ "; |
| 384 | 481 |
ignore (pp_machine_instrs machines [] m fmt m.mstep.step_instrs); |
| ... | ... | |
| 386 | 483 |
pp_machine_step_name m.mname.node_id |
| 387 | 484 |
(Utils.fprintf_list ~sep:" " (pp_horn_var m)) (step_vars machines m); |
| 388 | 485 |
end |
| 389 |
|
|
| 390 |
|
|
| 486 |
|
|
| 487 |
|
|
| 391 | 488 |
end |
| 392 | 489 |
end |
| 393 | 490 |
|
| 394 | 491 |
|
| 492 |
let mk_flags arity = |
|
| 493 |
let b_range = |
|
| 494 |
let rec range i j = |
|
| 495 |
if i > arity then [] else i :: (range (i+1) j) in |
|
| 496 |
range 2 arity; |
|
| 497 |
in |
|
| 498 |
List.fold_left (fun acc x -> acc ^ " false") "true" b_range |
|
| 499 |
|
|
| 500 |
|
|
| 501 |
(*Get sfunction infos from command line*) |
|
| 502 |
let get_sf_info() = |
|
| 503 |
let splitted = Str.split (Str.regexp "@") !Options.sfunction in |
|
| 504 |
Log.report ~level:1 (fun fmt -> fprintf fmt ".. sfunction name: %s@," !Options.sfunction); |
|
| 505 |
let sf_name, flags, arity = match splitted with |
|
| 506 |
[h;flg;par] -> h, flg, par |
|
| 507 |
| _ -> failwith "Wrong Sfunction info" |
|
| 508 |
|
|
| 509 |
in |
|
| 510 |
Log.report ~level:1 (fun fmt -> fprintf fmt "... sf_name: %s@, .. flags: %s@ .. arity: %s@," sf_name flags arity); |
|
| 511 |
sf_name, flags, arity |
|
| 512 |
|
|
| 513 |
|
|
| 514 |
(*a function to print the rules in case we have an s-function*) |
|
| 515 |
let print_sfunction machines fmt m = |
|
| 516 |
if m.mname.node_id = arrow_id then |
|
| 517 |
(* We don't print arrow function *) |
|
| 518 |
() |
|
| 519 |
else |
|
| 520 |
begin |
|
| 521 |
Format.fprintf fmt "; SFUNCTION@."; |
|
| 522 |
Format.fprintf fmt "; %s@." m.mname.node_id; |
|
| 523 |
Format.fprintf fmt "; EndPoint Predicate %s." !Options.sfunction; |
|
| 524 |
|
|
| 525 |
(* Check if there is annotation for s-function *) |
|
| 526 |
if m.mannot != [] then( |
|
| 527 |
Format.fprintf fmt "; @[%a@]@]@\n" (Utils.fprintf_list ~sep:"@ " Printers.pp_s_function) m.mannot; |
|
| 528 |
); |
|
| 529 |
|
|
| 530 |
(* Printing variables *) |
|
| 531 |
Utils.fprintf_list ~sep:"@." pp_decl_var fmt |
|
| 532 |
((step_vars machines m)@ |
|
| 533 |
(rename_machine_list m.mname.node_id m.mstep.step_locals)); |
|
| 534 |
Format.pp_print_newline fmt (); |
|
| 535 |
let sf_name, flags, arity = get_sf_info() in |
|
| 536 |
|
|
| 537 |
if is_stateless m then |
|
| 538 |
begin |
|
| 539 |
(* Declaring single predicate *) |
|
| 540 |
Format.fprintf fmt "(declare-rel %a (%a))@." |
|
| 541 |
pp_machine_stateless_name m.mname.node_id |
|
| 542 |
(Utils.fprintf_list ~sep:" " pp_type) |
|
| 543 |
(List.map (fun v -> v.var_type) (reset_vars machines m)); |
|
| 544 |
Format.pp_print_newline fmt (); |
|
| 545 |
(* Rule for single predicate *) |
|
| 546 |
let str_flags = sf_name ^ " " ^ mk_flags (int_of_string flags) in |
|
| 547 |
Format.fprintf fmt "@[<v 2>(rule (=> @ (%s %a) (%a %a)@]@.))@.@." |
|
| 548 |
str_flags |
|
| 549 |
(Utils.fprintf_list ~sep:" " (pp_horn_var m)) (reset_vars machines m) |
|
| 550 |
pp_machine_stateless_name m.mname.node_id |
|
| 551 |
(Utils.fprintf_list ~sep:" " (pp_horn_var m)) (reset_vars machines m); |
|
| 552 |
end |
|
| 553 |
else |
|
| 554 |
begin |
|
| 555 |
(* Declaring predicate *) |
|
| 556 |
Format.fprintf fmt "(declare-rel %a (%a))@." |
|
| 557 |
pp_machine_reset_name m.mname.node_id |
|
| 558 |
(Utils.fprintf_list ~sep:" " pp_type) |
|
| 559 |
(List.map (fun v -> v.var_type) (inout_vars machines m)); |
|
| 560 |
|
|
| 561 |
Format.fprintf fmt "(declare-rel %a (%a))@." |
|
| 562 |
pp_machine_step_name m.mname.node_id |
|
| 563 |
(Utils.fprintf_list ~sep:" " pp_type) |
|
| 564 |
(List.map (fun v -> v.var_type) (step_vars machines m)); |
|
| 565 |
|
|
| 566 |
Format.pp_print_newline fmt (); |
|
| 567 |
(* Adding assertions *) |
|
| 568 |
match m.mstep.step_asserts with |
|
| 569 |
| [] -> |
|
| 570 |
begin |
|
| 571 |
|
|
| 572 |
(* Rule for step*) |
|
| 573 |
fprintf fmt "@[<v 2>(rule (=> @ "; |
|
| 574 |
ignore (pp_machine_instrs machines [] m fmt m.mstep.step_instrs); |
|
| 575 |
fprintf fmt "@ (%a @[<v 0>%a)@]@]@.))@.@." |
|
| 576 |
pp_machine_step_name m.mname.node_id |
|
| 577 |
(Utils.fprintf_list ~sep:"@ " (pp_horn_var m)) (step_vars machines m); |
|
| 578 |
end |
|
| 579 |
| assertsl -> |
|
| 580 |
begin |
|
| 581 |
let pp_val = pp_horn_val ~is_lhs:true m.mname.node_id (pp_horn_var m) in |
|
| 582 |
(* print_string pp_val; *) |
|
| 583 |
fprintf fmt "; with Assertions @."; |
|
| 584 |
|
|
| 585 |
(*Rule for step*) |
|
| 586 |
fprintf fmt "@[<v 2>(rule (=> @ (and @ "; |
|
| 587 |
ignore (pp_machine_instrs machines [] m fmt m.mstep.step_instrs); |
|
| 588 |
fprintf fmt "@. %a)(%a @[<v 0>%a)@]@]@.))@.@." (pp_conj pp_val) assertsl |
|
| 589 |
pp_machine_step_name m.mname.node_id |
|
| 590 |
(Utils.fprintf_list ~sep:" " (pp_horn_var m)) (step_vars machines m); |
|
| 591 |
end |
|
| 592 |
|
|
| 593 |
end |
|
| 594 |
|
|
| 595 |
end |
|
| 395 | 596 |
(* Local Variables: *) |
| 396 | 597 |
(* compile-command:"make -C ../../.." *) |
| 397 | 598 |
(* End: *) |
Also available in: Unified diff