src/HOL/Tools/SMT/z3_model.ML
author haftmann
Thu, 08 Jul 2010 16:19:24 +0200
changeset 37744 3daaf23b9ab4
parent 37153 8feed34275ce
child 39536 c62359dd253d
permissions -rw-r--r--
tuned titles
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/z3_model.ML
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
     2
    Author:     Sascha Boehme and Philipp Meyer, 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
Parser for counterexamples generated by Z3.
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 Z3_MODEL =
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 parse_counterex: SMT_Translate.recon -> string list -> term list
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 Z3_Model: Z3_MODEL =
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
(* counterexample expressions *)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    16
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    17
datatype expr = True | False | Number of int * int option | Value of int |
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    18
  Array of array
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    19
and array = Fresh of expr | Store of (array * expr) * expr
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    20
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    21
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    22
(* parsing *)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    23
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    24
val space = Scan.many Symbol.is_ascii_blank
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    25
fun in_parens p = Scan.$$ "(" |-- p --| Scan.$$ ")"
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    26
fun in_braces p = (space -- Scan.$$ "{") |-- p --| (space -- Scan.$$ "}")
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 digit = (fn
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    29
  "0" => SOME 0 | "1" => SOME 1 | "2" => SOME 2 | "3" => SOME 3 |
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    30
  "4" => SOME 4 | "5" => SOME 5 | "6" => SOME 6 | "7" => SOME 7 |
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    31
  "8" => SOME 8 | "9" => SOME 9 | _ => NONE)
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 nat_num = Scan.repeat1 (Scan.some digit) >>
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    34
  (fn ds => fold (fn d => fn i => i * 10 + d) ds 0)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    35
val int_num = Scan.optional ($$ "-" >> K (fn i => ~i)) I :|--
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    36
  (fn sign => nat_num >> sign)
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 is_char = Symbol.is_ascii_letter orf Symbol.is_ascii_digit orf
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    39
  member (op =) (explode "_+*-/%~=<>$&|?!.@^#")
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    40
val name = Scan.many1 is_char >> implode
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    41
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    42
fun array_expr st = st |>
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    43
  in_parens (space |-- (
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    44
  Scan.this_string "const" |-- expr >> Fresh ||
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    45
  Scan.this_string "store" -- space |-- array_expr -- expr -- expr >> Store))
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    46
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    47
and expr st = st |> (space |-- (
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    48
  Scan.this_string "true" >> K True ||
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    49
  Scan.this_string "false" >> K False ||
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    50
  int_num -- Scan.option (Scan.$$ "/" |-- int_num) >> Number ||
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    51
  Scan.this_string "val!" |-- nat_num >> Value ||
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    52
  array_expr >> Array))
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 mapping = space -- Scan.this_string "->"
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    55
val value = mapping |-- expr
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    56
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    57
val args_case = Scan.repeat expr -- value
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    58
val else_case = space -- Scan.this_string "else" |-- value >>
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    59
  pair ([] : expr list)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    60
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    61
val func =
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    62
  let fun cases st = (else_case >> single || args_case ::: cases) st
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    63
  in in_braces cases end
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    64
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    65
val cex = space |-- Scan.repeat (space |-- name --| mapping --
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    66
  (func || expr >> (single o pair [])))
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    67
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    68
fun read_cex ls =
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    69
  explode (cat_lines ls)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    70
  |> try (fst o Scan.finite Symbol.stopper cex)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    71
  |> the_default []
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    72
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    73
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    74
(* translation into terms *)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    75
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    76
fun lookup_term tab (name, e) = Option.map (rpair e) (Symtab.lookup tab name)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    77
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    78
fun with_name_context tab f xs =
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    79
  let
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    80
    val ns = Symtab.fold (Term.add_free_names o snd) tab []
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    81
    val nctxt = Name.make_context ns
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    82
  in fst (fold_map f xs (Inttab.empty, nctxt)) end
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    83
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    84
fun fresh_term T (tab, nctxt) =
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    85
  let val (n, nctxt') = yield_singleton Name.variants "" nctxt
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    86
  in (Free (n, T), (tab, nctxt')) end
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    87
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    88
fun term_of_value T i (cx as (tab, _)) =
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    89
  (case Inttab.lookup tab i of
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    90
    SOME t => (t, cx)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    91
  | NONE =>
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    92
      let val (t, (tab', nctxt')) = fresh_term T cx
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    93
      in (t, (Inttab.update (i, t) tab', nctxt')) end)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    94
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    95
fun trans_expr _ True = pair @{term True}
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    96
  | trans_expr _ False = pair @{term False}
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    97
  | trans_expr T (Number (i, NONE)) = pair (HOLogic.mk_number T i)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    98
  | trans_expr T (Number (i, SOME j)) =
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    99
      pair (Const (@{const_name divide}, [T, T] ---> T) $
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   100
        HOLogic.mk_number T i $ HOLogic.mk_number T j)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   101
  | trans_expr T (Value i) = term_of_value T i
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   102
  | trans_expr T (Array a) = trans_array T a
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   103
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   104
and trans_array T a =
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   105
  let val dT = Term.domain_type T and rT = Term.range_type T
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   106
  in
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   107
    (case a of
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   108
      Fresh e => trans_expr rT e #>> (fn t => Abs ("x", dT, t))
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   109
    | Store ((a', e1), e2) =>
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   110
        trans_array T a' ##>> trans_expr dT e1 ##>> trans_expr rT e2 #>>
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   111
        (fn ((m, k), v) =>
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   112
          Const (@{const_name fun_upd}, [T, dT, rT] ---> T) $ m $ k $ v))
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   113
  end
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   114
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   115
fun trans_pat i T f x =
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   116
  f (Term.domain_type T) ##>> trans (i-1) (Term.range_type T) x #>>
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   117
  (fn (u, (us, t)) => (u :: us, t))
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   118
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   119
and trans i T ([], v) =
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   120
      if i > 0 then trans_pat i T fresh_term ([], v)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   121
      else trans_expr T v #>> pair []
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   122
  | trans i T (p :: ps, v) = trans_pat i T (fn U => trans_expr U p) (ps, v)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   123
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   124
fun mk_eq' t us u = HOLogic.mk_eq (Term.list_comb (t, us), u)
37153
8feed34275ce renamed constant "apply" to "fun_app" (which is closer to the related "fun_upd")
boehmes
parents: 36898
diff changeset
   125
fun mk_eq (Const (@{const_name fun_app}, _)) (u' :: us', u) = mk_eq' u' us' u
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   126
  | mk_eq t (us, u) = mk_eq' t us u
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   127
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   128
fun translate (t, cs) =
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   129
  let val T = Term.fastype_of t
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   130
  in
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   131
    (case (can HOLogic.dest_number t, cs) of
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   132
      (true, [c]) => trans 0 T c #>> (fn (_, u) => [mk_eq u ([], t)])
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   133
    | (_, (es, _) :: _) => fold_map (trans (length es) T) cs #>> map (mk_eq t)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   134
    | _ => raise TERM ("translate: no cases", [t]))
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   135
  end
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   136
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   137
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   138
(* overall procedure *)
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 parse_counterex ({terms, ...} : SMT_Translate.recon) ls =
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   141
  read_cex ls
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   142
  |> map_filter (lookup_term terms)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   143
  |> with_name_context terms translate
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   144
  |> flat
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   145
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   146
end