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