src/HOL/Tools/SMT/cvc4_interface.ML

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/SMT/cvc4_interface.ML	Wed Sep 17 16:53:39 2014 +0200
@@ -0,0 +1,31 @@
+(*  Title:      HOL/Tools/SMT/cvc4_interface.ML
+    Author:     Sascha Boehme, TU Muenchen
+
+Interface to CVC4 based on an extended version of SMT-LIB.
+*)
+
+signature CVC4_INTERFACE =
+sig
+  val smtlib_cvc4C: SMT_Util.class
+end;
+
+structure CVC4_Interface: CVC4_INTERFACE =
+struct
+
+val smtlib_cvc4C = SMTLIB_Interface.smtlibC @ ["cvc4"]
+
+
+(* interface *)
+
+local
+  fun translate_config ctxt =
+    {logic = K "", fp_kinds = [BNF_Util.Least_FP, BNF_Util.Greatest_FP],
+     serialize = #serialize (SMTLIB_Interface.translate_config ctxt)}
+in
+
+val _ =
+  Theory.setup (Context.theory_map (SMT_Translate.add_config (smtlib_cvc4C, translate_config)))
+
+end
+
+end;