Project

General

Profile

Revision dbab1fe5 src/tools/zustre/zustre_analyze.ml

View differences:

src/tools/zustre/zustre_analyze.ml
42 42
  (* Init case *)
43 43
  let decl_init = decl_rel "INIT_STATE" [] in
44 44

  
45
  (* rule INIT_STATE *)
46
  let _ = add_rule [] (Z3.Expr.mk_app
47
			 !ctx
48
			 decl_init
49
			 []
50
  )  in
45
  (* (special) rule INIT_STATE *)
46
  let init_expr = Z3.Expr.mk_app !ctx decl_init [] in
47
  Z3.Fixedpoint.add_rule !fp init_expr None;
48
  (* let _ = add_rule [] (Z3.Expr.mk_app *)
49
  (* 			 !ctx *)
50
  (* 			 decl_init *)
51
  (* 			 [] *)
52
  (* )  in *)
51 53

  
52 54
  (* Re-declaring variables *)
53 55
  let _ = List.map decl_var main_memory_next in
......
149 151
	Z3.Expr.mk_app !ctx (get_fdecl (step_name node)) (List.map horn_var_to_expr (step_vars machines machine))
150 152
      ]
151 153
  in
154
  (* Vars contains all vars: in_out, current, mid, neXt memories *)
155
  let vars = (step_vars_c_m_x machines machine) @ main_output_dummy in
152 156
  let _ =
153
    add_rule ~dont_touch:[decl_main] []  (Z3.Boolean.mk_implies !ctx horn_body horn_head)
157
    add_rule ~dont_touch:[decl_main] vars  (Z3.Boolean.mk_implies !ctx horn_body horn_head)
154 158
      
155 159
  in
156 160

  
......
164 168
  let not_prop =
165 169
    Z3.Boolean.mk_not !ctx prop
166 170
  in
167
  add_rule ~dont_touch:[decl_main;decl_err] main_memory_next (Z3.Boolean.mk_implies !ctx
171
  add_rule (*~dont_touch:[decl_main;decl_err]*) main_memory_next (Z3.Boolean.mk_implies !ctx
168 172
	      (
169 173
		Z3.Boolean.mk_and !ctx
170 174
		  [not_prop;
......
182 186

  
183 187
      (* Debug instructions *)
184 188
  let rules_expr = Z3.Fixedpoint.get_rules !fp in
185
  Format.eprintf "@[<v 2>Registered rules:@ %a@ @]@."
189
  if false then
190
    Format.eprintf "@[<v 2>Registered rules:@ %a@ @]@."
186 191
    (Utils.fprintf_list ~sep:"@ "
187 192
       (fun fmt e -> Format.pp_print_string fmt (Z3.Expr.to_string e)) )
188 193
    rules_expr;
189

  
190
  
191 194
  let res_status = Z3.Fixedpoint.query_r !fp [decl_err] in
192 195

  
193 196
  Format.eprintf "Status: %s@." (Z3.Solver.string_of_status res_status)
194
  
197

  
195 198
(* Local Variables: *)
196 199
(* compile-command:"make -C ../.." *)
197 200
(* End: *)

Also available in: Unified diff