Project

General

Profile

« Previous | Next » 

Revision ca7ff3f7

Added by LĂ©lio Brun 7 months ago

reformatting

View differences:

src/tools/zustre/zustre_common.ml
1 1
open Lustre_types
2 2
open Machine_code_types
3 3
open Machine_code_common
4

  
4 5
(* open Horn_backend_common
5 6
 * open Horn_backend *)
6 7
open Zustre_data
7
  
8

  
8 9
let report = Log.report ~plugin:"z3 interface"
9
           
10

  
10 11
module HBC = Horn_backend_common
12

  
11 13
let node_name = HBC.node_name
12 14

  
13 15
let concat = HBC.concat
14 16

  
15 17
let rename_machine = HBC.rename_machine
18

  
16 19
let rename_machine_list = HBC.rename_machine_list
17 20

  
18 21
let rename_next = HBC.rename_next
22

  
19 23
let rename_mid = HBC.rename_mid
24

  
20 25
let rename_current = HBC.rename_current
21 26

  
22 27
let rename_current_list = HBC.rename_current_list
28

  
23 29
let rename_mid_list = HBC.rename_mid_list
30

  
24 31
let rename_next_list = HBC.rename_next_list
25 32

  
26 33
let full_memory_vars = HBC.full_memory_vars
34

  
27 35
let inout_vars = HBC.inout_vars
36

  
28 37
let reset_vars = HBC.reset_vars
38

  
29 39
let step_vars = HBC.step_vars
40

  
30 41
let local_memory_vars = HBC.local_memory_vars
42

  
31 43
let step_vars_m_x = HBC.step_vars_m_x
44

  
32 45
let step_vars_c_m_x = HBC.step_vars_c_m_x
33
  
34
let machine_reset_name = HBC.machine_reset_name 
35
let machine_step_name = HBC.machine_step_name 
36
let machine_stateless_name = HBC.machine_stateless_name 
46

  
47
let machine_reset_name = HBC.machine_reset_name
48

  
49
let machine_step_name = HBC.machine_step_name
50

  
51
let machine_stateless_name = HBC.machine_stateless_name
37 52

  
38 53
let preprocess = Horn_backend.preprocess
39
  
40 54

  
41 55
exception UnknownFunction of (string * (Format.formatter -> unit))
42 56
(** Sorts
43 57

  
44
A sort is introduced for each basic type and each enumerated type.
58
    A sort is introduced for each basic type and each enumerated type.
45 59

  
46
A hashtbl records these and allow easy access to sort values, when
47
   provided with a enumerated type name. 
60
    A hashtbl records these and allow easy access to sort values, when provided
61
    with a enumerated type name. *)
48 62

  
49
*)
50
        
51 63
let bool_sort = Z3.Boolean.mk_sort !ctx
64

  
52 65
let int_sort = Z3.Arithmetic.Integer.mk_sort !ctx
66

  
53 67
let real_sort = Z3.Arithmetic.Real.mk_sort !ctx
54 68

  
69
let get_const_sort = Hashtbl.find const_sorts
55 70

  
56
let get_const_sort = Hashtbl.find const_sorts  
57 71
let get_sort_elems = Hashtbl.find sort_elems
58
let get_tag_sort id = try Hashtbl.find const_tags id with _ -> Format.eprintf "Unable to find sort for tag=%s@." id; assert false
59
  
60 72

  
61
  
73
let get_tag_sort id =
74
  try Hashtbl.find const_tags id
75
  with _ ->
76
    Format.eprintf "Unable to find sort for tag=%s@." id;
77
    assert false
78

  
62 79
let decl_sorts () =
63
  Hashtbl.iter (fun typ decl ->
64
    match typ with
65
    | Tydec_const var ->
66
      (match decl.top_decl_desc with
67
      | TypeDef tdef -> (
68
	match tdef.tydef_desc with
69
	| Tydec_enum tl ->
70
	  let new_sort = Z3.Enumeration.mk_sort_s !ctx var tl in
71
          Hashtbl.add const_sorts var new_sort;
72
          Hashtbl.add sort_elems new_sort tl;
73
          List.iter (fun t -> Hashtbl.add const_tags t new_sort) tl
74
          
75
	| _ -> Format.eprintf "Unknown type : %a@.@?" Printers.pp_var_type_dec_desc typ; assert false
76
      )
77
      | _ -> assert false
78
      )
79
    | _        -> ()) Corelang.type_table
80

  
81
                 
82
let rec type_to_sort t =
83
  if Types.is_bool_type t  then bool_sort else
84
    if Types.is_int_type t then int_sort else 
85
  if Types.is_real_type t then real_sort else 
86
  match (Types.repr t).Types.tdesc with
87
  | Types.Tconst ty       -> get_const_sort ty
88
  | Types.Tclock t        -> type_to_sort t
89
  | Types.Tarray(_, ty)   -> Z3.Z3Array.mk_sort !ctx int_sort (type_to_sort ty)
90
  | Types.Tstatic(_, ty)  -> type_to_sort ty
91
  | Types.Tarrow _
92
  | _                     -> Format.eprintf "internal error: pp_type %a@."
93
                               Types.print_ty t; assert false
80
  Hashtbl.iter
81
    (fun typ decl ->
82
      match typ with
83
      | Tydec_const var -> (
84
        match decl.top_decl_desc with
85
        | TypeDef tdef -> (
86
          match tdef.tydef_desc with
87
          | Tydec_enum tl ->
88
            let new_sort = Z3.Enumeration.mk_sort_s !ctx var tl in
89
            Hashtbl.add const_sorts var new_sort;
90
            Hashtbl.add sort_elems new_sort tl;
91
            List.iter (fun t -> Hashtbl.add const_tags t new_sort) tl
92
          | _ ->
93
            Format.eprintf "Unknown type : %a@.@?" Printers.pp_var_type_dec_desc
94
              typ;
95
            assert false)
96
        | _ ->
97
          assert false)
98
      | _ ->
99
        ())
100
    Corelang.type_table
94 101

  
102
let rec type_to_sort t =
103
  if Types.is_bool_type t then bool_sort
104
  else if Types.is_int_type t then int_sort
105
  else if Types.is_real_type t then real_sort
106
  else
107
    match (Types.repr t).Types.tdesc with
108
    | Types.Tconst ty ->
109
      get_const_sort ty
110
    | Types.Tclock t ->
111
      type_to_sort t
112
    | Types.Tarray (_, ty) ->
113
      Z3.Z3Array.mk_sort !ctx int_sort (type_to_sort ty)
114
    | Types.Tstatic (_, ty) ->
115
      type_to_sort ty
116
    | Types.Tarrow _ | _ ->
117
      Format.eprintf "internal error: pp_type %a@." Types.print_ty t;
118
      assert false
95 119

  
96 120
(* let idx_var = *)
97 121
(*   Z3.FuncDecl.mk_func_decl_s !ctx "__idx__" [] idx_sort  *)
98
    
122

  
99 123
(* let uid_var = *)
100 124
(*   Z3.FuncDecl.mk_func_decl_s !ctx "__uid__" [] uid_sort  *)
101 125

  
......
103 127

  
104 128
    Similarly fun_decls are registerd, by their name, into a hashtbl. The
105 129
    proposed encoding introduces a 0-ary fun_decl to model variables and
106
    fun_decl with arguments to declare reset and step predicates.
107

  
108

  
109

  
110
*)
130
    fun_decl with arguments to declare reset and step predicates. *)
111 131
let register_fdecl id fd = Hashtbl.add decls id fd
132

  
112 133
let get_fdecl id =
113
  try
114
    Hashtbl.find decls id
115
  with Not_found -> (report ~level:3 (fun fmt -> Format.fprintf fmt  "Unable to find func_decl %s@.@?" id); raise Not_found)
134
  try Hashtbl.find decls id
135
  with Not_found ->
136
    report ~level:3 (fun fmt ->
137
        Format.fprintf fmt "Unable to find func_decl %s@.@?" id);
138
    raise Not_found
116 139

  
117 140
let pp_fdecls fmt =
118 141
  Format.fprintf fmt "Registered fdecls: @[%a@]@ "
119
    (Utils.fprintf_list ~sep:"@ " Format.pp_print_string)  (Hashtbl.fold (fun id _ accu -> id::accu) decls [])
142
    (Utils.fprintf_list ~sep:"@ " Format.pp_print_string)
143
    (Hashtbl.fold (fun id _ accu -> id :: accu) decls [])
120 144

  
121
    
