Project

General

Profile

« Previous | Next » 

Revision ca7ff3f7

Added by LĂ©lio Brun 7 months ago

reformatting

View differences:

src/backends/Horn/horn_backend_printers.ml
12 12
(* The compilation presented here was first defined in Garoche, Gurfinkel,
13 13
   Kahsai, HCSV'14.
14 14

  
15
   This is a modified version that handle reset
16
*)
15
   This is a modified version that handle reset *)
17 16

  
18 17
open Format
19 18
open Lustre_types
20 19
open Machine_code_types
21 20
open Corelang
22 21
open Machine_code_common
23

  
24 22
open Horn_backend_common
25
  
23

  
26 24
(********************************************************************************************)
27
(*                    Instruction Printing functions                                        *)
25
(* Instruction Printing functions *)
28 26
(********************************************************************************************)
29 27

  
30 28
let pp_horn_var _ fmt id =
31
  (*if Types.is_array_type id.var_type
32
  then
33
    assert false (* no arrays in Horn output *)
34
  else*)
35
    fprintf fmt "%s" id.var_id
29
  (*if Types.is_array_type id.var_type then assert false (* no arrays in Horn
30
    output *) else*)
31
  fprintf fmt "%s" id.var_id
36 32

  
37 33
(* Used to print boolean constants *)
38 34
let pp_horn_tag fmt t =
39
  pp_print_string fmt (if t = tag_true then "true" else if t = tag_false then "false" else t)
40
    
35
  pp_print_string fmt
36
    (if t = tag_true then "true" else if t = tag_false then "false" else t)
37

  
41 38
(* Prints a constant value *)
42 39
let pp_horn_const fmt c =
43 40
  match c with
44
    | Const_int i    -> pp_print_int fmt i
45
    | Const_real r   -> Real.pp fmt r
46
    | Const_tag t    -> pp_horn_tag fmt t
47
    | _              -> assert false
41
  | Const_int i ->
42
    pp_print_int fmt i
43
  | Const_real r ->
44
    Real.pp fmt r
45
  | Const_tag t ->
46
    pp_horn_tag fmt t
47
  | _ ->
48
    assert false
48 49

  
49 50
(* Default value for each type, used when building arrays. Eg integer array
50 51
   [2;7] is defined as (store (store (0) 1 7) 0 2) where 0 is this default value
51
   for the type integer (arrays).
52
*)
52
   for the type integer (arrays). *)
53 53
let rec pp_default_val fmt t =
54 54
  let t = Types.dynamic_type t in
55
  if Types.is_bool_type t  then fprintf fmt "true" else
56
  if Types.is_int_type t then fprintf fmt "0" else 
57
  if Types.is_real_type t then fprintf fmt "0" else 
58
  match (Types.dynamic_type t).Types.tdesc with
59
  | Types.Tarray _ -> (* TODO PL: this strange code has to be (heavily) checked *)
60
     let valt = Types.array_element_type t in
61
     fprintf fmt "((as const (Array Int %a)) %a)"
62
       pp_type valt 
63
       pp_default_val valt
64
  | Types.Tstruct _ -> assert false
65
  | Types.Ttuple _ -> assert false
66
  |_ -> assert false
55
  if Types.is_bool_type t then fprintf fmt "true"
56
  else if Types.is_int_type t then fprintf fmt "0"
57
  else if Types.is_real_type t then fprintf fmt "0"
58
  else
59
    match (Types.dynamic_type t).Types.tdesc with
60
    | Types.Tarray _ ->
61
      (* TODO PL: this strange code has to be (heavily) checked *)
62
      let valt = Types.array_element_type t in
63
      fprintf fmt "((as const (Array Int %a)) %a)" pp_type valt pp_default_val
64
        valt
65
    | Types.Tstruct _ ->
66
      assert false
67
    | Types.Ttuple _ ->
68
      assert false
69
    | _ ->
70
      assert false
67 71

  
68 72
let pp_mod pp_val v1 v2 fmt =
69
  if Types.is_int_type v1.value_type &&  not !Options.integer_div_euclidean then
70
    (* C semantics: converting it from Euclidean operators
71
       (a mod_M b) - ((a mod_M b > 0 && a < 0) ? abs(b) : 0)            
72
    *)
73
    Format.fprintf fmt "(- (mod %a %a) (ite (and (> (mod %a %a) 0) (< %a 0)) (abs %a) 0))"
74
      pp_val v1 pp_val v2
75
      pp_val v1 pp_val v2
76
      pp_val v1
77
      pp_val v2
78
  else
79
    Format.fprintf fmt "(mod %a %a)" pp_val v1 pp_val v2
73
  if Types.is_int_type v1.value_type && not !Options.integer_div_euclidean then
74
    (* C semantics: converting it from Euclidean operators (a mod_M b) - ((a
75
       mod_M b > 0 && a < 0) ? abs(b) : 0) *)
76
    Format.fprintf fmt
77
      "(- (mod %a %a) (ite (and (> (mod %a %a) 0) (< %a 0)) (abs %a) 0))" pp_val
78
      v1 pp_val v2 pp_val v1 pp_val v2 pp_val v1 pp_val v2
79
  else Format.fprintf fmt "(mod %a %a)" pp_val v1 pp_val v2
80 80

  
81 81
let pp_div pp_val v1 v2 fmt =
82
  if Types.is_int_type v1.value_type &&  not !Options.integer_div_euclidean then
83
    (* C semantics: converting it from Euclidean operators
84
       (a - (a mod_C b)) div_M b
85
    *)
86
    Format.fprintf fmt "(div (- %a %t) %a)"
87
      pp_val v1
88
      (pp_mod pp_val v1 v2)
82
  if Types.is_int_type v1.value_type && not !Options.integer_div_euclidean then
83
    (* C semantics: converting it from Euclidean operators (a - (a mod_C b))
84
       div_M b *)
85
    Format.fprintf fmt "(div (- %a %t) %a)" pp_val v1 (pp_mod pp_val v1 v2)
89 86
      pp_val v2
90
  else
91
    Format.fprintf fmt "(div %a %a)" pp_val v1 pp_val v2
92

  
87
  else Format.fprintf fmt "(div %a %a)" pp_val v1 pp_val v2
93 88

  
94 89
let pp_basic_lib_fun i pp_val fmt vl =
95 90
  match i, vl with
96
  | "ite", [v1; v2; v3] -> Format.fprintf fmt "(@[<hov 2>ite %a@ %a@ %a@])" pp_val v1 pp_val v2 pp_val v3
97
  | "uminus", [v] -> Format.fprintf fmt "(- %a)" pp_val v
98
  | "not", [v] -> Format.fprintf fmt "(not %a)" pp_val v
99
  | "=", [v1; v2] -> Format.fprintf fmt "(= %a %a)" pp_val v1 pp_val v2
100
  | "&&", [v1; v2] -> Format.fprintf fmt "(and %a %a)" pp_val v1 pp_val v2
101
  | "||", [v1; v2] -> Format.fprintf fmt "(or %a %a)" pp_val v1 pp_val v2
102
  | "impl", [v1; v2] -> Format.fprintf fmt "(=> %a %a)" pp_val v1 pp_val v2
103
  | "equi", [v1; v2] -> Format.fprintf fmt "(%a = %a)" pp_val v1 pp_val v2
104
  | "xor", [v1; v2] -> Format.fprintf fmt "(%a xor %a)" pp_val v1 pp_val v2
105
  | "!=", [v1; v2] -> Format.fprintf fmt "(not (= %a %a))" pp_val v1 pp_val v2
106
  | "mod", [v1; v2] -> pp_mod pp_val v1 v2 fmt
107
  | "/", [v1; v2] -> pp_div pp_val v1 v2 fmt
108
  | _, [v1; v2] -> Format.fprintf fmt "(%s %a %a)" i pp_val v1 pp_val v2
109
  | _ -> (Format.eprintf "internal error: Basic_library.pp_horn %s@." i; assert false)
110
(*  | "mod", [v1; v2] -> Format.fprintf fmt "(%a %% %a)" pp_val v1 pp_val v2
111

  
112
*)
113

  
114

  
115
(* Prints a value expression [v], with internal function calls only.
116
   [pp_var] is a printer for variables (typically [pp_c_var_read]),
117
   but an offset suffix may be added for array variables
118
*)
119
let rec pp_horn_val ?(is_lhs=false) m self pp_var fmt v =
120
  match v.value_desc with
121
  | Cst c       -> pp_horn_const fmt c
91
  | "ite", [ v1; v2; v3 ] ->
