Abduction: sort active orkeys based on importance.

TODOs:
- implement bests-first expansion.
- adjust importance based on the results of Nitpick (quasi_genuineN and potentialN).

Abduction/Abduction_Graph.ML

@@ -43,6 +43,7 @@ val is_branch     : abduction_graph -> key -> bool;
 val is_ornode     : key -> bool;
 val is_andnode    : key -> bool;
 val is_or2and_edge: key -> bool;
+val importance    : abduction_graph -> key -> real;
 
 (* query on abduction_node for ornode and andnode *)
 val is_proved_completely                         : abduction_graph -> key -> bool;
@@ -52,9 +53,12 @@ val is_final_goal                                : abduction_graph -> key -> boo
 val lemma_name_of                                : abduction_graph -> key -> string;
 val proof_of                                     : abduction_graph -> key -> strings;
 val proof_id_of                                  : abduction_graph -> key -> int option;
+val compute_importance_of_ornode                 : abduction_graph -> key -> real;
+val sort_orkeys_based_on_importance              : abduction_graph -> keys -> keys;
 
 val grand_parents                                : abduction_graph -> key -> keys;
 val grand_children                               : abduction_graph -> key -> keys;
+val great_grand_parents                          : abduction_graph -> key -> keys;
 val all_gg_parents_are_proved                    : abduction_graph -> key -> bool;
 
 (* query on abduction_node for or2and_edge *)
@@ -183,6 +187,29 @@ fun is_andnode (And_N, _) = true
 fun is_or2and_edge (O2A_E _, _) = true
   | is_or2and_edge  _           = false;
 
+(* importance *)
+fun importance (ag:abduction_graph) (orkey as (Or_N, _)) =
+     PGraph.get_node ag orkey |> Abduction_Node.importance
+  | importance (ag:abduction_graph) (edge_key as (O2A_E _, _)) =
+     PGraph.get_node ag edge_key |> Abduction_Node.importance
+  | importance (ag:abduction_graph) (andkey as (And_N, _)) =
+let
+  val parents_of             = PGraph.immediate_preds ag;
+  val parent_or2and_edges    = parents_of andkey: keys;
+  fun computation f x        = (x, f x);
+  val edge_and_ornodes_pairs = map (computation parents_of) parent_or2and_edges: (key * keys) list;
+  val ornodess               = map snd edge_and_ornodes_pairs: keys list;
+  val _ = if forall (fn ornodes => length ornodes = 1) ornodess then () else error "importance_of_andnode failed";
+  val edge_and_ornode_pairs  = map (apsnd hd) edge_and_ornodes_pairs: (key * key) list;
+  val importance_pairs       = map (apply2 (importance ag)) edge_and_ornode_pairs: (real * real) list;
+  val importances            = map (fn (imp1, imp2) => imp1 * imp2) importance_pairs: real list;
+  val importance             = case Utils.reals_to_max_option importances of
+                                 NONE     => error "importance in Abduction_Graph failed. No ancestral pairs."
+                               | SOME max => max: real;
+in
+  importance
+end;
+
 (* is_proved_completely *)
 fun is_proved_completely (graph:abduction_graph) (key:key): bool =
   PGraph.get_node graph key |> Abduction_Node.is_proved_completely;
@@ -274,6 +301,28 @@ fun is_worth_proving (ctxt:Proof.context) (graph:abduction_graph) (key:key)  =
 (* proof_id_of *)
 fun proof_id_of (graph:abduction_graph) (key:key) = PGraph.get_node graph key |> Abduction_Node.proof_id_of: int option;
 
+(* compute_importance_of_ornode *)
+fun compute_importance_of_ornode (ag:abduction_graph) (orkey as (Or_N, _)) =
+    let
+      val parent_andkeys         = PGraph.immediate_preds ag orkey: keys;
+      val importances_of_parents = map (importance ag) parent_andkeys: real list;
+      val importance             = case Utils.reals_to_max_option importances_of_parents of
+                                     NONE     => error "compute_importance_of_ornode. No ancestral andnode."
+                                   | SOME max => max: real;
+    in
+      importance
+    end
+  | compute_importance_of_ornode _ _ = error "compute_importance_of_ornode failed. It expects a key of an or-node.";
+
+(* sort_orkeys_based_on_importance *)
+fun sort_orkeys_based_on_importance (ag:abduction_graph) (keys:keys) =
+  let
+    fun key_compare (key1, key2) = Real.compare (importance ag key1, importance ag key2);
+    val sorted_keys = sort key_compare keys |> rev;
+  in
+    sorted_keys: keys
+  end;
+
 (* proof_of *)
 fun proof_of (graph:abduction_graph) (key:key) =
   let

