src/HOL/Tools/SMT/cvc_interface.ML

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/SMT/cvc_interface.ML	Fri Aug 12 15:35:07 2022 +0200
@@ -0,0 +1,37 @@
+(*  Title:      HOL/Tools/SMT/cvc_interface.ML
+    Author:     Jasmin Blanchette, TU Muenchen
+
+Interface to CVC4 and cvc5 based on an extended version of SMT-LIB.
+*)
+
+signature CVC_INTERFACE =
+sig
+  val smtlib_cvcC: SMT_Util.class
+  val hosmtlib_cvcC: SMT_Util.class
+end;
+
+structure CVC_Interface: CVC_INTERFACE =
+struct
+
+val cvcC = ["cvc"]
+val smtlib_cvcC = SMTLIB_Interface.smtlibC @ cvcC
+val hosmtlib_cvcC = SMTLIB_Interface.hosmtlibC @ cvcC
+
+
+(* interface *)
+
+local
+  fun translate_config order ctxt =
+    {order = order,
+     logic = K (K "(set-logic ALL_SUPPORTED)\n"),
+     fp_kinds = [BNF_Util.Least_FP, BNF_Util.Greatest_FP],
+     serialize = #serialize (SMTLIB_Interface.translate_config order ctxt)}
+in
+
+val _ = Theory.setup (Context.theory_map
+  (SMT_Translate.add_config (smtlib_cvcC, translate_config SMT_Util.First_Order) #>
+   SMT_Translate.add_config (hosmtlib_cvcC, translate_config SMT_Util.Higher_Order)))
+
+end
+
+end;