author | blanchet |
Thu, 28 Aug 2014 16:58:27 +0200 | |
changeset 58084 | 9f77084444df |
parent 58043 | a90847f03ec8 |
child 58325 | 3b16fe3d9ad6 |
permissions | -rw-r--r-- |
57706 | 1 |
(* Title: HOL/Tools/ATP/atp_satallax.ML |
2 |
Author: Mathias Fleury, ENS Rennes |
|
3 |
Author: Jasmin Blanchette, TU Muenchen |
|
4 |
||
5 |
Satallax proof parser and transformation for Sledgehammer. |
|
6 |
*) |
|
7 |
||
8 |
signature ATP_SATALLAX = |
|
9 |
sig |
|
10 |
val atp_proof_of_tstplike_proof : string -> string ATP_Proof.atp_problem -> string -> |
|
11 |
string ATP_Proof.atp_proof |
|
12 |
end; |
|
13 |
||
14 |
structure ATP_Satallax : ATP_SATALLAX = |
|
15 |
struct |
|
16 |
||
17 |
open ATP_Proof |
|
18 |
open ATP_Util |
|
19 |
open ATP_Problem |
|
20 |
||
21 |
(*Undocumented format: |
|
22 |
thf (number, plain | Axiom | ..., inference(rule, [status(thm), assumptions ([hypotheses list]), |
|
23 |
detailed_rule(discharge,used_hypothese_list) *], used_hypotheses_list, premises)) |
|
24 |
(seen by tab_mat) |
|
25 |
||
26 |
Also seen -- but we can ignore it: |
|
27 |
"tab_inh (a) __11." meaning that the type a is inhabited usueful of variable eigen__11, |
|
28 |
*) |
|
29 |
fun parse_satallax_tstp_information x = |
|
30 |
((Symbol.scan_ascii_id || ($$ "$" |-- Symbol.scan_ascii_id)) |
|
31 |
-- Scan.option ( $$ "(" |-- Scan.option (Symbol.scan_ascii_id --| $$ ",") |
|
32 |
-- ((Scan.option (($$ "[" |-- (Scan.option ((scan_general_id |
|
57716 | 33 |
-- Scan.repeat ($$ "," |-- scan_general_id)) >> op ::) --| $$ "]")) |
57710
323a57d7455c
imported patch satallax_skolemization_in_tree_part
fleury
parents:
57707
diff
changeset
|
34 |
|| (skip_term >> K "") >> (fn x => SOME [x])) |
323a57d7455c
imported patch satallax_skolemization_in_tree_part
fleury
parents:
57707
diff
changeset
|
35 |
>> (fn (SOME x) => x | NONE => NONE)) --| $$ ")"))) x |
57706 | 36 |
|
37 |
fun parse_prem x = |
|
38 |
((Symbol.scan_ascii_id || scan_general_id) --| Scan.option ($$ ":" -- skip_term)) x |
|
39 |
||
40 |
fun parse_prems x = |
|
41 |
(($$ "[" |-- parse_prem -- Scan.repeat ($$ "," |-- parse_prem) --| $$ "]") |
|
57716 | 42 |
>> op ::) x |
57706 | 43 |
|
44 |
fun parse_tstp_satallax_extra_arguments x = |
|
45 |
($$ "," |-- scan_general_id -- (($$ "(" |-- Symbol.scan_ascii_id --| $$ "," ) |
|
46 |
-- ($$ "[" |-- Scan.option ((parse_satallax_tstp_information |
|
57716 | 47 |
-- Scan.repeat ($$ "," |-- parse_satallax_tstp_information)) >> op ::) |
57706 | 48 |
--| $$ "]") -- |
49 |
(Scan.optional ($$ "," |-- parse_prems) [] -- Scan.optional ($$ "," |-- parse_prems) [] |
|
50 |
>> (fn (x, []) => x | (_, x) => x)) |
|
51 |
--| $$ ")")) x |
|
52 |
||
53 |
val dummy_satallax_step = ((("~1", "tab_inh"), AAtom (ATerm(("False", []), []))), NONE) |
|
54 |
fun parse_tstp_thf0_satallax_line x = |
|
55 |
(((Scan.this_string tptp_thf |
|
56 |
-- $$ "(") |-- scan_general_id --| $$ "," -- Symbol.scan_ascii_id --| $$ "," |
|
57 |
-- parse_thf0_formula -- Scan.option parse_tstp_satallax_extra_arguments --| $$ ")" --| $$ ".") |
|
58 |
|| (Scan.this_string "tab_inh" |-- skip_term --| $$ ".") |
|
59 |
>> K dummy_satallax_step) x |
|
60 |
||
61 |
datatype satallax_step = Satallax_Step of { |
|
62 |
id: string, |
|
63 |
role: string, |
|
64 |
theorem: (string, string, (string, string ATP_Problem.atp_type) ATP_Problem.atp_term, string) |
|
65 |
ATP_Problem.atp_formula, |
|
66 |
assumptions: string list, |
|
67 |
rule: string, |
|
68 |
used_assumptions: string list, |
|
57710
323a57d7455c
imported patch satallax_skolemization_in_tree_part
fleury
parents:
57707
diff
changeset
|
69 |
detailed_eigen: string, |
57706 | 70 |
generated_goal_assumptions: (string * string list) list} |
71 |
||
72 |
fun mk_satallax_step id role theorem assumptions rule used_assumptions |
|
57710
323a57d7455c
imported patch satallax_skolemization_in_tree_part
fleury
parents:
57707
diff
changeset
|
73 |
generated_goal_assumptions detailed_eigen = |
323a57d7455c
imported patch satallax_skolemization_in_tree_part
fleury
parents:
57707
diff
changeset
|
74 |
Satallax_Step {id = id, role = role, theorem = theorem, assumptions = assumptions, rule = rule, |
323a57d7455c
imported patch satallax_skolemization_in_tree_part
fleury
parents:
57707
diff
changeset
|
75 |
used_assumptions = used_assumptions, generated_goal_assumptions = generated_goal_assumptions, |
323a57d7455c
imported patch satallax_skolemization_in_tree_part
fleury
parents:
57707
diff
changeset
|
76 |
detailed_eigen = detailed_eigen} |
57706 | 77 |
|
78 |
fun get_assumptions (("assumptions", SOME (_ , assumptions)) :: _) = |
|
79 |
the_default [] assumptions |
|
80 |
| get_assumptions (_ :: l) = get_assumptions l |
|
81 |
| get_assumptions [] = [] |
|
82 |
||
57710
323a57d7455c
imported patch satallax_skolemization_in_tree_part
fleury
parents:
57707
diff
changeset
|
83 |
fun get_detailled_eigen ((_, SOME (SOME "eigenvar" , var)) :: _) = |
323a57d7455c
imported patch satallax_skolemization_in_tree_part
fleury
parents:
57707
diff
changeset
|
84 |
hd (the_default [""] var) |
323a57d7455c
imported patch satallax_skolemization_in_tree_part
fleury
parents:
57707
diff
changeset
|
85 |
| get_detailled_eigen (_ :: l) = get_detailled_eigen l |
323a57d7455c
imported patch satallax_skolemization_in_tree_part
fleury
parents:
57707
diff
changeset
|
86 |
| get_detailled_eigen [] = "" |
323a57d7455c
imported patch satallax_skolemization_in_tree_part
fleury
parents:
57707
diff
changeset
|
87 |
|
57706 | 88 |
fun seperate_dependices dependencies = |
57710
323a57d7455c
imported patch satallax_skolemization_in_tree_part
fleury
parents:
57707
diff
changeset
|
89 |
let |
323a57d7455c
imported patch satallax_skolemization_in_tree_part
fleury
parents:
57707
diff
changeset
|
90 |
fun sep_dep [] used_assumptions new_goals generated_assumptions _ = |
323a57d7455c
imported patch satallax_skolemization_in_tree_part
fleury
parents:
57707
diff
changeset
|
91 |
(used_assumptions, new_goals, generated_assumptions) |
323a57d7455c
imported patch satallax_skolemization_in_tree_part
fleury
parents:
57707
diff
changeset
|
92 |
| sep_dep (x :: l) used_assumptions new_goals generated_assumptions state = |
323a57d7455c
imported patch satallax_skolemization_in_tree_part
fleury
parents:
57707
diff
changeset
|
93 |
if hd (raw_explode x) = "h" orelse Int.fromString x = NONE then |
323a57d7455c
imported patch satallax_skolemization_in_tree_part
fleury
parents:
57707
diff
changeset
|
94 |
if state = 0 then |
323a57d7455c
imported patch satallax_skolemization_in_tree_part
fleury
parents:
57707
diff
changeset
|
95 |
sep_dep l (x :: used_assumptions) new_goals generated_assumptions state |
57706 | 96 |
else |
57710
323a57d7455c
imported patch satallax_skolemization_in_tree_part
fleury
parents:
57707
diff
changeset
|
97 |
sep_dep l used_assumptions new_goals (x :: generated_assumptions) 3 |
323a57d7455c
imported patch satallax_skolemization_in_tree_part
fleury
parents:
57707
diff
changeset
|
98 |
else |
323a57d7455c
imported patch satallax_skolemization_in_tree_part
fleury
parents:
57707
diff
changeset
|
99 |
if state = 1 orelse state = 0 then |
323a57d7455c
imported patch satallax_skolemization_in_tree_part
fleury
parents:
57707
diff
changeset
|
100 |
sep_dep l used_assumptions (x :: new_goals) generated_assumptions 1 |
323a57d7455c
imported patch satallax_skolemization_in_tree_part
fleury
parents:
57707
diff
changeset
|
101 |
else |
58043 | 102 |
raise Fail ("incorrect Satallax proof: " ^ @{make_string} l) |
57710
323a57d7455c
imported patch satallax_skolemization_in_tree_part
fleury
parents:
57707
diff
changeset
|
103 |
in |
323a57d7455c
imported patch satallax_skolemization_in_tree_part
fleury
parents:
57707
diff
changeset
|
104 |
sep_dep dependencies [] [] [] 0 |
323a57d7455c
imported patch satallax_skolemization_in_tree_part
fleury
parents:
57707
diff
changeset
|
105 |
end |
57706 | 106 |
|
107 |
fun create_grouped_goal_assumption rule new_goals generated_assumptions = |
|
57714
4856a7b8b9c3
Changing the role of rule "tmp_ite_elim" of the SMT solver veriT to Lemma.
fleury
parents:
57710
diff
changeset
|
108 |
let |
4856a7b8b9c3
Changing the role of rule "tmp_ite_elim" of the SMT solver veriT to Lemma.
fleury
parents:
57710
diff
changeset
|
109 |
val number_of_new_goals = length new_goals |
4856a7b8b9c3
Changing the role of rule "tmp_ite_elim" of the SMT solver veriT to Lemma.
fleury
parents:
57710
diff
changeset
|
110 |
val number_of_new_assms = length generated_assumptions |
4856a7b8b9c3
Changing the role of rule "tmp_ite_elim" of the SMT solver veriT to Lemma.
fleury
parents:
57710
diff
changeset
|
111 |
in |
4856a7b8b9c3
Changing the role of rule "tmp_ite_elim" of the SMT solver veriT to Lemma.
fleury
parents:
57710
diff
changeset
|
112 |
if number_of_new_goals = number_of_new_assms then |
4856a7b8b9c3
Changing the role of rule "tmp_ite_elim" of the SMT solver veriT to Lemma.
fleury
parents:
57710
diff
changeset
|
113 |
new_goals ~~ (map single generated_assumptions) |
4856a7b8b9c3
Changing the role of rule "tmp_ite_elim" of the SMT solver veriT to Lemma.
fleury
parents:
57710
diff
changeset
|
114 |
else if 2 * number_of_new_goals = number_of_new_assms then |
4856a7b8b9c3
Changing the role of rule "tmp_ite_elim" of the SMT solver veriT to Lemma.
fleury
parents:
57710
diff
changeset
|
115 |
let |
4856a7b8b9c3
Changing the role of rule "tmp_ite_elim" of the SMT solver veriT to Lemma.
fleury
parents:
57710
diff
changeset
|
116 |
fun group_by_pair (new_goal :: new_goals) (assumpt1 :: assumpt2 :: generated_assumptions) = |
4856a7b8b9c3
Changing the role of rule "tmp_ite_elim" of the SMT solver veriT to Lemma.
fleury
parents:
57710
diff
changeset
|
117 |
(new_goal, [assumpt1, assumpt2]) :: group_by_pair new_goals generated_assumptions |
4856a7b8b9c3
Changing the role of rule "tmp_ite_elim" of the SMT solver veriT to Lemma.
fleury
parents:
57710
diff
changeset
|
118 |
| group_by_pair [] [] = [] |
4856a7b8b9c3
Changing the role of rule "tmp_ite_elim" of the SMT solver veriT to Lemma.
fleury
parents:
57710
diff
changeset
|
119 |
in |
4856a7b8b9c3
Changing the role of rule "tmp_ite_elim" of the SMT solver veriT to Lemma.
fleury
parents:
57710
diff
changeset
|
120 |
group_by_pair new_goals generated_assumptions |
4856a7b8b9c3
Changing the role of rule "tmp_ite_elim" of the SMT solver veriT to Lemma.
fleury
parents:
57710
diff
changeset
|
121 |
end |
4856a7b8b9c3
Changing the role of rule "tmp_ite_elim" of the SMT solver veriT to Lemma.
fleury
parents:
57710
diff
changeset
|
122 |
else |
4856a7b8b9c3
Changing the role of rule "tmp_ite_elim" of the SMT solver veriT to Lemma.
fleury
parents:
57710
diff
changeset
|
123 |
raise Fail ("the rule " ^ rule ^" is not supported in the reconstruction.") |
4856a7b8b9c3
Changing the role of rule "tmp_ite_elim" of the SMT solver veriT to Lemma.
fleury
parents:
57710
diff
changeset
|
124 |
end |
57706 | 125 |
fun to_satallax_step (((id, role), formula), (SOME (_,((rule, l), used_rules)))) = |
126 |
let |
|
127 |
val (used_assumptions, new_goals, generated_assumptions) = seperate_dependices used_rules |
|
128 |
in |
|
129 |
mk_satallax_step id role formula (get_assumptions (the_default [] l)) rule used_assumptions |
|
130 |
(create_grouped_goal_assumption rule new_goals generated_assumptions) |
|
57710
323a57d7455c
imported patch satallax_skolemization_in_tree_part
fleury
parents:
57707
diff
changeset
|
131 |
(get_detailled_eigen (the_default [] l)) |
57706 | 132 |
end |
133 |
| to_satallax_step (((id, role), formula), NONE) = |
|
57710
323a57d7455c
imported patch satallax_skolemization_in_tree_part
fleury
parents:
57707
diff
changeset
|
134 |
mk_satallax_step id role formula [] "assumption" [] [] "" |
57706 | 135 |
|
136 |
fun is_assumption (Satallax_Step {role, ...}) = role = "assumption" orelse role = "axiom" orelse |
|
137 |
role = "negated_conjecture" orelse role = "conjecture" |
|
138 |
||
139 |
fun seperate_assumptions_and_steps l = |
|
57710
323a57d7455c
imported patch satallax_skolemization_in_tree_part
fleury
parents:
57707
diff
changeset
|
140 |
let |
323a57d7455c
imported patch satallax_skolemization_in_tree_part
fleury
parents:
57707
diff
changeset
|
141 |
fun seperate_assumption [] l l' = (l, l') |
323a57d7455c
imported patch satallax_skolemization_in_tree_part
fleury
parents:
57707
diff
changeset
|
142 |
| seperate_assumption (step :: steps) l l' = |
323a57d7455c
imported patch satallax_skolemization_in_tree_part
fleury
parents:
57707
diff
changeset
|
143 |
if is_assumption step then |
323a57d7455c
imported patch satallax_skolemization_in_tree_part
fleury
parents:
57707
diff
changeset
|
144 |
seperate_assumption steps (step :: l) l' |
323a57d7455c
imported patch satallax_skolemization_in_tree_part
fleury
parents:
57707
diff
changeset
|
145 |
else |
323a57d7455c
imported patch satallax_skolemization_in_tree_part
fleury
parents:
57707
diff
changeset
|
146 |
seperate_assumption steps l (step :: l') |
323a57d7455c
imported patch satallax_skolemization_in_tree_part
fleury
parents:
57707
diff
changeset
|
147 |
in |
323a57d7455c
imported patch satallax_skolemization_in_tree_part
fleury
parents:
57707
diff
changeset
|
148 |
seperate_assumption l [] [] |
323a57d7455c
imported patch satallax_skolemization_in_tree_part
fleury
parents:
57707
diff
changeset
|
149 |
end |
57706 | 150 |
|
151 |
datatype satallax_proof_graph = |
|
57710
323a57d7455c
imported patch satallax_skolemization_in_tree_part
fleury
parents:
57707
diff
changeset
|
152 |
Linear_Part of {node: satallax_step, succs: satallax_proof_graph list} | |
323a57d7455c
imported patch satallax_skolemization_in_tree_part
fleury
parents:
57707
diff
changeset
|
153 |
Tree_Part of {node: satallax_step, deps: satallax_proof_graph list} |
57706 | 154 |
|
155 |
fun find_proof_step ((x as Satallax_Step {id, ...}) :: l) h = |
|
156 |
if h = id then x else find_proof_step l h |
|
58043 | 157 |
| find_proof_step [] h = raise Fail ("not_found: " ^ @{make_string} h ^ " (probably a parsing \ |
57710
323a57d7455c
imported patch satallax_skolemization_in_tree_part
fleury
parents:
57707
diff
changeset
|
158 |
\error)") |
57706 | 159 |
|
160 |
fun remove_not_not (x as ATerm ((op1, _), [ATerm ((op2, _), [th])])) = |
|
161 |
if op1 = op2 andalso op1 = tptp_not then th else x |
|
162 |
| remove_not_not th = th |
|
163 |
||
164 |
fun tptp_term_equal (ATerm((op1, _), l1), ATerm((op2, _), l2)) = op1 = op2 andalso |
|
165 |
fold2 (fn t1 => fn t2 => fn c => c andalso t1 = t2) l1 l2 true |
|
166 |
| tptp_term_equal (_, _) = false |
|
167 |
||
57710
323a57d7455c
imported patch satallax_skolemization_in_tree_part
fleury
parents:
57707
diff
changeset
|
168 |
val dummy_true_aterm = ATerm (("$true", [dummy_atype]), []) |
323a57d7455c
imported patch satallax_skolemization_in_tree_part
fleury
parents:
57707
diff
changeset
|
169 |
|
57706 | 170 |
fun find_assumptions_to_inline ths (assm :: assms) to_inline no_inline = |
171 |
(case List.find (curry (op =) assm o fst) no_inline of |
|
172 |
SOME _ => find_assumptions_to_inline ths assms to_inline no_inline |
|
173 |
| NONE => |
|
174 |
(case List.find (curry (op =) assm o fst) to_inline of |
|
175 |
NONE => find_assumptions_to_inline ths assms to_inline no_inline |
|
176 |
| SOME (_, th) => |
|
177 |
let |
|
178 |
val simplified_ths_with_inlined_assumption = |
|
57714
4856a7b8b9c3
Changing the role of rule "tmp_ite_elim" of the SMT solver veriT to Lemma.
fleury
parents:
57710
diff
changeset
|
179 |
(case List.partition (curry tptp_term_equal th o remove_not_not) ths of |
4856a7b8b9c3
Changing the role of rule "tmp_ite_elim" of the SMT solver veriT to Lemma.
fleury
parents:
57710
diff
changeset
|
180 |
([], ths) => ATerm ((tptp_not, [dummy_atype]), [th]) :: ths |
4856a7b8b9c3
Changing the role of rule "tmp_ite_elim" of the SMT solver veriT to Lemma.
fleury
parents:
57710
diff
changeset
|
181 |
| (_, _) => []) |
57706 | 182 |
in |
183 |
find_assumptions_to_inline simplified_ths_with_inlined_assumption assms to_inline no_inline |
|
184 |
end)) |
|
185 |
| find_assumptions_to_inline ths [] _ _ = ths |
|
186 |
||
187 |
fun inline_if_needed_and_simplify th assms to_inline no_inline = |
|
57707
0242e9578828
imported patch satallax_proof_support_Sledgehammer
fleury
parents:
57706
diff
changeset
|
188 |
(case find_assumptions_to_inline [th] assms to_inline no_inline of |
57710
323a57d7455c
imported patch satallax_skolemization_in_tree_part
fleury
parents:
57707
diff
changeset
|
189 |
[] => dummy_true_aterm |
323a57d7455c
imported patch satallax_skolemization_in_tree_part
fleury
parents:
57707
diff
changeset
|
190 |
| l => foldl1 (fn (a, b) => |
323a57d7455c
imported patch satallax_skolemization_in_tree_part
fleury
parents:
57707
diff
changeset
|
191 |
(case b of |
323a57d7455c
imported patch satallax_skolemization_in_tree_part
fleury
parents:
57707
diff
changeset
|
192 |
ATerm (("$false", _), _) => a |
323a57d7455c
imported patch satallax_skolemization_in_tree_part
fleury
parents:
57707
diff
changeset
|
193 |
| ATerm (("~", _ ), [ATerm (("$true", _), _)]) => a |
323a57d7455c
imported patch satallax_skolemization_in_tree_part
fleury
parents:
57707
diff
changeset
|
194 |
| _ => ATerm ((tptp_or, [dummy_atype]), [a, b]))) l) |
57706 | 195 |
|
196 |
fun get_conclusion (Satallax_Step {theorem = AAtom theorem, ...}) = theorem |
|
197 |
||
57710
323a57d7455c
imported patch satallax_skolemization_in_tree_part
fleury
parents:
57707
diff
changeset
|
198 |
fun add_assumption new_used_assumptions ((Satallax_Step {id, role, theorem, assumptions, |
323a57d7455c
imported patch satallax_skolemization_in_tree_part
fleury
parents:
57707
diff
changeset
|
199 |
rule, generated_goal_assumptions, used_assumptions, detailed_eigen})) = |
323a57d7455c
imported patch satallax_skolemization_in_tree_part
fleury
parents:
57707
diff
changeset
|
200 |
mk_satallax_step id role theorem assumptions rule (new_used_assumptions @ used_assumptions) |
323a57d7455c
imported patch satallax_skolemization_in_tree_part
fleury
parents:
57707
diff
changeset
|
201 |
generated_goal_assumptions detailed_eigen |
57706 | 202 |
|
203 |
fun set_rule new_rule (Satallax_Step {id, role, theorem, assumptions, |
|
57710
323a57d7455c
imported patch satallax_skolemization_in_tree_part
fleury
parents:
57707
diff
changeset
|
204 |
generated_goal_assumptions, used_assumptions, detailed_eigen, ...}) = |
323a57d7455c
imported patch satallax_skolemization_in_tree_part
fleury
parents:
57707
diff
changeset
|
205 |
mk_satallax_step id role theorem assumptions new_rule used_assumptions |
323a57d7455c
imported patch satallax_skolemization_in_tree_part
fleury
parents:
57707
diff
changeset
|
206 |
generated_goal_assumptions detailed_eigen |
57706 | 207 |
|
208 |
fun transform_inline_assumption hypotheses_step proof_sketch = |
|
209 |
let |
|
57710
323a57d7455c
imported patch satallax_skolemization_in_tree_part
fleury
parents:
57707
diff
changeset
|
210 |
fun inline_in_step (Linear_Part {node as Satallax_Step {generated_goal_assumptions, |
323a57d7455c
imported patch satallax_skolemization_in_tree_part
fleury
parents:
57707
diff
changeset
|
211 |
used_assumptions, rule, ...}, succs}) = |
57706 | 212 |
if generated_goal_assumptions = [] then |
57714
4856a7b8b9c3
Changing the role of rule "tmp_ite_elim" of the SMT solver veriT to Lemma.
fleury
parents:
57710
diff
changeset
|
213 |
Linear_Part {node = node, succs = []} |
57706 | 214 |
else |
215 |
let |
|
216 |
(*one singel goal is created, two hypothesis can be created, for the "and" rule: |
|
217 |
(A /\ B) create two hypotheses A, and B.*) |
|
218 |
fun set_hypotheses_as_goal [hypothesis] succs = |
|
57710
323a57d7455c
imported patch satallax_skolemization_in_tree_part
fleury
parents:
57707
diff
changeset
|
219 |
Linear_Part {node = set_rule rule (add_assumption used_assumptions |
323a57d7455c
imported patch satallax_skolemization_in_tree_part
fleury
parents:
57707
diff
changeset
|
220 |
(find_proof_step hypotheses_step hypothesis)), |
57706 | 221 |
succs = map inline_in_step succs} |
222 |
| set_hypotheses_as_goal (hypothesis :: new_goal_hypotheses) succs = |
|
57710
323a57d7455c
imported patch satallax_skolemization_in_tree_part
fleury
parents:
57707
diff
changeset
|
223 |
Linear_Part {node = set_rule rule (add_assumption used_assumptions |
323a57d7455c
imported patch satallax_skolemization_in_tree_part
fleury
parents:
57707
diff
changeset
|
224 |
(find_proof_step hypotheses_step hypothesis)), |
57706 | 225 |
succs = [set_hypotheses_as_goal new_goal_hypotheses succs]} |
226 |
in |
|
227 |
set_hypotheses_as_goal (snd (hd generated_goal_assumptions)) succs |
|
228 |
end |
|
57710
323a57d7455c
imported patch satallax_skolemization_in_tree_part
fleury
parents:
57707
diff
changeset
|
229 |
| inline_in_step (Tree_Part {node = node, deps}) = |
323a57d7455c
imported patch satallax_skolemization_in_tree_part
fleury
parents:
57707
diff
changeset
|
230 |
Tree_Part {node = node, deps = map inline_in_step deps} |
57706 | 231 |
|
57710
323a57d7455c
imported patch satallax_skolemization_in_tree_part
fleury
parents:
57707
diff
changeset
|
232 |
fun inline_contradictory_assumptions (Linear_Part {node as Satallax_Step{id, theorem, ...}, |
323a57d7455c
imported patch satallax_skolemization_in_tree_part
fleury
parents:
57707
diff
changeset
|
233 |
succs}) (to_inline, no_inline) = |
323a57d7455c
imported patch satallax_skolemization_in_tree_part
fleury
parents:
57707
diff
changeset
|
234 |
let |
57714
4856a7b8b9c3
Changing the role of rule "tmp_ite_elim" of the SMT solver veriT to Lemma.
fleury
parents:
57710
diff
changeset
|
235 |
val (succs, inliner) = fold_map inline_contradictory_assumptions succs |
4856a7b8b9c3
Changing the role of rule "tmp_ite_elim" of the SMT solver veriT to Lemma.
fleury
parents:
57710
diff
changeset
|
236 |
(to_inline, (id, theorem) :: no_inline) |
57710
323a57d7455c
imported patch satallax_skolemization_in_tree_part
fleury
parents:
57707
diff
changeset
|
237 |
in |
323a57d7455c
imported patch satallax_skolemization_in_tree_part
fleury
parents:
57707
diff
changeset
|
238 |
(Linear_Part {node = node, succs = succs}, inliner) |
323a57d7455c
imported patch satallax_skolemization_in_tree_part
fleury
parents:
57707
diff
changeset
|
239 |
end |
323a57d7455c
imported patch satallax_skolemization_in_tree_part
fleury
parents:
57707
diff
changeset
|
240 |
| inline_contradictory_assumptions (Tree_Part {node = Satallax_Step {id, role, |
323a57d7455c
imported patch satallax_skolemization_in_tree_part
fleury
parents:
57707
diff
changeset
|
241 |
theorem = AAtom theorem, assumptions, rule, generated_goal_assumptions, |
323a57d7455c
imported patch satallax_skolemization_in_tree_part
fleury
parents:
57707
diff
changeset
|
242 |
used_assumptions, detailed_eigen}, deps}) (to_inline, no_inline) = |
323a57d7455c
imported patch satallax_skolemization_in_tree_part
fleury
parents:
57707
diff
changeset
|
243 |
let |
57714
4856a7b8b9c3
Changing the role of rule "tmp_ite_elim" of the SMT solver veriT to Lemma.
fleury
parents:
57710
diff
changeset
|
244 |
val (dep', (to_inline', no_inline')) = fold_map inline_contradictory_assumptions deps |
4856a7b8b9c3
Changing the role of rule "tmp_ite_elim" of the SMT solver veriT to Lemma.
fleury
parents:
57710
diff
changeset
|
245 |
(to_inline, no_inline) |
57710
323a57d7455c
imported patch satallax_skolemization_in_tree_part
fleury
parents:
57707
diff
changeset
|
246 |
val to_inline'' = |
323a57d7455c
imported patch satallax_skolemization_in_tree_part
fleury
parents:
57707
diff
changeset
|
247 |
map (fn s => (s, get_conclusion (find_proof_step hypotheses_step s))) |
323a57d7455c
imported patch satallax_skolemization_in_tree_part
fleury
parents:
57707
diff
changeset
|
248 |
(List.filter (fn s => nth_string s 0 = "h") |
323a57d7455c
imported patch satallax_skolemization_in_tree_part
fleury
parents:
57707
diff
changeset
|
249 |
(used_assumptions @ (map snd generated_goal_assumptions |> flat))) |
323a57d7455c
imported patch satallax_skolemization_in_tree_part
fleury
parents:
57707
diff
changeset
|
250 |
@ to_inline' |
323a57d7455c
imported patch satallax_skolemization_in_tree_part
fleury
parents:
57707
diff
changeset
|
251 |
val node' = Satallax_Step {id = id, role = role, theorem = |
323a57d7455c
imported patch satallax_skolemization_in_tree_part
fleury
parents:
57707
diff
changeset
|
252 |
AAtom (inline_if_needed_and_simplify theorem assumptions to_inline'' no_inline'), |
323a57d7455c
imported patch satallax_skolemization_in_tree_part
fleury
parents:
57707
diff
changeset
|
253 |
assumptions = assumptions, rule = rule, |
323a57d7455c
imported patch satallax_skolemization_in_tree_part
fleury
parents:
57707
diff
changeset
|
254 |
generated_goal_assumptions = generated_goal_assumptions, detailed_eigen = detailed_eigen, |
323a57d7455c
imported patch satallax_skolemization_in_tree_part
fleury
parents:
57707
diff
changeset
|
255 |
used_assumptions = |
323a57d7455c
imported patch satallax_skolemization_in_tree_part
fleury
parents:
57707
diff
changeset
|
256 |
List.filter (fn s => List.find (curry (op =) s o fst) to_inline = NONE) |
323a57d7455c
imported patch satallax_skolemization_in_tree_part
fleury
parents:
57707
diff
changeset
|
257 |
used_assumptions} |
323a57d7455c
imported patch satallax_skolemization_in_tree_part
fleury
parents:
57707
diff
changeset
|
258 |
in |
323a57d7455c
imported patch satallax_skolemization_in_tree_part
fleury
parents:
57707
diff
changeset
|
259 |
(Tree_Part {node = node', deps = dep'}, (to_inline'', no_inline')) |
323a57d7455c
imported patch satallax_skolemization_in_tree_part
fleury
parents:
57707
diff
changeset
|
260 |
end |
57706 | 261 |
in |
262 |
fst (inline_contradictory_assumptions (inline_in_step proof_sketch) ([], [])) |
|
263 |
end |
|
264 |
||
57710
323a57d7455c
imported patch satallax_skolemization_in_tree_part
fleury
parents:
57707
diff
changeset
|
265 |
fun correct_dependencies (Linear_Part {node, succs}) = |
323a57d7455c
imported patch satallax_skolemization_in_tree_part
fleury
parents:
57707
diff
changeset
|
266 |
Linear_Part {node = node, succs = map correct_dependencies succs} |
323a57d7455c
imported patch satallax_skolemization_in_tree_part
fleury
parents:
57707
diff
changeset
|
267 |
| correct_dependencies (Tree_Part {node, deps}) = |
57706 | 268 |
let |
269 |
val new_used_assumptions = |
|
57710
323a57d7455c
imported patch satallax_skolemization_in_tree_part
fleury
parents:
57707
diff
changeset
|
270 |
map (fn Linear_Part {node = (Satallax_Step{id, ...}), ...} => id |
323a57d7455c
imported patch satallax_skolemization_in_tree_part
fleury
parents:
57707
diff
changeset
|
271 |
| Tree_Part {node = (Satallax_Step{id, ...}), ...} => id) deps |
57706 | 272 |
in |
57710
323a57d7455c
imported patch satallax_skolemization_in_tree_part
fleury
parents:
57707
diff
changeset
|
273 |
Tree_Part {node = add_assumption new_used_assumptions node, |
57706 | 274 |
deps = map correct_dependencies deps} |
275 |
end |
|
276 |
||
277 |
fun create_satallax_proof_graph (hypotheses_step, proof_sketch) = |
|
57710
323a57d7455c
imported patch satallax_skolemization_in_tree_part
fleury
parents:
57707
diff
changeset
|
278 |
let |
323a57d7455c
imported patch satallax_skolemization_in_tree_part
fleury
parents:
57707
diff
changeset
|
279 |
fun create_step (step as Satallax_Step {generated_goal_assumptions, ...}) = |
323a57d7455c
imported patch satallax_skolemization_in_tree_part
fleury
parents:
57707
diff
changeset
|
280 |
Linear_Part {node = step, |
323a57d7455c
imported patch satallax_skolemization_in_tree_part
fleury
parents:
57707
diff
changeset
|
281 |
succs = map (create_step o (find_proof_step (hypotheses_step @ proof_sketch))) |
323a57d7455c
imported patch satallax_skolemization_in_tree_part
fleury
parents:
57707
diff
changeset
|
282 |
(map fst generated_goal_assumptions)} |
323a57d7455c
imported patch satallax_skolemization_in_tree_part
fleury
parents:
57707
diff
changeset
|
283 |
fun reverted_discharged_steps is_branched (Linear_Part {node as |
323a57d7455c
imported patch satallax_skolemization_in_tree_part
fleury
parents:
57707
diff
changeset
|
284 |
Satallax_Step {generated_goal_assumptions, ...}, succs}) = |
323a57d7455c
imported patch satallax_skolemization_in_tree_part
fleury
parents:
57707
diff
changeset
|
285 |
if is_branched orelse length generated_goal_assumptions > 1 then |
323a57d7455c
imported patch satallax_skolemization_in_tree_part
fleury
parents:
57707
diff
changeset
|
286 |
Tree_Part {node = node, deps = map (reverted_discharged_steps true) succs} |
323a57d7455c
imported patch satallax_skolemization_in_tree_part
fleury
parents:
57707
diff
changeset
|
287 |
else |
323a57d7455c
imported patch satallax_skolemization_in_tree_part
fleury
parents:
57707
diff
changeset
|
288 |
Linear_Part {node = node, succs = map (reverted_discharged_steps is_branched) succs} |
323a57d7455c
imported patch satallax_skolemization_in_tree_part
fleury
parents:
57707
diff
changeset
|
289 |
val proof_with_correct_sense = |
323a57d7455c
imported patch satallax_skolemization_in_tree_part
fleury
parents:
57707
diff
changeset
|
290 |
correct_dependencies (reverted_discharged_steps false |
323a57d7455c
imported patch satallax_skolemization_in_tree_part
fleury
parents:
57707
diff
changeset
|
291 |
(create_step (find_proof_step proof_sketch "0" ))) |
323a57d7455c
imported patch satallax_skolemization_in_tree_part
fleury
parents:
57707
diff
changeset
|
292 |
in |
323a57d7455c
imported patch satallax_skolemization_in_tree_part
fleury
parents:
57707
diff
changeset
|
293 |
transform_inline_assumption hypotheses_step proof_with_correct_sense |
323a57d7455c
imported patch satallax_skolemization_in_tree_part
fleury
parents:
57707
diff
changeset
|
294 |
end |
57706 | 295 |
|
296 |
val satallax_known_theorems = ["eq_ind", "eq_trans2", "eq_trans3", "eq_neg_neg_id", "eq_true", |
|
57714
4856a7b8b9c3
Changing the role of rule "tmp_ite_elim" of the SMT solver veriT to Lemma.
fleury
parents:
57710
diff
changeset
|
297 |
"eq_and_nor", "eq_or_nand", "eq_or_imp", "eq_and_imp", "eq_imp_or", "eq_iff", "eq_sym_eq", |
4856a7b8b9c3
Changing the role of rule "tmp_ite_elim" of the SMT solver veriT to Lemma.
fleury
parents:
57710
diff
changeset
|
298 |
"eq_forall_nexists", "eq_exists_nforall", "eq_leib1", "eq_leib2", "eq_leib3", "eq_leib4", |
4856a7b8b9c3
Changing the role of rule "tmp_ite_elim" of the SMT solver veriT to Lemma.
fleury
parents:
57710
diff
changeset
|
299 |
"eq_eta", "SinhE", "eq_forall_Seps", "eq_SPi_Seps", "eq_exists_Seps"] |
57706 | 300 |
val is_special_satallax_rule = member (op =) satallax_known_theorems |
301 |
||
57710
323a57d7455c
imported patch satallax_skolemization_in_tree_part
fleury
parents:
57707
diff
changeset
|
302 |
fun terms_to_upper_case var (AAbs (((var', ty), b), ts)) = |
57714
4856a7b8b9c3
Changing the role of rule "tmp_ite_elim" of the SMT solver veriT to Lemma.
fleury
parents:
57710
diff
changeset
|
303 |
let |
4856a7b8b9c3
Changing the role of rule "tmp_ite_elim" of the SMT solver veriT to Lemma.
fleury
parents:
57710
diff
changeset
|
304 |
val bdy = terms_to_upper_case var b |
4856a7b8b9c3
Changing the role of rule "tmp_ite_elim" of the SMT solver veriT to Lemma.
fleury
parents:
57710
diff
changeset
|
305 |
val ts' = map (terms_to_upper_case var) ts |
4856a7b8b9c3
Changing the role of rule "tmp_ite_elim" of the SMT solver veriT to Lemma.
fleury
parents:
57710
diff
changeset
|
306 |
in |
57710
323a57d7455c
imported patch satallax_skolemization_in_tree_part
fleury
parents:
57707
diff
changeset
|
307 |
AAbs (((((var = var' ? String.implode o (map Char.toUpper) o String.explode) var'), ty), |
323a57d7455c
imported patch satallax_skolemization_in_tree_part
fleury
parents:
57707
diff
changeset
|
308 |
bdy), ts') |
323a57d7455c
imported patch satallax_skolemization_in_tree_part
fleury
parents:
57707
diff
changeset
|
309 |
end |
323a57d7455c
imported patch satallax_skolemization_in_tree_part
fleury
parents:
57707
diff
changeset
|
310 |
| terms_to_upper_case var (ATerm ((var', ty), ts)) = |
323a57d7455c
imported patch satallax_skolemization_in_tree_part
fleury
parents:
57707
diff
changeset
|
311 |
ATerm ((((var = var' ? String.implode o (map Char.toUpper) o String.explode) var'), |
323a57d7455c
imported patch satallax_skolemization_in_tree_part
fleury
parents:
57707
diff
changeset
|
312 |
ty), map (terms_to_upper_case var) ts) |
57706 | 313 |
|
57710
323a57d7455c
imported patch satallax_skolemization_in_tree_part
fleury
parents:
57707
diff
changeset
|
314 |
fun add_quantifier_in_tree_part vars_to_add assumption_to_add (Linear_Part {node, succs}) = |
323a57d7455c
imported patch satallax_skolemization_in_tree_part
fleury
parents:
57707
diff
changeset
|
315 |
Linear_Part {node = node, succs = map (add_quantifier_in_tree_part vars_to_add assumption_to_add) succs} |
323a57d7455c
imported patch satallax_skolemization_in_tree_part
fleury
parents:
57707
diff
changeset
|
316 |
| add_quantifier_in_tree_part vars_to_add assumption_to_add (Tree_Part {node = Satallax_Step {rule, detailed_eigen, |
323a57d7455c
imported patch satallax_skolemization_in_tree_part
fleury
parents:
57707
diff
changeset
|
317 |
id, role, theorem = AAtom theorem, assumptions, used_assumptions, generated_goal_assumptions}, |
323a57d7455c
imported patch satallax_skolemization_in_tree_part
fleury
parents:
57707
diff
changeset
|
318 |
deps}) = |
57706 | 319 |
let |
57710
323a57d7455c
imported patch satallax_skolemization_in_tree_part
fleury
parents:
57707
diff
changeset
|
320 |
val theorem' = fold (fn v => fn body => terms_to_upper_case v body) vars_to_add theorem |
323a57d7455c
imported patch satallax_skolemization_in_tree_part
fleury
parents:
57707
diff
changeset
|
321 |
val theorem'' = theorem' |
323a57d7455c
imported patch satallax_skolemization_in_tree_part
fleury
parents:
57707
diff
changeset
|
322 |
val node' = mk_satallax_step id role (AAtom theorem'') assumptions rule |
323a57d7455c
imported patch satallax_skolemization_in_tree_part
fleury
parents:
57707
diff
changeset
|
323 |
(used_assumptions @ (filter (curry (op <=) (the (Int.fromString id)) o size) |
323a57d7455c
imported patch satallax_skolemization_in_tree_part
fleury
parents:
57707
diff
changeset
|
324 |
assumption_to_add)) generated_goal_assumptions detailed_eigen |
323a57d7455c
imported patch satallax_skolemization_in_tree_part
fleury
parents:
57707
diff
changeset
|
325 |
in |
323a57d7455c
imported patch satallax_skolemization_in_tree_part
fleury
parents:
57707
diff
changeset
|
326 |
if detailed_eigen <> "" then |
323a57d7455c
imported patch satallax_skolemization_in_tree_part
fleury
parents:
57707
diff
changeset
|
327 |
Tree_Part {node = node', |
323a57d7455c
imported patch satallax_skolemization_in_tree_part
fleury
parents:
57707
diff
changeset
|
328 |
deps = map (add_quantifier_in_tree_part (detailed_eigen :: vars_to_add) |
323a57d7455c
imported patch satallax_skolemization_in_tree_part
fleury
parents:
57707
diff
changeset
|
329 |
(used_assumptions @ assumption_to_add)) deps} |
323a57d7455c
imported patch satallax_skolemization_in_tree_part
fleury
parents:
57707
diff
changeset
|
330 |
else |
323a57d7455c
imported patch satallax_skolemization_in_tree_part
fleury
parents:
57707
diff
changeset
|
331 |
Tree_Part {node = node', |
323a57d7455c
imported patch satallax_skolemization_in_tree_part
fleury
parents:
57707
diff
changeset
|
332 |
deps = map (add_quantifier_in_tree_part vars_to_add assumption_to_add) deps} |
323a57d7455c
imported patch satallax_skolemization_in_tree_part
fleury
parents:
57707
diff
changeset
|
333 |
end |
57706 | 334 |
|
57710
323a57d7455c
imported patch satallax_skolemization_in_tree_part
fleury
parents:
57707
diff
changeset
|
335 |
fun transform_to_standard_atp_step already_transformed proof = |
323a57d7455c
imported patch satallax_skolemization_in_tree_part
fleury
parents:
57707
diff
changeset
|
336 |
let |
323a57d7455c
imported patch satallax_skolemization_in_tree_part
fleury
parents:
57707
diff
changeset
|
337 |
fun create_fact_step id = |
323a57d7455c
imported patch satallax_skolemization_in_tree_part
fleury
parents:
57707
diff
changeset
|
338 |
((id, [id]), Axiom, AAtom (ATerm((id, []), [])), "", []) |
323a57d7455c
imported patch satallax_skolemization_in_tree_part
fleury
parents:
57707
diff
changeset
|
339 |
fun transform_one_step already_transformed (Satallax_Step {id, theorem, used_assumptions, role, |
323a57d7455c
imported patch satallax_skolemization_in_tree_part
fleury
parents:
57707
diff
changeset
|
340 |
rule, ...}) = |
323a57d7455c
imported patch satallax_skolemization_in_tree_part
fleury
parents:
57707
diff
changeset
|
341 |
let |
323a57d7455c
imported patch satallax_skolemization_in_tree_part
fleury
parents:
57707
diff
changeset
|
342 |
val role' = role_of_tptp_string role |
323a57d7455c
imported patch satallax_skolemization_in_tree_part
fleury
parents:
57707
diff
changeset
|
343 |
val new_transformed = List.filter |
323a57d7455c
imported patch satallax_skolemization_in_tree_part
fleury
parents:
57707
diff
changeset
|
344 |
(fn s => size s >=4 andalso not (is_special_satallax_rule s) andalso not |
323a57d7455c
imported patch satallax_skolemization_in_tree_part
fleury
parents:
57707
diff
changeset
|
345 |
(member (op =) already_transformed s)) used_assumptions |
323a57d7455c
imported patch satallax_skolemization_in_tree_part
fleury
parents:
57707
diff
changeset
|
346 |
in |
323a57d7455c
imported patch satallax_skolemization_in_tree_part
fleury
parents:
57707
diff
changeset
|
347 |
(map create_fact_step new_transformed |
323a57d7455c
imported patch satallax_skolemization_in_tree_part
fleury
parents:
57707
diff
changeset
|
348 |
@ [((id, []), if role' = Unknown then Plain else role', theorem, rule, |
323a57d7455c
imported patch satallax_skolemization_in_tree_part
fleury
parents:
57707
diff
changeset
|
349 |
map (fn s => (s, [])) (filter_out is_special_satallax_rule used_assumptions))], |
323a57d7455c
imported patch satallax_skolemization_in_tree_part
fleury
parents:
57707
diff
changeset
|
350 |
new_transformed @ already_transformed) |
323a57d7455c
imported patch satallax_skolemization_in_tree_part
fleury
parents:
57707
diff
changeset
|
351 |
end |
323a57d7455c
imported patch satallax_skolemization_in_tree_part
fleury
parents:
57707
diff
changeset
|
352 |
fun transform_steps (Linear_Part {node, succs}) (already_transformed:string list) = |
323a57d7455c
imported patch satallax_skolemization_in_tree_part
fleury
parents:
57707
diff
changeset
|
353 |
transform_one_step already_transformed node |
323a57d7455c
imported patch satallax_skolemization_in_tree_part
fleury
parents:
57707
diff
changeset
|
354 |
||> (fold_map transform_steps succs) |
323a57d7455c
imported patch satallax_skolemization_in_tree_part
fleury
parents:
57707
diff
changeset
|
355 |
||> apfst flat |
323a57d7455c
imported patch satallax_skolemization_in_tree_part
fleury
parents:
57707
diff
changeset
|
356 |
|> (fn (a, (b, transformed)) => (a @ b, transformed)) |
323a57d7455c
imported patch satallax_skolemization_in_tree_part
fleury
parents:
57707
diff
changeset
|
357 |
| transform_steps (Tree_Part {node, deps}) (already_transformed: string list) = |
323a57d7455c
imported patch satallax_skolemization_in_tree_part
fleury
parents:
57707
diff
changeset
|
358 |
fold_map transform_steps deps already_transformed |
323a57d7455c
imported patch satallax_skolemization_in_tree_part
fleury
parents:
57707
diff
changeset
|
359 |
|>> flat |
323a57d7455c
imported patch satallax_skolemization_in_tree_part
fleury
parents:
57707
diff
changeset
|
360 |
||> (fn transformed => transform_one_step transformed node) |
323a57d7455c
imported patch satallax_skolemization_in_tree_part
fleury
parents:
57707
diff
changeset
|
361 |
|> (fn (a, (b, transformed)) => (a @ b, transformed)) |
323a57d7455c
imported patch satallax_skolemization_in_tree_part
fleury
parents:
57707
diff
changeset
|
362 |
in |
323a57d7455c
imported patch satallax_skolemization_in_tree_part
fleury
parents:
57707
diff
changeset
|
363 |
fst (transform_steps proof already_transformed) |
323a57d7455c
imported patch satallax_skolemization_in_tree_part
fleury
parents:
57707
diff
changeset
|
364 |
end |
323a57d7455c
imported patch satallax_skolemization_in_tree_part
fleury
parents:
57707
diff
changeset
|
365 |
|
323a57d7455c
imported patch satallax_skolemization_in_tree_part
fleury
parents:
57707
diff
changeset
|
366 |
fun remove_unused_dependency steps = |
323a57d7455c
imported patch satallax_skolemization_in_tree_part
fleury
parents:
57707
diff
changeset
|
367 |
let |
323a57d7455c
imported patch satallax_skolemization_in_tree_part
fleury
parents:
57707
diff
changeset
|
368 |
fun find_all_ids [] = [] |
57714
4856a7b8b9c3
Changing the role of rule "tmp_ite_elim" of the SMT solver veriT to Lemma.
fleury
parents:
57710
diff
changeset
|
369 |
| find_all_ids (((id, _), _, _, _, _) :: steps) = id :: find_all_ids steps |
57710
323a57d7455c
imported patch satallax_skolemization_in_tree_part
fleury
parents:
57707
diff
changeset
|
370 |
fun keep_only_used used_ids steps = |
323a57d7455c
imported patch satallax_skolemization_in_tree_part
fleury
parents:
57707
diff
changeset
|
371 |
let |
323a57d7455c
imported patch satallax_skolemization_in_tree_part
fleury
parents:
57707
diff
changeset
|
372 |
fun remove_unused (((id, ids), role, theorem, rule, deps) :: steps) = |
323a57d7455c
imported patch satallax_skolemization_in_tree_part
fleury
parents:
57707
diff
changeset
|
373 |
(((id, ids), role, theorem, rule, filter (member (op =) used_ids o fst) deps) :: steps) |
323a57d7455c
imported patch satallax_skolemization_in_tree_part
fleury
parents:
57707
diff
changeset
|
374 |
| remove_unused [] = [] |
323a57d7455c
imported patch satallax_skolemization_in_tree_part
fleury
parents:
57707
diff
changeset
|
375 |
in |
323a57d7455c
imported patch satallax_skolemization_in_tree_part
fleury
parents:
57707
diff
changeset
|
376 |
remove_unused steps |
323a57d7455c
imported patch satallax_skolemization_in_tree_part
fleury
parents:
57707
diff
changeset
|
377 |
end |
323a57d7455c
imported patch satallax_skolemization_in_tree_part
fleury
parents:
57707
diff
changeset
|
378 |
in |
323a57d7455c
imported patch satallax_skolemization_in_tree_part
fleury
parents:
57707
diff
changeset
|
379 |
keep_only_used (find_all_ids steps) steps |
323a57d7455c
imported patch satallax_skolemization_in_tree_part
fleury
parents:
57707
diff
changeset
|
380 |
end |
57706 | 381 |
|
382 |
fun parse_proof local_name problem = |
|
57714
4856a7b8b9c3
Changing the role of rule "tmp_ite_elim" of the SMT solver veriT to Lemma.
fleury
parents:
57710
diff
changeset
|
383 |
strip_spaces_except_between_idents |
4856a7b8b9c3
Changing the role of rule "tmp_ite_elim" of the SMT solver veriT to Lemma.
fleury
parents:
57710
diff
changeset
|
384 |
#> raw_explode |
4856a7b8b9c3
Changing the role of rule "tmp_ite_elim" of the SMT solver veriT to Lemma.
fleury
parents:
57710
diff
changeset
|
385 |
#> |
4856a7b8b9c3
Changing the role of rule "tmp_ite_elim" of the SMT solver veriT to Lemma.
fleury
parents:
57710
diff
changeset
|
386 |
(if local_name <> satallaxN then |
4856a7b8b9c3
Changing the role of rule "tmp_ite_elim" of the SMT solver veriT to Lemma.
fleury
parents:
57710
diff
changeset
|
387 |
(Scan.error (!! (fn _ => raise UNRECOGNIZED_ATP_PROOF ()) |
4856a7b8b9c3
Changing the role of rule "tmp_ite_elim" of the SMT solver veriT to Lemma.
fleury
parents:
57710
diff
changeset
|
388 |
(Scan.finite Symbol.stopper (Scan.repeat1 (parse_line local_name problem) >> flat))) |
4856a7b8b9c3
Changing the role of rule "tmp_ite_elim" of the SMT solver veriT to Lemma.
fleury
parents:
57710
diff
changeset
|
389 |
#> fst) |
4856a7b8b9c3
Changing the role of rule "tmp_ite_elim" of the SMT solver veriT to Lemma.
fleury
parents:
57710
diff
changeset
|
390 |
else |
4856a7b8b9c3
Changing the role of rule "tmp_ite_elim" of the SMT solver veriT to Lemma.
fleury
parents:
57710
diff
changeset
|
391 |
(Scan.error (!! (fn _ => raise UNRECOGNIZED_ATP_PROOF ()) |
4856a7b8b9c3
Changing the role of rule "tmp_ite_elim" of the SMT solver veriT to Lemma.
fleury
parents:
57710
diff
changeset
|
392 |
(Scan.finite Symbol.stopper (Scan.repeat1 (parse_tstp_thf0_satallax_line)))) |
4856a7b8b9c3
Changing the role of rule "tmp_ite_elim" of the SMT solver veriT to Lemma.
fleury
parents:
57710
diff
changeset
|
393 |
#> fst |
4856a7b8b9c3
Changing the role of rule "tmp_ite_elim" of the SMT solver veriT to Lemma.
fleury
parents:
57710
diff
changeset
|
394 |
#> rev |
4856a7b8b9c3
Changing the role of rule "tmp_ite_elim" of the SMT solver veriT to Lemma.
fleury
parents:
57710
diff
changeset
|
395 |
#> map to_satallax_step |
4856a7b8b9c3
Changing the role of rule "tmp_ite_elim" of the SMT solver veriT to Lemma.
fleury
parents:
57710
diff
changeset
|
396 |
#> seperate_assumptions_and_steps |
4856a7b8b9c3
Changing the role of rule "tmp_ite_elim" of the SMT solver veriT to Lemma.
fleury
parents:
57710
diff
changeset
|
397 |
#> create_satallax_proof_graph |
4856a7b8b9c3
Changing the role of rule "tmp_ite_elim" of the SMT solver veriT to Lemma.
fleury
parents:
57710
diff
changeset
|
398 |
#> add_quantifier_in_tree_part [] [] |
4856a7b8b9c3
Changing the role of rule "tmp_ite_elim" of the SMT solver veriT to Lemma.
fleury
parents:
57710
diff
changeset
|
399 |
#> transform_to_standard_atp_step [] |
4856a7b8b9c3
Changing the role of rule "tmp_ite_elim" of the SMT solver veriT to Lemma.
fleury
parents:
57710
diff
changeset
|
400 |
#> remove_unused_dependency)) |
57706 | 401 |
|
402 |
fun atp_proof_of_tstplike_proof _ _ "" = [] |
|
403 |
| atp_proof_of_tstplike_proof local_prover problem tstp = |
|
404 |
(case core_of_agsyhol_proof tstp of |
|
405 |
SOME facts => facts |> map (core_inference agsyhol_core_rule) |
|
406 |
| NONE => |
|
407 |
tstp ^ "$" (* the $ sign acts as a sentinel (FIXME: needed?) *) |
|
408 |
|> parse_proof local_prover problem |
|
409 |
|> local_prover = vampireN ? perhaps (try (sort (vampire_step_name_ord o pairself #1))) |
|
410 |
|> local_prover = zipperpositionN ? rev) |
|
411 |
||
412 |
end; |