Abduction/Abduction_Node.ML

@@ -23,6 +23,7 @@ datatype abduction_node =
 val is_ornode                                    : abduction_node -> bool;
 val is_andnode                                   : abduction_node -> bool;
 val is_or2and_edge                               : abduction_node -> bool;
+val importance                                   : abduction_node -> real;
 
 (* query on abduction_node for ornode and andnode *)
 val is_proved_completely                         : abduction_node -> bool;
@@ -36,7 +37,7 @@ val lemma_name_of                                : abduction_node -> string;
 val is_worth_proving                             : Proof.context -> abduction_node -> bool;
 
 (* query on abduction_node for or2and_edge *)
-val or2and_edge_to_proof         : abduction_node -> strings;
+val or2and_edge_to_proof                         : abduction_node -> strings;
 
 (* destructors of abduction_node *)
 val dest_Or_Node  : abduction_node -> ornode;
@@ -78,6 +79,13 @@ fun is_andnode (And_Node _) = true
 fun is_or2and_edge (Or_To_And _) = true
   | is_or2and_edge _ = false;
 
+(* importance *)
+fun importance (Or_To_And {importance,...}) = importance
+  | importance (Or_Node   {importance,...}) = (case importance of
+      NONE => (warning "Importance is not defined for this Or_Node!"; 0.0)
+    | SOME imp => imp)
+  | importance _ = error "importance in Abduction_Node failed. And_Node does not carry importance explicilty";
+
 (* is_proved_completely *)
 fun is_proved_completely (Or_Node  nd) = #proved_completely nd
   | is_proved_completely (And_Node nd) = #proved_completely nd

Abduction/Or2And_Edge.ML

@@ -39,7 +39,7 @@ fun proof_is_from_tactic (Tactic _) = true
 type or2and_edge = {
   how_to_get_andnodes_from_ornode: how_to_get_andnodes_from_ornode,
   proof_of_ornode_assmng_andnodes: strings,
-  importance                     : real}
+  importance                     : real};
 
 (* or2and_edge_to_proof *)
 fun or2and_edge_to_proof ({proof_of_ornode_assmng_andnodes, ...}:or2and_edge) = proof_of_ornode_assmng_andnodes;

Abduction/Or_Node.ML

@@ -27,6 +27,7 @@ val update_proved_completely     : ornode -> ornode;
 val update_proof_n_proof_id      : strings -> ornode -> ornode;
 val update_is_branch             : ornode -> ornode;
 val update_importance            : real -> ornode -> ornode;
+val update_imp_if_this_is_larger : real -> ornode -> ornode;
 
 end;
 
