src/HOL/Library/Old_SMT/old_z3_model.ML
author wenzelm
Wed Jun 17 11:03:05 2015 +0200 (2015-06-17)
changeset 60500 903bb1495239
parent 59058 a78612c67ec0
permissions -rw-r--r--
isabelle update_cartouches;
blanchet@58058
     1
(*  Title:      HOL/Library/Old_SMT/old_z3_model.ML
boehmes@36898
     2
    Author:     Sascha Boehme and Philipp Meyer, TU Muenchen
boehmes@36898
     3
boehmes@36898
     4
Parser for counterexamples generated by Z3.
boehmes@36898
     5
*)
boehmes@36898
     6
blanchet@58058
     7
signature OLD_Z3_MODEL =
boehmes@36898
     8
sig
blanchet@58058
     9
  val parse_counterex: Proof.context -> Old_SMT_Translate.recon -> string list ->
boehmes@40828
    10
    term list * term list
boehmes@36898
    11
end
boehmes@36898
    12
blanchet@58058
    13
structure Old_Z3_Model: OLD_Z3_MODEL =
boehmes@36898
    14
struct
boehmes@36898
    15
boehmes@40663
    16
boehmes@36898
    17
(* counterexample expressions *)
boehmes@36898
    18
boehmes@36898
    19
datatype expr = True | False | Number of int * int option | Value of int |
boehmes@39536
    20
  Array of array | App of string * expr list
boehmes@36898
    21
and array = Fresh of expr | Store of (array * expr) * expr
boehmes@36898
    22
boehmes@36898
    23
boehmes@36898
    24
(* parsing *)
boehmes@36898
    25
boehmes@36898
    26
val space = Scan.many Symbol.is_ascii_blank
boehmes@39536
    27
fun spaced p = p --| space
boehmes@39536
    28
fun in_parens p = spaced (Scan.$$ "(") |-- p --| spaced (Scan.$$ ")")
boehmes@39536
    29
fun in_braces p = spaced (Scan.$$ "{") |-- p --| spaced (Scan.$$ "}")
boehmes@36898
    30
boehmes@36898
    31
val digit = (fn
boehmes@36898
    32
  "0" => SOME 0 | "1" => SOME 1 | "2" => SOME 2 | "3" => SOME 3 |
boehmes@36898
    33
  "4" => SOME 4 | "5" => SOME 5 | "6" => SOME 6 | "7" => SOME 7 |
boehmes@36898
    34
  "8" => SOME 8 | "9" => SOME 9 | _ => NONE)
boehmes@36898
    35
boehmes@39536
    36
val nat_num = spaced (Scan.repeat1 (Scan.some digit) >>
boehmes@39536
    37
  (fn ds => fold (fn d => fn i => i * 10 + d) ds 0))
boehmes@39536
    38
val int_num = spaced (Scan.optional ($$ "-" >> K (fn i => ~i)) I :|--
boehmes@39536
    39
  (fn sign => nat_num >> sign))
boehmes@36898
    40
boehmes@36898
    41
val is_char = Symbol.is_ascii_letter orf Symbol.is_ascii_digit orf
wenzelm@40627
    42
  member (op =) (raw_explode "_+*-/%~=<>$&|?!.@^#")
boehmes@39536
    43
val name = spaced (Scan.many1 is_char >> implode)
boehmes@39536
    44
boehmes@39536
    45
fun $$$ s = spaced (Scan.this_string s)
boehmes@36898
    46
boehmes@39536
    47
fun array_expr st = st |> in_parens (
boehmes@39536
    48
  $$$ "const" |-- expr >> Fresh ||
boehmes@39536
    49
  $$$ "store" |-- array_expr -- expr -- expr >> Store)
boehmes@36898
    50
boehmes@39536
    51
