Project

General

Profile

Download (22.1 KB) Statistics
| Branch: | Tag: | Revision:
1
open LustreSpec
2
open Machine_code
3
open Format
4
(* open Horn_backend_common
5
 * open Horn_backend *)
6

    
7
module HBC = Horn_backend_common
8
let machine_step_name = HBC.machine_step_name
9
let node_name = HBC.node_name
10
let concat = HBC.concat
11
let rename_machine = HBC.rename_machine
12
let rename_machine_list = HBC.rename_machine_list
13
let rename_next = HBC.rename_next
14
let rename_current = HBC.rename_current
15
let rename_current_list = HBC.rename_current_list
16
let rename_mid_list = HBC.rename_mid_list
17
let rename_next_list = HBC.rename_next_list
18
let full_memory_vars = HBC.full_memory_vars
19
   
20
let active = ref false
21
let ctx = ref (Z3.mk_context [])
22
let machine_reset_name = HBC.machine_reset_name 
23

    
24
(** Sorts
25

    
26
A sort is introduced for each basic type and each enumerated type.
27

    
28
A hashtbl records these and allow easy access to sort values, when
29
   provided with a enumerated type name. 
30

    
31
*)
32
        
33
let bool_sort = Z3.Boolean.mk_sort !ctx
34
let int_sort = Z3.Arithmetic.Integer.mk_sort !ctx
35
let real_sort = Z3.Arithmetic.Real.mk_sort !ctx
36

    
37
let const_sorts = Hashtbl.create 13
38
let const_tags = Hashtbl.create 13
39
let sort_elems = Hashtbl.create 13
40

    
41
let get_const_sort = Hashtbl.find const_sorts 
42
let get_sort_elems = Hashtbl.find sort_elems
43
let get_tag_sort = Hashtbl.find const_tags
44
  
45

    
46
  
47
let decl_sorts () =
48
  Hashtbl.iter (fun typ decl ->
49
    match typ with
50
    | Tydec_const var ->
51
      (match decl.top_decl_desc with
52
      | TypeDef tdef -> (
53
	match tdef.tydef_desc with
54
	| Tydec_enum tl ->
55
	  let new_sort = Z3.Enumeration.mk_sort_s !ctx var tl in
56
          Hashtbl.add const_sorts var new_sort;
57
          Hashtbl.add sort_elems new_sort tl;
58
          List.iter (fun t -> Hashtbl.add const_tags t new_sort) tl
59
          
60
	| _ -> assert false
61
      )
62
      | _ -> assert false
63
      )
64
    | _        -> ()) Corelang.type_table
65

    
66
                 
67
let rec type_to_sort t =
68
  if Types.is_bool_type t  then bool_sort else
69
    if Types.is_int_type t then int_sort else 
70
  if Types.is_real_type t then real_sort else 
71
  match (Types.repr t).Types.tdesc with
72
  | Types.Tconst ty       -> get_const_sort ty
73
  | Types.Tclock t        -> type_to_sort t
74
  | Types.Tarray(dim,ty)   -> Z3.Z3Array.mk_sort !ctx int_sort (type_to_sort ty)
75
  | Types.Tstatic(d, ty)-> type_to_sort ty
76
  | Types.Tarrow _
77
  | _                     -> Format.eprintf "internal error: pp_type %a@."
78
                               Types.print_ty t; assert false
79

    
80
(** Func decls
81

    
82
Similarly fun_decls are registerd, by their name, into a hashtbl. The
83
   proposed encoding introduces a 0-ary fun_decl to model variables
84
   and fun_decl with arguments to declare reset and step predicates.
85

    
86

    
87

    
88
 *)
89
let decls = Hashtbl.create 13
90
let register_fdecl id fd = Hashtbl.add decls id fd
91
let get_fdecl id = Hashtbl.find decls id
92
                 
93
let decl_var id =
94
  let fdecl = Z3.FuncDecl.mk_func_decl_s !ctx id.var_id [] (type_to_sort id.var_type) in
95
  register_fdecl id.var_id fdecl;
96
  fdecl
97

    
98
let decl_rel name args =
99
  (*verifier ce qui est construit. On veut un declare-rel *)
100
  let args_sorts = List.map (fun v -> type_to_sort v.var_type) args in
