src/HOL/Tools/SMT/cvc4_interface.ML
author blanchet
Wed Sep 17 16:53:39 2014 +0200 (2014-09-17)
changeset 58360 dee1fd1cc631
child 58369 149fb885dcd8
permissions -rw-r--r--
added interface for CVC4 extensions
blanchet@58360
     1
(*  Title:      HOL/Tools/SMT/cvc4_interface.ML
blanchet@58360
     2
    Author:     Sascha Boehme, 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@58360
    10
end;
blanchet@58360
    11
blanchet@58360
    12
structure CVC4_Interface: CVC4_INTERFACE =
blanchet@58360
    13
struct
blanchet@58360
    14
blanchet@58360
    15
val smtlib_cvc4C = SMTLIB_Interface.smtlibC @ ["cvc4"]
blanchet@58360
    16
blanchet@58360
    17
blanchet@58360
    18
(* interface *)
blanchet@58360
    19
blanchet@58360
    20
local
blanchet@58360
    21
  fun translate_config ctxt =
blanchet@58360
    22
    {logic = K "", fp_kinds = [BNF_Util.Least_FP, BNF_Util.Greatest_FP],
blanchet@58360
    23
     serialize = #serialize (SMTLIB_Interface.translate_config ctxt)}
blanchet@58360
    24
in
blanchet@58360
    25
blanchet@58360
    26
val _ =
blanchet@58360
    27
  Theory.setup (Context.theory_map (SMT_Translate.add_config (smtlib_cvc4C, translate_config)))
blanchet@58360
    28
blanchet@58360
    29
end
blanchet@58360
    30
blanchet@58360
    31
end;