diff -r 6d1ecdb81ff0 -r 8e55aa1306c5 src/HOL/Tools/SMT/z3_model.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/SMT/z3_model.ML	Wed May 12 23:54:02 2010 +0200
@@ -0,0 +1,146 @@
+(*  Title:      HOL/Tools/SMT/z3_model.ML
+    Author:     Sascha Boehme and Philipp Meyer, TU Muenchen
+
+Parser for counterexamples generated by Z3.
+*)
+
+signature Z3_MODEL =
+sig
+  val parse_counterex: SMT_Translate.recon -> string list -> term list
+end
+
+structure Z3_Model: Z3_MODEL =
+struct
+
+(* counterexample expressions *)
+
+datatype expr = True | False | Number of int * int option | Value of int |
+  Array of array
+and array = Fresh of expr | Store of (array * expr) * expr
+
+
+(* parsing *)
+
+val space = Scan.many Symbol.is_ascii_blank
+fun in_parens p = Scan.$$ "(" |-- p --| Scan.$$ ")"
+fun in_braces p = (space -- Scan.$$ "{") |-- p --| (space -- Scan.$$ "}")
+
+val digit = (fn
+  "0" => SOME 0 | "1" => SOME 1 | "2" => SOME 2 | "3" => SOME 3 |
+  "4" => SOME 4 | "5" => SOME 5 | "6" => SOME 6 | "7" => SOME 7 |
+  "8" => SOME 8 | "9" => SOME 9 | _ => NONE)
+
+val nat_num = Scan.repeat1 (Scan.some digit) >>
+  (fn ds => fold (fn d => fn i => i * 10 + d) ds 0)
+val int_num = Scan.optional ($$ "-" >> K (fn i => ~i)) I :|--
+  (fn sign => nat_num >> sign)
+
+val is_char = Symbol.is_ascii_letter orf Symbol.is_ascii_digit orf
+  member (op =) (explode "_+*-/%~=<>$&|?!.@^#")
+val name = Scan.many1 is_char >> implode
+
+fun array_expr st = st |>
+  in_parens (space |-- (
+  Scan.this_string "const" |-- expr >> Fresh ||
+  Scan.this_string "store" -- space |-- array_expr -- expr -- expr >> Store))
+
+and expr st = st |> (space |-- (
+  Scan.this_string "true" >> K True ||
+  Scan.this_string "false" >> K False ||
+  int_num -- Scan.option (Scan.$$ "/" |-- int_num) >> Number ||
+  Scan.this_string "val!" |-- nat_num >> Value ||
+  array_expr >> Array))
+
+val mapping = space -- Scan.this_string "->"
+val value = mapping |-- expr
+
+val args_case = Scan.repeat expr -- value
+val else_case = space -- Scan.this_string "else" |-- value >>
+  pair ([] : expr list)
+
+val func =
+  let fun cases st = (else_case >> single || args_case ::: cases) st
+  in in_braces cases end
+
+val cex = space |-- Scan.repeat (space |-- name --| mapping --
+  (func || expr >> (single o pair [])))
+
+fun read_cex ls =
+  explode (cat_lines ls)
+  |> try (fst o Scan.finite Symbol.stopper cex)
+  |> the_default []
+
+
+(* translation into terms *)
+
+fun lookup_term tab (name, e) = Option.map (rpair e) (Symtab.lookup tab name)
+
+fun with_name_context tab f xs =
+  let
+    val ns = Symtab.fold (Term.add_free_names o snd) tab []
+    val nctxt = Name.make_context ns
+  in fst (fold_map f xs (Inttab.empty, nctxt)) end
+
+fun fresh_term T (tab, nctxt) =
+  let val (n, nctxt') = yield_singleton Name.variants "" nctxt
+  in (Free (n, T), (tab, nctxt')) end
+
+fun term_of_value T i (cx as (tab, _)) =
+  (case Inttab.lookup tab i of
+    SOME t => (t, cx)
+  | NONE =>
+      let val (t, (tab', nctxt')) = fresh_term T cx
+      in (t, (Inttab.update (i, t) tab', nctxt')) end)
+
+fun trans_expr _ True = pair @{term True}
+  | trans_expr _ False = pair @{term False}
+  | trans_expr T (Number (i, NONE)) = pair (HOLogic.mk_number T i)
+  | trans_expr T (Number (i, SOME j)) =
+      pair (Const (@{const_name divide}, [T, T] ---> T) $
+        HOLogic.mk_number T i $ HOLogic.mk_number T j)
+  | trans_expr T (Value i) = term_of_value T i
+  | trans_expr T (Array a) = trans_array T a
+
+and trans_array T a =
+  let val dT = Term.domain_type T and rT = Term.range_type T
+  in
+    (case a of
+      Fresh e => trans_expr rT e #>> (fn t => Abs ("x", dT, t))
+    | Store ((a', e1), e2) =>
+        trans_array T a' ##>> trans_expr dT e1 ##>> trans_expr rT e2 #>>
+        (fn ((m, k), v) =>
+          Const (@{const_name fun_upd}, [T, dT, rT] ---> T) $ m $ k $ v))
+  end
+
+fun trans_pat i T f x =
+  f (Term.domain_type T) ##>> trans (i-1) (Term.range_type T) x #>>
+  (fn (u, (us, t)) => (u :: us, t))
+
+and trans i T ([], v) =
+      if i > 0 then trans_pat i T fresh_term ([], v)
+      else trans_expr T v #>> pair []
+  | trans i T (p :: ps, v) = trans_pat i T (fn U => trans_expr U p) (ps, v)
+
+fun mk_eq' t us u = HOLogic.mk_eq (Term.list_comb (t, us), u)
+fun mk_eq (Const (@{const_name apply}, _)) (u' :: us', u) = mk_eq' u' us' u
+  | mk_eq t (us, u) = mk_eq' t us u
+
+fun translate (t, cs) =
+  let val T = Term.fastype_of t
+  in
+    (case (can HOLogic.dest_number t, cs) of
+      (true, [c]) => trans 0 T c #>> (fn (_, u) => [mk_eq u ([], t)])
+    | (_, (es, _) :: _) => fold_map (trans (length es) T) cs #>> map (mk_eq t)
+    | _ => raise TERM ("translate: no cases", [t]))
+  end
+
+
+(* overall procedure *)
+
+fun parse_counterex ({terms, ...} : SMT_Translate.recon) ls =
+  read_cex ls
+  |> map_filter (lookup_term terms)
+  |> with_name_context terms translate
+  |> flat
+
+end