and expr st = st |> (
boehmes@39536
    52
  $$$ "true" >> K True ||
boehmes@39536
    53
  $$$ "false" >> K False ||
boehmes@39536
    54
  int_num -- Scan.option ($$$ "/" |-- int_num) >> Number ||
boehmes@39536
    55
  $$$ "val!" |-- nat_num >> Value ||
boehmes@39536
    56
  name >> (App o rpair []) ||
boehmes@39536
    57
  array_expr >> Array ||
boehmes@39536
    58
  in_parens (name -- Scan.repeat1 expr) >> App)
boehmes@36898
    59
boehmes@39536
    60
fun args st = ($$$ "->" >> K [] || expr ::: args) st
boehmes@39536
    61
val args_case = args -- expr
boehmes@39536
    62
val else_case = $$$ "else" -- $$$ "->" |-- expr >> pair ([] : expr list)
boehmes@36898
    63
boehmes@36898
    64
val func =
boehmes@36898
    65
  let fun cases st = (else_case >> single || args_case ::: cases) st
boehmes@36898
    66
  in in_braces cases end
boehmes@36898
    67
boehmes@39536
    68
val cex = space |--
boehmes@39536
    69
  Scan.repeat (name --| $$$ "->" -- (func || expr >> (single o pair [])))
boehmes@36898
    70
boehmes@40828
    71
fun resolve terms ((n, k), cases) =
boehmes@40828
    72
  (case Symtab.lookup terms n of
boehmes@40828
    73
    NONE => NONE
boehmes@40828
    74
  | SOME t => SOME ((t, k), cases))
boehmes@40828
    75
boehmes@40828
    76
fun annotate _ (_, []) = NONE
boehmes@40828
    77
  | annotate terms (n, [([], c)]) = resolve terms ((n, 0), (c, []))
boehmes@40828
    78
  | annotate _ (_, [_]) = NONE
boehmes@40828
    79
  | annotate terms (n, cases as (args, _) :: _) =
