Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / tools / zustre / zustre_common.ml @ 04a188ec

History | View | Annotate | Download (29.5 KB)

1
open Lustre_types
2
open Machine_code_types
3
open Machine_code_common
4
open Format
5
(* open Horn_backend_common
6
 * open Horn_backend *)
7
open Zustre_data
8

    
9
module HBC = Horn_backend_common
10
let node_name = HBC.node_name
11

    
12
let concat = HBC.concat
13

    
14
let rename_machine = HBC.rename_machine
15
let rename_machine_list = HBC.rename_machine_list
16

    
17
let rename_next = HBC.rename_next
18
let rename_mid = HBC.rename_mid
19
let rename_current = HBC.rename_current
20

    
21
let rename_current_list = HBC.rename_current_list
22
let rename_mid_list = HBC.rename_mid_list
23
let rename_next_list = HBC.rename_next_list
24

    
25
let full_memory_vars = HBC.full_memory_vars
26
let inout_vars = HBC.inout_vars
27
let reset_vars = HBC.reset_vars
28
let step_vars = HBC.step_vars
29
let local_memory_vars = HBC.local_memory_vars
30
let step_vars_m_x = HBC.step_vars_m_x
31
let step_vars_c_m_x = HBC.step_vars_c_m_x
32
  
33
let machine_reset_name = HBC.machine_reset_name 
34
let machine_step_name = HBC.machine_step_name 
35
let machine_stateless_name = HBC.machine_stateless_name 
36

    
37
let preprocess = Horn_backend.preprocess
38
  
39

    
40
exception UnknownFunction of (string * (Format.formatter -> unit))
41
(** Sorts
42

    
43
A sort is introduced for each basic type and each enumerated type.
44

    
45
A hashtbl records these and allow easy access to sort values, when
46
   provided with a enumerated type name. 
47

    
48
*)
49
        
50
let bool_sort = Z3.Boolean.mk_sort !ctx
51
let int_sort = Z3.Arithmetic.Integer.mk_sort !ctx
52
let real_sort = Z3.Arithmetic.Real.mk_sort !ctx
53

    
54

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

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

    
80
                 
81
let rec type_to_sort t =
82
  if Types.is_bool_type t  then bool_sort else
83
    if Types.is_int_type t then int_sort else 
84
  if Types.is_real_type t then real_sort else 
85
  match (Types.repr t).Types.tdesc with
86
  | Types.Tconst ty       -> get_const_sort ty
87
  | Types.Tclock t        -> type_to_sort t
88
  | Types.Tarray(dim,ty)   -> Z3.Z3Array.mk_sort !ctx int_sort (type_to_sort ty)
89
  | Types.Tstatic(d, ty)-> type_to_sort ty
90
  | Types.Tarrow _
91
  | _                     -> Format.eprintf "internal error: pp_type %a@."
92
                               Types.print_ty t; assert false
93

    
94

    
95
(* let idx_var = *)
96
(*   Z3.FuncDecl.mk_func_decl_s !ctx "__idx__" [] idx_sort  *)
97
    
98
(* let uid_var = *)
99
(*   Z3.FuncDecl.mk_func_decl_s !ctx "__uid__" [] uid_sort  *)
100

    
101
(** Func decls
102

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

    
107

    
108

    
109
*)
110
let register_fdecl id fd = Hashtbl.add decls id fd
111
let get_fdecl id =
112
  try
113
    Hashtbl.find decls id
114
  with Not_found -> (Format.eprintf "Unable to find func_decl %s@.@?" id; raise Not_found)
115

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

    
120
    
121
let decl_var id =
122
  (* Format.eprintf "Declaring var %s@." id.var_id; *)
123
  let fdecl = Z3.FuncDecl.mk_func_decl_s !ctx id.var_id [] (type_to_sort id.var_type) in
124
  register_fdecl id.var_id fdecl;
125
  fdecl
126

    
127
let idx_sort = int_sort
128
let uid_sort = Z3.Z3List.mk_sort !ctx (Z3.Symbol.mk_string !ctx "uid_list") int_sort
129
let uid_conc = 
130
  let fd = Z3.Z3List.get_cons_decl uid_sort in
131
  fun head tail -> Z3.FuncDecl.apply fd [head;tail]
132

    
133
let get_instance_uid =
134
  let hash : (string, int) Hashtbl.t = Hashtbl.create 13 in
135
  let cpt = ref 0 in
136
  fun i ->
137
    let id =
138
      if Hashtbl.mem hash i then
139
	Hashtbl.find hash i
140
      else (
141
	incr cpt;
142
	Hashtbl.add hash i !cpt;
143
	!cpt
144
      )
145
    in
146
    Z3.Arithmetic.Integer.mk_numeral_i !ctx id
147
  
