| 1 |
5778dd5e
|
ploc
|
let ctx = ref (Z3.mk_context [])
|
| 2 |
ca7ff3f7
|
Lélio Brun
|
|
| 3 |
5778dd5e
|
ploc
|
let fp = ref (Z3.Fixedpoint.mk_fixedpoint !ctx)
|
| 4 |
|
|
|
| 5 |
ca7ff3f7
|
Lélio Brun
|
let const_sorts : (Lustre_types.ident, Z3.Sort.sort) Hashtbl.t =
|
| 6 |
|
|
Hashtbl.create 13
|
| 7 |
5778dd5e
|
ploc
|
|
| 8 |
ca7ff3f7
|
Lélio Brun
|
let const_tags : (Lustre_types.ident, Z3.Sort.sort) Hashtbl.t =
|
| 9 |
|
|
Hashtbl.create 13
|
| 10 |
5778dd5e
|
ploc
|
|
| 11 |
ca7ff3f7
|
Lélio Brun
|
let sort_elems : (Z3.Sort.sort, Lustre_types.ident list) Hashtbl.t =
|
| 12 |
|
|
Hashtbl.create 13
|
| 13 |
5778dd5e
|
ploc
|
|
| 14 |
ca7ff3f7
|
Lélio Brun
|
let decls : (Lustre_types.ident, Z3.FuncDecl.func_decl) Hashtbl.t =
|
| 15 |
|
|
Hashtbl.create 13
|
| 16 |
5778dd5e
|
ploc
|
|
| 17 |
4300981b
|
ploc
|
let debug = ref false
|
| 18 |
ca7ff3f7
|
Lélio Brun
|
|
| 19 |
|
|
let timeout = ref 10000
|
| 20 |
|
|
(* default : 10 s = 10 000 ms *)
|
| 21 |
5778dd5e
|
ploc
|
|
| 22 |
|
|
(* Local Variables: *)
|
| 23 |
|
|
(* compile-command:"make -C ../.." *)
|
| 24 |
|
|
(* End: *)
|