boehmes@40828
    80
      let val (cases', (_, else_case)) = split_last cases
boehmes@40828
    81
      in resolve terms ((n, length args), (else_case, cases')) end
boehmes@40828
    82
boehmes@40828
    83
fun read_cex terms ls =
wenzelm@40627
    84
  maps (cons "\n" o raw_explode) ls
boehmes@36898
    85
  |> try (fst o Scan.finite Symbol.stopper cex)
boehmes@36898
    86
  |> the_default []
boehmes@40828
    87
  |> map_filter (annotate terms)
boehmes@39536
    88
boehmes@39536
    89
boehmes@36898
    90
(* translation into terms *)
boehmes@36898
    91
boehmes@40828
    92
fun max_value vs =
boehmes@40828
    93
  let
boehmes@40828
    94
    fun max_val_expr (Value i) = Integer.max i
boehmes@40828
    95
      | max_val_expr (App (_, es)) = fold max_val_expr es
boehmes@40828
    96
      | max_val_expr (Array a) = max_val_array a
boehmes@40828
    97
      | max_val_expr _ = I
boehmes@36898
    98
boehmes@40828
    99
    and max_val_array (Fresh e) = max_val_expr e
boehmes@40828
   100
      | max_val_array (Store ((a, e1), e2)) =
boehmes@40828
   101
          max_val_array a #> max_val_expr e1 #> max_val_expr e2
boehmes@36898
   102
boehmes@40828
   103
    fun max_val (_, (ec, cs)) =
boehmes@40828
   104
      max_val_expr ec #> fold (fn (es, e) => fold max_val_expr (e :: es)) cs
boehmes@40828
   105
boehmes@40828
   106
  in fold max_val vs ~1 end
boehmes@40828
   107
boehmes@40828
   108
fun with_context terms f vs = fst (fold_map f vs (terms, max_value vs + 1))
boehmes@40828
   109
boehmes@40828
   110
fun get_term n T es (cx as (terms, next_val)) =
boehmes@40828
   111
  (case Symtab.lookup terms n of
boehmes@40828
   112
    SOME t => ((t, es), cx)
boehmes@36898
   113
  | NONE =>
boehmes@41058
   114
      let val t = Var (("skolem", next_val), T)
boehmes@40828
   115
      in ((t, []), (Symtab.update (n, t) terms, next_val + 1)) end)
boehmes@36898
   116
boehmes@40579
   117
fun trans_expr _ True = pair @{const True}
boehmes@40579
   118
  | trans_expr _ False = pair @{const False}
boehmes@36898
   119
  | trans_expr T (Number (i, NONE)) = pair (HOLogic.mk_number T i)
boehmes@36898
   120
  | trans_expr T (Number (i, SOME j)) =
boehmes@36898
   121
      pair (Const (@{const_name divide}, [T, T] ---> T) $
boehmes@36898
   122
        HOLogic.mk_number T i $ HOLogic.mk_number T j)
boehmes@40828
   123
  | trans_expr T (Value i) = pair (Var (("value", i), T))
boehmes@36898
   124
  | trans_expr T (Array a) = trans_array T a
boehmes@40828
   125
  | trans_expr T (App (n, es)) = get_term n T es #-> (fn (t, es') =>
blanchet@58058
   126
      let val Ts = fst (Old_SMT_Utils.dest_funT (length es') (Term.fastype_of t))
boehmes@39536
   127
      in
boehmes@40828
   128
        fold_map (uncurry trans_expr) (Ts ~~ es') #>> Term.list_comb o pair t
boehmes@40828
   129
      end)
boehmes@36898
   130
boehmes@36898
   131
and trans_array T a =
wenzelm@40840
   132
  let val (dT, rT) = Term.dest_funT T
boehmes@36898
   133
  in
boehmes@36898
   134
    (case a of
boehmes@36898
   135
      Fresh e => trans_expr rT e #>> (fn t => Abs ("x", dT, t))
boehmes@36898
   136
    | Store ((a', e1), e2) =>
boehmes@36898
   137
        trans_array T a' ##>> trans_expr dT e1 ##>> trans_expr rT e2 #>>
boehmes@36898
   138
        (fn ((m, k), v) =>
boehmes@36898
   139
          Const (@{const_name fun_upd}, [T, dT, rT] ---> T) $ m $ k $ v))
boehmes@36898
   140
  end
boehmes@36898
   141
boehmes@39536
   142
fun trans_pattern T ([], e) = trans_expr T e #>> pair []
boehmes@39536
   143
  | trans_pattern T (arg :: args, e) =
boehmes@39536
   144
      trans_expr (Term.domain_type T) arg ##>>
boehmes@39536
   145
      trans_pattern (Term.range_type T) (args, e) #>>
boehmes@39536
   146
      (fn (arg', (args', e')) => (arg' :: args', e'))
boehmes@36898
   147
boehmes@39536
   148
fun mk_fun_upd T U = Const (@{const_name fun_upd}, [T --> U, T, U, T] ---> U)
boehmes@39536
   149
boehmes@39536
   150
fun mk_update ([], u) _ = u
boehmes@39536
   151
  | mk_update ([t], u) f =
wenzelm@40840
   152
      uncurry mk_fun_upd (Term.dest_funT (Term.fastype_of f)) $ f $ t $ u
boehmes@39536
   153
  | mk_update (t :: ts, u) f =
boehmes@39536
   154
      let
wenzelm@40840
   155
        val (dT, rT) = Term.dest_funT (Term.fastype_of f)
wenzelm@40840
   156
        val (dT', rT') = Term.dest_funT rT
boehmes@39536
   157
      in
boehmes@39536
   158
        mk_fun_upd dT rT $ f $ t $
wenzelm@44241
   159
          mk_update (ts, u) (absdummy dT' (Const ("_", rT')))
boehmes@39536
   160
      end
boehmes@39536
   161
boehmes@39536
   162
fun mk_lambda Ts (t, pats) =
wenzelm@44241
   163
  fold_rev absdummy Ts t |> fold mk_update pats
boehmes@36898
   164
boehmes@40828
   165
fun translate ((t, k), (e, cs)) =
boehmes@40828
   166
  let
boehmes@40828
   167
    val T = Term.fastype_of t
blanchet@58058
   168
    val (Us, U) = Old_SMT_Utils.dest_funT k (Term.fastype_of t)
boehmes@40828
   169
boehmes@40828
   170
    fun mk_full_def u' pats =
boehmes@40828
   171
      pats
boehmes@40828
   172
      |> filter_out (fn (_, u) => u aconv u')
boehmes@40828
   173
      |> HOLogic.mk_eq o pair t o mk_lambda Us o pair u'
boehmes@40828
   174
boehmes@40828
   175
    fun mk_eq (us, u) = HOLogic.mk_eq (Term.list_comb (t, us), u)
boehmes@40828
   176
    fun mk_eqs u' [] = [HOLogic.mk_eq (t, u')]
boehmes@40828
   177
      | mk_eqs _ pats = map mk_eq pats
boehmes@40828
   178
  in
boehmes@40828
   179
    trans_expr U e ##>>
boehmes@40828
   180
    (if k = 0 then pair [] else fold_map (trans_pattern T) cs) #>>
boehmes@40828
   181
    (fn (u', pats) => (mk_eqs u' pats, mk_full_def u' pats))
boehmes@40828
   182
  end
boehmes@40828
   183
boehmes@40828
   184
boehmes@40828
   185
(* normalization *)
boehmes@40828
   186
boehmes@40828
   187
fun partition_eqs f =
boehmes@40828
   188
  let
boehmes@40828
   189
    fun part t (xs, ts) =
boehmes@40828
   190
      (case try HOLogic.dest_eq t of
boehmes@40828
   191
        SOME (l, r) => (case f l r of SOME x => (x::xs, ts) | _ => (xs, t::ts))
boehmes@40828
   192
      | NONE => (xs, t :: ts))
boehmes@40828
   193
  in (fn ts => fold part ts ([], [])) end
boehmes@40828
   194
boehmes@41122
   195
fun first_eq pred =
boehmes@41122
   196
  let
boehmes@41122
   197
    fun part _ [] = NONE
boehmes@41122
   198
      | part us (t :: ts) =
boehmes@41570
   199
          (case try (pred o HOLogic.dest_eq) t of
boehmes@41570
   200
            SOME (SOME lr) => SOME (lr, fold cons us ts)
boehmes@41570
   201
          | _ => part (t :: us) ts)
boehmes@41122
   202
  in (fn ts => part [] ts) end
boehmes@41122
   203
boehmes@40828
   204
fun replace_vars tab =
boehmes@40828
   205
  let
boehmes@41570
   206
    fun repl v = the_default v (AList.lookup (op aconv) tab v)
boehmes@41570
   207
    fun replace (v as Var _) = repl v
boehmes@41570
   208
      | replace (v as Free _) = repl v
boehmes@40828
   209
      | replace t = t
boehmes@40828
   210
  in map (Term.map_aterms replace) end
boehmes@40828
   211
boehmes@40828
   212
fun remove_int_nat_coercions (eqs, defs) =
boehmes@40828
   213
  let
boehmes@40828
   214
    fun mk_nat_num t i =
boehmes@40828
   215
      (case try HOLogic.dest_number i of
boehmes@40828
   216
        SOME (_, n) => SOME (t, HOLogic.mk_number @{typ nat} n)
boehmes@40828
   217
      | NONE => NONE)
boehmes@40828
   218
    fun nat_of (@{const of_nat (int)} $ (t as Var _)) i = mk_nat_num t i
boehmes@40828
   219
      | nat_of (@{const nat} $ i) (t as Var _) = mk_nat_num t i
boehmes@40828
   220
      | nat_of _ _ = NONE
boehmes@40828
   221
    val (nats, eqs') = partition_eqs nat_of eqs
boehmes@39536
   222
boehmes@40828
   223
    fun is_coercion t =
boehmes@40828
   224
      (case try HOLogic.dest_eq t of
boehmes@40828
   225
        SOME (@{const of_nat (int)}, _) => true
boehmes@40828
   226
      | SOME (@{const nat}, _) => true
boehmes@40828
   227
      | _ => false)
wenzelm@59058
   228
  in apply2 (replace_vars nats) (eqs', filter_out is_coercion defs) end
boehmes@40828
   229
boehmes@40828
   230
fun unfold_funapp (eqs, defs) =
boehmes@40828
   231
  let
blanchet@58057
   232
    fun unfold_app (Const (@{const_name fun_app}, _) $ f $ t) = f $ t
boehmes@40828
   233
      | unfold_app t = t
boehmes@40828
   234
    fun unfold_eq ((eq as Const (@{const_name HOL.eq}, _)) $ t $ u) =
boehmes@40828
   235
          eq $ unfold_app t $ u
boehmes@40828
   236
      | unfold_eq t = t
boehmes@40828
   237
boehmes@40828
   238
    fun is_fun_app t =
boehmes@40828
   239
      (case try HOLogic.dest_eq t of
blanchet@58057
   240
        SOME (Const (@{const_name fun_app}, _), _) => true
boehmes@40828
   241
      | _ => false)
boehmes@40828
   242
boehmes@40828
   243
  in (map unfold_eq eqs, filter_out is_fun_app defs) end
boehmes@40828
   244
boehmes@41570
   245
val unfold_eqs =
boehmes@40828
   246
  let
boehmes@41122
   247
    val is_ground = not o Term.exists_subterm Term.is_Var
boehmes@41570
   248
    fun is_non_rec (v, t) = not (Term.exists_subterm (equal v) t)
boehmes@41570
   249
boehmes@41570
   250
    fun rewr_var (l as Var _, r) = if is_ground r then SOME (l, r) else NONE
boehmes@41570
   251
      | rewr_var (r, l as Var _) = if is_ground r then SOME (l, r) else NONE
boehmes@41570
   252
      | rewr_var _ = NONE
boehmes@41570
   253
boehmes@41570
   254
    fun rewr_free' e = if is_non_rec e then SOME e else NONE
boehmes@41570
   255
    fun rewr_free (e as (Free _, _)) = rewr_free' e
boehmes@41570
   256
      | rewr_free (e as (_, Free _)) = rewr_free' (swap e)
boehmes@41570
   257
      | rewr_free _ = NONE
boehmes@40828
   258
boehmes@40828
   259
    fun is_trivial (Const (@{const_name HOL.eq}, _) $ t $ u) = t aconv u
boehmes@40828
   260
      | is_trivial _ = false
boehmes@41058
   261
boehmes@41122
   262
    fun replace r = replace_vars [r] #> filter_out is_trivial
boehmes@41058
   263
boehmes@41570
   264
    fun unfold_vars (es, ds) =
boehmes@41570
   265
      (case first_eq rewr_var es of
wenzelm@59058
   266
        SOME (lr, es') => unfold_vars (apply2 (replace lr) (es', ds))
boehmes@41122
   267
      | NONE => (es, ds))
boehmes@41058
   268
boehmes@41570
   269
    fun unfold_frees ues (es, ds) =
boehmes@41570
   270
      (case first_eq rewr_free es of
boehmes@41570
   271
        SOME (lr, es') =>
wenzelm@59058
   272
          apply2 (replace lr) (es', ds)
boehmes@41570
   273
          |> unfold_frees (HOLogic.mk_eq lr :: replace lr ues)
boehmes@41570
   274
      | NONE => (ues @ es, ds))
boehmes@41570
   275
boehmes@41570
   276
  in unfold_vars #> unfold_frees [] end
boehmes@40828
   277
boehmes@40828
   278
fun swap_free ((eq as Const (@{const_name HOL.eq}, _)) $ t $ (u as Free _)) =
boehmes@40828
   279
      eq $ u $ t
boehmes@40828
   280
  | swap_free t = t
boehmes@40828
   281
boehmes@40828
   282
fun frees_for_vars ctxt (eqs, defs) =
boehmes@40828
   283
  let
boehmes@40828
   284
    fun fresh_free i T (cx as (frees, ctxt)) =
boehmes@40828
   285
      (case Inttab.lookup frees i of
boehmes@40828
   286
        SOME t => (t, cx)
boehmes@40828
   287
      | NONE =>
boehmes@40828
   288
          let
boehmes@40828
   289
            val (n, ctxt') = yield_singleton Variable.variant_fixes "" ctxt
boehmes@40828
   290
            val t = Free (n, T)
boehmes@40828
   291
          in (t, (Inttab.update (i, t) frees, ctxt')) end)
boehmes@40828
   292
boehmes@40828
   293
    fun repl_var (Var ((_, i), T)) = fresh_free i T
boehmes@40828
   294
      | repl_var (t $ u) = repl_var t ##>> repl_var u #>> op $
boehmes@40828
   295
      | repl_var (Abs (n, T, t)) = repl_var t #>> (fn t' => Abs (n, T, t'))
boehmes@40828
   296
      | repl_var t = pair t
boehmes@40828
   297
  in
boehmes@40828
   298
    (Inttab.empty, ctxt)
boehmes@40828
   299
    |> fold_map repl_var eqs
boehmes@40828
   300
    ||>> fold_map repl_var defs
boehmes@40828
   301
    |> fst
boehmes@40828
   302
  end
boehmes@36898
   303
boehmes@36898
   304
boehmes@36898
   305
(* overall procedure *)
boehmes@36898
   306
boehmes@40828
   307
val is_free_constraint = Term.exists_subterm (fn Free _ => true | _ => false)
boehmes@40828
   308
boehmes@41129
   309
fun is_free_def (Const (@{const_name HOL.eq}, _) $ Free _ $ _) = true
boehmes@41129
   310
  | is_free_def _ = false
boehmes@41129
   311
boehmes@41129
   312
fun defined tp =
wenzelm@59058
   313
  try (apply2 (fst o HOLogic.dest_eq)) tp
boehmes@41129
   314
  |> the_default false o Option.map (op aconv)
boehmes@41129
   315
boehmes@41129
   316
fun add_free_defs free_cs defs =
boehmes@41129
   317
  let val (free_defs, defs') = List.partition is_free_def defs
boehmes@41129
   318
  in (free_cs @ filter_out (member defined free_cs) free_defs, defs') end
boehmes@41129
   319
boehmes@40828
   320
fun is_const_def (Const (@{const_name HOL.eq}, _) $ Const _ $ _) = true
boehmes@40828
   321
  | is_const_def _ = false
boehmes@40828
   322
blanchet@58058
   323
fun parse_counterex ctxt ({terms, ...} : Old_SMT_Translate.recon) ls =
boehmes@40828
   324
  read_cex terms ls
boehmes@40828
   325
  |> with_context terms translate
boehmes@40828
   326
  |> apfst flat o split_list
boehmes@40828
   327
  |> remove_int_nat_coercions
boehmes@40828
   328
  |> unfold_funapp
boehmes@41058
   329
  |> unfold_eqs
boehmes@40828
   330
  |>> map swap_free
boehmes@40828
   331
  |>> filter is_free_constraint
boehmes@41129
   332
  |-> add_free_defs
boehmes@40828
   333
  |> frees_for_vars ctxt
boehmes@40828
   334
  ||> filter is_const_def
boehmes@36898
   335
boehmes@36898
   336
end
boehmes@39536
   337