src/HOL/Tools/SMT/z3_model.ML
author wenzelm
Sat Nov 20 00:53:26 2010 +0100 (2010-11-20)
changeset 40627 becf5d5187cc
parent 40579 98ebd2300823
child 40663 e080c9e68752
permissions -rw-r--r--
renamed raw "explode" function to "raw_explode" to emphasize its meaning;
boehmes@36898
     1
(*  Title:      HOL/Tools/SMT/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
boehmes@36898
     7
signature Z3_MODEL =
boehmes@36898
     8
sig
boehmes@39536
     9
  val parse_counterex: Proof.context -> SMT_Translate.recon -> string list ->
boehmes@39536
    10
    term list
boehmes@36898
    11
end
boehmes@36898
    12
boehmes@36898
    13
structure Z3_Model: Z3_MODEL =
boehmes@36898
    14
struct
boehmes@36898
    15
boehmes@36898
    16
(* counterexample expressions *)
boehmes@36898
    17
boehmes@36898
    18
datatype expr = True | False | Number of int * int option | Value of int |
boehmes@39536
    19
  Array of array | App of string * expr list
boehmes@36898
    20
and array = Fresh of expr | Store of (array * expr) * expr
boehmes@36898
    21
boehmes@36898
    22
boehmes@36898
    23
(* parsing *)
boehmes@36898
    24
boehmes@36898
    25
val space = Scan.many Symbol.is_ascii_blank
boehmes@39536
    26
fun spaced p = p --| space
boehmes@39536
    27
fun in_parens p = spaced (Scan.$$ "(") |-- p --| spaced (Scan.$$ ")")
boehmes@39536
    28
fun in_braces p = spaced (Scan.$$ "{") |-- p --| spaced (Scan.$$ "}")
boehmes@36898
    29
boehmes@36898
    30
val digit = (fn
boehmes@36898
    31
  "0" => SOME 0 | "1" => SOME 1 | "2" => SOME 2 | "3" => SOME 3 |
boehmes@36898
    32
  "4" => SOME 4 | "5" => SOME 5 | "6" => SOME 6 | "7" => SOME 7 |
boehmes@36898
    33
  "8" => SOME 8 | "9" => SOME 9 | _ => NONE)
boehmes@36898
    34
boehmes@39536
    35
val nat_num = spaced (Scan.repeat1 (Scan.some digit) >>
boehmes@39536
    36
  (fn ds => fold (fn d => fn i => i * 10 + d) ds 0))
boehmes@39536
    37
val int_num = spaced (Scan.optional ($$ "-" >> K (fn i => ~i)) I :|--
boehmes@39536
    38
  (fn sign => nat_num >> sign))
boehmes@36898
    39
boehmes@36898
    40
val is_char = Symbol.is_ascii_letter orf Symbol.is_ascii_digit orf
wenzelm@40627
    41
  member (op =) (raw_explode "_+*-/%~=<>$&|?!.@^#")
boehmes@39536
    42
val name = spaced (Scan.many1 is_char >> implode)
boehmes@39536
    43
boehmes@39536
    44
fun $$$ s = spaced (Scan.this_string s)
boehmes@36898
    45
boehmes@39536
    46
fun array_expr st = st |> in_parens (
boehmes@39536
    47
  $$$ "const" |-- expr >> Fresh ||
boehmes@39536
    48
  $$$ "store" |-- array_expr -- expr -- expr >> Store)
boehmes@36898
    49
boehmes@39536
    50
and expr st = st |> (
boehmes@39536
    51
  $$$ "true" >> K True ||
boehmes@39536
    52
  $$$ "false" >> K False ||
boehmes@39536
    53
  int_num -- Scan.option ($$$ "/" |-- int_num) >> Number ||
boehmes@39536
    54
  $$$ "val!" |-- nat_num >> Value ||
boehmes@39536
    55
  name >> (App o rpair []) ||
boehmes@39536
    56
  array_expr >> Array ||
boehmes@39536
    57
  in_parens (name -- Scan.repeat1 expr) >> App)
boehmes@36898
    58
boehmes@39536
    59
fun args st = ($$$ "->" >> K [] || expr ::: args) st
boehmes@39536
    60
val args_case = args -- expr
boehmes@39536
    61
val else_case = $$$ "else" -- $$$ "->" |-- expr >> pair ([] : expr list)
boehmes@36898
    62
boehmes@36898
    63
val func =
boehmes@36898
    64
  let fun cases st = (else_case >> single || args_case ::: cases) st
boehmes@36898
    65
  in in_braces cases end
boehmes@36898
    66
boehmes@39536
    67
val cex = space |--
boehmes@39536
    68
  Scan.repeat (name --| $$$ "->" -- (func || expr >> (single o pair [])))
boehmes@36898
    69
boehmes@36898
    70
fun read_cex ls =
wenzelm@40627
    71
  maps (cons "\n" o raw_explode) ls
boehmes@36898
    72
  |> try (fst o Scan.finite Symbol.stopper cex)
boehmes@36898
    73
  |> the_default []
boehmes@36898
    74
boehmes@36898
    75
boehmes@39536
    76
(* normalization *)
boehmes@39536
    77
boehmes@39536
    78
local
boehmes@39536
    79
  fun matches terms f n =
boehmes@39536
    80
    (case Symtab.lookup terms n of
boehmes@39536
    81
      NONE => false
boehmes@39536
    82
    | SOME t => f t)
boehmes@39536
    83
boehmes@39536
    84
  fun subst f (n, cases) = (n, map (fn (args, v) => (map f args, f v)) cases)
boehmes@39536
    85
in
boehmes@39536
    86
boehmes@39536
    87
fun reduce_function (n, [c]) = SOME ((n, 0), [c])
boehmes@39536
    88
  | reduce_function (n, cases) =
boehmes@39536
    89
      let val (patterns, else_case as (_, e)) = split_last cases
boehmes@39536
    90
      in
boehmes@39536
    91
        (case patterns of
boehmes@39536
    92
          [] => NONE
boehmes@39536
    93
        | (args, _) :: _ => SOME ((n, length args),
boehmes@39536
    94
            filter_out (equal e o snd) patterns @ [else_case]))
boehmes@39536
    95
      end
boehmes@39536
    96
boehmes@39536
    97
fun drop_skolem_constants terms = filter (Symtab.defined terms o fst o fst)
boehmes@39536
    98
boehmes@39536
    99
fun substitute_constants terms =
boehmes@39536
   100
  let
boehmes@39536
   101
    fun check vs1 [] = rev vs1
boehmes@39536
   102
      | check vs1 ((v as ((n, k), [([], Value i)])) :: vs2) =
boehmes@39536
   103
          if matches terms (fn Free _ => true | _ => false) n orelse k > 0
boehmes@39536
   104
          then check (v :: vs1) vs2
boehmes@39536
   105
          else
boehmes@39536
   106
            let
boehmes@39536
   107
              fun sub (e as Value j) = if i = j then App (n, []) else e
boehmes@39536
   108
                | sub e = e
boehmes@39536
   109
            in check (map (subst sub) vs1) (map (subst sub) vs2) end
boehmes@39536
   110
      | check vs1 (v :: vs2) = check (v :: vs1) vs2
boehmes@39536
   111
  in check [] end
boehmes@39536
   112
boehmes@39536
   113
fun remove_int_nat_coercions terms vs =
boehmes@39536
   114
  let
boehmes@39536
   115
    fun match ts ((n, _), _) = matches terms (member (op aconv) ts) n
boehmes@39536
   116
boehmes@40551
   117
    val (default_int, ints) =
boehmes@40579
   118
      (case find_first (match [@{const of_nat (int)}]) vs of
boehmes@40551
   119
        NONE => (NONE, [])
boehmes@40551
   120
      | SOME (_, cases) =>
boehmes@40551
   121
          let val (cs, (_, e)) = split_last cases
boehmes@40551
   122
          in (SOME e, map (apfst hd) cs) end)
boehmes@40551
   123
boehmes@40551
   124
    fun nat_of @{typ nat} (v as Value _) =
boehmes@40551
   125
          AList.lookup (op =) ints v |> the_default (the_default v default_int)
boehmes@40551
   126
      | nat_of _ e = e
boehmes@40551
   127
boehmes@40551
   128
    fun subst_nat T k ([], e) =
boehmes@40551
   129
          let fun app f i = if i <= 0 then I else app f (i-1) o f
boehmes@40551
   130
          in ([], nat_of (app Term.range_type k T) e) end
boehmes@40551
   131
      | subst_nat T k (arg :: args, e) =
boehmes@40551
   132
          subst_nat (Term.range_type T) (k-1) (args, e)
boehmes@40551
   133
          |> apfst (cons (nat_of (Term.domain_type T) arg))
boehmes@40551
   134
boehmes@40551
   135
    fun subst_nats (v as ((n, k), cases)) =
boehmes@40551
   136
      (case Symtab.lookup terms n of
boehmes@40551
   137
        NONE => v
boehmes@40551
   138
      | SOME t => ((n, k), map (subst_nat (Term.fastype_of t) k) cases))
boehmes@39536
   139
  in
boehmes@40551
   140
    map subst_nats vs
boehmes@40579
   141
    |> filter_out (match [@{const of_nat (int)}, @{const nat}])
boehmes@39536
   142
  end
boehmes@39536
   143
boehmes@39536
   144
fun filter_valid_valuations terms = map_filter (fn
boehmes@39536
   145
    (_, []) => NONE
boehmes@39536
   146
  | ((n, i), cases) =>
boehmes@39536
   147
      let
boehmes@39536
   148
        fun valid_expr (Array a) = valid_array a
boehmes@39536
   149
          | valid_expr (App (n, es)) =
boehmes@39536
   150
              Symtab.defined terms n andalso forall valid_expr es
boehmes@39536
   151
          | valid_expr _ = true
boehmes@39536
   152
        and valid_array (Fresh e) = valid_expr e
boehmes@39536
   153
          | valid_array (Store ((a, e1), e2)) =
boehmes@39536
   154
              valid_array a andalso valid_expr e1 andalso valid_expr e2
boehmes@39536
   155
        fun valid_case (es, e) = forall valid_expr (e :: es)
boehmes@39536
   156
      in
boehmes@39536
   157
        if not (forall valid_case cases) then NONE
boehmes@39536
   158
        else Option.map (rpair cases o rpair i) (Symtab.lookup terms n)
boehmes@39536
   159
      end)
boehmes@39536
   160
boehmes@39536
   161
end
boehmes@39536
   162
boehmes@39536
   163
boehmes@36898
   164
(* translation into terms *)
boehmes@36898
   165
boehmes@39536
   166
fun with_context ctxt terms f vs =
boehmes@39536
   167
  fst (fold_map f vs (ctxt, terms, Inttab.empty))
boehmes@36898
   168
boehmes@39536
   169
fun fresh_term T (ctxt, terms, values) =
boehmes@39536
   170
  let val (n, ctxt') = yield_singleton Variable.variant_fixes "" ctxt
boehmes@39536
   171
  in (Free (n, T), (ctxt', terms, values)) end
boehmes@36898
   172
boehmes@39536
   173
fun term_of_value T i (cx as (_, _, values)) =
boehmes@39536
   174
  (case Inttab.lookup values i of
boehmes@36898
   175
    SOME t => (t, cx)
boehmes@36898
   176
  | NONE =>
boehmes@39536
   177
      let val (t, (ctxt', terms', values')) = fresh_term T cx
boehmes@39536
   178
      in (t, (ctxt', terms', Inttab.update (i, t) values')) end)
boehmes@39536
   179
boehmes@39536
   180
fun get_term n (cx as (_, terms, _)) = (the (Symtab.lookup terms n), cx)
boehmes@36898
   181
boehmes@40579
   182
fun trans_expr _ True = pair @{const True}
boehmes@40579
   183
  | trans_expr _ False = pair @{const False}
boehmes@36898
   184
  | trans_expr T (Number (i, NONE)) = pair (HOLogic.mk_number T i)
boehmes@36898
   185
  | trans_expr T (Number (i, SOME j)) =
boehmes@36898
   186
      pair (Const (@{const_name divide}, [T, T] ---> T) $
boehmes@36898
   187
        HOLogic.mk_number T i $ HOLogic.mk_number T j)
boehmes@36898
   188
  | trans_expr T (Value i) = term_of_value T i
boehmes@36898
   189
  | trans_expr T (Array a) = trans_array T a
boehmes@39536
   190
  | trans_expr _ (App (n, es)) =
boehmes@39536
   191
      let val get_Ts = take (length es) o Term.binder_types o Term.fastype_of
boehmes@39536
   192
      in
boehmes@39536
   193
        get_term n #-> (fn t =>
boehmes@39536
   194
        fold_map (uncurry trans_expr) (get_Ts t ~~ es) #>>
boehmes@39536
   195
        Term.list_comb o pair t)
boehmes@39536
   196
      end
boehmes@36898
   197
boehmes@36898
   198
and trans_array T a =
boehmes@36898
   199
  let val dT = Term.domain_type T and rT = Term.range_type T
boehmes@36898
   200
  in
boehmes@36898
   201
    (case a of
boehmes@36898
   202
      Fresh e => trans_expr rT e #>> (fn t => Abs ("x", dT, t))
boehmes@36898
   203
    | Store ((a', e1), e2) =>
boehmes@36898
   204
        trans_array T a' ##>> trans_expr dT e1 ##>> trans_expr rT e2 #>>
boehmes@36898
   205
        (fn ((m, k), v) =>
boehmes@36898
   206
          Const (@{const_name fun_upd}, [T, dT, rT] ---> T) $ m $ k $ v))
boehmes@36898
   207
  end
boehmes@36898
   208
boehmes@39536
   209
fun trans_pattern T ([], e) = trans_expr T e #>> pair []
boehmes@39536
   210
  | trans_pattern T (arg :: args, e) =
boehmes@39536
   211
      trans_expr (Term.domain_type T) arg ##>>
boehmes@39536
   212
      trans_pattern (Term.range_type T) (args, e) #>>
boehmes@39536
   213
      (fn (arg', (args', e')) => (arg' :: args', e'))
boehmes@36898
   214
boehmes@39536
   215
fun mk_fun_upd T U = Const (@{const_name fun_upd}, [T --> U, T, U, T] ---> U)
boehmes@39536
   216
boehmes@39536
   217
fun split_type T = (Term.domain_type T, Term.range_type T)
boehmes@36898
   218
boehmes@39536
   219
fun mk_update ([], u) _ = u
boehmes@39536
   220
  | mk_update ([t], u) f =
boehmes@39536
   221
      uncurry mk_fun_upd (split_type (Term.fastype_of f)) $ f $ t $ u
boehmes@39536
   222
  | mk_update (t :: ts, u) f =
boehmes@39536
   223
      let
boehmes@39536
   224
        val (dT, rT) = split_type (Term.fastype_of f)
boehmes@39536
   225
        val (dT', rT') = split_type rT
boehmes@39536
   226
      in
boehmes@39536
   227
        mk_fun_upd dT rT $ f $ t $
boehmes@39536
   228
          mk_update (ts, u) (Term.absdummy (dT', Const ("_", rT')))
boehmes@39536
   229
      end
boehmes@39536
   230
boehmes@39536
   231
fun mk_lambda Ts (t, pats) =
boehmes@39536
   232
  fold_rev (curry Term.absdummy) Ts t |> fold mk_update pats
boehmes@36898
   233
boehmes@39536
   234
fun translate' T i [([], e)] =
boehmes@39536
   235
      if i = 0 then trans_expr T e
boehmes@39536
   236
      else 
boehmes@39536
   237
        let val ((Us1, Us2), U) = Term.strip_type T |>> chop i
boehmes@39536
   238
        in trans_expr (Us2 ---> U) e #>> mk_lambda Us1 o rpair [] end
boehmes@39536
   239
  | translate' T i cases =
boehmes@39536
   240
      let
boehmes@39536
   241
        val (pat_cases, def) = split_last cases |> apsnd snd
boehmes@39536
   242
        val ((Us1, Us2), U) = Term.strip_type T |>> chop i
boehmes@39536
   243
      in
boehmes@39536
   244
        trans_expr (Us2 ---> U) def ##>>
boehmes@39536
   245
        fold_map (trans_pattern T) pat_cases #>>
boehmes@39536
   246
        mk_lambda Us1
boehmes@39536
   247
      end
boehmes@39536
   248
boehmes@39536
   249
fun translate ((t, i), cases) =
boehmes@39536
   250
  translate' (Term.fastype_of t) i cases #>> HOLogic.mk_eq o pair t
boehmes@36898
   251
boehmes@36898
   252
boehmes@36898
   253
(* overall procedure *)
boehmes@36898
   254
boehmes@39536
   255
fun parse_counterex ctxt ({terms, ...} : SMT_Translate.recon) ls =
boehmes@36898
   256
  read_cex ls
boehmes@39536
   257
  |> map_filter reduce_function
boehmes@39536
   258
  |> drop_skolem_constants terms
boehmes@39536
   259
  |> substitute_constants terms
boehmes@39536
   260
  |> remove_int_nat_coercions terms
boehmes@39536
   261
  |> filter_valid_valuations terms
boehmes@39536
   262
  |> with_context ctxt terms translate
boehmes@36898
   263
boehmes@36898
   264
end
boehmes@39536
   265