equal
deleted
inserted
replaced
1 (* Title: HOL/Tools/SMT/cvc4_interface.ML |
|
2 Author: Jasmin Blanchette, TU Muenchen |
|
3 |
|
4 Interface to CVC4 based on an extended version of SMT-LIB. |
|
5 *) |
|
6 |
|
7 signature CVC4_INTERFACE = |
|
8 sig |
|
9 val smtlib_cvc4C: SMT_Util.class |
|
10 val hosmtlib_cvc4C: SMT_Util.class |
|
11 end; |
|
12 |
|
13 structure CVC4_Interface: CVC4_INTERFACE = |
|
14 struct |
|
15 |
|
16 val cvc4C = ["cvc4"] |
|
17 val smtlib_cvc4C = SMTLIB_Interface.smtlibC @ cvc4C |
|
18 val hosmtlib_cvc4C = SMTLIB_Interface.hosmtlibC @ cvc4C |
|
19 |
|
20 |
|
21 (* interface *) |
|
22 |
|
23 local |
|
24 fun translate_config order ctxt = |
|
25 {order = order, |
|
26 logic = K (K "(set-logic ALL_SUPPORTED)\n"), |
|
27 fp_kinds = [BNF_Util.Least_FP, BNF_Util.Greatest_FP], |
|
28 serialize = #serialize (SMTLIB_Interface.translate_config order ctxt)} |
|
29 in |
|
30 |
|
31 val _ = Theory.setup (Context.theory_map |
|
32 (SMT_Translate.add_config (smtlib_cvc4C, translate_config SMT_Util.First_Order) #> |
|
33 SMT_Translate.add_config (hosmtlib_cvc4C, translate_config SMT_Util.Higher_Order))) |
|
34 |
|
35 end |
|
36 |
|
37 end; |
|