author | wenzelm |
Sat, 20 Nov 2010 00:53:26 +0100 | |
changeset 40627 | becf5d5187cc |
parent 40579 | 98ebd2300823 |
child 40663 | e080c9e68752 |
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 -> |
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
|
10 |
term list |
36898 | 11 |
end |
12 |
||
13 |
structure Z3_Model: Z3_MODEL = |
|
14 |
struct |
|
15 |
||
16 |
(* counterexample expressions *) |
|
17 |
||
18 |
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
|
19 |
Array of array | App of string * expr list |
36898 | 20 |
and array = Fresh of expr | Store of (array * expr) * expr |
21 |
||
22 |
||
23 |
(* parsing *) |
|
24 |
||
25 |
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
|
26 |
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
|
27 |
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
|
28 |
fun in_braces p = spaced (Scan.$$ "{") |-- p --| spaced (Scan.$$ "}") |
36898 | 29 |
|
30 |
val digit = (fn |
|
31 |
"0" => SOME 0 | "1" => SOME 1 | "2" => SOME 2 | "3" => SOME 3 | |
|
32 |
"4" => SOME 4 | "5" => SOME 5 | "6" => SOME 6 | "7" => SOME 7 | |
|
33 |
"8" => SOME 8 | "9" => SOME 9 | _ => NONE) |
|
34 |
||
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
|
35 |
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
|
36 |
(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
|
37 |
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
|
38 |
(fn sign => nat_num >> sign)) |
36898 | 39 |
|
40 |
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
|
41 |
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
|
42 |
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
|
43 |
|
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
|
44 |
fun $$$ s = spaced (Scan.this_string s) |
36898 | 45 |
|
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
|
46 |
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
|
47 |
$$$ "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
|
48 |
$$$ "store" |-- array_expr -- expr -- expr >> Store) |
36898 | 49 |
|
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
|
50 |
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
|
51 |
$$$ "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
|
52 |
$$$ "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
|
53 |
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
|
54 |
$$$ "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
|
55 |
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
|
56 |
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
|
57 |
in_parens (name -- Scan.repeat1 expr) >> App) |
36898 | 58 |
|
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
|
59 |
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
|
60 |
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
|
61 |
val else_case = $$$ "else" -- $$$ "->" |-- expr >> pair ([] : expr list) |
36898 | 62 |
|
63 |
val func = |
|
64 |
let fun cases st = (else_case >> single || args_case ::: cases) st |
|
65 |
in in_braces cases end |
|
66 |
||
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
|
67 |
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
|
68 |
Scan.repeat (name --| $$$ "->" -- (func || expr >> (single o pair []))) |
36898 | 69 |
|
70 |
fun read_cex ls = |
|
40627
becf5d5187cc
renamed raw "explode" function to "raw_explode" to emphasize its meaning;
wenzelm
parents:
40579
diff
changeset
|
71 |
maps (cons "\n" o raw_explode) ls |
36898 | 72 |
|> try (fst o Scan.finite Symbol.stopper cex) |
73 |
|> the_default [] |
|
74 |
||
75 |
||
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
|
76 |
(* normalization *) |
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
|
77 |
|
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
|
78 |
local |
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
|
79 |
fun matches terms f n = |
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
|
80 |
(case Symtab.lookup terms n of |
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
|
81 |
NONE => 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
|
82 |
| SOME t => 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
|
83 |
|
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
|
84 |
fun subst f (n, cases) = (n, map (fn (args, v) => (map f args, f v)) cases) |
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
|
85 |
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
|
86 |
|
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
|
87 |
fun reduce_function (n, [c]) = SOME ((n, 0), [c]) |
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
|
88 |
| reduce_function (n, cases) = |
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
|
89 |
let val (patterns, else_case as (_, e)) = split_last cases |
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 |
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
|
91 |
(case patterns of |
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
|
92 |
[] => NONE |
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
|
93 |
| (args, _) :: _ => SOME ((n, length args), |
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
|
94 |
filter_out (equal e o snd) patterns @ [else_case])) |
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
|
95 |
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
|
96 |
|
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
|
97 |
fun drop_skolem_constants terms = filter (Symtab.defined terms o fst o fst) |
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
|
98 |
|
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
|
99 |
fun substitute_constants terms = |
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
|
100 |
let |
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
|
101 |
fun check vs1 [] = rev vs1 |
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
|
102 |
| check vs1 ((v as ((n, k), [([], Value i)])) :: vs2) = |
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
|
103 |
if matches terms (fn Free _ => true | _ => false) n orelse k > 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
|
104 |
then check (v :: vs1) vs2 |
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
|
105 |
else |
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
|
106 |
let |
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
|
107 |
fun sub (e as Value j) = if i = j then App (n, []) else 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
|
108 |
| sub e = 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
|
109 |
in check (map (subst sub) vs1) (map (subst sub) vs2) 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
|
110 |
| check vs1 (v :: vs2) = check (v :: vs1) vs2 |
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
|
111 |
in check [] 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
|
112 |
|
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
|
113 |
fun remove_int_nat_coercions terms vs = |
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
|
114 |
let |
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
|
115 |
fun match ts ((n, _), _) = matches terms (member (op aconv) ts) n |
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
|
116 |
|
40551
a0dd429e97d9
only replace unknowns of type nat with known integer numbers, don't alias unknown values in Z3's counterexamples with known integers
boehmes
parents:
39536
diff
changeset
|
117 |
val (default_int, ints) = |
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
|
118 |
(case find_first (match [@{const of_nat (int)}]) vs of |
40551
a0dd429e97d9
only replace unknowns of type nat with known integer numbers, don't alias unknown values in Z3's counterexamples with known integers
boehmes
parents:
39536
diff
changeset
|
119 |
NONE => (NONE, []) |
a0dd429e97d9
only replace unknowns of type nat with known integer numbers, don't alias unknown values in Z3's counterexamples with known integers
boehmes
parents:
39536
diff
changeset
|
120 |
| SOME (_, cases) => |
a0dd429e97d9
only replace unknowns of type nat with known integer numbers, don't alias unknown values in Z3's counterexamples with known integers
boehmes
parents:
39536
diff
changeset
|
121 |
let val (cs, (_, e)) = split_last cases |
a0dd429e97d9
only replace unknowns of type nat with known integer numbers, don't alias unknown values in Z3's counterexamples with known integers
boehmes
parents:
39536
diff
changeset
|
122 |
in (SOME e, map (apfst hd) cs) end) |
a0dd429e97d9
only replace unknowns of type nat with known integer numbers, don't alias unknown values in Z3's counterexamples with known integers
boehmes
parents:
39536
diff
changeset
|
123 |
|
a0dd429e97d9
only replace unknowns of type nat with known integer numbers, don't alias unknown values in Z3's counterexamples with known integers
boehmes
parents:
39536
diff
changeset
|
124 |
fun nat_of @{typ nat} (v as Value _) = |
a0dd429e97d9
only replace unknowns of type nat with known integer numbers, don't alias unknown values in Z3's counterexamples with known integers
boehmes
parents:
39536
diff
changeset
|
125 |
AList.lookup (op =) ints v |> the_default (the_default v default_int) |
a0dd429e97d9
only replace unknowns of type nat with known integer numbers, don't alias unknown values in Z3's counterexamples with known integers
boehmes
parents:
39536
diff
changeset
|
126 |
| nat_of _ e = e |
a0dd429e97d9
only replace unknowns of type nat with known integer numbers, don't alias unknown values in Z3's counterexamples with known integers
boehmes
parents:
39536
diff
changeset
|
127 |
|
a0dd429e97d9
only replace unknowns of type nat with known integer numbers, don't alias unknown values in Z3's counterexamples with known integers
boehmes
parents:
39536
diff
changeset
|
128 |
fun subst_nat T k ([], e) = |
a0dd429e97d9
only replace unknowns of type nat with known integer numbers, don't alias unknown values in Z3's counterexamples with known integers
boehmes
parents:
39536
diff
changeset
|
129 |
let fun app f i = if i <= 0 then I else app f (i-1) o f |
a0dd429e97d9
only replace unknowns of type nat with known integer numbers, don't alias unknown values in Z3's counterexamples with known integers
boehmes
parents:
39536
diff
changeset
|
130 |
in ([], nat_of (app Term.range_type k T) e) end |
a0dd429e97d9
only replace unknowns of type nat with known integer numbers, don't alias unknown values in Z3's counterexamples with known integers
boehmes
parents:
39536
diff
changeset
|
131 |
| subst_nat T k (arg :: args, e) = |
a0dd429e97d9
only replace unknowns of type nat with known integer numbers, don't alias unknown values in Z3's counterexamples with known integers
boehmes
parents:
39536
diff
changeset
|
132 |
subst_nat (Term.range_type T) (k-1) (args, e) |
a0dd429e97d9
only replace unknowns of type nat with known integer numbers, don't alias unknown values in Z3's counterexamples with known integers
boehmes
parents:
39536
diff
changeset
|
133 |
|> apfst (cons (nat_of (Term.domain_type T) arg)) |
a0dd429e97d9
only replace unknowns of type nat with known integer numbers, don't alias unknown values in Z3's counterexamples with known integers
boehmes
parents:
39536
diff
changeset
|
134 |
|
a0dd429e97d9
only replace unknowns of type nat with known integer numbers, don't alias unknown values in Z3's counterexamples with known integers
boehmes
parents:
39536
diff
changeset
|
135 |
fun subst_nats (v as ((n, k), cases)) = |
a0dd429e97d9
only replace unknowns of type nat with known integer numbers, don't alias unknown values in Z3's counterexamples with known integers
boehmes
parents:
39536
diff
changeset
|
136 |
(case Symtab.lookup terms n of |
a0dd429e97d9
only replace unknowns of type nat with known integer numbers, don't alias unknown values in Z3's counterexamples with known integers
boehmes
parents:
39536
diff
changeset
|
137 |
NONE => v |
a0dd429e97d9
only replace unknowns of type nat with known integer numbers, don't alias unknown values in Z3's counterexamples with known integers
boehmes
parents:
39536
diff
changeset
|
138 |
| SOME t => ((n, k), map (subst_nat (Term.fastype_of t) k) cases)) |
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
|
139 |
in |
40551
a0dd429e97d9
only replace unknowns of type nat with known integer numbers, don't alias unknown values in Z3's counterexamples with known integers
boehmes
parents:
39536
diff
changeset
|
140 |
map subst_nats vs |
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
|
141 |
|> filter_out (match [@{const of_nat (int)}, @{const nat}]) |
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
|
142 |
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
|
143 |
|
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 filter_valid_valuations terms = map_filter (fn |
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 |
(_, []) => NONE |
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 |
| ((n, i), cases) => |
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 |
let |
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 |
fun valid_expr (Array a) = valid_array a |
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
|
149 |
| valid_expr (App (n, es)) = |
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 |
Symtab.defined terms n andalso forall valid_expr es |
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 |
| valid_expr _ = 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
|
152 |
and valid_array (Fresh e) = valid_expr 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
|
153 |
| valid_array (Store ((a, e1), e2)) = |
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
|
154 |
valid_array a andalso valid_expr e1 andalso valid_expr e2 |
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 |
fun valid_case (es, e) = forall valid_expr (e :: es) |
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 |
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
|
157 |
if not (forall valid_case cases) then NONE |
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
|
158 |
else Option.map (rpair cases o rpair i) (Symtab.lookup terms n) |
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 |
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
|
160 |
|
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 |
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
|
162 |
|
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 |
|
36898 | 164 |
(* translation into terms *) |
165 |
||
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
|
166 |
fun with_context ctxt terms f vs = |
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
|
167 |
fst (fold_map f vs (ctxt, terms, Inttab.empty)) |
36898 | 168 |
|
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
|
169 |
fun fresh_term T (ctxt, terms, values) = |
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
|
170 |
let val (n, ctxt') = yield_singleton Variable.variant_fixes "" ctxt |
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
|
171 |
in (Free (n, T), (ctxt', terms, values)) end |
36898 | 172 |
|
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
|
173 |
fun term_of_value T i (cx as (_, _, values)) = |
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
|
174 |
(case Inttab.lookup values i of |
36898 | 175 |
SOME t => (t, cx) |
176 |
| NONE => |
|
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
|
177 |
let val (t, (ctxt', terms', values')) = fresh_term T cx |
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
|
178 |
in (t, (ctxt', terms', Inttab.update (i, t) values')) 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
|
179 |
|
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
|
180 |
fun get_term n (cx as (_, terms, _)) = (the (Symtab.lookup terms n), cx) |
36898 | 181 |
|
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
|
182 |
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
|
183 |
| trans_expr _ False = pair @{const False} |
36898 | 184 |
| trans_expr T (Number (i, NONE)) = pair (HOLogic.mk_number T i) |
185 |
| trans_expr T (Number (i, SOME j)) = |
|
186 |
pair (Const (@{const_name divide}, [T, T] ---> T) $ |
|
187 |
HOLogic.mk_number T i $ HOLogic.mk_number T j) |
|
188 |
| trans_expr T (Value i) = term_of_value T i |
|
189 |
| trans_expr T (Array a) = trans_array T a |
|
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
|
190 |
| trans_expr _ (App (n, es)) = |
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
|
191 |
let val get_Ts = take (length es) o Term.binder_types o Term.fastype_of |
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
|
192 |
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
|
193 |
get_term n #-> (fn 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
|
194 |
fold_map (uncurry trans_expr) (get_Ts t ~~ es) #>> |
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
|
195 |
Term.list_comb o pair 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
|
196 |
end |
36898 | 197 |
|
198 |
and trans_array T a = |
|
199 |
let val dT = Term.domain_type T and rT = Term.range_type T |
|
200 |
in |
|
201 |
(case a of |
|
202 |
Fresh e => trans_expr rT e #>> (fn t => Abs ("x", dT, t)) |
|
203 |
| Store ((a', e1), e2) => |
|
204 |
trans_array T a' ##>> trans_expr dT e1 ##>> trans_expr rT e2 #>> |
|
205 |
(fn ((m, k), v) => |
|
206 |
Const (@{const_name fun_upd}, [T, dT, rT] ---> T) $ m $ k $ v)) |
|
207 |
end |
|
208 |
||
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
|
209 |
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
|
210 |
| 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
|
211 |
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
|
212 |
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
|
213 |
(fn (arg', (args', e')) => (arg' :: args', e')) |
36898 | 214 |
|
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
|
215 |
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
|
216 |
|
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
|
217 |
fun split_type T = (Term.domain_type T, Term.range_type T) |
36898 | 218 |
|
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
|
219 |
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
|
220 |
| mk_update ([t], 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
|
221 |
uncurry mk_fun_upd (split_type (Term.fastype_of f)) $ f $ 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
|
222 |
| 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
|
223 |
let |
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
|
224 |
val (dT, rT) = split_type (Term.fastype_of 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
|
225 |
val (dT', rT') = split_type 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
|
226 |
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
|
227 |
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
|
228 |
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
|
229 |
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
|
230 |
|
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
|
231 |
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
|
232 |
fold_rev (curry Term.absdummy) Ts t |> fold mk_update pats |
36898 | 233 |
|
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
|
234 |
fun translate' T i [([], 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
|
235 |
if i = 0 then trans_expr T 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
|
236 |
else |
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
|
237 |
let val ((Us1, Us2), U) = Term.strip_type T |>> chop 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
|
238 |
in trans_expr (Us2 ---> U) e #>> mk_lambda Us1 o rpair [] 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
|
239 |
| translate' T i cases = |
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
|
240 |
let |
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
|
241 |
val (pat_cases, def) = split_last cases |> apsnd snd |
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
|
242 |
val ((Us1, Us2), U) = Term.strip_type T |>> chop 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
|
243 |
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
|
244 |
trans_expr (Us2 ---> U) def ##>> |
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
|
245 |
fold_map (trans_pattern T) pat_cases #>> |
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
|
246 |
mk_lambda Us1 |
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
|
247 |
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
|
248 |
|
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
|
249 |
fun translate ((t, i), cases) = |
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
|
250 |
translate' (Term.fastype_of t) i cases #>> HOLogic.mk_eq o pair t |
36898 | 251 |
|
252 |
||
253 |
(* overall procedure *) |
|
254 |
||
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
|
255 |
fun parse_counterex ctxt ({terms, ...} : SMT_Translate.recon) ls = |
36898 | 256 |
read_cex ls |
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
|
257 |
|> map_filter reduce_function |
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
|
258 |
|> drop_skolem_constants terms |
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
|
259 |
|> substitute_constants terms |
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
|
260 |
|> remove_int_nat_coercions terms |
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
|
261 |
|> filter_valid_valuations terms |
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
|
262 |
|> with_context ctxt terms translate |
36898 | 263 |
|
264 |
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
|
265 |