Revision ca7ff3f7
Added by Lélio Brun over 1 year ago
src/tools/zustre/zustre_data.ml | ||
---|---|---|
1 | 1 |
let ctx = ref (Z3.mk_context []) |
2 |
|
|
2 | 3 |
let fp = ref (Z3.Fixedpoint.mk_fixedpoint !ctx) |
3 | 4 |
|
5 |
let const_sorts : (Lustre_types.ident, Z3.Sort.sort) Hashtbl.t = |
|
6 |
Hashtbl.create 13 |
|
4 | 7 |
|
5 |
let const_sorts : (Lustre_types.ident, Z3.Sort.sort) Hashtbl.t = Hashtbl.create 13 |
|
6 |
let const_tags : (Lustre_types.ident, Z3.Sort.sort) Hashtbl.t = Hashtbl.create 13 |
|
7 |
let sort_elems : (Z3.Sort.sort, Lustre_types.ident list) Hashtbl.t = Hashtbl.create 13 |
|
8 |
let const_tags : (Lustre_types.ident, Z3.Sort.sort) Hashtbl.t = |
|
9 |
Hashtbl.create 13 |
|
8 | 10 |
|
11 |
let sort_elems : (Z3.Sort.sort, Lustre_types.ident list) Hashtbl.t = |
|
12 |
Hashtbl.create 13 |
|
9 | 13 |
|
10 |
let decls: (Lustre_types.ident, Z3.FuncDecl.func_decl) Hashtbl.t = Hashtbl.create 13 |
|
14 |
let decls : (Lustre_types.ident, Z3.FuncDecl.func_decl) Hashtbl.t = |
|
15 |
Hashtbl.create 13 |
|
11 | 16 |
|
12 | 17 |
let debug = ref false |
13 |
let timeout = ref 10000 (* default : 10 s = 10 000 ms *) |
|
18 |
|
|
19 |
let timeout = ref 10000 |
|
20 |
(* default : 10 s = 10 000 ms *) |
|
14 | 21 |
|
15 | 22 |
(* Local Variables: *) |
16 | 23 |
(* compile-command:"make -C ../.." *) |
Also available in: Unified diff
reformatting