Skip to content

Commit d59677e

Browse files
yutakangyutakang
committed
preparation for decremental abduction.
1 parent e7b4820 commit d59677e

File tree

2 files changed

+104
-37
lines changed

2 files changed

+104
-37
lines changed

‎Abduction/Proof_By_Abduction.ML

+9-2
Original file line numberDiff line numberDiff line change
@@ -61,14 +61,21 @@ fun expand_ornode (or_key as (Or_N, [lemma_term]):key) (pst:state, graph:abducti
6161
(*top-down explicit conjecturing*)
6262
val top_down_conjectures = All_Top_Down_Conjecturing.top_down_conjectures (Proof.context_of pst) lemma_term: (string * term) list;
6363
val seeds_from_conjectures = (*TODO: At the moment, we throw away the hints for top-down auxiliary lemma names, since incorporating this information requires changing the type of andnode.*)
64-
SOOE.conjectures_to_seeds_of_or2and_edge (pst, pst_to_prove) top_down_conjectures : seeds_of_or2and_edge;
64+
SOOE.conjectures_to_seeds_of_or2and_edge (pst, pst_to_prove) top_down_conjectures : seeds_of_or2and_edge;
6565
val all_seeds = seeds_from_conjectures @ seeds_from_tactics : seeds_of_or2and_edge;
6666
val filtered_seeds = SOOE.filter_out_bad_seeds_of_or2and_edge lemma_term pst graph all_seeds: seeds_of_or2and_edge;
6767
val seeds_wo_counterexample = filter_out (SOOE.seed_has_counterexample pst) filtered_seeds : seeds_of_or2and_edge;
68+
(*
6869
val expanded_graph = SOOE.seeds_to_updated_graph or_key seeds_wo_counterexample graph : abduction_graph;
70+
*)
71+
val good_seeds_from_tactics = filter SOOE.seed_is_from_tactic seeds_wo_counterexample : seeds_of_or2and_edge;
72+
val graph_extended_by_tactics = SOOE.seeds_to_updated_graph or_key good_seeds_from_tactics graph : abduction_graph;
73+
val good_seeds_from_cnjctr = filter_out SOOE.seed_is_from_tactic seeds_wo_counterexample : seeds_of_or2and_edge;
74+
val graph_extended_by_cnjctr = SOOE.seeds_to_updated_graph or_key good_seeds_from_cnjctr graph_extended_by_tactics: abduction_graph;
75+
6976
in
7077
(*seeds_to_updated_graph is very expensive*)
71-
(pst, expanded_graph)
78+
(pst, graph_extended_by_cnjctr(*expanded_graph*))
7279
end
7380
end
7481
| expand_ornode _ _ = error "expand_ornode failed. Not an Or_N.";

‎Abduction/Seed_Of_Or2And_Edge.ML

+95-35
Original file line numberDiff line numberDiff line change
@@ -11,10 +11,10 @@ sig
1111

1212
type abduction_graph;
1313
type key;
14-
type how_to_get_andnodes_from_ornode;
15-
type abduction_node
14+
type how_to_get_andnodes_from_ornode = Or2And_Edge.how_to_get_andnodes_from_ornode;
15+
type abduction_node;
1616
type seed_of_or2and_edge =
17-
{new_goals: terms,
17+
{new_goals: (string * term) list,
1818
proof : how_to_get_andnodes_from_ornode,
1919
state : Proof.state};
2020
type seeds_of_or2and_edge;
@@ -39,21 +39,22 @@ structure UAG = Update_Abduction_Graph;
3939
type how_to_get_andnodes_from_ornode = Or2And_Edge.how_to_get_andnodes_from_ornode;
4040

4141
type seed_of_or2and_edge =
42-
{new_goals: terms,
42+
{new_goals: (string * term) list,
4343
proof : how_to_get_andnodes_from_ornode,
4444
state : Proof.state};
4545

4646
type seeds_of_or2and_edge = seed_of_or2and_edge list;
4747

4848
fun print_seed_of_or2and_edge ctxt ({new_goals,...}: seed_of_or2and_edge) = (
4949
tracing "== print_seed_of_or2and_edge: ==";
50-
map (tracing o Isabelle_Utils.trm_to_string ctxt) new_goals
50+
map (tracing o Isabelle_Utils.trm_to_string ctxt o snd) new_goals
5151
);
5252

5353
fun seed_is_from_tactic ({proof, ...}) = Or2And_Edge.proof_is_from_tactic proof: bool;
5454

5555
(* apply_Extend_Leaf_to_pst_get_records_to_mk_andnodes *)
56-
(*TODO: handle the case where we actually finish to prove this.*)
56+
(* The return type of this function should be seeds_of_or2and_edge because we need the resulting
57+
* proof states. *)
5758
fun apply_PSL_to_get_seeds_of_or2and_edges (pst:Proof.state) =
5859
let
5960
val ctxt = Proof.context_of pst;
@@ -72,14 +73,15 @@ fun apply_PSL_to_get_seeds_of_or2and_edges (pst:Proof.state) =
7273
|> Isabelle_Utils.trm_to_string ctxt
7374
|> Syntax.read_term ctxt
7475
|> Top_Down_Util.standardize_vnames;
75-
76-
fun check_print_read_terms ctxt terms = map (check_print_read ctxt) terms: terms;
76+
77+
fun check_print_read_terms ctxt terms = map (check_print_read ctxt) terms: terms;
7778
fun pass_check_print_read_terms ctxt terms = try (check_print_read_terms ctxt) terms |> is_some;
79+
val mk_lemma_name = Shared_State.get_lemma_name: Proof.context -> term -> string;
7880

7981
val nonempty_subgs =
8082
if length subgs = 0 orelse not (pass_check_print_read_terms ctxt standardized_subgs)
81-
then [@{prop "True"}]
82-
else standardized_subgs: terms;
83+
then [(mk_lemma_name ctxt @{prop "True"}, @{prop "True"})]
84+
else map (mk_lemma_name ctxt) standardized_subgs ~~ standardized_subgs: (string * term) list;
8385

8486
in
8587
{proof = Or2And_Edge.Tactic pscript, new_goals = nonempty_subgs, state = pst}: seed_of_or2and_edge
@@ -93,9 +95,7 @@ fun condition_to_filter_out_cnjctr (parent_or:term) (pst:Proof.state) (ag:abduct
9395

9496
datatype conjecture_typ = Explicit_Conjecturing | Implicit_Conjecturing (*tactic application*);
9597

96-
fun filtering_policy Explicit_Conjecturing = ()
97-
98-
fun condition_to_filter_out (parent_or:term) (pst:Proof.state) (ag:abduction_graph) (seed:seed_of_or2and_edge) =
98+
fun condition_to_filter_out (parent_or:term) (pst:Proof.state) (ag:abduction_graph) (seed:seed_of_or2and_edge): bool =
9999
let
100100
val final_goal = get_final_goal_key ag |> snd |> hd: term;
101101
(*
@@ -111,7 +111,7 @@ fun condition_to_filter_out (parent_or:term) (pst:Proof.state) (ag:abduction_gra
111111
Top_Down_Util.alpha_eq_over_fvar trm cncl
112112
end;
113113

114-
val trms = #new_goals seed : terms;
114+
val trms = map snd (#new_goals seed) : terms;
115115
val trms_empty = null trms : bool;
116116
fun too_large _ = exists (fn trm => Real.fromInt (Term.size_of_term trm) > upper_limit) trms: bool;
117117
fun eq_to_final_goal _ = exists (Top_Down_Util.alpha_eq_over_fvar final_goal) trms : bool;
@@ -141,36 +141,41 @@ fun condition_to_filter_out (parent_or:term) (pst:Proof.state) (ag:abduction_gra
141141
fun filter_out_bad_seeds_of_or2and_edge (parent_or:term) (pst:Proof.state) (graph:abduction_graph) (seeds:seeds_of_or2and_edge) =
142142
filter_out (condition_to_filter_out parent_or pst graph) seeds: seeds_of_or2and_edge;
143143

144-
fun conjectures_to_seed_of_or2and_edge (pst:Proof.state) (cnjctr:term): seed_of_or2and_edge =
145-
{new_goals = [cnjctr] : terms,
144+
fun conjecture_to_seed_of_or2and_edge (pst:Proof.state) (cnjctr:term): seed_of_or2and_edge =
145+
{new_goals = map (fn and_trm => (Shared_State.get_lemma_name (Proof.context_of pst) and_trm, and_trm)) [cnjctr]: (string * term) list,
146146
proof = Or2And_Edge.Conjecture: how_to_get_andnodes_from_ornode,
147147
state = pst : Proof.state};
148148

149+
(*TODO: decremental conjectring.*)
149150
fun conjectures_to_seeds_of_or2and_edge (pst:Proof.state, pst_to_prove_ornode:Proof.state) (cnjctrs_w_name: (string * term) list) =
150151
let
151-
val ctxt = Proof.context_of pst : Proof.context;
152-
fun get_ctxt_w_proof_goal trm = Proof.context_of (Top_Down_Util.mk_pst_to_prove_from_term ctxt trm) : Proof.context;
153-
fun check_prop (trm:term) = try (Syntax.check_prop (get_ctxt_w_proof_goal trm)) trm : term option;
154-
val cnjctrs = map snd cnjctrs_w_name : terms;
155-
val checked_cnjctrs = List.mapPartial check_prop cnjctrs : terms;
156-
val result = map (fn trm => conjectures_to_seed_of_or2and_edge pst_to_prove_ornode trm) checked_cnjctrs: seeds_of_or2and_edge;
152+
val ctxt = Proof.context_of pst : Proof.context;
153+
fun get_ctxt_w_proof_goal trm = Proof.context_of (Top_Down_Util.mk_pst_to_prove_from_term ctxt trm) : Proof.context;
154+
fun check_prop (trm:term) = try (Syntax.check_prop (get_ctxt_w_proof_goal trm)) trm : term option;
155+
val cnjctrs = map snd cnjctrs_w_name : terms;
156+
val checked_cnjctrs = List.mapPartial check_prop cnjctrs : terms;
157+
val result = map (fn trm => conjecture_to_seed_of_or2and_edge pst_to_prove_ornode trm) checked_cnjctrs: seeds_of_or2and_edge;
157158
in
158-
result
159+
result: seeds_of_or2and_edge
159160
end;
160161

161162
fun seed_has_counterexample (pst:Proof.state) ({new_goals,...}:seed_of_or2and_edge) =
162-
Shared_State.any_of_these_is_refuted pst new_goals;
163+
let
164+
val conjectures = map snd new_goals;
165+
in
166+
Shared_State.any_of_these_is_refuted pst conjectures
167+
end;
163168

164169
fun add_or2and_edge_and_connect_it_to_parental_ornode
165170
(parent_or_key as (Or_N, _): key)(*parent node*)
166-
({new_goals : terms,
171+
({new_goals : (string * term) list,
167172
proof : how_to_get_andnodes_from_ornode,
168173
state(*chained*) : Proof.state, ...}: seed_of_or2and_edge)(*child nodes*)
169174
(graph:abduction_graph): (key option * (string * term) list * abduction_graph) =
170175
let
171176
val ctxt = Proof.context_of state;
172-
val name_term_pairs = map (fn and_trm => (Shared_State.get_lemma_name ctxt and_trm, and_trm)) new_goals : (string * term) list;
173-
val pst_w_or_terms_assmd = Top_Down_Util.assume_cnjctrs_in_pst name_term_pairs state : Proof.state;
177+
(* val name_term_pairs = map (fn and_trm => (Shared_State.get_lemma_name ctxt and_trm, and_trm)) new_goals : (string * term) list;*)
178+
val pst_w_or_terms_assmd = Top_Down_Util.assume_cnjctrs_in_pst new_goals state : Proof.state;
174179
(*TODO: maybe we should assume or-nodes that have been already proved completely in the abduction_graph.*)
175180
val timeouts = {overall = 30.0, hammer = 10.0, quickcheck = 1.0, nitpick = 2.0}: TBC_Utils.timeouts;
176181
(*very expensive*)
@@ -189,17 +194,17 @@ fun add_or2and_edge_and_connect_it_to_parental_ornode
189194
val or2and_edge_key = ((O2A_E (serial())), []) : key;
190195
val thy = Proof.theory_of state : theory;
191196
val used_cnjctr_names = Top_Down_Util.get_lemma_names_from_sh_output thy script_to_prove_andnd : strings;
192-
val used_name_term_pairs = filter (fn (name, _) => member (op =) used_cnjctr_names name) name_term_pairs: (string * term) list;
193-
val relevant_name_term_pairs = if Or2And_Edge.how_to_get_andnodes_from_ornode_of proof = "" (*if this is the result of tactic application*)
194-
then used_name_term_pairs
195-
else name_term_pairs;
197+
val used_new_goals = filter (fn (name, _) => member (op =) used_cnjctr_names name) new_goals: (string * term) list;
198+
val relevant_new_goals = if Or2And_Edge.how_to_get_andnodes_from_ornode_of proof = "" (*if this is the result of tactic application*)
199+
then used_new_goals
200+
else new_goals;
196201

197202
(* updating abduction_graph *)
198203
val graph_w_ornode_to_or2and_edge = graph
199204
|> PGraph.new_node (or2and_edge_key, or2and_edge_val)
200205
|> Update_Abduction_Graph.add_edge_acyclic_if_possible parent_or_key or2and_edge_key: abduction_graph;
201206
in
202-
(SOME or2and_edge_key, relevant_name_term_pairs, graph_w_ornode_to_or2and_edge)
207+
(SOME or2and_edge_key, relevant_new_goals, graph_w_ornode_to_or2and_edge)
203208
end
204209
else (NONE, [], graph)
205210
end
@@ -219,8 +224,11 @@ fun add_then_connect_or2and_edge_andnd_ornds (parent_ornd:key) (seed: seed_of_or
219224
let
220225
val graph_w_ornode_is_now_branch = UAG.update_is_branch parent_ornd graph : abduction_graph;
221226
(*add an or2and_ege and connect them to their parental or-node if we can prove the or-node assuming the and-node.*)
222-
val (or2and_edge_opt, used_and_node_name_term_pairs, graph_w_connected_or2add_edges) =
223-
add_or2and_edge_and_connect_it_to_parental_ornode parent_ornd seed graph_w_ornode_is_now_branch: (key option * (string * term) list * abduction_graph);
227+
(*1,2,3*)
228+
val (or2and_edge_opt,
229+
used_and_node_name_term_pairs,
230+
graph_w_connected_or2add_edges) =
231+
add_or2and_edge_and_connect_it_to_parental_ornode parent_ornd seed graph_w_ornode_is_now_branch;
224232
val parent_ornd_is_proved_assmng_seed = is_some or2and_edge_opt: bool;
225233
in
226234
if parent_ornd_is_proved_assmng_seed
@@ -231,10 +239,14 @@ fun add_then_connect_or2and_edge_andnd_ornds (parent_ornd:key) (seed: seed_of_or
231239
val (added_andnode_keys, graph_w_addnodes) = UAG.add_andnode and_node_terms graph_w_connected_or2add_edges : (key list * abduction_graph);
232240
val _ = if length added_andnode_keys = 1 then () else error "length added_andnode_keys != 1"
233241
val or2and_edge_key = the or2and_edge_opt : key;
242+
(*4*)
234243
val added_andnode_key = hd added_andnode_keys : key;
244+
(*5*)
235245
val graph_w_connected_andnode = UAG.add_edge_acyclic_if_possible or2and_edge_key added_andnode_key graph_w_addnodes : abduction_graph;
246+
(*6*)
236247
val graph_w_child_ornode = fold UAG.add_child_ornode used_and_node_name_term_pairs graph_w_connected_andnode : abduction_graph;
237-
val graph_w_connected_child_ornode = UAG.add_edges_from_andnode_to_ornodes added_andnode_key graph_w_child_ornode : abduction_graph
248+
(*7*)
249+
val graph_w_connected_child_ornode = UAG.add_edges_from_andnode_to_ornodes added_andnode_key graph_w_child_ornode : abduction_graph;
238250
in
239251
graph_w_connected_child_ornode
240252
end
@@ -244,4 +256,52 @@ fun add_then_connect_or2and_edge_andnd_ornds (parent_ornd:key) (seed: seed_of_or
244256
fun seeds_to_updated_graph (parent_ornd:key) (seeds: seeds_of_or2and_edge) (graph:abduction_graph) =
245257
fold (add_then_connect_or2and_edge_andnd_ornds parent_ornd) seeds graph: abduction_graph;
246258

259+
(*
260+
(* decremental abduction*)
261+
(*
262+
* 0. We have an or-node to expand.
263+
* 1. add an or2and-edge.
264+
* 2. connect the or2and-edge to its parental or-node.
265+
* 3. prove the parental or-node using some conjectures.
266+
* 4. add an and-node that consists of used conjectures.
267+
* 5. connect the and-node to its parental or2and-edge.
268+
* 6. add child-or-nodes that correspond to the sub-goals or used conjectures in the and-node.
269+
* 7. connect the child-or-nodes to the and-node.
270+
*)
271+
fun add_then_connect_or2and_edge_andnd_ornds (parent_ornd:key) (seed: seed_of_or2and_edge) (graph:abduction_graph): abduction_graph =
272+
let
273+
val graph_w_ornode_is_now_branch = UAG.update_is_branch parent_ornd graph : abduction_graph;
274+
(*add an or2and_ege and connect them to their parental or-node if we can prove the or-node assuming the and-node.*)
275+
(*1,2,3*)
276+
val (or2and_edge_opt, used_and_node_name_term_pairs, graph_w_connected_or2add_edges) =
277+
add_or2and_edge_and_connect_it_to_parental_ornode parent_ornd seed graph_w_ornode_is_now_branch;
278+
val parent_ornd_is_proved_assmng_seed = is_some or2and_edge_opt: bool;
279+
in
280+
if parent_ornd_is_proved_assmng_seed
281+
then
282+
let
283+
val and_node_terms = map snd used_and_node_name_term_pairs: terms;
284+
(*length added_andnode_keys should be 1.*)
285+
val (added_andnode_keys, graph_w_addnodes) = UAG.add_andnode and_node_terms graph_w_connected_or2add_edges : (key list * abduction_graph);
286+
val _ = if length added_andnode_keys = 1 then () else error "length added_andnode_keys != 1"
287+
val or2and_edge_key = the or2and_edge_opt : key;
288+
(*4*)
289+
val added_andnode_key = hd added_andnode_keys : key;
290+
(*5*)
291+
val graph_w_connected_andnode = UAG.add_edge_acyclic_if_possible or2and_edge_key added_andnode_key graph_w_addnodes : abduction_graph;
292+
(*6*)
293+
val graph_w_child_ornode = fold UAG.add_child_ornode used_and_node_name_term_pairs graph_w_connected_andnode : abduction_graph;
294+
(*7*)
295+
val graph_w_connected_child_ornode = UAG.add_edges_from_andnode_to_ornodes added_andnode_key graph_w_child_ornode : abduction_graph;
296+
297+
val name_term_pairs_wo_one_used_term = map (fn (_, used_term) => remove (op =) used_term (#new_goals seed)) used_and_node_name_term_pairs
298+
in
299+
graph_w_connected_child_ornode
300+
end
301+
else graph
302+
end;
303+
304+
fun seeds_to_updated_graph (parent_ornd:key) (seeds: seeds_of_or2and_edge) (graph:abduction_graph) =
305+
fold (add_then_connect_or2and_edge_andnd_ornds parent_ornd) seeds graph: abduction_graph;
306+
*)
247307
end;

0 commit comments

Comments
 (0)