src/HOL/Tools/SMT/smtlib_interface.ML
author boehmes
Wed, 12 May 2010 23:54:02 +0200
changeset 36898 8e55aa1306c5
child 36899 bcd6fce5bf06
permissions -rw-r--r--
integrated SMT into the HOL image
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
     1
(*  Title:      HOL/Tools/SMT/smtlib_interface.ML
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
     2
    Author:     Sascha Boehme, TU Muenchen
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
     3
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
     4
Interface to SMT solvers based on the SMT-LIB format.
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
     5
*)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
     6
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
     7
signature SMTLIB_INTERFACE =
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
     8
sig
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
     9
  val interface: SMT_Solver.interface
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    10
end
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    11
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    12
structure SMTLIB_Interface: SMTLIB_INTERFACE =
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    13
struct
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    14
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    15
structure N = SMT_Normalize
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    16
structure T = SMT_Translate
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    17
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    18
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    19
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    20
(** facts about uninterpreted constants **)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    21
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    22
infix 2 ??
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    23
fun (ex ?? f) thms = if exists (ex o Thm.prop_of) thms then f thms else thms
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    24
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    25
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    26
(* pairs *)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    27
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    28
val pair_rules = [@{thm fst_conv}, @{thm snd_conv}, @{thm pair_collapse}]
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    29
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    30
val pair_type = (fn Type (@{type_name "*"}, _) => true | _ => false)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    31
val exists_pair_type = Term.exists_type (Term.exists_subtype pair_type)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    32
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    33
val add_pair_rules = exists_pair_type ?? append pair_rules
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    34
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    35
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    36
(* function update *)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    37
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    38
val fun_upd_rules = [@{thm fun_upd_same}, @{thm fun_upd_apply}]
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    39
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    40
val is_fun_upd = (fn Const (@{const_name fun_upd}, _) => true | _ => false)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    41
val exists_fun_upd = Term.exists_subterm is_fun_upd
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    42
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    43
val add_fun_upd_rules = exists_fun_upd ?? append fun_upd_rules
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    44
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    45
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    46
(* abs/min/max *)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    47
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    48
val exists_abs_min_max = Term.exists_subterm (fn
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    49
    Const (@{const_name abs}, _) => true
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    50
  | Const (@{const_name min}, _) => true
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    51
  | Const (@{const_name max}, _) => true
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    52
  | _ => false)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    53
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    54
val unfold_abs_conv = Conv.rewr_conv @{thm abs_if[THEN eq_reflection]}
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    55
val unfold_min_conv = Conv.rewr_conv @{thm min_def[THEN eq_reflection]}
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    56
val unfold_max_conv = Conv.rewr_conv @{thm max_def[THEN eq_reflection]}
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    57
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    58
fun expand_conv cv = N.eta_expand_conv (K cv)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    59
fun expand2_conv cv = N.eta_expand_conv (N.eta_expand_conv (K cv))
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    60
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    61
fun unfold_def_conv ctxt ct =
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    62
  (case Thm.term_of ct of
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    63
    Const (@{const_name abs}, _) $ _ => unfold_abs_conv
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    64
  | Const (@{const_name abs}, _) => expand_conv unfold_abs_conv ctxt
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    65
  | Const (@{const_name min}, _) $ _ $ _ => unfold_min_conv
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    66
  | Const (@{const_name min}, _) $ _ => expand_conv unfold_min_conv ctxt
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    67
  | Const (@{const_name min}, _) => expand2_conv unfold_min_conv ctxt
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    68
  | Const (@{const_name max}, _) $ _ $ _ => unfold_max_conv
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    69
  | Const (@{const_name max}, _) $ _ => expand_conv unfold_max_conv ctxt
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    70
  | Const (@{const_name max}, _) => expand2_conv unfold_max_conv ctxt
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    71
  | _ => Conv.all_conv) ct
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    72
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    73
fun unfold_abs_min_max_defs ctxt thm =
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    74
  if exists_abs_min_max (Thm.prop_of thm)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    75
  then Conv.fconv_rule (More_Conv.top_conv unfold_def_conv ctxt) thm
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    76
  else thm
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    77
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    78
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    79
(* include additional facts *)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    80
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    81
fun extra_norm thms ctxt =
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    82
  thms
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    83
  |> add_pair_rules
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    84
  |> add_fun_upd_rules
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    85
  |> map (unfold_abs_min_max_defs ctxt)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    86
  |> rpair ctxt
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    87
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    88
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    89
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    90
(** builtins **)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    91
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    92
fun dest_binT T =
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    93
  (case T of
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    94
    Type (@{type_name "Numeral_Type.num0"}, _) => 0
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    95
  | Type (@{type_name "Numeral_Type.num1"}, _) => 1
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    96
  | Type (@{type_name "Numeral_Type.bit0"}, [T]) => 2 * dest_binT T
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    97
  | Type (@{type_name "Numeral_Type.bit1"}, [T]) => 1 + 2 * dest_binT T
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    98
  | _ => raise TYPE ("dest_binT", [T], []))
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    99
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   100
fun dest_wordT (Type (@{type_name word}, [T])) = dest_binT T
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   101
  | dest_wordT T = raise TYPE ("dest_wordT", [T], [])
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   102
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   103
fun index1 n i = n ^ "[" ^ string_of_int i ^ "]"
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   104
fun index2 n i j = n ^ "[" ^ string_of_int i ^ ":" ^ string_of_int j ^ "]"
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   105
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   106
fun builtin_typ @{typ int} = SOME "Int"
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   107
  | builtin_typ @{typ real} = SOME "Real"
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   108
  | builtin_typ (Type (@{type_name word}, [T])) =
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   109
      Option.map (index1 "BitVec") (try dest_binT T)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   110
  | builtin_typ _ = NONE
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   111
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   112
fun builtin_num @{typ int} i = SOME (string_of_int i)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   113
  | builtin_num @{typ real} i = SOME (string_of_int i ^ ".0")
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   114
  | builtin_num (Type (@{type_name word}, [T])) i =
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   115
      Option.map (index1 ("bv" ^ string_of_int i)) (try dest_binT T)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   116
  | builtin_num _ _ = NONE
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   117
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   118
val is_propT = (fn @{typ prop} => true | _ => false)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   119
fun is_connT T = Term.strip_type T |> (fn (Us, U) => forall is_propT (U :: Us))
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   120
fun is_predT T = is_propT (Term.body_type T)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   121
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   122
fun just c ts = SOME (c, ts)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   123
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   124
val is_arith_type = member (op =) [@{typ int}, @{typ real}] o Term.domain_type
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   125
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   126
fun fixed_bvT (Ts, T) x =
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   127
  if forall (can dest_wordT) (T :: Ts) then SOME x else NONE
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   128
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   129
fun if_fixed_bvT' T = fixed_bvT ([], Term.domain_type T)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   130
fun if_fixed_bvT T = curry (fixed_bvT ([], Term.domain_type T))
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   131
fun if_full_fixed_bvT T = curry (fixed_bvT (Term.strip_type T))
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   132
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   133
fun dest_word_funT (Type ("fun", [T, U])) = (dest_wordT T, dest_wordT U)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   134
  | dest_word_funT T = raise TYPE ("dest_word_funT", [T], [])
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   135
fun dest_nat (@{term nat} $ n :: ts) = (snd (HOLogic.dest_number n), ts)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   136
  | dest_nat ts = raise TERM ("dest_nat", ts)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   137
