Project

General

Profile

Revision dbab1fe5 src/tools/zustre/zustre_common.ml

View differences:

src/tools/zustre/zustre_common.ml
111 111

  
112 112
    
113 113
let decl_var id =
114
  Format.eprintf "Declaring var %s@." id.var_id;
114
  (* Format.eprintf "Declaring var %s@." id.var_id; *)
115 115
  let fdecl = Z3.FuncDecl.mk_func_decl_s !ctx id.var_id [] (type_to_sort id.var_type) in
116 116
  register_fdecl id.var_id fdecl;
117 117
  fdecl
......
644 644
    if nb_args <= 0 then (
645 645
      let fdecl = Z3.Expr.get_func_decl e in
646 646
      (* let params = Z3.FuncDecl.get_parameters fdecl in *)
647
      Format.eprintf "Extracting info about %s: @." (Z3.Expr.to_string e);
647
      (* Format.eprintf "Extracting info about %s: @." (Z3.Expr.to_string e); *)
648 648
      let dkind = Z3.FuncDecl.get_decl_kind fdecl in
649 649
      match dkind with Z3enums.OP_UNINTERPRETED -> (
650 650
	(* Format.eprintf "kind = %s, " (match dkind with Z3enums.OP_TRUE -> "true" | Z3enums.OP_UNINTERPRETED -> "uninter"); *)
......
674 674
  let extracted_sorts = List.map Z3.FuncDecl.get_range extracted_vars in
675 675
  let extracted_symbols = List.map Z3.FuncDecl.get_name extracted_vars in
676 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
    ;
677
  (* Format.eprintf "Declaring rule: %s with variables @[<v 0>@ [%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 681
  let expr = Z3.Quantifier.mk_forall_const
682 682
    !ctx  (* context *)
683 683
    (List.map horn_var_to_expr vars) (* TODO provide bounded variables as expr *)
......
690 690
    None (* ? *)
691 691
    None (* ? *)
692 692
  in
693
  Format.eprintf "OK@.@?";
693
  (* Format.eprintf "OK@.@?"; *)
694 694

  
695 695
  (*
696 696
    TODO: bizarre la declaration de INIT tout seul semble poser pb.
......
845 845
	  match m.mstep.step_asserts with
846 846
	  | [] ->
847 847
	     begin
848
	       (* Rule for single predicate *)
849
	       let vars = vars @(rename_machine_list m.mname.node_id m.mstep.step_locals) in
848
	       (* Rule for single predicate *) 
849
	       let vars = (step_vars_c_m_x machines m) @(rename_machine_list m.mname.node_id m.mstep.step_locals) in
850 850
	       add_rule vars (Z3.Boolean.mk_implies !ctx horn_step_body horn_step_head)
851 851
		 
852 852
	     end
......
857 857
		 Z3.Boolean.mk_and !ctx
858 858
		   (horn_step_body :: List.map (horn_val_to_expr m.mname.node_id) assertsl)
859 859
	       in
860
	       let vars = vars @(rename_machine_list m.mname.node_id m.mstep.step_locals) in
860
	       let vars = (step_vars_c_m_x machines m) @(rename_machine_list m.mname.node_id m.mstep.step_locals) in
861 861
	       add_rule vars (Z3.Boolean.mk_implies !ctx body_with_asserts horn_step_head)
862 862
		 
863 863
	     end
......
870 870
(* Debug functions *)
871 871

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

  
916 917
(* Local Variables: *)
917 918
(* compile-command:"make -C ../.." *)

Also available in: Unified diff