Project

General

Profile

« Previous | Next » 

Revision 2f7c9195

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

zustre progress. Issues with sliced predicates

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