From: Andrea Asperti <andrea.asperti@unibo.it>
Date: Fri, 29 Jan 2010 10:16:03 +0000 (+0000)
Subject: Nuova gestione della width.
X-Git-Tag: make_still_working~3086
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=78be7f337d5bb2753295a329952b0e9b8a15773a;p=helm.git

Nuova gestione della width.
---

diff --git a/helm/software/components/ng_tactics/nnAuto.ml b/helm/software/components/ng_tactics/nnAuto.ml
index 6044f3a34..fdf2d2ea3 100644
--- a/helm/software/components/ng_tactics/nnAuto.ml
+++ b/helm/software/components/ng_tactics/nnAuto.ml
@@ -94,13 +94,14 @@ let solve fast status eq_cache goal =
   let gty = NCicUntrusted.apply_subst subst ctx gty in
   let build_status (pt, _, metasenv, subst) =
     try
-      print (lazy ("refining: "^(NCicPp.ppterm ctx subst metasenv pt)));
+      debug_print (lazy ("refining: "^(NCicPp.ppterm ctx subst metasenv pt)));
       let stamp = Unix.gettimeofday () in 
       let metasenv, subst, pt, pty =
 	NCicRefiner.typeof status
        	 (* (status#set_coerc_db NCicCoercion.empty_db) *)
 	  metasenv subst ctx pt None in
-	print (lazy ("synt: "^(NCicPp.ppterm ctx subst metasenv pty)));
+	debug_print (lazy ("refined: "^(NCicPp.ppterm ctx subst metasenv pt)));
+	debug_print (lazy ("synt: "^(NCicPp.ppterm ctx subst metasenv pty)));
 	let metasenv, subst =
 	  NCicUnification.unify status metasenv subst ctx gty pty 
 	(* the previous code is much less expensive than directly refining
@@ -1425,9 +1426,9 @@ let try_candidate ?(smart=0) flags depth status eq_cache t =
       with Error _ -> 
 	smart_apply_auto ("",0,t) eq_cache status in 
   let og_no = openg_no status in 
-    if og_no > flags.maxwidth || 
+    if (* og_no > flags.maxwidth || *)
       (depth = flags.maxdepth && og_no <> 0) then
-	(debug_print ~depth (lazy "pruned immediately"); None)
+	(print ~depth (lazy "pruned immediately"); None)
    else
      (incr candidate_no;
       Some ((!candidate_no,t),status))
@@ -1492,7 +1493,10 @@ let applicative_case depth signature status flags gty (cache:cache) =
   debug_print ~depth
     (lazy ("smart candidates: " ^ 
 	     string_of_int (List.length smart_candidates)));
-  let sm = if is_eq then 0 else 2 in
+(*
+  let sm = 0 in 
+  let smart_candidates = [] in *)
+  let sm = if is_eq then 0 else 2 in 
   let elems = 
     List.fold_left 
       (fun elems cand ->
@@ -1772,7 +1776,10 @@ auto_main flags signature (cache:cache) depth status: unit =
   match goals with
     | [] -> raise (Proved status)
     | orig::_ ->
-        let branch = List.length(goals)>1 in
+	let ng = List.length goals in 
+        if ng > flags.maxwidth then 
+	  (print (lazy "FAIL WIDTH"); raise (Gaveup IntSet.empty))
+        else let branch = ng>1 in
 	if depth = flags.maxdepth then raise (Gaveup IntSet.empty)
         else
 	let status = 
@@ -1804,7 +1811,9 @@ auto_main flags signature (cache:cache) depth status: unit =
 		 else depth+1, loop_cache in
                debug_print (~depth:depth') 
 		 (lazy ("Case: " ^ CicNotationPp.pp_term t));
-	       try auto_clusters flags signature loop_cache
+	       let flags' = 
+		 {flags with maxwidth = flags.maxwidth - ng +1} in 
+	       try auto_clusters flags' signature loop_cache
 		 depth' status; unsat
                with 
 		 | Proved status ->
@@ -1859,7 +1868,7 @@ let auto_tac ~params:(_univ,flags) status =
 *)
   let depth = int "depth" flags 3 in 
   let size  = int "size" flags 10 in 
-  let width = int "width" flags (3+List.length goals) in 
+  let width = int "width" flags 4 (* (3+List.length goals)*) in 
   (* XXX fix sort *)
   let goals = List.map (fun i -> (i,P)) goals in
   let signature = () in