[r2005-05-10 16:28:49 by afrisch] Empty log message

Original author: afrisch
Date: 2005-05-10 16:28:49+00:00

Makefile.distrib

@@ -142,7 +142,7 @@ OBJECTS = \
  driver/config.cmo \
  misc/stats.cmo \
  misc/serialize.cmo misc/custom.cmo \
- misc/state.cmo misc/pool.cmo misc/encodings.cmo misc/myweak.cmo \
+ misc/state.cmo misc/pool.cmo misc/encodings.cmo \
   misc/pretty.cmo misc/ns.cmo misc/inttbl.cmo misc/imap.cmo \
  misc/html.cmo \
  \

misc/bool.ml

@@ -597,7 +597,6 @@ struct
     | Zero -> False | One -> True | Branch (x,p,n,_,_) -> Br (x,p,n)
 end
 
-(*
 module Simplify(X : Custom.T) = struct
   type elem = X.t
 
@@ -638,7 +637,7 @@ module Simplify(X : Custom.T) = struct
     let add k t =
       let rec ins = function
 	| Empty -> Leaf k
-	| Leaf j as t -> if j== k then t else join (id k, Leaf k, id j, t)
+	| Leaf j as t -> if j == k then t else join (id k, Leaf k, id j, t)
 	| Branch (p,m,t0,t1) as t ->
             if match_prefix (id k) p m then
               if zero_bit (id k) m then Branch (p, m, ins t0, t1)
@@ -784,10 +783,6 @@ module Simplify(X : Custom.T) = struct
       | Leaf _ -> 1
       | Branch (_,_,t0,t1) -> cardinal t0 + cardinal t1
 
-    let rec allvars = function
-      | Empty -> V.empty
-      | Leaf f -> f.allvars
-      | Branch (_,_,t0,t1) -> V.cup (allvars t0) (allvars t1)
   end
 
 
@@ -862,7 +857,7 @@ module Simplify(X : Custom.T) = struct
 
   let mk_f = let id = ref 0 and tbl = W.create 16387 in
   fun pos neg subs ->
-    assert (V.length pos + V.length neg + F.cardinal >= 2);
+    assert (V.length pos + V.length neg + F.cardinal subs >= 2);
     let f = W.merge tbl { pos = pos; neg = neg; subs = subs; id = 0 } in
     if f.id = 0 then f.id <- (incr id; !id);
     f
@@ -888,6 +883,25 @@ module Simplify(X : Custom.T) = struct
     | [],[],Leaf f -> NegF f
     | _ -> PosF (mk_f pos neg subs)
 
+  let trivially_disjoint f g =
+    F.mem f g.subs || F.mem g f.subs ||
+      not (V.disjoint f.pos g.neg) || not (V.disjoint f.neg g.pos)
+
+  let cap_f f g =
+    if trivially_disjoint f g then Zero
+    else
+      PosF 
+	(mk_f (V.cup f.pos g.pos) (V.cup f.neg g.neg) (F.union f.subs g.subs))
+
+  let diff_f f g =
+    if trivially_disjoint f g then PosF f
+    else
+      PosF (mk_f f.pos f.neg (F.union (Leaf g) f.subs))
+
+  let nor_f f g =
+    (* TODO: factorize *)
+    PosF (mk_f [] [] (F.union (Leaf f) (Leaf g)))
+
   let cap t1 t2 = match t1,t2 with 
     | Zero, t | t, Zero -> Zero
     | One, t | t, One -> t
@@ -905,11 +919,45 @@ module Simplify(X : Custom.T) = struct
     | PosF f, NegF g
     | NegF g, PosF f -> diff_f f g
     | NegF f, NegF g -> nor_f f g
-    | (PosF f as t), PosV x
-    | PosV x, (PosF f as t) -> 
-	if V.mem x f.pos then t
-	else if V.mem x f.neg then Zero
-	else PosF (mk_f 
+    | (PosF f as t), PosV x | PosV x, (PosF f as t) -> 
+	if V.mem f.pos x then t
+	else if V.mem f.neg x then Zero
+	else PosF (mk_f (V.add x f.pos) f.neg f.subs)
+    | (PosF f as t), NegV x | NegV x, (PosF f as t) -> 
+	if V.mem f.neg x then t
+	else if V.mem f.pos x then Zero
+	else PosF (mk_f f.pos (V.add x f.neg) f.subs)
+    | (PosV x as t), NegF f | NegF f, (PosV x as t) ->
+	if V.mem f.pos x then 
+	  match mk (V.remove x f.pos) f.neg f.subs with
+	    | PosF g -> PosF (mk_f [x] [] (Leaf g))
+	    | NegF g -> PosF (mk_f (V.add x f.pos) f.neg f.subs)
+	    | PosV y -> if X.equal x y then Zero else PosF (mk_f [x] [y] Empty)
+	    | NegV y -> 	
+		let c = X.compare x y in
+		if c = 0 then t
+		else PosF (mk_f (if c <0 then [x;y] else [y;x]) [] Empty)
+	    | Zero | One -> assert false
+	else if V.mem f.neg x then t
+	else PosF (mk_f [x] [] (Leaf f))
+    | (NegV x as t), NegF f | NegF f, (NegV x as t) ->
+	if V.mem f.neg x then 
+	  match mk f.pos (V.remove x f.neg) f.subs with
+	    | PosF g -> PosF (mk_f [] [x] (Leaf g))
+	    | NegF g -> PosF (mk_f f.pos (V.add x f.neg) f.subs)
+	    | NegV y -> if X.equal x y then Zero else PosF (mk_f [y] [x] Empty)
+	    | PosV y -> 	
+		let c = X.compare x y in
+		if c = 0 then t
+		else PosF (mk_f [] (if c <0 then [x;y] else [y;x]) Empty)
+	    | Zero | One -> assert false
+	else if V.mem f.pos x then t
+	else PosF (mk_f [] [x] (Leaf f))
+
+
+(*
+
+
 
 		     PosF { tmpl with pos = [x]; neg = [y]; 
 		   allvars = if c <0 then [x;y] else [y;x] }
@@ -1300,6 +1348,7 @@ module Simplify(X : Custom.T) = struct
 
   type t = f
 *)
-end
 *)
+end
+