Project

General

Profile

Revision dbab1fe5

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: *)
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 ../.." *)
src/tools/zustre/zustre_test.ml
135 135
  Z3.Fixedpoint.add_rule !fp expr_forall_main1 None;
136 136

  
137 137
  (* Rule 2: forall x,y, MAIN(x,y) => MAIN(x+1, y+1) *)
138
  let expr_main2_lhs = main_x_y_expr in
139
  let plus_one x = Z3.Arithmetic.mk_add !ctx
140
    [
141
      x;
142
      (* Z3.Arithmetic.Integer.mk_const_s !ctx "1" *)
143
	Z3.Expr.mk_numeral_int !ctx 1 int_sort
144
    ] in
145
  let main_x_y_plus_one_expr = Z3.Expr.mk_app !ctx decl_main [plus_one x_expr; plus_one y_expr] in
146
  let expr_main2_rhs = main_x_y_plus_one_expr in
147
  let expr_main2 = Z3.Boolean.mk_implies !ctx expr_main2_lhs expr_main2_rhs in
148
  (* Adding forall as prefix *)
149
  let expr_forall_main2 = Z3.Quantifier.mk_forall_const
150
    !ctx  (* context *)
151
    (*
152
    [int_sort; int_sort]           (* sort list*)
153
    [Z3.FuncDecl.get_name x; Z3.FuncDecl.get_name y] (* symbol list *)
154
    *)
155
    (*    [x_expr; y_expr] Second try with expr list "const" *)
156
    [Z3.Expr.mk_const_f !ctx x; Z3.Expr.mk_const_f !ctx y]
157
    expr_main2 (* expression *)
158
    None (* quantifier weight, None means 1 *)
159
    [] (* pattern list ? *)
160
    [] (* ? *)
161
    None (* ? *)
162
    None (* ? *)
163
  in
164
  let expr_forall_main2 = Z3.Quantifier.expr_of_quantifier expr_forall_main2 in
165
  Z3.Fixedpoint.add_rule !fp expr_forall_main2 None;
166
  
138 167
  
139 168
  
140 169
  (* TODO: not implemented yet since the error is visible without it *)

Also available in: Unified diff