92
    Format.fprintf fmt "(@[<hov 2>ite %a@ %a@ %a@])" pp_val v1 pp_val v2 pp_val
93
      v3
94
  | "uminus", [ v ] ->
95
    Format.fprintf fmt "(- %a)" pp_val v
96
  | "not", [ v ] ->
97
    Format.fprintf fmt "(not %a)" pp_val v
98
  | "=", [ v1; v2 ] ->
99
    Format.fprintf fmt "(= %a %a)" pp_val v1 pp_val v2
100
  | "&&", [ v1; v2 ] ->
101
    Format.fprintf fmt "(and %a %a)" pp_val v1 pp_val v2
102
  | "||", [ v1; v2 ] ->
103
    Format.fprintf fmt "(or %a %a)" pp_val v1 pp_val v2
104
  | "impl", [ v1; v2 ] ->
105
    Format.fprintf fmt "(=> %a %a)" pp_val v1 pp_val v2
106
  | "equi", [ v1; v2 ] ->
107
    Format.fprintf fmt "(%a = %a)" pp_val v1 pp_val v2
108
  | "xor", [ v1; v2 ] ->
109
    Format.fprintf fmt "(%a xor %a)" pp_val v1 pp_val v2
110
  | "!=", [ v1; v2 ] ->
111
    Format.fprintf fmt "(not (= %a %a))" pp_val v1 pp_val v2
112
  | "mod", [ v1; v2 ] ->
113
    pp_mod pp_val v1 v2 fmt
114
  | "/", [ v1; v2 ] ->
115
    pp_div pp_val v1 v2 fmt
116
  | _, [ v1; v2 ] ->
117
    Format.fprintf fmt "(%s %a %a)" i pp_val v1 pp_val v2
118
  | _ ->
119
    Format.eprintf "internal error: Basic_library.pp_horn %s@." i;
120
    assert false
121
(* | "mod", [v1; v2] -> Format.fprintf fmt "(%a %% %a)" pp_val v1 pp_val v2 *)
122 122

  
123
(* Prints a value expression [v], with internal function calls only. [pp_var] is
124
   a printer for variables (typically [pp_c_var_read]), but an offset suffix may
125
   be added for array variables *)
126
let rec pp_horn_val ?(is_lhs = false) m self pp_var fmt v =
127
  match v.value_desc with
128
  | Cst c ->
129
    pp_horn_const fmt c
123 130
  (* Code specific for arrays *)
124
  | Array il    ->
