blanchet@58058: (*  Title:      HOL/Library/Old_SMT/old_smtlib_interface.ML
boehmes@36898:     Author:     Sascha Boehme, TU Muenchen
boehmes@36898: 
boehmes@36898: Interface to SMT solvers based on the SMT-LIB format.
boehmes@36898: *)
boehmes@36898: 
blanchet@58058: signature OLD_SMTLIB_INTERFACE =
boehmes@36898: sig
blanchet@58058:   val smtlibC: Old_SMT_Utils.class
boehmes@41059:   val add_logic: int * (term list -> string option) -> Context.generic ->
boehmes@36899:     Context.generic
blanchet@58058:   val translate_config: Proof.context -> Old_SMT_Translate.config
boehmes@41059:   val setup: theory -> theory
boehmes@36898: end
boehmes@36898: 
blanchet@58058: structure Old_SMTLIB_Interface: OLD_SMTLIB_INTERFACE =
boehmes@36898: struct
boehmes@36898: 
boehmes@36898: 
boehmes@41059: val smtlibC = ["smtlib"]
boehmes@36898: 
boehmes@36898: 
boehmes@41059: (* builtins *)
boehmes@36898: 
boehmes@41059: local
boehmes@41059:   fun int_num _ i = SOME (string_of_int i)
boehmes@36899: 
blanchet@58058:   fun is_linear [t] = Old_SMT_Utils.is_number t
blanchet@58058:     | is_linear [t, u] = Old_SMT_Utils.is_number t orelse Old_SMT_Utils.is_number u
boehmes@41280:     | is_linear _ = false
boehmes@41280: 
boehmes@41281:   fun times _ _ ts =
boehmes@41281:     let val mk = Term.list_comb o pair @{const times (int)}
boehmes@41281:     in if is_linear ts then SOME ("*", 2, ts, mk) else NONE end
boehmes@41059: in
boehmes@36898: 
boehmes@41072: val setup_builtins =
blanchet@58058:   Old_SMT_Builtin.add_builtin_typ smtlibC (@{typ int}, K (SOME "Int"), int_num) #>
blanchet@58058:   fold (Old_SMT_Builtin.add_builtin_fun' smtlibC) [
boehmes@41059:     (@{const True}, "true"),
boehmes@41059:     (@{const False}, "false"),
boehmes@41059:     (@{const Not}, "not"),
boehmes@41059:     (@{const HOL.conj}, "and"),
boehmes@41059:     (@{const HOL.disj}, "or"),
boehmes@41059:     (@{const HOL.implies}, "implies"),
boehmes@41059:     (@{const HOL.eq (bool)}, "iff"),
boehmes@41059:     (@{const HOL.eq ('a)}, "="),
boehmes@41059:     (@{const If (bool)}, "if_then_else"),
boehmes@41059:     (@{const If ('a)}, "ite"),
boehmes@41059:     (@{const less (int)}, "<"),
boehmes@41059:     (@{const less_eq (int)}, "<="),
boehmes@41059:     (@{const uminus (int)}, "~"),
boehmes@41059:     (@{const plus (int)}, "+"),
boehmes@41280:     (@{const minus (int)}, "-") ] #>
blanchet@58058:   Old_SMT_Builtin.add_builtin_fun smtlibC
boehmes@47155:     (Term.dest_Const @{const times (int)}, times)
boehmes@36898: 
boehmes@41059: end
boehmes@36898: 
boehmes@36898: 
boehmes@41059: (* serialization *)
boehmes@36898: 
boehmes@41059: (** header **)
boehmes@41059: 
boehmes@41059: fun fst_int_ord ((i1, _), (i2, _)) = int_ord (i1, i2)
boehmes@36899: 
boehmes@36899: structure Logics = Generic_Data
boehmes@36899: (
boehmes@36899:   type T = (int * (term list -> string option)) list
boehmes@36899:   val empty = []
boehmes@36899:   val extend = I
wenzelm@41473:   fun merge data = Ord_List.merge fst_int_ord data
boehmes@36899: )
boehmes@36899: 
boehmes@41059: fun add_logic pf = Logics.map (Ord_List.insert fst_int_ord pf)
boehmes@36899: 
boehmes@36899: fun choose_logic ctxt ts =
boehmes@36899:   let
boehmes@36899:     fun choose [] = "AUFLIA"
boehmes@41059:       | choose ((_, f) :: fs) = (case f ts of SOME s => s | NONE => choose fs)
boehmes@41059:   in [":logic " ^ choose (Logics.get (Context.Proof ctxt))] end
boehmes@36899: 
boehmes@36899: 
boehmes@41072: (** serialization **)
boehmes@36899: 
boehmes@36898: val add = Buffer.add
boehmes@36898: fun sep f = add " " #> f
boehmes@36898: fun enclose l r f = sep (add l #> f #> add r)
boehmes@36898: val par = enclose "(" ")"
boehmes@36898: fun app n f = (fn [] => sep (add n) | xs => par (add n #> fold f xs))
boehmes@36898: fun line f = f #> add "\n"
boehmes@36898: 
boehmes@36898: fun var i = add "?v" #> add (string_of_int i)
boehmes@36898: 
blanchet@58058: fun sterm l (Old_SMT_Translate.SVar i) = sep (var (l - i - 1))
blanchet@58058:   | sterm l (Old_SMT_Translate.SApp (n, ts)) = app n (sterm l) ts
blanchet@58058:   | sterm _ (Old_SMT_Translate.SLet _) =
boehmes@41328:       raise Fail "SMT-LIB: unsupported let expression"
blanchet@58058:   | sterm l (Old_SMT_Translate.SQua (q, ss, ps, w, t)) =
boehmes@36898:       let
blanchet@58058:         fun quant Old_SMT_Translate.SForall = add "forall"
blanchet@58058:           | quant Old_SMT_Translate.SExists = add "exists"
boehmes@36898:         val vs = map_index (apfst (Integer.add l)) ss
boehmes@36898:         fun var_decl (i, s) = par (var i #> sep (add s))
boehmes@36898:         val sub = sterm (l + length ss)
boehmes@36898:         fun pat kind ts = sep (add kind #> enclose "{" " }" (fold sub ts))
blanchet@58058:         fun pats (Old_SMT_Translate.SPat ts) = pat ":pat" ts
blanchet@58058:           | pats (Old_SMT_Translate.SNoPat ts) = pat ":nopat" ts
boehmes@40664:         fun weight NONE = I
boehmes@40664:           | weight (SOME i) =
boehmes@40664:               sep (add ":weight { " #> add (string_of_int i) #> add " }")
boehmes@40664:       in
boehmes@40664:         par (quant q #> fold var_decl vs #> sub t #> fold pats ps #> weight w)
boehmes@40664:       end
boehmes@36898: 
boehmes@37155: fun ssort sorts = sort fast_string_ord sorts
boehmes@37155: fun fsort funcs = sort (prod_ord fast_string_ord (K EQUAL)) funcs
boehmes@37155: 
boehmes@39298: fun sdatatypes decls =
boehmes@39298:   let
boehmes@41426:     fun con (n, []) = sep (add n)
boehmes@39298:       | con (n, sels) = par (add n #>
boehmes@41426:           fold (fn (n, s) => par (add n #> sep (add s))) sels)
boehmes@41426:     fun dtyp (n, decl) = add n #> fold con decl
boehmes@39298:   in line (add ":datatypes " #> par (fold (par o dtyp) decls)) end
boehmes@39298: 
boehmes@39298: fun serialize comments {header, sorts, dtyps, funcs} ts =
boehmes@36898:   Buffer.empty
boehmes@36898:   |> line (add "(benchmark Isabelle")
boehmes@36898:   |> line (add ":status unknown")
boehmes@36899:   |> fold (line o add) header
boehmes@36898:   |> length sorts > 0 ?
boehmes@37155:        line (add ":extrasorts" #> par (fold (sep o add) (ssort sorts)))
boehmes@39298:   |> fold sdatatypes dtyps
boehmes@36898:   |> length funcs > 0 ? (
boehmes@36898:        line (add ":extrafuns" #> add " (") #>
boehmes@36898:        fold (fn (f, (ss, s)) =>
boehmes@37155:          line (sep (app f (sep o add) (ss @ [s])))) (fsort funcs) #>
boehmes@36898:        line (add ")"))
boehmes@36898:   |> fold (fn t => line (add ":assumption" #> sterm 0 t)) ts
boehmes@36898:   |> line (add ":formula true)")
boehmes@36898:   |> fold (fn str => line (add "; " #> add str)) comments
boehmes@36898:   |> Buffer.content
boehmes@36898: 
boehmes@36898: 
boehmes@41072: (* interface *)
boehmes@36898: 
boehmes@41127: fun translate_config ctxt = {
boehmes@41127:   prefixes = {
boehmes@41127:     sort_prefix = "S",
boehmes@41127:     func_prefix = "f"},
boehmes@41127:   header = choose_logic ctxt,
boehmes@41127:   is_fol = true,
boehmes@41127:   has_datatypes = false,
boehmes@41127:   serialize = serialize}
boehmes@36898: 
boehmes@41127: val setup = Context.theory_map (
boehmes@41127:   setup_builtins #>
blanchet@58058:   Old_SMT_Translate.add_config (smtlibC, translate_config))
boehmes@41072: 
boehmes@36898: end