148

    
149
  
150
let decl_rel ?(no_additional_vars=false) name args_sorts =
151
  (* Enriching arg_sorts with two new variables: a counting index and an
152
     uid *)
153
  let args_sorts =
154
    if no_additional_vars then args_sorts else idx_sort::uid_sort::args_sorts in
155
  
156
  (* let args_sorts = List.map (fun v -> type_to_sort v.var_type) args in *)
157
  if !debug then
158
    Format.eprintf "Registering fdecl %s (%a)@."
159
      name
160
      (Utils.fprintf_list ~sep:"@ "
161
	 (fun fmt sort -> Format.fprintf fmt "%s" (Z3.Sort.to_string sort)))
162
      args_sorts
163
  ;
164
  let fdecl = Z3.FuncDecl.mk_func_decl_s !ctx name args_sorts bool_sort in
165
  Z3.Fixedpoint.register_relation !fp fdecl;
166
  register_fdecl name fdecl;
167
  fdecl
168
  
169

    
170

    
171
(* Shared variables to describe counter and uid *)
172

    
173
let idx = Corelang.dummy_var_decl "__idx__" Type_predef.type_int
174
let idx_var = Z3.Expr.mk_const_f !ctx (decl_var idx) 
175
let uid = Corelang.dummy_var_decl "__uid__" Type_predef.type_int
176
let uid_fd = Z3.FuncDecl.mk_func_decl_s !ctx "__uid__" [] uid_sort 
177
let _ = register_fdecl "__uid__"  uid_fd  
178
let uid_var = Z3.Expr.mk_const_f !ctx uid_fd 
179

    
180
(** Conversion functions
181

    
182
    The following is similar to the Horn backend. Each printing function is
183
    rephrased from pp_xx to xx_to_expr and produces a Z3 value.
184

    
185
*)
186

    
187

    
188
(* Returns the f_decl associated to the variable v *)
189
let horn_var_to_expr v =
190
  Z3.Expr.mk_const_f !ctx (get_fdecl v.var_id)
191

    
192

    
193

    
194

    
195
  (* Used to print boolean constants *)
196
let horn_tag_to_expr t =
197
  if t = tag_true then
198
    Z3.Boolean.mk_true !ctx
199
  else if t = tag_false then
200
    Z3.Boolean.mk_false !ctx
201
  else
202
    (* Finding the associated sort *)
203
    let sort = get_tag_sort t in
204
    let elems = get_sort_elems sort in 
205
    let res : Z3.Expr.expr option =
206
      List.fold_left2 (fun res cst expr ->
207
          match res with
208
          | Some _ -> res
209
          | None -> if t = cst then Some (expr:Z3.Expr.expr) else None
210
        ) None elems (Z3.Enumeration.get_consts sort)
211
    in
212
    match res with None -> assert false | Some s -> s
213
    
214
(* Prints a constant value *)
215
let rec horn_const_to_expr c =
216
  match c with
217
    | Const_int i    -> Z3.Arithmetic.Integer.mk_numeral_i !ctx i
218
    | Const_real r  -> Z3.Arithmetic.Real.mk_numeral_s !ctx (Real.to_string r)
219
    | Const_tag t    -> horn_tag_to_expr t
220
    | _              -> assert false
221

    
222

    
223

    
224
(* Default value for each type, used when building arrays. Eg integer array
225
   [2;7] is defined as (store (store (0) 1 7) 0 2) where 0 is this default value
226
   for the type integer (arrays).
227
*)
228
let rec horn_default_val t =
229
  let t = Types.dynamic_type t in
230
  if Types.is_bool_type t  then Z3.Boolean.mk_true !ctx else
231
  if Types.is_int_type t then Z3.Arithmetic.Integer.mk_numeral_i !ctx 0 else 
232
  if Types.is_real_type t then Z3.Arithmetic.Real.mk_numeral_i !ctx 0 else 
233
  (* match (Types.dynamic_type t).Types.tdesc with
234
   * | Types.Tarray(dim, l) -> (\* TODO PL: this strange code has to be (heavily) checked *\)
235
   *    let valt = Types.array_element_type t in
236
   *    fprintf fmt "((as const (Array Int %a)) %a)"
237
   *      pp_type valt 
238
   *      pp_default_val valt
239
   * | Types.Tstruct(l) -> assert false
240
   * | Types.Ttuple(l) -> assert false
241
   * |_ -> *) assert false
242

    
243
(* Conversion of basic library functions *)
244
    
245
let horn_basic_app i val_to_expr vl =
246
  match i, vl with
247
  | "ite", [v1; v2; v3] ->
248
     Z3.Boolean.mk_ite
249
       !ctx
250
       (val_to_expr v1)
251
       (val_to_expr v2)
252
       (val_to_expr v3)
