1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/src/HOL/Library/Old_SMT/old_smtlib_interface.ML Thu Aug 28 00:40:38 2014 +0200
1.3 @@ -0,0 +1,161 @@
1.4 +(* Title: HOL/Library/Old_SMT/old_smtlib_interface.ML
1.5 + Author: Sascha Boehme, TU Muenchen
1.6 +
1.7 +Interface to SMT solvers based on the SMT-LIB format.
1.8 +*)
1.9 +
1.10 +signature OLD_SMTLIB_INTERFACE =
1.11 +sig
1.12 + val smtlibC: Old_SMT_Utils.class
1.13 + val add_logic: int * (term list -> string option) -> Context.generic ->
1.14 + Context.generic
1.15 + val translate_config: Proof.context -> Old_SMT_Translate.config
1.16 + val setup: theory -> theory
1.17 +end
1.18 +
1.19 +structure Old_SMTLIB_Interface: OLD_SMTLIB_INTERFACE =
1.20 +struct
1.21 +
1.22 +
1.23 +val smtlibC = ["smtlib"]
1.24 +
1.25 +
1.26 +(* builtins *)
1.27 +
1.28 +local
1.29 + fun int_num _ i = SOME (string_of_int i)
1.30 +
1.31 + fun is_linear [t] = Old_SMT_Utils.is_number t
1.32 + | is_linear [t, u] = Old_SMT_Utils.is_number t orelse Old_SMT_Utils.is_number u
1.33 + | is_linear _ = false
1.34 +
1.35 + fun times _ _ ts =
1.36 + let val mk = Term.list_comb o pair @{const times (int)}
1.37 + in if is_linear ts then SOME ("*", 2, ts, mk) else NONE end
1.38 +in
1.39 +
1.40 +val setup_builtins =
1.41 + Old_SMT_Builtin.add_builtin_typ smtlibC (@{typ int}, K (SOME "Int"), int_num) #>
1.42 + fold (Old_SMT_Builtin.add_builtin_fun' smtlibC) [
1.43 + (@{const True}, "true"),
1.44 + (@{const False}, "false"),
1.45 + (@{const Not}, "not"),
1.46 + (@{const HOL.conj}, "and"),
1.47 + (@{const HOL.disj}, "or"),
1.48 + (@{const HOL.implies}, "implies"),
1.49 + (@{const HOL.eq (bool)}, "iff"),
1.50 + (@{const HOL.eq ('a)}, "="),
1.51 + (@{const If (bool)}, "if_then_else"),
1.52 + (@{const If ('a)}, "ite"),
1.53 + (@{const less (int)}, "<"),
1.54 + (@{const less_eq (int)}, "<="),
1.55 + (@{const uminus (int)}, "~"),
1.56 + (@{const plus (int)}, "+"),
1.57 + (@{const minus (int)}, "-") ] #>
1.58 + Old_SMT_Builtin.add_builtin_fun smtlibC
1.59 + (Term.dest_Const @{const times (int)}, times)
1.60 +
1.61 +end
1.62 +
1.63 +
1.64 +(* serialization *)
1.65 +
1.66 +(** header **)
1.67 +
1.68 +fun fst_int_ord ((i1, _), (i2, _)) = int_ord (i1, i2)
1.69 +
1.70 +structure Logics = Generic_Data
1.71 +(
1.72 + type T = (int * (term list -> string option)) list
1.73 + val empty = []
1.74 + val extend = I
1.75 + fun merge data = Ord_List.merge fst_int_ord data
1.76 +)
1.77 +
1.78 +fun add_logic pf = Logics.map (Ord_List.insert fst_int_ord pf)
1.79 +
1.80 +fun choose_logic ctxt ts =
1.81 + let
1.82 + fun choose [] = "AUFLIA"
1.83 + | choose ((_, f) :: fs) = (case f ts of SOME s => s | NONE => choose fs)
1.84 + in [":logic " ^ choose (Logics.get (Context.Proof ctxt))] end
1.85 +
1.86 +
1.87 +(** serialization **)
1.88 +
1.89 +val add = Buffer.add
1.90 +fun sep f = add " " #> f
1.91 +fun enclose l r f = sep (add l #> f #> add r)
1.92 +val par = enclose "(" ")"
1.93 +fun app n f = (fn [] => sep (add n) | xs => par (add n #> fold f xs))
1.94 +fun line f = f #> add "\n"
1.95 +
1.96 +fun var i = add "?v" #> add (string_of_int i)
1.97 +
1.98 +fun sterm l (Old_SMT_Translate.SVar i) = sep (var (l - i - 1))
1.99 + | sterm l (Old_SMT_Translate.SApp (n, ts)) = app n (sterm l) ts
1.100 + | sterm _ (Old_SMT_Translate.SLet _) =
1.101 + raise Fail "SMT-LIB: unsupported let expression"
1.102 + | sterm l (Old_SMT_Translate.SQua (q, ss, ps, w, t)) =
1.103 + let
1.104 + fun quant Old_SMT_Translate.SForall = add "forall"
1.105 + | quant Old_SMT_Translate.SExists = add "exists"
1.106 + val vs = map_index (apfst (Integer.add l)) ss
1.107 + fun var_decl (i, s) = par (var i #> sep (add s))
1.108 + val sub = sterm (l + length ss)
1.109 + fun pat kind ts = sep (add kind #> enclose "{" " }" (fold sub ts))
1.110 + fun pats (Old_SMT_Translate.SPat ts) = pat ":pat" ts
1.111 + | pats (Old_SMT_Translate.SNoPat ts) = pat ":nopat" ts
1.112 + fun weight NONE = I
1.113 + | weight (SOME i) =
1.114 + sep (add ":weight { " #> add (string_of_int i) #> add " }")
1.115 + in
1.116 + par (quant q #> fold var_decl vs #> sub t #> fold pats ps #> weight w)
1.117 + end
1.118 +
1.119 +fun ssort sorts = sort fast_string_ord sorts
1.120 +fun fsort funcs = sort (prod_ord fast_string_ord (K EQUAL)) funcs
1.121 +
1.122 +fun sdatatypes decls =
1.123 + let
1.124 + fun con (n, []) = sep (add n)
1.125 + | con (n, sels) = par (add n #>
1.126 + fold (fn (n, s) => par (add n #> sep (add s))) sels)
1.127 + fun dtyp (n, decl) = add n #> fold con decl
1.128 + in line (add ":datatypes " #> par (fold (par o dtyp) decls)) end
1.129 +
1.130 +fun serialize comments {header, sorts, dtyps, funcs} ts =
1.131 + Buffer.empty
1.132 + |> line (add "(benchmark Isabelle")
1.133 + |> line (add ":status unknown")
1.134 + |> fold (line o add) header
1.135 + |> length sorts > 0 ?
1.136 + line (add ":extrasorts" #> par (fold (sep o add) (ssort sorts)))
1.137 + |> fold sdatatypes dtyps
1.138 + |> length funcs > 0 ? (
1.139 + line (add ":extrafuns" #> add " (") #>
1.140 + fold (fn (f, (ss, s)) =>
1.141 + line (sep (app f (sep o add) (ss @ [s])))) (fsort funcs) #>
1.142 + line (add ")"))
1.143 + |> fold (fn t => line (add ":assumption" #> sterm 0 t)) ts
1.144 + |> line (add ":formula true)")
1.145 + |> fold (fn str => line (add "; " #> add str)) comments
1.146 + |> Buffer.content
1.147 +
1.148 +
1.149 +(* interface *)
1.150 +
1.151 +fun translate_config ctxt = {
1.152 + prefixes = {
1.153 + sort_prefix = "S",
1.154 + func_prefix = "f"},
1.155 + header = choose_logic ctxt,
1.156 + is_fol = true,
1.157 + has_datatypes = false,
1.158 + serialize = serialize}
1.159 +
1.160 +val setup = Context.theory_map (
1.161 + setup_builtins #>
1.162 + Old_SMT_Translate.add_config (smtlibC, translate_config))
1.163 +
1.164 +end