fun dest_nat_word_funT (T, ts) =
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   138
  (dest_word_funT (Term.range_type T), dest_nat ts)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   139
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   140
fun bv_extend n T ts =
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   141
  (case try dest_word_funT T of
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   142
    SOME (i, j) => if j-i >= 0 then SOME (index1 n (j-i), ts) else NONE
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   143
  | _ => NONE)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   144
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   145
fun bv_rotate n T ts =
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   146
  try dest_nat ts
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   147
  |> Option.map (fn (i, ts') => (index1 n i, ts'))
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   148
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   149
fun bv_extract n T ts =
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   150
  try dest_nat_word_funT (T, ts)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   151
  |> Option.map (fn ((_, i), (lb, ts')) => (index2 n (i + lb - 1) lb, ts'))
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   152
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   153
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   154
fun conn @{const_name True} = SOME "true"
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   155
  | conn @{const_name False} = SOME "false"
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   156
  | conn @{const_name Not} = SOME "not"
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   157
  | conn @{const_name "op &"} = SOME "and"
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   158
  | conn @{const_name "op |"} = SOME "or"
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   159
  | conn @{const_name "op -->"} = SOME "implies"
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   160
  | conn @{const_name "op ="} = SOME "iff"
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   161
  | conn @{const_name If} = SOME "if_then_else"
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   162
  | conn _ = NONE
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   163
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   164
fun pred @{const_name distinct} _ = SOME "distinct"
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   165
  | pred @{const_name "op ="} _ = SOME "="
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   166
  | pred @{const_name term_eq} _ = SOME "="
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   167
  | pred @{const_name less} T =
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   168
      if is_arith_type T then SOME "<"
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   169
      else if_fixed_bvT' T "bvult"
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   170
  | pred @{const_name less_eq} T =
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   171
      if is_arith_type T then SOME "<="
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   172
      else if_fixed_bvT' T "bvule"
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   173
  | pred @{const_name word_sless} T = if_fixed_bvT' T "bvslt"
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   174
  | pred @{const_name word_sle} T = if_fixed_bvT' T "bvsle"
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   175
  | pred _ _ = NONE
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   176
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   177
fun func @{const_name If} _ = just "ite"
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   178
  | func @{const_name uminus} T =
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   179
      if is_arith_type T then just "~"
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   180
      else if_fixed_bvT T "bvneg"
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   181
  | func @{const_name plus} T = 
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   182
      if is_arith_type T then just "+"
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   183
      else if_fixed_bvT T "bvadd"
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   184
  | func @{const_name minus} T =
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   185
      if is_arith_type T then just "-"
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   186
      else if_fixed_bvT T "bvsub"
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   187
  | func @{const_name times} T = 
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   188
      if is_arith_type T then just "*"
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   189
      else if_fixed_bvT T "bvmul"
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   190
  | func @{const_name bitNOT} T = if_fixed_bvT T "bvnot"
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   191
  | func @{const_name bitAND} T = if_fixed_bvT T "bvand"
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   192
  | func @{const_name bitOR} T = if_fixed_bvT T "bvor"
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   193
  | func @{const_name bitXOR} T = if_fixed_bvT T "bvxor"
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   194
  | func @{const_name div} T = if_fixed_bvT T "bvudiv"
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   195
  | func @{const_name mod} T = if_fixed_bvT T "bvurem"
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   196
  | func @{const_name sdiv} T = if_fixed_bvT T "bvsdiv"
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   197
  | func @{const_name smod} T = if_fixed_bvT T "bvsmod"
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   198
  | func @{const_name srem} T = if_fixed_bvT T "bvsrem"
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   199
  | func @{const_name word_cat} T = if_full_fixed_bvT T "concat"
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   200
  | func @{const_name bv_shl} T = if_full_fixed_bvT T "bvshl"
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   201
  | func @{const_name bv_lshr} T = if_full_fixed_bvT T "bvlshr"
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   202
  | func @{const_name bv_ashr} T = if_full_fixed_bvT T "bvashr"
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   203
  | func @{const_name slice} T = bv_extract "extract" T
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   204
  | func @{const_name ucast} T = bv_extend "zero_extend" T
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   205
  | func @{const_name scast} T = bv_extend "sign_extend" T
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   206
  | func @{const_name word_rotl} T = bv_rotate "rotate_left" T
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   207
  | func @{const_name word_rotr} T = bv_rotate "rotate_right" T
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   208
  | func _ _ = K NONE
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   209
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   210
fun is_builtin_conn (n, T) = is_connT T andalso is_some (conn n)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   211
fun is_builtin_pred (n, T) = is_predT T andalso is_some (pred n T)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   212
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   213
fun builtin_fun (n, T) ts =
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   214
  if is_connT T then conn n |> Option.map (rpair ts)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   215
  else if is_predT T then pred n T |> Option.map (rpair ts)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   216
  else func n T ts
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   217
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   218
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   219
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   220
(** serialization **)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   221
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   222
val add = Buffer.add
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   223
fun sep f = add " " #> f
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   224
fun enclose l r f = sep (add l #> f #> add r)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   225
val par = enclose "(" ")"
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   226
fun app n f = (fn [] => sep (add n) | xs => par (add n #> fold f xs))
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   227
fun line f = f #> add "\n"
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   228
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   229
fun var i = add "?v" #> add (string_of_int i)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   230
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   231
fun sterm l (T.SVar i) = sep (var (l - i - 1))
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   232
  | sterm l (T.SApp (n, ts)) = app n (sterm l) ts
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   233
  | sterm _ (T.SLet _) = raise Fail "SMT-LIB: unsupported let expression"
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   234
  | sterm l (T.SQua (q, ss, ps, t)) =
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   235
      let
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   236
        val quant = add o (fn T.SForall => "forall" | T.SExists => "exists")
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   237
        val vs = map_index (apfst (Integer.add l)) ss
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   238
        fun var_decl (i, s) = par (var i #> sep (add s))
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   239
        val sub = sterm (l + length ss)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   240
        fun pat kind ts = sep (add kind #> enclose "{" " }" (fold sub ts))
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   241
        fun pats (T.SPat ts) = pat ":pat" ts
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   242
          | pats (T.SNoPat ts) = pat ":nopat" ts
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   243
      in par (quant q #> fold var_decl vs #> sub t #> fold pats ps) end
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   244
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   245
fun choose_logic theories =
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   246
  if member (op =) theories T.Bitvector then "QF_AUFBV"
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   247
  else if member (op =) theories T.Real then "AUFLIRA"
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   248
  else "AUFLIA"
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   249
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   250
fun serialize comments {theories, sorts, funcs} ts =
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   251
  Buffer.empty
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   252
  |> line (add "(benchmark Isabelle")
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   253
  |> line (add ":status unknown")
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   254
  |> line (add ":logic " #> add (choose_logic theories))
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   255
  |> length sorts > 0 ?
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   256
       line (add ":extrasorts" #> par (fold (sep o add) sorts))
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   257
  |> length funcs > 0 ? (
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   258
       line (add ":extrafuns" #> add " (") #>
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   259
       fold (fn (f, (ss, s)) =>
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   260
         line (sep (app f (sep o add) (ss @ [s])))) funcs #>
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   261
       line (add ")"))
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   262
  |> fold (fn t => line (add ":assumption" #> sterm 0 t)) ts
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   263
  |> line (add ":formula true)")
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   264
  |> fold (fn str => line (add "; " #> add str)) comments
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   265
  |> Buffer.content
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   266
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   267
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   268
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   269
(** interface **)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   270
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   271
val interface = {
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   272
  extra_norm = extra_norm,
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   273
  translate = {
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   274
    prefixes = {
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   275
      sort_prefix = "S",
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   276
      func_prefix = "f"},
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   277
    strict = SOME {
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   278
      is_builtin_conn = is_builtin_conn,
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   279
      is_builtin_pred = is_builtin_pred,
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   280
      is_builtin_distinct = true},
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   281
    builtins = {
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   282
      builtin_typ = builtin_typ,
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   283
      builtin_num = builtin_num,
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   284
      builtin_fun = builtin_fun},
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   285
    serialize = serialize}}
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   286
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   287
end