|
1 (* Title: HOL/Tools/SMT/vampire_interface.ML |
|
2 Author: Jasmin Blanchette, LMU Muenchen |
|
3 Author: Elisabeth Lempa, LMU Muenchen |
|
4 |
|
5 Interface to Vampire as an SMT prover. |
|
6 *) |
|
7 |
|
8 signature VAMPIRE_INTERFACE = |
|
9 sig |
|
10 val smtlib_vampireC: SMT_Util.class |
|
11 end; |
|
12 |
|
13 structure Vampire_Interface : VAMPIRE_INTERFACE = |
|
14 struct |
|
15 |
|
16 val vampireC = ["vampire"] |
|
17 val smtlib_vampireC = SMTLIB_Interface.smtlibC @ vampireC |
|
18 |
|
19 fun sctrarg (sel, typ) = "(" ^ sel ^ " " ^ typ ^ ")" |
|
20 fun sctr (name, args) = enclose "(" ")" (implode_space (name :: map sctrarg args)) |
|
21 fun sdatatype (_, ctrs) = enclose "(" ")" (implode_space (map sctr ctrs)) |
|
22 fun sarity (name, _) = enclose "(" ")" (name ^ " 0") |
|
23 |
|
24 fun sdtyp ((fp, dtyps : SMTLIB_Interface.dtype_decls)) = |
|
25 Buffer.add (enclose ("(declare-" ^ BNF_FP_Util.co_prefix fp ^ "datatypes (" ^ |
|
26 implode_space (map sarity dtyps) ^ ") (") "))\n" |
|
27 (space_implode"\n " (map sdatatype dtyps))) |
|
28 |
|
29 (* interface *) |
|
30 |
|
31 local |
|
32 fun translate_config ctxt : SMT_Translate.config = |
|
33 {order = SMT_Util.First_Order, |
|
34 logic = K (K ""), |
|
35 fp_kinds = [BNF_Util.Least_FP], |
|
36 serialize = SMTLIB_Interface.serialize sdtyp} |
|
37 in |
|
38 |
|
39 val _ = Theory.setup (Context.theory_map |
|
40 (SMT_Translate.add_config (smtlib_vampireC, translate_config))) |
|
41 |
|
42 end |
|
43 |
|
44 end; |