Project

General

Profile

« Previous | Next » 

Revision 51ec4e8c

Added by Pierre-Loïc Garoche almost 7 years ago

Try to debug the use of Z3 API. Still having troubles

View differences:

src/tools/zustre/zustre_analyze.ml
48 48 
			 decl_init
49 49 
			 []
50 50 
  )  in
51
51 

  		




  
  52
  
    
  (* Re-declaring variables *)


  		




  
  53
  
    
  let _ = List.map decl_var main_memory_next in


  		




  
  54
  
    

  		




  52
  55
  
    
  let horn_head = 


  		




  53
  56
  
    
    Z3.Expr.mk_app


  		




  54
  57
  
    
      !ctx


  		




  ......




  65
  68
  
    

  		




  66
  69
  
    
	(* Note that vars here contains main_memory_next *)


  		




  67
  70
  
    
	let vars = step_vars_m_x machines machine in


  		




  
  71
  
    
	(* Re-declaring variables *)


  		




  
  72
  
    
	let _ = List.map decl_var vars in


  		




  68
  73
  
    
	


  		




  69
  74
  
    
	let horn_body =


  		




  70
  75
  
    
	  Z3.Boolean.mk_and !ctx


  		




  ......




  82
  87
  
    
    else


  		




  83
  88
  
    
      begin


  		




  84
  89
  
    
	(* Initial set: Reset(c,m) + One Step(m,x) @. *)


  		




  
  90
  
    

  		




  
  91
  
    
	(* Re-declaring variables *)


  		




  
  92
  
    
	let vars_reset = reset_vars machines machine in


  		




  
  93
  
    
	let vars_step = step_vars_m_x machines machine in


  		




  
  94
  
    
	let vars_step_all = step_vars_c_m_x machines machine in


  		




  
  95
  
    
	let _ = List.map decl_var (vars_reset @ vars_step @ vars_step_all ) in


  		




  
  96
  
    

  		




  85
  97
  
    
	(* rule => (INIT_STATE and reset(mid) and step(mid, next)) MAIN(next) *)


  		




  86
  98
  
    
	let horn_body =


  		




  87
  99
  
    
	  Z3.Boolean.mk_and !ctx


  		












Also available in:  Unified diff