253

    
254
  | "uminus", [v] ->
255
     Z3.Arithmetic.mk_unary_minus
256
       !ctx
257
       (val_to_expr v)
258
  | "not", [v] ->
259
     Z3.Boolean.mk_not
260
       !ctx
261
       (val_to_expr v)
262
  | "=", [v1; v2] ->
263
     Z3.Boolean.mk_eq
264
       !ctx
265
       (val_to_expr v1)
266
       (val_to_expr v2)
267
  | "&&", [v1; v2] ->
268
     Z3.Boolean.mk_and
269
       !ctx
270
       [val_to_expr v1;
271
        val_to_expr v2]
272
  | "||", [v1; v2] ->
273
          Z3.Boolean.mk_or
274
       !ctx
275
       [val_to_expr v1;
276
        val_to_expr v2]
277

    
278
  | "impl", [v1; v2] ->
279
     Z3.Boolean.mk_implies
280
       !ctx
281
       (val_to_expr v1)
282
       (val_to_expr v2)
283
 | "mod", [v1; v2] ->
284
          Z3.Arithmetic.Integer.mk_mod
285
       !ctx
286
       (val_to_expr v1)
287
       (val_to_expr v2)
288
  | "equi", [v1; v2] ->
289
          Z3.Boolean.mk_eq
290
       !ctx
291
       (val_to_expr v1)
292
       (val_to_expr v2)
293
  | "xor", [v1; v2] ->
294
          Z3.Boolean.mk_xor
295
       !ctx
296
       (val_to_expr v1)
297
       (val_to_expr v2)
298
  | "!=", [v1; v2] ->
299
     Z3.Boolean.mk_not
300
       !ctx
301
       (
302
         Z3.Boolean.mk_eq
303
           !ctx
304
           (val_to_expr v1)
305
           (val_to_expr v2)
306
       )
307
  | "/", [v1; v2] ->
308
     Z3.Arithmetic.mk_div
309
       !ctx
310
       (val_to_expr v1)
311
       (val_to_expr v2)
312

    
313
  | "+", [v1; v2] ->
314
     Z3.Arithmetic.mk_add
315
       !ctx
316
       [val_to_expr v1; val_to_expr v2]
317

    
318
  | "-", [v1; v2] ->
319
     Z3.Arithmetic.mk_sub
320
       !ctx
321
       [val_to_expr v1 ; val_to_expr v2]
322
       
323
  | "*", [v1; v2] ->
324
     Z3.Arithmetic.mk_mul
325
       !ctx
326
       [val_to_expr v1; val_to_expr v2]
327

    
328

    
329
  | "<", [v1; v2] ->
330
     Z3.Arithmetic.mk_lt
331
       !ctx
332
       (val_to_expr v1)
333
       (val_to_expr v2)
334

    
335
  | "<=", [v1; v2] ->
336
     Z3.Arithmetic.mk_le
337
       !ctx
338
       (val_to_expr v1)
339
       (val_to_expr v2)
340

    
341
  | ">", [v1; v2] ->
342
     Z3.Arithmetic.mk_gt
343
       !ctx
344
       (val_to_expr v1)
345
       (val_to_expr v2)
346

    
347
  | ">=", [v1; v2] ->
348
     Z3.Arithmetic.mk_ge
349
       !ctx
350
       (val_to_expr v1)
351
       (val_to_expr v2)
352

    
353
  | "int_to_real", [v1] ->
354
     Z3.Arithmetic.Integer.mk_int2real
355
       !ctx
356
       (val_to_expr v1)
357

    
358
    
359
  (* | _, [v1; v2] ->      Z3.Boolean.mk_and
360
   *      !ctx
361
   *      (val_to_expr v1)
362
   *      (val_to_expr v2)
363
   * 
364
   *      Format.fprintf fmt "(%s %a %a)" i val_to_exprr v1 val_to_expr v2 *)
365
  | _ -> (
366
    let msg fmt = Format.fprintf fmt
367
                    "internal error: zustre unkown function %s (nb args = %i)@."
368
                    i (List.length vl)
369
    in
370
    raise (UnknownFunction(i, msg))
371
  )
372

    
373
           
374
(* Convert a value expression [v], with internal function calls only.  [pp_var]
375
   is a printer for variables (typically [pp_c_var_read]), but an offset suffix
376
   may be added for array variables
377
*)
378
let rec horn_val_to_expr ?(is_lhs=false) m self v =
379
  match v.value_desc with
380
  | Cst c       -> horn_const_to_expr c
381

    
382
  (* Code specific for arrays *)
383
  | Array il    ->
