1.1 --- a/src/HOL/SMT/Tools/z3_model.ML Wed May 12 23:54:01 2010 +0200
1.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
1.3 @@ -1,146 +0,0 @@
1.4 -(* Title: HOL/SMT/Tools/z3_model.ML
1.5 - Author: Sascha Boehme and Philipp Meyer, TU Muenchen
1.6 -
1.7 -Parser for counterexamples generated by Z3.
1.8 -*)
1.9 -
1.10 -signature Z3_MODEL =
1.11 -sig
1.12 - val parse_counterex: SMT_Translate.recon -> string list -> term list
1.13 -end
1.14 -
1.15 -structure Z3_Model: Z3_MODEL =
1.16 -struct
1.17 -
1.18 -(* counterexample expressions *)
1.19 -
1.20 -datatype expr = True | False | Number of int * int option | Value of int |
1.21 - Array of array
1.22 -and array = Fresh of expr | Store of (array * expr) * expr
1.23 -
1.24 -
1.25 -(* parsing *)
1.26 -
1.27 -val space = Scan.many Symbol.is_ascii_blank
1.28 -fun in_parens p = Scan.$$ "(" |-- p --| Scan.$$ ")"
1.29 -fun in_braces p = (space -- Scan.$$ "{") |-- p --| (space -- Scan.$$ "}")
1.30 -
1.31 -val digit = (fn
1.32 - "0" => SOME 0 | "1" => SOME 1 | "2" => SOME 2 | "3" => SOME 3 |
1.33 - "4" => SOME 4 | "5" => SOME 5 | "6" => SOME 6 | "7" => SOME 7 |
1.34 - "8" => SOME 8 | "9" => SOME 9 | _ => NONE)
1.35 -
1.36 -val nat_num = Scan.repeat1 (Scan.some digit) >>
1.37 - (fn ds => fold (fn d => fn i => i * 10 + d) ds 0)
1.38 -val int_num = Scan.optional ($$ "-" >> K (fn i => ~i)) I :|--
1.39 - (fn sign => nat_num >> sign)
1.40 -
1.41 -val is_char = Symbol.is_ascii_letter orf Symbol.is_ascii_digit orf
1.42 - member (op =) (explode "_+*-/%~=<>$&|?!.@^#")
1.43 -val name = Scan.many1 is_char >> implode
1.44 -
1.45 -fun array_expr st = st |>
1.46 - in_parens (space |-- (
1.47 - Scan.this_string "const" |-- expr >> Fresh ||
1.48 - Scan.this_string "store" -- space |-- array_expr -- expr -- expr >> Store))
1.49 -
1.50 -and expr st = st |> (space |-- (
1.51 - Scan.this_string "true" >> K True ||
1.52 - Scan.this_string "false" >> K False ||
1.53 - int_num -- Scan.option (Scan.$$ "/" |-- int_num) >> Number ||
1.54 - Scan.this_string "val!" |-- nat_num >> Value ||
1.55 - array_expr >> Array))
1.56 -
1.57 -val mapping = space -- Scan.this_string "->"
1.58 -val value = mapping |-- expr
1.59 -
1.60 -val args_case = Scan.repeat expr -- value
1.61 -val else_case = space -- Scan.this_string "else" |-- value >>
1.62 - pair ([] : expr list)
1.63 -
1.64 -val func =
1.65 - let fun cases st = (else_case >> single || args_case ::: cases) st
1.66 - in in_braces cases end
1.67 -
1.68 -val cex = space |-- Scan.repeat (space |-- name --| mapping --
1.69 - (func || expr >> (single o pair [])))
1.70 -
1.71 -fun read_cex ls =
1.72 - explode (cat_lines ls)
1.73 - |> try (fst o Scan.finite Symbol.stopper cex)
1.74 - |> the_default []
1.75 -
1.76 -
1.77 -(* translation into terms *)
1.78 -
1.79 -fun lookup_term tab (name, e) = Option.map (rpair e) (Symtab.lookup tab name)
1.80 -
1.81 -fun with_name_context tab f xs =
1.82 - let
1.83 - val ns = Symtab.fold (Term.add_free_names o snd) tab []
1.84 - val nctxt = Name.make_context ns
1.85 - in fst (fold_map f xs (Inttab.empty, nctxt)) end
1.86 -
1.87 -fun fresh_term T (tab, nctxt) =
1.88 - let val (n, nctxt') = yield_singleton Name.variants "" nctxt
1.89 - in (Free (n, T), (tab, nctxt')) end
1.90 -
1.91 -fun term_of_value T i (cx as (tab, _)) =
1.92 - (case Inttab.lookup tab i of
1.93 - SOME t => (t, cx)
1.94 - | NONE =>
1.95 - let val (t, (tab', nctxt')) = fresh_term T cx
1.96 - in (t, (Inttab.update (i, t) tab', nctxt')) end)
1.97 -
1.98 -fun trans_expr _ True = pair @{term True}
1.99 - | trans_expr _ False = pair @{term False}
1.100 - | trans_expr T (Number (i, NONE)) = pair (HOLogic.mk_number T i)
1.101 - | trans_expr T (Number (i, SOME j)) =
1.102 - pair (Const (@{const_name divide}, [T, T] ---> T) $
1.103 - HOLogic.mk_number T i $ HOLogic.mk_number T j)
1.104 - | trans_expr T (Value i) = term_of_value T i
1.105 - | trans_expr T (Array a) = trans_array T a
1.106 -
1.107 -and trans_array T a =
1.108 - let val dT = Term.domain_type T and rT = Term.range_type T
1.109 - in
1.110 - (case a of
1.111 - Fresh e => trans_expr rT e #>> (fn t => Abs ("x", dT, t))
1.112 - | Store ((a', e1), e2) =>
1.113 - trans_array T a' ##>> trans_expr dT e1 ##>> trans_expr rT e2 #>>
1.114 - (fn ((m, k), v) =>
1.115 - Const (@{const_name fun_upd}, [T, dT, rT] ---> T) $ m $ k $ v))
1.116 - end
1.117 -
1.118 -fun trans_pat i T f x =
1.119 - f (Term.domain_type T) ##>> trans (i-1) (Term.range_type T) x #>>
1.120 - (fn (u, (us, t)) => (u :: us, t))
1.121 -
1.122 -and trans i T ([], v) =
1.123 - if i > 0 then trans_pat i T fresh_term ([], v)
1.124 - else trans_expr T v #>> pair []
1.125 - | trans i T (p :: ps, v) = trans_pat i T (fn U => trans_expr U p) (ps, v)
1.126 -
1.127 -fun mk_eq' t us u = HOLogic.mk_eq (Term.list_comb (t, us), u)
1.128 -fun mk_eq (Const (@{const_name apply}, _)) (u' :: us', u) = mk_eq' u' us' u
1.129 - | mk_eq t (us, u) = mk_eq' t us u
1.130 -
1.131 -fun translate (t, cs) =
1.132 - let val T = Term.fastype_of t
1.133 - in
1.134 - (case (can HOLogic.dest_number t, cs) of
1.135 - (true, [c]) => trans 0 T c #>> (fn (_, u) => [mk_eq u ([], t)])
1.136 - | (_, (es, _) :: _) => fold_map (trans (length es) T) cs #>> map (mk_eq t)
1.137 - | _ => raise TERM ("translate: no cases", [t]))
1.138 - end
1.139 -
1.140 -
1.141 -(* overall procedure *)
1.142 -
1.143 -fun parse_counterex ({terms, ...} : SMT_Translate.recon) ls =
1.144 - read_cex ls
1.145 - |> map_filter (lookup_term terms)
1.146 - |> with_name_context terms translate
1.147 - |> flat
1.148 -
1.149 -end