Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / tools / zustre / zustre_common.ml @ 2f7c9195

History | View | Annotate | Download (27 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
(** 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
  let fdecl = Z3.FuncDecl.mk_func_decl_s !ctx name args_sorts bool_sort in
124
  Z3.Fixedpoint.register_relation !fp fdecl;
125
  register_fdecl name fdecl;
126
  fdecl
127
  
128

    
129
(** Conversion functions
130

    
131
    The following is similar to the Horn backend. Each printing function is
132
    rephrased from pp_xx to xx_to_expr and produces a Z3 value.
133

    
134
*)
135

    
136

    
137
(* Returns the f_decl associated to the variable v *)
138
let horn_var_to_expr v =
139
  Z3.Expr.mk_const_f !ctx (get_fdecl v.var_id)
140

    
141

    
142

    
143

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

    
171

    
172

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

    
192
(* Conversion of basic library functions *)
193
    
194
let horn_basic_app i val_to_expr vl =
195
  match i, vl with
196
  | "ite", [v1; v2; v3] ->
197
     Z3.Boolean.mk_ite
198
       !ctx
199
       (val_to_expr v1)
200
       (val_to_expr v2)
201
       (val_to_expr v3)
202

    
203
  | "uminus", [v] ->
204
     Z3.Arithmetic.mk_unary_minus
205
       !ctx
206
       (val_to_expr v)
207
  | "not", [v] ->
208
     Z3.Boolean.mk_not
209
       !ctx
210
       (val_to_expr v)
211
  | "=", [v1; v2] ->
212
     Z3.Boolean.mk_eq
213
       !ctx
214
       (val_to_expr v1)
215
       (val_to_expr v2)
216
  | "&&", [v1; v2] ->
217
     Z3.Boolean.mk_and
218
       !ctx
219
       [val_to_expr v1;
220
        val_to_expr v2]
221
  | "||", [v1; v2] ->
222
          Z3.Boolean.mk_or
223
       !ctx
224
       [val_to_expr v1;
225
        val_to_expr v2]
226

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

    
262
  | "+", [v1; v2] ->
263
     Z3.Arithmetic.mk_add
264
       !ctx
265
       [val_to_expr v1; val_to_expr v2]
266

    
267
  | "-", [v1; v2] ->
268
     Z3.Arithmetic.mk_sub
269
       !ctx
270
       [val_to_expr v1 ; val_to_expr v2]
271
       
272
  | "*", [v1; v2] ->
273
     Z3.Arithmetic.mk_mul
274
       !ctx
275
       [val_to_expr v1; val_to_expr v2]
276

    
277

    
278
  | "<", [v1; v2] ->
279
     Z3.Arithmetic.mk_lt
280
       !ctx
281
       (val_to_expr v1)
282
       (val_to_expr v2)
283

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

    
290
  | ">", [v1; v2] ->
291
     Z3.Arithmetic.mk_gt
292
       !ctx
293
       (val_to_expr v1)
294
       (val_to_expr v2)
295

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

    
302
       
303
  (* | _, [v1; v2] ->      Z3.Boolean.mk_and
304
   *      !ctx
305
   *      (val_to_expr v1)
306
   *      (val_to_expr v2)
307
   * 
308
   *      Format.fprintf fmt "(%s %a %a)" i val_to_exprr v1 val_to_expr v2 *)
309
  | _ -> (
310
    Format.eprintf
311
      "internal error: zustre unkown function %s@." i;
312
    assert false)
313

    
314
           
315
(* Convert a value expression [v], with internal function calls only.  [pp_var]
316
   is a printer for variables (typically [pp_c_var_read]), but an offset suffix
317
   may be added for array variables
318
*)
319
let rec horn_val_to_expr ?(is_lhs=false) self v =
320
  match v.value_desc with
321
  | Cst c       -> horn_const_to_expr c
322

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

    
355
  (* Code specific for arrays *)
356
    
357
  | Power (v, n)  -> assert false
358
  | LocalVar v    ->
359
     horn_var_to_expr
360
       (rename_machine
361
          self
362
          v)
363
  | StateVar v    ->
364
     if Types.is_array_type v.var_type
365
     then assert false
366
     else horn_var_to_expr (rename_machine self ((if is_lhs then rename_next else rename_current) (* self *) v))
367
  | Fun (n, vl)   -> horn_basic_app n (horn_val_to_expr self) vl
368

    
369
let no_reset_to_exprs machines m i =
370
  let (n,_) = List.assoc i m.minstances in
371
  let target_machine = List.find (fun m  -> m.mname.node_id = (Corelang.node_name n)) machines in
372

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

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

    
428
let instance_call_to_exprs machines reset_instances m i inputs outputs =
429
  let self = m.mname.node_id in
430
  try (* stateful node instance *)
431
    begin
432
      let (n,_) = List.assoc i m.minstances in
433
      let target_machine = List.find (fun m  -> m.mname.node_id = Corelang.node_name n) machines in
434

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

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

    
475
      | node_name_n ->
476
         let expr = 
477
           Z3.Expr.mk_app
478
             !ctx
479
             (get_fdecl (machine_step_name (node_name n)))
480
             ( (* Arguments are input, output, mid_mems, next_mems *)
481
               (
482
                 List.map (horn_val_to_expr self) (
483
                     inputs @
484
	               (List.map (fun v -> mk_val (LocalVar v) v.var_type) outputs)
485
                   )
486
               ) @ (
487
                 List.map (horn_var_to_expr) (mid_mems@next_mems)
488
	       )
489
             )
490
         in
491
         [expr]
492
      in
493

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

    
512

    
513
    
514
(* (\* Prints a [value] indexed by the suffix list [loop_vars] *\) *)
515
(* let rec value_suffix_to_expr self value = *)
516
(*  match value.value_desc with *)
517
(*  | Fun (n, vl)  ->  *)
518
(*     horn_basic_app n (horn_val_to_expr self) (value_suffix_to_expr self vl) *)
519
    
520
(*  |  _            -> *)
521
(*    horn_val_to_expr self value *)
522

    
523

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

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

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

    
590
      [e], branch_resets
591
	  
592
    in
593
    List.fold_left (fun (instrs, resets) b ->
594
      let b_instrs, b_resets = branch_to_expr b in
595
      instrs@b_instrs, resets@b_resets 
596
    ) ([], reset_instances) hl 
597

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

    
622

    
623
(*********************************************************)
624

    
625
(* Quantifiying universally all occuring variables *)
626
let add_rule ?(dont_touch=[]) vars  expr =
627
  (* let fds = Z3.Expr.get_args expr in *)
628
  (* Format.eprintf "Expr %s: args: [%a]@." *)
629
  (*   (Z3.Expr.to_string expr) *)
630
  (*   (Utils.fprintf_list ~sep:", " (fun fmt e -> Format.pp_print_string fmt (Z3.Expr.to_string e))) fds; *)
631

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

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

    
696
  (*
697
    TODO: bizarre la declaration de INIT tout seul semble poser pb.
698
  *) 
699
  Z3.Fixedpoint.add_rule !fp
700
    (Z3.Quantifier.expr_of_quantifier expr)
701
    None
702

    
703
 
704
(********************************************************)
705
    
706
let machine_reset machines m =
707
  let locals = local_memory_vars machines m in
708
  
709
  (* print "x_m = x_c" for each local memory *)
710
  let mid_mem_def =
711
    List.map (fun v ->
712
      Z3.Boolean.mk_eq !ctx
713
	(horn_var_to_expr (rename_mid v))
714
	(horn_var_to_expr (rename_current v))
715
    ) locals
716
  in
717

    
718
  (* print "child_reset ( associated vars _ {c,m} )" for each subnode.
719
     Special treatment for _arrow: _first = true
720
  *)
721

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

    
754
(*  TODO: empty list means true statement *)
755
let decl_machine machines m =
756
  if m.mname.node_id = Arrow.arrow_id then
757
    (* We don't do arrow function *)
758
    ()
759
  else
760
    begin
761
      let _ =
762
        List.map decl_var
763
      	  (
764
      	    (inout_vars machines m)@
765
      	      (rename_current_list (full_memory_vars machines m)) @
766
      	      (rename_mid_list (full_memory_vars machines m)) @
767
      	      (rename_next_list (full_memory_vars machines m)) @
768
      	      (rename_machine_list m.mname.node_id m.mstep.step_locals)
769
      	  )
770
      in
771
      
772
      if is_stateless m then
773
	begin
774
	  (* Declaring single predicate *)
775
	  let vars = inout_vars machines m in
776
	  let vars_types = List.map (fun v -> type_to_sort v.var_type) vars in
777
	  let _ = decl_rel (machine_stateless_name m.mname.node_id) vars_types in
778
	  let horn_body, _ (* don't care for reset here *) =
779
	    instrs_to_expr
780
	      machines
781
	      ([] (* No reset info for stateless nodes *) )
782
	      m
783
	      m.mstep.step_instrs
784
	  in
785
	  let horn_head = 
786
	    Z3.Expr.mk_app
787
	      !ctx
788
	      (get_fdecl (machine_stateless_name m.mname.node_id))
789
	      (List.map (horn_var_to_expr) vars)
790
	  in
791
	  let vars = vars@(rename_machine_list m.mname.node_id m.mstep.step_locals) in
792
	  match m.mstep.step_asserts with
793
	  | [] ->
794
	     begin
795
	       (* Rule for single predicate : "; Stateless step rule @." *)
796
	       let vars = rename_machine_list m.mname.node_id m.mstep.step_locals in
797
	       add_rule vars (Z3.Boolean.mk_implies !ctx horn_body horn_head)
798
		 
799
	     end
800
	  | assertsl ->
801
	     begin
802
	       (*Rule for step "; Stateless step rule with Assertions @.";*)
803
	       let body_with_asserts =
804
		 Z3.Boolean.mk_and !ctx (horn_body :: List.map (horn_val_to_expr m.mname.node_id) assertsl)
805
	       in
806
	       let vars = rename_machine_list m.mname.node_id m.mstep.step_locals in
807
	       add_rule vars (Z3.Boolean.mk_implies !ctx body_with_asserts horn_head)
808
	     end
809
	end
810
      else
811
	begin
812

    
813
	  (* Rule for reset *)
814

    
815
	  let vars = reset_vars machines m in
816
	  let vars_types = List.map (fun v -> type_to_sort v.var_type) vars in
817
	  let _ = decl_rel (machine_reset_name m.mname.node_id) vars_types in
818
	  let horn_reset_body = machine_reset machines m in	    
819
	  let horn_reset_head = 
820
	    Z3.Expr.mk_app
821
	      !ctx
822
	      (get_fdecl (machine_reset_name m.mname.node_id))
823
	      (List.map (horn_var_to_expr) vars)
824
	  in
825

    
826
	  
827
	  let _ =
828
	    add_rule vars (Z3.Boolean.mk_implies !ctx horn_reset_body horn_reset_head)
829
	      
830
	  in
831

    
832
	  (* Rule for step*)
833
	  let vars = step_vars machines m in
834
  	  let vars_types = List.map (fun v -> type_to_sort v.var_type) vars in
835
          let _ = decl_rel (machine_step_name m.mname.node_id) vars_types in
836
	  let horn_step_body, _ (* don't care for reset here *) =
837
	    instrs_to_expr
838
	      machines
839
	      []
840
	      m
841
	      m.mstep.step_instrs
842
	  in
843
	  let horn_step_head = 
844
	    Z3.Expr.mk_app
845
	      !ctx
846
	      (get_fdecl (machine_step_name m.mname.node_id))
847
	      (List.map (horn_var_to_expr) vars)
848
	  in
849
	  match m.mstep.step_asserts with
850
	  | [] ->
851
	     begin
852
	       (* Rule for single predicate *) 
853
	       let vars = (step_vars_c_m_x machines m) @(rename_machine_list m.mname.node_id m.mstep.step_locals) in
854
	       add_rule vars (Z3.Boolean.mk_implies !ctx horn_step_body horn_step_head)
855
		 
856
	     end
857
	  | assertsl ->
858
	     begin
859
	       (* Rule for step Assertions @.; *)
860
	       let body_with_asserts =
861
		 Z3.Boolean.mk_and !ctx
862
		   (horn_step_body :: List.map (horn_val_to_expr m.mname.node_id) assertsl)
863
	       in
864
	       let vars = (step_vars_c_m_x machines m) @(rename_machine_list m.mname.node_id m.mstep.step_locals) in
865
	       add_rule vars (Z3.Boolean.mk_implies !ctx body_with_asserts horn_step_head)
866
		 
867
	     end
868
     	       
869
	end
870
    end
871

    
872

    
873

    
874
(* Debug functions *)
875

    
876
let rec extract_expr_fds e =
877
  (* Format.eprintf "@[<v 2>Extracting fundecls from expr %s@ " *)
878
  (*   (Z3.Expr.to_string e); *)
879
  
880
  (* Removing quantifier is there are some *)
881
  let e = (* I didn't found a nicer way to do it than with an exception.  My
882
	     bad *)
883
    try
884
      let eq = Z3.Quantifier.quantifier_of_expr e in
885
      let e2 = Z3.Quantifier.get_body eq in
886
      (* Format.eprintf "Extracted quantifier body@ "; *)
887
      e2
888
	
889
    with _ -> Format.eprintf "No quantifier info@ "; e
890
  in
891
  let _ =
892
    try 
893
    (
894
      let fd = Z3.Expr.get_func_decl e in
895
      let fd_symbol = Z3.FuncDecl.get_name fd in
896
      let fd_name = Z3.Symbol.to_string fd_symbol in
897
      if not (Hashtbl.mem decls fd_name) then
898
	register_fdecl fd_name fd;
899
      (* Format.eprintf "fdecls (%s): %s@ " *)
900
      (* 	fd_name *)
901
      (* 	(Z3.FuncDecl.to_string fd); *)
902
      try
903
	(
904
	  let args = Z3.Expr.get_args e in
905
	  (* Format.eprintf "@[<v>@ "; *)
906
	  (* List.iter extract_expr_fds args; *)
907
	  (* Format.eprintf "@]@ "; *)
908
	  ()
909
	)
910
      with _ ->
911
	Format.eprintf "Impossible to extract fundecl args for expression %s@ "
912
	  (Z3.Expr.to_string e)
913
    )
914
  with _ ->
915
    Format.eprintf "Impossible to extract anything from expression %s@ "
916
      (Z3.Expr.to_string e)
917
  in
918
  (* Format.eprintf "@]@ " *)
919
  ()      
920

    
921
(* Local Variables: *)
922
(* compile-command:"make -C ../.." *)
923
(* End: *)