Skip to content

Commit

Permalink
remove is_refuted from and_nodes and or_nodes of abduction_graph.
Browse files Browse the repository at this point in the history 
Now the information is stored in Shared_State.
This simplified the codebase quite a bit.
  • Loading branch information
@yutakang
yutakang committed May 22, 2023
1 parent d07d567 commit 565e1c3
Show file tree
Hide file tree
Showing 9 changed files with 38 additions and 145 deletions.
26 changes: 9 additions & 17 deletions Abduction/Abduction_Graph.ML
View file
Original file line number Diff line number Diff line change
Expand Up @@ -45,7 +45,6 @@ val is_or2and_edge: key -> bool;

(* query on abduction_node for ornode and andnode *)
val is_proved_completely : abduction_graph -> key -> bool;
val is_refuted : abduction_graph -> key -> bool;

(* query on abduction_node for ornode *)
val is_final_goal : abduction_graph -> key -> bool;
Expand All @@ -66,7 +65,7 @@ val is_worth_proving : Proof.context -> abduction_gr
(*TODO: it is a little strange that we have proof_of and or2and_edge_to_proof separately.*)
val get_final_goal_term : abduction_graph -> term;
val get_final_goal_key : abduction_graph -> key;
val keys_tobe_expanded_in : Proof.context -> abduction_graph -> keys;
val orkeys_tobe_expanded_in : Proof.context -> abduction_graph -> keys;

val goal_as_string : Proof.state -> key -> string;

Expand Down Expand Up @@ -145,8 +144,7 @@ fun mk_andnode (goals:terms) =
(And_N, goals): key,
Abduction_Node.And_Node {
subgoals = goals,
proved_completely = false,
refuted = false
proved_completely = false
});

(* key to term *)
Expand Down Expand Up @@ -183,10 +181,6 @@ fun is_or2and_edge (O2A_E _, _) = true
fun is_proved_completely (graph:abduction_graph) (key:key): bool =
PGraph.get_node graph key |> Abduction_Node.is_proved_completely;

(* is_refuted *)
fun is_refuted (graph:abduction_graph) (key:key): bool =
PGraph.get_node graph key |> Abduction_Node.is_refuted;

(* lemma_name_of *)
fun lemma_name_of (graph:abduction_graph) (key:key) =
PGraph.get_node graph key |> Abduction_Node.lemma_name_of: string;
Expand Down Expand Up @@ -278,19 +272,17 @@ fun goal_as_string (pst:Proof.state) ((Or_N, [term]):key) = Isabelle_Utils.trm_t
| goal_as_string (pst:Proof.state) ((And_N, terms):key) = map (Isabelle_Utils.trm_to_string (Proof.context_of pst)) terms |> String.concatWith "\n"
| goal_as_string _ _ = error "goal_as_string in Proof_Graph.ML failed"

(* keys_tobe_expanded_in *)
fun keys_tobe_expanded_in (ctxt:Proof.context) (graph:abduction_graph): keys =
(* orkeys_tobe_expanded_in *)
fun orkeys_tobe_expanded_in (ctxt:Proof.context) (graph:abduction_graph): keys =
let
val or_keys = PGraph.keys graph |> filter is_ornode : keys;
val orleaf_keys = filter_out (is_branch graph) or_keys : keys
val or_keys = PGraph.keys graph |> filter is_ornode : keys;
val orleaf_keys = filter_out (is_branch graph) or_keys : keys
val keys_worth_trying = filter (is_worth_proving ctxt graph) orleaf_keys: keys;
val final_goal_key = get_final_goal_key graph : key;
val keys_reachable_from_final_goal = PGraph.all_succs graph [final_goal_key] : keys;
val keys_reachable_from_final_goal = PGraph.all_succs graph [final_goal_key] : keys;
val _ = tracing ("Number of keys_reachable_from_final_goal: " ^ Int.toString (length keys_reachable_from_final_goal));
val _ = map (print_key ctxt) keys_reachable_from_final_goal
val result = inter equal_keys keys_worth_trying keys_reachable_from_final_goal;
val _ = tracing ("Number of keys_reachable_from_final_goal after removing dups: " ^ Int.toString (length result));
val _ = map (print_key ctxt) result
(*val _ = map (print_key ctxt) keys_reachable_from_final_goal*)
val result = inter equal_keys keys_worth_trying keys_reachable_from_final_goal;
in
result
end;
Expand Down
6 changes: 0 additions & 6 deletions Abduction/Abduction_Node.ML
View file
Original file line number Diff line number Diff line change
Expand Up @@ -26,7 +26,6 @@ val is_or2and_edge : abduction_node -> bool;

