equal
deleted
inserted
replaced
|
1 (* Title: HOL/Tools/SMT/z3_interface.ML |
|
2 Author: Sascha Boehme, TU Muenchen |
|
3 |
|
4 Interface to Z3 based on a relaxed version of SMT-LIB. |
|
5 *) |
|
6 |
|
7 signature Z3_INTERFACE = |
|
8 sig |
|
9 val interface: SMT_Translate.config |
|
10 |
|
11 val is_builtin: term -> bool |
|
12 end |
|
13 |
|
14 structure Z3_Interface: Z3_INTERFACE = |
|
15 struct |
|
16 |
|
17 fun z3_builtin_fun bf c ts = |
|
18 (case Const c of |
|
19 @{term "op / :: real => _"} => SOME ("/", ts) |
|
20 | _ => bf c ts) |
|
21 |
|
22 |
|
23 val {prefixes, strict, builtins, serialize} = SMTLIB_Interface.interface |
|
24 val {builtin_typ, builtin_num, builtin_fun} = builtins |
|
25 |
|
26 val interface = { |
|
27 extra_norm = |
|
28 translate = { |
|
29 prefixes = prefixes, |
|
30 strict = strict, |
|
31 builtins = { |
|
32 builtin_typ = builtin_typ, |
|
33 builtin_num = builtin_num, |
|
34 builtin_fun = z3_builtin_fun builtin_fun}, |
|
35 serialize = serialize}} |
|
36 |
|
37 end |