author | fleury |
Wed, 30 Jul 2014 14:03:13 +0200 | |
changeset 57714 | 4856a7b8b9c3 |
parent 57713 | 9e4d2f7ad0a0 |
child 57715 | cf8e4b1acd33 |
permissions | -rw-r--r-- |
57708
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
1 |
(* Title: HOL/Tools/SMT2/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 |
|
24 |
val veriT_rewrite_rule : string |
|
57714
4856a7b8b9c3
Changing the role of rule "tmp_ite_elim" of the SMT solver veriT to Lemma.
fleury
parents:
57713
diff
changeset
|
25 |
val veriT_tmp_skolemize_rule : string |
4856a7b8b9c3
Changing the role of rule "tmp_ite_elim" of the SMT solver veriT to Lemma.
fleury
parents:
57713
diff
changeset
|
26 |
val veriT_tmp_ite_elim_rule : string |
57704 | 27 |
end; |
28 |
||
29 |
structure VeriT_Proof: VERIT_PROOF = |
|
30 |
struct |
|
31 |
||
32 |
open SMTLIB2_Proof |
|
33 |
||
34 |
datatype veriT_node = VeriT_Node of { |
|
57712
3c4e6bc7455f
Simplifying the labels in the proof of the SMT solver veriT.
fleury
parents:
57710
diff
changeset
|
35 |
id: string, |
57704 | 36 |
rule: string, |
37 |
prems: string list, |
|
38 |
concl: term, |
|
39 |
bounds: string list} |
|
40 |
||
41 |
fun mk_node id rule prems concl bounds = |
|
42 |
VeriT_Node {id = id, rule = rule, prems = prems, concl = concl, bounds = bounds} |
|
43 |
||
44 |
datatype veriT_step = VeriT_Step of { |
|
57712
3c4e6bc7455f
Simplifying the labels in the proof of the SMT solver veriT.
fleury
parents:
57710
diff
changeset
|
45 |
id: string, |
57704 | 46 |
rule: string, |
47 |
prems: string list, |
|
48 |
concl: term, |
|
49 |
fixes: string list} |
|
50 |
||
51 |
fun mk_step id rule prems concl fixes = |
|
52 |
VeriT_Step {id = id, rule = rule, prems = prems, concl = concl, fixes = fixes} |
|
53 |
||
57705 | 54 |
val veriT_step_prefix = ".c" |
55 |
val veriT_input_rule = "input" |
|
56 |
val veriT_rewrite_rule = "__rewrite" (*arbitrary*) |
|
57708
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
57 |
val veriT_tmp_ite_elim_rule = "tmp_ite_elim" |
57713 | 58 |
val veriT_tmp_skolemize_rule = "tmp_skolemize" |
59 |
val veriT_alpha_conv_rule = "tmp_alphaconv" |
|
57708
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
60 |
|
57704 | 61 |
(* proof parser *) |
62 |
||
63 |
fun node_of p cx = |
|
64 |
([], cx) |
|
65 |
||>> with_fresh_names (term_of p) |
|
57712
3c4e6bc7455f
Simplifying the labels in the proof of the SMT solver veriT.
fleury
parents:
57710
diff
changeset
|
66 |
|>> (fn (_, (t, ns)) => (t, ns)) |
57704 | 67 |
|
68 |
(*in order to get Z3-style quantification*) |
|
69 |
fun fix_quantification (SMTLIB2.S (SMTLIB2.Sym "forall" :: l)) = |
|
57705 | 70 |
let val (quantified_vars, t) = split_last (map fix_quantification l) |
57704 | 71 |
in |
72 |
SMTLIB2.S (SMTLIB2.Sym "forall" :: SMTLIB2.S quantified_vars :: t :: []) |
|
73 |
end |
|
74 |
| fix_quantification (SMTLIB2.S (SMTLIB2.Sym "exists" :: l)) = |
|
75 |
let val (quantified_vars, t) = split_last (map fix_quantification l) |
|
76 |
in |
|
77 |
SMTLIB2.S (SMTLIB2.Sym "exists" :: SMTLIB2.S quantified_vars :: t :: []) |
|
78 |
end |
|
79 |
| fix_quantification (SMTLIB2.S l) = SMTLIB2.S (map fix_quantification l) |
|
80 |
| fix_quantification x = x |
|
81 |
||
57708
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
82 |
fun replace_bound_var_by_free_var (q $ Abs (var, ty, u)) free_var = |
57705 | 83 |
(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
|
84 |
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
|
85 |
| 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
|
86 |
| 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
|
87 |
replace_bound_var_by_free_var v free_vars |
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
88 |
| replace_bound_var_by_free_var u _ = u |
57705 | 89 |
|
57714
4856a7b8b9c3
Changing the role of rule "tmp_ite_elim" of the SMT solver veriT to Lemma.
fleury
parents:
57713
diff
changeset
|
90 |
fun replace_bound_all_by_ex ((q as Const (_, typ)) $ Abs (var, ty, u)) free_var = |
4856a7b8b9c3
Changing the role of rule "tmp_ite_elim" of the SMT solver veriT to Lemma.
fleury
parents:
57713
diff
changeset
|
91 |
(case List.find (fn v => String.isPrefix v var) free_var of |
4856a7b8b9c3
Changing the role of rule "tmp_ite_elim" of the SMT solver veriT to Lemma.
fleury
parents:
57713
diff
changeset
|
92 |
NONE => q $ Abs (var, ty, replace_bound_all_by_ex u free_var) |
4856a7b8b9c3
Changing the role of rule "tmp_ite_elim" of the SMT solver veriT to Lemma.
fleury
parents:
57713
diff
changeset
|
93 |
| SOME _ => Const (@{const_name "HOL.Ex"}, typ) $ Abs (var, ty, replace_bound_all_by_ex u free_var)) |
4856a7b8b9c3
Changing the role of rule "tmp_ite_elim" of the SMT solver veriT to Lemma.
fleury
parents:
57713
diff
changeset
|
94 |
| replace_bound_all_by_ex (u $ v) free_vars = replace_bound_all_by_ex u free_vars $ |
4856a7b8b9c3
Changing the role of rule "tmp_ite_elim" of the SMT solver veriT to Lemma.
fleury
parents:
57713
diff
changeset
|
95 |
replace_bound_all_by_ex v free_vars |
4856a7b8b9c3
Changing the role of rule "tmp_ite_elim" of the SMT solver veriT to Lemma.
fleury
parents:
57713
diff
changeset
|
96 |
| replace_bound_all_by_ex u _ = u |
4856a7b8b9c3
Changing the role of rule "tmp_ite_elim" of the SMT solver veriT to Lemma.
fleury
parents:
57713
diff
changeset
|
97 |
|
57705 | 98 |
fun find_type_in_formula (Abs(v, ty, u)) var_name = |
57708
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
99 |
if String.isPrefix var_name v then SOME ty else find_type_in_formula u var_name |
57705 | 100 |
| find_type_in_formula (u $ v) var_name = |
101 |
(case find_type_in_formula u var_name of |
|
102 |
NONE => find_type_in_formula v var_name |
|
103 |
| a => a) |
|
104 |
| find_type_in_formula _ _ = NONE |
|
105 |
||
57708
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
106 |
fun add_bound_variables_to_ctxt cx bounds concl = |
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
107 |
fold (fn a => fn b => update_binding a b) |
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
108 |
(map (fn s => ((s, Term (Free (s, the_default dummyT (find_type_in_formula concl s)))))) |
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
109 |
bounds) cx |
57705 | 110 |
|
57708
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
111 |
fun update_step_and_cx (st as VeriT_Node {id, rule, prems, concl, bounds}) cx = |
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
112 |
if rule = veriT_tmp_ite_elim_rule then |
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
113 |
(mk_node id rule prems concl bounds, add_bound_variables_to_ctxt cx bounds concl) |
57713 | 114 |
else if rule = veriT_tmp_skolemize_rule then |
57705 | 115 |
let |
57708
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
116 |
val concl' = replace_bound_var_by_free_var concl bounds |
57705 | 117 |
in |
57708
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
118 |
(mk_node id rule prems concl' [], add_bound_variables_to_ctxt cx bounds concl) |
57705 | 119 |
end |
120 |
else |
|
121 |
(st, cx) |
|
122 |
||
57708
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
123 |
(*FIXME: using a reference would be better to know th numbers of the steps to add*) |
57712
3c4e6bc7455f
Simplifying the labels in the proof of the SMT solver veriT.
fleury
parents:
57710
diff
changeset
|
124 |
fun fix_subproof_steps ((((id_of_father_step, rule), prems), subproof), ((step_concl, bounds), |
57705 | 125 |
cx)) = |
126 |
let |
|
57708
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
127 |
fun mk_prop_of_term concl = (fastype_of concl = @{typ "bool"} ? |
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
128 |
curry (op $) @{term "Trueprop"}) concl |
57705 | 129 |
fun inline_assumption assumption assumption_id (st as VeriT_Node {id, rule, prems, concl, |
130 |
bounds}) = |
|
131 |
if List.find (curry (op =) assumption_id) prems <> NONE then |
|
57712
3c4e6bc7455f
Simplifying the labels in the proof of the SMT solver veriT.
fleury
parents:
57710
diff
changeset
|
132 |
let |
3c4e6bc7455f
Simplifying the labels in the proof of the SMT solver veriT.
fleury
parents:
57710
diff
changeset
|
133 |
val prems' = filter_out (curry (op =) assumption_id) prems |
3c4e6bc7455f
Simplifying the labels in the proof of the SMT solver veriT.
fleury
parents:
57710
diff
changeset
|
134 |
in |
3c4e6bc7455f
Simplifying the labels in the proof of the SMT solver veriT.
fleury
parents:
57710
diff
changeset
|
135 |
mk_node id rule (filter_out (curry (op =) assumption_id) prems') |
3c4e6bc7455f
Simplifying the labels in the proof of the SMT solver veriT.
fleury
parents:
57710
diff
changeset
|
136 |
(Const (@{const_name "Pure.imp"}, @{typ "prop"} --> @{typ "prop"} --> @{typ "prop"}) |
3c4e6bc7455f
Simplifying the labels in the proof of the SMT solver veriT.
fleury
parents:
57710
diff
changeset
|
137 |
$ mk_prop_of_term assumption $ mk_prop_of_term concl) bounds |
3c4e6bc7455f
Simplifying the labels in the proof of the SMT solver veriT.
fleury
parents:
57710
diff
changeset
|
138 |
end |
57705 | 139 |
else |
140 |
st |
|
57712
3c4e6bc7455f
Simplifying the labels in the proof of the SMT solver veriT.
fleury
parents:
57710
diff
changeset
|
141 |
fun find_input_steps_and_inline [] last_step = ([], last_step) |
3c4e6bc7455f
Simplifying the labels in the proof of the SMT solver veriT.
fleury
parents:
57710
diff
changeset
|
142 |
| find_input_steps_and_inline (VeriT_Node {id = id', rule, prems, concl, bounds} :: steps) |
3c4e6bc7455f
Simplifying the labels in the proof of the SMT solver veriT.
fleury
parents:
57710
diff
changeset
|
143 |
last_step = |
57705 | 144 |
if rule = veriT_input_rule then |
57712
3c4e6bc7455f
Simplifying the labels in the proof of the SMT solver veriT.
fleury
parents:
57710
diff
changeset
|
145 |
find_input_steps_and_inline (map (inline_assumption concl id') steps) last_step |
57705 | 146 |
else |
57712
3c4e6bc7455f
Simplifying the labels in the proof of the SMT solver veriT.
fleury
parents:
57710
diff
changeset
|
147 |
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
|
148 |
(find_input_steps_and_inline steps (id_of_father_step ^ id')) |
3c4e6bc7455f
Simplifying the labels in the proof of the SMT solver veriT.
fleury
parents:
57710
diff
changeset
|
149 |
val (subproof', last_step_id) = find_input_steps_and_inline subproof "~1" |
57708
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
150 |
val prems' = |
57712
3c4e6bc7455f
Simplifying the labels in the proof of the SMT solver veriT.
fleury
parents:
57710
diff
changeset
|
151 |
if last_step_id = "~1" then prems |
57708
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
152 |
else |
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
153 |
(case prems of |
57712
3c4e6bc7455f
Simplifying the labels in the proof of the SMT solver veriT.
fleury
parents:
57710
diff
changeset
|
154 |
NONE => SOME [last_step_id] |
3c4e6bc7455f
Simplifying the labels in the proof of the SMT solver veriT.
fleury
parents:
57710
diff
changeset
|
155 |
| SOME l => SOME (last_step_id :: l)) |
57705 | 156 |
in |
57712
3c4e6bc7455f
Simplifying the labels in the proof of the SMT solver veriT.
fleury
parents:
57710
diff
changeset
|
157 |
(subproof', (((((id_of_father_step, rule), prems'), step_concl), bounds), cx)) |
57705 | 158 |
end |
159 |
||
160 |
(* |
|
161 |
(set id rule :clauses(...) :args(..) :conclusion (...)). |
|
162 |
or |
|
163 |
(set id subproof (set ...) :conclusion (...)). |
|
164 |
*) |
|
165 |
||
57712
3c4e6bc7455f
Simplifying the labels in the proof of the SMT solver veriT.
fleury
parents:
57710
diff
changeset
|
166 |
fun parse_proof_step cx = |
57704 | 167 |
let |
168 |
fun rotate_pair (a, (b, c)) = ((a, b), c) |
|
169 |
fun get_id (SMTLIB2.S [SMTLIB2.Sym "set", SMTLIB2.Sym id, SMTLIB2.S l]) = (id, l) |
|
170 |
| get_id t = raise Fail ("unrecognized VeriT Proof" ^ PolyML.makestring t) |
|
171 |
fun parse_rule (SMTLIB2.Sym rule :: l) = (rule, l) |
|
172 |
fun parse_source (SMTLIB2.Key "clauses" :: SMTLIB2.S source ::l) = |
|
173 |
(SOME (map (fn (SMTLIB2.Sym id) => id) source), l) |
|
174 |
| parse_source l = (NONE, l) |
|
57712
3c4e6bc7455f
Simplifying the labels in the proof of the SMT solver veriT.
fleury
parents:
57710
diff
changeset
|
175 |
fun parse_subproof cx id_of_father_step ((subproof_step as SMTLIB2.S (SMTLIB2.Sym "set" :: _)) :: l) = |
3c4e6bc7455f
Simplifying the labels in the proof of the SMT solver veriT.
fleury
parents:
57710
diff
changeset
|
176 |
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
|
177 |
apfst (apfst (curry (op @) subproof_steps)) (parse_subproof cx' id_of_father_step l) |
57705 | 178 |
end |
57712
3c4e6bc7455f
Simplifying the labels in the proof of the SMT solver veriT.
fleury
parents:
57710
diff
changeset
|
179 |
| parse_subproof cx _ l = (([], cx), l) |
57704 | 180 |
fun skip_args (SMTLIB2.Key "args" :: SMTLIB2.S _ :: l) = l |
181 |
| skip_args l = l |
|
57705 | 182 |
fun parse_conclusion (SMTLIB2.Key "conclusion" :: SMTLIB2.S concl :: []) = concl |
57704 | 183 |
fun make_or_from_clausification l = |
57708
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
184 |
foldl1 (fn ((concl1, bounds1), (concl2, bounds2)) => |
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
185 |
(HOLogic.mk_disj (perhaps (try HOLogic.dest_Trueprop) concl1, |
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
186 |
perhaps (try HOLogic.dest_Trueprop) concl2), bounds1 @ bounds2)) l |
57705 | 187 |
fun to_node (((((id, rule), prems), concl), bounds), cx) = (mk_node id rule |
57713 | 188 |
(the_default [] prems) concl bounds, cx) |
57704 | 189 |
in |
190 |
get_id |
|
191 |
##> parse_rule |
|
192 |
#> rotate_pair |
|
193 |
##> parse_source |
|
194 |
#> rotate_pair |
|
195 |
##> skip_args |
|
57712
3c4e6bc7455f
Simplifying the labels in the proof of the SMT solver veriT.
fleury
parents:
57710
diff
changeset
|
196 |
#> (fn (((id, rule), prems), sub) => (((id, rule), prems), parse_subproof cx id sub)) |
57705 | 197 |
#> rotate_pair |
57704 | 198 |
##> parse_conclusion |
199 |
##> map fix_quantification |
|
57705 | 200 |
#> (fn ((((id, rule), prems), (subproof, cx)), terms) => |
201 |
(((((id, rule), prems), subproof), fold_map (fn t => fn cx => node_of t cx) terms cx))) |
|
202 |
(*the conclusion is the empty list, ie no false is written, we have to add it.*) |
|
203 |
##> (apfst (fn [] => (@{const False}, []) |
|
204 |
| concls => make_or_from_clausification concls)) |
|
57712
3c4e6bc7455f
Simplifying the labels in the proof of the SMT solver veriT.
fleury
parents:
57710
diff
changeset
|
205 |
#> fix_subproof_steps |
57705 | 206 |
##> to_node |
207 |
#> (fn (subproof, (step, cx)) => (subproof @ [step], cx)) |
|
57714
4856a7b8b9c3
Changing the role of rule "tmp_ite_elim" of the SMT solver veriT to Lemma.
fleury
parents:
57713
diff
changeset
|
208 |
#> uncurry (fold_map update_step_and_cx) |
57705 | 209 |
end |
210 |
||
57708
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
211 |
|
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
212 |
(*function related to parsing and general transformation*) |
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
213 |
|
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
214 |
(*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
|
215 |
unbalanced on each line*) |
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
216 |
fun seperate_into_steps lines = |
57705 | 217 |
let |
218 |
fun count ("(" :: l) n = count l (n+1) |
|
219 |
| count (")" :: l) n = count l (n-1) |
|
220 |
| count (_ :: l) n = count l n |
|
221 |
| count [] n = n |
|
222 |
fun seperate (line :: l) actual_lines m = |
|
223 |
let val n = count (raw_explode line) 0 in |
|
224 |
if m + n = 0 then |
|
225 |
[actual_lines ^ line] :: seperate l "" 0 |
|
226 |
else seperate l (actual_lines ^ line) (m + n) |
|
57713 | 227 |
end |
57705 | 228 |
| seperate [] _ 0 = [] |
229 |
in |
|
230 |
seperate lines "" 0 |
|
57704 | 231 |
end |
232 |
||
57705 | 233 |
(*VeriT adds @ before every variable.*) |
234 |
fun remove_all_at (SMTLIB2.Sym v :: l) = |
|
235 |
SMTLIB2.Sym (if nth_string v 0 = "@" then String.extract (v, 1, NONE) else v) :: remove_all_at l |
|
236 |
| remove_all_at (SMTLIB2.S l :: l') = SMTLIB2.S (remove_all_at l) :: remove_all_at l' |
|
237 |
| remove_all_at (SMTLIB2.Key v :: l) = SMTLIB2.Key v :: remove_all_at l |
|
238 |
| remove_all_at (v :: l) = v :: remove_all_at l |
|
239 |
| remove_all_at [] = [] |
|
240 |
||
57708
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
241 |
fun find_in_which_step_defined var (VeriT_Node {id, bounds, ...} :: l) = |
57705 | 242 |
(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
|
243 |
NONE => find_in_which_step_defined var l |
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
244 |
| SOME _ => id) |
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
245 |
| 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
|
246 |
|
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
247 |
(*Yes every case is possible: the introduced var is not on a special size of the equality sign.*) |
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
248 |
fun find_ite_var_in_term (Const ("HOL.If", _) $ _ $ |
57714
4856a7b8b9c3
Changing the role of rule "tmp_ite_elim" of the SMT solver veriT to Lemma.
fleury
parents:
57713
diff
changeset
|
249 |
(Const (@{const_name "HOL.eq"}, _) $ Free (var1, _) $ Free (var2, _) ) $ |
4856a7b8b9c3
Changing the role of rule "tmp_ite_elim" of the SMT solver veriT to Lemma.
fleury
parents:
57713
diff
changeset
|
250 |
(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
|
251 |
let |
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
252 |
fun get_number_of_ite_transformed_var var = |
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
253 |
perhaps (try (unprefix "ite")) var |
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
254 |
|> Int.fromString |
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
255 |
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
|
256 |
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
|
257 |
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
|
258 |
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
|
259 |
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
|
260 |
in |
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
261 |
(case (var1_introduced_var, var2_introduced_var) of |
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
262 |
(SOME a, SOME b) => |
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
263 |
(*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
|
264 |
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
|
265 |
(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
|
266 |
(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
|
267 |
(*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
|
268 |
Or the name convention has been changed.*) |
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
269 |
| (NONE, SOME _) => var2_introduced_var |
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
270 |
| (SOME _, NONE) => var2_introduced_var) |
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
271 |
| (_, SOME _) => var2_introduced_var |
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
272 |
| (SOME _, _) => var1_introduced_var) |
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
273 |
end |
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
274 |
| find_ite_var_in_term (Const (@{const_name "If"}, _) $ _ $ |
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
275 |
(Const (@{const_name "HOL.eq"}, _) $ Free (var, _) $ _ ) $ |
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
276 |
(Const (@{const_name "HOL.eq"}, _) $ Free (var', _) $ _ )) = |
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
277 |
if var = var' then SOME var else NONE |
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
278 |
| find_ite_var_in_term (Const (@{const_name "If"}, _) $ _ $ |
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
279 |
(Const (@{const_name "HOL.eq"}, _) $ _ $ Free (var, _)) $ |
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
280 |
(Const (@{const_name "HOL.eq"}, _) $ _ $ Free (var', _))) = |
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
281 |
if var = var' then SOME var else NONE |
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
282 |
| find_ite_var_in_term (p $ q) = |
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
283 |
(case find_ite_var_in_term p of |
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
284 |
NONE => find_ite_var_in_term q |
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
285 |
| x => x) |
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
286 |
| 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
|
287 |
| find_ite_var_in_term _ = NONE |
57705 | 288 |
|
289 |
||
57712
3c4e6bc7455f
Simplifying the labels in the proof of the SMT solver veriT.
fleury
parents:
57710
diff
changeset
|
290 |
fun correct_veriT_step steps (st 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
|
291 |
if rule = veriT_tmp_ite_elim_rule then |
57708
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
292 |
if bounds = [] then |
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
293 |
(*if the introduced var has already been defined, |
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
294 |
adding the definition as a dependency*) |
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
295 |
let |
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
296 |
val SOME var = find_ite_var_in_term concl |
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
297 |
val new_dep = find_in_which_step_defined var steps |
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
298 |
in |
57712
3c4e6bc7455f
Simplifying the labels in the proof of the SMT solver veriT.
fleury
parents:
57710
diff
changeset
|
299 |
VeriT_Node {id = id, rule = rule, prems = new_dep :: prems, concl = concl, bounds = bounds} |
57708
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
300 |
end |
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
301 |
else |
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
302 |
(*some new variables are created*) |
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
303 |
let |
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
304 |
val concl' = replace_bound_var_by_free_var concl bounds |
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
305 |
in |
57713 | 306 |
mk_node id veriT_tmp_skolemize_rule prems concl' [] |
57708
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
307 |
end |
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
308 |
else |
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
309 |
st |
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
310 |
|
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
311 |
(*remove alpha conversion step, that just renames the variables*) |
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
312 |
fun remove_alpha_conversion _ [] = [] |
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
313 |
| remove_alpha_conversion replace_table (VeriT_Node {id, rule, prems, concl, bounds} :: steps) = |
57705 | 314 |
let |
57708
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
315 |
fun correct_dependency prems = |
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
316 |
map (fn x => perhaps (Symtab.lookup replace_table) x) prems |
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
317 |
fun find_predecessor prem = perhaps (Symtab.lookup replace_table) prem |
57705 | 318 |
in |
57713 | 319 |
if rule = veriT_alpha_conv_rule then |
57712
3c4e6bc7455f
Simplifying the labels in the proof of the SMT solver veriT.
fleury
parents:
57710
diff
changeset
|
320 |
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
|
321 |
replace_table) steps |
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
322 |
else |
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
323 |
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
|
324 |
concl = concl, bounds = bounds} :: remove_alpha_conversion replace_table steps |
57705 | 325 |
end |
326 |
||
57708
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
327 |
fun correct_veriT_steps steps = |
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
328 |
steps |
57712
3c4e6bc7455f
Simplifying the labels in the proof of the SMT solver veriT.
fleury
parents:
57710
diff
changeset
|
329 |
|> map (correct_veriT_step steps) |
57708
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
330 |
|> remove_alpha_conversion Symtab.empty |
57704 | 331 |
|
332 |
(* overall proof parser *) |
|
333 |
fun parse typs funs lines ctxt = |
|
334 |
let |
|
57708
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
335 |
val smtlib2_lines_without_at = |
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
336 |
remove_all_at (map SMTLIB2.parse (seperate_into_steps lines)) |
57712
3c4e6bc7455f
Simplifying the labels in the proof of the SMT solver veriT.
fleury
parents:
57710
diff
changeset
|
337 |
val (u, env) = apfst flat (fold_map (fn l => fn cx => parse_proof_step cx l) |
57714
4856a7b8b9c3
Changing the role of rule "tmp_ite_elim" of the SMT solver veriT to Lemma.
fleury
parents:
57713
diff
changeset
|
338 |
smtlib2_lines_without_at (empty_context ctxt typs funs)) |
57708
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
339 |
val t = correct_veriT_steps u |
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
340 |
fun node_to_step (VeriT_Node {id, rule, prems, concl, bounds, ...}) = |
57705 | 341 |
mk_step id rule prems concl bounds |
342 |
in |
|
343 |
(map node_to_step t, ctxt_of env) |
|
57704 | 344 |
end |
345 |
||
346 |
end; |