Abduction: better handling of the maximum number of decrementation.

checked.
data61 · Aug 18, 2023 · a7a05e0 · a7a05e0
1 parent 4645a23
commit a7a05e0
Show file tree

Hide file tree

Showing 3 changed files with 12 additions and 1 deletion.
diff --git a/Abduction/Abduction.thy b/Abduction/Abduction.thy
@@ -68,6 +68,8 @@ strategy Attack_On_Or_Node =
   ]
 
 setup\<open> Config.put_global Top_Down_Util.timeout_config (60.0 * 60.0 * 10.0) \<close>
+setup\<open> Config.put_global Top_Down_Util.limit_for_first_decrement 30 \<close>
+setup\<open> Config.put_global Top_Down_Util.limit_for_other_decrement 10 \<close>
 
 (* UI *)
 ML\<open> (*This part (the definitions of long_keyword, long_statement, and short_statement) are from

diff --git a/Abduction/Seed_Of_Or2And_Edge.ML b/Abduction/Seed_Of_Or2And_Edge.ML
@@ -371,7 +371,10 @@ fun decremental_abduction (pst:Proof.state) (parent_ornd:key) (conjectures:conje
     val _ = Abduction_Graph.print_key (Proof.context_of pst) parent_ornd;
     val _ = tracing' " decremental abduction starts";
     val _ = map snd conjectures |> map (tracing' o Isabelle_Utils.trm_to_string (Proof.context_of pst));
-    val max_number = if (Abduction_Graph.is_final_goal (Synchronized.value synched_agraph) parent_ornd) then 50 else 5;
+    val ctxt = Proof.context_of pst: Proof.context;
+    val max_number = if Abduction_Graph.is_final_goal (Synchronized.value synched_agraph) parent_ornd
+                     then Config.get ctxt Top_Down_Util.limit_for_first_decrement
+                     else Config.get ctxt Top_Down_Util.limit_for_other_decrement
     val _ = decremental max_number pst parent_ornd [conjectures] [] synched_agraph []: unit;
     val _ = tracing' " decremental abduction ends";
   in

diff --git a/Abduction/Top_Down_Util.ML b/Abduction/Top_Down_Util.ML
@@ -34,6 +34,8 @@ val mk_new_lemma_name                : Proof.context -> bool(*is_final_goal*) ->
 val term_compare                     : term * term -> order;
 val term_to_thm                      : Proof.context -> term -> thm;
 val timeout_config                   : real Config.T;
+val limit_for_first_decrement        : int Config.T;
+val limit_for_other_decrement        : int Config.T;
 
 end;
 
@@ -231,6 +233,10 @@ fun term_to_thm (ctxt:Proof.context) (cnjctr:term) =
 (*default timeout is 10 hours*)
 val timeout_config = Config.declare_real ("prove_timeout", \<^here>) (K (60.0 * 60.0 * 10.0)): real Config.T;
 
+val limit_for_first_decrement = Config.declare_int ("limit_for_first_decrement", \<^here>) (K 15): int Config.T;
+
+val limit_for_other_decrement = Config.declare_int ("limit_for_first_decrement", \<^here>) (K  5): int Config.T;
+
 end;