src/HOL/Tools/SMT/cvc4_interface.ML

tuned;

(*  Title:      HOL/Tools/SMT/cvc4_interface.ML
    Author:     Jasmin Blanchette, TU Muenchen

Interface to CVC4 based on an extended version of SMT-LIB.
*)

signature CVC4_INTERFACE =
sig
  val smtlib_cvc4C: SMT_Util.class
  val hosmtlib_cvc4C: SMT_Util.class
end;

structure CVC4_Interface: CVC4_INTERFACE =
struct

val cvc4C = ["cvc4"]
val smtlib_cvc4C = SMTLIB_Interface.smtlibC @ cvc4C
val hosmtlib_cvc4C = SMTLIB_Interface.hosmtlibC @ cvc4C


(* interface *)

local
  fun translate_config order ctxt =
    {order = order,
     logic = K "(set-logic ALL_SUPPORTED)\n",
     fp_kinds = [BNF_Util.Least_FP, BNF_Util.Greatest_FP],
     serialize = #serialize (SMTLIB_Interface.translate_config order ctxt)}
in

val _ = Theory.setup (Context.theory_map
  (SMT_Translate.add_config (smtlib_cvc4C, translate_config SMT_Util.First_Order) #>
   SMT_Translate.add_config (hosmtlib_cvc4C, translate_config SMT_Util.Higher_Order)))

end

end;