Project

General

Profile

« Previous | Next » 

Revision 4300981b

Added by Pierre-Loïc Garoche over 3 years ago

Zustre: timeout and slicing

View differences:

src/tools/zustre/zustre_common.ml
120 120
  (*verifier ce qui est construit. On veut un declare-rel *)
121 121
  
122 122
  (* let args_sorts = List.map (fun v -> type_to_sort v.var_type) args in *)
123
  if !debug then
124
    Format.eprintf "Registering fdecl %s (%a)@."
125
      name
126
      (Utils.fprintf_list ~sep:"@ "
127
	 (fun fmt sort -> Format.fprintf fmt "%s" (Z3.Sort.to_string sort)))
128
      args_sorts
129
  ;
123 130
  let fdecl = Z3.FuncDecl.mk_func_decl_s !ctx name args_sorts bool_sort in
124 131
  Z3.Fixedpoint.register_relation !fp fdecl;
125 132
  register_fdecl name fdecl;
......
675 682
  let extracted_sorts = List.map Z3.FuncDecl.get_range extracted_vars in
676 683
  let extracted_symbols = List.map Z3.FuncDecl.get_name extracted_vars in
677 684

  
678
  (* Format.eprintf "Declaring rule: %s with variables @[<v 0>@ [%a@ ]@]@ @." *)
679
  (*   (Z3.Expr.to_string expr) *)
680
  (*   (Utils.fprintf_list ~sep:",@ " (fun fmt e -> Format.fprintf fmt "%s" (Z3.Expr.to_string e))) (List.map horn_var_to_expr vars) *)
681
  (*   ; *)
685
  if !debug then (
686
    Format.eprintf "Declaring rule: %s with variables @[<v 0>@ [%a@ ]@]@ @."
687
      (Z3.Expr.to_string expr)
688
      (Utils.fprintf_list ~sep:",@ " (fun fmt e -> Format.fprintf fmt "%s" (Z3.Expr.to_string e))) (List.map horn_var_to_expr vars)
689
  )
690
    ;
682 691
  let expr = Z3.Quantifier.mk_forall_const
683 692
    !ctx  (* context *)
684 693
    (List.map horn_var_to_expr vars) (* TODO provide bounded variables as expr *)
......
768 777
      	      (rename_machine_list m.mname.node_id m.mstep.step_locals)
769 778
      	  )
770 779
      in
771
      
772 780
      if is_stateless m then
773 781
	begin
782
	  if !debug then 
783
	    Format.eprintf "Declaring a stateless machine: %s@." m.mname.node_id;
784

  
774 785
	  (* Declaring single predicate *)
775 786
	  let vars = inout_vars machines m in
776 787
	  let vars_types = List.map (fun v -> type_to_sort v.var_type) vars in
777 788
	  let _ = decl_rel (machine_stateless_name m.mname.node_id) vars_types in
789
	  
778 790
	  let horn_body, _ (* don't care for reset here *) =
779 791
	    instrs_to_expr
780 792
	      machines
......
788 800
	      (get_fdecl (machine_stateless_name m.mname.node_id))
789 801
	      (List.map (horn_var_to_expr) vars)
790 802
	  in
803
	  (* this line seems useless *)
791 804
	  let vars = vars@(rename_machine_list m.mname.node_id m.mstep.step_locals) in
805
	  (* Format.eprintf "useless Vars: %a@." (Utils.fprintf_list ~sep:"@ " Printers.pp_var) vars; *)
792 806
	  match m.mstep.step_asserts with
793 807
	  | [] ->
794 808
	     begin
795 809
	       (* Rule for single predicate : "; Stateless step rule @." *)
796
	       let vars = rename_machine_list m.mname.node_id m.mstep.step_locals in
810
	       (*let vars = rename_machine_list m.mname.node_id m.mstep.step_locals in*)
811
	       (* TODO clean code *)
812
	       (* Format.eprintf "used Vars: %a@." (Utils.fprintf_list ~sep:"@ " Printers.pp_var) vars; *)
797 813
	       add_rule vars (Z3.Boolean.mk_implies !ctx horn_body horn_head)
798 814
		 
799 815
	     end

Also available in: Unified diff