Nuova gestione della width.

diff --git a/helm/software/components/ng_tactics/nnAuto.ml b/helm/software/components/ng_tactics/nnAuto.ml
index 6044f3a34399ad6bb4688b8e189779d54fcff349..fdf2d2ea3138130ca23aa7ecabeac40b0fc1fdb0 100644 (file)
--- 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