src/HOL/Library/Old_SMT/old_smtlib_interface.ML
changeset 58058 1a0b18176548
parent 58057 883f3c4c928e
     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