1(*  Title:      HOL/Tools/SMT/cvc4_interface.ML
2    Author:     Jasmin Blanchette, TU Muenchen
3
4Interface to CVC4 based on an extended version of SMT-LIB.
5*)
6
7signature CVC4_INTERFACE =
8sig
9  val smtlib_cvc4C: SMT_Util.class
10  val hosmtlib_cvc4C: SMT_Util.class
11end;
12
13structure CVC4_Interface: CVC4_INTERFACE =
14struct
15
16val cvc4C = ["cvc4"]
17val smtlib_cvc4C = SMTLIB_Interface.smtlibC @ cvc4C
18val hosmtlib_cvc4C = SMTLIB_Interface.hosmtlibC @ cvc4C
19
20
21(* interface *)
22
23local
24  fun translate_config order ctxt =
25    {order = order,
26     logic = 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)}
29in
30
31val _ = 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
35end
36
37end;
38