125
     (* An array definition: 
126
	(store (
127
	  ...
128
 	    (store (
129
	       store (
130
	          default_val
131
	       ) 
132
	       idx_n val_n
133
	    ) 
134
	    idx_n-1 val_n-1)
135
	  ... 
136
	  idx_1 val_1
137
	) *)
138
     let rec print fmt (tab, x) =
139
       match tab with
140
       | [] -> pp_default_val fmt v.value_type(* (get_type v) *)
141
       | h::t ->
142
	  fprintf fmt "(store %a %i %a)"
143
	    print (t, (x+1))
144
	    x
145
	    (pp_horn_val ~is_lhs:is_lhs m self pp_var) h
146
     in
147
     print fmt (il, 0)
148
       
149
  | Access(tab,index) ->
150
     fprintf fmt "(select %a %a)"
151
       (pp_horn_val ~is_lhs:is_lhs m self pp_var) tab
152
       (pp_horn_val ~is_lhs:is_lhs m self pp_var) index
153

  
131
  | Array il ->
132
    (* An array definition: (store ( ... (store ( store ( default_val ) idx_n
133
       val_n ) idx_n-1 val_n-1) ... idx_1 val_1 ) *)
134
    let rec print fmt (tab, x) =
135
      match tab with
136
      | [] ->
137
        pp_default_val fmt v.value_type (* (get_type v) *)
138
      | h :: t ->
139
        fprintf fmt "(store %a %i %a)" print
140
          (t, x + 1)
141
          x
142
          (pp_horn_val ~is_lhs m self pp_var)
143
          h
144
    in
145
    print fmt (il, 0)
146
  | Access (tab, index) ->
147
    fprintf fmt "(select %a %a)"
148
      (pp_horn_val ~is_lhs m self pp_var)
149
      tab
150
      (pp_horn_val ~is_lhs m self pp_var)
151
      index
154 152
  (* Code specific for arrays *)
155
    
156
  | Power _ -> assert false
157
  | Var v    ->
158
     if is_memory m v then
159
       if Types.is_array_type v.var_type
160
       then assert false
161
       else pp_var fmt (rename_machine self ((if is_lhs then rename_next else rename_current) (* self *) v))
162
     else
163
       pp_var fmt (rename_machine self v)
164
    
165
  | Fun (n, vl)   -> fprintf fmt "%a" (pp_basic_lib_fun n (pp_horn_val m self pp_var)) vl
153
  | Power _ ->
154
    assert false
155
  | Var v ->
156
    if is_memory m v then
157
      if Types.is_array_type v.var_type then assert false
158
      else
159
        pp_var fmt
160
          (rename_machine self
161
             ((if is_lhs then rename_next else rename_current (* self *)) v))
162
    else pp_var fmt (rename_machine self v)
163
  | Fun (n, vl) ->
164
    fprintf fmt "%a" (pp_basic_lib_fun n (pp_horn_val m self pp_var)) vl
166 165
  | ResetFlag ->
167 166
    (* TODO: handle reset flag *)
168 167
    assert false
169 168

  
170 169
(* Prints a [value] indexed by the suffix list [loop_vars] *)
171 170
let rec pp_value_suffix m self pp_value fmt value =
172
 match value.value_desc with
173
 | Fun (n, vl)  ->
171
  match value.value_desc with
172
  | Fun (n, vl) ->
174 173
    pp_basic_lib_fun n (pp_value_suffix m self pp_value) fmt vl
175
 |  _            ->
176
   pp_horn_val m self pp_value fmt value
177

  
178
(* type_directed assignment: array vs. statically sized type
179
   - [var_type]: type of variable to be assigned
180
   - [var_name]: name of variable to be assigned
181
   - [value]: assigned value
182
   - [pp_var]: printer for variables
183
*)
174
  | _ ->
175
    pp_horn_val m self pp_value fmt value
176

  
177
(* type_directed assignment: array vs. statically sized type - [var_type]: type
178
   of variable to be assigned - [var_name]: name of variable to be assigned -
179
   [value]: assigned value - [pp_var]: printer for variables *)
184 180
let pp_assign m pp_var fmt var_name value =
185 181
  let self = m.mname.node_id in
186
  fprintf fmt "(= %a %a)" 
187
    (pp_horn_val ~is_lhs:true m self pp_var) var_name
188
    (pp_value_suffix m self pp_var) value
189
    
182
  fprintf fmt "(= %a %a)"
183
    (pp_horn_val ~is_lhs:true m self pp_var)
184
    var_name
185
    (pp_value_suffix m self pp_var)
186
    value
190 187

  
191 188
(* In case of no reset call, we define mid_mem = current_mem *)
192 189
let pp_no_reset machines m fmt i =
193
  let (n,_) = List.assoc i m.minstances in
194
  let target_machine = List.find (fun m  -> m.mname.node_id = (node_name n)) machines in
190
  let n, _ = List.assoc i m.minstances in
191
  let target_machine =
192
    List.find (fun m -> m.mname.node_id = node_name n) machines
193
  in
195 194

  
196
  let m_list = 
197
    rename_machine_list
198
      (concat m.mname.node_id i)
195
  let m_list =
196
    rename_machine_list (concat m.mname.node_id i)
199 197
      (rename_mid_list (full_memory_vars machines target_machine))
200 198
  in
201 199
  let c_list =
202
    rename_machine_list
203
      (concat m.mname.node_id i)
200
    rename_machine_list (concat m.mname.node_id i)
204 201
      (rename_current_list (full_memory_vars machines target_machine))
205 202
  in
206 203
  match c_list, m_list with
207
  | [chd], [mhd] ->
208
    fprintf fmt "(= %a %a)"
209
      (pp_horn_var m) mhd
210
      (pp_horn_var m) chd
211
  
212
  | _ -> (
204
  | [ chd ], [ mhd ] ->
205
    fprintf fmt "(= %a %a)" (pp_horn_var m) mhd (pp_horn_var m) chd
206
  | _ ->
213 207
    fprintf fmt "@[<v 0>(and @[<v 0>";
214
    List.iter2 (fun mhd chd -> 
215
      fprintf fmt "(= %a %a)@ "
216
      (pp_horn_var m) mhd
217
      (pp_horn_var m) chd
218
    )
219
      m_list
220
      c_list      ;
208
    List.iter2
209
      (fun mhd chd ->
210
        fprintf fmt "(= %a %a)@ " (pp_horn_var m) mhd (pp_horn_var m) chd)
211
      m_list c_list;
221 212
    fprintf fmt ")@]@ @]"
222
  )
223 213

  
224 214
let pp_instance_reset machines m fmt i =
225
  let (n,_) = List.assoc i m.minstances in
226
  let target_machine = List.find (fun m  -> m.mname.node_id = (node_name n)) machines in
227
  
228
  fprintf fmt "(%a @[<v 0>%a)@]"
229
    pp_machine_reset_name (node_name n)
230
    (Utils.fprintf_list ~sep:"@ " (pp_horn_var m)) 
231
    (
232
      (rename_machine_list
233
	 (concat m.mname.node_id i)
234
	 (rename_current_list (full_memory_vars machines target_machine))
235
      ) 
236
      @
237
	(rename_machine_list
238
	   (concat m.mname.node_id i)
239
	   (rename_mid_list (full_memory_vars machines target_machine))
240
	)
241
    )
215
  let n, _ = List.assoc i m.minstances in
216
  let target_machine =
217
    List.find (fun m -> m.mname.node_id = node_name n) machines
218
  in
219

  
220
  fprintf fmt "(%a @[<v 0>%a)@]" pp_machine_reset_name (node_name n)
221
    (Utils.fprintf_list ~sep:"@ " (pp_horn_var m))
222
    (rename_machine_list (concat m.mname.node_id i)
223
       (rename_current_list (full_memory_vars machines target_machine))
224
    @ rename_machine_list (concat m.mname.node_id i)
225
        (rename_mid_list (full_memory_vars machines target_machine)))
242 226

  
243 227
let pp_instance_call machines reset_instances m fmt i inputs outputs =
244 228
  let self = m.mname.node_id in
245
  try (* stateful node instance *)
246
    begin
247
      let (n,_) = List.assoc i m.minstances in
248
      let target_machine = List.find (fun m  -> m.mname.node_id = node_name n) machines in
249
      (* Checking whether this specific instances has been reset yet *)
250
      if not (List.mem i reset_instances) then
251
	(* If not, declare mem_m = mem_c *)
252
	pp_no_reset machines m fmt i;
253
      
254
      let mems = full_memory_vars machines target_machine in
255
      let rename_mems f = rename_machine_list (concat m.mname.node_id i) (f mems) in
256
      let mid_mems = rename_mems rename_mid_list in
257
      let next_mems = rename_mems rename_next_list in
258

  
259
      match node_name n, inputs, outputs, mid_mems, next_mems with
260
      | "_arrow", [i1; i2], [o], [mem_m], [mem_x] -> begin
261
	fprintf fmt "@[<v 5>(and ";
262
	fprintf fmt "(= %a (ite %a %a %a))"
263
	  (pp_horn_val ~is_lhs:true m self (pp_horn_var m)) (mk_val (Var o) o.var_type) (* output var *)
264
	  (pp_horn_var m) mem_m 
265
	  (pp_horn_val m self (pp_horn_var m)) i1
266
	  (pp_horn_val m self (pp_horn_var m)) i2
267
	;
268
	fprintf fmt "@ ";
269
	fprintf fmt "(= %a false)" (pp_horn_var m) mem_x;
270
	fprintf fmt ")@]"
271
      end
272

  
273
      | _ -> begin
274
	fprintf fmt "(%a @[<v 0>%a%t%a%t%a)@]"
275
	  pp_machine_step_name (node_name n)
276
	  (Utils.fprintf_list ~sep:"@ " (pp_horn_val m self (pp_horn_var m))) inputs
277
	  (Utils.pp_final_char_if_non_empty "@ " inputs)
278
	  (Utils.fprintf_list ~sep:"@ " (pp_horn_val m self (pp_horn_var m)))
279
	  (List.map (fun v -> mk_val (Var v) v.var_type) outputs)
280
	  (Utils.pp_final_char_if_non_empty "@ " outputs)
281
	  (Utils.fprintf_list ~sep:"@ " (pp_horn_var m)) (mid_mems@next_mems)
282
	
283
      end
284
    end
285
  with Not_found -> ( (* stateless node instance *)
286
    let (n,_) = List.assoc i m.mcalls in
287
    fprintf fmt "(%a @[<v 0>%a%t%a)@]"
288
      pp_machine_stateless_name (node_name n)
229
  try
230
    (* stateful node instance *)
231
    let n, _ = List.assoc i m.minstances in
232
    let target_machine =
233
      List.find (fun m -> m.mname.node_id = node_name n) machines
234
    in
235
    (* Checking whether this specific instances has been reset yet *)
236
    if not (List.mem i reset_instances) then
237
      (* If not, declare mem_m = mem_c *)
238
      pp_no_reset machines m fmt i;
239

  
240
    let mems = full_memory_vars machines target_machine in
241
    let rename_mems f =
242
      rename_machine_list (concat m.mname.node_id i) (f mems)
243
    in
244
    let mid_mems = rename_mems rename_mid_list in
245
    let next_mems = rename_mems rename_next_list in
246

  
247
    match node_name n, inputs, outputs, mid_mems, next_mems with
248
    | "_arrow", [ i1; i2 ], [ o ], [ mem_m ], [ mem_x ] ->
249
      fprintf fmt "@[<v 5>(and ";
250
      fprintf fmt "(= %a (ite %a %a %a))"
251
        (pp_horn_val ~is_lhs:true m self (pp_horn_var m))
252
        (mk_val (Var o) o.var_type)
253
        (* output var *)
254
        (pp_horn_var m)
255
        mem_m
256
        (pp_horn_val m self (pp_horn_var m))
257
        i1
258
        (pp_horn_val m self (pp_horn_var m))
259
        i2;
260
      fprintf fmt "@ ";
261
      fprintf fmt "(= %a false)" (pp_horn_var m) mem_x;
262
      fprintf fmt ")@]"
263
    | _ ->
264
      fprintf fmt "(%a @[<v 0>%a%t%a%t%a)@]" pp_machine_step_name (node_name n)
265
        (Utils.fprintf_list ~sep:"@ " (pp_horn_val m self (pp_horn_var m)))
266
        inputs
267
        (Utils.pp_final_char_if_non_empty "@ " inputs)
268
        (Utils.fprintf_list ~sep:"@ " (pp_horn_val m self (pp_horn_var m)))
269
        (List.map (fun v -> mk_val (Var v) v.var_type) outputs)
270
        (Utils.pp_final_char_if_non_empty "@ " outputs)
271
        (Utils.fprintf_list ~sep:"@ " (pp_horn_var m))
272
        (mid_mems @ next_mems)
273
  with Not_found ->
274
    (* stateless node instance *)
275
    let n, _ = List.assoc i m.mcalls in
276
    fprintf fmt "(%a @[<v 0>%a%t%a)@]" pp_machine_stateless_name (node_name n)
289 277
      (Utils.fprintf_list ~sep:"@ " (pp_horn_val m self (pp_horn_var m)))
290 278
      inputs
291 279
      (Utils.pp_final_char_if_non_empty "@ " inputs)
292 280
      (Utils.fprintf_list ~sep:"@ " (pp_horn_val m self (pp_horn_var m)))
293 281
      (List.map (fun v -> mk_val (Var v) v.var_type) outputs)
294
  )
295
    
296
    
282

  
297 283
(* Print the instruction and update the set of reset instances *)
298
let rec pp_machine_instr machines reset_instances (m: machine_t) fmt instr : ident list =
284
let rec pp_machine_instr machines reset_instances (m : machine_t) fmt instr :
285
    ident list =
299 286
  match get_instr_desc instr with
300
  | MSpec _ | MComment _ -> reset_instances
287
  | MSpec _ | MComment _ ->
288
    reset_instances
301 289
  (* TODO: handle reset flag *)
302
  | MResetAssign _ -> reset_instances
290
  | MResetAssign _ ->
291
    reset_instances
303 292
  (* TODO: handle clear_reset *)
304
  | MClearReset -> reset_instances
305
  | MNoReset i -> (* we assign middle_mem with mem_m. And declare i as reset *)
293
  | MClearReset ->
294
    reset_instances
295
  | MNoReset i ->
296
    (* we assign middle_mem with mem_m. And declare i as reset *)
306 297
    pp_no_reset machines m fmt i;
307
    i::reset_instances
308
  | MSetReset i -> (* we assign middle_mem with reset: reset(mem_m) *)
298
    i :: reset_instances
299
  | MSetReset i ->
300
    (* we assign middle_mem with reset: reset(mem_m) *)
309 301
    pp_instance_reset machines m fmt i;
310
    i::reset_instances
311
  | MLocalAssign (i,v) ->
312
    pp_assign
313
      m (pp_horn_var m) fmt
314
      (mk_val (Var i) i.var_type) v;
302
    i :: reset_instances
303
  | MLocalAssign (i, v) ->
304
    pp_assign m (pp_horn_var m) fmt (mk_val (Var i) i.var_type) v;
315 305
    reset_instances
316
  | MStateAssign (i,v) ->
317
    pp_assign
318
      m (pp_horn_var m) fmt
319
      (mk_val (Var i) i.var_type) v;
306
  | MStateAssign (i, v) ->
307
    pp_assign m (pp_horn_var m) fmt (mk_val (Var i) i.var_type) v;
320 308
    reset_instances
321
  | MStep ([_], i, vl) when Basic_library.is_internal_fun i (List.map (fun v -> v.value_type) vl) ->
309
  | MStep ([ _ ], i, vl)
310
    when Basic_library.is_internal_fun i (List.map (fun v -> v.value_type) vl)
311
    ->
322 312
    assert false (* This should not happen anymore *)
323 313
  | MStep (il, i, vl) ->
324
    (* if reset instance, just print the call over mem_m , otherwise declare mem_m =
325
       mem_c and print the call to mem_m *)
314
    (* if reset instance, just print the call over mem_m , otherwise declare
315
       mem_m = mem_c and print the call to mem_m *)
326 316
    pp_instance_call machines reset_instances m fmt i vl il;
327
    reset_instances (* Since this instance call will only happen once, we
328
		       don't have to update reset_instances *)
329

  
330
  | MBranch (g,hl) -> (* (g = tag1 => expr1) and (g = tag2 => expr2) ...
331
			 should not be produced yet. Later, we will have to
332
			 compare the reset_instances of each branch and
333
			 introduced the mem_m = mem_c for branches to do not
334
			 address it while other did. Am I clear ? *)
317
    reset_instances
318
  (* Since this instance call will only happen once, we don't have to update
319
     reset_instances *)
320
  | MBranch (g, hl) ->
321
    (* (g = tag1 => expr1) and (g = tag2 => expr2) ... should not be produced
322
       yet. Later, we will have to compare the reset_instances of each branch
323
       and introduced the mem_m = mem_c for branches to do not address it while
324
       other did. Am I clear ? *)
335 325
    (* For each branch we obtain the logical encoding, and the information
336 326
       whether a sub node has been reset or not. If a node has been reset in one
337
       of the branch, then all others have to have the mem_m = mem_c
338
       statement. *)
327
       of the branch, then all others have to have the mem_m = mem_c statement. *)
339 328
    let self = m.mname.node_id in
340 329
    let pp_branch fmt (tag, instrs) =
341
      fprintf fmt 
342
	"@[<v 3>(or (not (= %a %a))@ " 
343
	(*"@[<v 3>(=> (= %a %s)@ "*)  (* Issues with some versions of Z3. It
344
					  seems that => within Horn predicate
345
					  may cause trouble. I have hard time
346
					  producing a MWE, so I'll just keep the
347
					  fix here as (not a) or b *)
348
	(pp_horn_val m self (pp_horn_var m)) g
349
	pp_horn_tag tag;
350
      let _ (* rs *) = pp_machine_instrs machines reset_instances m fmt instrs in 
330
      fprintf fmt "@[<v 3>(or (not (= %a %a))@ "
331
        (*"@[<v 3>(=> (= %a %s)@ "*)
332
        (* Issues with some versions of Z3. It seems that => within Horn
333
           predicate may cause trouble. I have hard time producing a MWE, so
334
           I'll just keep the fix here as (not a) or b *)
335
        (pp_horn_val m self (pp_horn_var m))
336
        g pp_horn_tag tag;
337
      let _ (* rs *) =
338
        pp_machine_instrs machines reset_instances m fmt instrs
339
      in
351 340
      fprintf fmt "@])";
352
      () (* rs *)
341
      ()
342
      (* rs *)
353 343
    in
354 344
    pp_conj pp_branch fmt hl;
355
    reset_instances 
345
    reset_instances
356 346

  
357
and pp_machine_instrs machines reset_instances m fmt instrs = 
347
and pp_machine_instrs machines reset_instances m fmt instrs =
358 348
  let ppi rs fmt i = pp_machine_instr machines rs m fmt i in
359 349
  match instrs with
360
  | [x] -> ppi reset_instances fmt x 
361
  | _::_ ->
350
  | [ x ] ->
351
    ppi reset_instances fmt x
352
  | _ :: _ ->
362 353
    fprintf fmt "(and @[<v 0>";
363
    let rs = List.fold_left (fun rs i -> 
364
      let rs = ppi rs fmt i in
365
      fprintf fmt "@ ";
366
      rs
367
    )
368
      reset_instances instrs 
354
    let rs =
355
      List.fold_left
356
        (fun rs i ->
357
          let rs = ppi rs fmt i in
358
          fprintf fmt "@ ";
359
          rs)
360
        reset_instances instrs
369 361
    in
370 362
    fprintf fmt "@])";
371 363
    rs
372

  
373
  | [] -> fprintf fmt "true"; reset_instances
364
  | [] ->
365
    fprintf fmt "true";
366
    reset_instances
374 367

  
375 368
let pp_machine_reset machines fmt m =
376 369
  let locals = local_memory_vars m in
377 370
  fprintf fmt "@[<v 5>(and @ ";
378 371

  
379 372
  (* print "x_m = x_c" for each local memory *)
380
  (Utils.fprintf_list ~sep:"@ " (fun fmt v -> 
381
    fprintf fmt "(= %a %a)"
382
      (pp_horn_var m) (rename_mid v)
383
      (pp_horn_var m) (rename_current v)
384
   )) fmt locals;
373
  (Utils.fprintf_list ~sep:"@ " (fun fmt v ->
374
       fprintf fmt "(= %a %a)" (pp_horn_var m) (rename_mid v) (pp_horn_var m)
375
         (rename_current v)))
376
    fmt locals;
385 377
  fprintf fmt "@ ";
386 378

  
387
  (* print "child_reset ( associated vars _ {c,m} )" for each subnode.
388
     Special treatment for _arrow: _first = true
389
  *)
379
  (* print "child_reset ( associated vars _ {c,m} )" for each subnode. Special
380
     treatment for _arrow: _first = true *)
390 381
  (Utils.fprintf_list ~sep:"@ " (fun fmt (id, (n, _)) ->
391
    let name = node_name n in
392
    if name = "_arrow" then ( 
393
      fprintf fmt "(= %s._arrow._first_m true)"
394
	(concat m.mname.node_id id)  
395
    ) else (
396
      let machine_n = get_machine machines name in 
397
      fprintf fmt "(%s_reset @[<hov 0>%a@])" 
398
	name
399
	(Utils.fprintf_list ~sep:"@ " (pp_horn_var m)) 
400
	(rename_machine_list (concat m.mname.node_id id) (reset_vars machines machine_n))
401
    )
402
   )) fmt m.minstances;
382
       let name = node_name n in
383
       if name = "_arrow" then
384
         fprintf fmt "(= %s._arrow._first_m true)" (concat m.mname.node_id id)
385
       else
386
         let machine_n = get_machine machines name in
387
         fprintf fmt "(%s_reset @[<hov 0>%a@])" name
388
           (Utils.fprintf_list ~sep:"@ " (pp_horn_var m))
389
           (rename_machine_list
390
              (concat m.mname.node_id id)
391
              (reset_vars machines machine_n))))
392
    fmt m.minstances;
403 393

  
404 394
  fprintf fmt "@]@ )"
405 395

  
406

  
407

  
408 396
(**************************************************************)
409 397

  
410

  
411
(* Print the machine m:
412
   two functions: m_init and m_step
413
   - m_init is a predicate over m memories
414
   - m_step is a predicate over old_memories, inputs, new_memories, outputs
415
   We first declare all variables then the two /rules/.
416
*)
398
(* Print the machine m: two functions: m_init and m_step - m_init is a predicate
399
   over m memories - m_step is a predicate over old_memories, inputs,
400
   new_memories, outputs We first declare all variables then the two /rules/. *)
417 401
let print_machine machines fmt m =
418
  if m.mname.node_id = Arrow.arrow_id then
419
    (* We don't print arrow function *)
402
  if m.mname.node_id = Arrow.arrow_id then (* We don't print arrow function *)
420 403
    ()
421
  else
422
    begin
423
      fprintf fmt "; %s@." m.mname.node_id;
424
      
425
      (* Printing variables *)
426
      Utils.fprintf_list ~sep:"@." pp_decl_var fmt
427
	(
428
	  (inout_vars m)@
429
	    (rename_current_list (full_memory_vars machines m)) @
430
	    (rename_mid_list (full_memory_vars machines m)) @
431
	    (rename_next_list (full_memory_vars machines m)) @
432
	    (rename_machine_list m.mname.node_id m.mstep.step_locals)
433
	);
434
      pp_print_newline fmt ();
404
  else (
405
    fprintf fmt "; %s@." m.mname.node_id;
406

  
407
    (* Printing variables *)
408
    Utils.fprintf_list ~sep:"@." pp_decl_var fmt
409
      (inout_vars m
410
      @ rename_current_list (full_memory_vars machines m)
411
      @ rename_mid_list (full_memory_vars machines m)
412
      @ rename_next_list (full_memory_vars machines m)
413
      @ rename_machine_list m.mname.node_id m.mstep.step_locals);
414
    pp_print_newline fmt ();
415

  
416
    if is_stateless m then (
417
      (* Declaring single predicate *)
418
      fprintf fmt "(declare-rel %a (%a))@." pp_machine_stateless_name
419
        m.mname.node_id
420
        (Utils.fprintf_list ~sep:" " pp_type)
421
        (List.map (fun v -> v.var_type) (inout_vars m));
422

  
423
      match m.mstep.step_asserts with
424
      | [] ->
425
        (* Rule for single predicate *)
426
        fprintf fmt "; Stateless step rule @.";
427
        fprintf fmt "@[<v 2>(rule (=> @ ";
428
        ignore
429
          (pp_machine_instrs machines []
430
             (* No reset info for stateless nodes *) m fmt m.mstep.step_instrs);
431
        fprintf fmt "@ (%a @[<v 0>%a)@]@]@.))@.@." pp_machine_stateless_name
432
          m.mname.node_id
433
          (Utils.fprintf_list ~sep:" " (pp_horn_var m))
434
          (inout_vars m)
435
      | assertsl ->
436
        let pp_val =
437
          pp_horn_val ~is_lhs:true m m.mname.node_id (pp_horn_var m)
438
        in
439

  
440
        fprintf fmt "; Stateless step rule with Assertions @.";
441
        (*Rule for step*)
442
        fprintf fmt "@[<v 2>(rule (=> @ (and @ ";
443
        ignore (pp_machine_instrs machines [] m fmt m.mstep.step_instrs);
444
        fprintf fmt "@. %a)@ (%a @[<v 0>%a)@]@]@.))@.@." (pp_conj pp_val)
445
          assertsl pp_machine_stateless_name m.mname.node_id
446
          (Utils.fprintf_list ~sep:" " (pp_horn_var m))
447
          (step_vars machines m))
448
    else (
449
      (* Declaring predicate *)
450
      fprintf fmt "(declare-rel %a (%a))@." pp_machine_reset_name
451
        m.mname.node_id
452
        (Utils.fprintf_list ~sep:" " pp_type)
453
        (List.map (fun v -> v.var_type) (reset_vars machines m));
454

  
455
      fprintf fmt "(declare-rel %a (%a))@." pp_machine_step_name m.mname.node_id
456
        (Utils.fprintf_list ~sep:" " pp_type)
457
        (List.map (fun v -> v.var_type) (step_vars machines m));
435 458

  
436
      if is_stateless m then
437
	begin
438
	  (* Declaring single predicate *)
439
	  fprintf fmt "(declare-rel %a (%a))@."
440
	    pp_machine_stateless_name m.mname.node_id
441
	    (Utils.fprintf_list ~sep:" " pp_type)
442
	    (List.map (fun v -> v.var_type) (inout_vars m));
443

  
444
          match m.mstep.step_asserts with
445
	  | [] ->
446
	     begin
447

  
448
	       (* Rule for single predicate *)
449
	       fprintf fmt "; Stateless step rule @.";
450
	       fprintf fmt "@[<v 2>(rule (=> @ ";
451
	       ignore (pp_machine_instrs machines ([] (* No reset info for stateless nodes *) )  m fmt m.mstep.step_instrs);
452
	       fprintf fmt "@ (%a @[<v 0>%a)@]@]@.))@.@."
453
		 pp_machine_stateless_name m.mname.node_id
454
		 (Utils.fprintf_list ~sep:" " (pp_horn_var m)) (inout_vars m);
455
	     end
456
	  | assertsl ->
457
	     begin
458
	       let pp_val = pp_horn_val ~is_lhs:true m m.mname.node_id (pp_horn_var m) in
459
	       
460
	       fprintf fmt "; Stateless step rule with Assertions @.";
461
	       (*Rule for step*)
462
	       fprintf fmt "@[<v 2>(rule (=> @ (and @ ";
463
	       ignore (pp_machine_instrs machines [] m fmt m.mstep.step_instrs);
464
	       fprintf fmt "@. %a)@ (%a @[<v 0>%a)@]@]@.))@.@." (pp_conj pp_val) assertsl
465
		 pp_machine_stateless_name m.mname.node_id
466
		 (Utils.fprintf_list ~sep:" " (pp_horn_var m)) (step_vars machines m);
467
	  
468
	     end
469
	       
470
	end
471
      else
472
	begin
473
	  (* Declaring predicate *)
474
	  fprintf fmt "(declare-rel %a (%a))@."
475
	    pp_machine_reset_name m.mname.node_id
476
	    (Utils.fprintf_list ~sep:" " pp_type)
477
	    (List.map (fun v -> v.var_type) (reset_vars machines m));
478

  
479
	  fprintf fmt "(declare-rel %a (%a))@."
480
	    pp_machine_step_name m.mname.node_id
481
	    (Utils.fprintf_list ~sep:" " pp_type)
482
	    (List.map (fun v -> v.var_type) (step_vars machines m));
483

  
484
	  pp_print_newline fmt ();
485

  
486
	  (* Rule for reset *)
487
	  fprintf fmt "@[<v 2>(rule (=> @ %a@ (%a @[<v 0>%a)@]@]@.))@.@."
488
	    (pp_machine_reset machines) m 
489
	    pp_machine_reset_name m.mname.node_id
490
	    (Utils.fprintf_list ~sep:"@ " (pp_horn_var m)) (reset_vars machines m);
491

  
492
          match m.mstep.step_asserts with
493
	  | [] ->
494
	     begin
495
	       fprintf fmt "; Step rule @.";
496
	       (* Rule for step*)
497
	       fprintf fmt "@[<v 2>(rule (=> @ ";
498
	       ignore (pp_machine_instrs machines [] m fmt m.mstep.step_instrs);
499
	       fprintf fmt "@ (%a @[<v 0>%a)@]@]@.))@.@."
500
		 pp_machine_step_name m.mname.node_id
501
		 (Utils.fprintf_list ~sep:"@ " (pp_horn_var m)) (step_vars machines m);
502
	     end
503
	  | assertsl -> 
504
	     begin
505
	       let pp_val = pp_horn_val ~is_lhs:true m m.mname.node_id (pp_horn_var m) in
506
	       (* print_string pp_val; *)
507
	       fprintf fmt "; Step rule with Assertions @.";
508
	       
509
	       (*Rule for step*)
510
	       fprintf fmt "@[<v 2>(rule (=> @ (and @ ";
511
	       ignore (pp_machine_instrs machines [] m fmt m.mstep.step_instrs);
512
	       fprintf fmt "@. %a)@ (%a @[<v 0>%a)@]@]@.))@.@." (pp_conj pp_val) assertsl
513
		 pp_machine_step_name m.mname.node_id
514
		 (Utils.fprintf_list ~sep:" " (pp_horn_var m)) (step_vars machines m);
515
	     end
516
	       
517
	       
518
	end
519
    end
459
      pp_print_newline fmt ();
520 460

  
461
      (* Rule for reset *)
462
      fprintf fmt "@[<v 2>(rule (=> @ %a@ (%a @[<v 0>%a)@]@]@.))@.@."
463
        (pp_machine_reset machines)
464
        m pp_machine_reset_name m.mname.node_id
465
        (Utils.fprintf_list ~sep:"@ " (pp_horn_var m))
466
        (reset_vars machines m);
467

  
468
      match m.mstep.step_asserts with
469
      | [] ->
470
        fprintf fmt "; Step rule @.";
471
        (* Rule for step*)
472
        fprintf fmt "@[<v 2>(rule (=> @ ";
473
        ignore (pp_machine_instrs machines [] m fmt m.mstep.step_instrs);
474
        fprintf fmt "@ (%a @[<v 0>%a)@]@]@.))@.@." pp_machine_step_name
475
          m.mname.node_id
476
          (Utils.fprintf_list ~sep:"@ " (pp_horn_var m))
477
          (step_vars machines m)
478
      | assertsl ->
479
        let pp_val =
480
          pp_horn_val ~is_lhs:true m m.mname.node_id (pp_horn_var m)
481
        in
482
        (* print_string pp_val; *)
483
        fprintf fmt "; Step rule with Assertions @.";
484

  
485
        (*Rule for step*)
486
        fprintf fmt "@[<v 2>(rule (=> @ (and @ ";
487
        ignore (pp_machine_instrs machines [] m fmt m.mstep.step_instrs);
488
        fprintf fmt "@. %a)@ (%a @[<v 0>%a)@]@]@.))@.@." (pp_conj pp_val)
489
          assertsl pp_machine_step_name m.mname.node_id
490
          (Utils.fprintf_list ~sep:" " (pp_horn_var m))
491
          (step_vars machines m)))
521 492

  
522 493
let mk_flags arity =
523 494
  let b_range =
524
   let rec range i j =
525
     if i > arity then [] else i :: (range (i+1) j) in
526
   range 2 arity;
527
 in
528
 List.fold_left (fun acc _ -> acc ^ " false") "true" b_range
529

  
495
    let rec range i j = if i > arity then [] else i :: range (i + 1) j in
496
    range 2 arity
497
  in
498
  List.fold_left (fun acc _ -> acc ^ " false") "true" b_range
530 499

  
531
  (*Get sfunction infos from command line*)
532
let get_sf_info() =
500
(*Get sfunction infos from command line*)
501
let get_sf_info () =
533 502
  let splitted = Str.split (Str.regexp "@") !Options.sfunction in
534
  Log.report ~level:1 (fun fmt -> fprintf fmt ".. sfunction name: %s@," !Options.sfunction);
535
  let sf_name, flags, arity = match splitted with
536
      [h;flg;par] -> h, flg, par
537
    | _ -> failwith "Wrong Sfunction info"
538

  
503
  Log.report ~level:1 (fun fmt ->
504
      fprintf fmt ".. sfunction name: %s@," !Options.sfunction);
505
  let sf_name, flags, arity =
506
    match splitted with
507
    | [ h; flg; par ] ->
508
      h, flg, par
509
    | _ ->
510
      failwith "Wrong Sfunction info"
539 511
  in
540
  Log.report ~level:1 (fun fmt -> fprintf fmt "... sf_name: %s@, .. flags: %s@ .. arity: %s@," sf_name flags arity);
541
  sf_name, flags, arity
542

  
543 512

  
544
    (*a function to print the rules in case we have an s-function*)
545
  let print_sfunction machines fmt m =
546
      if m.mname.node_id = Arrow.arrow_id then
547
        (* We don't print arrow function *)
548
        ()
549
      else
550
        begin
551
          Format.fprintf fmt "; SFUNCTION@.";
552
          Format.fprintf fmt "; %s@." m.mname.node_id;
553
          Format.fprintf fmt "; EndPoint Predicate %s." !Options.sfunction;
554

  
555
          (* Check if there is annotation for s-function *)
556
          if m.mannot != [] then(
557
              Format.fprintf fmt "; @[%a@]@]@\n" (Utils.fprintf_list ~sep:"@ " Printers.pp_s_function) m.mannot;
558
            );
559

  
560
       (* Printing variables *)
561
          Utils.fprintf_list ~sep:"@." pp_decl_var fmt
562
                             ((step_vars machines m)@
563
    	                        (rename_machine_list m.mname.node_id m.mstep.step_locals));
564
          Format.pp_print_newline fmt ();
565
          let sf_name, flags, _ = get_sf_info() in
566

  
567
       if is_stateless m then
568
         begin
569
           (* Declaring single predicate *)
570
           Format.fprintf fmt "(declare-rel %a (%a))@."
571
    	                  pp_machine_stateless_name m.mname.node_id
572
    	                  (Utils.fprintf_list ~sep:" " pp_type)
573
    	                  (List.map (fun v -> v.var_type) (reset_vars machines m));
574
           Format.pp_print_newline fmt ();
575
           (* Rule for single predicate *)
576
           let str_flags = sf_name ^ " " ^ mk_flags (int_of_string flags) in
577
           Format.fprintf fmt "@[<v 2>(rule (=> @ (%s %a) (%a %a)@]@.))@.@."
578
                          str_flags
579
                          (Utils.fprintf_list ~sep:" " (pp_horn_var m)) (reset_vars machines m)
580
	                  pp_machine_stateless_name m.mname.node_id
581
	                  (Utils.fprintf_list ~sep:" " (pp_horn_var m)) (reset_vars machines m);
582
         end
583
      else
584
         begin
585
           (* Declaring predicate *)
586
           Format.fprintf fmt "(declare-rel %a (%a))@."
587
    	                  pp_machine_reset_name m.mname.node_id
588
    	                  (Utils.fprintf_list ~sep:" " pp_type)
589
    	                  (List.map (fun v -> v.var_type) (inout_vars m));
590

  
591
           Format.fprintf fmt "(declare-rel %a (%a))@."
592
    	                  pp_machine_step_name m.mname.node_id
593
    	                  (Utils.fprintf_list ~sep:" " pp_type)
594
    	                  (List.map (fun v -> v.var_type) (step_vars machines m));
595

  
596
           Format.pp_print_newline fmt ();
597
          (* Adding assertions *)
598
           match m.mstep.step_asserts with
599
	  | [] ->
600
	    begin
601

  
602
	      (* Rule for step*)
603
	      fprintf fmt "@[<v 2>(rule (=> @ ";
604
	      ignore (pp_machine_instrs machines [] m fmt m.mstep.step_instrs);
605
	      fprintf fmt "@ (%a @[<v 0>%a)@]@]@.))@.@."
606
		pp_machine_step_name m.mname.node_id
607
		(Utils.fprintf_list ~sep:"@ " (pp_horn_var m)) (step_vars machines m);
608
	    end
609
	  | assertsl ->
610
	    begin
611
	      let pp_val = pp_horn_val ~is_lhs:true m m.mname.node_id (pp_horn_var m) in
612
	      (* print_string pp_val; *)
613
	      fprintf fmt "; with Assertions @.";
614

  
615
	      (*Rule for step*)
616
	      fprintf fmt "@[<v 2>(rule (=> @ (and @ ";
617
	      ignore (pp_machine_instrs machines [] m fmt m.mstep.step_instrs);
618
	      fprintf fmt "@. %a)(%a @[<v 0>%a)@]@]@.))@.@." (pp_conj pp_val) assertsl
619
		pp_machine_step_name m.mname.node_id
620
		(Utils.fprintf_list ~sep:" " (pp_horn_var m)) (step_vars machines m);
621
	    end
622

  
623
         end
624

  
625
        end
513
  Log.report ~level:1 (fun fmt ->
514
      fprintf fmt "... sf_name: %s@, .. flags: %s@ .. arity: %s@," sf_name flags
515
        arity);
516
  sf_name, flags, arity
626 517

  
518
(*a function to print the rules in case we have an s-function*)
519
let print_sfunction machines fmt m =
520
  if m.mname.node_id = Arrow.arrow_id then (* We don't print arrow function *)
521
    ()
522
  else (
523
    Format.fprintf fmt "; SFUNCTION@.";
524
    Format.fprintf fmt "; %s@." m.mname.node_id;
525
    Format.fprintf fmt "; EndPoint Predicate %s." !Options.sfunction;
526

  
527
    (* Check if there is annotation for s-function *)
528
    if m.mannot != [] then
529
      Format.fprintf fmt "; @[%a@]@]@\n"
530
        (Utils.fprintf_list ~sep:"@ " Printers.pp_s_function)
531
        m.mannot;
532

  
533
    (* Printing variables *)
534
    Utils.fprintf_list ~sep:"@." pp_decl_var fmt
535
      (step_vars machines m
536
      @ rename_machine_list m.mname.node_id m.mstep.step_locals);
537
    Format.pp_print_newline fmt ();
538
    let sf_name, flags, _ = get_sf_info () in
539

  
540
    if is_stateless m then (
541
      (* Declaring single predicate *)
542
      Format.fprintf fmt "(declare-rel %a (%a))@." pp_machine_stateless_name
543
        m.mname.node_id
544
        (Utils.fprintf_list ~sep:" " pp_type)
545
        (List.map (fun v -> v.var_type) (reset_vars machines m));
546
      Format.pp_print_newline fmt ();
547
      (* Rule for single predicate *)
548
      let str_flags = sf_name ^ " " ^ mk_flags (int_of_string flags) in
549
      Format.fprintf fmt "@[<v 2>(rule (=> @ (%s %a) (%a %a)@]@.))@.@."
550
        str_flags
551
        (Utils.fprintf_list ~sep:" " (pp_horn_var m))
552
        (reset_vars machines m) pp_machine_stateless_name m.mname.node_id
553
        (Utils.fprintf_list ~sep:" " (pp_horn_var m))
554
        (reset_vars machines m))
555
    else (
556
      (* Declaring predicate *)
557
      Format.fprintf fmt "(declare-rel %a (%a))@." pp_machine_reset_name
558
        m.mname.node_id
559
        (Utils.fprintf_list ~sep:" " pp_type)
560
        (List.map (fun v -> v.var_type) (inout_vars m));
561

  
562
      Format.fprintf fmt "(declare-rel %a (%a))@." pp_machine_step_name
563
        m.mname.node_id
564
        (Utils.fprintf_list ~sep:" " pp_type)
565
        (List.map (fun v -> v.var_type) (step_vars machines m));
566

  
567
      Format.pp_print_newline fmt ();
568
      (* Adding assertions *)
569
      match m.mstep.step_asserts with
570
      | [] ->
571
        (* Rule for step*)
572
        fprintf fmt "@[<v 2>(rule (=> @ ";
573
        ignore (pp_machine_instrs machines [] m fmt m.mstep.step_instrs);
574
        fprintf fmt "@ (%a @[<v 0>%a)@]@]@.))@.@." pp_machine_step_name
575
          m.mname.node_id
576
          (Utils.fprintf_list ~sep:"@ " (pp_horn_var m))
577
          (step_vars machines m)
578
      | assertsl ->
579
        let pp_val =
580
          pp_horn_val ~is_lhs:true m m.mname.node_id (pp_horn_var m)
581
        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))
591
          (step_vars machines m)))
627 592

  
628 593
(**************** XML printing functions *************)
629 594

  
630
	  let rec pp_xml_expr fmt expr =
631
  (match expr.expr_annot with 
632
  | None -> fprintf fmt "%t" 
633
  | Some ann -> fprintf fmt "@[(%a %t)@]" pp_xml_expr_annot ann)
634
    (fun fmt -> 
595
let rec pp_xml_expr fmt expr =
596
  (match expr.expr_annot with
597
  | None ->
598
    fprintf fmt "%t"
599
  | Some ann ->
600
    fprintf fmt "@[(%a %t)@]" pp_xml_expr_annot ann) (fun fmt ->
635 601
      match expr.expr_desc with
636
    | Expr_const c -> Printers.pp_const fmt c
637
    | Expr_ident id -> fprintf fmt "%s" id
638
    | Expr_array a -> fprintf fmt "[%a]" pp_xml_tuple a
639
    | Expr_access (a, d) -> fprintf fmt "%a[%a]" pp_xml_expr a Dimension.pp_dimension d
640
    | Expr_power (a, d) -> fprintf fmt "(%a^%a)" pp_xml_expr a Dimension.pp_dimension d
641
    | Expr_tuple el -> fprintf fmt "(%a)" pp_xml_tuple el
642
    | Expr_ite (c, t, e) -> fprintf fmt "@[<hov 1>(if %a then@ @[<hov 2>%a@]@ else@ @[<hov 2>%a@]@])" pp_xml_expr c pp_xml_expr t pp_xml_expr e
643
    | Expr_arrow (e1, e2) -> fprintf fmt "(%a -> %a)" pp_xml_expr e1 pp_xml_expr e2
644
    | Expr_fby (e1, e2) -> fprintf fmt "%a fby %a" pp_xml_expr e1 pp_xml_expr e2
645
    | Expr_pre e -> fprintf fmt "pre %a" pp_xml_expr e
646
    | Expr_when (e, id, l) -> fprintf fmt "%a when %s(%s)" pp_xml_expr e l id
647
    | Expr_merge (id, hl) -> 
648
      fprintf fmt "merge %s %a" id pp_xml_handlers hl
649
    | Expr_appl (id, e, r) -> pp_xml_app fmt id e r
650
    )
651
and pp_xml_tuple fmt el =
652
 Utils.fprintf_list ~sep:"," pp_xml_expr fmt el
653

  
654
and pp_xml_handler fmt (t, h) =
655
 fprintf fmt "(%s -> %a)" t pp_xml_expr h
656

  
657
and pp_xml_handlers fmt hl =
658
 Utils.fprintf_list ~sep:" " pp_xml_handler fmt hl
602
      | Expr_const c ->
603
        Printers.pp_const fmt c
604
      | Expr_ident id ->
605
        fprintf fmt "%s" id
606
      | Expr_array a ->
607
        fprintf fmt "[%a]" pp_xml_tuple a
608
      | Expr_access (a, d) ->
609
        fprintf fmt "%a[%a]" pp_xml_expr a Dimension.pp_dimension d
610
      | Expr_power (a, d) ->
611
        fprintf fmt "(%a^%a)" pp_xml_expr a Dimension.pp_dimension d
612
      | Expr_tuple el ->
613
        fprintf fmt "(%a)" pp_xml_tuple el
614
      | Expr_ite (c, t, e) ->
615
        fprintf fmt
616
          "@[<hov 1>(if %a then@ @[<hov 2>%a@]@ else@ @[<hov 2>%a@]@])"
617
          pp_xml_expr c pp_xml_expr t pp_xml_expr e
618
      | Expr_arrow (e1, e2) ->
619
        fprintf fmt "(%a -> %a)" pp_xml_expr e1 pp_xml_expr e2
620
      | Expr_fby (e1, e2) ->
621
        fprintf fmt "%a fby %a" pp_xml_expr e1 pp_xml_expr e2
622
      | Expr_pre e ->
623
        fprintf fmt "pre %a" pp_xml_expr e
624
      | Expr_when (e, id, l) ->
625
        fprintf fmt "%a when %s(%s)" pp_xml_expr e l id
626
      | Expr_merge (id, hl) ->
627
        fprintf fmt "merge %s %a" id pp_xml_handlers hl
628
      | Expr_appl (id, e, r) ->
629
        pp_xml_app fmt id e r)
630

  
631
and pp_xml_tuple fmt el = Utils.fprintf_list ~sep:"," pp_xml_expr fmt el
632

  
633
and pp_xml_handler fmt (t, h) = fprintf fmt "(%s -> %a)" t pp_xml_expr h
634

  
635
and pp_xml_handlers fmt hl = Utils.fprintf_list ~sep:" " pp_xml_handler fmt hl
659 636

  
660 637
and pp_xml_app fmt id e r =
661 638
  match r with
662
  | None -> pp_xml_call fmt id e
663
  | Some c -> fprintf fmt "%t every (%a)" (fun fmt -> pp_xml_call fmt id e) pp_xml_expr c 
639
  | None ->
640
    pp_xml_call fmt id e
641
  | Some c ->
642
    fprintf fmt "%t every (%a)" (fun fmt -> pp_xml_call fmt id e) pp_xml_expr c
664 643

  
665 644
and pp_xml_call fmt id e =
666 645
  match id, e.expr_desc with
667
  | "+", Expr_tuple([e1;e2]) -> fprintf fmt "(%a + %a)" pp_xml_expr e1 pp_xml_expr e2
668
  | "uminus", _ -> fprintf fmt "(- %a)" pp_xml_expr e
669
  | "-", Expr_tuple([e1;e2]) -> fprintf fmt "(%a - %a)" pp_xml_expr e1 pp_xml_expr e2
670
  | "*", Expr_tuple([e1;e2]) -> fprintf fmt "(%a * %a)" pp_xml_expr e1 pp_xml_expr e2
671
  | "/", Expr_tuple([e1;e2]) -> fprintf fmt "(%a / %a)" pp_xml_expr e1 pp_xml_expr e2
672
  | "mod", Expr_tuple([e1;e2]) -> fprintf fmt "(%a mod %a)" pp_xml_expr e1 pp_xml_expr e2
673
  | "&&", Expr_tuple([e1;e2]) -> fprintf fmt "(%a and %a)" pp_xml_expr e1 pp_xml_expr e2
674
  | "||", Expr_tuple([e1;e2]) -> fprintf fmt "(%a or %a)" pp_xml_expr e1 pp_xml_expr e2
675
  | "xor", Expr_tuple([e1;e2]) -> fprintf fmt "(%a xor %a)" pp_xml_expr e1 pp_xml_expr e2
676
  | "impl", Expr_tuple([e1;e2]) -> fprintf fmt "(%a => %a)" pp_xml_expr e1 pp_xml_expr e2
677
  | "<", Expr_tuple([e1;e2]) -> fprintf fmt "(%a &lt; %a)" pp_xml_expr e1 pp_xml_expr e2
678
  | "<=", Expr_tuple([e1;e2]) -> fprintf fmt "(%a &lt;= %a)" pp_xml_expr e1 pp_xml_expr e2
679
  | ">", Expr_tuple([e1;e2]) -> fprintf fmt "(%a &gt; %a)" pp_xml_expr e1 pp_xml_expr e2
680
  | ">=", Expr_tuple([e1;e2]) -> fprintf fmt "(%a &gt;= %a)" pp_xml_expr e1 pp_xml_expr e2
681
  | "!=", Expr_tuple([e1;e2]) -> fprintf fmt "(%a != %a)" pp_xml_expr e1 pp_xml_expr e2
682
  | "=", Expr_tuple([e1;e2]) -> fprintf fmt "(%a = %a)" pp_xml_expr e1 pp_xml_expr e2
683
  | "not", _ -> fprintf fmt "(not %a)" pp_xml_expr e
684
  | _, Expr_tuple _ -> fprintf fmt "%s %a" id pp_xml_expr e
685
  | _ -> fprintf fmt "%s (%a)" id pp_xml_expr e
646
  | "+", Expr_tuple [ e1; e2 ] ->
647
    fprintf fmt "(%a + %a)" pp_xml_expr e1 pp_xml_expr e2
648
  | "uminus", _ ->
649
    fprintf fmt "(- %a)" pp_xml_expr e
650
  | "-", Expr_tuple [ e1; e2 ] ->
651
    fprintf fmt "(%a - %a)" pp_xml_expr e1 pp_xml_expr e2
652
  | "*", Expr_tuple [ e1; e2 ] ->
653
    fprintf fmt "(%a * %a)" pp_xml_expr e1 pp_xml_expr e2
654
  | "/", Expr_tuple [ e1; e2 ] ->
655
    fprintf fmt "(%a / %a)" pp_xml_expr e1 pp_xml_expr e2
656
  | "mod", Expr_tuple [ e1; e2 ] ->
657
    fprintf fmt "(%a mod %a)" pp_xml_expr e1 pp_xml_expr e2
658
  | "&&", Expr_tuple [ e1; e2 ] ->
659
    fprintf fmt "(%a and %a)" pp_xml_expr e1 pp_xml_expr e2
660
  | "||", Expr_tuple [ e1; e2 ] ->
661
    fprintf fmt "(%a or %a)" pp_xml_expr e1 pp_xml_expr e2
662
  | "xor", Expr_tuple [ e1; e2 ] ->
663
    fprintf fmt "(%a xor %a)" pp_xml_expr e1 pp_xml_expr e2
664
  | "impl", Expr_tuple [ e1; e2 ] ->
665
    fprintf fmt "(%a => %a)" pp_xml_expr e1 pp_xml_expr e2
666
  | "<", Expr_tuple [ e1; e2 ] ->
667
    fprintf fmt "(%a &lt; %a)" pp_xml_expr e1 pp_xml_expr e2
668
  | "<=", Expr_tuple [ e1; e2 ] ->
669
    fprintf fmt "(%a &lt;= %a)" pp_xml_expr e1 pp_xml_expr e2
670
  | ">", Expr_tuple [ e1; e2 ] ->
671
    fprintf fmt "(%a &gt; %a)" pp_xml_expr e1 pp_xml_expr e2
672
  | ">=", Expr_tuple [ e1; e2 ] ->
673
    fprintf fmt "(%a &gt;= %a)" pp_xml_expr e1 pp_xml_expr e2
674
  | "!=", Expr_tuple [ e1; e2 ] ->
675
    fprintf fmt "(%a != %a)" pp_xml_expr e1 pp_xml_expr e2
676
  | "=", Expr_tuple [ e1; e2 ] ->
677
    fprintf fmt "(%a = %a)" pp_xml_expr e1 pp_xml_expr e2
678
  | "not", _ ->
679
    fprintf fmt "(not %a)" pp_xml_expr e
680
  | _, Expr_tuple _ ->
681
    fprintf fmt "%s %a" id pp_xml_expr e
682
  | _ ->
683
    fprintf fmt "%s (%a)" id pp_xml_expr e
686 684

  
687 685
and pp_xml_eexpr fmt e =
688 686
  fprintf fmt "%a%t %a"
689
    (Utils.fprintf_list ~sep:"; " Printers.pp_quantifiers) e.eexpr_quantifiers
690
    (fun fmt -> match e.eexpr_quantifiers with [] -> () | _ -> fprintf fmt ";")
687
    (Utils.fprintf_list ~sep:"; " Printers.pp_quantifiers)
688
    e.eexpr_quantifiers
689
    (fun fmt ->
690
      match e.eexpr_quantifiers with [] -> () | _ -> fprintf fmt ";")
691 691
    pp_xml_expr e.eexpr_qfexpr
692 692

  
693
and  pp_xml_sf_value fmt e =
694
   fprintf fmt "%a"
695
     (* (Utils.fprintf_list ~sep:"; " pp_xml_quantifiers) e.eexpr_quantifiers *)
696
     (* (fun fmt -> match e.eexpr_quantifiers *)
697
     (*             with [] -> () *)
698
     (*                | _ -> fprintf fmt ";") *)
699
     pp_xml_expr e.eexpr_qfexpr
693
and pp_xml_sf_value fmt e =
694
  fprintf fmt "%a"
695
    (* (Utils.fprintf_list ~sep:"; " pp_xml_quantifiers) e.eexpr_quantifiers *)
696
    (* (fun fmt -> match e.eexpr_quantifiers *)
697
    (*             with [] -> () *)
698
    (*                | _ -> fprintf fmt ";") *)
699
    pp_xml_expr e.eexpr_qfexpr
700 700

  
701 701
and pp_xml_s_function fmt expr_ann =
702 702
  let pp_xml_annot fmt (kwds, ee) =
703 703
    Format.fprintf fmt " %t : %a"
704
                   (fun fmt -> match kwds with
705
                               | [] -> assert false
706
                               | [x] -> Format.pp_print_string fmt x
707
                               | _ -> Format.fprintf fmt "%a" (Utils.fprintf_list ~sep:"/" Format.pp_print_string) kwds)
708
                   pp_xml_sf_value ee
704
      (fun fmt ->
705
        match kwds with
706
        | [] ->
707
          assert false
708
        | [ x ] ->
709
          Format.pp_print_string fmt x
710
        | _ ->
711
          Format.fprintf fmt "%a"
712
            (Utils.fprintf_list ~sep:"/" Format.pp_print_string)
713
            kwds)
714
      pp_xml_sf_value ee
709 715
  in
710 716
  Utils.fprintf_list ~sep:"@ " pp_xml_annot fmt expr_ann.annots
711 717

  
712 718
and pp_xml_expr_annot fmt expr_ann =
713 719
  let pp_xml_annot fmt (kwds, ee) =
714 720
    Format.fprintf fmt "(*! %t: %a; *)"
715
      (fun fmt -> match kwds with | [] -> assert false | [x] -> Format.pp_print_string fmt x | _ -> Format.fprintf fmt "/%a/" (Utils.fprintf_list ~sep:"/" Format.pp_print_string) kwds)
721
      (fun fmt ->
722
        match kwds with
723
        | [] ->
724
          assert false
725
        | [ x ] ->
726
          Format.pp_print_string fmt x
727
        | _ ->
728
          Format.fprintf fmt "/%a/"
729
            (Utils.fprintf_list ~sep:"/" Format.pp_print_string)
730
            kwds)
716 731
      pp_xml_eexpr ee
717 732
  in
718 733
  Utils.fprintf_list ~sep:"@ " pp_xml_annot fmt expr_ann.annots
719 734

  
720

  
721 735
(* Local Variables: *)
722 736
(* compile-command:"make -C ../../.." *)
723 737
(* End: *)

Also available in: Unified diff