@@ -213,4 +214,13 @@ fun update_importance (importance:real) ({
   importance             = SOME importance
 }: ornode;
 
+(* update_imp_if_this_is_larger *)
+fun update_imp_if_this_is_larger (new_imp:real) (ornode as {importance: real option, ...}: ornode) =
+  case importance of
+    NONE => update_importance new_imp ornode
+  | SOME (old_imp:real) =>
+      if   old_imp < new_imp
+      then update_importance new_imp ornode
+      else ornode;
+
 end;

Abduction/Proof_By_Abduction.ML

@@ -173,10 +173,12 @@ fun loop (counter:int) (max_depth:int) (start:Timing.start)
       val ctxt                   = Proof.context_of pst;
       val abduction_graph        = Synchronized.value synched_agraph: Abduction_Graph.abduction_graph;
       val orkeys_worth_expanding = orkeys_tobe_expanded_in ctxt abduction_graph: keys;
-      val _                      = tracing ("The number of keys worth expanding is:" ^ Int.toString (length orkeys_worth_expanding) ^ ".");
+      val sorted_orkeys          = sort_orkeys_based_on_importance abduction_graph orkeys_worth_expanding: keys;
+      val _                      = tracing ("The number of keys worth expanding is:" ^ Int.toString (length sorted_orkeys) ^ ".");
       val _                      = tracing "They are:"
-      val _                      = map (print_key ctxt) orkeys_worth_expanding
-      val some_orkey             = Par_List.find_some (expand_ornode_if_original_goral_is_unproved_w_timeout start (pst, synched_agraph, refutation, term2name, proved_ors)) orkeys_worth_expanding: key option;
+      val _                      = map (print_key ctxt) sorted_orkeys
+      val expand_ornode          = expand_ornode_if_original_goral_is_unproved_w_timeout start (pst, synched_agraph, refutation, term2name, proved_ors): Abduction_Graph.key -> bool;
+      val some_orkey             = Par_List.find_some expand_ornode sorted_orkeys: key option;
       val solved                 = is_some some_orkey: bool;
       val _                      = tracing ("We have " ^ (if solved then "already solved" else "not solve") ^ " the final goal.");
     in

Abduction/Seed_Of_Or2And_Edge.ML

@@ -67,12 +67,12 @@ fun seed_is_from_tactic ({proof, ...}) = Or2And_Edge.proof_is_from_tactic proof:
 fun apply_PSL_to_get_seeds_of_or2and_edges (synched_term2string:SS.synched_term2string_table) (pst:Proof.state) =
   let
     val ctxt          = Proof.context_of pst;
-    val extend_str    = PSL_Interface.lookup ctxt "Extend_Leaf" |> the                      : PSL_Interface.strategy;
-    val timeouts      = {overall = 60.0, hammer = 8.0, quickcheck = 1.0, nitpick = 2.0}     : TBC_Utils.timeouts;
-    val result_seq    = TBC_Utils.psl_strategy_to_monadic_tactic timeouts extend_str pst [] : (Dynamic_Utils.log * Proof.state) Seq.seq;
-    val result_list   = Seq.list_of result_seq                                              : (Dynamic_Utils.log * Proof.state) list;
-    val script_n_psts = map (apfst Dynamic_Utils.mk_apply_scripts_for_abduction) result_list: (strings * Proof.state) list;
-    fun mk_proof_key_value (pscript, pst) =
+    val extend_str    = PSL_Interface.lookup ctxt "Extend_Leaf" |> the                     : PSL_Interface.strategy;
+    val timeouts      = {overall = 60.0, hammer = 8.0, quickcheck = 1.0, nitpick = 2.0}    : TBC_Utils.timeouts;
+    val result_seq    = TBC_Utils.psl_strategy_to_monadic_tactic timeouts extend_str pst []: (Dynamic_Utils.log * Proof.state) Seq.seq;
+    val result_list   = Seq.list_of result_seq                                             : (Dynamic_Utils.log * Proof.state) list;
+    val pairs_n_psts  = map (apfst Dynamic_Utils.log_to_script_n_importance) result_list   : ((strings * real) * Proof.state) list;
+    fun mk_proof_key_value ((pscript, importance), pst) =
         let
           val subgs              = Isabelle_Utils.pst_to_subgs pst
           val subgs_wo_meta_uni  = map TDU.strip_outermost_meta_quantifiers subgs: terms;
@@ -87,12 +87,12 @@ fun apply_PSL_to_get_seeds_of_or2and_edges (synched_term2string:SS.synched_term2
                        then NONE
                        else SOME {proof      = Or2And_Edge.Tactic pscript,
                                   new_goals  = nonempty_subgs,
-                                  importance = 1.0}(*TODO*)
+                                  importance = importance};
         in
           result: seed_of_or2and_edge option
         end;
   in
-    List.mapPartial mk_proof_key_value script_n_psts: seeds_of_or2and_edge
+    List.mapPartial mk_proof_key_value pairs_n_psts: seeds_of_or2and_edge
   end;
 
 
@@ -147,7 +147,7 @@ fun filter_out_bad_seeds_from_tactic (parent_or:term) (refutation:SS.synched_ter
 fun conjecture_to_seed_of_or2and_edge (conjectures:(string * term) list): seed_of_or2and_edge =
   {new_goals  = conjectures: (string * term) list,
    proof      = Or2And_Edge.Conjecture: how_to_get_andnodes_from_ornode,
-   importance = 0.95};(*TODO: We should use different importance for different explicit conjectures?*)
+   importance = 0.95};(*TODO: magic number.*)
 
 fun conjectures_to_seed_of_or2and_edge (term2name:SS.synched_term2string_table) (pst:Proof.state) (conjectures_w_name: (string * term) list) =
   let
@@ -174,8 +174,7 @@ fun seed_has_counterexample (refutation:SS.synched_term2bool_table) (pst:Proof.s
 
 fun prove_goal_assuming_conjectures (pst:Proof.state) ((Or_N, [orterm]): key)(*parent node*)
      ({new_goals : (string * term) list,
-       proof     : how_to_get_andnodes_from_ornode,
-       importance: real}: seed_of_or2and_edge)(*child nodes*) =
+       proof     : how_to_get_andnodes_from_ornode,...}: seed_of_or2and_edge)(*child nodes*) =
    let
      fun register_thm_in_lthy (name:string) (thm:thm) (lthy:local_theory): local_theory =
          Local_Theory.note ((Binding.name name, []), [thm]) lthy |> snd: local_theory;
