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