src/HOL/Tools/SMT/cvc4_interface.ML
author wenzelm
Sun Nov 26 21:08:32 2017 +0100 (18 months ago)
changeset 67091 1393c2340eec
parent 66551 4df6b0ae900d
permissions -rw-r--r--
more symbols;
     1 (*  Title:      HOL/Tools/SMT/cvc4_interface.ML
     2     Author:     Jasmin Blanchette, TU Muenchen
     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   val hosmtlib_cvc4C: SMT_Util.class
    11 end;
    12 
    13 structure CVC4_Interface: CVC4_INTERFACE =
    14 struct
    15 
    16 val cvc4C = ["cvc4"]
    17 val smtlib_cvc4C = SMTLIB_Interface.smtlibC @ cvc4C
    18 val hosmtlib_cvc4C = SMTLIB_Interface.hosmtlibC @ cvc4C
    19 
    20 
    21 (* interface *)
    22 
    23 local
    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)}
    29 in
    30 
    31 val _ = 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 
    35 end
    36 
    37 end;