Project

General

Profile

Revision 2f7c9195 src/tools/zustre/zustre_common.ml

View differences:

src/tools/zustre/zustre_common.ml
116 116
  register_fdecl id.var_id fdecl;
117 117
  fdecl
118 118

  
119
let decl_rel name args =
119
let decl_rel name args_sorts =
120 120
  (*verifier ce qui est construit. On veut un declare-rel *)
121
  let args_sorts = List.map (fun v -> type_to_sort v.var_type) args in
121
  
122
  (* let args_sorts = List.map (fun v -> type_to_sort v.var_type) args in *)
122 123
  let fdecl = Z3.FuncDecl.mk_func_decl_s !ctx name args_sorts bool_sort in
123 124
  Z3.Fixedpoint.register_relation !fp fdecl;
124 125
  register_fdecl name fdecl;
......
772 773
	begin
773 774
	  (* Declaring single predicate *)
774 775
	  let vars = inout_vars machines m in
775
	  let _ = decl_rel (machine_stateless_name m.mname.node_id) vars in
776
	  let vars_types = List.map (fun v -> type_to_sort v.var_type) vars in
777
	  let _ = decl_rel (machine_stateless_name m.mname.node_id) vars_types in
776 778
	  let horn_body, _ (* don't care for reset here *) =
777 779
	    instrs_to_expr
778 780
	      machines
......
811 813
	  (* Rule for reset *)
812 814

  
813 815
	  let vars = reset_vars machines m in
814
	  let _ = decl_rel (machine_reset_name m.mname.node_id) vars in
816
	  let vars_types = List.map (fun v -> type_to_sort v.var_type) vars in
817
	  let _ = decl_rel (machine_reset_name m.mname.node_id) vars_types in
815 818
	  let horn_reset_body = machine_reset machines m in	    
816 819
	  let horn_reset_head = 
817 820
	    Z3.Expr.mk_app
......
828 831

  
829 832
	  (* Rule for step*)
830 833
	  let vars = step_vars machines m in
831
          let _ = decl_rel (machine_step_name m.mname.node_id) vars in
834
  	  let vars_types = List.map (fun v -> type_to_sort v.var_type) vars in
835
          let _ = decl_rel (machine_step_name m.mname.node_id) vars_types in
832 836
	  let horn_step_body, _ (* don't care for reset here *) =
833 837
	    instrs_to_expr
834 838
	      machines

Also available in: Unified diff