122 145
let decl_var id =
123 146
  (* Format.eprintf "Declaring var %s@." id.var_id; *)
124
  let fdecl = Z3.FuncDecl.mk_func_decl_s !ctx id.var_id [] (type_to_sort id.var_type) in
147
  let fdecl =
148
    Z3.FuncDecl.mk_func_decl_s !ctx id.var_id [] (type_to_sort id.var_type)
149
  in
125 150
  register_fdecl id.var_id fdecl;
126 151
  fdecl
127 152

  
128
(* Declaring the function used in expr *) 
153
(* Declaring the function used in expr *)
129 154
let decl_fun op args typ =
130 155
  let args = List.map type_to_sort args in
131 156
  let fdecl = Z3.FuncDecl.mk_func_decl_s !ctx op args (type_to_sort typ) in
......
133 158
  fdecl
134 159

  
135 160
let idx_sort = int_sort
136
let uid_sort = Z3.Z3List.mk_sort !ctx (Z3.Symbol.mk_string !ctx "uid_list") int_sort
137
let uid_conc = 
161

  
162
let uid_sort =
163
  Z3.Z3List.mk_sort !ctx (Z3.Symbol.mk_string !ctx "uid_list") int_sort
164

  
165
let uid_conc =
138 166
  let fd = Z3.Z3List.get_cons_decl uid_sort in
139
  fun head tail -> Z3.FuncDecl.apply fd [head;tail]
167
  fun head tail -> Z3.FuncDecl.apply fd [ head; tail ]
140 168

  
141 169
let get_instance_uid =
142 170
  let hash : (string, int) Hashtbl.t = Hashtbl.create 13 in
143 171
  let cpt = ref 0 in
144 172
  fun i ->
145 173
    let id =
146
      if Hashtbl.mem hash i then
147
	Hashtbl.find hash i
174
      if Hashtbl.mem hash i then Hashtbl.find hash i
148 175
      else (
149
	incr cpt;
150
	Hashtbl.add hash i !cpt;
151
	!cpt
152
      )
176
        incr cpt;
177
        Hashtbl.add hash i !cpt;
178
        !cpt)
153 179
    in
154 180
    Z3.Arithmetic.Integer.mk_numeral_i !ctx id
155
  
156 181

  
157
  
158
let decl_rel ?(no_additional_vars=false) name args_sorts =
159
  (* Enriching arg_sorts with two new variables: a counting index and an
160
     uid *)
182
let decl_rel ?(no_additional_vars = false) name args_sorts =
183
  (* Enriching arg_sorts with two new variables: a counting index and an uid *)
161 184
  let args_sorts =
162
    if no_additional_vars then args_sorts else idx_sort::uid_sort::args_sorts in
163
  
185
    if no_additional_vars then args_sorts
186
    else idx_sort :: uid_sort :: args_sorts
187
  in
188

  
164 189
  (* let args_sorts = List.map (fun v -> type_to_sort v.var_type) args in *)
165 190
  if !debug then
166
    Format.eprintf "Registering fdecl %s (%a)@."
167
      name
168
      (Utils.fprintf_list ~sep:"@ "
169
	 (fun fmt sort -> Format.fprintf fmt "%s" (Z3.Sort.to_string sort)))
170
      args_sorts
171
  ;
191
    Format.eprintf "Registering fdecl %s (%a)@." name
192
      (Utils.fprintf_list ~sep:"@ " (fun fmt sort ->
193
           Format.fprintf fmt "%s" (Z3.Sort.to_string sort)))
194
      args_sorts;
172 195
  let fdecl = Z3.FuncDecl.mk_func_decl_s !ctx name args_sorts bool_sort in
173 196
  Z3.Fixedpoint.register_relation !fp fdecl;
174 197
  register_fdecl name fdecl;
175 198
  fdecl
176
  
177

  
178 199

  
179 200
(* Shared variables to describe counter and uid *)
180 201

  
181 202
let idx = Corelang.dummy_var_decl "__idx__" Type_predef.type_int
182
let idx_var = Z3.Expr.mk_const_f !ctx (decl_var idx) 
183
let uid = Corelang.dummy_var_decl "__uid__" Type_predef.type_int
184
let uid_fd = Z3.FuncDecl.mk_func_decl_s !ctx "__uid__" [] uid_sort 
185
let _ = register_fdecl "__uid__"  uid_fd  
186
let uid_var = Z3.Expr.mk_const_f !ctx uid_fd 
187 203

  
188
(** Conversion functions
204
let idx_var = Z3.Expr.mk_const_f !ctx (decl_var idx)
189 205

  
190
    The following is similar to the Horn backend. Each printing function is
191
    rephrased from pp_xx to xx_to_expr and produces a Z3 value.
206
let uid = Corelang.dummy_var_decl "__uid__" Type_predef.type_int
192 207

  
193
*)
208
let uid_fd = Z3.FuncDecl.mk_func_decl_s !ctx "__uid__" [] uid_sort
194 209

  
210
let _ = register_fdecl "__uid__" uid_fd
195 211

  
196
(* Returns the f_decl associated to the variable v *)
197
let horn_var_to_expr v =
198
  Z3.Expr.mk_const_f !ctx (get_fdecl v.var_id)
212
let uid_var = Z3.Expr.mk_const_f !ctx uid_fd
199 213

  
214
(** Conversion functions
200 215

  
216
    The following is similar to the Horn backend. Each printing function is
217
    rephrased from pp_xx to xx_to_expr and produces a Z3 value. *)
201 218

  
219
(* Returns the f_decl associated to the variable v *)
220
let horn_var_to_expr v = Z3.Expr.mk_const_f !ctx (get_fdecl v.var_id)
202 221

  
203
  (* Used to print boolean constants *)
222
(* Used to print boolean constants *)
204 223
let horn_tag_to_expr t =
205
  if t = tag_true then
206
    Z3.Boolean.mk_true !ctx
207
  else if t = tag_false then
208
    Z3.Boolean.mk_false !ctx
224
  if t = tag_true then Z3.Boolean.mk_true !ctx
225
  else if t = tag_false then Z3.Boolean.mk_false !ctx
209 226
  else
210 227
    (* Finding the associated sort *)
211 228
    let sort = get_tag_sort t in
212
    let elems = get_sort_elems sort in 
229
    let elems = get_sort_elems sort in
213 230
    let res : Z3.Expr.expr option =
214
      List.fold_left2 (fun res cst expr ->
231
      List.fold_left2
232
        (fun res cst expr ->
215 233
          match res with
216
          | Some _ -> res
217
          | None -> if t = cst then Some (expr:Z3.Expr.expr) else None
218
        ) None elems (Z3.Enumeration.get_consts sort)
234
          | Some _ ->
235
            res
236
          | None ->
237
            if t = cst then Some (expr : Z3.Expr.expr) else None)
238
        None elems
239
        (Z3.Enumeration.get_consts sort)
219 240
    in
220 241
    match res with None -> assert false | Some s -> s
221
    
242

  
222 243
(* Prints a constant value *)
223 244
let horn_const_to_expr c =
224 245
  match c with
225
    | Const_int i    -> Z3.Arithmetic.Integer.mk_numeral_i !ctx i
226
    | Const_real r  -> Z3.Arithmetic.Real.mk_numeral_s !ctx (Real.to_string r)
227
    | Const_tag t    -> horn_tag_to_expr t
228
    | _              -> assert false
229

  
230

  
246
  | Const_int i ->
247
    Z3.Arithmetic.Integer.mk_numeral_i !ctx i
248
  | Const_real r ->
249
    Z3.Arithmetic.Real.mk_numeral_s !ctx (Real.to_string r)
250
  | Const_tag t ->
251
    horn_tag_to_expr t
252
  | _ ->
253
    assert false
231 254

  
232 255
(* Default value for each type, used when building arrays. Eg integer array
233 256
   [2;7] is defined as (store (store (0) 1 7) 0 2) where 0 is this default value
234
   for the type integer (arrays).
235
*)
257
   for the type integer (arrays). *)
236 258
let horn_default_val t =
237 259
  let t = Types.dynamic_type t in
238
  if Types.is_bool_type t  then Z3.Boolean.mk_true !ctx else
239
  if Types.is_int_type t then Z3.Arithmetic.Integer.mk_numeral_i !ctx 0 else 
240
  if Types.is_real_type t then Z3.Arithmetic.Real.mk_numeral_i !ctx 0 else 
