src/HOL/Tools/SMT/z3_interface.ML

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/SMT/z3_interface.ML	Wed May 12 23:54:02 2010 +0200
@@ -0,0 +1,37 @@
+(*  Title:      HOL/Tools/SMT/z3_interface.ML
+    Author:     Sascha Boehme, TU Muenchen
+
+Interface to Z3 based on a relaxed version of SMT-LIB.
+*)
+
+signature Z3_INTERFACE =
+sig
+  val interface: SMT_Translate.config
+
+  val is_builtin: term -> bool
+end
+
+structure Z3_Interface: Z3_INTERFACE =
+struct
+
+fun z3_builtin_fun bf c ts =
+  (case Const c of
+    @{term "op / :: real => _"} => SOME ("/", ts)
+  | _ => bf c ts)
+
+
+val {prefixes, strict, builtins, serialize} = SMTLIB_Interface.interface
+val {builtin_typ, builtin_num, builtin_fun} = builtins
+
+val interface = {
+  extra_norm = 
+  translate = {
+    prefixes = prefixes,
+    strict = strict,
+    builtins = {
+      builtin_typ = builtin_typ,
+      builtin_num = builtin_num,
+      builtin_fun = z3_builtin_fun builtin_fun},
+    serialize = serialize}}
+
+end