author | boehmes |
Tue, 30 Nov 2010 18:22:43 +0100 | |
changeset 40828 | 47ff261431c4 |
parent 40663 | e080c9e68752 |
child 40840 | 2f97215e79bf |
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 |
|
39536
c62359dd253d
properly parse Z3 error models, including datatypes, and represent function valuations as lambda terms; also normalize Z3 error models
boehmes
parents:
37153
diff
changeset
|
9 |
val parse_counterex: Proof.context -> SMT_Translate.recon -> string list -> |
40828
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset
|
10 |
term list * term list |
36898 | 11 |
end |
12 |
||
13 |
structure Z3_Model: Z3_MODEL = |
|
14 |
struct |
|
15 |
||
40663 | 16 |
structure U = SMT_Utils |
17 |
||
18 |
||
36898 | 19 |
(* counterexample expressions *) |
20 |
||
21 |
datatype expr = True | False | Number of int * int option | Value of int | |
|
39536
c62359dd253d
properly parse Z3 error models, including datatypes, and represent function valuations as lambda terms; also normalize Z3 error models
boehmes
parents:
37153
diff
changeset
|
22 |
Array of array | App of string * expr list |
36898 | 23 |
and array = Fresh of expr | Store of (array * expr) * expr |
24 |
||
25 |
||
26 |
(* parsing *) |
|
27 |
||
28 |
val space = Scan.many Symbol.is_ascii_blank |
|
39536
c62359dd253d
properly parse Z3 error models, including datatypes, and represent function valuations as lambda terms; also normalize Z3 error models
boehmes
parents:
37153
diff
changeset
|
29 |
fun spaced p = p --| space |
c62359dd253d
properly parse Z3 error models, including datatypes, and represent function valuations as lambda terms; also normalize Z3 error models
boehmes
parents:
37153
diff
changeset
|
30 |
fun in_parens p = spaced (Scan.$$ "(") |-- p --| spaced (Scan.$$ ")") |
c62359dd253d
properly parse Z3 error models, including datatypes, and represent function valuations as lambda terms; also normalize Z3 error models
boehmes
parents:
37153
diff
changeset
|
31 |
fun in_braces p = spaced (Scan.$$ "{") |-- p --| spaced (Scan.$$ "}") |
36898 | 32 |
|
33 |
val digit = (fn |
|
34 |
"0" => SOME 0 | "1" => SOME 1 | "2" => SOME 2 | "3" => SOME 3 | |
|
35 |
"4" => SOME 4 | "5" => SOME 5 | "6" => SOME 6 | "7" => SOME 7 | |
|
36 |
"8" => SOME 8 | "9" => SOME 9 | _ => NONE) |
|
37 |
||
39536
c62359dd253d
properly parse Z3 error models, including datatypes, and represent function valuations as lambda terms; also normalize Z3 error models
boehmes
parents:
37153
diff
changeset
|
38 |
val nat_num = spaced (Scan.repeat1 (Scan.some digit) >> |
c62359dd253d
properly parse Z3 error models, including datatypes, and represent function valuations as lambda terms; also normalize Z3 error models
boehmes
parents:
37153
diff
changeset
|
39 |
(fn ds => fold (fn d => fn i => i * 10 + d) ds 0)) |
c62359dd253d
properly parse Z3 error models, including datatypes, and represent function valuations as lambda terms; also normalize Z3 error models
boehmes
parents:
37153
diff
changeset
|
40 |
val int_num = spaced (Scan.optional ($$ "-" >> K (fn i => ~i)) I :|-- |
c62359dd253d
properly parse Z3 error models, including datatypes, and represent function valuations as lambda terms; also normalize Z3 error models
boehmes
parents:
37153
diff
changeset
|
41 |
(fn sign => nat_num >> sign)) |
36898 | 42 |
|
43 |
val is_char = Symbol.is_ascii_letter orf Symbol.is_ascii_digit orf |
|
40627
becf5d5187cc
renamed raw "explode" function to "raw_explode" to emphasize its meaning;
wenzelm
parents:
40579
diff
changeset
|
44 |
member (op =) (raw_explode "_+*-/%~=<>$&|?!.@^#") |
39536
c62359dd253d
properly parse Z3 error models, including datatypes, and represent function valuations as lambda terms; also normalize Z3 error models
boehmes
parents:
37153
diff
changeset
|
45 |
val name = spaced (Scan.many1 is_char >> implode) |
c62359dd253d
properly parse Z3 error models, including datatypes, and represent function valuations as lambda terms; also normalize Z3 error models
boehmes
parents:
37153
diff
changeset
|
46 |
|
c62359dd253d
properly parse Z3 error models, including datatypes, and represent function valuations as lambda terms; also normalize Z3 error models
boehmes
parents:
37153
diff
changeset
|
47 |
fun $$$ s = spaced (Scan.this_string s) |
36898 | 48 |
|
39536
c62359dd253d
properly parse Z3 error models, including datatypes, and represent function valuations as lambda terms; also normalize Z3 error models
boehmes
parents:
37153
diff
changeset
|
49 |
fun array_expr st = st |> in_parens ( |
c62359dd253d
properly parse Z3 error models, including datatypes, and represent function valuations as lambda terms; also normalize Z3 error models
boehmes
parents:
37153
diff
changeset
|
50 |
$$$ "const" |-- expr >> Fresh || |
c62359dd253d
properly parse Z3 error models, including datatypes, and represent function valuations as lambda terms; also normalize Z3 error models
boehmes
parents:
37153
diff
changeset
|
51 |
$$$ "store" |-- array_expr -- expr -- expr >> Store) |
36898 | 52 |
|
39536
c62359dd253d
properly parse Z3 error models, including datatypes, and represent function valuations as lambda terms; also normalize Z3 error models
boehmes
parents:
37153
diff
changeset
|
53 |
and expr st = st |> ( |
c62359dd253d
properly parse Z3 error models, including datatypes, and represent function valuations as lambda terms; also normalize Z3 error models
boehmes
parents:
37153
diff
changeset
|
54 |
$$$ "true" >> K True || |
c62359dd253d
properly parse Z3 error models, including datatypes, and represent function valuations as lambda terms; also normalize Z3 error models
boehmes
parents:
37153
diff
changeset
|
55 |
$$$ "false" >> K False || |
c62359dd253d
properly parse Z3 error models, including datatypes, and represent function valuations as lambda terms; also normalize Z3 error models
boehmes
parents:
37153
diff
changeset
|
56 |
int_num -- Scan.option ($$$ "/" |-- int_num) >> Number || |
c62359dd253d
properly parse Z3 error models, including datatypes, and represent function valuations as lambda terms; also normalize Z3 error models
boehmes
parents:
37153
diff
changeset
|
57 |
$$$ "val!" |-- nat_num >> Value || |
c62359dd253d
properly parse Z3 error models, including datatypes, and represent function valuations as lambda terms; also normalize Z3 error models
boehmes
parents:
37153
diff
changeset
|
58 |
name >> (App o rpair []) || |
c62359dd253d
properly parse Z3 error models, including datatypes, and represent function valuations as lambda terms; also normalize Z3 error models
boehmes
parents:
37153
diff
changeset
|
59 |
array_expr >> Array || |
c62359dd253d
properly parse Z3 error models, including datatypes, and represent function valuations as lambda terms; also normalize Z3 error models
boehmes
parents:
37153
diff
changeset
|
60 |
in_parens (name -- Scan.repeat1 expr) >> App) |
36898 | 61 |
|
39536
c62359dd253d
properly parse Z3 error models, including datatypes, and represent function valuations as lambda terms; also normalize Z3 error models
boehmes
parents:
37153
diff
changeset
|
62 |
fun args st = ($$$ "->" >> K [] || expr ::: args) st |
c62359dd253d
properly parse Z3 error models, including datatypes, and represent function valuations as lambda terms; also normalize Z3 error models
boehmes
parents:
37153
diff
changeset
|
63 |
val args_case = args -- expr |
c62359dd253d
properly parse Z3 error models, including datatypes, and represent function valuations as lambda terms; also normalize Z3 error models
boehmes
parents:
37153
diff
changeset
|
64 |
val else_case = $$$ "else" -- $$$ "->" |-- expr >> pair ([] : expr list) |
36898 | 65 |
|
66 |
val func = |
|
67 |
let fun cases st = (else_case >> single || args_case ::: cases) st |
|
68 |
in in_braces cases end |
|
69 |
||
39536
c62359dd253d
properly parse Z3 error models, including datatypes, and represent function valuations as lambda terms; also normalize Z3 error models
boehmes
parents:
37153
diff
changeset
|
70 |
val cex = space |-- |
c62359dd253d
properly parse Z3 error models, including datatypes, and represent function valuations as lambda terms; also normalize Z3 error models
boehmes
parents:
37153
diff
changeset
|
71 |
Scan.repeat (name --| $$$ "->" -- (func || expr >> (single o pair []))) |
36898 | 72 |
|
40828
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset
|
73 |
fun resolve terms ((n, k), cases) = |
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset
|
74 |
(case Symtab.lookup terms n of |
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset
|
75 |
NONE => NONE |
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset
|
76 |
| SOME t => SOME ((t, k), cases)) |
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset
|
77 |
|
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset
|
78 |
fun annotate _ (_, []) = NONE |
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset
|
79 |
| annotate terms (n, [([], c)]) = resolve terms ((n, 0), (c, [])) |
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset
|
80 |
| annotate _ (_, [_]) = NONE |
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset
|
81 |
| annotate terms (n, cases as (args, _) :: _) = |
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset
|
82 |
let val (cases', (_, else_case)) = split_last cases |
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset
|
83 |
in resolve terms ((n, length args), (else_case, cases')) end |
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset
|
84 |
|
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset
|
85 |
fun read_cex terms ls = |
40627
becf5d5187cc
renamed raw "explode" function to "raw_explode" to emphasize its meaning;
wenzelm
parents:
40579
diff
changeset
|
86 |
maps (cons "\n" o raw_explode) ls |
36898 | 87 |
|> try (fst o Scan.finite Symbol.stopper cex) |
88 |
|> the_default [] |
|
40828
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset
|
89 |
|> map_filter (annotate terms) |
39536
c62359dd253d
properly parse Z3 error models, including datatypes, and represent function valuations as lambda terms; also normalize Z3 error models
boehmes
parents:
37153
diff
changeset
|
90 |
|
c62359dd253d
properly parse Z3 error models, including datatypes, and represent function valuations as lambda terms; also normalize Z3 error models
boehmes
parents:
37153
diff
changeset
|
91 |
|
36898 | 92 |
(* translation into terms *) |
93 |
||
40828
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset
|
94 |
fun max_value vs = |
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset
|
95 |
let |
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset
|
96 |
fun max_val_expr (Value i) = Integer.max i |
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset
|
97 |
| max_val_expr (App (_, es)) = fold max_val_expr es |
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset
|
98 |
| max_val_expr (Array a) = max_val_array a |
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset
|
99 |
| max_val_expr _ = I |
36898 | 100 |
|
40828
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset
|
101 |
and max_val_array (Fresh e) = max_val_expr e |
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset
|
102 |
| max_val_array (Store ((a, e1), e2)) = |
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset
|
103 |
max_val_array a #> max_val_expr e1 #> max_val_expr e2 |
36898 | 104 |
|
40828
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset
|
105 |
fun max_val (_, (ec, cs)) = |
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset
|
106 |
max_val_expr ec #> fold (fn (es, e) => fold max_val_expr (e :: es)) cs |
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset
|
107 |
|
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset
|
108 |
in fold max_val vs ~1 end |
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset
|
109 |
|
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset
|
110 |
fun with_context terms f vs = fst (fold_map f vs (terms, max_value vs + 1)) |
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset
|
111 |
|
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset
|
112 |
fun get_term n T es (cx as (terms, next_val)) = |
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset
|
113 |
(case Symtab.lookup terms n of |
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset
|
114 |
SOME t => ((t, es), cx) |
36898 | 115 |
| NONE => |
40828
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset
|
116 |
let val t = Var (("fresh", next_val), T) |
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset
|
117 |
in ((t, []), (Symtab.update (n, t) terms, next_val + 1)) end) |
36898 | 118 |
|
40579
98ebd2300823
use the const antiquotation for constants (this checks that the constant is declared, whereas the more general term antiquotation treats undeclared names as free variable)
boehmes
parents:
40551
diff
changeset
|
119 |
fun trans_expr _ True = pair @{const True} |
98ebd2300823
use the const antiquotation for constants (this checks that the constant is declared, whereas the more general term antiquotation treats undeclared names as free variable)
boehmes
parents:
40551
diff
changeset
|
120 |
| trans_expr _ False = pair @{const False} |
36898 | 121 |
| trans_expr T (Number (i, NONE)) = pair (HOLogic.mk_number T i) |
122 |
| trans_expr T (Number (i, SOME j)) = |
|
123 |
pair (Const (@{const_name divide}, [T, T] ---> T) $ |
|
124 |
HOLogic.mk_number T i $ HOLogic.mk_number T j) |
|
40828
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset
|
125 |
| trans_expr T (Value i) = pair (Var (("value", i), T)) |
36898 | 126 |
| trans_expr T (Array a) = trans_array T a |
40828
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset
|
127 |
| trans_expr T (App (n, es)) = get_term n T es #-> (fn (t, es') => |
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset
|
128 |
let val Ts = fst (U.dest_funT (length es') (Term.fastype_of t)) |
39536
c62359dd253d
properly parse Z3 error models, including datatypes, and represent function valuations as lambda terms; also normalize Z3 error models
boehmes
parents:
37153
diff
changeset
|
129 |
in |
40828
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset
|
130 |
fold_map (uncurry trans_expr) (Ts ~~ es') #>> Term.list_comb o pair t |
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset
|
131 |
end) |
36898 | 132 |
|
133 |
and trans_array T a = |
|
40828
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset
|
134 |
let val (dT, rT) = U.split_type T |
36898 | 135 |
in |
136 |
(case a of |
|
137 |
Fresh e => trans_expr rT e #>> (fn t => Abs ("x", dT, t)) |
|
138 |
| Store ((a', e1), e2) => |
|
139 |
trans_array T a' ##>> trans_expr dT e1 ##>> trans_expr rT e2 #>> |
|
140 |
(fn ((m, k), v) => |
|
141 |
Const (@{const_name fun_upd}, [T, dT, rT] ---> T) $ m $ k $ v)) |
|
142 |
end |
|
143 |
||
39536
c62359dd253d
properly parse Z3 error models, including datatypes, and represent function valuations as lambda terms; also normalize Z3 error models
boehmes
parents:
37153
diff
changeset
|
144 |
fun trans_pattern T ([], e) = trans_expr T e #>> pair [] |
c62359dd253d
properly parse Z3 error models, including datatypes, and represent function valuations as lambda terms; also normalize Z3 error models
boehmes
parents:
37153
diff
changeset
|
145 |
| trans_pattern T (arg :: args, e) = |
c62359dd253d
properly parse Z3 error models, including datatypes, and represent function valuations as lambda terms; also normalize Z3 error models
boehmes
parents:
37153
diff
changeset
|
146 |
trans_expr (Term.domain_type T) arg ##>> |
c62359dd253d
properly parse Z3 error models, including datatypes, and represent function valuations as lambda terms; also normalize Z3 error models
boehmes
parents:
37153
diff
changeset
|
147 |
trans_pattern (Term.range_type T) (args, e) #>> |
c62359dd253d
properly parse Z3 error models, including datatypes, and represent function valuations as lambda terms; also normalize Z3 error models
boehmes
parents:
37153
diff
changeset
|
148 |
(fn (arg', (args', e')) => (arg' :: args', e')) |
36898 | 149 |
|
39536
c62359dd253d
properly parse Z3 error models, including datatypes, and represent function valuations as lambda terms; also normalize Z3 error models
boehmes
parents:
37153
diff
changeset
|
150 |
fun mk_fun_upd T U = Const (@{const_name fun_upd}, [T --> U, T, U, T] ---> U) |
c62359dd253d
properly parse Z3 error models, including datatypes, and represent function valuations as lambda terms; also normalize Z3 error models
boehmes
parents:
37153
diff
changeset
|
151 |
|
c62359dd253d
properly parse Z3 error models, including datatypes, and represent function valuations as lambda terms; also normalize Z3 error models
boehmes
parents:
37153
diff
changeset
|
152 |
fun mk_update ([], u) _ = u |
c62359dd253d
properly parse Z3 error models, including datatypes, and represent function valuations as lambda terms; also normalize Z3 error models
boehmes
parents:
37153
diff
changeset
|
153 |
| mk_update ([t], u) f = |
40663 | 154 |
uncurry mk_fun_upd (U.split_type (Term.fastype_of f)) $ f $ t $ u |
39536
c62359dd253d
properly parse Z3 error models, including datatypes, and represent function valuations as lambda terms; also normalize Z3 error models
boehmes
parents:
37153
diff
changeset
|
155 |
| mk_update (t :: ts, u) f = |
c62359dd253d
properly parse Z3 error models, including datatypes, and represent function valuations as lambda terms; also normalize Z3 error models
boehmes
parents:
37153
diff
changeset
|
156 |
let |
40663 | 157 |
val (dT, rT) = U.split_type (Term.fastype_of f) |
158 |
val (dT', rT') = U.split_type rT |
|
39536
c62359dd253d
properly parse Z3 error models, including datatypes, and represent function valuations as lambda terms; also normalize Z3 error models
boehmes
parents:
37153
diff
changeset
|
159 |
in |
c62359dd253d
properly parse Z3 error models, including datatypes, and represent function valuations as lambda terms; also normalize Z3 error models
boehmes
parents:
37153
diff
changeset
|
160 |
mk_fun_upd dT rT $ f $ t $ |
c62359dd253d
properly parse Z3 error models, including datatypes, and represent function valuations as lambda terms; also normalize Z3 error models
boehmes
parents:
37153
diff
changeset
|
161 |
mk_update (ts, u) (Term.absdummy (dT', Const ("_", rT'))) |
c62359dd253d
properly parse Z3 error models, including datatypes, and represent function valuations as lambda terms; also normalize Z3 error models
boehmes
parents:
37153
diff
changeset
|
162 |
end |
c62359dd253d
properly parse Z3 error models, including datatypes, and represent function valuations as lambda terms; also normalize Z3 error models
boehmes
parents:
37153
diff
changeset
|
163 |
|
c62359dd253d
properly parse Z3 error models, including datatypes, and represent function valuations as lambda terms; also normalize Z3 error models
boehmes
parents:
37153
diff
changeset
|
164 |
fun mk_lambda Ts (t, pats) = |
c62359dd253d
properly parse Z3 error models, including datatypes, and represent function valuations as lambda terms; also normalize Z3 error models
boehmes
parents:
37153
diff
changeset
|
165 |
fold_rev (curry Term.absdummy) Ts t |> fold mk_update pats |
36898 | 166 |
|
40828
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset
|
167 |
fun translate ((t, k), (e, cs)) = |
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset
|
168 |
let |
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset
|
169 |
val T = Term.fastype_of t |
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset
|
170 |
val (Us, U) = U.dest_funT k (Term.fastype_of t) |
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset
|
171 |
|
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset
|
172 |
fun mk_full_def u' pats = |
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset
|
173 |
pats |
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset
|
174 |
|> filter_out (fn (_, u) => u aconv u') |
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset
|
175 |
|> HOLogic.mk_eq o pair t o mk_lambda Us o pair u' |
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset
|
176 |
|
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset
|
177 |
fun mk_eq (us, u) = HOLogic.mk_eq (Term.list_comb (t, us), u) |
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset
|
178 |
fun mk_eqs u' [] = [HOLogic.mk_eq (t, u')] |
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset
|
179 |
| mk_eqs _ pats = map mk_eq pats |
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset
|
180 |
in |
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset
|
181 |
trans_expr U e ##>> |
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset
|
182 |
(if k = 0 then pair [] else fold_map (trans_pattern T) cs) #>> |
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset
|
183 |
(fn (u', pats) => (mk_eqs u' pats, mk_full_def u' pats)) |
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset
|
184 |
end |
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset
|
185 |
|
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset
|
186 |
|
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset
|
187 |
(* normalization *) |
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset
|
188 |
|
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset
|
189 |
fun partition_eqs f = |
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset
|
190 |
let |
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset
|
191 |
fun part t (xs, ts) = |
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset
|
192 |
(case try HOLogic.dest_eq t of |
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset
|
193 |
SOME (l, r) => (case f l r of SOME x => (x::xs, ts) | _ => (xs, t::ts)) |
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset
|
194 |
| NONE => (xs, t :: ts)) |
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset
|
195 |
in (fn ts => fold part ts ([], [])) end |
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset
|
196 |
|
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset
|
197 |
fun replace_vars tab = |
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset
|
198 |
let |
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset
|
199 |
fun replace (v as Var _) = the_default v (AList.lookup (op aconv) tab v) |
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset
|
200 |
| replace t = t |
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset
|
201 |
in map (Term.map_aterms replace) end |
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset
|
202 |
|
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset
|
203 |
fun remove_int_nat_coercions (eqs, defs) = |
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset
|
204 |
let |
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset
|
205 |
fun mk_nat_num t i = |
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset
|
206 |
(case try HOLogic.dest_number i of |
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset
|
207 |
SOME (_, n) => SOME (t, HOLogic.mk_number @{typ nat} n) |
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset
|
208 |
| NONE => NONE) |
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset
|
209 |
fun nat_of (@{const of_nat (int)} $ (t as Var _)) i = mk_nat_num t i |
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset
|
210 |
| nat_of (@{const nat} $ i) (t as Var _) = mk_nat_num t i |
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset
|
211 |
| nat_of _ _ = NONE |
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset
|
212 |
val (nats, eqs') = partition_eqs nat_of eqs |
39536
c62359dd253d
properly parse Z3 error models, including datatypes, and represent function valuations as lambda terms; also normalize Z3 error models
boehmes
parents:
37153
diff
changeset
|
213 |
|
40828
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset
|
214 |
fun is_coercion t = |
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset
|
215 |
(case try HOLogic.dest_eq t of |
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset
|
216 |
SOME (@{const of_nat (int)}, _) => true |
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset
|
217 |
| SOME (@{const nat}, _) => true |
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset
|
218 |
| _ => false) |
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset
|
219 |
in pairself (replace_vars nats) (eqs', filter_out is_coercion defs) end |
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset
|
220 |
|
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset
|
221 |
fun unfold_funapp (eqs, defs) = |
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset
|
222 |
let |
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset
|
223 |
fun unfold_app (Const (@{const_name SMT.fun_app}, _) $ f $ t) = f $ t |
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset
|
224 |
| unfold_app t = t |
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset
|
225 |
fun unfold_eq ((eq as Const (@{const_name HOL.eq}, _)) $ t $ u) = |
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset
|
226 |
eq $ unfold_app t $ u |
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset
|
227 |
| unfold_eq t = t |
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset
|
228 |
|
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset
|
229 |
fun is_fun_app t = |
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset
|
230 |
(case try HOLogic.dest_eq t of |
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset
|
231 |
SOME (Const (@{const_name SMT.fun_app}, _), _) => true |
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset
|
232 |
| _ => false) |
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset
|
233 |
|
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset
|
234 |
in (map unfold_eq eqs, filter_out is_fun_app defs) end |
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset
|
235 |
|
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset
|
236 |
fun unfold_simple_eqs (eqs, defs) = |
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset
|
237 |
let |
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset
|
238 |
fun add_rewr (l as Const _) (r as Var _) = SOME (r, l) |
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset
|
239 |
| add_rewr (l as Free _) (r as Var _) = SOME (r, l) |
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset
|
240 |
| add_rewr _ _ = NONE |
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset
|
241 |
val (rs, eqs') = partition_eqs add_rewr eqs |
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset
|
242 |
|
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset
|
243 |
fun is_trivial (Const (@{const_name HOL.eq}, _) $ t $ u) = t aconv u |
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset
|
244 |
| is_trivial _ = false |
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset
|
245 |
in pairself (replace_vars rs #> filter_out is_trivial) (eqs', defs) end |
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset
|
246 |
|
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset
|
247 |
fun swap_free ((eq as Const (@{const_name HOL.eq}, _)) $ t $ (u as Free _)) = |
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset
|
248 |
eq $ u $ t |
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset
|
249 |
| swap_free t = t |
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset
|
250 |
|
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset
|
251 |
fun frees_for_vars ctxt (eqs, defs) = |
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset
|
252 |
let |
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset
|
253 |
fun fresh_free i T (cx as (frees, ctxt)) = |
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset
|
254 |
(case Inttab.lookup frees i of |
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset
|
255 |
SOME t => (t, cx) |
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset
|
256 |
| NONE => |
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset
|
257 |
let |
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset
|
258 |
val (n, ctxt') = yield_singleton Variable.variant_fixes "" ctxt |
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset
|
259 |
val t = Free (n, T) |
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset
|
260 |
in (t, (Inttab.update (i, t) frees, ctxt')) end) |
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset
|
261 |
|
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset
|
262 |
fun repl_var (Var ((_, i), T)) = fresh_free i T |
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset
|
263 |
| repl_var (t $ u) = repl_var t ##>> repl_var u #>> op $ |
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset
|
264 |
| repl_var (Abs (n, T, t)) = repl_var t #>> (fn t' => Abs (n, T, t')) |
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset
|
265 |
| repl_var t = pair t |
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset
|
266 |
in |
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset
|
267 |
(Inttab.empty, ctxt) |
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset
|
268 |
|> fold_map repl_var eqs |
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset
|
269 |
||>> fold_map repl_var defs |
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset
|
270 |
|> fst |
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset
|
271 |
end |
36898 | 272 |
|
273 |
||
274 |
(* overall procedure *) |
|
275 |
||
40828
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset
|
276 |
val is_free_constraint = Term.exists_subterm (fn Free _ => true | _ => false) |
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset
|
277 |
|
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset
|
278 |
fun is_const_def (Const (@{const_name HOL.eq}, _) $ Const _ $ _) = true |
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset
|
279 |
| is_const_def _ = false |
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset
|
280 |
|
39536
c62359dd253d
properly parse Z3 error models, including datatypes, and represent function valuations as lambda terms; also normalize Z3 error models
boehmes
parents:
37153
diff
changeset
|
281 |
fun parse_counterex ctxt ({terms, ...} : SMT_Translate.recon) ls = |
40828
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset
|
282 |
read_cex terms ls |
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset
|
283 |
|> with_context terms translate |
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset
|
284 |
|> apfst flat o split_list |
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset
|
285 |
|> remove_int_nat_coercions |
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset
|
286 |
|> unfold_funapp |
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset
|
287 |
|> unfold_simple_eqs |
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset
|
288 |
|>> map swap_free |
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset
|
289 |
|>> filter is_free_constraint |
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset
|
290 |
|> frees_for_vars ctxt |
47ff261431c4
split up Z3 models into constraints on free variables and constant definitions;
boehmes
parents:
40663
diff
changeset
|
291 |
||> filter is_const_def |
36898 | 292 |
|
293 |
end |
|
39536
c62359dd253d
properly parse Z3 error models, including datatypes, and represent function valuations as lambda terms; also normalize Z3 error models
boehmes
parents:
37153
diff
changeset
|
294 |