src/HOL/Tools/SMT/cvc4_interface.ML

avoid hardwired frees;
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
end;

structure CVC4_Interface: CVC4_INTERFACE =
struct

val smtlib_cvc4C = SMTLIB_Interface.smtlibC @ ["cvc4"]


(* interface *)

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

val _ =
  Theory.setup (Context.theory_map (SMT_Translate.add_config (smtlib_cvc4C, translate_config)))

end

end;