author | fleury <Mathias.Fleury@mpi-inf.mpg.de> |
Tue, 10 Nov 2015 17:49:54 +0100 | |
changeset 61611 | a9c0572109af |
parent 59014 | cc5e34575354 |
child 69205 | 8050734eee3e |
permissions | -rw-r--r-- |
58061 | 1 |
(* Title: HOL/Tools/SMT/verit_proof.ML |
57704 | 2 |
Author: Mathias Fleury, ENS Rennes |
3 |
Author: Sascha Boehme, TU Muenchen |
|
4 |
||
5 |
VeriT proofs: parsing and abstract syntax tree. |
|
6 |
*) |
|
7 |
||
8 |
signature VERIT_PROOF = |
|
9 |
sig |
|
10 |
(*proofs*) |
|
11 |
datatype veriT_step = VeriT_Step of { |
|
57712
3c4e6bc7455f
Simplifying the labels in the proof of the SMT solver veriT.
fleury
parents:
57710
diff
changeset
|
12 |
id: string, |
57704 | 13 |
rule: string, |
14 |
prems: string list, |
|
15 |
concl: term, |
|
16 |
fixes: string list} |
|
17 |
||
18 |
(*proof parser*) |
|
19 |
val parse: typ Symtab.table -> term Symtab.table -> string list -> |
|
20 |
Proof.context -> veriT_step list * Proof.context |
|
21 |
||
57705 | 22 |
val veriT_step_prefix : string |
23 |
val veriT_input_rule: string |
|
57762 | 24 |
val veriT_la_generic_rule : string |
57705 | 25 |
val veriT_rewrite_rule : string |
57762 | 26 |
val veriT_simp_arith_rule : string |
27 |
val veriT_tmp_ite_elim_rule : string |
|
57714
4856a7b8b9c3
Changing the role of rule "tmp_ite_elim" of the SMT solver veriT to Lemma.
fleury
parents:
57713
diff
changeset
|
28 |
val veriT_tmp_skolemize_rule : string |
57704 | 29 |
end; |
30 |
||
31 |
structure VeriT_Proof: VERIT_PROOF = |
|
32 |
struct |
|
33 |
||
58061 | 34 |
open SMTLIB_Proof |
57704 | 35 |
|
36 |
datatype veriT_node = VeriT_Node of { |
|
57712
3c4e6bc7455f
Simplifying the labels in the proof of the SMT solver veriT.
fleury
parents:
57710
diff
changeset
|
37 |
id: string, |
57704 | 38 |
rule: string, |
39 |
prems: string list, |
|
40 |
concl: term, |
|
41 |
bounds: string list} |
|
42 |
||
43 |
fun mk_node id rule prems concl bounds = |
|
44 |
VeriT_Node {id = id, rule = rule, prems = prems, concl = concl, bounds = bounds} |
|
45 |
||
46 |
datatype veriT_step = VeriT_Step of { |
|
57712
3c4e6bc7455f
Simplifying the labels in the proof of the SMT solver veriT.
fleury
parents:
57710
diff
changeset
|
47 |
id: string, |
57704 | 48 |
rule: string, |
49 |
prems: string list, |
|
50 |
concl: term, |
|
51 |
fixes: string list} |
|
52 |
||
53 |
fun mk_step id rule prems concl fixes = |
|
54 |
VeriT_Step {id = id, rule = rule, prems = prems, concl = concl, fixes = fixes} |
|
55 |
||
57705 | 56 |
val veriT_step_prefix = ".c" |
57 |
val veriT_input_rule = "input" |
|
57762 | 58 |
val veriT_la_generic_rule = "la_generic" |
59 |
val veriT_rewrite_rule = "__rewrite" (* arbitrary *) |
|
60 |
val veriT_simp_arith_rule = "simp_arith" |
|
59014 | 61 |
val veriT_tmp_alphaconv_rule = "tmp_alphaconv" |
57708
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
62 |
val veriT_tmp_ite_elim_rule = "tmp_ite_elim" |
57713 | 63 |
val veriT_tmp_skolemize_rule = "tmp_skolemize" |
57708
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
64 |
|
57704 | 65 |
(* proof parser *) |
66 |
||
67 |
fun node_of p cx = |
|
68 |
([], cx) |
|
57747 | 69 |
||>> `(with_fresh_names (term_of p)) |
57716 | 70 |
|>> snd |
57704 | 71 |
|
72 |
(*in order to get Z3-style quantification*) |
|
58061 | 73 |
fun repair_quantification (SMTLIB.S (SMTLIB.Sym "forall" :: l)) = |
57762 | 74 |
let val (quantified_vars, t) = split_last (map repair_quantification l) |
57704 | 75 |
in |
58061 | 76 |
SMTLIB.S (SMTLIB.Sym "forall" :: SMTLIB.S quantified_vars :: t :: []) |
57704 | 77 |
end |
58061 | 78 |
| repair_quantification (SMTLIB.S (SMTLIB.Sym "exists" :: l)) = |
57762 | 79 |
let val (quantified_vars, t) = split_last (map repair_quantification l) |
57704 | 80 |
in |
58061 | 81 |
SMTLIB.S (SMTLIB.Sym "exists" :: SMTLIB.S quantified_vars :: t :: []) |
57704 | 82 |
end |
58061 | 83 |
| repair_quantification (SMTLIB.S l) = SMTLIB.S (map repair_quantification l) |
57762 | 84 |
| repair_quantification x = x |
57704 | 85 |
|
57708
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
86 |
fun replace_bound_var_by_free_var (q $ Abs (var, ty, u)) free_var = |
57705 | 87 |
(case List.find (fn v => String.isPrefix v var) free_var of |
57708
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
88 |
NONE => q $ Abs (var, ty, replace_bound_var_by_free_var u free_var) |
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
89 |
| SOME _ => replace_bound_var_by_free_var (Term.subst_bound (Free (var, ty), u)) free_var) |
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
90 |
| replace_bound_var_by_free_var (u $ v) free_vars = replace_bound_var_by_free_var u free_vars $ |
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
91 |
replace_bound_var_by_free_var v free_vars |
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
92 |
| replace_bound_var_by_free_var u _ = u |
57705 | 93 |
|
58490 | 94 |
fun find_type_in_formula (Abs (v, T, u)) var_name = |
95 |
if String.isPrefix var_name v then SOME T else find_type_in_formula u var_name |
|
57705 | 96 |
| find_type_in_formula (u $ v) var_name = |
97 |
(case find_type_in_formula u var_name of |
|
98 |
NONE => find_type_in_formula v var_name |
|
58490 | 99 |
| some_T => some_T) |
57705 | 100 |
| find_type_in_formula _ _ = NONE |
101 |
||
58490 | 102 |
fun add_bound_variables_to_ctxt concl = |
103 |
fold (update_binding o |
|
104 |
(fn s => (s, Term (Free (s, the_default dummyT (find_type_in_formula concl s)))))) |
|
57705 | 105 |
|
58490 | 106 |
fun update_step_and_cx (node as VeriT_Node {id, rule, prems, concl, bounds}) cx = |
57708
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
107 |
if rule = veriT_tmp_ite_elim_rule then |
58490 | 108 |
(mk_node id rule prems concl bounds, add_bound_variables_to_ctxt concl bounds cx) |
57713 | 109 |
else if rule = veriT_tmp_skolemize_rule then |
58490 | 110 |
let val concl' = replace_bound_var_by_free_var concl bounds in |
111 |
(mk_node id rule prems concl' [], add_bound_variables_to_ctxt concl bounds cx) |
|
57705 | 112 |
end |
113 |
else |
|
58490 | 114 |
(node, cx) |
57705 | 115 |
|
57712
3c4e6bc7455f
Simplifying the labels in the proof of the SMT solver veriT.
fleury
parents:
57710
diff
changeset
|
116 |
fun fix_subproof_steps ((((id_of_father_step, rule), prems), subproof), ((step_concl, bounds), |
57705 | 117 |
cx)) = |
118 |
let |
|
58490 | 119 |
fun mk_prop_of_term concl = |
120 |
concl |> fastype_of concl = @{typ bool} ? curry (op $) @{term Trueprop} |
|
61611
a9c0572109af
fixing premises in veriT proof reconstruction
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
59014
diff
changeset
|
121 |
fun update_prems assumption_id prems = |
a9c0572109af
fixing premises in veriT proof reconstruction
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
59014
diff
changeset
|
122 |
map (fn prem => id_of_father_step ^ prem) |
a9c0572109af
fixing premises in veriT proof reconstruction
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
59014
diff
changeset
|
123 |
(filter_out (curry (op =) assumption_id) prems) |
58490 | 124 |
fun inline_assumption assumption assumption_id |
61611
a9c0572109af
fixing premises in veriT proof reconstruction
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
59014
diff
changeset
|
125 |
(VeriT_Node {id, rule, prems, concl, bounds}) = |
a9c0572109af
fixing premises in veriT proof reconstruction
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
59014
diff
changeset
|
126 |
mk_node id rule (update_prems assumption_id prems) |
58493 | 127 |
(@{const Pure.imp} $ mk_prop_of_term assumption $ mk_prop_of_term concl) bounds |
57712
3c4e6bc7455f
Simplifying the labels in the proof of the SMT solver veriT.
fleury
parents:
57710
diff
changeset
|
128 |
fun find_input_steps_and_inline [] last_step = ([], last_step) |
57716 | 129 |
| find_input_steps_and_inline (VeriT_Node {id = id', rule, prems, concl, bounds} :: steps) |
57712
3c4e6bc7455f
Simplifying the labels in the proof of the SMT solver veriT.
fleury
parents:
57710
diff
changeset
|
130 |
last_step = |
57705 | 131 |
if rule = veriT_input_rule then |
57712
3c4e6bc7455f
Simplifying the labels in the proof of the SMT solver veriT.
fleury
parents:
57710
diff
changeset
|
132 |
find_input_steps_and_inline (map (inline_assumption concl id') steps) last_step |
57705 | 133 |
else |
57712
3c4e6bc7455f
Simplifying the labels in the proof of the SMT solver veriT.
fleury
parents:
57710
diff
changeset
|
134 |
apfst (cons (mk_node (id_of_father_step ^ id') rule prems concl bounds)) |
3c4e6bc7455f
Simplifying the labels in the proof of the SMT solver veriT.
fleury
parents:
57710
diff
changeset
|
135 |
(find_input_steps_and_inline steps (id_of_father_step ^ id')) |
57716 | 136 |
val (subproof', last_step_id) = find_input_steps_and_inline subproof "" |
57708
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
137 |
val prems' = |
58490 | 138 |
if last_step_id = "" then |
139 |
prems |
|
57708
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
140 |
else |
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
141 |
(case prems of |
57712
3c4e6bc7455f
Simplifying the labels in the proof of the SMT solver veriT.
fleury
parents:
57710
diff
changeset
|
142 |
NONE => SOME [last_step_id] |
3c4e6bc7455f
Simplifying the labels in the proof of the SMT solver veriT.
fleury
parents:
57710
diff
changeset
|
143 |
| SOME l => SOME (last_step_id :: l)) |
57705 | 144 |
in |
57712
3c4e6bc7455f
Simplifying the labels in the proof of the SMT solver veriT.
fleury
parents:
57710
diff
changeset
|
145 |
(subproof', (((((id_of_father_step, rule), prems'), step_concl), bounds), cx)) |
57705 | 146 |
end |
147 |
||
148 |
(* |
|
149 |
(set id rule :clauses(...) :args(..) :conclusion (...)). |
|
150 |
or |
|
151 |
(set id subproof (set ...) :conclusion (...)). |
|
152 |
*) |
|
153 |
||
57712
3c4e6bc7455f
Simplifying the labels in the proof of the SMT solver veriT.
fleury
parents:
57710
diff
changeset
|
154 |
fun parse_proof_step cx = |
57704 | 155 |
let |
156 |
fun rotate_pair (a, (b, c)) = ((a, b), c) |
|
58061 | 157 |
fun get_id (SMTLIB.S [SMTLIB.Sym "set", SMTLIB.Sym id, SMTLIB.S l]) = (id, l) |
58078
d44c9dc4bf30
took out one more occurrence of 'PolyML.makestring'
blanchet
parents:
58061
diff
changeset
|
158 |
| get_id t = raise Fail ("unrecognized VeriT proof " ^ @{make_string} t) |
58061 | 159 |
fun parse_rule (SMTLIB.Sym rule :: l) = (rule, l) |
160 |
fun parse_source (SMTLIB.Key "clauses" :: SMTLIB.S source ::l) = |
|
161 |
(SOME (map (fn (SMTLIB.Sym id) => id) source), l) |
|
57704 | 162 |
| parse_source l = (NONE, l) |
58061 | 163 |
fun parse_subproof cx id_of_father_step ((subproof_step as SMTLIB.S (SMTLIB.Sym "set" :: _)) :: l) = |
57712
3c4e6bc7455f
Simplifying the labels in the proof of the SMT solver veriT.
fleury
parents:
57710
diff
changeset
|
164 |
let val (subproof_steps, cx') = parse_proof_step cx subproof_step in |
3c4e6bc7455f
Simplifying the labels in the proof of the SMT solver veriT.
fleury
parents:
57710
diff
changeset
|
165 |
apfst (apfst (curry (op @) subproof_steps)) (parse_subproof cx' id_of_father_step l) |
57705 | 166 |
end |
57712
3c4e6bc7455f
Simplifying the labels in the proof of the SMT solver veriT.
fleury
parents:
57710
diff
changeset
|
167 |
| parse_subproof cx _ l = (([], cx), l) |
58061 | 168 |
fun skip_args (SMTLIB.Key "args" :: SMTLIB.S _ :: l) = l |
57704 | 169 |
| skip_args l = l |
58061 | 170 |
fun parse_conclusion (SMTLIB.Key "conclusion" :: SMTLIB.S concl :: []) = concl |
57704 | 171 |
fun make_or_from_clausification l = |
57708
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
172 |
foldl1 (fn ((concl1, bounds1), (concl2, bounds2)) => |
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
173 |
(HOLogic.mk_disj (perhaps (try HOLogic.dest_Trueprop) concl1, |
58490 | 174 |
perhaps (try HOLogic.dest_Trueprop) concl2), bounds1 @ bounds2)) l |
175 |
fun to_node (((((id, rule), prems), concl), bounds), cx) = |
|
176 |
(mk_node id rule (the_default [] prems) concl bounds, cx) |
|
57704 | 177 |
in |
178 |
get_id |
|
179 |
##> parse_rule |
|
180 |
#> rotate_pair |
|
181 |
##> parse_source |
|
182 |
#> rotate_pair |
|
183 |
##> skip_args |
|
57712
3c4e6bc7455f
Simplifying the labels in the proof of the SMT solver veriT.
fleury
parents:
57710
diff
changeset
|
184 |
#> (fn (((id, rule), prems), sub) => (((id, rule), prems), parse_subproof cx id sub)) |
57705 | 185 |
#> rotate_pair |
57704 | 186 |
##> parse_conclusion |
57762 | 187 |
##> map repair_quantification |
57705 | 188 |
#> (fn ((((id, rule), prems), (subproof, cx)), terms) => |
189 |
(((((id, rule), prems), subproof), fold_map (fn t => fn cx => node_of t cx) terms cx))) |
|
57762 | 190 |
##> apfst (fn [] => (@{const False}, []) | concls => make_or_from_clausification concls) |
57712
3c4e6bc7455f
Simplifying the labels in the proof of the SMT solver veriT.
fleury
parents:
57710
diff
changeset
|
191 |
#> fix_subproof_steps |
57705 | 192 |
##> to_node |
193 |
#> (fn (subproof, (step, cx)) => (subproof @ [step], cx)) |
|
57762 | 194 |
#-> fold_map update_step_and_cx |
57705 | 195 |
end |
196 |
||
57708
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
197 |
(*subproofs are written on multiple lines: SMTLIB can not parse then, because parentheses are |
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
198 |
unbalanced on each line*) |
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
199 |
fun seperate_into_steps lines = |
57705 | 200 |
let |
58490 | 201 |
fun count ("(" :: l) n = count l (n + 1) |
202 |
| count (")" :: l) n = count l (n - 1) |
|
57705 | 203 |
| count (_ :: l) n = count l n |
204 |
| count [] n = n |
|
205 |
fun seperate (line :: l) actual_lines m = |
|
206 |
let val n = count (raw_explode line) 0 in |
|
207 |
if m + n = 0 then |
|
208 |
[actual_lines ^ line] :: seperate l "" 0 |
|
58490 | 209 |
else |
210 |
seperate l (actual_lines ^ line) (m + n) |
|
57713 | 211 |
end |
57705 | 212 |
| seperate [] _ 0 = [] |
213 |
in |
|
214 |
seperate lines "" 0 |
|
57704 | 215 |
end |
216 |
||
58490 | 217 |
(* VeriT adds "@" before every variable. *) |
218 |
fun remove_all_at (SMTLIB.Sym v :: l) = |
|
219 |
SMTLIB.Sym (perhaps (try (unprefix "@")) v) :: remove_all_at l |
|
58061 | 220 |
| remove_all_at (SMTLIB.S l :: l') = SMTLIB.S (remove_all_at l) :: remove_all_at l' |
221 |
| remove_all_at (SMTLIB.Key v :: l) = SMTLIB.Key v :: remove_all_at l |
|
57705 | 222 |
| remove_all_at (v :: l) = v :: remove_all_at l |
223 |
| remove_all_at [] = [] |
|
224 |
||
57708
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
225 |
fun find_in_which_step_defined var (VeriT_Node {id, bounds, ...} :: l) = |
57705 | 226 |
(case List.find (fn v => String.isPrefix v var) bounds of |
57708
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
227 |
NONE => find_in_which_step_defined var l |
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
228 |
| SOME _ => id) |
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
229 |
| find_in_which_step_defined var _ = raise Fail ("undefined " ^ var) |
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
230 |
|
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
231 |
(*Yes every case is possible: the introduced var is not on a special size of the equality sign.*) |
58490 | 232 |
fun find_ite_var_in_term (Const (@{const_name If}, _) $ _ $ |
233 |
(Const (@{const_name HOL.eq}, _) $ Free (var1, _) $ Free (var2, _) ) $ |
|
234 |
(Const (@{const_name HOL.eq}, _) $ Free (var3, _) $ Free (var4, _) )) = |
|
57708
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
235 |
let |
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
236 |
fun get_number_of_ite_transformed_var var = |
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
237 |
perhaps (try (unprefix "ite")) var |
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
238 |
|> Int.fromString |
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
239 |
fun is_equal_and_has_correct_substring var var' var'' = |
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
240 |
if var = var' andalso String.isPrefix "ite" var then SOME var' |
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
241 |
else if var = var'' andalso String.isPrefix "ite" var then SOME var'' else NONE |
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
242 |
val var1_introduced_var = is_equal_and_has_correct_substring var1 var3 var4 |
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
243 |
val var2_introduced_var = is_equal_and_has_correct_substring var3 var1 var2 |
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
244 |
in |
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
245 |
(case (var1_introduced_var, var2_introduced_var) of |
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
246 |
(SOME a, SOME b) => |
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
247 |
(*ill-generated case, might be possible when applying the rule to max a a. Only if the |
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
248 |
variable have been introduced before. Probably an impossible edge case*) |
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
249 |
(case (get_number_of_ite_transformed_var a, get_number_of_ite_transformed_var b) of |
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
250 |
(SOME a, SOME b) => if a < b then var2_introduced_var else var1_introduced_var |
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
251 |
(*Otherwise, it is a name clase between a parameter name and the introduced variable. |
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
252 |
Or the name convention has been changed.*) |
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
253 |
| (NONE, SOME _) => var2_introduced_var |
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
254 |
| (SOME _, NONE) => var2_introduced_var) |
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
255 |
| (_, SOME _) => var2_introduced_var |
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
256 |
| (SOME _, _) => var1_introduced_var) |
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
257 |
end |
58490 | 258 |
| find_ite_var_in_term (Const (@{const_name If}, _) $ _ $ |
259 |
(Const (@{const_name HOL.eq}, _) $ Free (var, _) $ _ ) $ |
|
260 |
(Const (@{const_name HOL.eq}, _) $ Free (var', _) $ _ )) = |
|
57708
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
261 |
if var = var' then SOME var else NONE |
58490 | 262 |
| find_ite_var_in_term (Const (@{const_name If}, _) $ _ $ |
263 |
(Const (@{const_name HOL.eq}, _) $ _ $ Free (var, _)) $ |
|
264 |
(Const (@{const_name HOL.eq}, _) $ _ $ Free (var', _))) = |
|
57708
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
265 |
if var = var' then SOME var else NONE |
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
266 |
| find_ite_var_in_term (p $ q) = |
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
267 |
(case find_ite_var_in_term p of |
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
268 |
NONE => find_ite_var_in_term q |
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
269 |
| x => x) |
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
270 |
| find_ite_var_in_term (Abs (_, _, body)) = find_ite_var_in_term body |
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
271 |
| find_ite_var_in_term _ = NONE |
57705 | 272 |
|
58490 | 273 |
fun correct_veriT_step steps (node as VeriT_Node {id, rule, prems, concl, bounds}) = |
57714
4856a7b8b9c3
Changing the role of rule "tmp_ite_elim" of the SMT solver veriT to Lemma.
fleury
parents:
57713
diff
changeset
|
274 |
if rule = veriT_tmp_ite_elim_rule then |
57708
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
275 |
if bounds = [] then |
57762 | 276 |
(*if the introduced var has already been defined, adding the definition as a dependency*) |
57708
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
277 |
let |
58490 | 278 |
val new_prems = prems |
279 |
|> (case find_ite_var_in_term concl of |
|
280 |
NONE => I |
|
281 |
| SOME var => cons (find_in_which_step_defined var steps)) |
|
57708
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
282 |
in |
57716 | 283 |
VeriT_Node {id = id, rule = rule, prems = new_prems, concl = concl, bounds = bounds} |
57708
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
284 |
end |
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
285 |
else |
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
286 |
(*some new variables are created*) |
58490 | 287 |
let val concl' = replace_bound_var_by_free_var concl bounds in |
57715
cf8e4b1acd33
Skolemization for tmp_ite_elim rule in the SMT solver veriT.
fleury
parents:
57714
diff
changeset
|
288 |
mk_node id rule prems concl' [] |
57708
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
289 |
end |
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
290 |
else |
58490 | 291 |
node |
57708
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
292 |
|
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
293 |
fun remove_alpha_conversion _ [] = [] |
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
294 |
| remove_alpha_conversion replace_table (VeriT_Node {id, rule, prems, concl, bounds} :: steps) = |
57705 | 295 |
let |
58490 | 296 |
val correct_dependency = map (perhaps (Symtab.lookup replace_table)) |
297 |
val find_predecessor = perhaps (Symtab.lookup replace_table) |
|
57705 | 298 |
in |
59014 | 299 |
if rule = veriT_tmp_alphaconv_rule then |
57712
3c4e6bc7455f
Simplifying the labels in the proof of the SMT solver veriT.
fleury
parents:
57710
diff
changeset
|
300 |
remove_alpha_conversion (Symtab.update (id, find_predecessor (hd prems)) |
57708
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
301 |
replace_table) steps |
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
302 |
else |
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
303 |
VeriT_Node {id = id, rule = rule, prems = correct_dependency prems, |
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
304 |
concl = concl, bounds = bounds} :: remove_alpha_conversion replace_table steps |
57705 | 305 |
end |
306 |
||
57708
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
307 |
fun correct_veriT_steps steps = |
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
308 |
steps |
57712
3c4e6bc7455f
Simplifying the labels in the proof of the SMT solver veriT.
fleury
parents:
57710
diff
changeset
|
309 |
|> map (correct_veriT_step steps) |
57708
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
310 |
|> remove_alpha_conversion Symtab.empty |
57704 | 311 |
|
312 |
fun parse typs funs lines ctxt = |
|
313 |
let |
|
58061 | 314 |
val smtlib_lines_without_at = remove_all_at (map SMTLIB.parse (seperate_into_steps lines)) |
57712
3c4e6bc7455f
Simplifying the labels in the proof of the SMT solver veriT.
fleury
parents:
57710
diff
changeset
|
315 |
val (u, env) = apfst flat (fold_map (fn l => fn cx => parse_proof_step cx l) |
58061 | 316 |
smtlib_lines_without_at (empty_context ctxt typs funs)) |
57708
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
317 |
val t = correct_veriT_steps u |
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
318 |
fun node_to_step (VeriT_Node {id, rule, prems, concl, bounds, ...}) = |
57705 | 319 |
mk_step id rule prems concl bounds |
58490 | 320 |
in |
57705 | 321 |
(map node_to_step t, ctxt_of env) |
57704 | 322 |
end |
323 |
||
324 |
end; |