58360
|
1 |
(* Title: HOL/Tools/SMT/cvc4_interface.ML
|
58369
|
2 |
Author: Jasmin Blanchette, TU Muenchen
|
58360
|
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 |
end;
|
|
11 |
|
|
12 |
structure CVC4_Interface: CVC4_INTERFACE =
|
|
13 |
struct
|
|
14 |
|
|
15 |
val smtlib_cvc4C = SMTLIB_Interface.smtlibC @ ["cvc4"]
|
|
16 |
|
|
17 |
|
|
18 |
(* interface *)
|
|
19 |
|
|
20 |
local
|
|
21 |
fun translate_config ctxt =
|
|
22 |
{logic = K "", fp_kinds = [BNF_Util.Least_FP, BNF_Util.Greatest_FP],
|
|
23 |
serialize = #serialize (SMTLIB_Interface.translate_config ctxt)}
|
|
24 |
in
|
|
25 |
|
|
26 |
val _ =
|
|
27 |
Theory.setup (Context.theory_map (SMT_Translate.add_config (smtlib_cvc4C, translate_config)))
|
|
28 |
|
|
29 |
end
|
|
30 |
|
|
31 |
end;
|