equal
deleted
inserted
replaced
6 |
6 |
7 signature Z3_INTERFACE = |
7 signature Z3_INTERFACE = |
8 sig |
8 sig |
9 type builtin_fun = string * typ -> term list -> (string * term list) option |
9 type builtin_fun = string * typ -> term list -> (string * term list) option |
10 val add_builtin_funs: builtin_fun -> Context.generic -> Context.generic |
10 val add_builtin_funs: builtin_fun -> Context.generic -> Context.generic |
11 val interface: bool -> SMT_Solver.interface |
11 val interface: SMT_Solver.interface |
12 |
12 |
13 datatype sym = Sym of string * sym list |
13 datatype sym = Sym of string * sym list |
14 type mk_builtins = { |
14 type mk_builtins = { |
15 mk_builtin_typ: sym -> typ option, |
15 mk_builtin_typ: sym -> typ option, |
16 mk_builtin_num: theory -> int -> typ -> cterm option, |
16 mk_builtin_num: theory -> int -> typ -> cterm option, |
93 |
93 |
94 fun is_builtin_fun ctxt (c as (n, T)) ts = |
94 fun is_builtin_fun ctxt (c as (n, T)) ts = |
95 is_some (z3_builtin_fun' ctxt c ts) orelse |
95 is_some (z3_builtin_fun' ctxt c ts) orelse |
96 is_builtin_pred ctxt (n, Term.strip_type T ||> as_propT |> (op --->)) |
96 is_builtin_pred ctxt (n, Term.strip_type T ||> as_propT |> (op --->)) |
97 |
97 |
98 fun interface has_datatypes = { |
98 val interface = { |
99 extra_norm = extra_norm' has_datatypes, |
99 extra_norm = extra_norm', |
100 translate = { |
100 translate = { |
101 prefixes = prefixes, |
101 prefixes = prefixes, |
102 strict = strict, |
102 strict = strict, |
103 header = header, |
103 header = header, |
104 builtins = { |
104 builtins = { |
105 builtin_typ = builtin_typ, |
105 builtin_typ = builtin_typ, |
106 builtin_num = builtin_num, |
106 builtin_num = builtin_num, |
107 builtin_fun = z3_builtin_fun', |
107 builtin_fun = z3_builtin_fun', |
108 has_datatypes = has_datatypes}, |
108 has_datatypes = true}, |
109 serialize = serialize}} |
109 serialize = serialize}} |
110 |
110 |
111 end |
111 end |
112 |
112 |
113 |
113 |