Project

General

Profile

« Previous | Next » 

Revision 51ec4e8c

Added by Pierre-Loïc Garoche almost 4 years ago

Try to debug the use of Z3 API. Still having troubles

View differences:

src/tools/zustre/zustre_analyze.ml
48 48
			 decl_init
49 49
			 []
50 50
  )  in
51
  
51

  
52
  (* Re-declaring variables *)
53
  let _ = List.map decl_var main_memory_next in
54

  
52 55
  let horn_head = 
53 56
    Z3.Expr.mk_app
54 57
      !ctx
......
65 68

  
66 69
	(* Note that vars here contains main_memory_next *)
67 70
	let vars = step_vars_m_x machines machine in
71
	(* Re-declaring variables *)
72
	let _ = List.map decl_var vars in
68 73
	
69 74
	let horn_body =
70 75
	  Z3.Boolean.mk_and !ctx
......
82 87
    else
83 88
      begin
84 89
	(* Initial set: Reset(c,m) + One Step(m,x) @. *)
90

  
91
	(* Re-declaring variables *)
92
	let vars_reset = reset_vars machines machine in
93
	let vars_step = step_vars_m_x machines machine in
94
	let vars_step_all = step_vars_c_m_x machines machine in
95
	let _ = List.map decl_var (vars_reset @ vars_step @ vars_step_all ) in
96

  
85 97
	(* rule => (INIT_STATE and reset(mid) and step(mid, next)) MAIN(next) *)
86 98
	let horn_body =
87 99
	  Z3.Boolean.mk_and !ctx
src/tools/zustre/zustre_common.ml
104 104
  try
105 105
    Hashtbl.find decls id
106 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

  
107 112
    
108 113
let decl_var id =
109 114
  Format.eprintf "Declaring var %s@." id.var_id;
......
120 125
  fdecl
121 126
  
122 127

  
123
(* Quantifiying universally all occuring variables *)
124
let add_rule ?(dont_touch=[]) vars expr =
125
  (* let fds = Z3.Expr.get_args expr in *)
126
  (* Format.eprintf "Expr %s: args: [%a]@." *)
127
  (*   (Z3.Expr.to_string expr) *)
128
  (*   (Utils.fprintf_list ~sep:", " (fun fmt e -> Format.pp_print_string fmt (Z3.Expr.to_string e))) fds; *)
129

  
130
  (* Old code relying on provided vars *)
131
  let sorts = (List.map (fun id -> type_to_sort id.var_type) vars) in
132
  let symbols = (List.map (fun id -> Z3.FuncDecl.get_name (get_fdecl id.var_id)) vars) in
133
  
134
  (* New code: we extract vars from expr *)
135
  let module FDSet = Set.Make (struct type t = Z3.FuncDecl.func_decl
136
				      let compare = compare
137
				      let hash = Hashtbl.hash
138
  end)
139
  in
140
  let rec get_expr_vars e =
141
    let open Utils in
142
    let nb_args = Z3.Expr.get_num_args e in
143
    if nb_args <= 0 then (
144
      let fdecl = Z3.Expr.get_func_decl e in
145
      (* let params = Z3.FuncDecl.get_parameters fdecl in *)
146
      Format.eprintf "Extracting info about %s: [@?" (Z3.Expr.to_string e);
147
      let dkind = Z3.FuncDecl.get_decl_kind fdecl in
148
      match dkind with Z3enums.OP_UNINTERPRETED -> (
149
	(* Format.eprintf "kind = %s, " (match dkind with Z3enums.OP_TRUE -> "true" | Z3enums.OP_UNINTERPRETED -> "uninter"); *)
150
	(* let open Z3.FuncDecl.Parameter in *)
151
	(* List.iter (fun p -> *)
152
	(*   match p with *)
153
        (*     P_Int i -> Format.eprintf "int %i" i *)
154
	(*   | P_Dbl f -> Format.eprintf "dbl %f" f *)
155
	(*   | P_Sym s -> Format.eprintf "symb"  *)
156
	(*   | P_Srt s -> Format.eprintf "sort"  *)
157
	(*   | P_Ast _ ->Format.eprintf "ast"  *)
158
	(*   | P_Fdl f -> Format.eprintf "fundecl"  *)
159
	(*   | P_Rat s -> Format.eprintf "rat %s" s  *)
160
	     
161
	(* ) params; *)
162
	(* Format.eprintf "]@."; *)
163
	FDSet.singleton fdecl
164
      )
165
      | _ -> FDSet.empty
166
    )
167
    else (*if nb_args > 0 then*)
168
      List.fold_left