101
  let fdecl = Z3.FuncDecl.mk_func_decl_s !ctx name args_sorts bool_sort in
102
  register_fdecl name fdecl;
103
  fdecl
104
  
105

    
106

    
107
(** conversion functions
108

    
109
The following is similar to the Horn backend. Each printing function
110
   is rephrased from pp_xx to xx_to_expr and produces a Z3 value.
111

    
112
 *)
113

    
114

    
115
(* Returns the f_decl associated to the variable v *)
116
let horn_var_to_expr v =
117
  Z3.Expr.mk_const_f !ctx (get_fdecl v.var_id)
118

    
119

    
120

    
121

    
122
  (* Used to print boolean constants *)
123
let horn_tag_to_expr t =
124
  if t = Corelang.tag_true then
125
    Z3.Boolean.mk_true !ctx
126
  else if t = Corelang.tag_false then
127
    Z3.Boolean.mk_false !ctx
128
  else
129
    (* Finding the associated sort *)
130
    let sort = get_tag_sort t in
131
    let elems = get_sort_elems sort in 
132
    let res : Z3.Expr.expr option =
133
      List.fold_left2 (fun res cst expr ->
134
          match res with
135
          | Some _ -> res
136
          | None -> if t = cst then Some (expr:Z3.Expr.expr) else None
137
        ) None elems (Z3.Enumeration.get_consts sort)
138
    in
139
    match res with None -> assert false | Some s -> s
140
    
141
(* Prints a constant value *)
142
let rec horn_const_to_expr c =
143
  match c with
144
    | Const_int i    -> Z3.Arithmetic.Integer.mk_numeral_i !ctx i
145
    | Const_real (_,_,s)   -> Z3.Arithmetic.Real.mk_numeral_i !ctx 0
146
    | Const_tag t    -> horn_tag_to_expr t
147
    | _              -> assert false
148

    
149

    
150

    
151
(* Default value for each type, used when building arrays. Eg integer array
152
   [2;7] is defined as (store (store (0) 1 7) 0 2) where 0 is this default value
153
   for the type integer (arrays).
154
*)
155
let rec horn_default_val t =
156
  let t = Types.dynamic_type t in
157
  if Types.is_bool_type t  then Z3.Boolean.mk_true !ctx else
158
  if Types.is_int_type t then Z3.Arithmetic.Integer.mk_numeral_i !ctx 0 else 
159
  if Types.is_real_type t then Z3.Arithmetic.Real.mk_numeral_i !ctx 0 else 
160
  (* match (Types.dynamic_type t).Types.tdesc with
161
   * | Types.Tarray(dim, l) -> (\* TODO PL: this strange code has to be (heavily) checked *\)
162
   *    let valt = Types.array_element_type t in
163
   *    fprintf fmt "((as const (Array Int %a)) %a)"
164
   *      pp_type valt 
165
   *      pp_default_val valt
166
   * | Types.Tstruct(l) -> assert false
167
   * | Types.Ttuple(l) -> assert false
168
   * |_ -> *) assert false
169

    
170

    
171
let horn_basic_app i val_to_expr vl =
172
  match i, vl with
173
  | "ite", [v1; v2; v3] ->
174
     Z3.Boolean.mk_ite
175
       !ctx
176
       (val_to_expr v1)
177
       (val_to_expr v2)
178
       (val_to_expr v3)
179

    
180
  | "uminus", [v] ->
181
     Z3.Arithmetic.mk_unary_minus
182
       !ctx
183
       (val_to_expr v)
184
  | "not", [v] ->
185
     Z3.Boolean.mk_not
186
       !ctx
187
       (val_to_expr v)
188
  | "=", [v1; v2] ->
189
     Z3.Boolean.mk_eq
190
       !ctx
191
       (val_to_expr v1)
192
       (val_to_expr v2)
193
  | "&&", [v1; v2] ->
194
     Z3.Boolean.mk_and
195
       !ctx
196
       [val_to_expr v1;
197
        val_to_expr v2]
198
  | "||", [v1; v2] ->
199
          Z3.Boolean.mk_or
200
       !ctx
201
       [val_to_expr v1;
202
        val_to_expr v2]
203

    
204
  | "impl", [v1; v2] ->
205
     Z3.Boolean.mk_implies
206
       !ctx
207
       (val_to_expr v1)
