Revision a0c92fa8 src/tools/zustre/zustre_common.ml
src/tools/zustre/zustre_common.ml  

5  5 
(* open Horn_backend_common 
6  6 
* open Horn_backend *) 
7  7 
open Zustre_data 
8  
8 


9 
let report = Log.report ~plugin:"z3 interface" 

10 


9  11 
module HBC = Horn_backend_common 
10  12 
let node_name = HBC.node_name 
11  13  
...  ...  
111  113 
let get_fdecl id = 
112  114 
try 
113  115 
Hashtbl.find decls id 
114 
with Not_found > (Format.eprintf "Unable to find func_decl %s@.@?" id; raise Not_found)


116 
with Not_found > (report ~level:3 (fun fmt > Format.fprintf fmt "Unable to find func_decl %s@.@?" id); raise Not_found)


115  117  
116  118 
let pp_fdecls fmt = 
117  119 
Format.fprintf fmt "Registered fdecls: @[%a@]@ " 
...  ...  
124  126 
register_fdecl id.var_id fdecl; 
125  127 
fdecl 
126  128  
129 
(* Declaring the function used in expr *) 

130 
let decl_fun op args typ = 

131 
let args = List.map type_to_sort args in 

132 
let fdecl = Z3.FuncDecl.mk_func_decl_s !ctx op args (type_to_sort typ) in 

133 
register_fdecl op fdecl; 

134 
fdecl 

135  
127  136 
let idx_sort = int_sort 
128  137 
let uid_sort = Z3.Z3List.mk_sort !ctx (Z3.Symbol.mk_string !ctx "uid_list") int_sort 
129  138 
let uid_conc = 
...  ...  
242  251  
243  252 
(* Conversion of basic library functions *) 
244  253 

245 
let horn_basic_app i val_to_expr vl =


254 
let horn_basic_app i vl (vltyp, typ) =


246  255 
match i, vl with 
247 
 "ite", [v1; v2; v3] > 

248 
Z3.Boolean.mk_ite 

249 
!ctx 

250 
(val_to_expr v1) 

251 
(val_to_expr v2) 

252 
(val_to_expr v3) 

253  
254 
 "uminus", [v] > 

255 
Z3.Arithmetic.mk_unary_minus 

256 
!ctx 

257 
(val_to_expr v) 

256 
 "ite", [v1; v2; v3] > Z3.Boolean.mk_ite !ctx v1 v2 v3 

257 
 "uminus", [v] > Z3.Arithmetic.mk_unary_minus 

258 
!ctx v 

258  259 
 "not", [v] > 
259  260 
Z3.Boolean.mk_not 
260 
!ctx 

261 
(val_to_expr v) 

261 
!ctx v 

262  262 
 "=", [v1; v2] > 
263  263 
Z3.Boolean.mk_eq 
264 
!ctx 

265 
(val_to_expr v1) 

266 
(val_to_expr v2) 

264 
!ctx v1 v2 

267  265 
 "&&", [v1; v2] > 
268  266 
Z3.Boolean.mk_and 
269  267 
!ctx 
270 
[val_to_expr v1; 

271 
val_to_expr v2] 

268 
[v1; v2] 

272  269 
 "", [v1; v2] > 
273  270 
Z3.Boolean.mk_or 
274  271 
!ctx 
275 
[val_to_expr v1;


276 
val_to_expr v2]


272 
[v1; 

273 
v2] 

277  274  
278  275 
 "impl", [v1; v2] > 
279  276 
Z3.Boolean.mk_implies 
280 
!ctx 

281 
(val_to_expr v1) 

282 
(val_to_expr v2) 

277 
!ctx v1 v2 

283  278 
 "mod", [v1; v2] > 
284  279 
Z3.Arithmetic.Integer.mk_mod 
285 
!ctx 

286 
(val_to_expr v1) 

287 
(val_to_expr v2) 

280 
!ctx v1 v2 

288  281 
 "equi", [v1; v2] > 
289  282 
Z3.Boolean.mk_eq 
290  283 
!ctx 
291 
(val_to_expr v1) 

292 
(val_to_expr v2) 

284 
v1 v2 

293  285 
 "xor", [v1; v2] > 
294  286 
Z3.Boolean.mk_xor 
295 
!ctx 

296 
(val_to_expr v1) 

297 
(val_to_expr v2) 

287 
!ctx v1 v2 

298  288 
 "!=", [v1; v2] > 
299  289 
Z3.Boolean.mk_not 
300  290 
!ctx 
301  291 
( 
302  292 
Z3.Boolean.mk_eq 
303 
!ctx 

304 
(val_to_expr v1) 

305 
(val_to_expr v2) 

293 
!ctx v1 v2 

306  294 
) 
307  295 
 "/", [v1; v2] > 