@@ -271,9 +270,11 @@ fun add_nodes_and_edges_to_graph (pst:Proof.state) (parent_ornd:key) (synched_ag
     val _                  = map add_child_ornode used_conjectures: unit list;
     (*step 7*)
     val _                  = SS.add_edges_from_andnode_to_ornodes added_andnode_key synched_agraph: unit;
-    val connected_orkeys   = map (fn or_term => (Or_N, [or_term])) and_node_terms: keys;
     (*step 8: TODO: add the importance of the child-or-nodes.*)
-    val _                  = SS.update_after_connecting_andnd_to_existing_ornd ctxt synched_agraph connected_orkeys: unit list;
+    val child_orkeys       = map (fn or_term => (Or_N, [or_term])) and_node_terms: keys;
+    val _                  = map (SS.update_importance_of_ornode synched_agraph) child_orkeys: unit list;
+    (*step 9*)
+    val _                  = SS.update_after_connecting_andnd_to_existing_ornd ctxt synched_agraph child_orkeys: unit list;
   in
     ()
   end;
@@ -289,6 +290,7 @@ fun add_nodes_and_edges_to_graph (pst:Proof.state) (parent_ornd:key) (synched_ag
  * step 6. add child-or-nodes that correspond to the sub-goals or used conjectures in the and-node.
  * step 7. connect the child-or-nodes to the and-node.
  * step 8. TODO: add the importance of the child-or-nodes.
+ * step 9. update the values of or-nodes and and-nodes in the graph.
  *)
 fun abduction_for_tactic_based_conjectures (pst:Proof.state) (parent_or:key) (seeds: seeds_of_or2and_edge) (sagraph:SS.synched_abduction_graph) =
   let

Abduction/Shared_State.ML

@@ -39,6 +39,7 @@ val add_edges_from_andnode_to_ornodes             : Abduction_Graph.key -> synch
 val update_proved_completely                      : Abduction_Graph.key -> synched_abduction_graph -> unit;
 val update_proof_n_proof_id                       : (*proof*)strings -> (*or*)Abduction_Graph.key -> synched_abduction_graph -> unit;
 val update_after_proving_ornode                   : strings -> Abduction_Graph.key -> Proof.context -> synched_abduction_graph -> unit;
+val update_importance_of_ornode                   : synched_abduction_graph -> Abduction_Graph.key -> unit;
 val update_after_connecting_andnd_to_existing_ornd: Proof.context -> synched_abduction_graph -> (*or_key*)Abduction_Graph.keys -> unit list;
 
 val final_goal_proved_completely     : synched_abduction_graph -> bool;
@@ -194,6 +195,9 @@ fun update_proof_n_proof_id (proof:strings) (key:AG.key) (sagraph:synched_abduct
 fun update_after_proving_ornode (proof:strings) (orkey:AG.key) (ctxt:Proof.context) (sagraph:synched_abduction_graph) =
   Synchronized.change sagraph (UAG.update_after_proving_ornode proof orkey ctxt): unit;
 
+fun update_importance_of_ornode (sagraph:synched_abduction_graph) (orkey:AG.key) =
+  Synchronized.change sagraph (UAG.update_importance_of_ornode orkey): unit;
+
 fun update_after_connecting_andnd_to_existing_ornd' (ctxt:Proof.context) (sagraph:synched_abduction_graph) (orkey:AG.key) =
   Synchronized.change sagraph (UAG.update_after_connecting_andnd_to_existing_ornd orkey ctxt): unit;
 

Abduction/Update_Abduction_Graph.ML

@@ -23,6 +23,8 @@ val update_proof_n_proof_id           : (*proof*)strings -> (*or*)key -> update_
 (* update of abduction_graph *)
 val update_is_branch                  : key -> update_abduction_graph;
 val update_importance                 : key -> real -> update_abduction_graph;
+val update_imp_if_this_is_larger      : key -> real -> update_abduction_graph;
+val update_importance_of_ornode       : key -> update_abduction_graph;
 
 val update_after_proving_ornode       : (*proof*)strings -> (*or*)key -> Proof.context -> update_abduction_graph;
 val update_after_connecting_andnd_to_existing_ornd: (*or*)key -> Proof.context -> update_abduction_graph;
@@ -37,29 +39,40 @@ end;
 structure Update_Abduction_Graph: UPDATE_ABDUCTION_GRAPH =
 struct
 
-open Abduction_Node;
 open Abduction_Graph;
+structure UAN = Update_Abduction_Node;
 
 type update_abduction_graph = abduction_graph -> abduction_graph;
 
 fun update_proved_completely (key:key) (ag:abduction_graph) =
-    PGraph.map_node key (Update_Abduction_Node.update_proved_completely) ag: abduction_graph;
+    PGraph.map_node key (UAN.update_proved_completely) ag: abduction_graph;
 
 fun update_proof_n_proof_id (prf:strings) (key:key) (ag:abduction_graph) =
-    PGraph.map_node key (Update_Abduction_Node.update_proof_n_proof_id prf) ag: abduction_graph;
+    PGraph.map_node key (UAN.update_proof_n_proof_id prf) ag: abduction_graph;
 
 fun update_is_branch (key:key) (graph:abduction_graph) =
-    PGraph.map_node key Update_Abduction_Node.update_is_branch graph: abduction_graph;
+    PGraph.map_node key UAN.update_is_branch graph: abduction_graph;
 
 fun update_importance (key:key) (imp:real) (graph:abduction_graph) =
-    PGraph.map_node key (Update_Abduction_Node.update_importance imp) graph: abduction_graph;
+    PGraph.map_node key (UAN.update_importance imp) graph: abduction_graph;
+
+fun update_imp_if_this_is_larger (key:key) (imp:real) (graph:abduction_graph) =
+    PGraph.map_node key (UAN.update_imp_if_this_is_larger imp) graph: abduction_graph;
+
+fun update_importance_of_ornode (orkey:key) (graph:abduction_graph) =
+  let
+    val importance = compute_importance_of_ornode graph orkey: real;
+    val new_graph  = PGraph.map_node orkey (UAN.update_importance importance) graph: abduction_graph;
+  in
+    new_graph
+  end;
 
 local
 
 fun update_gg_parent_not_finished_of_or_key (key as (Or_N, _):key) (gr:abduction_graph): abduction_graph =
     let
       val does_need_proof = not (all_gg_parents_are_proved gr key)                             : bool;
-      val update          = Update_Abduction_Node.update_gg_parent_not_finished does_need_proof: abduction_node -> abduction_node;
+      val update          = UAN.update_gg_parent_not_finished does_need_proof: abduction_node -> abduction_node;
     in
       PGraph.map_node key update gr
     end
@@ -81,11 +94,11 @@ fun update_gg_parent_not_finished (graph:abduction_graph) =
 
 (* update_proof_n_proof_id *)
 fun update_proof_n_proof_id (proof:strings) (key:key) (graph:abduction_graph) =
-    PGraph.map_node key (Update_Abduction_Node.update_proof_n_proof_id proof) graph: abduction_graph;
+    PGraph.map_node key (UAN.update_proof_n_proof_id proof) graph: abduction_graph;
 
 (* update_proved_completely *)
 fun update_proved_completely_of_node (key:key) (graph:abduction_graph) =
-    PGraph.map_node key Update_Abduction_Node.update_proved_completely graph: abduction_graph;
+    PGraph.map_node key UAN.update_proved_completely graph: abduction_graph;
 
 (* forall_at_least_one *)
 fun forall_at_least_one assertion xs = forall assertion xs andalso (length xs > 0);

Abduction/Update_Abduction_Node.ML

@@ -21,6 +21,7 @@ val update_proved_completely     : update_abduction_node;
 val update_proof_n_proof_id      : strings -> update_abduction_node;
 val update_is_branch             : update_abduction_node;
 val update_importance            : real -> update_abduction_node;
+val update_imp_if_this_is_larger : real -> update_abduction_node;
 
 end;
 
@@ -54,4 +55,8 @@ fun update_is_branch (Or_Node ornode) = Or_Node.update_is_branch ornode |> Or_No
 fun update_importance (imp:real) (Or_Node ornode) = Or_Node.update_importance imp ornode |> Or_Node
   | update_importance  _          _               = error "update_importance failed!";
 
+(* update_imp_if_this_is_larger *)
+fun update_imp_if_this_is_larger (imp:real) (Or_Node ornode) = Or_Node.update_imp_if_this_is_larger imp ornode |> Or_Node
+  | update_imp_if_this_is_larger  _          _               = error "update_importance failed!";
+
 end;