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