(* query on abduction_node for ornode and andnode *)
val is_proved_completely : abduction_node -> bool;
val is_refuted : abduction_node -> bool;

(* query on abduction_node for ornode *)
val proof_id_of : abduction_node -> int option;
Expand Down Expand Up @@ -84,11 +83,6 @@ fun is_proved_completely (Or_Node nd) = #proved_completely nd
| is_proved_completely (And_Node nd) = #proved_completely nd
| is_proved_completely (Or_To_And _) = error "is_proved_completely failed."

(* is_refuted *)
fun is_refuted (Or_Node ornode ) = #refuted ornode
| is_refuted (And_Node andnode) = #refuted andnode
| is_refuted _ = error "is_refuted failed. This should not be applied to an edge."

(* is_worth_proving *)
fun is_worth_proving ctxt (Or_Node or_nd) = Or_Node.is_worth_proving ctxt or_nd
| is_worth_proving _ (And_Node _) = error "is_worth_proving failed. This is And_Node."
Expand Down
22 changes: 3 additions & 19 deletions Abduction/And_Node.ML
View file
Original file line number Diff line number Diff line change
Expand Up @@ -17,7 +17,6 @@ type andnodes;

(* update of andnode *)
val update_proved_completely: andnode -> andnode;
val update_refuted : andnode -> andnode;

end

Expand All @@ -30,8 +29,7 @@ struct
type andnode =
{
subgoals : terms, (*Used to detect the order of sub-goals.*)
proved_completely : bool,
refuted : bool
proved_completely : bool
};

(* andnodes *)
Expand All @@ -41,25 +39,11 @@ type andnodes = andnode list;
(* update_proved_completely_of_andnode *)
fun update_proved_completely (
{
subgoals: terms,
refuted: bool, ...
subgoals: terms,...
}: andnode) =
{
subgoals = subgoals,
proved_completely = true,
refuted = refuted
}: andnode;

(* update_refuted_of_andnode *)
fun update_refuted (
{
subgoals : terms,
proved_completely: bool,...
}: andnode) =
{
subgoals = subgoals,
proved_completely = proved_completely,
refuted = true
proved_completely = true
}: andnode;

end;
39 changes: 0 additions & 39 deletions Abduction/Or_Node.ML
View file
Original file line number Diff line number Diff line change
Expand Up @@ -15,7 +15,6 @@ type ornode;
type ornodes;

(* query on ornode *)
val is_refuted : ornode -> bool;
val is_worth_proving : Proof.context -> ornode -> bool;

(* creation of ornode *)
Expand All @@ -26,7 +25,6 @@ val mk_ornode: is_final_goal -> term -> ornode;
val update_gg_parent_not_finished: ornode -> bool -> ornode;
val update_proved_completely : ornode -> ornode;
val update_proof_n_proof_id : string -> ornode -> ornode;
val update_refuted : ornode -> ornode;
val update_branch : ornode -> ornode;