241
  (* match (Types.dynamic_type t).Types.tdesc with
242
   * | Types.Tarray(dim, l) -> (\* TODO PL: this strange code has to be (heavily) checked *\)
243
   *    let valt = Types.array_element_type t in
244
   *    fprintf fmt "((as const (Array Int %a)) %a)"
245
   *      pp_type valt 
246
   *      pp_default_val valt
247
   * | Types.Tstruct(l) -> assert false
248
   * | Types.Ttuple(l) -> assert false
249
   * |_ -> *) assert false
260
  if Types.is_bool_type t then Z3.Boolean.mk_true !ctx
261
  else if Types.is_int_type t then Z3.Arithmetic.Integer.mk_numeral_i !ctx 0
262
  else if Types.is_real_type t then Z3.Arithmetic.Real.mk_numeral_i !ctx 0
263
  else
264
    (* match (Types.dynamic_type t).Types.tdesc with
265
     * | Types.Tarray(dim, l) -> (\* TODO PL: this strange code has to be (heavily) checked *\)
266
     *    let valt = Types.array_element_type t in
267
     *    fprintf fmt "((as const (Array Int %a)) %a)"
268
     *      pp_type valt 
269
     *      pp_default_val valt
270
     * | Types.Tstruct(l) -> assert false
271
     * | Types.Ttuple(l) -> assert false
272
     * |_ -> *)
273
    assert false
250 274

  
251 275
(* Conversion of basic library functions *)
252
    
276

  
253 277
let horn_basic_app i vl (vltyp, typ) =
254 278
  match i, vl with
255
  | "ite", [v1; v2; v3] ->  Z3.Boolean.mk_ite !ctx v1 v2 v3
256
  | "uminus", [v] ->    Z3.Arithmetic.mk_unary_minus
257
       !ctx v
258
  | "not", [v] ->
259
     Z3.Boolean.mk_not
260
       !ctx v
261
  | "=", [v1; v2] ->
262
     Z3.Boolean.mk_eq
263
       !ctx v1 v2
264
  | "&&", [v1; v2] ->
265
     Z3.Boolean.mk_and
266
       !ctx
267
       [v1; v2]
268
  | "||", [v1; v2] ->
269
          Z3.Boolean.mk_or
270
       !ctx
271
       [v1;
272
         v2]
273

  
274
  | "impl", [v1; v2] ->
275
     Z3.Boolean.mk_implies
276
       !ctx v1 v2
277
 | "mod", [v1; v2] ->
278
          Z3.Arithmetic.Integer.mk_mod
279
       !ctx v1 v2
280
  | "equi", [v1; v2] ->
281
          Z3.Boolean.mk_eq
282
       !ctx
283
       v1 v2
284
  | "xor", [v1; v2] ->
285
          Z3.Boolean.mk_xor
286
       !ctx v1 v2
287
  | "!=", [v1; v2] ->
288
     Z3.Boolean.mk_not
289
       !ctx
290
       (
291
         Z3.Boolean.mk_eq
292
           !ctx v1 v2
293
       )
294
  | "/", [v1; v2] ->
295
     Z3.Arithmetic.mk_div
296
       !ctx v1 v2
297

  
298
  | "+", [v1; v2] ->
299
     Z3.Arithmetic.mk_add
300
       !ctx
301
       [v1; v2]
302
  | "-", [v1; v2] ->
303
     Z3.Arithmetic.mk_sub
304
       !ctx
305
       [v1 ;  v2]
306
       
307
  | "*", [v1; v2] ->
308
     Z3.Arithmetic.mk_mul
309
       !ctx
310
       [ v1;  v2]
311

  
312

  
313
  | "<", [v1; v2] ->
314
     Z3.Arithmetic.mk_lt
315
       !ctx v1 v2
316
  | "<=", [v1; v2] ->
317
     Z3.Arithmetic.mk_le
318
       !ctx v1 v2
319
  | ">", [v1; v2] ->
320
     Z3.Arithmetic.mk_gt
321
       !ctx v1 v2
322
  | ">=", [v1; v2] ->
323
     Z3.Arithmetic.mk_ge
324
       !ctx v1 v2
325
  | "int_to_real", [v1] ->
326
     Z3.Arithmetic.Integer.mk_int2real
327
       !ctx v1
279
  | "ite", [ v1; v2; v3 ] ->
280
    Z3.Boolean.mk_ite !ctx v1 v2 v3
281
  | "uminus", [ v ] ->
282
    Z3.Arithmetic.mk_unary_minus !ctx v
283
  | "not", [ v ] ->
284
    Z3.Boolean.mk_not !ctx v
285
  | "=", [ v1; v2 ] ->
286
    Z3.Boolean.mk_eq !ctx v1 v2
287
  | "&&", [ v1; v2 ] ->
288
    Z3.Boolean.mk_and !ctx [ v1; v2 ]
289
  | "||", [ v1; v2 ] ->
290
    Z3.Boolean.mk_or !ctx [ v1; v2 ]
291
  | "impl", [ v1; v2 ] ->
292
    Z3.Boolean.mk_implies !ctx v1 v2
293
  | "mod", [ v1; v2 ] ->
294
    Z3.Arithmetic.Integer.mk_mod !ctx v1 v2
295
  | "equi", [ v1; v2 ] ->
296
    Z3.Boolean.mk_eq !ctx v1 v2
297
  | "xor", [ v1; v2 ] ->
298
    Z3.Boolean.mk_xor !ctx v1 v2
299
  | "!=", [ v1; v2 ] ->
300
    Z3.Boolean.mk_not !ctx (Z3.Boolean.mk_eq !ctx v1 v2)
301
  | "/", [ v1; v2 ] ->
302
    Z3.Arithmetic.mk_div !ctx v1 v2
303
  | "+", [ v1; v2 ] ->
304
    Z3.Arithmetic.mk_add !ctx [ v1; v2 ]
305
  | "-", [ v1; v2 ] ->
306
    Z3.Arithmetic.mk_sub !ctx [ v1; v2 ]
307
  | "*", [ v1; v2 ] ->
308
    Z3.Arithmetic.mk_mul !ctx [ v1; v2 ]
309
  | "<", [ v1; v2 ] ->
310
    Z3.Arithmetic.mk_lt !ctx v1 v2
311
  | "<=", [ v1; v2 ] ->
312
    Z3.Arithmetic.mk_le !ctx v1 v2
313
  | ">", [ v1; v2 ] ->
314
    Z3.Arithmetic.mk_gt !ctx v1 v2
315
  | ">=", [ v1; v2 ] ->
316
    Z3.Arithmetic.mk_ge !ctx v1 v2
317
  | "int_to_real", [ v1 ] ->
318
    Z3.Arithmetic.Integer.mk_int2real !ctx v1
328 319
  | _ ->
329
     let fd =
330
       try
331
         get_fdecl i
332
       with Not_found -> begin
333
           report ~level:3 (fun fmt -> Format.fprintf fmt "Registering function %s as uninterpreted function in Z3@.%s: (%a) -> %a" i i (Utils.fprintf_list ~sep:"," Types.print_ty) vltyp Types.print_ty typ); 
334
           decl_fun i vltyp typ
335
         end
336
     in
337
     Z3.FuncDecl.apply fd vl
338
    
339
     
340
  (* | _, [v1; v2] ->      Z3.Boolean.mk_and
341
   *      !ctx
342
   *      (val_to_expr v1)
343
   *      (val_to_expr v2)
344
   * 
345
   *      Format.fprintf fmt "(%s %a %a)" i val_to_exprr v1 val_to_expr v2 *)
320
    let fd =
321
      try get_fdecl i
322
      with Not_found ->
323
        report ~level:3 (fun fmt ->
324
            Format.fprintf fmt
325
              "Registering function %s as uninterpreted function in Z3@.%s: \
326
               (%a) -> %a"
327
              i i
328
              (Utils.fprintf_list ~sep:"," Types.print_ty)
329
              vltyp Types.print_ty typ);
330
        decl_fun i vltyp typ
331
    in
332
    Z3.FuncDecl.apply fd vl
333

  
334
(* | _, [v1; v2] ->      Z3.Boolean.mk_and
335
 *      !ctx
336
 *      (val_to_expr v1)
337
 *      (val_to_expr v2)
338
 * 
339
 *      Format.fprintf fmt "(%s %a %a)" i val_to_exprr v1 val_to_expr v2 *)
346 340

  
347 341
(* | _ -> (
348 342
 *     let msg fmt = Format.fprintf fmt
......
352 346
 *     raise (UnknownFunction(i, msg))
353 347
 *   ) *)
354 348

  
355
           
