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