Commit 0ac20cd1 authored by Pietro Abate's avatar Pietro Abate
Browse files

[r2003-03-18 07:22:11 by cvscast] Empty log message

Original author: cvscast
Date: 2003-03-18 07:22:11+00:00
parent 9cf4a7db
......@@ -62,8 +62,13 @@ let full = [ [],[] ]
let atom x = [ [x],[] ]
let may_remove (p1,n1) (p2,n2) =
(* false *)
(SList.subset p2 p1) && (SList.subset n2 n1)
(* in some cases, it is faster to avoid may_remove...
investigate this... *)
let cup t s =
if t == s then t
else match (t,s) with
......
......@@ -441,6 +441,11 @@ let cap_product l =
(fun (d1,d2) (t1,t2) -> (cap_t d1 t1, cap_t d2 t2))
(any,any)
l
let cup_product l =
List.fold_left
(fun (d1,d2) (t1,t2) -> (cup_t d1 t1, cup_t d2 t2))
(empty,empty)
l
let rec exists max f =
(max > 0) && (f (max - 1) || exists (max - 1) f)
......@@ -489,7 +494,6 @@ let rec big_conj f l n =
if s.active then n.active <- true
with NotEmpty -> if n.status = NEmpty then raise NotEmpty
let rec guard a f n =
match slot a with
| { status = Empty } -> ()
......@@ -503,6 +507,7 @@ and slot d =
(not d.absent)) then slot_not_empty
else try DescrHash.find memo d
with Not_found ->
(* Format.fprintf Format.std_formatter "Empty:%a@\n" !print_descr d; *)
let s = { status = Maybe; active = false; notify = Nothing } in
DescrHash.add memo d s;
(try
......@@ -517,7 +522,7 @@ and slot d =
and check_times (left,right) s =
(* Printf.eprintf "[%i]" (List.length right);
flush stderr; *)
flush stderr; *)
let rec aux accu1 accu2 right s = match right with
| (t1,t2)::right ->
if trivially_empty (cap_t accu1 t1) ||
......@@ -529,6 +534,15 @@ and check_times (left,right) s =
)
| [] -> set s
in
(*
if List.length right > 6 then (
Printf.eprintf "HEURISTIC\n"; flush stderr;
let (n1,n2) = cup_product right in
let n1 = diff accu1 n1 and n2 = diff accu2 n2 in
guard n1 set s;
guard n2 set s;
Printf.eprintf "HEURISTIC failed\n"; flush stderr;
); *)
let (accu1,accu2) = cap_product left in
guard accu1 (guard accu2 (aux accu1 accu2 right)) s
......@@ -979,6 +993,7 @@ struct
let end_print ppf =
Format.fprintf ppf "@]";
(match List.rev !wh with
| [] -> ()
| (na,d)::t ->
......@@ -989,7 +1004,7 @@ struct
t;
Format.fprintf ppf "@]"
);
Format.fprintf ppf "@]";
(* Format.fprintf ppf "@]"; *)
count_name := 0;
wh := [];
DescrHash.clear marks
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment