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;
blanchet@58360
     1
(*  Title:      HOL/Tools/SMT/cvc4_interface.ML
blanchet@58369
     2
    Author:     Jasmin Blanchette, TU Muenchen
blanchet@58360
     3
blanchet@58360
     4
Interface to CVC4 based on an extended version of SMT-LIB.
blanchet@58360
     5
*)
blanchet@58360
     6
blanchet@58360
     7
signature CVC4_INTERFACE =
blanchet@58360
     8
sig
blanchet@58360
     9
  val smtlib_cvc4C: SMT_Util.class
blanchet@66551
    10
  val hosmtlib_cvc4C: SMT_Util.class
blanchet@58360
    11
end;
blanchet@58360
    12
blanchet@58360
    13
structure CVC4_Interface: CVC4_INTERFACE =
blanchet@58360
    14
struct
blanchet@58360
    15
blanchet@66551
    16
val cvc4C = ["cvc4"]
blanchet@66551
    17
val smtlib_cvc4C = SMTLIB_Interface.smtlibC @ cvc4C
blanchet@66551
    18
val hosmtlib_cvc4C = SMTLIB_Interface.hosmtlibC @ cvc4C
blanchet@58360
    19
blanchet@58360
    20
blanchet@58360
    21
(* interface *)
blanchet@58360
    22
blanchet@58360
    23
local
blanchet@66551
    24
  fun translate_config order ctxt =
blanchet@66551
    25
    {order = order,
blanchet@66551
    26
     logic = K "(set-logic ALL_SUPPORTED)\n",
blanchet@66551
    27
     fp_kinds = [BNF_Util.Least_FP, BNF_Util.Greatest_FP],
blanchet@66551
    28
     serialize = #serialize (SMTLIB_Interface.translate_config order ctxt)}
blanchet@58360
    29
in
blanchet@58360
    30
blanchet@66551
    31
val _ = Theory.setup (Context.theory_map
blanchet@66551
    32
  (SMT_Translate.add_config (smtlib_cvc4C, translate_config SMT_Util.First_Order) #>
blanchet@66551
    33
   SMT_Translate.add_config (hosmtlib_cvc4C, translate_config SMT_Util.Higher_Order)))
blanchet@58360
    34
blanchet@58360
    35
end
blanchet@58360
    36
blanchet@58360
    37
end;