From 74873bc65100f11036fc3a7ec6f13d999de631a8 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Mon, 2 Oct 2006 15:17:01 +0000 Subject: [PATCH] 50 steps on goal are fine for irrat2 --- components/tactics/auto.ml | 11 +++++++---- 1 file changed, 7 insertions(+), 4 deletions(-) diff --git a/components/tactics/auto.ml b/components/tactics/auto.ml index 2db8cc001..c65826a4f 100644 --- a/components/tactics/auto.ml +++ b/components/tactics/auto.ml @@ -26,7 +26,7 @@ open AutoTypes;; open AutoCache;; -let debug_print s = () (* prerr_endline s;; *) +let debug_print s = () (*prerr_endline s;;*) (* {{{ *********** local given_clause wrapper ***********) @@ -59,7 +59,7 @@ let given_clause dbd ?tables maxm ?auto cache subst flags smart_flag status = let passive = Saturation.add_to_passive equalities passive in let goal_steps, saturation_steps, timeout = if flags.use_only_paramod then max_int,max_int,flags.timeout - else max 80 minsteps, minsteps, infinity + else max 50 minsteps, minsteps, infinity in active,passive,bag,cache,maxm,goal_steps,saturation_steps,timeout in @@ -274,9 +274,11 @@ let equational_case = let ppterm = ppterm context in prerr_endline ("PARAMOD SU: " ^ string_of_int goalno ^ " " ^ ppterm goalty ); +(* prerr_endline ""; prerr_endline (cache_print context cache); prerr_endline ""; +*) match given_clause dbd ?tables maxm ?auto cache subst flags false (fake_proof,goalno) with @@ -356,7 +358,8 @@ let is_equational_case goalty flags = (flags.use_only_paramod && ensure_equational goalty) ;; let cache_add_success sort cache k v = - if sort = P then cache_add_success cache k v else cache + if sort = P then cache_add_success cache k v else cache_remove_underinspection + cache k ;; let rec auto_main dbd tables maxm context flags elems cache = @@ -476,7 +479,7 @@ let rec auto_main dbd tables maxm context flags elems cache = depth fake_proof goalno goalty subst context flags with | Some elems, tables, cache, maxm -> - elems, tables, cache, maxm (* manca cache *) + elems, tables, cache, maxm | None, tables,cache,maxm -> applicative_case dbd tables maxm depth subst fake_proof goalno goalty metasenv context cache -- 2.39.2