384
     (* An array definition: 
385
	(store (
386
	  ...
387
 	    (store (
388
	       store (
389
	          default_val
390
	       ) 
391
	       idx_n val_n
392
	    ) 
393
	    idx_n-1 val_n-1)
394
	  ... 
395
	  idx_1 val_1
396
	) *)
397
     let rec build_array (tab, x) =
398
       match tab with
399
       | [] -> horn_default_val v.value_type(* (get_type v) *)
400
       | h::t ->
401
	  Z3.Z3Array.mk_store
402
            !ctx
403
	    (build_array (t, (x+1)))
404
	    (Z3.Arithmetic.Integer.mk_numeral_i !ctx x)
405
	    (horn_val_to_expr ~is_lhs:is_lhs m self h)
406
     in
407
     build_array (il, 0)
408
     
409
  | Access(tab,index) ->
410
     Z3.Z3Array.mk_select !ctx 
411
       (horn_val_to_expr ~is_lhs:is_lhs m self tab)
412
       (horn_val_to_expr ~is_lhs:is_lhs m self index)
413

    
414
  (* Code specific for arrays *)
415
    
416
  | Power (v, n)  -> assert false
417
  | Var v    ->
418
     if is_memory m v then
419
       if Types.is_array_type v.var_type
420
       then assert false
421
       else horn_var_to_expr (rename_machine self ((if is_lhs then rename_next else rename_current) (* self *) v))
422
     
423
     else 
424
       horn_var_to_expr
425
         (rename_machine
426
            self
427
            v)
428
  | Fun (n, vl)   -> horn_basic_app n (horn_val_to_expr m self) vl
429

    
430
let no_reset_to_exprs machines m i =
431
  let (n,_) = List.assoc i m.minstances in
432
  let target_machine = List.find (fun m  -> m.mname.node_id = (Corelang.node_name n)) machines in
433

    
434
  let m_list = 
435
    rename_machine_list
436
      (concat m.mname.node_id i)
437
      (rename_mid_list (full_memory_vars machines target_machine))
438
  in
439
  let c_list =
440
    rename_machine_list
441
      (concat m.mname.node_id i)
442
      (rename_current_list (full_memory_vars machines target_machine))
443
  in
444
  match c_list, m_list with
445
  | [chd], [mhd] ->
446
     let expr =
447
       Z3.Boolean.mk_eq !ctx 
448
         (horn_var_to_expr mhd)
449
         (horn_var_to_expr chd)
450
     in
451
     [expr]
452
  | _ -> (
453
    let exprs =
454
      List.map2 (fun mhd chd -> 
455
          Z3.Boolean.mk_eq !ctx 
456
            (horn_var_to_expr mhd)
457
            (horn_var_to_expr chd)
458
        )
459
        m_list
460
        c_list
461
    in
462
    exprs
463
  )
464

    
465
let instance_reset_to_exprs machines m i =
466
  let (n,_) = List.assoc i m.minstances in
467
  let target_machine = List.find (fun m  -> m.mname.node_id = (Corelang.node_name n)) machines in
468
  let vars =
469
    (rename_machine_list
470
       (concat m.mname.node_id i)
471
       (rename_current_list (full_memory_vars machines target_machine))@  (rename_mid_list (full_memory_vars machines target_machine))
472
    )
473
    
474
  in
475
  let expr =
476
    Z3.Expr.mk_app
477
      !ctx
478
      (get_fdecl (machine_reset_name (Corelang.node_name n)))
479
      (List.map (horn_var_to_expr) (idx::uid::vars))
480
  in
481
  [expr]
482

    
483
let instance_call_to_exprs machines reset_instances m i inputs outputs =
484
  let self = m.mname.node_id in
485

    
486
  (* Building call args *)
487
  let idx_uid_inout =
488
    (* Additional input to register step counters, and uid *)
489
    let idx = horn_var_to_expr idx in
490
    let uid = uid_conc (get_instance_uid i) (horn_var_to_expr uid) in
491
    let inout = 
492
      List.map (horn_val_to_expr m self)
493
	(inputs @ (List.map (fun v -> mk_val (Var v) v.var_type) outputs))
494
    in
495
    idx::uid::inout
496
  in
497
    
498
  try (* stateful node instance *)
499
    begin
500
      let (n,_) = List.assoc i m.minstances in
501
      let target_machine = List.find (fun m  -> m.mname.node_id = Corelang.node_name n) machines in
502

    
503
      (* Checking whether this specific instances has been reset yet *)
504
      let reset_exprs = 
505
        if not (List.mem i reset_instances) then
506
	  (* If not, declare mem_m = mem_c *)
507
	  no_reset_to_exprs machines m i
508
        else
509
          [] (* Nothing to add yet *)
510
      in
511
      
512
      let mems = full_memory_vars machines target_machine in
513
      let rename_mems f = rename_machine_list (concat m.mname.node_id i) (f mems) in
514
      let mid_mems = rename_mems rename_mid_list in
515
      let next_mems = rename_mems rename_next_list in
516

    
517
      let call_expr = 
518
	match Corelang.node_name n, inputs, outputs, mid_mems, next_mems with
519
	| "_arrow", [i1; i2], [o], [mem_m], [mem_x] -> begin
520
          let stmt1 = (* out = ite mem_m then i1 else i2 *)
521
            Z3.Boolean.mk_eq !ctx
522
              ( (* output var *)
523
                horn_val_to_expr 
524
                  ~is_lhs:true
525
                  m self
526
                  (mk_val (Var o) o.var_type)
527
              )
528
              (
529
                Z3.Boolean.mk_ite !ctx 
530
	          (horn_var_to_expr mem_m) 
531
	          (horn_val_to_expr m self i1)
532
	          (horn_val_to_expr m self i2)
533
              )
534
          in
535
          let stmt2 = (* mem_X = false *)
536
            Z3.Boolean.mk_eq !ctx
537
	      (horn_var_to_expr mem_x)
538
              (Z3.Boolean.mk_false !ctx)
539
          in
540
          [stmt1; stmt2]
541
	end
542

    
543
	| node_name_n ->
544
           let expr = 
545
             Z3.Expr.mk_app
546
               !ctx
547
               (get_fdecl (machine_step_name (node_name n)))
548
               ( (* Arguments are input, output, mid_mems, next_mems *)
549
		 idx_uid_inout @ List.map (horn_var_to_expr) (mid_mems@next_mems)
550
		    
551
               )
552
           in
553
           [expr]
554
      in
555

    
556
      reset_exprs@call_expr
557
    end
558
  with Not_found -> ( (* stateless node instance *)
559
    let (n,_) = List.assoc i m.mcalls in
560
    let expr = 
561
      Z3.Expr.mk_app
562
        !ctx
563
        (get_fdecl (machine_stateless_name (node_name n)))
564
        idx_uid_inout 	  (* Arguments are inputs, outputs *)
565
    in
566
    [expr]
567
  )
568

    
569

    
570
    
571
(* (\* Prints a [value] indexed by the suffix list [loop_vars] *\) *)
572
(* let rec value_suffix_to_expr self value = *)
573
(*  match value.value_desc with *)
574
(*  | Fun (n, vl)  ->  *)
575
(*     horn_basic_app n (horn_val_to_expr self) (value_suffix_to_expr self vl) *)
576
    
577
(*  |  _            -> *)
578
(*    horn_val_to_expr self value *)
579

    
580

    
581
(* type_directed assignment: array vs. statically sized type
582
   - [var_type]: type of variable to be assigned
583
   - [var_name]: name of variable to be assigned
584
   - [value]: assigned value
585
   - [pp_var]: printer for variables
586
*)
587
let assign_to_exprs m var_name value =
588
  let self = m.mname.node_id in
589
  let e =
590
    Z3.Boolean.mk_eq
591
      !ctx
592
      (horn_val_to_expr ~is_lhs:true m self var_name)
593
      (horn_val_to_expr m self value)
594
  (* was: TODO deal with array accesses       (value_suffix_to_expr self value) *)
595
  in
596
  [e]
597

    
598
    
599
(* Convert instruction to Z3.Expr and update the set of reset instances *)
600
let rec instr_to_exprs machines reset_instances (m: machine_t) instr : Z3.Expr.expr list * ident list =
601
  match Corelang.get_instr_desc instr with
602
  | MComment _ -> [], reset_instances
603
  | MNoReset i -> (* we assign middle_mem with mem_m. And declare i as reset *)
604
    no_reset_to_exprs machines m i,
605
    i::reset_instances
606
  | MReset i -> (* we assign middle_mem with reset: reset(mem_m) *)
607
    instance_reset_to_exprs machines m i,
608
    i::reset_instances
609
  | MLocalAssign (i,v) ->
610
    assign_to_exprs
611
      m  
612
      (mk_val (Var i) i.var_type) v,
613
    reset_instances
614
  | MStateAssign (i,v) ->
615
    assign_to_exprs
616
      m 
617
      (mk_val (Var i) i.var_type) v,
618
    reset_instances
619
  | MStep ([i0], i, vl) when Basic_library.is_internal_fun i (List.map (fun v -> v.value_type) vl) ->
620
    assert false (* This should not happen anymore *)
621
  | MStep (il, i, vl) ->
622
    (* if reset instance, just print the call over mem_m , otherwise declare mem_m =
623
       mem_c and print the call to mem_m *)
624
    instance_call_to_exprs machines reset_instances m i vl il,
625
    reset_instances (* Since this instance call will only happen once, we
626
		       don't have to update reset_instances *)
627

    
628
  | MBranch (g,hl) -> (* (g = tag1 => expr1) and (g = tag2 => expr2) ...
629
			 should not be produced yet. Later, we will have to
630
			 compare the reset_instances of each branch and
631
			 introduced the mem_m = mem_c for branches to do not
632
			 address it while other did. Am I clear ? *)
633
    (* For each branch we obtain the logical encoding, and the information
634
       whether a sub node has been reset or not. If a node has been reset in one
635
       of the branch, then all others have to have the mem_m = mem_c
636
       statement. *)
637
    let self = m.mname.node_id in
638
    let branch_to_expr (tag, instrs) =
639
      let branch_def, branch_resets = instrs_to_expr machines reset_instances m instrs in
640
      let e =
641
	Z3.Boolean.mk_implies !ctx
642
          (Z3.Boolean.mk_eq !ctx 
643
             (horn_val_to_expr m self g)
644
	     (horn_tag_to_expr tag))
645
          branch_def in
646

    
647
      [e], branch_resets
648
	  
649
    in
650
    List.fold_left (fun (instrs, resets) b ->
651
      let b_instrs, b_resets = branch_to_expr b in
652
      instrs@b_instrs, resets@b_resets 
653
      ) ([], reset_instances) hl
654
  | MSpec _ -> assert false
655

    
656
and instrs_to_expr machines reset_instances m instrs = 
657
  let instr_to_exprs rs i = instr_to_exprs machines rs m i in
658
  let e_list, rs = 
659
    match instrs with
660
    | [x] -> instr_to_exprs reset_instances x 
661
    | _::_ -> (* 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 *)
662
       
663
       List.fold_left (fun (exprs, rs) i -> 
664
         let exprs_i, rs_i = instr_to_exprs rs i in
665
         exprs@exprs_i, rs@rs_i
666
       )
667
         ([], reset_instances) instrs 
668
	 
669
	 
670
    | [] -> [], reset_instances
671
  in
672
  let e = 
673
    match e_list with
674
    | [e] -> e
675
    | [] -> Z3.Boolean.mk_true !ctx
676
    | _ -> Z3.Boolean.mk_and !ctx e_list
677
  in
678
  e, rs
679

    
680

    
681
(*********************************************************)
682

    
683
(* Quantifiying universally all occuring variables *)
684
let add_rule ?(dont_touch=[]) vars  expr =
685
  (* let fds = Z3.Expr.get_args expr in *)
686
  (* Format.eprintf "Expr %s: args: [%a]@." *)
687
  (*   (Z3.Expr.to_string expr) *)
688
  (*   (Utils.fprintf_list ~sep:", " (fun fmt e -> Format.pp_print_string fmt (Z3.Expr.to_string e))) fds; *)
689

    
690
  (* (\* Old code relying on provided vars *\) *)
691
  (* let sorts = (List.map (fun id -> type_to_sort id.var_type) vars) in *)
692
  (* let symbols = (List.map (fun id -> Z3.FuncDecl.get_name (get_fdecl id.var_id)) vars) in *)
693
  
694
  (* New code: we extract vars from expr *)
695
  let module FDSet = Set.Make (struct type t = Z3.FuncDecl.func_decl
696
				      let compare = compare
697
				      let hash = Hashtbl.hash
698
  end)
699
  in
700
(* Fonction seems unused 
701

    
702
  let rec get_expr_vars e =
703
    let open Utils in
704
    let nb_args = Z3.Expr.get_num_args e in
705
    if nb_args <= 0 then (
706
      let fdecl = Z3.Expr.get_func_decl e in
707
      (* let params = Z3.FuncDecl.get_parameters fdecl in *)
708
      (* Format.eprintf "Extracting info about %s: @." (Z3.Expr.to_string e); *)
709
      let dkind = Z3.FuncDecl.get_decl_kind fdecl in
710
      match dkind with Z3enums.OP_UNINTERPRETED -> (
711
	(* Format.eprintf "kind = %s, " (match dkind with Z3enums.OP_TRUE -> "true" | Z3enums.OP_UNINTERPRETED -> "uninter"); *)
712
	(* let open Z3.FuncDecl.Parameter in *)
713
	(* List.iter (fun p -> *)
714
	(*   match p with *)
715
        (*     P_Int i -> Format.eprintf "int %i" i *)
716
	(*   | P_Dbl f -> Format.eprintf "dbl %f" f *)
717
	(*   | P_Sym s -> Format.eprintf "symb"  *)
718
	(*   | P_Srt s -> Format.eprintf "sort"  *)
719
	(*   | P_Ast _ ->Format.eprintf "ast"  *)
720
	(*   | P_Fdl f -> Format.eprintf "fundecl"  *)
721
	(*   | P_Rat s -> Format.eprintf "rat %s" s  *)
722
	     
723
	(* ) params; *)
724
	(* Format.eprintf "]@."; *)
725
	FDSet.singleton fdecl
726
      )
727
      | _ -> FDSet.empty
728
    )
729
    else (*if nb_args > 0 then*)
730
      List.fold_left
731
	(fun accu e ->  FDSet.union accu (get_expr_vars e))
732
	FDSet.empty (Z3.Expr.get_args e)
733
  in
734
 *)
735
  (* Unsed variable. Coul;d be reintroduced 
736
  let extracted_vars = FDSet.elements (FDSet.diff (get_expr_vars expr) (FDSet.of_list dont_touch)) in
737
  let extracted_sorts = List.map Z3.FuncDecl.get_range extracted_vars in
738
  let extracted_symbols = List.map Z3.FuncDecl.get_name extracted_vars in
739
   *)
740
  if !debug then (
741
    Format.eprintf "Declaring rule: %s with variables @[<v 0>@ [%a@ ]@]@ @."
742
      (Z3.Expr.to_string expr)
743
      (Utils.fprintf_list ~sep:",@ " (fun fmt e -> Format.fprintf fmt "%s" (Z3.Expr.to_string e))) (List.map horn_var_to_expr vars)
744
  )
745
    ;
746
  let expr = Z3.Quantifier.mk_forall_const
747
    !ctx  (* context *)
748
    (List.map horn_var_to_expr vars) (* TODO provide bounded variables as expr *)
749
    (* sorts           (\* sort list*\) *)
750
    (* symbols (\* symbol list *\) *)
751
    expr (* expression *)
752
    None (* quantifier weight, None means 1 *)
753
    [] (* pattern list ? *)
754
    [] (* ? *)
755
    None (* ? *)
756
    None (* ? *)
757
  in
758
  (* Format.eprintf "OK@.@?"; *)
759

    
760
  (*
761
    TODO: bizarre la declaration de INIT tout seul semble poser pb.
762
  *) 
763
  Z3.Fixedpoint.add_rule !fp
764
    (Z3.Quantifier.expr_of_quantifier expr)
765
    None
766

    
767
 
768
(********************************************************)
769
    
770
let machine_reset machines m =
771
  let locals = local_memory_vars machines m in
772
  
773
  (* print "x_m = x_c" for each local memory *)
774
  let mid_mem_def =
775
    List.map (fun v ->
776
      Z3.Boolean.mk_eq !ctx
777
	(horn_var_to_expr (rename_mid v))
778
	(horn_var_to_expr (rename_current v))
779
    ) locals
780
  in
781

    
782
  (* print "child_reset ( associated vars _ {c,m} )" for each subnode.
783
     Special treatment for _arrow: _first = true
784
  *)
785

    
786
  let reset_instances =
787
    
788
    List.map (fun (id, (n, _)) ->
789
      let name = node_name n in
790
      if name = "_arrow" then (
791
	Z3.Boolean.mk_eq !ctx
792
	  (
793
	    let vdecl = get_fdecl ((concat m.mname.node_id id) ^ "._arrow._first_m") in
794
	    Z3.Expr.mk_const_f !ctx vdecl
795
	  )
796
	  (Z3.Boolean.mk_true !ctx)
797
	  
798
      ) else (
799
	let machine_n = get_machine machines name in 
800
	
801
	Z3.Expr.mk_app
802
	  !ctx
803
	  (get_fdecl (name ^ "_reset"))
804
	  (List.map (horn_var_to_expr)
805
	     (idx::uid:: (* Additional vars: counters, uid *)
806
	      	(rename_machine_list (concat m.mname.node_id id) (reset_vars machines machine_n))
807
	  ))
808
	  
809
      )
810
    ) m.minstances
811
      
812
      
813
  in
814
  
815
  Z3.Boolean.mk_and !ctx (mid_mem_def @ reset_instances)
816
    
817
        
818

    
819
(*  TODO: empty list means true statement *)
820
let decl_machine machines m =
821
  if m.mname.node_id = Arrow.arrow_id then
822
    (* We don't do arrow function *)
823
    ()
824
  else
825
    begin
826
      let _ =
827
        List.map decl_var
828
      	  (
829
      	    (inout_vars machines m)@
830
      	      (rename_current_list (full_memory_vars machines m)) @
831
      	      (rename_mid_list (full_memory_vars machines m)) @
832
      	      (rename_next_list (full_memory_vars machines m)) @
833
      	      (rename_machine_list m.mname.node_id m.mstep.step_locals)
834
      	  )
835
      in
836
      if is_stateless m then
837
	begin
838
	  if !debug then 
839
	    Format.eprintf "Declaring a stateless machine: %s@." m.mname.node_id;
840

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

    
885
	  (* Rule for reset *)
886

    
887
	  let vars = reset_vars machines m in
888
	  let vars_types = List.map (fun v -> type_to_sort v.var_type) vars in
889
	  let _ = decl_rel (machine_reset_name m.mname.node_id) vars_types in
890
	  let horn_reset_body = machine_reset machines m in	    
891
	  let horn_reset_head = 
892
	    Z3.Expr.mk_app
893
	      !ctx
894
	      (get_fdecl (machine_reset_name m.mname.node_id))
895
	      (	List.map (horn_var_to_expr) (idx::uid:: (* Additional vars: counters, uid *) vars))
896
	  in
897

    
898
	  
899
	  let _ =
900
	    add_rule (idx::uid::vars) (Z3.Boolean.mk_implies !ctx horn_reset_body horn_reset_head)
901
	      
902
	  in
903

    
904
	  (* Rule for step*)
905
	  let vars = step_vars machines m in
906
  	  let vars_types = List.map (fun v -> type_to_sort v.var_type) vars in
907
          let _ = decl_rel (machine_step_name m.mname.node_id) vars_types in
908
	  let horn_step_body, _ (* don't care for reset here *) =
909
	    instrs_to_expr
910
	      machines
911
	      []
912
	      m
913
	      m.mstep.step_instrs
914
	  in
915
	  let horn_step_head = 
916
	    Z3.Expr.mk_app
917
	      !ctx
918
	      (get_fdecl (machine_step_name m.mname.node_id))
919
	      (	List.map (horn_var_to_expr) (idx::uid:: (* Additional vars: counters, uid *) vars))
920
	  in
921
	  match m.mstep.step_asserts with
922
	  | [] ->
923
	     begin
924
	       (* Rule for single predicate *) 
925
	       let vars = (step_vars_c_m_x machines m) @(rename_machine_list m.mname.node_id m.mstep.step_locals) in
926
	       add_rule (idx::uid::vars) (Z3.Boolean.mk_implies !ctx horn_step_body horn_step_head)
927
		 
928
	     end
929
	  | assertsl ->
930
	     begin
931
	       (* Rule for step Assertions @.; *)
932
	       let body_with_asserts =
933
		 Z3.Boolean.mk_and !ctx
934
		   (horn_step_body :: List.map (horn_val_to_expr m m.mname.node_id) assertsl)
935
	       in
936
	       let vars = (step_vars_c_m_x machines m) @(rename_machine_list m.mname.node_id m.mstep.step_locals) in
937
	       add_rule (idx::uid::vars) (Z3.Boolean.mk_implies !ctx body_with_asserts horn_step_head)
938
		 
939
	     end
940
     	       
941
	end
942
    end
943

    
944

    
945

    
946
(* Debug functions *)
947
(*
948
let rec extract_expr_fds e =
949
  (* Format.eprintf "@[<v 2>Extracting fundecls from expr %s@ " *)
950
  (*   (Z3.Expr.to_string e); *)
951
  
952
  (* Removing quantifier is there are some *)
953
  let e = (* I didn't found a nicer way to do it than with an exception.  My
954
	     bad *)
955
    try
956
      let eq = Z3.Quantifier.quantifier_of_expr e in
957
      let e2 = Z3.Quantifier.get_body eq in
958
      (* Format.eprintf "Extracted quantifier body@ "; *)
959
      e2
960
	
961
    with _ -> Format.eprintf "No quantifier info@ "; e
962
  in
963
  let _ =
964
    try 
965
    (
966
      let fd = Z3.Expr.get_func_decl e in
967
      let fd_symbol = Z3.FuncDecl.get_name fd in
968
      let fd_name = Z3.Symbol.to_string fd_symbol in
969
      if not (Hashtbl.mem decls fd_name) then
970
	register_fdecl fd_name fd;
971
      (* Format.eprintf "fdecls (%s): %s@ " *)
972
      (* 	fd_name *)
973
      (* 	(Z3.FuncDecl.to_string fd); *)
974
      try
975
	(
976
	  let args = Z3.Expr.get_args e in
977
	  (* Format.eprintf "@[<v>@ "; *)
978
	  (* List.iter extract_expr_fds args; *)
979
	  (* Format.eprintf "@]@ "; *)
980
	  ()
981
	)
982
      with _ ->
983
	Format.eprintf "Impossible to extract fundecl args for expression %s@ "
984
	  (Z3.Expr.to_string e)
985
    )
986
  with _ ->
987
    Format.eprintf "Impossible to extract anything from expression %s@ "
988
      (Z3.Expr.to_string e)
989
  in
990
  (* Format.eprintf "@]@ " *)
991
  ()      
992
 *)
993
(* Local Variables: *)
994
(* compile-command:"make -C ../.." *)
995
(* End: *)