end;
Expand All @@ -44,7 +42,6 @@ type ornode = {
lemma_term : term,(*For now we ignore "assumes" and "using".*)
proof : string option,(*Proof script to finish proving this node.*)
proof_id : int option,(*To track dependency. based on the timing proved with or w/o assuming conjectures.*)
refuted : bool,
proved_completely : bool, (*= proved w/o assuming conjectures.*)
(* If an or-node has a great grandparent that is not proved or refuted and this node is not
* proved_completely, this node still needs a proof.*)
Expand All @@ -55,9 +52,6 @@ type ornodes = ornode list;

(** query on ornode **)

(* is_refuted *)
fun is_refuted ({refuted,...}:ornode) = refuted: bool;

(* is_worth_proving *)
fun is_worth_proving (ctxt:Proof.context) (ornode:ornode) =
((*
Expand All @@ -72,8 +66,6 @@ fun is_worth_proving (ctxt:Proof.context) (ornode:ornode) =
is_some (try (Syntax.check_term ctxt) (#lemma_term ornode))
andalso
#gg_parent_not_finished ornode
andalso
not (#refuted ornode): bool
andalso
is_none (#proof ornode));

Expand All @@ -90,7 +82,6 @@ fun mk_ornode (is_final_goal:is_final_goal) (goal:term) =
lemma_term = goal,
proof = NONE,
proof_id = NONE,
refuted = false,
proved_completely = false,(*We do not search for a counterexample before checking for duplication.*)
gg_parent_not_finished = true
}: ornode
Expand All @@ -112,7 +103,6 @@ fun update_gg_parent_not_finished ({
lemma_term : term,
proof : string option,
proof_id : int option,
refuted : bool,
proved_completely: bool,...
}: ornode) (gg_parent_not_finished: bool) =
{
Expand All @@ -122,7 +112,6 @@ fun update_gg_parent_not_finished ({
lemma_term = lemma_term,
proof = proof,
proof_id = proof_id,
refuted = refuted,
proved_completely = proved_completely,
gg_parent_not_finished = gg_parent_not_finished
}: ornode;
Expand All @@ -135,7 +124,6 @@ fun update_proved_completely ({
lemma_term : term,
proof : string option,
proof_id : int option,
refuted : bool,
gg_parent_not_finished: bool,...
}: ornode) =
{
Expand All @@ -145,7 +133,6 @@ fun update_proved_completely ({
lemma_term = lemma_term,
proof = proof,
proof_id = proof_id,
refuted = refuted,
proved_completely = true,
gg_parent_not_finished = gg_parent_not_finished
}: ornode;
Expand All @@ -156,7 +143,6 @@ fun update_proof_n_proof_id (proof:string) ({
branch : bool,
lemma_name : string,
lemma_term : term,
refuted : bool,
proved_completely : bool,
gg_parent_not_finished: bool,...
}: ornode) =
Expand All @@ -169,33 +155,10 @@ fun update_proof_n_proof_id (proof:string) ({
(*TODO: This should be synchronized.*)
proof_id = (Unsynchronized.inc TBC_Utils.proof_id_counter;
SOME (Unsynchronized.! TBC_Utils.proof_id_counter)),
refuted = refuted,
proved_completely = proved_completely: bool,
gg_parent_not_finished = gg_parent_not_finished
}: ornode;

(* update_refuted *)
fun update_refuted ({
final_goal : bool,
branch : bool,
lemma_name : string,
lemma_term : term,
proof : string option,
proof_id : int option,
proved_completely : bool,
gg_parent_not_finished: bool,...
}: ornode) =
{
final_goal = final_goal,
branch = branch,
lemma_name = lemma_name,
lemma_term = lemma_term,
proof = proof,
proof_id = proof_id,
refuted = true,
proved_completely = proved_completely: bool,
gg_parent_not_finished = gg_parent_not_finished
}: ornode;

(* update_branch *)
fun update_branch ({
Expand All @@ -204,7 +167,6 @@ fun update_branch ({
lemma_term : term,
proof : string option,
proof_id : int option,
refuted : bool,
proved_completely : bool,
gg_parent_not_finished: bool,...
}: ornode) =
Expand All @@ -215,7 +177,6 @@ fun update_branch ({
lemma_term = lemma_term,
proof = proof,
proof_id = proof_id,
refuted = refuted,
proved_completely = proved_completely: bool,
gg_parent_not_finished = gg_parent_not_finished
}: ornode;
Expand Down
32 changes: 9 additions & 23 deletions Abduction/Proof_By_Abduction.ML
View file
Original file line number Diff line number Diff line change
Expand Up @@ -42,24 +42,9 @@ fun seeds_to_updated_graph (or_key:key) (seeds: seeds_of_andnode) (pst:Proof.sta
val graph_w_ornode_is_now_branch = update_branch or_key graph : abduction_graph;
val (new_andnds_keys, graph_w_andnodes) = add_andnodes pairs_to_mk_andnodes graph_w_ornode_is_now_branch : (keys * abduction_graph);
val graph_w_ornodes(*expensive*) = fold (process_andkey_and_add_child_ornodes pst) new_andnds_keys graph_w_andnodes: abduction_graph;

fun one_of_ands_child_nodes_is_refuted (and_key:key) (graph:abduction_graph) =
let
val child_ors = PGraph.immediate_succs graph and_key: keys;
val is_refuted = exists (is_refuted graph) child_ors: bool;
val result_graph = if is_refuted
then PGraph.map_node and_key Update_Abduction_Node.update_refuted graph
else graph;
in
result_graph:abduction_graph
end;

val graph_w_refuted_andnodes = fold one_of_ands_child_nodes_is_refuted new_andnds_keys graph_w_ornodes: abduction_graph;
fun seed_is_refuted ({andnode_key,...}:seed_of_andnode) = is_refuted graph_w_refuted_andnodes andnode_key : bool;
val seeds_not_refuted_yet = filter_out seed_is_refuted seeds : seeds_of_andnode;
val seeds_of_newly_added_andnodes = filter (fn seed => member equal_keys new_andnds_keys (#andnode_key seed)) seeds_not_refuted_yet: seeds_of_andnode;
val seeds_of_newly_added_andnodes = filter (fn seed => member equal_keys new_andnds_keys (#andnode_key seed)) seeds : seeds_of_andnode;
(*add_or2and_edge is very expensive*)
val graph_w_ornodes_n_or2add_edges = fold (SOAN.add_or2and_edge or_key) seeds_of_newly_added_andnodes graph_w_ornodes : abduction_graph;
val graph_w_ornodes_n_or2add_edges = fold (SOAN.add_or2and_edge or_key) seeds_of_newly_added_andnodes graph_w_ornodes: abduction_graph;
in
graph_w_ornodes_n_or2add_edges: abduction_graph
end;
Expand Down Expand Up @@ -87,13 +72,14 @@ fun work_on_ornode (or_key as (Or_N, [lemma_term]):key) (pst:state, graph:abduct
val seeds_from_tactics = SOAN.apply_Extend_Leaf_to_pst_to_get_seeds_of_andnodes pst_to_prove: seeds_of_andnode;

(*conjecturing*)
val seeds_from_conjectures = All_Top_Down_Conjecturing.top_down_conjectures (Proof.context_of pst) lemma_term
|> map snd (*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.*)
|> SOAN.conjectures_to_seeds_of_andnode (pst, pst_to_prove): seeds_of_andnode;
val filtered_seeds = SOAN.filter_out_bad_seeds_of_andnode lemma_term pst graph (seeds_from_conjectures @ seeds_from_tactics): seeds_of_andnode;
val seeds_from_conjectures = All_Top_Down_Conjecturing.top_down_conjectures (Proof.context_of pst) lemma_term
|> map snd (*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.*)
|> SOAN.conjectures_to_seeds_of_andnode (pst, pst_to_prove): seeds_of_andnode;
val filtered_seeds = SOAN.filter_out_bad_seeds_of_andnode lemma_term pst graph (seeds_from_conjectures @ seeds_from_tactics): seeds_of_andnode;
val seeds_wo_counterexample = filter_out (Seed_Of_And_Node.seed_of_andnode_has_counterexample pst) filtered_seeds: seeds_of_andnode;
in
(*seeds_to_updated_graph is very expensive*)
(pst, seeds_to_updated_graph or_key filtered_seeds pst graph)
(pst, seeds_to_updated_graph or_key seeds_wo_counterexample pst graph)
end
end
| work_on_ornode _ _ = error "work_on_ornode failed. Not an Or_N.";
Expand All @@ -110,7 +96,7 @@ fun loop (counter:int) (pst:state, graph: abduction_graph) =
let
val _ = tracing ("==== In loop. Counter is: " ^ Int.toString counter ^ " =====");
val ctxt = Proof.context_of pst;
val orkeys_worth_expanding = keys_tobe_expanded_in ctxt graph: keys;
val orkeys_worth_expanding = orkeys_tobe_expanded_in ctxt graph: keys;
val _ = tracing ("The number of keys worth expanding is:" ^ Int.toString (length orkeys_worth_expanding));
val _ = tracing "They are:"
val _ = map (print_key ctxt) orkeys_worth_expanding
Expand Down
10 changes: 8 additions & 2 deletions Abduction/Seed_Of_And_Node.ML
View file
Original file line number Diff line number Diff line change
Expand Up @@ -29,6 +29,8 @@ val add_or2and_edge : key -> seed_of_andnode ->
val filter_out_bad_seeds_of_andnode: term (*parental or-node*) -> Proof.state -> abduction_graph -> seeds_of_andnode -> seeds_of_andnode
val conjectures_to_seeds_of_andnode: (Proof.state (*default pst*) * Proof.state (*chained pst to proved the parental ornode*)) -> terms -> seeds_of_andnode;

val seed_of_andnode_has_counterexample: Proof.state -> seed_of_andnode -> bool;

end;

(*** Seed_Of_And_Node ***)
Expand Down Expand Up @@ -85,8 +87,7 @@ fun apply_Extend_Leaf_to_pst_to_get_seeds_of_andnodes (pst:Proof.state) =
val key = (And_N, nonempty_subgs): key;
val value = Abduction_Node.And_Node
({subgoals = nonempty_subgs,
proved_completely = false,
refuted = false}: And_Node.andnode): abduction_node;
proved_completely = false}: And_Node.andnode): abduction_node;
in
{proof = Or2And_Edge.Tactic pscript, andnode_key = key, value = value, state = pst}: seed_of_andnode
end;
Expand Down Expand Up @@ -221,4 +222,9 @@ fun conjectures_to_seeds_of_andnode (pst:Proof.state, pst_to_prove_ornode:Proof.
result
end;

fun seed_of_andnode_has_counterexample (pst:Proof.state) ({andnode_key,...}:seed_of_andnode) =
case andnode_key of
(And_N, cnjctrs) => Shared_State.any_of_these_is_refuted pst cnjctrs
| _ => error "seed_of_andnode_has_counterexample failed. Not a seed_of_andnode."

end;
Loading

0 comments on commit 565e1c3

Please sign in to comment.