308  296 
Z3.Arithmetic.mk_div 
309 
!ctx 

310 
(val_to_expr v1) 

311 
(val_to_expr v2) 

297 
!ctx v1 v2 

312  298  
313  299 
 "+", [v1; v2] > 
314  300 
Z3.Arithmetic.mk_add 
315  301 
!ctx 
316 
[val_to_expr v1; val_to_expr v2] 

317  
302 
[v1; v2] 

318  303 
 "", [v1; v2] > 
319  304 
Z3.Arithmetic.mk_sub 
320  305 
!ctx 
321 
[val_to_expr v1 ; val_to_expr v2]


306 
[v1 ; v2]


322  307 

323  308 
 "*", [v1; v2] > 
324  309 
Z3.Arithmetic.mk_mul 
325  310 
!ctx 
326 
[val_to_expr v1; val_to_expr v2]


311 
[ v1; v2]


327  312  
328  313  
329  314 
 "<", [v1; v2] > 
330  315 
Z3.Arithmetic.mk_lt 
331 
!ctx 

332 
(val_to_expr v1) 

333 
(val_to_expr v2) 

334  
316 
!ctx v1 v2 

335  317 
 "<=", [v1; v2] > 
336  318 
Z3.Arithmetic.mk_le 
337 
!ctx 

338 
(val_to_expr v1) 

339 
(val_to_expr v2) 

340  
319 
!ctx v1 v2 

341  320 
 ">", [v1; v2] > 
342  321 
Z3.Arithmetic.mk_gt 
343 
!ctx 

344 
(val_to_expr v1) 

345 
(val_to_expr v2) 

346  
322 
!ctx v1 v2 

347  323 
 ">=", [v1; v2] > 
348  324 
Z3.Arithmetic.mk_ge 
349 
!ctx 

350 
(val_to_expr v1) 

351 
(val_to_expr v2) 

352  
325 
!ctx v1 v2 

353  326 
 "int_to_real", [v1] > 
354  327 
Z3.Arithmetic.Integer.mk_int2real 
355 
!ctx 

356 
(val_to_expr v1) 

357  
328 
!ctx v1 

329 
 _ > 

330 
let fd = 

331 
try 

332 
get_fdecl i 

333 
with Not_found > begin 

334 
report ~level:3 (fun fmt > Format.fprintf fmt "Registering function %s as uninterpreted function in Z3@.%s: (%a) > %a" i i (Utils.fprintf_list ~sep:"," Types.print_ty) vltyp Types.print_ty typ); 

335 
decl_fun i vltyp typ 

336 
end 

337 
in 

338 
Z3.FuncDecl.apply fd vl 

358  339 

340 


359  341 
(*  _, [v1; v2] > Z3.Boolean.mk_and 
360  342 
* !ctx 
361  343 
* (val_to_expr v1) 
362  344 
* (val_to_expr v2) 
363  345 
* 
364  346 
* Format.fprintf fmt "(%s %a %a)" i val_to_exprr v1 val_to_expr v2 *) 
365 
 _ > ( 

366 
let msg fmt = Format.fprintf fmt 

367 
"internal error: zustre unkown function %s (nb args = %i)@." 

368 
i (List.length vl) 

369 
in 

370 
raise (UnknownFunction(i, msg)) 

371 
) 

347  
348 
(*  _ > ( 

349 
* let msg fmt = Format.fprintf fmt 

350 
* "internal error: zustre unkown function %s (nb args = %i)@." 

351 
* i (List.length vl) 

352 
* in 

353 
* raise (UnknownFunction(i, msg)) 

354 
* ) *) 

372  355  
373  356 

374  357 
(* Convert a value expression [v], with internal function calls only. [pp_var] 
...  ...  
376  359 
may be added for array variables 
377  360 
*) 
378  361 
let rec horn_val_to_expr ?(is_lhs=false) m self v = 
362 
(* Format.eprintf "h_v2e %a@." (Machine_code_common.pp_val m) v ; *) 

379  363 
match v.value_desc with 
380  364 
 Cst c > horn_const_to_expr c 
381  365  
...  ...  
425  409 
(rename_machine 
426  410 
self 
427  411 
v) 
428 
 Fun (n, vl) > horn_basic_app n (horn_val_to_expr m self) vl


412 
 Fun (n, vl) > horn_basic_app n (List.map (horn_val_to_expr m self) vl) (List.map (fun v > v.value_type) vl, v.value_type)


429  413  
430  414 
let no_reset_to_exprs machines m i = 
431  415 
let (n,_) = List.assoc i m.minstances in 
Also available in: Unified diff