356
(* Convert a value expression [v], with internal function calls only.  [pp_var]
349
(* Convert a value expression [v], with internal function calls only. [pp_var]
357 350
   is a printer for variables (typically [pp_c_var_read]), but an offset suffix
358
   may be added for array variables
359
*)
360
let rec horn_val_to_expr ?(is_lhs=false) m self v =
351
   may be added for array variables *)
352
let rec horn_val_to_expr ?(is_lhs = false) m self v =
361 353
  (* Format.eprintf "h_v2e %a@." (Machine_code_common.pp_val m) v ; *)
362 354
  match v.value_desc with
363
  | Cst c       -> horn_const_to_expr c
364

  
355
  | Cst c ->
356
    horn_const_to_expr c
365 357
  (* Code specific for arrays *)
366
  | Array il    ->
367
     (* An array definition: 
368
	(store (
369
	  ...
370
 	    (store (
371
	       store (
372
	          default_val
373
	       ) 
374
	       idx_n val_n
375
	    ) 
376
	    idx_n-1 val_n-1)
377
	  ... 
378
	  idx_1 val_1
379
	) *)
380
     let rec build_array (tab, x) =
381
       match tab with
382
       | [] -> horn_default_val v.value_type(* (get_type v) *)
383
       | h::t ->
384
	  Z3.Z3Array.mk_store
385
            !ctx
386
	    (build_array (t, (x+1)))
387
	    (Z3.Arithmetic.Integer.mk_numeral_i !ctx x)
388
	    (horn_val_to_expr ~is_lhs:is_lhs m self h)
389
     in
390
     build_array (il, 0)
391
     
392
  | Access(tab,index) ->
393
     Z3.Z3Array.mk_select !ctx 
394
       (horn_val_to_expr ~is_lhs:is_lhs m self tab)
395
       (horn_val_to_expr ~is_lhs:is_lhs m self index)
396

  
358
  | Array il ->
359
    (* An array definition: (store ( ... (store ( store ( default_val ) idx_n
360
       val_n ) idx_n-1 val_n-1) ... idx_1 val_1 ) *)
361
    let rec build_array (tab, x) =
362
      match tab with
363
      | [] ->
364
        horn_default_val v.value_type (* (get_type v) *)
365
      | h :: t ->
366
        Z3.Z3Array.mk_store !ctx
367
          (build_array (t, x + 1))
368
          (Z3.Arithmetic.Integer.mk_numeral_i !ctx x)
369
          (horn_val_to_expr ~is_lhs m self h)
370
    in
371
    build_array (il, 0)
372
  | Access (tab, index) ->
373
    Z3.Z3Array.mk_select !ctx
374
      (horn_val_to_expr ~is_lhs m self tab)
375
      (horn_val_to_expr ~is_lhs m self index)
397 376
  (* Code specific for arrays *)
398
    
399
  | Power _  -> assert false
400
  | Var v    ->
401
     if is_memory m v then
402
       if Types.is_array_type v.var_type
403
       then assert false
404
       else horn_var_to_expr (rename_machine self ((if is_lhs then rename_next else rename_current) (* self *) v))
405
     
406
     else 
407
       horn_var_to_expr
408
         (rename_machine
409
            self
410
            v)
411
  | Fun (n, vl)   -> horn_basic_app n (List.map (horn_val_to_expr m self) vl) (List.map (fun v -> v.value_type) vl, v.value_type)
377
  | Power _ ->
378
    assert false
379
  | Var v ->
380
    if is_memory m v then
381
      if Types.is_array_type v.var_type then assert false
382
      else
383
        horn_var_to_expr
384
          (rename_machine self
385
             ((if is_lhs then rename_next else rename_current (* self *)) v))
386
    else horn_var_to_expr (rename_machine self v)
387
  | Fun (n, vl) ->
388
    horn_basic_app n
389
      (List.map (horn_val_to_expr m self) vl)
390
      (List.map (fun v -> v.value_type) vl, v.value_type)
412 391

  
413 392
let no_reset_to_exprs machines m i =
414
  let (n,_) = List.assoc i m.minstances in
415
  let target_machine = List.find (fun m  -> m.mname.node_id = (Corelang.node_name n)) machines in
393
  let n, _ = List.assoc i m.minstances in
394
  let target_machine =
395
    List.find (fun m -> m.mname.node_id = Corelang.node_name n) machines
396
  in
416 397

  
417
  let m_list = 
418
    rename_machine_list
419
      (concat m.mname.node_id i)
398
  let m_list =
399
    rename_machine_list (concat m.mname.node_id i)
420 400
      (rename_mid_list (full_memory_vars machines target_machine))
421 401
  in
422 402
  let c_list =
423
    rename_machine_list
424
      (concat m.mname.node_id i)
403
    rename_machine_list (concat m.mname.node_id i)
425 404
      (rename_current_list (full_memory_vars machines target_machine))
426 405
  in
427 406
  match c_list, m_list with
428
  | [chd], [mhd] ->
429
     let expr =
430
       Z3.Boolean.mk_eq !ctx 
431
         (horn_var_to_expr mhd)
432
         (horn_var_to_expr chd)
433
     in
434
     [expr]
435
  | _ -> (
407
  | [ chd ], [ mhd ] ->
408
    let expr =
409
      Z3.Boolean.mk_eq !ctx (horn_var_to_expr mhd) (horn_var_to_expr chd)
410
    in
411
    [ expr ]
412
  | _ ->
436 413
    let exprs =
437
      List.map2 (fun mhd chd -> 
438
          Z3.Boolean.mk_eq !ctx 
439
            (horn_var_to_expr mhd)
440
            (horn_var_to_expr chd)
441
        )
442
        m_list
443
        c_list
414
      List.map2
415
        (fun mhd chd ->
416
          Z3.Boolean.mk_eq !ctx (horn_var_to_expr mhd) (horn_var_to_expr chd))
417
        m_list c_list
444 418
    in
445 419
    exprs
446
  )
447 420

  
448 421
let instance_reset_to_exprs machines m i =
449
  let (n,_) = List.assoc i m.minstances in
450
  let target_machine = List.find (fun m  -> m.mname.node_id = (Corelang.node_name n)) machines in
422
  let n, _ = List.assoc i m.minstances in
423
  let target_machine =
424
    List.find (fun m -> m.mname.node_id = Corelang.node_name n) machines
425
  in
451 426
  let vars =
452
    (rename_machine_list
453
       (concat m.mname.node_id i)
454
       (rename_current_list (full_memory_vars machines target_machine))@  (rename_mid_list (full_memory_vars machines target_machine))
455
    )
456
    
427
    rename_machine_list (concat m.mname.node_id i)
428
      (rename_current_list (full_memory_vars machines target_machine))
429
    @ rename_mid_list (full_memory_vars machines target_machine)
457 430
  in
431

  
458 432
  let expr =
459
    Z3.Expr.mk_app
460
      !ctx
433
    Z3.Expr.mk_app !ctx
461 434
      (get_fdecl (machine_reset_name (Corelang.node_name n)))
462
      (List.map (horn_var_to_expr) (idx::uid::vars))
435
      (List.map horn_var_to_expr (idx :: uid :: vars))
463 436
  in
464
  [expr]
437
  [ expr ]
465 438

  
466 439
let instance_call_to_exprs machines reset_instances m i inputs outputs =
467 440
  let self = m.mname.node_id in
......
471 444
    (* Additional input to register step counters, and uid *)
472 445
    let idx = horn_var_to_expr idx in
473 446
    let uid = uid_conc (get_instance_uid i) (horn_var_to_expr uid) in
474
    let inout = 
447
    let inout =
475 448
      List.map (horn_val_to_expr m self)
476
	(inputs @ (List.map (fun v -> mk_val (Var v) v.var_type) outputs))
449
        (inputs @ List.map (fun v -> mk_val (Var v) v.var_type) outputs)
477 450
    in
478
    idx::uid::inout
451
    idx :: uid :: inout
479 452
  in
480
    
481
  try (* stateful node instance *)
482
    begin
483
      let (n,_) = List.assoc i m.minstances in
484
      let target_machine = List.find (fun m  -> m.mname.node_id = Corelang.node_name n) machines in
485

  
486
      (* Checking whether this specific instances has been reset yet *)
487
      let reset_exprs = 
488
        if not (List.mem i reset_instances) then
489
	  (* If not, declare mem_m = mem_c *)
490
	  no_reset_to_exprs machines m i
491
        else
492
          [] (* Nothing to add yet *)
493
      in
494
      
495
      let mems = full_memory_vars machines target_machine in
496
      let rename_mems f = rename_machine_list (concat m.mname.node_id i) (f mems) in
497
      let mid_mems = rename_mems rename_mid_list in
498
      let next_mems = rename_mems rename_next_list in
499

  
500
      let call_expr = 
501
	match Corelang.node_name n, inputs, outputs, mid_mems, next_mems with
502
	| "_arrow", [i1; i2], [o], [mem_m], [mem_x] -> begin
503
          let stmt1 = (* out = ite mem_m then i1 else i2 *)
504
            Z3.Boolean.mk_eq !ctx
505
              ( (* output var *)
506
                horn_val_to_expr 
507
                  ~is_lhs:true
508
                  m self
509
                  (mk_val (Var o) o.var_type)
510
              )
511
              (
512
                Z3.Boolean.mk_ite !ctx 
513
	          (horn_var_to_expr mem_m) 
514
	          (horn_val_to_expr m self i1)
515
	          (horn_val_to_expr m self i2)
516
              )
517
          in
518
          let stmt2 = (* mem_X = false *)
519
            Z3.Boolean.mk_eq !ctx
520
	      (horn_var_to_expr mem_x)
521
              (Z3.Boolean.mk_false !ctx)
522
          in
523
          [stmt1; stmt2]
524
	end
525

  
526
	| _ ->
527
           let expr = 
528
             Z3.Expr.mk_app
529
               !ctx
530
               (get_fdecl (machine_step_name (node_name n)))
531
               ( (* Arguments are input, output, mid_mems, next_mems *)
532
		 idx_uid_inout @ List.map (horn_var_to_expr) (mid_mems@next_mems)
533
		    
534
               )
535
           in
536
           [expr]
537
      in
538 453

  
539
      reset_exprs@call_expr
540
    end
541
  with Not_found -> ( (* stateless node instance *)
542
    let (n,_) = List.assoc i m.mcalls in
543
    let expr = 
544
      Z3.Expr.mk_app
545
        !ctx
546
        (get_fdecl (machine_stateless_name (node_name n)))
547
        idx_uid_inout 	  (* Arguments are inputs, outputs *)
454
  try
455
    (* stateful node instance *)
456
    let n, _ = List.assoc i m.minstances in
457
    let target_machine =
458
      List.find (fun m -> m.mname.node_id = Corelang.node_name n) machines
548 459
    in
549
    [expr]
550
  )
551 460

  
461
    (* Checking whether this specific instances has been reset yet *)
462
    let reset_exprs =
463
      if not (List.mem i reset_instances) then
464
        (* If not, declare mem_m = mem_c *)
465
        no_reset_to_exprs machines m i
466
      else []
467
      (* Nothing to add yet *)
468
    in
469

  
470
    let mems = full_memory_vars machines target_machine in
471
    let rename_mems f =
472
      rename_machine_list (concat m.mname.node_id i) (f mems)
473
    in
474
    let mid_mems = rename_mems rename_mid_list in
475
    let next_mems = rename_mems rename_next_list in
476

  
477
    let call_expr =
478
      match Corelang.node_name n, inputs, outputs, mid_mems, next_mems with
479
      | "_arrow", [ i1; i2 ], [ o ], [ mem_m ], [ mem_x ] ->
480
        let stmt1 =
481
          (* out = ite mem_m then i1 else i2 *)
482
          Z3.Boolean.mk_eq !ctx
483
            ((* output var *)
484
             horn_val_to_expr ~is_lhs:true m self
485
               (mk_val (Var o) o.var_type))
486
            (Z3.Boolean.mk_ite !ctx (horn_var_to_expr mem_m)
487
               (horn_val_to_expr m self i1)
488
               (horn_val_to_expr m self i2))
489
        in
490
        let stmt2 =
491
          (* mem_X = false *)
492
          Z3.Boolean.mk_eq !ctx (horn_var_to_expr mem_x)
493
            (Z3.Boolean.mk_false !ctx)
494
        in
495
        [ stmt1; stmt2 ]
496
      | _ ->
497
        let expr =
498
          Z3.Expr.mk_app !ctx
499
            (get_fdecl (machine_step_name (node_name n)))
500
            ((* Arguments are input, output, mid_mems, next_mems *)
501
             idx_uid_inout
502
            @ List.map horn_var_to_expr (mid_mems @ next_mems))
503
        in
504
        [ expr ]
505
    in
506

  
507
    reset_exprs @ call_expr
508
  with Not_found ->
509
    (* stateless node instance *)
510
    let n, _ = List.assoc i m.mcalls in
511
    let expr =
512
      Z3.Expr.mk_app !ctx
513
        (get_fdecl (machine_stateless_name (node_name n)))
514
        idx_uid_inout
515
      (* Arguments are inputs, outputs *)
516
    in
517
    [ expr ]
552 518

  
553
    
554 519
(* (\* Prints a [value] indexed by the suffix list [loop_vars] *\) *)
555 520
(* let rec value_suffix_to_expr self value = *)
556 521
(*  match value.value_desc with *)
557 522
(*  | Fun (n, vl)  ->  *)
558 523
(*     horn_basic_app n (horn_val_to_expr self) (value_suffix_to_expr self vl) *)
559
    
524

  
560 525
(*  |  _            -> *)
561 526
(*    horn_val_to_expr self value *)
562 527

  
563

  
564
(* type_directed assignment: array vs. statically sized type
565
   - [var_type]: type of variable to be assigned
566
   - [var_name]: name of variable to be assigned
567
   - [value]: assigned value
568
   - [pp_var]: printer for variables
569
*)
528
(* type_directed assignment: array vs. statically sized type - [var_type]: type
529
   of variable to be assigned - [var_name]: name of variable to be assigned -
530
   [value]: assigned value - [pp_var]: printer for variables *)
570 531
let assign_to_exprs m var_name value =
571 532
  let self = m.mname.node_id in
572 533
  let e =
573
    Z3.Boolean.mk_eq
574
      !ctx
534
    Z3.Boolean.mk_eq !ctx
575 535
      (horn_val_to_expr ~is_lhs:true m self var_name)
576 536
      (horn_val_to_expr m self value)
577
  (* was: TODO deal with array accesses       (value_suffix_to_expr self value) *)
537
    (* was: TODO deal with array accesses (value_suffix_to_expr self value) *)
578 538
  in
579
  [e]
539
  [ e ]
580 540

  
581
    
582 541
(* Convert instruction to Z3.Expr and update the set of reset instances *)
583
let rec instr_to_exprs machines reset_instances (m: machine_t) instr : Z3.Expr.expr list * ident list =
542
let rec instr_to_exprs machines reset_instances (m : machine_t) instr :
543
    Z3.Expr.expr list * ident list =
584 544
  match Corelang.get_instr_desc instr with
585
  | MComment _ -> [], reset_instances
586
  | MNoReset i -> (* we assign middle_mem with mem_m. And declare i as reset *)
587
    no_reset_to_exprs machines m i,
588
    i::reset_instances
589
  | MReset i -> (* we assign middle_mem with reset: reset(mem_m) *)
590
    instance_reset_to_exprs machines m i,
591
    i::reset_instances
592
  | MLocalAssign (i,v) ->
593
    assign_to_exprs
594
      m  
595
      (mk_val (Var i) i.var_type) v,
596
    reset_instances
597
  | MStateAssign (i,v) ->
598
    assign_to_exprs
599
      m 
600
      (mk_val (Var i) i.var_type) v,
601
    reset_instances
602
  | MStep ([_], i, vl) when Basic_library.is_internal_fun i (List.map (fun v -> v.value_type) vl) ->
545
  | MComment _ ->
546
    [], reset_instances
547
  | MNoReset i ->
548
    (* we assign middle_mem with mem_m. And declare i as reset *)
549
    no_reset_to_exprs machines m i, i :: reset_instances
550
  | MReset i ->
551
    (* we assign middle_mem with reset: reset(mem_m) *)
552
    instance_reset_to_exprs machines m i, i :: reset_instances
553
  | MLocalAssign (i, v) ->
554
    assign_to_exprs m (mk_val (Var i) i.var_type) v, reset_instances
555
  | MStateAssign (i, v) ->
556
    assign_to_exprs m (mk_val (Var i) i.var_type) v, reset_instances
557
  | MStep ([ _ ], i, vl)
558
    when Basic_library.is_internal_fun i (List.map (fun v -> v.value_type) vl)
559
    ->
603 560
    assert false (* This should not happen anymore *)
604 561
  | MStep (il, i, vl) ->
605
    (* if reset instance, just print the call over mem_m , otherwise declare mem_m =
606
       mem_c and print the call to mem_m *)
607
    instance_call_to_exprs machines reset_instances m i vl il,
608
    reset_instances (* Since this instance call will only happen once, we
609
		       don't have to update reset_instances *)
610

  
611
  | MBranch (g,hl) -> (* (g = tag1 => expr1) and (g = tag2 => expr2) ...
612
			 should not be produced yet. Later, we will have to
613
			 compare the reset_instances of each branch and
614
			 introduced the mem_m = mem_c for branches to do not
615
			 address it while other did. Am I clear ? *)
562
    (* if reset instance, just print the call over mem_m , otherwise declare
563
       mem_m = mem_c and print the call to mem_m *)
564
    instance_call_to_exprs machines reset_instances m i vl il, reset_instances
565
  (* Since this instance call will only happen once, we don't have to update
566
     reset_instances *)
567
  | MBranch (g, hl) ->
568
    (* (g = tag1 => expr1) and (g = tag2 => expr2) ... should not be produced
569
       yet. Later, we will have to compare the reset_instances of each branch
570
       and introduced the mem_m = mem_c for branches to do not address it while
571
       other did. Am I clear ? *)
616 572
    (* For each branch we obtain the logical encoding, and the information
617 573
       whether a sub node has been reset or not. If a node has been reset in one
618
       of the branch, then all others have to have the mem_m = mem_c
619
       statement. *)
574
       of the branch, then all others have to have the mem_m = mem_c statement. *)
620 575
    let self = m.mname.node_id in
621 576
    let branch_to_expr (tag, instrs) =
622
      let branch_def, branch_resets = instrs_to_expr machines reset_instances m instrs in
577
      let branch_def, branch_resets =
578
        instrs_to_expr machines reset_instances m instrs
579
      in
623 580
      let e =
624
	Z3.Boolean.mk_implies !ctx
625
          (Z3.Boolean.mk_eq !ctx 
581
        Z3.Boolean.mk_implies !ctx
582
          (Z3.Boolean.mk_eq !ctx
626 583
             (horn_val_to_expr m self g)
627
	     (horn_tag_to_expr tag))
628
          branch_def in
584
             (horn_tag_to_expr tag))
585
          branch_def
586
      in
629 587

  
630
      [e], branch_resets
631
	  
588
      [ e ], branch_resets
632 589
    in
633
    List.fold_left (fun (instrs, resets) b ->
634
      let b_instrs, b_resets = branch_to_expr b in
635
      instrs@b_instrs, resets@b_resets 
636
      ) ([], reset_instances) hl
637
  | MSpec _ -> assert false
638 590

  
639
and instrs_to_expr machines reset_instances m instrs = 
591
    List.fold_left
592
      (fun (instrs, resets) b ->
593
        let b_instrs, b_resets = branch_to_expr b in
594
        instrs @ b_instrs, resets @ b_resets)
595
      ([], reset_instances) hl
596
  | MSpec _ ->
597
    assert false
598

  
599
and instrs_to_expr machines reset_instances m instrs =
640 600
  let instr_to_exprs rs i = instr_to_exprs machines rs m i in
641
  let e_list, rs = 
601
  let e_list, rs =
642 602
    match instrs with
643
    | [x] -> instr_to_exprs reset_instances x 
644
    | _::_ -> (* TODO: check whether we should compuyte a AND on the exprs (expr list) built here. It was performed in the printer setting but seems to be useless here since the output is a list of exprs *)
645
       
646
       List.fold_left (fun (exprs, rs) i -> 
647
         let exprs_i, rs_i = instr_to_exprs rs i in
648
         exprs@exprs_i, rs@rs_i
649
       )
650
         ([], reset_instances) instrs 
651
	 
652
	 
653
    | [] -> [], reset_instances
603
    | [ x ] ->
604
      instr_to_exprs reset_instances x
605
    | _ :: _ ->
606
      (* TODO: check whether we should compuyte a AND on the exprs (expr list)
607
         built here. It was performed in the printer setting but seems to be
608
         useless here since the output is a list of exprs *)
609
      List.fold_left
610
        (fun (exprs, rs) i ->
611
          let exprs_i, rs_i = instr_to_exprs rs i in
612
          exprs @ exprs_i, rs @ rs_i)
613
        ([], reset_instances) instrs
614
    | [] ->
615
      [], reset_instances
654 616
  in
655
  let e = 
617
  let e =
656 618
    match e_list with
657
    | [e] -> e
658
    | [] -> Z3.Boolean.mk_true !ctx
659
    | _ -> Z3.Boolean.mk_and !ctx e_list
619
    | [ e ] ->
620
      e
621
    | [] ->
622
      Z3.Boolean.mk_true !ctx
623
    | _ ->
624
      Z3.Boolean.mk_and !ctx e_list
660 625
  in
661 626
  e, rs
662 627

  
663

  
664 628
(*********************************************************)
665 629

  
666 630
(* Quantifiying universally all occuring variables *)
667
let add_rule ?(dont_touch=[]) vars  expr =
631
let add_rule ?(dont_touch = []) vars expr =
668 632
  (* let fds = Z3.Expr.get_args expr in *)
669 633
  (* Format.eprintf "Expr %s: args: [%a]@." *)
670 634
  (*   (Z3.Expr.to_string expr) *)
671
  (*   (Utils.fprintf_list ~sep:", " (fun fmt e -> Format.pp_print_string fmt (Z3.Expr.to_string e))) fds; *)
635
  (* (Utils.fprintf_list ~sep:", " (fun fmt e -> Format.pp_print_string fmt
636
     (Z3.Expr.to_string e))) fds; *)
672 637

  
673 638
  (* (\* Old code relying on provided vars *\) *)
674 639
  (* let sorts = (List.map (fun id -> type_to_sort id.var_type) vars) in *)
675
  (* let symbols = (List.map (fun id -> Z3.FuncDecl.get_name (get_fdecl id.var_id)) vars) in *)
676
  
640
  (* let symbols = (List.map (fun id -> Z3.FuncDecl.get_name (get_fdecl
641
     id.var_id)) vars) in *)
642

  
677 643
  (* New code: we extract vars from expr *)
678 644
  let module FDSet = Set.Make (struct
679
      type t = Z3.FuncDecl.func_decl
680
	  let compare = compare
681
	  (* let hash = Hashtbl.hash *)
682
    end)
683
  in
684
(* Fonction seems unused 
685

  
686
  let rec get_expr_vars e =
687
    let open Utils in
688
    let nb_args = Z3.Expr.get_num_args e in
689
    if nb_args <= 0 then (
690
      let fdecl = Z3.Expr.get_func_decl e in
691
      (* let params = Z3.FuncDecl.get_parameters fdecl in *)
692
      (* Format.eprintf "Extracting info about %s: @." (Z3.Expr.to_string e); *)
693
      let dkind = Z3.FuncDecl.get_decl_kind fdecl in
694
      match dkind with Z3enums.OP_UNINTERPRETED -> (
695
	(* Format.eprintf "kind = %s, " (match dkind with Z3enums.OP_TRUE -> "true" | Z3enums.OP_UNINTERPRETED -> "uninter"); *)
696
	(* let open Z3.FuncDecl.Parameter in *)
697
	(* List.iter (fun p -> *)
698
	(*   match p with *)
699
        (*     P_Int i -> Format.eprintf "int %i" i *)
700
	(*   | P_Dbl f -> Format.eprintf "dbl %f" f *)
701
	(*   | P_Sym s -> Format.eprintf "symb"  *)
702
	(*   | P_Srt s -> Format.eprintf "sort"  *)
703
	(*   | P_Ast _ ->Format.eprintf "ast"  *)
704
	(*   | P_Fdl f -> Format.eprintf "fundecl"  *)
705
	(*   | P_Rat s -> Format.eprintf "rat %s" s  *)
706
	     
707
	(* ) params; *)
708
	(* Format.eprintf "]@."; *)
709
	FDSet.singleton fdecl
710
      )
711
      | _ -> FDSet.empty
712
    )
713
    else (*if nb_args > 0 then*)
714
      List.fold_left
715
	(fun accu e ->  FDSet.union accu (get_expr_vars e))
716
	FDSet.empty (Z3.Expr.get_args e)
717
  in
718
 *)
719
  (* Unsed variable. Coul;d be reintroduced 
720
  let extracted_vars = FDSet.elements (FDSet.diff (get_expr_vars expr) (FDSet.of_list dont_touch)) in
721
  let extracted_sorts = List.map Z3.FuncDecl.get_range extracted_vars in
722
  let extracted_symbols = List.map Z3.FuncDecl.get_name extracted_vars in
723
   *)
724
  if !debug then (
645
    type t = Z3.FuncDecl.func_decl
646

  
647
    let compare = compare
648
    (* let hash = Hashtbl.hash *)
649
  end) in
650
  (* Fonction seems unused
651

  
652
     let rec get_expr_vars e = let open Utils in let nb_args =
653
     Z3.Expr.get_num_args e in if nb_args <= 0 then ( let fdecl =
654
     Z3.Expr.get_func_decl e in (* let params = Z3.FuncDecl.get_parameters fdecl
655
     in *) (* Format.eprintf "Extracting info about %s: @." (Z3.Expr.to_string
656
     e); *) let dkind = Z3.FuncDecl.get_decl_kind fdecl in match dkind with
657
     Z3enums.OP_UNINTERPRETED -> ( (* Format.eprintf "kind = %s, " (match dkind
658
     with Z3enums.OP_TRUE -> "true" | Z3enums.OP_UNINTERPRETED -> "uninter"); *)
659
     (* let open Z3.FuncDecl.Parameter in *) (* List.iter (fun p -> *) (* match
660
     p with *) (* P_Int i -> Format.eprintf "int %i" i *) (* | P_Dbl f ->
661
     Format.eprintf "dbl %f" f *) (* | P_Sym s -> Format.eprintf "symb" *) (* |
662
     P_Srt s -> Format.eprintf "sort" *) (* | P_Ast _ ->Format.eprintf "ast" *)
663
     (* | P_Fdl f -> Format.eprintf "fundecl" *) (* | P_Rat s -> Format.eprintf
664
     "rat %s" s *)
665

  
666
     (* ) params; *) (* Format.eprintf "]@."; *) FDSet.singleton fdecl ) | _ ->
667
     FDSet.empty ) else (*if nb_args > 0 then*) List.fold_left (fun accu e ->
668
     FDSet.union accu (get_expr_vars e)) FDSet.empty (Z3.Expr.get_args e) in *)
669
  (* Unsed variable. Coul;d be reintroduced let extracted_vars = FDSet.elements
670
     (FDSet.diff (get_expr_vars expr) (FDSet.of_list dont_touch)) in let
671
     extracted_sorts = List.map Z3.FuncDecl.get_range extracted_vars in let
672
     extracted_symbols = List.map Z3.FuncDecl.get_name extracted_vars in *)
673
  if !debug then
725 674
    Format.eprintf "Declaring rule: %s with variables @[<v 0>@ [%a@ ]@]@ @."
726 675
      (Z3.Expr.to_string expr)
727
      (Utils.fprintf_list ~sep:",@ " (fun fmt e -> Format.fprintf fmt "%s" (Z3.Expr.to_string e))) (List.map horn_var_to_expr vars)
728
  )
729
    ;
730
  let expr = Z3.Quantifier.mk_forall_const
731
    !ctx  (* context *)
732
    (List.map horn_var_to_expr vars) (* TODO provide bounded variables as expr *)
733
    (* sorts           (\* sort list*\) *)
734
    (* symbols (\* symbol list *\) *)
735
    expr (* expression *)
736
    None (* quantifier weight, None means 1 *)
737
    [] (* pattern list ? *)
738
    [] (* ? *)
739
    None (* ? *)
740
    None (* ? *)
676
      (Utils.fprintf_list ~sep:",@ " (fun fmt e ->
677
           Format.fprintf fmt "%s" (Z3.Expr.to_string e)))
678
      (List.map horn_var_to_expr vars);
679
  let expr =
680
    Z3.Quantifier.mk_forall_const !ctx
681
      (* context *)
682
      (List.map horn_var_to_expr vars)
683
      (* TODO provide bounded variables as expr *)
684
      (* sorts           (\* sort list*\) *)
685
      (* symbols (\* symbol list *\) *)
686
      expr (* expression *) None (* quantifier weight, None means 1 *) []
687
      (* pattern list ? *) [] (* ? *) None (* ? *) None
688
    (* ? *)
741 689
  in
690

  
742 691
  (* Format.eprintf "OK@.@?"; *)
743 692

  
744
  (*
745
    TODO: bizarre la declaration de INIT tout seul semble poser pb.
746
  *) 
747
  Z3.Fixedpoint.add_rule !fp
748
    (Z3.Quantifier.expr_of_quantifier expr)
749
    None
693
  (* TODO: bizarre la declaration de INIT tout seul semble poser pb. *)
694
  Z3.Fixedpoint.add_rule !fp (Z3.Quantifier.expr_of_quantifier expr) None
750 695

  
751
 
752 696
(********************************************************)
753
    
697

  
754 698
let machine_reset machines m =
755 699
  let locals = local_memory_vars m in
756
  
700

  
757 701
  (* print "x_m = x_c" for each local memory *)
758 702
  let mid_mem_def =
759
    List.map (fun v ->
760
      Z3.Boolean.mk_eq !ctx
761
	(horn_var_to_expr (rename_mid v))
762
	(horn_var_to_expr (rename_current v))
763
    ) locals
703
    List.map
704
      (fun v ->
705
        Z3.Boolean.mk_eq !ctx
706
          (horn_var_to_expr (rename_mid v))
707
          (horn_var_to_expr (rename_current v)))
708
      locals
764 709
  in
765 710

  
766
  (* print "child_reset ( associated vars _ {c,m} )" for each subnode.
767
     Special treatment for _arrow: _first = true
768
  *)
769

  
711
  (* print "child_reset ( associated vars _ {c,m} )" for each subnode. Special
712
     treatment for _arrow: _first = true *)
770 713
  let reset_instances =
771
    
772
    List.map (fun (id, (n, _)) ->
773
      let name = node_name n in
774
      if name = "_arrow" then (
775
	Z3.Boolean.mk_eq !ctx
776
	  (
777
	    let vdecl = get_fdecl ((concat m.mname.node_id id) ^ "._arrow._first_m") in
778
	    Z3.Expr.mk_const_f !ctx vdecl
779
	  )
780
	  (Z3.Boolean.mk_true !ctx)
781
	  
782
      ) else (
783
	let machine_n = get_machine machines name in 
784
	
785
	Z3.Expr.mk_app
786
	  !ctx
787
	  (get_fdecl (name ^ "_reset"))
788
	  (List.map (horn_var_to_expr)
789
	     (idx::uid:: (* Additional vars: counters, uid *)
790
	      	(rename_machine_list (concat m.mname.node_id id) (reset_vars machines machine_n))
791
	  ))
792
	  
793
      )
794
    ) m.minstances
795
      
796
      
714
    List.map
715
      (fun (id, (n, _)) ->
716
        let name = node_name n in
717
        if name = "_arrow" then
718
          Z3.Boolean.mk_eq !ctx
719
            (let vdecl =
720
               get_fdecl (concat m.mname.node_id id ^ "._arrow._first_m")
721
             in
722
             Z3.Expr.mk_const_f !ctx vdecl)
723
            (Z3.Boolean.mk_true !ctx)
724
        else
725
          let machine_n = get_machine machines name in
726

  
727
          Z3.Expr.mk_app !ctx
728
            (get_fdecl (name ^ "_reset"))
729
            (List.map horn_var_to_expr
730
               (idx
731
                ::
732
                uid
733
                ::
734
                (* Additional vars: counters, uid *)
735
                rename_machine_list
736
                  (concat m.mname.node_id id)
737
                  (reset_vars machines machine_n))))
738
      m.minstances
797 739
  in
798
  
740

  
799 741
  Z3.Boolean.mk_and !ctx (mid_mem_def @ reset_instances)
800
    
801
        
802 742

  
803
(*  TODO: empty list means true statement *)
743
(* TODO: empty list means true statement *)
804 744
let decl_machine machines m =
805
  if m.mname.node_id = Arrow.arrow_id then
806
    (* We don't do arrow function *)
745
  if m.mname.node_id = Arrow.arrow_id then (* We don't do arrow function *)
807 746
    ()
808 747
  else
809
    begin
810
      let _ =
811
        List.map decl_var
812
      	  (
813
      	    (inout_vars m)@
814
      	      (rename_current_list (full_memory_vars machines m)) @
815
      	      (rename_mid_list (full_memory_vars machines m)) @
816
      	      (rename_next_list (full_memory_vars machines m)) @
817
      	      (rename_machine_list m.mname.node_id m.mstep.step_locals)
818
      	  )
748
    let _ =
749
      List.map decl_var
750
        (inout_vars m
751
        @ rename_current_list (full_memory_vars machines m)
752
        @ rename_mid_list (full_memory_vars machines m)
753
        @ rename_next_list (full_memory_vars machines m)
754
        @ rename_machine_list m.mname.node_id m.mstep.step_locals)
755
    in
756
    if is_stateless m then (
757
      if !debug then
758
        Format.eprintf "Declaring a stateless machine: %s@." m.mname.node_id;
759

  
760
      (* Declaring single predicate *)
761
      let vars = inout_vars m in
762
      let vars_types = List.map (fun v -> type_to_sort v.var_type) vars in
763
      let _ = decl_rel (machine_stateless_name m.mname.node_id) vars_types in
764

  
765
      let horn_body, _ (* don't care for reset here *) =
766
        instrs_to_expr machines [] (* No reset info for stateless nodes *) m
767
          m.mstep.step_instrs
768
      in
769
      let horn_head =
770
        Z3.Expr.mk_app !ctx
771
          (get_fdecl (machine_stateless_name m.mname.node_id))
772
          (List.map horn_var_to_expr
773
             (idx :: uid :: (* Additional vars: counters, uid *)
774
                            vars))
775
      in
776
      (* this line seems useless *)
777
      let vars =
778
        idx :: uid :: vars
779
        @ rename_machine_list m.mname.node_id m.mstep.step_locals
780
      in
781
      (* Format.eprintf "useless Vars: %a@." (Utils.fprintf_list ~sep:"@ "
782
         Printers.pp_var) vars; *)
783
      match m.mstep.step_asserts with
784
      | [] ->
785
        (* Rule for single predicate : "; Stateless step rule @." *)
786
        (*let vars = rename_machine_list m.mname.node_id m.mstep.step_locals in*)
787
        (* TODO clean code *)
788
        (* Format.eprintf "used Vars: %a@." (Utils.fprintf_list ~sep:"@ "
789
           Printers.pp_var) vars; *)
790
        add_rule vars (Z3.Boolean.mk_implies !ctx horn_body horn_head)
791
      | assertsl ->
792
        (*Rule for step "; Stateless step rule with Assertions @.";*)
793
        let body_with_asserts =
794
          Z3.Boolean.mk_and !ctx
795
            (horn_body :: List.map (horn_val_to_expr m m.mname.node_id) assertsl)
796
        in
797
        let vars = rename_machine_list m.mname.node_id m.mstep.step_locals in
798
        add_rule vars (Z3.Boolean.mk_implies !ctx body_with_asserts horn_head))
799
    else
800
      (* Rule for reset *)
801
      let vars = reset_vars machines m in
802
      let vars_types = List.map (fun v -> type_to_sort v.var_type) vars in
803
      let _ = decl_rel (machine_reset_name m.mname.node_id) vars_types in
804
      let horn_reset_body = machine_reset machines m in
805
      let horn_reset_head =
806
        Z3.Expr.mk_app !ctx
807
          (get_fdecl (machine_reset_name m.mname.node_id))
808
          (List.map horn_var_to_expr
809
             (idx :: uid :: (* Additional vars: counters, uid *)
810
                            vars))
819 811
      in
820
      if is_stateless m then
821
	begin
822
	  if !debug then 
823
	    Format.eprintf "Declaring a stateless machine: %s@." m.mname.node_id;
824

  
825
	  (* Declaring single predicate *)
826
	  let vars = inout_vars m in
827
	  let vars_types = List.map (fun v -> type_to_sort v.var_type) vars in
828
	  let _ = decl_rel (machine_stateless_name m.mname.node_id) vars_types in
829
	  
830
	  let horn_body, _ (* don't care for reset here *) =
831
	    instrs_to_expr
832
	      machines
833
	      ([] (* No reset info for stateless nodes *) )
834
	      m
835
	      m.mstep.step_instrs
836
	  in
837
	  let horn_head = 
838
	    Z3.Expr.mk_app
839
	      !ctx
840
	      (get_fdecl (machine_stateless_name m.mname.node_id))
841
	      (	List.map (horn_var_to_expr) (idx::uid:: (* Additional vars: counters, uid *) vars))
842
	  in
843
	  (* this line seems useless *)
844
	  let vars = idx::uid::vars@(rename_machine_list m.mname.node_id m.mstep.step_locals) in
845
	  (* Format.eprintf "useless Vars: %a@." (Utils.fprintf_list ~sep:"@ " Printers.pp_var) vars; *)
846
	  match m.mstep.step_asserts with
847
	  | [] ->
848
	     begin
849
	       (* Rule for single predicate : "; Stateless step rule @." *)
850
	       (*let vars = rename_machine_list m.mname.node_id m.mstep.step_locals in*)
851
	       (* TODO clean code *)
852
	       (* Format.eprintf "used Vars: %a@." (Utils.fprintf_list ~sep:"@ " Printers.pp_var) vars; *)
853
	       add_rule vars (Z3.Boolean.mk_implies !ctx horn_body horn_head)
854
		 
855
	     end
856
	  | assertsl ->
857
	     begin
858
	       (*Rule for step "; Stateless step rule with Assertions @.";*)
859
	       let body_with_asserts =
860
		 Z3.Boolean.mk_and !ctx (horn_body :: List.map (horn_val_to_expr m m.mname.node_id) assertsl)
861
	       in
862
	       let vars = rename_machine_list m.mname.node_id m.mstep.step_locals in
863
	       add_rule vars (Z3.Boolean.mk_implies !ctx body_with_asserts horn_head)
864
	     end
865
	end
866
      else
867
	begin
868

  
869
	  (* Rule for reset *)
870

  
871
	  let vars = reset_vars machines m in
872
	  let vars_types = List.map (fun v -> type_to_sort v.var_type) vars in
873
	  let _ = decl_rel (machine_reset_name m.mname.node_id) vars_types in
874
	  let horn_reset_body = machine_reset machines m in	    
875
	  let horn_reset_head = 
876
	    Z3.Expr.mk_app
877
	      !ctx
878
	      (get_fdecl (machine_reset_name m.mname.node_id))
879
	      (	List.map (horn_var_to_expr) (idx::uid:: (* Additional vars: counters, uid *) vars))
880
	  in
881

  
882
	  
883
	  let _ =
884
	    add_rule (idx::uid::vars) (Z3.Boolean.mk_implies !ctx horn_reset_body horn_reset_head)
885
	      
886
	  in
887

  
888
	  (* Rule for step*)
889
	  let vars = step_vars machines m in
890
  	  let vars_types = List.map (fun v -> type_to_sort v.var_type) vars in
891
          let _ = decl_rel (machine_step_name m.mname.node_id) vars_types in
892
	  let horn_step_body, _ (* don't care for reset here *) =
893
	    instrs_to_expr
894
	      machines
895
	      []
896
	      m
897
	      m.mstep.step_instrs
898
	  in
899
	  let horn_step_head = 
900
	    Z3.Expr.mk_app
901
	      !ctx
902
	      (get_fdecl (machine_step_name m.mname.node_id))
903
	      (	List.map (horn_var_to_expr) (idx::uid:: (* Additional vars: counters, uid *) vars))
904
	  in
905
	  match m.mstep.step_asserts with
906
	  | [] ->
907
	     begin
908
	       (* Rule for single predicate *) 
909
	       let vars = (step_vars_c_m_x machines m) @(rename_machine_list m.mname.node_id m.mstep.step_locals) in
910
	       add_rule (idx::uid::vars) (Z3.Boolean.mk_implies !ctx horn_step_body horn_step_head)
911
		 
912
	     end
913
	  | assertsl ->
914
	     begin
915
	       (* Rule for step Assertions @.; *)
916
	       let body_with_asserts =
917
		 Z3.Boolean.mk_and !ctx
918
		   (horn_step_body :: List.map (horn_val_to_expr m m.mname.node_id) assertsl)
919
	       in
920
	       let vars = (step_vars_c_m_x machines m) @(rename_machine_list m.mname.node_id m.mstep.step_locals) in
921
	       add_rule (idx::uid::vars) (Z3.Boolean.mk_implies !ctx body_with_asserts horn_step_head)
922
		 
923
	     end
924
     	       
925
	end
926
    end
... This diff was truncated because it exceeds the maximum size that can be displayed.

Also available in: Unified diff