src/HOL/Tools/SMT/cvc4_interface.ML
changeset 58360 dee1fd1cc631
child 58369 149fb885dcd8
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Tools/SMT/cvc4_interface.ML	Wed Sep 17 16:53:39 2014 +0200
     1.3 @@ -0,0 +1,31 @@
     1.4 +(*  Title:      HOL/Tools/SMT/cvc4_interface.ML
     1.5 +    Author:     Sascha Boehme, TU Muenchen
     1.6 +
     1.7 +Interface to CVC4 based on an extended version of SMT-LIB.
     1.8 +*)
     1.9 +
    1.10 +signature CVC4_INTERFACE =
    1.11 +sig
    1.12 +  val smtlib_cvc4C: SMT_Util.class
    1.13 +end;
    1.14 +
    1.15 +structure CVC4_Interface: CVC4_INTERFACE =
    1.16 +struct
    1.17 +
    1.18 +val smtlib_cvc4C = SMTLIB_Interface.smtlibC @ ["cvc4"]
    1.19 +
    1.20 +
    1.21 +(* interface *)
    1.22 +
    1.23 +local
    1.24 +  fun translate_config ctxt =
    1.25 +    {logic = K "", fp_kinds = [BNF_Util.Least_FP, BNF_Util.Greatest_FP],
    1.26 +     serialize = #serialize (SMTLIB_Interface.translate_config ctxt)}
    1.27 +in
    1.28 +
    1.29 +val _ =
    1.30 +  Theory.setup (Context.theory_map (SMT_Translate.add_config (smtlib_cvc4C, translate_config)))
    1.31 +
    1.32 +end
    1.33 +
    1.34 +end;