Project

General

Profile

Revision a0c92fa8 src/tools/zustre/zustre_common.ml

View differences:

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