Fix Tallying.merge function.

types/types.ml

@@ -2224,7 +2224,8 @@ module Tallying = struct
       let compare = Pervasives.compare
     end)
 
-    type cset = S.t
+    type cs = S.t
+    type c = S.elt
 
     let singleton (b,v,s) = 
       S.singleton (M.singleton (b,v) s)
@@ -2234,6 +2235,7 @@ module Tallying = struct
         |(k,None,None) -> None
         |(k,Some v,None) -> Some v
         |(k,None,Some v) -> Some v
+        |((_,v),Some x,Some y) when Descr.equal x y -> Some x
         |((true,v),Some x,Some y) -> Some (cap x y)
         |((false,v),Some x,Some y) -> Some (cup x y)
       in
@@ -2269,12 +2271,9 @@ module Tallying = struct
       |false,true -> x
       |true,false -> y
       |false,false ->
-        let s = 
         S.fold (fun m1 acc ->
           S.fold (fun m2 acc1 -> S.add (merge m1 m2) acc1) y acc
         ) x S.empty
-        in
-        s
 
   end
 
@@ -2337,7 +2336,7 @@ module Tallying = struct
 
   let rec norm ( (t,m) : (s * DescrSet.t)) =
     if DescrSet.mem t m then CS.sat else begin
-      try
+      (* try *)
         let aux_base single norm_aux acc l = 
           List.fold_left (fun acc (pos,neg) -> 
             CS.cap acc (toplevel single norm_aux m (pos,neg))
@@ -2352,7 +2351,7 @@ module Tallying = struct
         let accu = aux_base single_record normrec accu (BoolRec.get t.record) in
         let accu = aux_base single_arrow normarrow accu (BoolPair.get t.arrow) in
         accu
-      with UnSatConstr -> CS.unsat
+      (* with UnSatConstr -> CS.unsat *)
     end
 
   (* (t1,t2) = intersection of all (fst pos,snd pos) \in P
@@ -2445,22 +2444,29 @@ module Tallying = struct
   let norm t = norm (t,DescrSet.empty)
 
   let rec merge (cs,mem) =
-    CS.M.fold (fun (b,v) s acc -> match (b,v) with
-      |(true,v) ->
-          begin try
-            let t = CS.M.find (false,v) cs in
-            let x = diff s t in
-            if DescrSet.mem x mem then acc
-            else
-              let c1 = CS.cap (CS.S.singleton cs) (norm x) in
-              let c2 = CS.S.fold (fun m acc -> CS.cup acc (merge (m,DescrSet.add x mem))) c1 CS.sat in
-              CS.cap acc c2
-          with Not_found -> acc end
-      |(false,v) -> acc
-    ) cs CS.sat
-
-  let merge c = 
-    CS.S.fold (fun cs acc -> CS.cup acc (merge (cs,DescrSet.empty))) c CS.sat
+    let aux (b,v) s =
+      try
+        let t = CS.M.find (not b,v) cs in
+        let x = if b then diff t s else diff s t in
+        if DescrSet.mem x mem then None
+        else
+          let c1 = CS.cap (CS.S.singleton cs) (norm x) in
+          let c2 = CS.S.fold (fun m acc -> CS.cup acc (merge (m,DescrSet.add x mem))) c1 CS.S.empty in
+          Some c2
+      with Not_found -> None
+    in
+      let s = 
+        CS.M.fold (fun (b,v) s acc ->
+          match aux (b,v) s with
+          |None -> acc
+          |Some c -> CS.cup c acc
+        ) cs CS.S.empty
+      in if CS.S.is_empty s then CS.S.singleton cs else s
+
+  let merge c = try merge (c,DescrSet.empty) with UnSatConstr -> CS.unsat
+  (*
+    CS.S.fold (fun c acc -> CS.cup acc (merge (c,DescrSet.empty))) cs CS.S.empty
+    *)
 
 (*
   let solve cs =
@@ -2494,4 +2500,13 @@ module Tallying = struct
         aux (t,a,x)::acc (subst e1 t a x)
 *)
 
+  let tallying l =
+    let n = List.fold_left (fun acc (s,t) -> CS.cap acc (norm(diff s t))) CS.S.empty l in
+    let m = CS.S.fold (fun c acc -> CS.cup acc (merge (c))) n CS.S.empty in
+      m
+      (*
+    let s =  CS.S.fold (fun c acc -> CS.cup acc (solve (c))) m CS.S.empty in
+    CS.S.fold (fun c acc -> CS.cup acc (unify(c))) s CS.S.empty
+    *)
+
 end

types/types.mli

@@ -354,18 +354,20 @@ module Tallying : sig
     type key = (bool * Custom.var)
     module M : Map.S with type key = key
     module S : Set.S with type elt = t M.t
-    type cset = S.t
+    type cs = S.t
+    type c = S.elt
     val print : Format.formatter -> S.t -> unit
     val merge : S.elt -> S.elt -> S.elt
-    val singleton : constr -> cset
-    val sat : cset
-    val unsat : cset
-    val cup : cset -> cset -> cset
-    val cap : cset -> cset -> cset
+    val singleton : constr -> cs
+    val sat : cs
+    val unsat : cs
+    val cup : cs -> cs -> cs
+    val cap : cs -> cs -> cs
   end
 
-  val norm : t -> CS.cset
-  val merge : CS.cset -> CS.cset
+  val norm : t -> CS.cs
+  val merge : CS.c -> CS.cs
+  val tallying : (t * t) list -> CS.cs
 
 end