author | fleury <Mathias.Fleury@mpi-inf.mpg.de> |
Tue, 30 Oct 2018 16:24:04 +0100 | |
changeset 69205 | 8050734eee3e |
parent 61611 | a9c0572109af |
child 69593 | 3dda49e08b9d |
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, |
|
69205
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
15 |
proof_ctxt: term list, |
57704 | 16 |
concl: term, |
17 |
fixes: string list} |
|
18 |
||
69205
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
19 |
datatype veriT_replay_node = VeriT_Replay_Node of { |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
20 |
id: string, |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
21 |
rule: string, |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
22 |
args: term list, |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
23 |
prems: string list, |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
24 |
proof_ctxt: term list, |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
25 |
concl: term, |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
26 |
bounds: (string * typ) list, |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
27 |
subproof: (string * typ) list * term list * veriT_replay_node list} |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
28 |
|
57704 | 29 |
(*proof parser*) |
30 |
val parse: typ Symtab.table -> term Symtab.table -> string list -> |
|
31 |
Proof.context -> veriT_step list * Proof.context |
|
69205
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
32 |
val parse_replay: typ Symtab.table -> term Symtab.table -> string list -> |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
33 |
Proof.context -> veriT_replay_node list * Proof.context |
57704 | 34 |
|
69205
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
35 |
val map_replay_prems: (string list -> string list) -> veriT_replay_node -> veriT_replay_node |
57705 | 36 |
val veriT_step_prefix : string |
37 |
val veriT_input_rule: string |
|
69205
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
38 |
val veriT_normalized_input_rule: string |
57762 | 39 |
val veriT_la_generic_rule : string |
57705 | 40 |
val veriT_rewrite_rule : string |
57762 | 41 |
val veriT_simp_arith_rule : string |
57714
4856a7b8b9c3
Changing the role of rule "tmp_ite_elim" of the SMT solver veriT to Lemma.
fleury
parents:
57713
diff
changeset
|
42 |
val veriT_tmp_skolemize_rule : string |
69205
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
43 |
val veriT_subproof_rule : string |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
44 |
val veriT_local_input_rule : string |
57704 | 45 |
end; |
46 |
||
47 |
structure VeriT_Proof: VERIT_PROOF = |
|
48 |
struct |
|
49 |
||
58061 | 50 |
open SMTLIB_Proof |
57704 | 51 |
|
69205
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
52 |
datatype raw_veriT_node = Raw_VeriT_Node of { |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
53 |
id: string, |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
54 |
rule: string, |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
55 |
args: SMTLIB.tree, |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
56 |
prems: string list, |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
57 |
concl: SMTLIB.tree, |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
58 |
subproof: raw_veriT_node list} |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
59 |
|
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
60 |
fun mk_raw_node id rule args prems concl subproof = |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
61 |
Raw_VeriT_Node {id = id, rule = rule, args = args, prems = prems, concl = concl, |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
62 |
subproof = subproof} |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
63 |
|
57704 | 64 |
datatype veriT_node = VeriT_Node of { |
57712
3c4e6bc7455f
Simplifying the labels in the proof of the SMT solver veriT.
fleury
parents:
57710
diff
changeset
|
65 |
id: string, |
57704 | 66 |
rule: string, |
67 |
prems: string list, |
|
69205
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
68 |
proof_ctxt: term list, |
57704 | 69 |
concl: term, |
70 |
bounds: string list} |
|
71 |
||
69205
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
72 |
fun mk_node id rule prems proof_ctxt concl bounds = |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
73 |
VeriT_Node {id = id, rule = rule, prems = prems, proof_ctxt = proof_ctxt, concl = concl, |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
74 |
bounds = bounds} |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
75 |
|
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
76 |
datatype veriT_replay_node = VeriT_Replay_Node of { |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
77 |
id: string, |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
78 |
rule: string, |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
79 |
args: term list, |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
80 |
prems: string list, |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
81 |
proof_ctxt: term list, |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
82 |
concl: term, |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
83 |
bounds: (string * typ) list, |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
84 |
subproof: (string * typ) list * term list * veriT_replay_node list} |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
85 |
|
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
86 |
fun mk_replay_node id rule args prems proof_ctxt concl bounds subproof = |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
87 |
VeriT_Replay_Node {id = id, rule = rule, args = args, prems = prems, proof_ctxt = proof_ctxt, |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
88 |
concl = concl, bounds = bounds, subproof = subproof} |
57704 | 89 |
|
90 |
datatype veriT_step = VeriT_Step of { |
|
57712
3c4e6bc7455f
Simplifying the labels in the proof of the SMT solver veriT.
fleury
parents:
57710
diff
changeset
|
91 |
id: string, |
57704 | 92 |
rule: string, |
93 |
prems: string list, |
|
69205
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
94 |
proof_ctxt: term list, |
57704 | 95 |
concl: term, |
96 |
fixes: string list} |
|
97 |
||
69205
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
98 |
fun mk_step id rule prems proof_ctxt concl fixes = |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
99 |
VeriT_Step {id = id, rule = rule, prems = prems, proof_ctxt = proof_ctxt, concl = concl, |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
100 |
fixes = fixes} |
57704 | 101 |
|
57705 | 102 |
val veriT_step_prefix = ".c" |
103 |
val veriT_input_rule = "input" |
|
57762 | 104 |
val veriT_la_generic_rule = "la_generic" |
69205
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
105 |
val veriT_normalized_input_rule = "__normalized_input" (* arbitrary *) |
57762 | 106 |
val veriT_rewrite_rule = "__rewrite" (* arbitrary *) |
69205
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
107 |
val veriT_subproof_rule = "subproof" |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
108 |
val veriT_local_input_rule = "__local_input" (* arbitrary *) |
57762 | 109 |
val veriT_simp_arith_rule = "simp_arith" |
69205
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
110 |
|
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
111 |
(* Even the veriT developer do not know if the following rule can still appear in proofs: *) |
57713 | 112 |
val veriT_tmp_skolemize_rule = "tmp_skolemize" |
57708
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
113 |
|
57704 | 114 |
(* proof parser *) |
115 |
||
116 |
fun node_of p cx = |
|
117 |
([], cx) |
|
57747 | 118 |
||>> `(with_fresh_names (term_of p)) |
57716 | 119 |
|>> snd |
57704 | 120 |
|
58490 | 121 |
fun find_type_in_formula (Abs (v, T, u)) var_name = |
122 |
if String.isPrefix var_name v then SOME T else find_type_in_formula u var_name |
|
57705 | 123 |
| find_type_in_formula (u $ v) var_name = |
124 |
(case find_type_in_formula u var_name of |
|
125 |
NONE => find_type_in_formula v var_name |
|
58490 | 126 |
| some_T => some_T) |
69205
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
127 |
| find_type_in_formula (Free(v, T)) var_name = |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
128 |
if String.isPrefix var_name v then SOME T else NONE |
57705 | 129 |
| find_type_in_formula _ _ = NONE |
130 |
||
69205
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
131 |
fun find_type_of_free_in_formula (Free (v, T) $ u) var_name = |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
132 |
if String.isPrefix var_name v then SOME T else find_type_in_formula u var_name |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
133 |
| find_type_of_free_in_formula (Abs (v, T, u)) var_name = |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
134 |
if String.isPrefix var_name v then SOME T else find_type_in_formula u var_name |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
135 |
| find_type_of_free_in_formula (u $ v) var_name = |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
136 |
(case find_type_in_formula u var_name of |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
137 |
NONE => find_type_in_formula v var_name |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
138 |
| some_T => some_T) |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
139 |
| find_type_of_free_in_formula _ _ = NONE |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
140 |
|
58490 | 141 |
fun add_bound_variables_to_ctxt concl = |
142 |
fold (update_binding o |
|
143 |
(fn s => (s, Term (Free (s, the_default dummyT (find_type_in_formula concl s)))))) |
|
57705 | 144 |
|
69205
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
145 |
|
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
146 |
local |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
147 |
|
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
148 |
fun remove_Sym (SMTLIB.Sym y) = y |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
149 |
|
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
150 |
fun extract_symbols bds = |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
151 |
bds |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
152 |
|> map (fn SMTLIB.S [SMTLIB.Key _, SMTLIB.Sym x, SMTLIB.Sym y] => [x, y] |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
153 |
| SMTLIB.S syms => map remove_Sym syms) |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
154 |
|> flat |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
155 |
|
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
156 |
fun extract_symbols_map bds = |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
157 |
bds |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
158 |
|> map (fn SMTLIB.S [SMTLIB.Key _, SMTLIB.Sym x, _] => [x] |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
159 |
| SMTLIB.S syms => map remove_Sym syms) |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
160 |
|> flat |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
161 |
in |
57705 | 162 |
|
69205
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
163 |
fun bound_vars_by_rule "bind" (SMTLIB.S bds) = extract_symbols bds |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
164 |
| bound_vars_by_rule "qnt_simplify" (SMTLIB.S bds) = extract_symbols_map bds |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
165 |
| bound_vars_by_rule "sko_forall" (SMTLIB.S bds) = extract_symbols_map bds |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
166 |
| bound_vars_by_rule "sko_ex" (SMTLIB.S bds) = extract_symbols_map bds |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
167 |
| bound_vars_by_rule _ _ = [] |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
168 |
|
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
169 |
fun global_bound_vars_by_rule _ _ = [] |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
170 |
|
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
171 |
(* VeriT adds "?" before some variable. *) |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
172 |
fun remove_all_qm (SMTLIB.Sym v :: l) = |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
173 |
SMTLIB.Sym (perhaps (try (unprefix "?")) v) :: remove_all_qm l |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
174 |
| remove_all_qm (SMTLIB.S l :: l') = SMTLIB.S (remove_all_qm l) :: remove_all_qm l' |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
175 |
| remove_all_qm (SMTLIB.Key v :: l) = SMTLIB.Key v :: remove_all_qm l |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
176 |
| remove_all_qm (v :: l) = v :: remove_all_qm l |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
177 |
| remove_all_qm [] = [] |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
178 |
|
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
179 |
fun remove_all_qm2 (SMTLIB.Sym v) = SMTLIB.Sym (perhaps (try (unprefix "?")) v) |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
180 |
| remove_all_qm2 (SMTLIB.S l) = SMTLIB.S (remove_all_qm l) |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
181 |
| remove_all_qm2 (SMTLIB.Key v) = SMTLIB.Key v |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
182 |
| remove_all_qm2 v = v |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
183 |
|
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
184 |
val parse_rule_and_args = |
57705 | 185 |
let |
69205
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
186 |
fun parse_rule_name (SMTLIB.Sym rule :: l) = (rule, l) |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
187 |
| parse_rule_name l = (veriT_subproof_rule, l) |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
188 |
fun parse_args (SMTLIB.Key "args" :: args :: l) = (remove_all_qm2 args, l) |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
189 |
| parse_args l = (SMTLIB.S [], l) |
57705 | 190 |
in |
69205
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
191 |
parse_rule_name |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
192 |
##> parse_args |
57705 | 193 |
end |
194 |
||
69205
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
195 |
end |
57705 | 196 |
|
69205
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
197 |
fun parse_raw_proof_step (p : SMTLIB.tree) : raw_veriT_node = |
57704 | 198 |
let |
199 |
fun rotate_pair (a, (b, c)) = ((a, b), c) |
|
58061 | 200 |
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
|
201 |
| get_id t = raise Fail ("unrecognized VeriT proof " ^ @{make_string} t) |
58061 | 202 |
fun parse_source (SMTLIB.Key "clauses" :: SMTLIB.S source ::l) = |
203 |
(SOME (map (fn (SMTLIB.Sym id) => id) source), l) |
|
57704 | 204 |
| parse_source l = (NONE, l) |
69205
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
205 |
fun parse_subproof rule args id_of_father_step ((subproof_step as SMTLIB.S (SMTLIB.Sym "set" :: _)) :: l) = |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
206 |
let |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
207 |
val subproof_steps = parse_raw_proof_step subproof_step |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
208 |
in |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
209 |
apfst (curry (op ::) subproof_steps) (parse_subproof rule args id_of_father_step l) |
57705 | 210 |
end |
69205
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
211 |
| parse_subproof _ _ _ l = ([], l) |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
212 |
|
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
213 |
fun parse_and_clausify_conclusion (SMTLIB.Key "conclusion" :: SMTLIB.S [] :: []) = |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
214 |
SMTLIB.Sym "false" |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
215 |
| parse_and_clausify_conclusion (SMTLIB.Key "conclusion" :: SMTLIB.S concl :: []) = |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
216 |
(SMTLIB.S (remove_all_qm (SMTLIB.Sym "or" :: concl))) |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
217 |
|
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
218 |
fun to_raw_node ((((((id, rule), args), prems), subproof), concl)) = |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
219 |
(mk_raw_node id rule args (the_default [] prems) concl subproof) |
57704 | 220 |
in |
69205
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
221 |
(get_id |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
222 |
##> parse_rule_and_args |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
223 |
#> rotate_pair |
57704 | 224 |
#> rotate_pair |
225 |
##> parse_source |
|
226 |
#> rotate_pair |
|
69205
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
227 |
#> (fn ((((id, rule), args), prems), sub) => |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
228 |
((((id, rule), args), prems), parse_subproof rule args id sub)) |
57705 | 229 |
#> rotate_pair |
69205
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
230 |
##> parse_and_clausify_conclusion |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
231 |
#> to_raw_node) |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
232 |
p |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
233 |
end |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
234 |
|
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
235 |
fun proof_ctxt_of_rule "bind" t = t |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
236 |
| proof_ctxt_of_rule "sko_forall" t = t |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
237 |
| proof_ctxt_of_rule "sko_ex" t = t |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
238 |
| proof_ctxt_of_rule "let" t = t |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
239 |
| proof_ctxt_of_rule "qnt_simplify" t = t |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
240 |
| proof_ctxt_of_rule _ _ = [] |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
241 |
|
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
242 |
fun args_of_rule "forall_inst" t = t |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
243 |
| args_of_rule _ _ = [] |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
244 |
|
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
245 |
fun map_replay_prems f (VeriT_Replay_Node {id, rule, args, prems, proof_ctxt, concl, bounds, |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
246 |
subproof = (bound, assms, subproof)}) = |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
247 |
(VeriT_Replay_Node {id = id, rule = rule, args = args, prems = f prems, proof_ctxt = proof_ctxt, |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
248 |
concl = concl, bounds = bounds, subproof = (bound, assms, map (map_replay_prems f) subproof)}) |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
249 |
|
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
250 |
fun map_replay_id f (VeriT_Replay_Node {id, rule, args, prems, proof_ctxt, concl, bounds, |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
251 |
subproof = (bound, assms, subproof)}) = |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
252 |
(VeriT_Replay_Node {id = f id, rule = rule, args = args, prems = prems, proof_ctxt = proof_ctxt, |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
253 |
concl = concl, bounds = bounds, subproof = (bound, assms, map (map_replay_id f) subproof)}) |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
254 |
|
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
255 |
fun id_of_last_step prems = |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
256 |
if null prems then [] |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
257 |
else |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
258 |
let val VeriT_Replay_Node {id, ...} = List.last prems in [id] end |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
259 |
|
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
260 |
val extract_assumptions_from_subproof = |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
261 |
let fun extract_assumptions_from_subproof (VeriT_Replay_Node {rule, concl, ...}) = |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
262 |
if rule = veriT_local_input_rule then [concl] else [] |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
263 |
in |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
264 |
map extract_assumptions_from_subproof |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
265 |
#> flat |
57705 | 266 |
end |
267 |
||
69205
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
268 |
fun normalized_rule_name id rule = |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
269 |
(case (rule = veriT_input_rule, can (unprefix SMTLIB_Interface.assert_prefix) id) of |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
270 |
(true, true) => veriT_normalized_input_rule |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
271 |
| (true, _) => veriT_local_input_rule |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
272 |
| _ => rule) |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
273 |
|
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
274 |
fun is_assm_repetition id rule = |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
275 |
rule = veriT_input_rule andalso can (unprefix SMTLIB_Interface.assert_prefix) id |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
276 |
|
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
277 |
fun postprocess_proof ctxt step = |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
278 |
let fun postprocess (Raw_VeriT_Node {id = id, rule = rule, args = args, |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
279 |
prems = prems, concl = concl, subproof = subproof}) cx = |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
280 |
let |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
281 |
val ((concl, bounds), cx') = node_of concl cx |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
282 |
|
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
283 |
val bound_vars = bound_vars_by_rule rule args |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
284 |
|
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
285 |
(* postprocess conclusion *) |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
286 |
val new_global_bounds = global_bound_vars_by_rule rule args |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
287 |
val concl = SMTLIB_Isar.unskolemize_names ctxt concl |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
288 |
|
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
289 |
val _ = (SMT_Config.veriT_msg ctxt) (fn () => @{print} ("id =", id, "concl =", concl)) |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
290 |
val _ = (SMT_Config.veriT_msg ctxt) (fn () => @{print} ("id =", id, "cx' =", cx', |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
291 |
"bound_vars =", bound_vars)) |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
292 |
val bound_vars = filter_out (member ((op =)) new_global_bounds) bound_vars |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
293 |
val bound_tvars = |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
294 |
map (fn s => (s, the (find_type_in_formula concl s))) bound_vars |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
295 |
val subproof_cx = add_bound_variables_to_ctxt concl bound_vars cx |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
296 |
val (p : veriT_replay_node list list, _) = |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
297 |
fold_map postprocess subproof subproof_cx |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
298 |
|
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
299 |
(* postprocess assms *) |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
300 |
val SMTLIB.S stripped_args = args |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
301 |
val sanitized_args = |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
302 |
proof_ctxt_of_rule rule stripped_args |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
303 |
|> map |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
304 |
(fn SMTLIB.S [SMTLIB.Key "=", x, y] => SMTLIB.S [SMTLIB.Sym "=", x, y] |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
305 |
| SMTLIB.S syms => |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
306 |
SMTLIB.S (SMTLIB.Sym "and" :: map (fn x => SMTLIB.S [SMTLIB.Sym "=", x, x]) syms) |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
307 |
| x => x) |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
308 |
val (termified_args, _) = fold_map node_of sanitized_args subproof_cx |> apfst (map fst) |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
309 |
val normalized_args = map (SMTLIB_Isar.unskolemize_names ctxt) termified_args |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
310 |
|
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
311 |
val subproof_assms = proof_ctxt_of_rule rule normalized_args |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
312 |
|
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
313 |
(* postprocess arguments *) |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
314 |
val rule_args = args_of_rule rule stripped_args |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
315 |
val (termified_args, _) = fold_map term_of rule_args subproof_cx |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
316 |
val normalized_args = map (SMTLIB_Isar.unskolemize_names ctxt) termified_args |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
317 |
val rule_args = normalized_args |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
318 |
|
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
319 |
(* fix subproof *) |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
320 |
val p = flat p |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
321 |
val p = map (map_replay_prems (map (curry (op ^) id))) p |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
322 |
val p = map (map_replay_id (curry (op ^) id)) p |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
323 |
|
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
324 |
val extra_assms2 = |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
325 |
(if rule = veriT_subproof_rule then extract_assumptions_from_subproof p else []) |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
326 |
|
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
327 |
(* fix step *) |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
328 |
val bound_t = |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
329 |
bounds |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
330 |
|> map (fn s => (s, the_default dummyT (find_type_of_free_in_formula concl s))) |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
331 |
val fixed_prems = |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
332 |
(if null subproof then prems else map (curry (op ^) id) prems) @ |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
333 |
(if is_assm_repetition id rule then [id] else []) @ |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
334 |
id_of_last_step p |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
335 |
val normalized_rule = normalized_rule_name id rule |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
336 |
val step = mk_replay_node id normalized_rule rule_args fixed_prems subproof_assms concl |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
337 |
bound_t (bound_tvars, subproof_assms @ extra_assms2, p) |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
338 |
in |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
339 |
([step], cx') |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
340 |
end |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
341 |
in postprocess step end |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
342 |
|
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
343 |
|
57708
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
344 |
(*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
|
345 |
unbalanced on each line*) |
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
346 |
fun seperate_into_steps lines = |
57705 | 347 |
let |
58490 | 348 |
fun count ("(" :: l) n = count l (n + 1) |
349 |
| count (")" :: l) n = count l (n - 1) |
|
57705 | 350 |
| count (_ :: l) n = count l n |
351 |
| count [] n = n |
|
352 |
fun seperate (line :: l) actual_lines m = |
|
353 |
let val n = count (raw_explode line) 0 in |
|
354 |
if m + n = 0 then |
|
355 |
[actual_lines ^ line] :: seperate l "" 0 |
|
58490 | 356 |
else |
357 |
seperate l (actual_lines ^ line) (m + n) |
|
57713 | 358 |
end |
57705 | 359 |
| seperate [] _ 0 = [] |
360 |
in |
|
361 |
seperate lines "" 0 |
|
57704 | 362 |
end |
363 |
||
69205
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
364 |
fun unprefix_all_syms c (SMTLIB.Sym v :: l) = |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
365 |
SMTLIB.Sym (perhaps (try (unprefix c)) v) :: unprefix_all_syms c l |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
366 |
| unprefix_all_syms c (SMTLIB.S l :: l') = SMTLIB.S (unprefix_all_syms c l) :: unprefix_all_syms c l' |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
367 |
| unprefix_all_syms c (SMTLIB.Key v :: l) = SMTLIB.Key v :: unprefix_all_syms c l |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
368 |
| unprefix_all_syms c (v :: l) = v :: unprefix_all_syms c l |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
369 |
| unprefix_all_syms _ [] = [] |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
370 |
|
58490 | 371 |
(* VeriT adds "@" before every variable. *) |
69205
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
372 |
val remove_all_ats = unprefix_all_syms "@" |
57705 | 373 |
|
69205
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
374 |
val linearize_proof = |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
375 |
let |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
376 |
fun linearize (VeriT_Replay_Node {id = id, rule = rule, args = _, prems = prems, |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
377 |
proof_ctxt = proof_ctxt, concl = concl, bounds = bounds, subproof = (_, _, subproof)}) = |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
378 |
let |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
379 |
fun mk_prop_of_term concl = |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
380 |
concl |> fastype_of concl = @{typ bool} ? curry (op $) @{term Trueprop} |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
381 |
fun remove_assumption_id assumption_id prems = |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
382 |
filter_out (curry (op =) assumption_id) prems |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
383 |
fun inline_assumption assumption assumption_id |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
384 |
(VeriT_Node {id, rule, prems, proof_ctxt, concl, bounds}) = |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
385 |
mk_node id rule (remove_assumption_id assumption_id prems) proof_ctxt |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
386 |
(@{const Pure.imp} $ mk_prop_of_term assumption $ mk_prop_of_term concl) bounds |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
387 |
fun find_input_steps_and_inline [] = [] |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
388 |
| find_input_steps_and_inline |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
389 |
(VeriT_Node {id = id', rule, prems, concl, bounds, ...} :: steps) = |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
390 |
if rule = veriT_input_rule then |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
391 |
find_input_steps_and_inline (map (inline_assumption concl id') steps) |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
392 |
else |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
393 |
mk_node (id') rule prems [] concl bounds :: find_input_steps_and_inline steps |
57708
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
394 |
|
69205
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
395 |
val subproof = flat (map linearize subproof) |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
396 |
val subproof' = find_input_steps_and_inline subproof |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
397 |
in |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
398 |
subproof' @ [mk_node id rule prems proof_ctxt concl (map fst bounds)] |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
399 |
end |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
400 |
in linearize end |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
401 |
|
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
402 |
local |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
403 |
fun import_proof_and_post_process typs funs lines ctxt = |
57708
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
404 |
let |
69205
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
405 |
val smtlib_lines_without_at = |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
406 |
seperate_into_steps lines |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
407 |
|> map SMTLIB.parse |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
408 |
|> remove_all_ats |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
409 |
in apfst flat (fold_map (fn l => postprocess_proof ctxt (parse_raw_proof_step l)) |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
410 |
smtlib_lines_without_at (empty_context ctxt typs funs)) end |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
411 |
in |
57704 | 412 |
|
413 |
fun parse typs funs lines ctxt = |
|
414 |
let |
|
69205
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
415 |
val (u, env) = import_proof_and_post_process typs funs lines ctxt |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
416 |
val t = flat (map linearize_proof u) |
57708
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
417 |
fun node_to_step (VeriT_Node {id, rule, prems, concl, bounds, ...}) = |
69205
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
418 |
mk_step id rule prems [] concl bounds |
58490 | 419 |
in |
57705 | 420 |
(map node_to_step t, ctxt_of env) |
57704 | 421 |
end |
422 |
||
69205
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
423 |
fun parse_replay typs funs lines ctxt = |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
424 |
let |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
425 |
val (u, env) = import_proof_and_post_process typs funs lines ctxt |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
426 |
val _ = (SMT_Config.veriT_msg ctxt) (fn () => @{print} u) |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
427 |
in |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
428 |
(u, ctxt_of env) |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
429 |
end |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
430 |
end |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
61611
diff
changeset
|
431 |
|
57704 | 432 |
end; |