From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Mon, 2 Oct 2006 15:17:01 +0000 (+0000)
Subject: 50 steps on goal are fine for irrat2
X-Git-Tag: make_still_working~6816
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;ds=sidebyside;h=67754d917af96623334ca9b8c1a16632d6c89391;p=helm.git

50 steps on goal are fine for irrat2
---

diff --git a/helm/software/components/tactics/auto.ml b/helm/software/components/tactics/auto.ml
index 2db8cc001..c65826a4f 100644
--- a/helm/software/components/tactics/auto.ml
+++ b/helm/software/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 "<CACHE>";
   prerr_endline (cache_print context cache);
   prerr_endline "</CACHE>";
+*)
   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