Project

General

Profile

Revision 7d77632f src/tools/zustre/zustre_analyze.ml

View differences:

src/tools/zustre/zustre_analyze.ml
11 11
open Zustre_common
12 12
open Zustre_data
13 13

  
14
let idx_0 = Z3.Arithmetic.Integer.mk_numeral_i !ctx 0 
15
let uid_0 = Z3.Z3List.nil uid_sort 
16
	    
14 17
let check machines node =
15 18

  
16 19
  let machine = get_machine machines node in
......
41 44
  (* TODO: push/pop? donner un nom different par instance pour les garder dans le buffer ?
42 45
     Faut-il declarer les "rel" dans la hashtbl ?
43 46
  *)
44
  
47

  
48
  let main_name node_id = "MAIN" ^ "_" ^ node_id in
49
    
45 50
  let decl_main =
46
    decl_rel
47
      ("MAIN" ^ "_" ^ node_id)
51
    decl_rel ~no_additional_vars:true
52
      (main_name node_id)
48 53
      (int_sort::(List.map (fun v -> type_to_sort v.var_type) (main_memory_next))) in
49 54

  
50 55
  
51 56
  
52 57
  (* Init case *)
53
  let decl_init = decl_rel "INIT_STATE" [] in
58
  let decl_init = decl_rel ~no_additional_vars:true "INIT_STATE" [] in
54 59

  
55 60
  (* (special) rule INIT_STATE *)
56 61
  let init_expr = Z3.Expr.mk_app !ctx decl_init [] in
......
68 73
    Z3.Expr.mk_app
69 74
      !ctx
70 75
      decl_main
71
      ((Z3.Arithmetic.Integer.mk_numeral_i !ctx 0)::(List.map horn_var_to_expr main_memory_next))
76
      (idx_0::(* uid_0:: *)(List.map horn_var_to_expr main_memory_next))
72 77
  in
73 78
  (* Special case when the main node is stateless *)
74 79
  let _ =
......
89 94
	      Z3.Expr.mk_app !ctx decl_init [];
90 95
	      Z3.Expr.mk_app !ctx
91 96
		(get_fdecl (machine_stateless_name node))
92
		(List.map horn_var_to_expr vars) 
97
		(idx_0::uid_0::(List.map horn_var_to_expr vars))
93 98
	    ]
94 99
	in
95 100
	add_rule vars (Z3.Boolean.mk_implies !ctx horn_body horn_head)
......
113 118
	      Z3.Expr.mk_app !ctx decl_init [];
114 119
	      Z3.Expr.mk_app !ctx
115 120
		(get_fdecl (machine_reset_name node))
116
		(List.map horn_var_to_expr (reset_vars machines machine));
121
		(idx_0::uid_0::List.map horn_var_to_expr (reset_vars machines machine));
117 122
	      Z3.Expr.mk_app !ctx
118 123
		(get_fdecl (machine_step_name node))
119
		(List.map horn_var_to_expr (step_vars_m_x machines machine))
124
		(idx_0::uid_0::List.map horn_var_to_expr (step_vars_m_x machines machine))
120 125
	    ]
121 126
	in
122 127

  
......
148 153
  (*   (Utils.fprintf_list ~sep:" " (pp_horn_var machine)) (step_vars machines machine) *)
149 154

  
150 155
  let k = Corelang.dummy_var_decl "k" Type_predef.type_int (*Corelang.mktyp Location.dummy_loc Types.type_int*) in
151
  let k_var = decl_var k in
156
  let k_var = Z3.Expr.mk_const_f !ctx (decl_var k) in
152 157
  
153 158
  let horn_head = 
154 159
    Z3.Expr.mk_app
......
156 161
      decl_main
157 162
      ((Z3.Arithmetic.mk_add
158 163
	  !ctx
159
	  [Z3.Expr.mk_const_f !ctx k_var; Z3.Arithmetic.Integer.mk_numeral_i !ctx 1]
164
	  [k_var; Z3.Arithmetic.Integer.mk_numeral_i !ctx 1]
160 165
       )::(List.map horn_var_to_expr main_memory_next))
161 166
  in
162 167
  let horn_body =
163 168
    Z3.Boolean.mk_and !ctx
164 169
      [
165
	Z3.Expr.mk_app !ctx decl_main (Z3.Expr.mk_const_f !ctx k_var::(List.map horn_var_to_expr main_memory_current));
166
	Z3.Expr.mk_app !ctx (get_fdecl (step_name node)) (List.map horn_var_to_expr (step_vars machines machine))
170
	Z3.Expr.mk_app !ctx decl_main (k_var::(List.map horn_var_to_expr main_memory_current));
171
	Z3.Expr.mk_app !ctx (get_fdecl (step_name node)) (k_var::uid_0::List.map horn_var_to_expr (step_vars machines machine))
167 172
      ]
168 173
  in
169 174
  (* Vars contains all vars: in_out, current, mid, neXt memories *)
......
175 180

  
176 181

  
177 182
  (* Property def *)
178
  let decl_err = decl_rel "ERR" [] in
183
  let decl_err = decl_rel ~no_additional_vars:true "ERR" [] in
179 184

  
180 185
  let prop =
181 186
    Z3.Boolean.mk_and !ctx (List.map horn_var_to_expr main_output)
......
187 192
	      (
188 193
		Z3.Boolean.mk_and !ctx
189 194
		  [not_prop;
190
		   Z3.Expr.mk_app !ctx decl_main (Z3.Expr.mk_const_f !ctx k_var::List.map horn_var_to_expr main_memory_next);
195
		   Z3.Expr.mk_app !ctx decl_main (k_var::List.map horn_var_to_expr main_memory_next);
191 196
		  ]
192 197
	      )
193 198
	      (Z3.Expr.mk_app !ctx decl_err []))

Also available in: Unified diff