Better handling of toplevel variables

types/types.ml

@@ -139,14 +139,26 @@ module BoolChars : BoolVar.S with
 
 module TLV = struct
 
-  open Var
+  module Set = Set.Make(
+    struct
+      type t = (Var.var * bool)
+      let compare (v1,p1) (v2,p2) =
+        let c = Var.compare v1 v2 in
+        if c == 0 then
+          if p1 == p2 then 0
+          else if p1 then 1 else -1
+        else c
+    end)
+
   (* s : top level variables
    * f : all free variables in the subtree
    * b : true if the type contains only variables *)
-  type t =  { s : Set.t ; f : Set.t ; b : bool }
+  type t =  { s : Set.t ; f : Var.Set.t ; b : bool }
 
-  let empty = { s = Set.empty ; f = Set.empty ; b = true }
-  let singleton v = { s = Set.singleton v; f = Set.singleton v; b = true }
+  let empty = { s = Set.empty ; f = Var.Set.empty ; b = true }
+  let any = { s = Set.empty ; f = Var.Set.empty ; b = false }
+
+  let singleton (v,p) = { s = Set.singleton (v,p); f = Var.Set.singleton v; b = true }
 
   (* return the max of top level variables *)
   let max x = Set.max_elt x.s
@@ -154,30 +166,30 @@ module TLV = struct
   let pair x y = {
     b = false ; 
     s = Set.empty ; 
-    f = Set.union x.f y.f 
+    f = Var.Set.union x.f y.f 
   }
 
   let union x y = {
     b = x.b && y.b;
     s = Set.union x.s y.s ;
-    f = Set.union x.f y.f ;
+    f = Var.Set.union x.f y.f ;
   }
 
   let inter x y = {
     b = x.b && y.b;
     s = Set.inter x.s y.s ;
-    f = Set.inter x.f y.f ;
+    f = Var.Set.inter x.f y.f ;
   }
 
   let diff x y = {
     b = x.b && y.b;
-    s = Set.diff x.s y.s; 
-    f = Set.diff x.f y.f;
+    s = Set.inter x.s (Set.fold (fun (v,p) acc -> Set.add (v,not p) acc) y.s Set.empty); 
+    f = Var.Set.union x.f y.f;
   }
 
   (* true if it contains only one variable *)
-  let is_single x = x.b && (Set.cardinal x.f = 1) && (Set.cardinal x.s = 1)
-  let no_variables x = (x.b == false) && (Set.cardinal x.f = 0)
+  let is_single x = x.b && (Var.Set.cardinal x.f = 1) && (Set.cardinal x.s = 1)
+  let no_variables x = (x.b == false) && (Var.Set.cardinal x.f = 0)
 
 end
 
@@ -388,7 +400,7 @@ let any =  {
   chars = BoolChars.full;
   abstract = Abstract.any;
   absent= false;
-  toplvars = TLV.empty
+  toplvars = TLV.any
 }
 
 let non_constructed =
@@ -411,8 +423,9 @@ let record_fields x =
   { empty with record = BoolRec.atom (`Atm (Rec.atom x)) }
 
 let atom a = { empty with atoms = BoolAtoms.atom (`Atm a) }
+
+(* Atm = Any ^ a *)
 let var a =  {
-  (* Atm = Any ^ a *)
   times = BoolPair.vars a;
   xml   = BoolPair.vars a;
   arrow = BoolPair.vars a;
@@ -422,7 +435,7 @@ let var a =  {
   chars = BoolChars.vars a;
   abstract = Abstract.empty;
   absent= false;
-  toplvars = TLV.singleton a
+  toplvars = TLV.singleton (a,true)
 }
 
 let is_var t = TLV.is_single t.toplvars
@@ -2609,10 +2622,14 @@ module Tallying = struct
 
   (* norm generates a constraint set for the costraint t <= 0 *)
   let rec norm (t,mem) =
-    (* if is_var t then XXX else *) 
+    if DescrSet.mem t mem then CS.sat else begin (* if we already evaluated it, it is sat *)
+    if is_var t then
+      let (v,p) = TLV.max t.toplvars in 
+      let s = if p then (Pos (v,empty)) else (Neg (any,v)) in
+      CS.singleton s
+    else
     (* XXX if there is only one variable then is it A <= 0 or 1 <= A *)
     if is_empty t then CS.sat else (* if it empty then it is sat *)
-    if DescrSet.mem t mem then CS.sat else begin (* if we already evaluated it, it is sat *)
       let mem = DescrSet.add t mem in
       let aux single norm_aux acc l = big_prod (toplevel single norm_aux mem) acc l in
 
@@ -2693,7 +2710,6 @@ module Tallying = struct
 
      P(Q v {a}) = {a} v P(Q) v {X v {a} | X \in P(Q) }
    *)
-  (*
   and normarrow (t,mem) =
     let rec norm_arrow pos neg =
       match neg with
@@ -2717,8 +2733,7 @@ module Tallying = struct
           CS.prod con11 con22
     in
     big_prod norm_arrow CS.sat (Pair.get t)
-*)
-
+(*
   and normarrow (t,mem) =
     let rec norm_arrow pos neg =
       match neg with
@@ -2743,6 +2758,7 @@ module Tallying = struct
             CS.prod con11 con22
     in
     big_prod norm_arrow CS.sat (Pair.get t)
+*)
 
   let memo_norm = DescrHash.create 17
   let norm t =
@@ -2803,7 +2819,7 @@ module Tallying = struct
               (* if t containts only a toplevel variable and nothing else
                * means that the constraint is of the form (alpha,beta). *)
               if is_var t then begin
-                let beta = TLV.max t.toplvars in
+                let (beta,_) = TLV.max t.toplvars in
                 let acc1 = aux beta (empty,any) acc in
                 (* alpha <= beta --> { empty <= alpha <= beta ; empty <= beta <= any } *)
                 if b then aux alpha (empty,t) acc1