Project

General

Profile

Download (27.6 KB) Statistics
| Branch: | Tag: | Revision:
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
(** Sorts
41

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

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

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

    
53

    
54
let get_const_sort = Hashtbl.find const_sorts 
55
let get_sort_elems = Hashtbl.find sort_elems
56
let get_tag_sort = Hashtbl.find const_tags
57
  
58

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

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

    
93
(** Func decls
94

    
95
    Similarly fun_decls are registerd, by their name, into a hashtbl. The
96
    proposed encoding introduces a 0-ary fun_decl to model variables and
97
    fun_decl with arguments to declare reset and step predicates.
98

    
99

    
100

    
101
*)
102
let register_fdecl id fd = Hashtbl.add decls id fd
103
let get_fdecl id =
104
  try
105
    Hashtbl.find decls id
106
  with Not_found -> (Format.eprintf "Unable to find func_decl %s@.@?" id; raise Not_found)
107

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

    
112
    
113
let decl_var id =
114
  (* Format.eprintf "Declaring var %s@." id.var_id; *)
115
  let fdecl = Z3.FuncDecl.mk_func_decl_s !ctx id.var_id [] (type_to_sort id.var_type) in
116
  register_fdecl id.var_id fdecl;
117
  fdecl
118

    
119
let decl_rel name args_sorts =
120
  (*verifier ce qui est construit. On veut un declare-rel *)
121
  
122
  (* let args_sorts = List.map (fun v -> type_to_sort v.var_type) args in *)
123
  if !debug then
124
    Format.eprintf "Registering fdecl %s (%a)@."
125
      name
126
      (Utils.fprintf_list ~sep:"@ "
127
	 (fun fmt sort -> Format.fprintf fmt "%s" (Z3.Sort.to_string sort)))
128
      args_sorts
129
  ;
130
  let fdecl = Z3.FuncDecl.mk_func_decl_s !ctx name args_sorts bool_sort in
131
  Z3.Fixedpoint.register_relation !fp fdecl;
132
  register_fdecl name fdecl;
133
  fdecl
134
  
135

    
136
(** Conversion functions
137

    
138
    The following is similar to the Horn backend. Each printing function is
139
    rephrased from pp_xx to xx_to_expr and produces a Z3 value.
140

    
141
*)
142

    
143

    
144
(* Returns the f_decl associated to the variable v *)
145
let horn_var_to_expr v =
146
  Z3.Expr.mk_const_f !ctx (get_fdecl v.var_id)
147

    
148

    
149

    
150

    
151
  (* Used to print boolean constants *)
152
let horn_tag_to_expr t =
153
  if t = Corelang.tag_true then
154
    Z3.Boolean.mk_true !ctx
155
  else if t = Corelang.tag_false then
156
    Z3.Boolean.mk_false !ctx
157
  else
158
    (* Finding the associated sort *)
159
    let sort = get_tag_sort t in
160
    let elems = get_sort_elems sort in 
161
    let res : Z3.Expr.expr option =
162
      List.fold_left2 (fun res cst expr ->
163
          match res with
164
          | Some _ -> res
165
          | None -> if t = cst then Some (expr:Z3.Expr.expr) else None
166
        ) None elems (Z3.Enumeration.get_consts sort)
167
    in
168
    match res with None -> assert false | Some s -> s
169
    
170
(* Prints a constant value *)
171
let rec horn_const_to_expr c =
172
  match c with
173
    | Const_int i    -> Z3.Arithmetic.Integer.mk_numeral_i !ctx i
174
    | Const_real (_,_,s)   -> Z3.Arithmetic.Real.mk_numeral_i !ctx 0
175
    | Const_tag t    -> horn_tag_to_expr t
176
    | _              -> assert false
177

    
178

    
179

    
180
(* Default value for each type, used when building arrays. Eg integer array
181
   [2;7] is defined as (store (store (0) 1 7) 0 2) where 0 is this default value
182
   for the type integer (arrays).
183
*)
184
let rec horn_default_val t =
185
  let t = Types.dynamic_type t in
186
  if Types.is_bool_type t  then Z3.Boolean.mk_true !ctx else
187
  if Types.is_int_type t then Z3.Arithmetic.Integer.mk_numeral_i !ctx 0 else 
188
  if Types.is_real_type t then Z3.Arithmetic.Real.mk_numeral_i !ctx 0 else 
189
  (* match (Types.dynamic_type t).Types.tdesc with
190
   * | Types.Tarray(dim, l) -> (\* TODO PL: this strange code has to be (heavily) checked *\)
191
   *    let valt = Types.array_element_type t in
192
   *    fprintf fmt "((as const (Array Int %a)) %a)"
193
   *      pp_type valt 
194
   *      pp_default_val valt
195
   * | Types.Tstruct(l) -> assert false
196
   * | Types.Ttuple(l) -> assert false
197
   * |_ -> *) assert false
198

    
199
(* Conversion of basic library functions *)
200
    
201
let horn_basic_app i val_to_expr vl =
202
  match i, vl with
203
  | "ite", [v1; v2; v3] ->
204
     Z3.Boolean.mk_ite
205
       !ctx
206
       (val_to_expr v1)
207
       (val_to_expr v2)
208
       (val_to_expr v3)
209

    
210
  | "uminus", [v] ->
211
     Z3.Arithmetic.mk_unary_minus
212
       !ctx
213
       (val_to_expr v)
214
  | "not", [v] ->
215
     Z3.Boolean.mk_not
216
       !ctx
217
       (val_to_expr v)
218
  | "=", [v1; v2] ->
219
     Z3.Boolean.mk_eq
220
       !ctx
221
       (val_to_expr v1)
222
       (val_to_expr v2)
223
  | "&&", [v1; v2] ->
224
     Z3.Boolean.mk_and
225
       !ctx
226
       [val_to_expr v1;
227
        val_to_expr v2]
228
  | "||", [v1; v2] ->
229
          Z3.Boolean.mk_or
230
       !ctx
231
       [val_to_expr v1;
232
        val_to_expr v2]
233

    
234
  | "impl", [v1; v2] ->
235
     Z3.Boolean.mk_implies
236
       !ctx
237
       (val_to_expr v1)
238
       (val_to_expr v2)
239
 | "mod", [v1; v2] ->
240
          Z3.Arithmetic.Integer.mk_mod
241
       !ctx
242
       (val_to_expr v1)
243
       (val_to_expr v2)
244
  | "equi", [v1; v2] ->
245
          Z3.Boolean.mk_eq
246
       !ctx
247
       (val_to_expr v1)
248
       (val_to_expr v2)
249
  | "xor", [v1; v2] ->
250
          Z3.Boolean.mk_xor
251
       !ctx
252
       (val_to_expr v1)
253
       (val_to_expr v2)
254
  | "!=", [v1; v2] ->
255
     Z3.Boolean.mk_not
256
       !ctx
257
       (
258
         Z3.Boolean.mk_eq
259
           !ctx
260
           (val_to_expr v1)
261
           (val_to_expr v2)
262
       )
263
  | "/", [v1; v2] ->
264
     Z3.Arithmetic.mk_div
265
       !ctx
266
       (val_to_expr v1)
267
       (val_to_expr v2)
268

    
269
  | "+", [v1; v2] ->
270
     Z3.Arithmetic.mk_add
271
       !ctx
272
       [val_to_expr v1; val_to_expr v2]
273

    
274
  | "-", [v1; v2] ->
275
     Z3.Arithmetic.mk_sub
276
       !ctx
277
       [val_to_expr v1 ; val_to_expr v2]
278
       
279
  | "*", [v1; v2] ->
280
     Z3.Arithmetic.mk_mul
281
       !ctx
282
       [val_to_expr v1; val_to_expr v2]
283

    
284

    
285
  | "<", [v1; v2] ->
286
     Z3.Arithmetic.mk_lt
287
       !ctx
288
       (val_to_expr v1)
289
       (val_to_expr v2)
290

    
291
  | "<=", [v1; v2] ->
292
     Z3.Arithmetic.mk_le
293
       !ctx
294
       (val_to_expr v1)
295
       (val_to_expr v2)
296

    
297
  | ">", [v1; v2] ->
298
     Z3.Arithmetic.mk_gt
299
       !ctx
300
       (val_to_expr v1)
301
       (val_to_expr v2)
302

    
303
  | ">=", [v1; v2] ->
304
     Z3.Arithmetic.mk_ge
305
       !ctx
306
       (val_to_expr v1)
307
       (val_to_expr v2)
308

    
309
       
310
  (* | _, [v1; v2] ->      Z3.Boolean.mk_and
311
   *      !ctx
312
   *      (val_to_expr v1)
313
   *      (val_to_expr v2)
314
   * 
315
   *      Format.fprintf fmt "(%s %a %a)" i val_to_exprr v1 val_to_expr v2 *)
316
  | _ -> (
317
    Format.eprintf
318
      "internal error: zustre unkown function %s@." i;
319
    assert false)
320

    
321
           
322
(* Convert a value expression [v], with internal function calls only.  [pp_var]
323
   is a printer for variables (typically [pp_c_var_read]), but an offset suffix
324
   may be added for array variables
325
*)
326
let rec horn_val_to_expr ?(is_lhs=false) self v =
327
  match v.value_desc with
328
  | Cst c       -> horn_const_to_expr c
329

    
330
  (* Code specific for arrays *)
331
  | Array il    ->
332
     (* An array definition: 
333
	(store (
334
	  ...
335
 	    (store (
336
	       store (
337
	          default_val
338
	       ) 
339
	       idx_n val_n
340
	    ) 
341
	    idx_n-1 val_n-1)
342
	  ... 
343
	  idx_1 val_1
344
	) *)
345
     let rec build_array (tab, x) =
346
       match tab with
347
       | [] -> horn_default_val v.value_type(* (get_type v) *)
348
       | h::t ->
349
	  Z3.Z3Array.mk_store
350
            !ctx
351
	    (build_array (t, (x+1)))
352
	    (Z3.Arithmetic.Integer.mk_numeral_i !ctx x)
353
	    (horn_val_to_expr ~is_lhs:is_lhs self h)
354
     in
355
     build_array (il, 0)
356
       
357
  | Access(tab,index) ->
358
     Z3.Z3Array.mk_select !ctx 
359
       (horn_val_to_expr ~is_lhs:is_lhs self tab)
360
       (horn_val_to_expr ~is_lhs:is_lhs self index)
361

    
362
  (* Code specific for arrays *)
363
    
364
  | Power (v, n)  -> assert false
365
  | LocalVar v    ->
366
     horn_var_to_expr
367
       (rename_machine
368
          self
369
          v)
370
  | StateVar v    ->
371
     if Types.is_array_type v.var_type
372
     then assert false
373
     else horn_var_to_expr (rename_machine self ((if is_lhs then rename_next else rename_current) (* self *) v))
374
  | Fun (n, vl)   -> horn_basic_app n (horn_val_to_expr self) vl
375

    
376
let no_reset_to_exprs machines m i =
377
  let (n,_) = List.assoc i m.minstances in
378
  let target_machine = List.find (fun m  -> m.mname.node_id = (Corelang.node_name n)) machines in
379

    
380
  let m_list = 
381
    rename_machine_list
382
      (concat m.mname.node_id i)
383
      (rename_mid_list (full_memory_vars machines target_machine))
384
  in
385
  let c_list =
386
    rename_machine_list
387
      (concat m.mname.node_id i)
388
      (rename_current_list (full_memory_vars machines target_machine))
389
  in
390
  match c_list, m_list with
391
  | [chd], [mhd] ->
392
     let expr =
393
       Z3.Boolean.mk_eq !ctx 
394
         (horn_var_to_expr mhd)
395
         (horn_var_to_expr chd)
396
     in
397
     [expr]
398
  | _ -> (
399
    let exprs =
400
      List.map2 (fun mhd chd -> 
401
          Z3.Boolean.mk_eq !ctx 
402
            (horn_var_to_expr mhd)
403
            (horn_var_to_expr chd)
404
        )
405
        m_list
406
        c_list
407
    in
408
    exprs
409
  )
410

    
411
let instance_reset_to_exprs machines m i =
412
  let (n,_) = List.assoc i m.minstances in
413
  let target_machine = List.find (fun m  -> m.mname.node_id = (Corelang.node_name n)) machines in
414
  let vars =
415
    (
416
      (rename_machine_list
417
	 (concat m.mname.node_id i)
418
	 (rename_current_list (full_memory_vars machines target_machine))
419
      ) 
420
      @
421
	(rename_machine_list
422
	   (concat m.mname.node_id i)
423
	   (rename_mid_list (full_memory_vars machines target_machine))
424
	)
425
    )
426
  in
427
  let expr =
428
    Z3.Expr.mk_app
429
      !ctx
430
      (get_fdecl (machine_reset_name (Corelang.node_name n)))
431
      (List.map (horn_var_to_expr) vars)
432
  in
433
  [expr]
434

    
435
let instance_call_to_exprs machines reset_instances m i inputs outputs =
436
  let self = m.mname.node_id in
437
  try (* stateful node instance *)
438
    begin
439
      let (n,_) = List.assoc i m.minstances in
440
      let target_machine = List.find (fun m  -> m.mname.node_id = Corelang.node_name n) machines in
441

    
442
      (* Checking whether this specific instances has been reset yet *)
443
      let reset_exprs = 
444
        if not (List.mem i reset_instances) then
445
	  (* If not, declare mem_m = mem_c *)
446
	  no_reset_to_exprs machines m i
447
        else
448
          [] (* Nothing to add yet *)
449
      in
450
      
451
      let mems = full_memory_vars machines target_machine in
452
      let rename_mems f = rename_machine_list (concat m.mname.node_id i) (f mems) in
453
      let mid_mems = rename_mems rename_mid_list in
454
      let next_mems = rename_mems rename_next_list in
455

    
456
      let call_expr = 
457
      match Corelang.node_name n, inputs, outputs, mid_mems, next_mems with
458
      | "_arrow", [i1; i2], [o], [mem_m], [mem_x] -> begin
459
          let stmt1 = (* out = ite mem_m then i1 else i2 *)
460
            Z3.Boolean.mk_eq !ctx
461
              ( (* output var *)
462
                horn_val_to_expr
463
                  ~is_lhs:true
464
                  self
465
                  (mk_val (LocalVar o) o.var_type)
466
              )
467
              (
468
                Z3.Boolean.mk_ite !ctx 
469
	          (horn_var_to_expr mem_m) 
470
	          (horn_val_to_expr self i1)
471
	          (horn_val_to_expr self i2)
472
              )
473
          in
474
          let stmt2 = (* mem_X = false *)
475
            Z3.Boolean.mk_eq !ctx
476
	      (horn_var_to_expr mem_x)
477
              (Z3.Boolean.mk_false !ctx)
478
          in
479
          [stmt1; stmt2]
480
      end
481

    
482
      | node_name_n ->
483
         let expr = 
484
           Z3.Expr.mk_app
485
             !ctx
486
             (get_fdecl (machine_step_name (node_name n)))
487
             ( (* Arguments are input, output, mid_mems, next_mems *)
488
               (
489
                 List.map (horn_val_to_expr self) (
490
                     inputs @
491
	               (List.map (fun v -> mk_val (LocalVar v) v.var_type) outputs)
492
                   )
493
               ) @ (
494
                 List.map (horn_var_to_expr) (mid_mems@next_mems)
495
	       )
496
             )
497
         in
498
         [expr]
499
      in
500

    
501
      reset_exprs@call_expr
502
    end
503
  with Not_found -> ( (* stateless node instance *)
504
    let (n,_) = List.assoc i m.mcalls in
505
    let expr = 
506
      Z3.Expr.mk_app
507
        !ctx
508
        (get_fdecl (machine_stateless_name (node_name n)))
509
        ((* Arguments are inputs, outputs *)
510
         List.map (horn_val_to_expr self)
511
           (
512
             inputs @ (List.map (fun v -> mk_val (LocalVar v) v.var_type) outputs)
513
           )
514
        )
515
    in
516
    [expr]
517
  )
518

    
519

    
520
    
521
(* (\* Prints a [value] indexed by the suffix list [loop_vars] *\) *)
522
(* let rec value_suffix_to_expr self value = *)
523
(*  match value.value_desc with *)
524
(*  | Fun (n, vl)  ->  *)
525
(*     horn_basic_app n (horn_val_to_expr self) (value_suffix_to_expr self vl) *)
526
    
527
(*  |  _            -> *)
528
(*    horn_val_to_expr self value *)
529

    
530

    
531
(* type_directed assignment: array vs. statically sized type
532
   - [var_type]: type of variable to be assigned
533
   - [var_name]: name of variable to be assigned
534
   - [value]: assigned value
535
   - [pp_var]: printer for variables
536
*)
537
let assign_to_exprs m var_name value =
538
  let self = m.mname.node_id in
539
  let e =
540
    Z3.Boolean.mk_eq
541
      !ctx
542
      (horn_val_to_expr ~is_lhs:true self var_name)
543
      (horn_val_to_expr self value)
544
  (* was: TODO deal with array accesses       (value_suffix_to_expr self value) *)
545
  in
546
  [e]
547

    
548
    
549
(* Convert instruction to Z3.Expr and update the set of reset instances *)
550
let rec instr_to_exprs machines reset_instances (m: machine_t) instr : Z3.Expr.expr list * ident list =
551
  match Corelang.get_instr_desc instr with
552
  | MComment _ -> [], reset_instances
553
  | MNoReset i -> (* we assign middle_mem with mem_m. And declare i as reset *)
554
    no_reset_to_exprs machines m i,
555
    i::reset_instances
556
  | MReset i -> (* we assign middle_mem with reset: reset(mem_m) *)
557
    instance_reset_to_exprs machines m i,
558
    i::reset_instances
559
  | MLocalAssign (i,v) ->
560
    assign_to_exprs
561
      m  
562
      (mk_val (LocalVar i) i.var_type) v,
563
    reset_instances
564
  | MStateAssign (i,v) ->
565
    assign_to_exprs
566
      m 
567
      (mk_val (StateVar i) i.var_type) v,
568
    reset_instances
569
  | MStep ([i0], i, vl) when Basic_library.is_internal_fun i (List.map (fun v -> v.value_type) vl) ->
570
    assert false (* This should not happen anymore *)
571
  | MStep (il, i, vl) ->
572
    (* if reset instance, just print the call over mem_m , otherwise declare mem_m =
573
       mem_c and print the call to mem_m *)
574
    instance_call_to_exprs machines reset_instances m i vl il,
575
    reset_instances (* Since this instance call will only happen once, we
576
		       don't have to update reset_instances *)
577

    
578
  | MBranch (g,hl) -> (* (g = tag1 => expr1) and (g = tag2 => expr2) ...
579
			 should not be produced yet. Later, we will have to
580
			 compare the reset_instances of each branch and
581
			 introduced the mem_m = mem_c for branches to do not
582
			 address it while other did. Am I clear ? *)
583
    (* For each branch we obtain the logical encoding, and the information
584
       whether a sub node has been reset or not. If a node has been reset in one
585
       of the branch, then all others have to have the mem_m = mem_c
586
       statement. *)
587
    let self = m.mname.node_id in
588
    let branch_to_expr (tag, instrs) =
589
      let branch_def, branch_resets = instrs_to_expr machines reset_instances m instrs in
590
      let e =
591
	Z3.Boolean.mk_implies !ctx
592
          (Z3.Boolean.mk_eq !ctx 
593
             (horn_val_to_expr self g)
594
	     (horn_tag_to_expr tag))
595
          branch_def in
596

    
597
      [e], branch_resets
598
	  
599
    in
600
    List.fold_left (fun (instrs, resets) b ->
601
      let b_instrs, b_resets = branch_to_expr b in
602
      instrs@b_instrs, resets@b_resets 
603
    ) ([], reset_instances) hl 
604

    
605
and instrs_to_expr machines reset_instances m instrs = 
606
  let instr_to_exprs rs i = instr_to_exprs machines rs m i in
607
  let e_list, rs = 
608
    match instrs with
609
    | [x] -> instr_to_exprs reset_instances x 
610
    | _::_ -> (* 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 *)
611
       
612
       List.fold_left (fun (exprs, rs) i -> 
613
         let exprs_i, rs_i = instr_to_exprs rs i in
614
         exprs@exprs_i, rs@rs_i
615
       )
616
         ([], reset_instances) instrs 
617
	 
618
	 
619
    | [] -> [], reset_instances
620
  in
621
  let e = 
622
    match e_list with
623
    | [e] -> e
624
    | [] -> Z3.Boolean.mk_true !ctx
625
    | _ -> Z3.Boolean.mk_and !ctx e_list
626
  in
627
  e, rs
628

    
629

    
630
(*********************************************************)
631

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

    
639
  (* (\* Old code relying on provided vars *\) *)
640
  (* let sorts = (List.map (fun id -> type_to_sort id.var_type) vars) in *)
641
  (* let symbols = (List.map (fun id -> Z3.FuncDecl.get_name (get_fdecl id.var_id)) vars) in *)
642
  
643
  (* New code: we extract vars from expr *)
644
  let module FDSet = Set.Make (struct type t = Z3.FuncDecl.func_decl
645
				      let compare = compare
646
				      let hash = Hashtbl.hash
647
  end)
648
  in
649
  let rec get_expr_vars e =
650
    let open Utils in
651
    let nb_args = Z3.Expr.get_num_args e in
652
    if nb_args <= 0 then (
653
      let fdecl = Z3.Expr.get_func_decl e in
654
      (* let params = Z3.FuncDecl.get_parameters fdecl in *)
655
      (* Format.eprintf "Extracting info about %s: @." (Z3.Expr.to_string e); *)
656
      let dkind = Z3.FuncDecl.get_decl_kind fdecl in
657
      match dkind with Z3enums.OP_UNINTERPRETED -> (
658
	(* Format.eprintf "kind = %s, " (match dkind with Z3enums.OP_TRUE -> "true" | Z3enums.OP_UNINTERPRETED -> "uninter"); *)
659
	(* let open Z3.FuncDecl.Parameter in *)
660
	(* List.iter (fun p -> *)
661
	(*   match p with *)
662
        (*     P_Int i -> Format.eprintf "int %i" i *)
663
	(*   | P_Dbl f -> Format.eprintf "dbl %f" f *)
664
	(*   | P_Sym s -> Format.eprintf "symb"  *)
665
	(*   | P_Srt s -> Format.eprintf "sort"  *)
666
	(*   | P_Ast _ ->Format.eprintf "ast"  *)
667
	(*   | P_Fdl f -> Format.eprintf "fundecl"  *)
668
	(*   | P_Rat s -> Format.eprintf "rat %s" s  *)
669
	     
670
	(* ) params; *)
671
	(* Format.eprintf "]@."; *)
672
	FDSet.singleton fdecl
673
      )
674
      | _ -> FDSet.empty
675
    )
676
    else (*if nb_args > 0 then*)
677
      List.fold_left
678
	(fun accu e ->  FDSet.union accu (get_expr_vars e))
679
	FDSet.empty (Z3.Expr.get_args e)
680
  in
681
  let extracted_vars = FDSet.elements (FDSet.diff (get_expr_vars expr) (FDSet.of_list dont_touch)) in
682
  let extracted_sorts = List.map Z3.FuncDecl.get_range extracted_vars in
683
  let extracted_symbols = List.map Z3.FuncDecl.get_name extracted_vars in
684

    
685
  if !debug then (
686
    Format.eprintf "Declaring rule: %s with variables @[<v 0>@ [%a@ ]@]@ @."
687
      (Z3.Expr.to_string expr)
688
      (Utils.fprintf_list ~sep:",@ " (fun fmt e -> Format.fprintf fmt "%s" (Z3.Expr.to_string e))) (List.map horn_var_to_expr vars)
689
  )
690
    ;
691
  let expr = Z3.Quantifier.mk_forall_const
692
    !ctx  (* context *)
693
    (List.map horn_var_to_expr vars) (* TODO provide bounded variables as expr *)
694
    (* sorts           (\* sort list*\) *)
695
    (* symbols (\* symbol list *\) *)
696
    expr (* expression *)
697
    None (* quantifier weight, None means 1 *)
698
    [] (* pattern list ? *)
699
    [] (* ? *)
700
    None (* ? *)
701
    None (* ? *)
702
  in
703
  (* Format.eprintf "OK@.@?"; *)
704

    
705
  (*
706
    TODO: bizarre la declaration de INIT tout seul semble poser pb.
707
  *) 
708
  Z3.Fixedpoint.add_rule !fp
709
    (Z3.Quantifier.expr_of_quantifier expr)
710
    None
711

    
712
 
713
(********************************************************)
714
    
715
let machine_reset machines m =
716
  let locals = local_memory_vars machines m in
717
  
718
  (* print "x_m = x_c" for each local memory *)
719
  let mid_mem_def =
720
    List.map (fun v ->
721
      Z3.Boolean.mk_eq !ctx
722
	(horn_var_to_expr (rename_mid v))
723
	(horn_var_to_expr (rename_current v))
724
    ) locals
725
  in
726

    
727
  (* print "child_reset ( associated vars _ {c,m} )" for each subnode.
728
     Special treatment for _arrow: _first = true
729
  *)
730

    
731
  let reset_instances =
732
    
733
    List.map (fun (id, (n, _)) ->
734
      let name = node_name n in
735
      if name = "_arrow" then (
736
	Z3.Boolean.mk_eq !ctx
737
	  (
738
	    let vdecl = get_fdecl ((concat m.mname.node_id id) ^ "._arrow._first_m") in
739
	    Z3.Expr.mk_const_f !ctx vdecl
740
	  )
741
	  (Z3.Boolean.mk_true !ctx)
742
	  
743
      ) else (
744
	let machine_n = get_machine machines name in 
745
	
746
	Z3.Expr.mk_app
747
	  !ctx
748
	  (get_fdecl (name ^ "_reset"))
749
	  (List.map (horn_var_to_expr)
750
	     (rename_machine_list (concat m.mname.node_id id) (reset_vars machines machine_n))
751
	  )
752
	  
753
      )
754
    ) m.minstances
755
      
756
      
757
  in
758
  
759
  Z3.Boolean.mk_and !ctx (mid_mem_def @ reset_instances)
760
    
761
        
762

    
763
(*  TODO: empty list means true statement *)
764
let decl_machine machines m =
765
  if m.mname.node_id = Arrow.arrow_id then
766
    (* We don't do arrow function *)
767
    ()
768
  else
769
    begin
770
      let _ =
771
        List.map decl_var
772
      	  (
773
      	    (inout_vars machines m)@
774
      	      (rename_current_list (full_memory_vars machines m)) @
775
      	      (rename_mid_list (full_memory_vars machines m)) @
776
      	      (rename_next_list (full_memory_vars machines m)) @
777
      	      (rename_machine_list m.mname.node_id m.mstep.step_locals)
778
      	  )
779
      in
780
      if is_stateless m then
781
	begin
782
	  if !debug then 
783
	    Format.eprintf "Declaring a stateless machine: %s@." m.mname.node_id;
784

    
785
	  (* Declaring single predicate *)
786
	  let vars = inout_vars machines m in
787
	  let vars_types = List.map (fun v -> type_to_sort v.var_type) vars in
788
	  let _ = decl_rel (machine_stateless_name m.mname.node_id) vars_types in
789
	  
790
	  let horn_body, _ (* don't care for reset here *) =
791
	    instrs_to_expr
792
	      machines
793
	      ([] (* No reset info for stateless nodes *) )
794
	      m
795
	      m.mstep.step_instrs
796
	  in
797
	  let horn_head = 
798
	    Z3.Expr.mk_app
799
	      !ctx
800
	      (get_fdecl (machine_stateless_name m.mname.node_id))
801
	      (List.map (horn_var_to_expr) vars)
802
	  in
803
	  (* this line seems useless *)
804
	  let vars = vars@(rename_machine_list m.mname.node_id m.mstep.step_locals) in
805
	  (* Format.eprintf "useless Vars: %a@." (Utils.fprintf_list ~sep:"@ " Printers.pp_var) vars; *)
806
	  match m.mstep.step_asserts with
807
	  | [] ->
808
	     begin
809
	       (* Rule for single predicate : "; Stateless step rule @." *)
810
	       (*let vars = rename_machine_list m.mname.node_id m.mstep.step_locals in*)
811
	       (* TODO clean code *)
812
	       (* Format.eprintf "used Vars: %a@." (Utils.fprintf_list ~sep:"@ " Printers.pp_var) vars; *)
813
	       add_rule vars (Z3.Boolean.mk_implies !ctx horn_body horn_head)
814
		 
815
	     end
816
	  | assertsl ->
817
	     begin
818
	       (*Rule for step "; Stateless step rule with Assertions @.";*)
819
	       let body_with_asserts =
820
		 Z3.Boolean.mk_and !ctx (horn_body :: List.map (horn_val_to_expr m.mname.node_id) assertsl)
821
	       in
822
	       let vars = rename_machine_list m.mname.node_id m.mstep.step_locals in
823
	       add_rule vars (Z3.Boolean.mk_implies !ctx body_with_asserts horn_head)
824
	     end
825
	end
826
      else
827
	begin
828

    
829
	  (* Rule for reset *)
830

    
831
	  let vars = reset_vars machines m in
832
	  let vars_types = List.map (fun v -> type_to_sort v.var_type) vars in
833
	  let _ = decl_rel (machine_reset_name m.mname.node_id) vars_types in
834
	  let horn_reset_body = machine_reset machines m in	    
835
	  let horn_reset_head = 
836
	    Z3.Expr.mk_app
837
	      !ctx
838
	      (get_fdecl (machine_reset_name m.mname.node_id))
839
	      (List.map (horn_var_to_expr) vars)
840
	  in
841

    
842
	  
843
	  let _ =
844
	    add_rule vars (Z3.Boolean.mk_implies !ctx horn_reset_body horn_reset_head)
845
	      
846
	  in
847

    
848
	  (* Rule for step*)
849
	  let vars = step_vars machines m in
850
  	  let vars_types = List.map (fun v -> type_to_sort v.var_type) vars in
851
          let _ = decl_rel (machine_step_name m.mname.node_id) vars_types in
852
	  let horn_step_body, _ (* don't care for reset here *) =
853
	    instrs_to_expr
854
	      machines
855
	      []
856
	      m
857
	      m.mstep.step_instrs
858
	  in
859
	  let horn_step_head = 
860
	    Z3.Expr.mk_app
861
	      !ctx
862
	      (get_fdecl (machine_step_name m.mname.node_id))
863
	      (List.map (horn_var_to_expr) vars)
864
	  in
865
	  match m.mstep.step_asserts with
866
	  | [] ->
867
	     begin
868
	       (* Rule for single predicate *) 
869
	       let vars = (step_vars_c_m_x machines m) @(rename_machine_list m.mname.node_id m.mstep.step_locals) in
870
	       add_rule vars (Z3.Boolean.mk_implies !ctx horn_step_body horn_step_head)
871
		 
872
	     end
873
	  | assertsl ->
874
	     begin
875
	       (* Rule for step Assertions @.; *)
876
	       let body_with_asserts =
877
		 Z3.Boolean.mk_and !ctx
878
		   (horn_step_body :: List.map (horn_val_to_expr m.mname.node_id) assertsl)
879
	       in
880
	       let vars = (step_vars_c_m_x machines m) @(rename_machine_list m.mname.node_id m.mstep.step_locals) in
881
	       add_rule vars (Z3.Boolean.mk_implies !ctx body_with_asserts horn_step_head)
882
		 
883
	     end
884
     	       
885
	end
886
    end
887

    
888

    
889

    
890
(* Debug functions *)
891

    
892
let rec extract_expr_fds e =
893
  (* Format.eprintf "@[<v 2>Extracting fundecls from expr %s@ " *)
894
  (*   (Z3.Expr.to_string e); *)
895
  
896
  (* Removing quantifier is there are some *)
897
  let e = (* I didn't found a nicer way to do it than with an exception.  My
898
	     bad *)
899
    try
900
      let eq = Z3.Quantifier.quantifier_of_expr e in
901
      let e2 = Z3.Quantifier.get_body eq in
902
      (* Format.eprintf "Extracted quantifier body@ "; *)
903
      e2
904
	
905
    with _ -> Format.eprintf "No quantifier info@ "; e
906
  in
907
  let _ =
908
    try 
909
    (
910
      let fd = Z3.Expr.get_func_decl e in
911
      let fd_symbol = Z3.FuncDecl.get_name fd in
912
      let fd_name = Z3.Symbol.to_string fd_symbol in
913
      if not (Hashtbl.mem decls fd_name) then
914
	register_fdecl fd_name fd;
915
      (* Format.eprintf "fdecls (%s): %s@ " *)
916
      (* 	fd_name *)
917
      (* 	(Z3.FuncDecl.to_string fd); *)
918
      try
919
	(
920
	  let args = Z3.Expr.get_args e in
921
	  (* Format.eprintf "@[<v>@ "; *)
922
	  (* List.iter extract_expr_fds args; *)
923
	  (* Format.eprintf "@]@ "; *)
924
	  ()
925
	)
926
      with _ ->
927
	Format.eprintf "Impossible to extract fundecl args for expression %s@ "
928
	  (Z3.Expr.to_string e)
929
    )
930
  with _ ->
931
    Format.eprintf "Impossible to extract anything from expression %s@ "
932
      (Z3.Expr.to_string e)
933
  in
934
  (* Format.eprintf "@]@ " *)
935
  ()      
936

    
937
(* Local Variables: *)
938
(* compile-command:"make -C ../.." *)
939
(* End: *)
(2-2/5)