208
       (val_to_expr v2)
209
 | "mod", [v1; v2] ->
210
          Z3.Arithmetic.Integer.mk_mod
211
       !ctx
212
       (val_to_expr v1)
213
       (val_to_expr v2)
214
  | "equi", [v1; v2] ->
215
          Z3.Boolean.mk_eq
216
       !ctx
217
       (val_to_expr v1)
218
       (val_to_expr v2)
219
  | "xor", [v1; v2] ->
220
          Z3.Boolean.mk_xor
221
       !ctx
222
       (val_to_expr v1)
223
       (val_to_expr v2)
224
  | "!=", [v1; v2] ->
225
     Z3.Boolean.mk_not
226
       !ctx
227
       (
228
         Z3.Boolean.mk_eq
229
           !ctx
230
           (val_to_expr v1)
231
           (val_to_expr v2)
232
       )
233
  | "/", [v1; v2] ->
234
     Z3.Arithmetic.mk_div
235
       !ctx
236
       (val_to_expr v1)
237
       (val_to_expr v2)
238

    
239
  (* | _, [v1; v2] ->      Z3.Boolean.mk_and
240
   *      !ctx
241
   *      (val_to_expr v1)
242
   *      (val_to_expr v2)
243
   * 
244
   *      Format.fprintf fmt "(%s %a %a)" i val_to_exprr v1 val_to_expr v2 *)
245
  | _ -> (
246
    Format.eprintf
247
      "internal error: zustre unkown function %s@." i;
248
    assert false)
249

    
250
           
251
(* Convert a value expression [v], with internal function calls only.
252
   [pp_var] is a printer for variables (typically [pp_c_var_read]),
253
   but an offset suffix may be added for array variables
254
*)
255
let rec horn_val_to_expr ?(is_lhs=false) self v =
256
  match v.value_desc with
257
  | Cst c       -> horn_const_to_expr c
258

    
259
  (* Code specific for arrays *)
260
  | Array il    ->
