Project

General

Profile

Revision 46cb4020 src/tools/zustre_verifier.ml

View differences:

src/tools/zustre_verifier.ml
69 69
          Hashtbl.add sort_elems new_sort tl;
70 70
          List.iter (fun t -> Hashtbl.add const_tags t new_sort) tl
71 71
          
72
	| _ -> assert false
72
	| _ -> Format.eprintf "Unknown type : %a@.@?" Printers.pp_var_type_dec_desc typ; assert false
73 73
      )
74 74
      | _ -> assert false
75 75
      )
......
249 249
       (val_to_expr v1)
250 250
       (val_to_expr v2)
251 251

  
252
  | "+", [v1; v2] ->
253
     Z3.Arithmetic.mk_add
254
       !ctx
255
       [val_to_expr v1; val_to_expr v2]
256

  
257
  | "-", [v1; v2] ->
258
     Z3.Arithmetic.mk_sub
259
       !ctx
260
       [val_to_expr v1 ; val_to_expr v2]
261
       
262
  | "*", [v1; v2] ->
263
     Z3.Arithmetic.mk_mul
264
       !ctx
265
       [val_to_expr v1; val_to_expr v2]
266

  
267

  
268
  | "<", [v1; v2] ->
269
     Z3.Arithmetic.mk_lt
270
       !ctx
271
       (val_to_expr v1)
272
       (val_to_expr v2)
273

  
274
  | "<=", [v1; v2] ->
275
     Z3.Arithmetic.mk_le
276
       !ctx
277
       (val_to_expr v1)
278
       (val_to_expr v2)
279

  
280
  | ">", [v1; v2] ->
281
     Z3.Arithmetic.mk_gt
282
       !ctx
283
       (val_to_expr v1)
284
       (val_to_expr v2)
285

  
286
  | ">=", [v1; v2] ->
287
     Z3.Arithmetic.mk_ge
288
       !ctx
289
       (val_to_expr v1)
290
       (val_to_expr v2)
291

  
292
       
252 293
  (* | _, [v1; v2] ->      Z3.Boolean.mk_and
253 294
   *      !ctx
254 295
   *      (val_to_expr v1)
......
834 875
      setup_solver ();
835 876
      decl_sorts ();
836 877
      List.iter (decl_machine machines) (List.rev machines);
878

  
879

  
880
      (* Debug instructions *)
881
      let rules_expr = Z3.Fixedpoint.get_rules !fp in
882
      Format.eprintf "@[<v 2>Registered rules:@ %a@ @]@."
883
	(Utils.fprintf_list ~sep:"@ "
884
	   (fun fmt e -> Format.pp_print_string fmt (Z3.Expr.to_string e)) )
885
	rules_expr;
886
      
837 887
      ()
838 888
      
839 889
      

Also available in: Unified diff