Project

General

Profile

Revision e4edf171

View differences:

configure.ac
79 79

  
80 80
# z3
81 81
AC_MSG_CHECKING(z3 library (optional))
82
define([z3path], esyscmd([ocamlfind query z3]))
82
define([z3path], esyscmd([ocamlfind query z3 | tr -d '\n']))
83 83

  
84 84
AS_IF([ocamlfind query z3 >/dev/null 2>&1],
85 85
    [z3=yes; AC_MSG_RESULT(yes)],[seal=no; AC_MSG_RESULT(no)],
src/backends/C/c_backend.ml
48 48
  (match !Options.main_node with
49 49
  | "" ->  () (* No main node: we do not generate main *)
50 50
  | main_node -> (
51
    match Machine_code_common.get_machine_opt main_node machines with
51
    match Machine_code_common.get_machine_opt machines main_node with
52 52
    | None -> begin
53 53
      Global.main_node := main_node;
54 54
      Format.eprintf "Code generation error: %a@." Error.pp_error_msg Error.Main_not_found;
......
70 70
  | "" ->  ()
71 71
  | mauve -> (
72 72
    (* looking for the main node *)
73
    match Machine_code_common.get_machine_opt mauve machines with
73
    match Machine_code_common.get_machine_opt machines mauve  with
74 74
    | None -> begin
75 75
      Global.main_node := mauve;
76 76
      Format.eprintf "Code generation error: %a@." Error.pp_error_msg Error.Main_not_found;
src/backends/Horn/horn_backend_collecting_sem.ml
49 49
  (* Init case *)
50 50
  let _ = 
51 51
    (* Special case when the main node is stateless *)
52
    if is_stateless machine then (
52
    if Machine_code_common.is_stateless machine then (
53 53
      let step_name = pp_machine_stateless_name in
54 54
      fprintf fmt "; Initial set: One Step(m,x)  -- Stateless node! @.";
55 55
      fprintf fmt "(declare-rel INIT_STATE ())@.";
......
86 86
  in
87 87

  
88 88
  let step_name = 
89
    if is_stateless machine then 
89
    if Machine_code_common.is_stateless machine then 
90 90
      pp_machine_stateless_name
91 91
    else
92 92
      pp_machine_step_name
......
142 142

  
143 143
    (* Special case when the cex node is stateless *)
144 144
  let reset_name, step_name =
145
    if is_stateless machine then
145
    if Machine_code_common.is_stateless machine then
146 146
      pp_machine_stateless_name, pp_machine_stateless_name
147 147
    else
148 148
      pp_machine_reset_name, pp_machine_step_name
src/backends/Horn/horn_backend_common.ml
14 14
open Machine_code_types
15 15
open Corelang
16 16

  
17
let get_machine = Machine_code_common.get_machine
18

  
17 19
let machine_reset_name id = id ^ "_reset"
18 20
let machine_step_name id = id ^ "_step" 
19 21
let machine_stateless_name id = id ^ "_fun" 
......
78 80
let rename_next = rename (fun n -> n ^ "_x")
79 81
let rename_next_list = List.map rename_next
80 82

  
81
let get_machine machines node_name =
82
(*  try *)
83
  List.find (fun m  -> m.mname.node_id = node_name) machines
84
(* with Not_found -> Format.eprintf "Unable to find machine %s in machines %a@.@?"  *)
85
(*   node_name *)
86
(*   (Utils.fprintf_list ~sep:", " (fun fmt m -> pp_print_string fmt m.mname.node_id)) machines *)
87
(*   ; assert false *)
88 83

  
89 84
let local_memory_vars machines machine =
90 85
  rename_machine_list machine.mname.node_id machine.mmemory
......
153 148
  @ (rename_mid_list (full_memory_vars machines m))
154 149

  
155 150

  
151

  
156 152
(* Local Variables: *)
157 153
(* compile-command:"make -C ../.." *)
158 154
(* End: *)
src/backends/Horn/horn_backend_printers.ml
419 419

  
420 420
(**************************************************************)
421 421

  
422
let is_stateless m = m.minstances = [] && m.mmemory = []
423 422

  
424 423
(* Print the machine m:
425 424
   two functions: m_init and m_step
src/machine_code_common.ml
116 116
let get_stateless_status m =
117 117
 (m.mname.node_dec_stateless, try Utils.desome m.mname.node_stateless with _ -> failwith ("stateless status of machine " ^ m.mname.node_id ^ " not computed"))
118 118

  
119
let is_stateless m = m.minstances = [] && m.mmemory = []
120

  
119 121
let is_input m id =
120 122
  List.exists (fun o -> o.var_id = id.var_id) m.mstep.step_inputs
121 123

  
......
223 225
    end
224 226

  
225 227

  
226
let get_machine_opt name machines =
228
let get_machine_opt machines name =
227 229
  List.fold_left
228 230
    (fun res m ->
229 231
      match res with
......
231 233
      | None -> if m.mname.node_id = name then Some m else None)
232 234
    None machines
233 235

  
236
let get_machine machines node_name =
237
 try
238
  List.find (fun m  -> m.mname.node_id = node_name) machines
239
 with Not_found -> Format.eprintf "Unable to find machine %s in machines %a@.@?"
240
   node_name
241
   (Utils.fprintf_list ~sep:", " (fun fmt m -> Format.pp_print_string fmt m.mname.node_id)) machines
242
   ; assert false
243
     
244
    
234 245
let get_const_assign m id =
235 246
  try
236 247
    match get_instr_desc (List.find
src/machine_code_common.mli
4 4
val is_const_value: Machine_code_types.value_t -> bool
5 5
val get_const_assign: Machine_code_types.machine_t -> Lustre_types.var_decl -> Machine_code_types.value_t
6 6
val get_stateless_status: Machine_code_types.machine_t -> bool * bool
7
val is_stateless: Machine_code_types.machine_t -> bool
7 8
val mk_val: Machine_code_types.value_t_desc -> Types.type_expr -> Machine_code_types.value_t
8 9
val mk_conditional: ?lustre_eq:Lustre_types.eq -> Machine_code_types.value_t -> Machine_code_types.instr_t list -> Machine_code_types.instr_t list -> Machine_code_types.instr_t
9 10
val empty_machine: Machine_code_types.machine_t
......
14 15
val pp_instr: Format.formatter -> Machine_code_types.instr_t -> unit
15 16
val pp_instrs: Format.formatter -> Machine_code_types.instr_t list -> unit
16 17
val pp_machines: Format.formatter -> Machine_code_types.machine_t list -> unit
17
val get_machine_opt: string -> Machine_code_types.machine_t list -> Machine_code_types.machine_t option
18
val get_machine_opt: Machine_code_types.machine_t list -> string -> Machine_code_types.machine_t option
19

  
20
(* Same function but fails if no such a machine  exists *)
21
val get_machine: Machine_code_types.machine_t list -> string -> Machine_code_types.machine_t
22

  
23
  
18 24
val get_node_def: string -> Machine_code_types.machine_t -> Lustre_types.node_desc
19 25
val join_guards_list: Machine_code_types.instr_t list -> Machine_code_types.instr_t list
src/tools/zustre_verifier.ml
1
open LustreSpec
2
open Machine_code
1
open Lustre_types
2
open Machine_code_types
3
open Machine_code_common
3 4
open Format
4 5
(* open Horn_backend_common
5 6
 * open Horn_backend *)
......
16 17
let rename_mid_list = HBC.rename_mid_list
17 18
let rename_next_list = HBC.rename_next_list
18 19
let full_memory_vars = HBC.full_memory_vars
19
   
20
let active = ref false
21
let ctx = ref (Z3.mk_context [])
20
let inout_vars = HBC.inout_vars
21
let reset_vars = HBC.reset_vars
22
let step_vars = HBC.step_vars
23
let local_memory_vars = HBC.local_memory_vars
24
  
22 25
let machine_reset_name = HBC.machine_reset_name 
23 26
let machine_stateless_name = HBC.machine_stateless_name 
24 27

  
28
let rename_mid = HBC.rename_mid
29

  
30
let preprocess = Horn_backend.preprocess
31
  
32
let active = ref false
33
let ctx = ref (Z3.mk_context [])
34
let fp = ref (Z3.Fixedpoint.mk_fixedpoint !ctx)
35

  
25 36
(** Sorts
26 37

  
27 38
A sort is introduced for each basic type and each enumerated type.
......
105 116
  
106 117

  
107 118

  
108
(** conversion functions
119
(** Conversion functions
109 120

  
110 121
The following is similar to the Horn backend. Each printing function
111 122
   is rephrased from pp_xx to xx_to_expr and produces a Z3 value.
......
168 179
   * | Types.Ttuple(l) -> assert false
169 180
   * |_ -> *) assert false
170 181

  
171

  
182
(* Conversion of basic library functions *)
183
    
172 184
let horn_basic_app i val_to_expr vl =
173 185
  match i, vl with
174 186
  | "ite", [v1; v2; v3] ->
......
445 457
    in
446 458
    [expr]
447 459
  )
460

  
461

  
462
    
463
(* (\* Prints a [value] indexed by the suffix list [loop_vars] *\) *)
464
(* let rec value_suffix_to_expr self value = *)
465
(*  match value.value_desc with *)
466
(*  | Fun (n, vl)  ->  *)
467
(*     horn_basic_app n (horn_val_to_expr self) (value_suffix_to_expr self vl) *)
448 468
    
469
(*  |  _            -> *)
470
(*    horn_val_to_expr self value *)
471

  
449 472

  
473
(* type_directed assignment: array vs. statically sized type
474
   - [var_type]: type of variable to be assigned
475
   - [var_name]: name of variable to be assigned
476
   - [value]: assigned value
477
   - [pp_var]: printer for variables
478
*)
479
let assign_to_exprs m var_name value =
480
  let self = m.mname.node_id in
481
  let e =
482
    Z3.Boolean.mk_eq
483
      !ctx
484
      (horn_val_to_expr ~is_lhs:true self var_name)
485
      (horn_val_to_expr self value)
486
  (* was: TODO deal with array accesses       (value_suffix_to_expr self value) *)
487
  in
488
  [e]
489

  
490
    
450 491
(* Convert instruction to Z3.Expr and update the set of reset instances *)
451
let rec instr_to_expr machines reset_instances (m: machine_t) instr : Z3.Expr.expr list * ident list =
492
let rec instr_to_exprs machines reset_instances (m: machine_t) instr : Z3.Expr.expr list * ident list =
452 493
  match Corelang.get_instr_desc instr with
453 494
  | MComment _ -> [], reset_instances
454 495
  | MNoReset i -> (* we assign middle_mem with mem_m. And declare i as reset *)
......
459 500
    i::reset_instances
460 501
  | MLocalAssign (i,v) ->
461 502
    assign_to_exprs
462
      m (horn_var_to_expr) 
503
      m  
463 504
      (mk_val (LocalVar i) i.var_type) v,
464 505
    reset_instances
465 506
  | MStateAssign (i,v) ->
466 507
    assign_to_exprs
467
      m (horn_var_to_expr) 
508
      m 
468 509
      (mk_val (StateVar i) i.var_type) v,
469 510
    reset_instances
470 511
  | MStep ([i0], i, vl) when Basic_library.is_internal_fun i (List.map (fun v -> v.value_type) vl) ->
......
487 528
       statement. *)
488 529
    let self = m.mname.node_id in
489 530
    let branch_to_expr (tag, instrs) =
490
      Z3.Boolean.mk_implies
491
        (Z3.Boolean.mk_eq !ctx 
492
           (horn_val_to_expr self g)
493
	   (horn_tag_to_expr tag))
494
        (machine_instrs_to_exprs machines reset_instances m instrs)
531
      let branch_def, branch_resets = instrs_to_expr machines reset_instances m instrs in
532
      let e =
533
	Z3.Boolean.mk_implies !ctx
534
          (Z3.Boolean.mk_eq !ctx 
535
             (horn_val_to_expr self g)
536
	     (horn_tag_to_expr tag))
537
          branch_def in
538

  
539
      [e], branch_resets
540
	  
495 541
    in
496
    List.map branch_to_expr hl,
497
    reset_instances 
542
    List.fold_left (fun (instrs, resets) b ->
543
      let b_instrs, b_resets = branch_to_expr b in
544
      instrs@b_instrs, resets@b_resets 
545
    ) ([], reset_instances) hl 
498 546

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

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

  
514

  
515
let basic_library_to_horn_expr i vl =
516
  match i, vl with
517
  | "ite", [v1; v2; v3] -> Format.fprintf fmt "(@[<hov 2>ite %a@ %a@ %a@])" pp_val v1 pp_val v2 pp_val v3
518

  
519
  | "uminus", [v] -> Format.fprintf fmt "(- %a)" pp_val v
520
  | "not", [v] -> Format.fprintf fmt "(not %a)" pp_val v
521
  | "=", [v1; v2] -> Format.fprintf fmt "(= %a %a)" pp_val v1 pp_val v2
522
  | "&&", [v1; v2] -> Format.fprintf fmt "(and %a %a)" pp_val v1 pp_val v2
523
  | "||", [v1; v2] -> Format.fprintf fmt "(or %a %a)" pp_val v1 pp_val v2
524
  | "impl", [v1; v2] -> Format.fprintf fmt "(=> %a %a)" pp_val v1 pp_val v2
525
  | "mod", [v1; v2] -> Format.fprintf fmt "(mod %a %a)" pp_val v1 pp_val v2
526
  | "equi", [v1; v2] -> Format.fprintf fmt "(%a = %a)" pp_val v1 pp_val v2
527
  | "xor", [v1; v2] -> Format.fprintf fmt "(%a xor %a)" pp_val v1 pp_val v2
528
  | "!=", [v1; v2] -> Format.fprintf fmt "(not (= %a %a))" pp_val v1 pp_val v2
529
  | "/", [v1; v2] -> Format.fprintf fmt "(div %a %a)" pp_val v1 pp_val v2
530
  | _, [v1; v2] -> Format.fprintf fmt "(%s %a %a)" i pp_val v1 pp_val v2
531
  | _ -> (Format.eprintf "internal error: Basic_library.pp_horn %s@." i; assert false)
532
(*  | "mod", [v1; v2] -> Format.fprintf fmt "(%a %% %a)" pp_val v1 pp_val v2
533

  
534
*)
548
  let instr_to_exprs rs i = instr_to_exprs machines rs m i in
549
  let e_list, rs = 
550
    match instrs with
551
    | [x] -> instr_to_exprs reset_instances x 
552
    | _::_ -> (* 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 *)
553
       
554
       List.fold_left (fun (exprs, rs) i -> 
555
         let exprs_i, rs_i = instr_to_exprs rs i in
556
         exprs@exprs_i, rs@rs_i
557
       )
558
         ([], reset_instances) instrs 
559
	 
560
	 
561
    | [] -> [], reset_instances
562
  in
563
  let e = 
564
    match e_list with
565
    | [e] -> e
566
    | [] -> Z3.Boolean.mk_true !ctx
567
    | _ -> Z3.Boolean.mk_and !ctx e_list
568
  in
569
  e, rs
535 570

  
536 571
        
537
(* Prints a [value] indexed by the suffix list [loop_vars] *)
538
let rec value_suffix_to_expr self value =
539
 match value.value_desc with
540
 | Fun (n, vl)  -> 
541
   basic_library_to_horn_expr n (value_suffix_to_expr self vl)
542
 |  _            ->
543
   horn_val_to_expr self value
572
let machine_reset machines m =
573
  let locals = local_memory_vars machines m in
574
  
575
  (* print "x_m = x_c" for each local memory *)
576
  let mid_mem_def =
577
    List.map (fun v ->
578
      Z3.Boolean.mk_eq !ctx
579
	(horn_var_to_expr (rename_mid v))
580
	(horn_var_to_expr (rename_current v))
581
    ) locals
582
  in
544 583

  
545
        
546
(* type_directed assignment: array vs. statically sized type
547
   - [var_type]: type of variable to be assigned
548
   - [var_name]: name of variable to be assigned
549
   - [value]: assigned value
550
   - [pp_var]: printer for variables
551
*)
552
let assign_to_exprs m var_name value =
553
  let self = m.mname.node_id in
554
  let e =
555
    Z3.Boolean.mk_eq
556
      !ctx
557
      (horn_val_to_expr ~is_lhs:true self var_name)
558
      (value_suffix_to_expr self value)
584
  (* print "child_reset ( associated vars _ {c,m} )" for each subnode.
585
     Special treatment for _arrow: _first = true
586
  *)
587

  
588
  let reset_instances =
589
    
590
    List.map (fun (id, (n, _)) ->
591
      let name = node_name n in
592
      if name = "_arrow" then (
593
	Z3.Boolean.mk_eq !ctx
594
	  (
595
	    let vdecl = get_fdecl ((concat m.mname.node_id id) ^ "._arrow._first_m") in
596
	    Z3.Expr.mk_const_f !ctx vdecl
597
	  )
598
	  (Z3.Boolean.mk_true !ctx)
599
	  
600
      ) else (
601
	let machine_n = get_machine machines name in 
602
	
603
	Z3.Expr.mk_app
604
	  !ctx
605
	  (get_fdecl (name ^ "_reset"))
606
	  (List.map (horn_var_to_expr)
607
	     (rename_machine_list (concat m.mname.node_id id) (reset_vars machines machine_n))
608
	  )
609
	  
610
      )
611
    ) m.minstances
612
      
613
      
559 614
  in
560
  [e]
615
  
616
  Z3.Boolean.mk_and !ctx (mid_mem_def @ reset_instances)
617
    
618
        
561 619

  
562
(*                TODO: empty list means true statement *)
620
(*  TODO: empty list means true statement *)
563 621
let decl_machine machines m =
564
  if m.Machine_code.mname.node_id = Machine_code.arrow_id then
565
    (* We don't print arrow function *)
622
  if m.mname.node_id = Arrow.arrow_id then
623
    (* We don't do arrow function *)
566 624
    ()
567 625
  else
568 626
    begin
......
571 629
      	  (
572 630
	    (inout_vars machines m)@
573 631
	      (rename_current_list (full_memory_vars machines m)) @
574
	        (rename_mid_list (full_memory_vars machines m)) @
575
	          (rename_next_list (full_memory_vars machines m)) @
576
	            (rename_machine_list m.mname.node_id m.mstep.step_locals)
632
	      (rename_mid_list (full_memory_vars machines m)) @
633
	      (rename_next_list (full_memory_vars machines m)) @
634
	      (rename_machine_list m.mname.node_id m.mstep.step_locals)
577 635
	  )
578 636
      in
579 637
      
580 638
      if is_stateless m then
581 639
	begin
582 640
	  (* Declaring single predicate *)
583
	  let _ = decl_rel (machine_stateless_name m.mname.node_id) (inout_vars machines m) in          
584
          match m.mstep.step_asserts with
641
	  let _ = decl_rel (machine_stateless_name m.mname.node_id) (inout_vars machines m) in
642
	  let horn_body, _ (* don't care for reset here *) =
643
	    instrs_to_expr
644
	      machines
645
	      ([] (* No reset info for stateless nodes *) )
646
	      m
647
	      m.mstep.step_instrs
648
	  in
649
	  let horn_head = 
650
	    Z3.Expr.mk_app
651
	      !ctx
652
	      (get_fdecl (machine_stateless_name m.mname.node_id))
653
	      (List.map (horn_var_to_expr) (inout_vars machines m))
654
	  in
655
	  match m.mstep.step_asserts with
585 656
	  | [] ->
586 657
	     begin
587

  
588
	       (* Rule for single predicate *)
589
	       fprintf fmt "; Stateless step rule @.";
590
	       fprintf fmt "@[<v 2>(rule (=> @ ";
591
	       ignore (pp_machine_instrs machines ([] (* No reset info for stateless nodes *) )  m fmt m.mstep.step_instrs);
592
	       fprintf fmt "@ (%a @[<v 0>%a)@]@]@.))@.@."
593
		 pp_machine_stateless_name m.mname.node_id
594
		 (Utils.fprintf_list ~sep:" " (horn_var_to_expr)) (inout_vars machines m);
658
	       (* Rule for single predicate : "; Stateless step rule @." *)
659
	       Z3.Fixedpoint.add_rule !fp
660
		 (Z3.Boolean.mk_implies !ctx horn_body horn_head)
661
		 None
595 662
	     end
596 663
	  | assertsl ->
597 664
	     begin
598
	       let pp_val = pp_horn_val ~is_lhs:true m.mname.node_id (horn_var_to_expr) in
599
	       
600
	       fprintf fmt "; Stateless step rule with Assertions @.";
601
	       (*Rule for step*)
602
	       fprintf fmt "@[<v 2>(rule (=> @ (and @ ";
603
	       ignore (pp_machine_instrs machines [] m fmt m.mstep.step_instrs);
604
	       fprintf fmt "@. %a)@ (%a @[<v 0>%a)@]@]@.))@.@." (pp_conj pp_val) assertsl
605
		 pp_machine_stateless_name m.mname.node_id
606
		 (Utils.fprintf_list ~sep:" " (horn_var_to_expr)) (step_vars machines m);
607
	  
665
	       (*Rule for step "; Stateless step rule with Assertions @.";*)
666
	       let body_with_asserts =
667
		 Z3.Boolean.mk_and !ctx (horn_body :: List.map (horn_val_to_expr m.mname.node_id) assertsl)
668
	       in
669
	       Z3.Fixedpoint.add_rule !fp
670
		 (Z3.Boolean.mk_implies !ctx body_with_asserts horn_head)
671
		 None
608 672
	     end
609
	       
610 673
	end
611 674
      else
612 675
	begin
......
615 678
          let _ = decl_rel (machine_step_name m.mname.node_id) (step_vars machines m) in
616 679

  
617 680
	  (* Rule for reset *)
618
	  fprintf fmt "@[<v 2>(rule (=> @ %a@ (%a @[<v 0>%a)@]@]@.))@.@."
619
	    (pp_machine_reset machines) m 
620
	    pp_machine_reset_name m.mname.node_id
621
	    (Utils.fprintf_list ~sep:"@ " (horn_var_to_expr)) (reset_vars machines m);
622 681

  
623
          match m.mstep.step_asserts with
682
	  let horn_reset_body = machine_reset machines m in	    
683
	  let horn_reset_head = 
684
	    Z3.Expr.mk_app
685
	      !ctx
686
	      (get_fdecl (machine_reset_name m.mname.node_id))
687
	      (List.map (horn_var_to_expr) (reset_vars machines m))
688
	  in
689
	  
690
	  let _ =
691
	    Z3.Fixedpoint.add_rule !fp
692
	      (Z3.Boolean.mk_implies !ctx horn_reset_body horn_reset_head)
693
	      None
694
	  in
695

  
696
	  (* Rule for step*)
697
	  let horn_step_body, _ (* don't care for reset here *) =
698
	    instrs_to_expr
699
	      machines
700
	      []
701
	      m
702
	      m.mstep.step_instrs
703
	  in
704
	  let horn_step_head = 
705
	    Z3.Expr.mk_app
706
	      !ctx
707
	      (get_fdecl (machine_step_name m.mname.node_id))
708
	      (List.map (horn_var_to_expr) (step_vars machines m))
709
	  in
710
	  match m.mstep.step_asserts with
624 711
	  | [] ->
625 712
	     begin
626
	       fprintf fmt "; Step rule @.";
627
	       (* Rule for step*)
628
	       fprintf fmt "@[<v 2>(rule (=> @ ";
629
	       ignore (pp_machine_instrs machines [] m fmt m.mstep.step_instrs);
630
	       fprintf fmt "@ (%a @[<v 0>%a)@]@]@.))@.@."
631
		 pp_machine_step_name m.mname.node_id
632
		 (Utils.fprintf_list ~sep:"@ " (horn_var_to_expr)) (step_vars machines m);
713
	       (* Rule for single predicate *)
714
	       Z3.Fixedpoint.add_rule !fp
715
		 (Z3.Boolean.mk_implies !ctx horn_step_body horn_step_head)
716
		 None
633 717
	     end
634
	  | assertsl -> 
718
	  | assertsl ->
635 719
	     begin
636
	       let pp_val = pp_horn_val ~is_lhs:true m.mname.node_id (horn_var_to_expr) in
637
	       (* print_string pp_val; *)
638
	       fprintf fmt "; Step rule with Assertions @.";
639
	       
640
	       (*Rule for step*)
641
	       fprintf fmt "@[<v 2>(rule (=> @ (and @ ";
642
	       ignore (pp_machine_instrs machines [] m fmt m.mstep.step_instrs);
643
	       fprintf fmt "@. %a)@ (%a @[<v 0>%a)@]@]@.))@.@." (pp_conj pp_val) assertsl
644
		 pp_machine_step_name m.mname.node_id
645
		 (Utils.fprintf_list ~sep:" " (horn_var_to_expr)) (step_vars machines m);
720
	       (* Rule for step Assertions @.; *)
721
	       let body_with_asserts =
722
		 Z3.Boolean.mk_and !ctx
723
		   (horn_step_body :: List.map (horn_val_to_expr m.mname.node_id) assertsl)
724
	       in
725
	       Z3.Fixedpoint.add_rule !fp
726
		 (Z3.Boolean.mk_implies !ctx body_with_asserts horn_step_head)
727
		 None
646 728
	     end
647
	       
648 729
     	       
649 730
	end
650 731
    end
......
679 760
      Backends.get_normalization_params ()
680 761

  
681 762
    let setup_solver () =
682
      let fp = Z3.Fixedpoint.mk_fixedpoint !ctx in
763
      fp := Z3.Fixedpoint.mk_fixedpoint !ctx;
683 764
      (* let help = Z3.Fixedpoint.get_help fp in
684 765
       * Format.eprintf "Fp help : %s@." help;
685 766
       * 
......
744 825
        P.add_bool params (mks "xform.inline_linear") false;
745 826
        P.add_bool params (mks "xform.inline_eager") false
746 827
      );
747
      Z3.Fixedpoint.set_parameters fp params
748
        
828
      Z3.Fixedpoint.set_parameters !fp params
829
              
749 830
      
750 831
    let run basename prog machines =
751
      let machines = Machine_code.arrow_machine::machines in
832
      let machines = Machine_code_common.arrow_machine::machines in
752 833
      let machines = preprocess machines in
753 834
      setup_solver ();
754 835
      decl_sorts ();
755 836
      List.iter (decl_machine machines) (List.rev machines);
756

  
757
      
758 837
      ()
838
      
839
      
759 840

  
760 841
  end: VerifierType.S)
761 842
    

Also available in: Unified diff