261
     (* An array definition: 
262
	(store (
263
	  ...
264
 	    (store (
265
	       store (
266
	          default_val
267
	       ) 
268
	       idx_n val_n
269
	    ) 
270
	    idx_n-1 val_n-1)
271
	  ... 
272
	  idx_1 val_1
273
	) *)
274
     let rec build_array (tab, x) =
275
       match tab with
276
       | [] -> horn_default_val v.value_type(* (get_type v) *)
277
       | h::t ->
278
	  Z3.Z3Array.mk_store
279
            !ctx
280
	    (build_array (t, (x+1)))
281
	    (Z3.Arithmetic.Integer.mk_numeral_i !ctx x)
282
	    (horn_val_to_expr ~is_lhs:is_lhs self h)
283
     in
284
     build_array (il, 0)
285
       
286
  | Access(tab,index) ->
287
     Z3.Z3Array.mk_select !ctx 
288
       (horn_val_to_expr ~is_lhs:is_lhs self tab)
289
       (horn_val_to_expr ~is_lhs:is_lhs self index)
290

    
291
  (* Code specific for arrays *)
292
    
293
  | Power (v, n)  -> assert false
294
  | LocalVar v    ->
295
     horn_var_to_expr
296
       (rename_machine
297
          self
298
          v)
299
  | StateVar v    ->
300
     if Types.is_array_type v.var_type
301
     then assert false
302
     else horn_var_to_expr (rename_machine self ((if is_lhs then rename_next else rename_current) (* self *) v))
303
  | Fun (n, vl)   -> horn_basic_app n (horn_val_to_expr self) vl
304

    
305
let no_reset_to_exprs machines m i =
306
  let (n,_) = List.assoc i m.minstances in
307
  let target_machine = List.find (fun m  -> m.mname.node_id = (Corelang.node_name n)) machines in
308

    
309
  let m_list = 
310
    rename_machine_list
311
      (concat m.mname.node_id i)
312
      (rename_mid_list (full_memory_vars machines target_machine))
313
  in
314
  let c_list =
315
    rename_machine_list
316
      (concat m.mname.node_id i)
317
      (rename_current_list (full_memory_vars machines target_machine))
318
  in
319
  match c_list, m_list with
320
  | [chd], [mhd] ->
321
     let expr =
322
       Z3.Boolean.mk_eq !ctx 
323
         (horn_var_to_expr mhd)
324
         (horn_var_to_expr chd)
325
     in
326
     [expr]
327
  | _ -> (
328
    let exprs =
329
      List.map2 (fun mhd chd -> 
330
          Z3.Boolean.mk_eq !ctx 
331
            (horn_var_to_expr mhd)
332
            (horn_var_to_expr chd)
333
        )
334
        m_list
335
        c_list
336
    in
337
    exprs
338
  )
339

    
340
let instance_reset_to_exprs machines m i =
341
  let (n,_) = List.assoc i m.minstances in
342
  let target_machine = List.find (fun m  -> m.mname.node_id = (Corelang.node_name n)) machines in
343
  let vars =
344
    (
345
      (rename_machine_list
346
	 (concat m.mname.node_id i)
347
	 (rename_current_list (full_memory_vars machines target_machine))
348
      ) 
349
      @
350
	(rename_machine_list
351
	   (concat m.mname.node_id i)
352
	   (rename_mid_list (full_memory_vars machines target_machine))
353
	)
354
    )
355
  in
356
  let expr =
357
    Z3.Expr.mk_app
358
      !ctx
359
      (get_fdecl (machine_reset_name (Corelang.node_name n)))
360
      (List.map (horn_var_to_expr) vars)
361
  in
362
  [expr]
363

    
364
let instance_call_to_exprs machines reset_instances m i inputs outputs =
365
  let self = m.mname.node_id in
366
  try (* stateful node instance *)
367
    begin
368
      let (n,_) = List.assoc i m.minstances in
369
      let target_machine = List.find (fun m  -> m.mname.node_id = Corelang.node_name n) machines in
370

    
371
      (* Checking whether this specific instances has been reset yet *)
372
      let reset_exprs = 
373
        if not (List.mem i reset_instances) then
374
	  (* If not, declare mem_m = mem_c *)
375
	  no_reset_to_exprs machines m i
376
        else
377
          [] (* Nothing to add yet *)
378
      in
379
      
380
      let mems = full_memory_vars machines target_machine in
381
      let rename_mems f = rename_machine_list (concat m.mname.node_id i) (f mems) in
382
      let mid_mems = rename_mems rename_mid_list in
383
      let next_mems = rename_mems rename_next_list in
384

    
385
      let call_expr = 
386
      match Corelang.node_name n, inputs, outputs, mid_mems, next_mems with
387
      | "_arrow", [i1; i2], [o], [mem_m], [mem_x] -> begin
388
          let stmt1 = (* out = ite mem_m then i1 else i2 *)
389
            Z3.Boolean.mk_eq !ctx
390
              ( (* output var *)
391
                horn_val_to_expr
392
                  ~is_lhs:true
393
                  self
394
                  (mk_val (LocalVar o) o.var_type)
395
              )
396
              (
397
                Z3.Boolean.mk_ite !ctx 
398
	          (horn_var_to_expr mem_m) 
399
	          (horn_val_to_expr self i1)
400
	          (horn_val_to_expr self i2)
401
              )
402
          in
403
          let stmt2 = (* mem_X = false *)
404
            Z3.Boolean.mk_eq !ctx
405
	      (horn_var_to_expr mem_x)
406
              (Z3.Boolean.mk_false !ctx)
407
          in
408
          [stmt1; stmt2]
409
      end
410

    
411
      | node_name_n ->
412
         let expr = 
413
           Z3.Expr.mk_app
414
             !ctx
415
             (get_fdecl (machine_step_name (node_name n)))
416
             ( (* Arguments are input, output, mid_mems, next_mems *)
417
               (
418
                 List.map (horn_val_to_expr self (pp_horn_var m)) (
419
                     inputs @
420
	               (List.map (fun v -> mk_val (LocalVar v) v.var_type) outputs)
421
                   )
422
               ) @ (
423
                 List.map (horn_var_to_expr) (mid_mems@next_mems)
424
	       )
425
             )
426
         in
427
         [expr]
428
      in
429

    
430
      reset_exprs@call_expr
431
    end
432
  with Not_found -> ( (* stateless node instance *)
433
    let (n,_) = List.assoc i m.mcalls in
434
    let expr = 
435
      Z3.Expr.mk_app
436
        !ctx
437
        (get_fdecl (machine_stateless_name (node_name n)))
438
        ((* Arguments are inputs, outputs *)
439
         List.map (horn_val_to_expr self)
440
           (
441
             inputs @ (List.map (fun v -> mk_val (LocalVar v) v.var_type) outputs)
442
           )
443
        )
444
    in
445
    [expr]
446
  )
447
    
448

    
449
(* Convert instruction to Z3.Expr and update the set of reset instances *)
450
let rec instr_to_expr machines reset_instances (m: machine_t) instr : expr list * ident list =
451
  match get_instr_desc instr with
452
  | MComment _ -> [], reset_instances
453
  | MNoReset i -> (* we assign middle_mem with mem_m. And declare i as reset *)
454
    no_reset_to_exprs machines m i,
455
    i::reset_instances
456
  | MReset i -> (* we assign middle_mem with reset: reset(mem_m) *)
457
    instance_reset_to_exprs machines m i,
458
    i::reset_instances
459
  | MLocalAssign (i,v) ->
460
    assign_to_exprs
461
      m (horn_var_to_expr) 
462
      (mk_val (LocalVar i) i.var_type) v,
463
    reset_instances
464
  | MStateAssign (i,v) ->
465
    assign_to_exprs
466
      m (horn_var_to_expr) 
467
      (mk_val (StateVar i) i.var_type) v,
468
    reset_instances
469
  | MStep ([i0], i, vl) when Basic_library.is_internal_fun i (List.map (fun v -> v.value_type) vl) ->
470
    assert false (* This should not happen anymore *)
471
  | MStep (il, i, vl) ->
472
    (* if reset instance, just print the call over mem_m , otherwise declare mem_m =
473
       mem_c and print the call to mem_m *)
474
    instance_call_to_exprs machines reset_instances m i vl il,
475
    reset_instances (* Since this instance call will only happen once, we
476
		       don't have to update reset_instances *)
477

    
478
  | MBranch (g,hl) -> (* (g = tag1 => expr1) and (g = tag2 => expr2) ...
479
			 should not be produced yet. Later, we will have to
480
			 compare the reset_instances of each branch and
481
			 introduced the mem_m = mem_c for branches to do not
482
			 address it while other did. Am I clear ? *)
483
    (* For each branch we obtain the logical encoding, and the information
484
       whether a sub node has been reset or not. If a node has been reset in one
485
       of the branch, then all others have to have the mem_m = mem_c
486
       statement. *)
487
    let self = m.mname.node_id in
488
    let branch_to_expr (tag, instrs) =
489
      Z3.Boolean.mk_implies
490
        (Z3.Boolean.mk_eq !ctx 
491
           (horn_val_to_expr self g)
492
	   (horn_tag_to_expr tag))
493
        (machine_instrs_to_exprs machines reset_instances m instrs)
494
    in
495
    List.map branch_to_expr hl,
496
    reset_instances 
497

    
498
and instrs_to_expr machines reset_instances m instrs = 
499
  let instr_to_expr rs i = instr_to_expr machines rs m i in
500
  match instrs with
501
  | [x] -> instr_to_expres reset_instances x 
502
  | _::_ -> (* 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 *)
503

    
504
      List.fold_left (fun (exprs, rs) i -> 
505
          let exprs_i, rs = ppi rs i in
506
          expr@exprs_i, rs
507
        )
508
        ([], reset_instances) instrs 
509
    
510
    
511
  | [] -> [], reset_instances
512

    
513

    
514
(*                TODO: empty list means true statement *)
515
let decl_machine machines m =
516
  if m.Machine_code.mname.node_id = Machine_code.arrow_id then
517
    (* We don't print arrow function *)
518
    ()
519
  else
520
    begin
521
      let vars =
522
        List.map decl_var 
523
      	  (
524
	    (inout_vars machines m)@
525
	      (rename_current_list (full_memory_vars machines m)) @
526
	        (rename_mid_list (full_memory_vars machines m)) @
527
	          (rename_next_list (full_memory_vars machines m)) @
528
	            (rename_machine_list m.mname.node_id m.mstep.step_locals)
529
	  )
530
      in
531
      
532
      if is_stateless m then
533
	begin
534
	  (* Declaring single predicate *)
535
	  let _ = decl_rel (machine_stateless_name m.mname.node_id) (inout_vars machines m) in          
536
          match m.mstep.step_asserts with
537
	  | [] ->
538
	     begin
539

    
540
	       (* Rule for single predicate *)
541
	       fprintf fmt "; Stateless step rule @.";
542
	       fprintf fmt "@[<v 2>(rule (=> @ ";
543
	       ignore (pp_machine_instrs machines ([] (* No reset info for stateless nodes *) )  m fmt m.mstep.step_instrs);
544
	       fprintf fmt "@ (%a @[<v 0>%a)@]@]@.))@.@."
545
		 pp_machine_stateless_name m.mname.node_id
546
		 (Utils.fprintf_list ~sep:" " (horn_var_to_expr)) (inout_vars machines m);
547
	     end
548
	  | assertsl ->
549
	     begin
550
	       let pp_val = pp_horn_val ~is_lhs:true m.mname.node_id (horn_var_to_expr) in
551
	       
552
	       fprintf fmt "; Stateless step rule with Assertions @.";
553
	       (*Rule for step*)
554
	       fprintf fmt "@[<v 2>(rule (=> @ (and @ ";
555
	       ignore (pp_machine_instrs machines [] m fmt m.mstep.step_instrs);
556
	       fprintf fmt "@. %a)@ (%a @[<v 0>%a)@]@]@.))@.@." (pp_conj pp_val) assertsl
557
		 pp_machine_stateless_name m.mname.node_id
558
		 (Utils.fprintf_list ~sep:" " (horn_var_to_expr)) (step_vars machines m);
559
	  
560
	     end
561
	       
562
	end
563
      else
564
	begin
565
	  (* Declaring predicate *)
566
	  let _ = decl_rel (machine_reset_name m.mname.node_id) (reset_vars machines m) in
567
          let _ = decl_rel (machine_step_name m.mname.node_id) (step_vars machines m) in
568

    
569
	  (* Rule for reset *)
570
	  fprintf fmt "@[<v 2>(rule (=> @ %a@ (%a @[<v 0>%a)@]@]@.))@.@."
571
	    (pp_machine_reset machines) m 
572
	    pp_machine_reset_name m.mname.node_id
573
	    (Utils.fprintf_list ~sep:"@ " (horn_var_to_expr)) (reset_vars machines m);
574

    
575
          match m.mstep.step_asserts with
576
	  | [] ->
577
	     begin
578
	       fprintf fmt "; Step rule @.";
579
	       (* Rule for step*)
580
	       fprintf fmt "@[<v 2>(rule (=> @ ";
581
	       ignore (pp_machine_instrs machines [] m fmt m.mstep.step_instrs);
582
	       fprintf fmt "@ (%a @[<v 0>%a)@]@]@.))@.@."
583
		 pp_machine_step_name m.mname.node_id
584
		 (Utils.fprintf_list ~sep:"@ " (horn_var_to_expr)) (step_vars machines m);
585
	     end
586
	  | assertsl -> 
587
	     begin
588
	       let pp_val = pp_horn_val ~is_lhs:true m.mname.node_id (horn_var_to_expr) in
589
	       (* print_string pp_val; *)
590
	       fprintf fmt "; Step rule with Assertions @.";
591
	       
592
	       (*Rule for step*)
593
	       fprintf fmt "@[<v 2>(rule (=> @ (and @ ";
594
	       ignore (pp_machine_instrs machines [] m fmt m.mstep.step_instrs);
595
	       fprintf fmt "@. %a)@ (%a @[<v 0>%a)@]@]@.))@.@." (pp_conj pp_val) assertsl
596
		 pp_machine_step_name m.mname.node_id
597
		 (Utils.fprintf_list ~sep:" " (horn_var_to_expr)) (step_vars machines m);
598
	     end
599
	       
600
     	       
601
	end
602
    end
603

    
604
let param_stat = ref false
605
let param_eldarica = ref false
606
let param_utvpi = ref false
607
let param_tosmt = ref false
608
let param_pp = ref false
609
             
610
module Verifier =
611
  (struct
612
    include VerifierType.Default
613
    let name = "zustre"
614
    let options = [
615
        "-stat", Arg.Set param_stat, "print statistics";
616
        "-eldarica", Arg.Set param_eldarica, "deactivate fixedpoint extensions when printing rules";
617
        "-no_utvpi", Arg.Set param_utvpi, "Deactivate UTVPI strategy";
618
        "-tosmt", Arg.Set param_tosmt, "Print low-level (possibly unreadable) SMT2 statements";
619
        "-no-pp", Arg.Set param_pp, "No preprocessing (inlining and slicing)";
620
      ]
621
                
622
    let activate () = (
623
        active := true;
624
        Options.output := "horn";
625
      )
626
    let is_active () = !active
627

    
628
    let get_normalization_params () =
629
      (* make sure the output is "Horn" *)
630
      assert(!Options.output = "horn");
631
      Backends.get_normalization_params ()
632

    
633
    let setup_solver () =
634
      let fp = Z3.Fixedpoint.mk_fixedpoint !ctx in
635
      (* let help = Z3.Fixedpoint.get_help fp in
636
       * Format.eprintf "Fp help : %s@." help;
637
       * 
638
       * let solver =Z3.Solver.mk_solver !ctx None in
639
       * let help = Z3.Solver.get_help solver in
640
       * Format.eprintf "Z3 help : %s@." help; *)
641
      
642
      let module P = Z3.Params in
643
      let module S = Z3.Symbol in
644
      let mks = S.mk_string !ctx in
645
      let params = P.mk_params !ctx in
646

    
647
      (* self.fp.set (engine='spacer') *)
648
      P.add_symbol params (mks "engine") (mks "spacer");
649
      
650
       (* #z3.set_option(rational_to_decimal=True) *)
651
       (* #self.fp.set('precision',30) *)
652
      if !param_stat then 
653
        (* self.fp.set('print_statistics',True) *)
654
        P.add_bool params (mks "print_statistics") true;
655

    
656
      (* Dont know where to find this parameter *)
657
      (* if !param_spacer_verbose then
658
         *   if self.args.spacer_verbose: 
659
         *        z3.set_option (verbose=1) *)
660

    
661
      (* The option is not recogined*)
662
      (* self.fp.set('use_heavy_mev',True) *)
663
      (* P.add_bool params (mks "use_heavy_mev") true; *)
664
      
665
      (* self.fp.set('pdr.flexible_trace',True) *)
666
      P.add_bool params (mks "pdr.flexible_trace") true;
667

    
668
      (* self.fp.set('reset_obligation_queue',False) *)
669
      P.add_bool params (mks "spacer.reset_obligation_queue") false;
670

    
671
      (* self.fp.set('spacer.elim_aux',False) *)
672
      P.add_bool params (mks "spacer.elim_aux") false;
673

    
674
      (* if self.args.eldarica:
675
        *     self.fp.set('print_fixedpoint_extensions', False) *)
676
      if !param_eldarica then
677
        P.add_bool params (mks "print_fixedpoint_extensions") false;
678
      
679
      (* if self.args.utvpi: self.fp.set('pdr.utvpi', False) *)
680
      if !param_utvpi then
681
        P.add_bool params (mks "pdr.utvpi") false;
682

    
683
      (* if self.args.tosmt:
684
       *        self.log.info("Setting low level printing")
685
       *        self.fp.set ('print.low_level_smt2',True) *)
686
      if !param_tosmt then
687
        P.add_bool params (mks "print.low_level_smt2") true;
688

    
689
      (* if not self.args.pp:
690
       *        self.log.info("No pre-processing")
691
       *        self.fp.set ('xform.slice', False)
692
       *        self.fp.set ('xform.inline_linear',False)
693
       *        self.fp.set ('xform.inline_eager',False) *\) *)
694
      if !param_pp then (
695
        P.add_bool params (mks "xform.slice") false;
696
        P.add_bool params (mks "xform.inline_linear") false;
697
        P.add_bool params (mks "xform.inline_eager") false
698
      );
699
      Z3.Fixedpoint.set_parameters fp params
700
        
701
      
702
    let run basename prog machines =
703
      let machines = Machine_code.arrow_machine::machines in
704
      let machines = preprocess machines in
705
      setup_solver ();
706
      decl_sorts ();
707
      List.iter (decl_machine machines) (List.rev machines);
708

    
709
      
710
      ()
711

    
712
  end: VerifierType.S)
713
    
(2-2/2)