/[svn]/types/types.ml
ViewVC logotype

Diff of /types/types.ml

Parent Directory Parent Directory | Revision Log Revision Log | View Patch Patch

revision 217 by abate, Tue Jul 10 17:13:41 2007 UTC revision 218 by abate, Tue Jul 10 17:15:29 2007 UTC
# Line 293  Line 293 
293    
294  exception NotEmpty  exception NotEmpty
295    
296    let trivially_empty d = d = empty
297    
298  let rec empty_rec d =  let rec empty_rec d =
299    if Assumptions.mem d !cache_false then false    if Assumptions.mem d !cache_false then false
300    else if Assumptions.mem d !memo then true    else if Assumptions.mem d !memo then true
# Line 324  Line 326 
326  (* This avoids explosion with huge rhs (+/- degenerated partitioning)  (* This avoids explosion with huge rhs (+/- degenerated partitioning)
327     May be slower when List.length right is small; could optimize     May be slower when List.length right is small; could optimize
328     this case... *)     this case... *)
329          if empty_rec (cap_t accu1 t1) || empty_rec (cap_t accu2 t2) then  (*      if empty_rec (cap_t accu1 t1) || empty_rec (cap_t accu2 t2) then*)
330    (* THIS IS NOT SOUND !!! *)
331            if trivially_empty (cap_t accu1 t1) ||
332               trivially_empty (cap_t accu2 t2) then
333            aux accu1 accu2 right            aux accu1 accu2 right
334          else          else
335            let accu1' = diff_t accu1 t1 in            let accu1' = diff_t accu1 t1 in
# Line 334  Line 339 
339      | [] -> raise NotEmpty      | [] -> raise NotEmpty
340    in    in
341    let (accu1,accu2) = cap_product left in    let (accu1,accu2) = cap_product left in
 (*  
   let right' = List.filter  
                  (fun (t1,t2) ->  
                     not  
                     (empty_rec (cap_t accu1 t1) || empty_rec (cap_t accu2 t2)  
                     )  
                  ) right in  
   if List.length right > 15 then (  
     Format.fprintf Format.std_formatter "[%i=>%i]@."  
                                     (List.length right) (List.length right');  
     Format.fprintf Format.std_formatter "(%a,%a)@."  
                                     !print_descr accu1  
                                     !print_descr accu2;  
     List.iter (fun (t1,t2) ->  
                  Format.fprintf Format.std_formatter "\ (%a,%a)@."  
                    !print_descr (descr t1)  
                    !print_descr (descr t2);  
               ) right  
   );  
   let right = right' in  
 *)  
   
342    (empty_rec accu1) || (empty_rec accu2) ||    (empty_rec accu1) || (empty_rec accu2) ||
343  (* OPT? It does'nt seem so ...  The hope was to return false quickly  (* OPT? It does'nt seem so ...  The hope was to return false quickly
344     for large right hand-side *)     for large right hand-side *)
# Line 536  Line 519 
519       (t,s) \ (t1,s1) = (t&t',s\s') | (t\t',s),       (t,s) \ (t1,s1) = (t&t',s\s') | (t\t',s),
520     don't call normal_aux *)     don't call normal_aux *)
521    
522    
523    let get ?(kind=`Normal) d =    let get ?(kind=`Normal) d =
524      match kind with      match kind with
525        | `Normal -> get_aux d.times        | `Normal -> get_aux d.times
Legend:
Removed from v.217  
changed lines
  Added in v.218
CVS Admin">CVS Admin
 ViewVC Help
Powered by ViewVC 1.1.5