169
	(fun accu e ->  FDSet.union accu (get_expr_vars e))
170
	FDSet.empty (Z3.Expr.get_args e)
171
  in
172
  let vars = FDSet.elements (FDSet.diff (get_expr_vars expr) (FDSet.of_list dont_touch)) in
173
  let sorts = List.map Z3.FuncDecl.get_range vars in
174
  let symbols = List.map Z3.FuncDecl.get_name vars in
175
  
176
  let expr = Z3.Quantifier.mk_forall
177
    !ctx  (* context *)
178
    sorts           (* sort list*)
179
    symbols (* symbol list *)
180
    expr (* expression *)
181
    None (* quantifier weight, None means 1 *)
182
    [] (* pattern list ? *)
183
    [] (* ? *)
184
    None (* ? *)
185
    None (* ? *)
186
  in
187
  Z3.Fixedpoint.add_rule !fp
188
    (Z3.Quantifier.expr_of_quantifier expr)
189
    None
190

  
191

  
192 128
(** Conversion functions
193 129

  
194 130
The following is similar to the Horn backend. Each printing function
......
682 618
  in
683 619
  e, rs
684 620

  
685
        
621

  
622
(*********************************************************)
623

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

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

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

  
695

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

  
702
(********************************************************)
703
    
686 704
let machine_reset machines m =
687 705
  let locals = local_memory_vars machines m in
688 706
  
......
772 790
	  | [] ->
773 791
	     begin
774 792
	       (* Rule for single predicate : "; Stateless step rule @." *)
793
	       let vars = rename_machine_list m.mname.node_id m.mstep.step_locals in
775 794
	       add_rule vars (Z3.Boolean.mk_implies !ctx horn_body horn_head)
776 795
		 
777 796
	     end
......
781 800
	       let body_with_asserts =
782 801
		 Z3.Boolean.mk_and !ctx (horn_body :: List.map (horn_val_to_expr m.mname.node_id) assertsl)
783 802
	       in
803
	       let vars = rename_machine_list m.mname.node_id m.mstep.step_locals in
784 804
	       add_rule vars (Z3.Boolean.mk_implies !ctx body_with_asserts horn_head)
785 805
	     end
786 806
	end
......
798 818
	      (get_fdecl (machine_reset_name m.mname.node_id))
799 819
	      (List.map (horn_var_to_expr) vars)
800 820
	  in
821

  
801 822
	  
802 823
	  let _ =
803 824
	    add_rule vars (Z3.Boolean.mk_implies !ctx horn_reset_body horn_reset_head)
......
844 865
    end
845 866

  
846 867

  
868

  
869
(* Debug functions *)
870

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

  
847 915
(* Local Variables: *)
848 916
(* compile-command:"make -C ../.." *)
849 917
(* End: *)
src/tools/zustre/zustre_test.ml
1
(* Example of a use of Z3 Fixedpoint that doesn't work 
2
   The file is self-contained and shall be compiled as follow:
3

  
4
   in File _tags, add the simple line
5
   <**/*>: package(z3)
6

  
7
   Then compile as
8
   ocamlbuild -use-ocamlfind zustre_test.native
9

  
10
   We obtain the following output:
11
   $ ./zustre_test.native 
12
   Registered rules:
13
     Rule: (forall ((x Int) (y Int)) (=> (= x y) (f x y)))  
14
     Rule: INIT_STATE
15
     Rule: (forall ((x Int) (y Int)) (=> (and (f x y) INIT_STATE) (MAIN x y)))
16
     Rule: (forall ((x Int) (y Int)) (=> (and (not (= x y)) (MAIN x y)) ERR))
17
     
18
   Fatal error: exception Z3.Error("Uninterpreted 'y' in <null>:
19
   f(#0,#1) :- 
20
     (= (:var 1) y),
21
     (= (:var 0) x),
22
     (= x y).
23
   ")
24

  
25
*)
26

  
27

  
28

  
29
let rec fprintf_list ~sep:sep f fmt = function
30
  | []   -> ()
31
  | [e]  -> f fmt e
32
  | x::r -> Format.fprintf fmt "%a%(%)%a" f x sep (fprintf_list ~sep f) r
33

  
34
(* Global references to declare Z3 context and Fixedpoint engine *)
35
     
36
let ctx = ref (Z3.mk_context [])
37
let fp = ref (Z3.Fixedpoint.mk_fixedpoint !ctx)
38

  
39
(* Shortcuts to basic sorts *)
40

  
41
let bool_sort = Z3.Boolean.mk_sort !ctx
42
let int_sort = Z3.Arithmetic.Integer.mk_sort !ctx
43
let real_sort = Z3.Arithmetic.Real.mk_sort !ctx
44

  
45
  
46
let _ =
47

  
48

  
49
  (* Setting up the fixed point engine *)
50
  fp := Z3.Fixedpoint.mk_fixedpoint !ctx;
51
  let module P = Z3.Params in
52
  let module S = Z3.Symbol in
53
  let mks = S.mk_string !ctx in
54
  let params = P.mk_params !ctx in
55
  P.add_symbol params (mks "engine") (mks "spacer");
56
  Z3.Fixedpoint.set_parameters !fp params;
57

  
58
  (* Three rules 
59
     R1: (x = y) => f(x,y)
60
     R2: INIT and f(x,y) => MAIN(x,y)
61
     R3: x!=y and MAIN(x,y) => ERR(x,y)
62
     INIT is assumed as the beginning
63

  
64
     Querying ERR shall be unsat since the only valid MAIN(x,y) are x=y and
65
     therefore ERR is unsat.
66
  *)
67
  
68
  (* Simple rule : forall x, y, (x=y => f(x,y)) *)
69
  let x = Z3.FuncDecl.mk_func_decl_s !ctx "x" [] int_sort in
70
  let y = Z3.FuncDecl.mk_func_decl_s !ctx "y" [] int_sort in
71
  let x_expr = Z3.Expr.mk_const_f !ctx x in
72
  let y_expr = Z3.Expr.mk_const_f !ctx y in
73
  
74
  let decl_f = Z3.FuncDecl.mk_func_decl_s !ctx "f" [int_sort; int_sort] bool_sort in
75
  Z3.Fixedpoint.register_relation !fp decl_f; (* since f appears in the rhs of a rule *)
76
  let f_x_y_expr = Z3.Expr.mk_app !ctx decl_f [x_expr; y_expr] in
77
  let x_eq_y_expr = Z3.Boolean.mk_eq !ctx x_expr y_expr in
78
  
79
  let expr_f_lhs = (* x = y *)
80
    x_eq_y_expr 
81
  in
82
  let expr_f_rhs = f_x_y_expr in
83
  let expr_f = Z3.Boolean.mk_implies !ctx expr_f_lhs expr_f_rhs in
84
  (* Adding forall as prefix *)
85
  let expr_forall_f = Z3.Quantifier.mk_forall_const
86
    !ctx  (* context *)
87
    (* [int_sort; int_sort]           (\* sort list*\) *)
88
    (* [Z3.FuncDecl.get_name x; Z3.FuncDecl.get_name y] (\* symbol list *\) *)
89
(*    [x_expr; y_expr] Second try with expr list "const" *)
90
    [Z3.Expr.mk_const_f !ctx x; Z3.Expr.mk_const_f !ctx y]
91
    expr_f (* expression *)
92
    None (* quantifier weight, None means 1 *)
93
    [] (* pattern list ? *)
94
    [] (* ? *)
95
    None (* ? *)
96
    None (* ? *)
97
  in
98
  let expr_forall_f = Z3.Quantifier.expr_of_quantifier expr_forall_f in
99
  Z3.Fixedpoint.add_rule !fp expr_forall_f None;
100
  
101
  
102
  (* INIT RULE *)
103
  let decl_init = Z3.FuncDecl.mk_func_decl_s !ctx "INIT_STATE" [] bool_sort in
104
  Z3.Fixedpoint.register_relation !fp decl_init; 
105
  let init_expr = Z3.Expr.mk_app !ctx decl_init [] in
106
  Z3.Fixedpoint.add_rule !fp init_expr None;
107

  
108
  (* MAIN is defined by two rules : INIT and induction *)
109
  let decl_main = Z3.FuncDecl.mk_func_decl_s !ctx "MAIN" [int_sort; int_sort] bool_sort in
110
  Z3.Fixedpoint.register_relation !fp decl_main;
111
  let main_x_y_expr = Z3.Expr.mk_app !ctx decl_main [x_expr; y_expr] in
112
  
113
  (* Rule 1: forall x, y, INIT_STATE and f(x,y) => MAIN(x,y) : at the beginning x=y *)
114
  let expr_main1_lhs = (* INIT_STATE and f(x, y) *)
115
    Z3.Boolean.mk_and !ctx [f_x_y_expr; init_expr] in
116
  let expr_main1_rhs = main_x_y_expr in
117
  let expr_main1 = Z3.Boolean.mk_implies !ctx expr_main1_lhs expr_main1_rhs in
118
  (* Adding forall as prefix *)
119
  let expr_forall_main1 = Z3.Quantifier.mk_forall_const
120
    !ctx  (* context *)
121
    (*
122
    [int_sort; int_sort]           (* sort list*)
123
    [Z3.FuncDecl.get_name x; Z3.FuncDecl.get_name y] (* symbol list *)
124
    *)
125
    (*    [x_expr; y_expr] Second try with expr list "const" *)
126
    [Z3.Expr.mk_const_f !ctx x; Z3.Expr.mk_const_f !ctx y]
127
    expr_main1 (* expression *)
128
    None (* quantifier weight, None means 1 *)
129
    [] (* pattern list ? *)
130
    [] (* ? *)
131
    None (* ? *)
132
    None (* ? *)
133
  in
134
  let expr_forall_main1 = Z3.Quantifier.expr_of_quantifier expr_forall_main1 in
135
  Z3.Fixedpoint.add_rule !fp expr_forall_main1 None;
136

  
137
  (* Rule 2: forall x,y, MAIN(x,y) => MAIN(x+1, y+1) *)
138
  
139
  
140
  (* TODO: not implemented yet since the error is visible without it *)
141
  
142
  (* Query: is it possible to have MAIN(x,y) and x!=y ? *)
143
  (* This is performed as follow:
144
     rule (forall x, y, MAIN(x,y) and x!=y => ERR)
145
  *)
146
  let decl_err = Z3.FuncDecl.mk_func_decl_s !ctx "ERR" [] bool_sort in
147
  Z3.Fixedpoint.register_relation !fp decl_err; 
148
  let err_expr = Z3.Expr.mk_app !ctx decl_err [] in
149
  let x_diff_y_expr = Z3.Boolean.mk_not !ctx x_eq_y_expr in
150
  let expr_err_lhs =
151
    Z3.Boolean.mk_and !ctx [x_diff_y_expr; main_x_y_expr] in
152
  let expr_err_rhs = err_expr in
153
  let expr_err = Z3.Boolean.mk_implies !ctx expr_err_lhs expr_err_rhs in
154
  (* Adding forall as prefix *)
155
  let expr_forall_err = Z3.Quantifier.mk_forall_const
156
    !ctx  (* context *)
157
(*    [int_sort; int_sort]           (* sort list*)
158
    [Z3.FuncDecl.get_name x; Z3.FuncDecl.get_name y] (* symbol list *)
159
*)
160
    (* [x_expr; y_expr] Second try with expr list "const" *)
161
    [Z3.Expr.mk_const_f !ctx x; Z3.Expr.mk_const_f !ctx y]
162
    expr_err (* expression *)
163
    None (* quantifier weight, None means 1 *)   
164
    [] (* pattern list ? *)
165
    [] (* ? *)
166
    None (* ? *)
167
    None (* ? *)
168
  in
169
  let expr_forall_err = Z3.Quantifier.expr_of_quantifier expr_forall_err in
170
  Z3.Fixedpoint.add_rule !fp expr_forall_err None;
171

  
172
  (* Printing the rules for sanity check *)
173
  
174
  let rules_expr = Z3.Fixedpoint.get_rules !fp in
175
  Format.eprintf "@[<v 2>Registered rules:@ %a@ @]@."
176
    (fprintf_list ~sep:"@ "
177
       (fun fmt e ->
178
	 (* let e2 = Z3.Quantifier.get_body eq in *)
179
	 (* let fd = Z3.Expr.get_func_decl e in *)
180
	 Format.fprintf fmt "Rule: %s@ "
181
	   (Z3.Expr.to_string e);
182
       )) rules_expr;
183

  
184

  
185
  let res_status = Z3.Fixedpoint.query_r !fp [decl_err] in
186

  
187
  Format.eprintf "Status: %s@." (Z3.Solver.string_of_status res_status)
188
    
189
	
190

  
191

  
192
  
src/tools/zustre/zustre_verifier.ml
83 83
      let mks = S.mk_string !ctx in
84 84
      let params = P.mk_params !ctx in
85 85

  
86
      (* self.fp.set (engine='spacer') *)
86
      (* (\* self.fp.set (engine='spacer') *\) *)
87 87
      P.add_symbol params (mks "engine") (mks "spacer");
88
      (* P.add_symbol params (mks "engine") (mks "pdr");  *)
88 89
      
89 90
       (* #z3.set_option(rational_to_decimal=True) *)
90 91
       (* #self.fp.set('precision',30) *)
......
152 153
	
153 154
	let queries = Z3.Fixedpoint.parse_file !fp "mini.smt2" in
154 155

  
155
      (* Debug instructions *)
156
      let rules_expr = Z3.Fixedpoint.get_rules !fp in
157
      Format.eprintf "@[<v 2>Registered rules:@ %a@ @]@."
158
      	(Utils.fprintf_list ~sep:"@ "
159
      	   (fun fmt e -> Format.pp_print_string fmt (Z3.Expr.to_string e)) )
160
      	rules_expr;
156
	(* Debug instructions *)
157
	
161 158

  
162
	let res_status = Z3.Fixedpoint.query !fp (List.hd queries )in
159
	
160
	let rules_expr = Z3.Fixedpoint.get_rules !fp in
161
	Format.eprintf "@[<v 2>Registered rules:@ %a@ @]@."
162
      	  (Utils.fprintf_list ~sep:"@ "
163
      	     (fun fmt e ->
164
	       (* let e2 = Z3.Quantifier.get_body eq in *)
165
	       (* let fd = Z3.Expr.get_func_decl e in *)
166
	       Format.fprintf fmt "Rule: %s@."
167
		 (Z3.Expr.to_string e);
168
	     )) rules_expr;
169
	
170
	let _ = List.map extract_expr_fds rules_expr in
171
	Format.eprintf "%t" pp_fdecls;
172
	
173
      	let res_status = Z3.Fixedpoint.query !fp (List.hd queries )in
163 174
	
164 175
	Format.eprintf "Status: %s@." (Z3.Solver.string_of_status res_status)
165 176
      )
177
      else if false then (
178

  
179
	(* No queries here *)
180
	let _ = Z3.Fixedpoint.parse_file !fp "mini_decl.smt2" in
181

  
182
	(* Debug instructions *)
183
	
184

  
185
	
186
	let rules_expr = Z3.Fixedpoint.get_rules !fp in
187
	Format.eprintf "@[<v 2>Registered rules:@ %a@ @]@."
188
      	  (Utils.fprintf_list ~sep:"@ "
189
      	     (fun fmt e ->
190
	       (* let e2 = Z3.Quantifier.get_body eq in *)
191
	       (* let fd = Z3.Expr.get_func_decl e in *)
192
	       Format.fprintf fmt "Rule: %s@."
193
		 (Z3.Expr.to_string e);
194
	     )) rules_expr;
195
	
196
	let _ = List.map extract_expr_fds rules_expr in
197
	Format.eprintf "%t" pp_fdecls;
198

  
199
	if !Options.main_node <> "" then
200
      	  begin
201
      	    Zustre_analyze.check machines !Options.main_node
202

  
203
      	  end
204
	else
205
      	  failwith "Require main node";
206

  
207
	()	
208
      )
166 209
      else (
167 210
	
168 211
	
169
      decl_sorts ();
170
      
171
      List.iter (decl_machine machines) (List.rev machines);
212
	decl_sorts ();
213
	
214
	List.iter (decl_machine machines) (List.rev machines);
172 215

  
173 216

  
174
      (* (\* Debug instructions *\) *)
175
      (* let rules_expr = Z3.Fixedpoint.get_rules !fp in *)
176
      (* Format.eprintf "@[<v 2>Registered rules:@ %a@ @]@." *)
177
      (* 	(Utils.fprintf_list ~sep:"@ " *)
178
      (* 	   (fun fmt e -> Format.pp_print_string fmt (Z3.Expr.to_string e)) ) *)
179
      (* 	rules_expr; *)
217
	(* (\* Debug instructions *\) *)
218
	(* let rules_expr = Z3.Fixedpoint.get_rules !fp in *)
219
	(* Format.eprintf "@[<v 2>Registered rules:@ %a@ @]@." *)
220
	(* 	(Utils.fprintf_list ~sep:"@ " *)
221
	(* 	   (fun fmt e -> Format.pp_print_string fmt (Z3.Expr.to_string e)) ) *)
222
	(* 	rules_expr; *)
180 223

  
181
      if !Options.main_node <> "" then
182
      	begin
183
      	  Zustre_analyze.check machines !Options.main_node
224
	if !Options.main_node <> "" then
225
      	  begin
226
      	    Zustre_analyze.check machines !Options.main_node
184 227

  
185
      	end
186
      else
187
      	failwith "Require main node";
188
      
189
      ()
228
      	  end
229
	else
230
      	  failwith "Require main node";
231
	
232
	()
190 233
      )
191 234
	
192 235

  
193
  end: VerifierType.S)
236
	    end: VerifierType.S)
194 237
    
195 238
(* Local Variables: *)
196 239
(* compile-command:"make -C ../.." *)

Also available in: Unified diff