| 148 |
end |
end |
| 149 |
) |
) |
| 150 |
|
|
| 151 |
|
let print_descr = ref (fun _ _ -> assert false) |
| 152 |
|
|
| 153 |
(* |
(* |
| 154 |
let define n d = check d; define n d |
let define n d = check d; define n d |
| 155 |
*) |
*) |
| 254 |
and empty_rec_times_aux (left,right) = |
and empty_rec_times_aux (left,right) = |
| 255 |
let rec aux accu1 accu2 = function |
let rec aux accu1 accu2 = function |
| 256 |
| (t1,t2)::right -> |
| (t1,t2)::right -> |
| 257 |
|
(* This may avoid explosion with huge rhs ... |
| 258 |
|
May be slower when List.length right is small; could optimize |
| 259 |
|
this case... *) |
| 260 |
|
if empty_rec (cap_t accu1 t1) || empty_rec (cap_t accu2 t2) then |
| 261 |
|
aux accu1 accu2 right |
| 262 |
|
else |
| 263 |
let accu1' = diff_t accu1 t1 in |
let accu1' = diff_t accu1 t1 in |
| 264 |
if not (empty_rec accu1') then aux accu1' accu2 right; |
if not (empty_rec accu1') then aux accu1' accu2 right; |
| 265 |
let accu2' = diff_t accu2 t2 in |
let accu2' = diff_t accu2 t2 in |
| 267 |
| [] -> raise NotEmpty |
| [] -> raise NotEmpty |
| 268 |
in |
in |
| 269 |
let (accu1,accu2) = cap_product left in |
let (accu1,accu2) = cap_product left in |
| 270 |
|
(* |
| 271 |
|
let right' = List.filter |
| 272 |
|
(fun (t1,t2) -> |
| 273 |
|
not |
| 274 |
|
(empty_rec (cap_t accu1 t1) || empty_rec (cap_t accu2 t2) |
| 275 |
|
) |
| 276 |
|
) right in |
| 277 |
|
if List.length right > 15 then ( |
| 278 |
|
Format.fprintf Format.std_formatter "[%i=>%i]@." |
| 279 |
|
(List.length right) (List.length right'); |
| 280 |
|
Format.fprintf Format.std_formatter "(%a,%a)@." |
| 281 |
|
!print_descr accu1 |
| 282 |
|
!print_descr accu2; |
| 283 |
|
List.iter (fun (t1,t2) -> |
| 284 |
|
Format.fprintf Format.std_formatter "\ (%a,%a)@." |
| 285 |
|
!print_descr (descr t1) |
| 286 |
|
!print_descr (descr t2); |
| 287 |
|
) right |
| 288 |
|
); |
| 289 |
|
let right = right' in |
| 290 |
|
*) |
| 291 |
|
|
| 292 |
(empty_rec accu1) || (empty_rec accu2) || |
(empty_rec accu1) || (empty_rec accu2) || |
| 293 |
(* 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 |
| 294 |
for large right hand-side *) |
for large right hand-side *) |
| 295 |
( |
( |
| 296 |
((*if (List length right > 2) then |
(* (if (List.length right > 2) then |
| 297 |
let (cup1,cup2) = cup_product right in |
let (cup1,cup2) = cup_product right in |
| 298 |
(empty_rec (diff accu1 cup1)) && (empty_rec (diff accu2 cup2)) |
(empty_rec (diff accu1 cup1)) && (empty_rec (diff accu2 cup2)) |
| 299 |
else*) true) |
else true) |
| 300 |
&& |
&& *) |
| 301 |
(try aux accu1 accu2 right; true with NotEmpty -> false) |
(try aux accu1 accu2 right; true with NotEmpty -> false) |
| 302 |
) |
) |
| 303 |
|
|
| 325 |
List.for_all aux (get_record c) |
List.for_all aux (get_record c) |
| 326 |
|
|
| 327 |
let is_empty d = |
let is_empty d = |
| 328 |
|
(* Printf.eprintf "+"; flush stderr; *) |
| 329 |
let old = !memo in |
let old = !memo in |
| 330 |
let r = empty_rec d in |
let r = empty_rec d in |
| 331 |
if not r then memo := old; |
if not r then memo := old; |
| 332 |
(* cache_false := Assumptions.empty; *) |
(* cache_false := Assumptions.empty; *) |
| 333 |
|
(* Printf.eprintf "-\n"; flush stderr; *) |
| 334 |
r |
r |
| 335 |
|
|
| 336 |
let non_empty d = |
let non_empty d = |
| 621 |
|
|
| 622 |
end |
end |
| 623 |
|
|
| 624 |
|
let () = print_descr := Print.print_descr |
| 625 |
|
|
| 626 |
module Positive = |
module Positive = |
| 627 |
struct |
struct |
Parent Directory
| 
Revision Log
| 
Patch