1 files changed, 313 insertions, 145 deletions

diff --git a/abstract/abs_interp_edd.ml b/abstract/abs_interp_edd.ml
index 4f2ad81..863a22d 100644
--- a/abstract/abs_interp_edd.ml
+++ b/abstract/abs_interp_edd.ml
@@ -7,10 +7,18 @@ open Util
 open Num_domain
 open Abs_interp
 
+let time id f =
+  Format.printf "%s[@?" id;
+  let r = f () in
+  Format.printf "] @?";
+  r
+
 module I (ND : NUMERICAL_ENVIRONMENT_DOMAIN) : sig
 
     val do_prog : cmdline_opt -> rooted_prog -> unit
 
+    val test : unit -> unit
+
 end = struct
 
 
@@ -29,11 +37,10 @@ end = struct
         ev_order      : (id, int) Hashtbl.t;
     }
 
-    type edd_node =
+    type edd =
         | DBot
         | DVal of int
-        | DChoice of id * (item * edd) list
-    and edd = int * edd_node
+        | DChoice of int * id * (item * edd) list
 
     type edd_v = {
         ve            : varenv;
@@ -45,41 +52,54 @@ end = struct
     (*
       Utility functions for memoization
 
-      memo : (((int * 'a) -> (int * 'b)) -> 'a -> 'b) -> (int * 'a) -> (int * 'b)
-      memo2 : (((int * 'a) -> (int * 'b) -> (int * 'c)) -> 'a -> 'b -> 'c) -> (int * 'a) -> (int * 'b) -> (int * 'c)
+      memo : (('a -> 'b) -> 'a -> 'b) -> 'a -> 'b
+                -> (int * 'a) -> (int * 'b)
+      memo2 : (('a -> 'b -> 'c) -> 'a -> 'b -> 'c)
+                -> 'a -> 'b -> 'c
+
+      Where 'a = 'b = 'c = edd, but it can be adapted.
     *)
+    let key = function
+        | DBot -> None
+        | DVal i -> Some (Left i)
+        | DChoice(i, _, _) -> Some (Right i)
+
     let memo f =
-        let n = ref 0 in
         let memo = Hashtbl.create 12 in
-        let rec ff (id, v) =
-          try Hashtbl.find memo id
+        let rec ff v =
+          try Hashtbl.find memo (key v)
           with Not_found ->
             let r = f ff v in
-            incr n;
-            Hashtbl.add memo id (n, r);
-            n, r
+            Hashtbl.add memo (key v) r; r
         in ff
           
     let memo2 f =
-        let n = ref 0 in
         let memo = Hashtbl.create 12 in
-        let rec ff (id1, v1) (id2, v2) =
-          try Hashtbl.find memo (id1, id2)
+        let rec ff v1 v2 =
+          try Hashtbl.find memo (key v1, key v2)
           with Not_found ->
             let r = f ff v1 v2 in
-            incr n;
-            Hashtbl.add memo (id1, id2) (n, r);
-            n, r
+            Hashtbl.add memo (key v1, key v2) r; r
         in ff
 
+    let edd_node_eq = function
+        | DBot, DBot -> true
+        | DVal i, DVal j when i = j -> true
+        | DChoice(i, _, _), DChoice(j, _, _) when i = j -> true
+        | _ -> false
+
     (*
       edd_print : Format.formatter -> edd_v -> unit
     *)
     let edd_print fmt v =
+        let max_n = ref 0 in
+        let max_v = ref 0 in
+
         let c_nodes = Hashtbl.create 12 in
         let rec add = function
-            | n, (DChoice(_, l) as x) ->
+            | DChoice(n, _, l) as x ->
               if not (Hashtbl.mem c_nodes n) then begin
+                if n > !max_n then max_n := n;
                 Hashtbl.add c_nodes n x;
                 List.iter (fun (_, y) -> add y) l
               end
@@ -87,31 +107,35 @@ end = struct
         in add v.root;
 
         let print_n fmt = function
-          | (_, DBot) -> Format.fprintf fmt "⊥";
-          | (_, DVal i) -> Format.fprintf fmt "v%d" i;
-          | (n, DChoice _) -> Format.fprintf fmt "n%d" n
+          | DBot -> Format.fprintf fmt "⊥";
+          | DVal i -> if i > !max_v then max_v := i;
+                    Format.fprintf fmt "v%d" i;
+          | DChoice(n, _, _) -> Format.fprintf fmt "n%d" n
         in
         Format.fprintf fmt "Root: %a@." print_n v.root;
 
-        Hashtbl.iter
-          (fun id x -> match x with
-              | DChoice (var, l) ->
+        for id = !max_n downto 0 do
+          try match Hashtbl.find c_nodes id with
+              | DChoice (_, var, l) ->
                 let p fmt (c, l) = Format.fprintf fmt "%s → %a" c print_n l in
                 Format.fprintf fmt "n%d: %a ? @[<hov>%a@]@."
                     id Formula_printer.print_id var
                     (print_list p ", ") l
-              | _ -> assert false)
-          c_nodes;
-        Hashtbl.iter
-            (fun id v -> Format.fprintf fmt "v%d: %a@." id ND.print v)
-            v.leaves
-            
+              | _ -> assert false
+          with Not_found -> ()
+        done;
+
+        for id = 0 to !max_v do
+          try let v = Hashtbl.find v.leaves id in
+            Format.fprintf fmt "v%d: %a@." id ND.print v
+          with Not_found -> ()
+        done
 
 
     (*
       edd_bot : varenv -> edd_v
     *)
-    let edd_bot ve = { ve; root = (0, DBot); leaves = Hashtbl.create 1 }
+    let edd_bot ve = { ve; root = DBot; leaves = Hashtbl.create 1 }
 
     (*
       edd_top : evar list -> nvar list -> edd_v
@@ -119,7 +143,7 @@ end = struct
     let edd_top ve =
         let leaves = Hashtbl.create 1 in
         Hashtbl.add leaves 0 (ND.top ve.nvars);
-        { ve; root = (1, DVal 0); leaves }
+        { ve; root = DVal 0; leaves }
 
     (*
       edd_of_cons : varenv -> enum_cons -> edd_v
@@ -130,12 +154,12 @@ end = struct
         let leaves = Hashtbl.create 1 in
         Hashtbl.add leaves 0 (ND.top ve.nvars);
 
-        let bot, top = (0, DBot), (1, DVal 0) in
+        let bot, top = DBot, DVal 0 in
 
         let root = match r with
         | EItem x ->
-          2, DChoice(vid,
-              List.map (fun v -> if op v x then v, bot else v, top)
+          DChoice(0, vid,
+              List.map (fun v -> if op v x then v, top else v, bot)
                 (List.assoc vid ve.evars))      
         | EIdent vid2 ->
             let a, b =
@@ -143,14 +167,14 @@ end = struct
                   then vid, vid2
                   else vid2, vid
             in
-            let n = ref 2 in
+            let n = ref 0 in
             let nb x =
               incr n;
-              !n, DChoice(b,
+              DChoice(!n, b,
                     List.map (fun v -> if op v x then v, top else v, bot)
                       (List.assoc b ve.evars))
             in
-            2, DChoice(a, List.map (fun x -> x, nb x) (List.assoc a ve.evars))
+            DChoice(0, a, List.map (fun x -> x, nb x) (List.assoc a ve.evars))
         in
         { ve; root; leaves }
 
@@ -161,61 +185,63 @@ end = struct
         let ve = a.ve in
 
         let leaves = Hashtbl.create 12 in
+        let lc = ref 0 in
 
-        let n = ref 0 in
         let get_leaf x = 
           let id = ref None in
           Hashtbl.iter (fun i v -> if ND.eq v x then id := Some i) leaves;
           begin match !id with
           | Some i -> DVal i
           | None ->
-            incr n;
-            Hashtbl.add leaves !n x;
-            DVal (!n)
+            incr lc;
+            Hashtbl.add leaves !lc x;
+            DVal (!lc)
           end
         in
 
-
+        let nc = ref 0 in
         let f f_rec na nb =
           let dq v l =
-            let _, (i, x0) = List.hd l in
-            if List.exists (fun (_, (j, x)) -> j <> i || x <> x0) l
-              then DChoice(v, l)
-              else x0
+            let _, x0 = List.hd l in
+            if List.exists (fun (_, x) -> not (edd_node_eq (x, x0))) l
+              then begin
+                incr nc; DChoice(!nc, v, l)
+              end else x0
           in
           match na, nb with
           | DBot, DBot -> DBot
-          | DBot, DVal i -> get_leaf (Hashtbl.find b.leaves i)
-          | x, DBot -> x
+          | DBot, DVal i ->
+              get_leaf (Hashtbl.find b.leaves i)
+          | DVal i, DBot ->
+              get_leaf (Hashtbl.find a.leaves i)
+          | DVal u, DVal v ->
+            let x = ND.join (Hashtbl.find a.leaves u) (Hashtbl.find b.leaves v) in
+            get_leaf x
 
-          | DChoice(va, la), DChoice(vb, lb) when va = vb ->
+          | DChoice(_, va, la), DChoice(_, vb, lb) when va = vb ->
             let kl = List.map2
                 (fun (ta, ba) (tb, bb) -> assert (ta = tb);
-                  ta, f (ba, bb))
+                  ta, f_rec ba bb)
                 la lb
             in
             dq va kl
-          | DChoice(va, la), DChoice(vb, lb) ->
+          | DChoice(_, va, la), DChoice(_, vb, lb) ->
             let v, kl =
               if Hashtbl.find ve.ev_order va < Hashtbl.find ve.ev_order vb then
-                va, List.map (fun (k, ca) -> k, f (ca, nb)) la
+                va, List.map (fun (k, ca) -> k, f_rec ca nb) la
               else
-                vb, List.map (fun (k, cb) -> k, f (na, cb)) lb
+                vb, List.map (fun (k, cb) -> k, f_rec na cb) lb
             in
             dq v kl
 
-          | DChoice(va, la), _ ->
-            let kl = List.map (fun (k, ca) -> k, f (ca, nb)) la in
+          | DChoice(_,va, la), _ ->
+            let kl = List.map (fun (k, ca) -> k, f_rec ca nb) la in
             dq va kl
-          | _, DChoice(vb, lb) ->
-            let kl = List.map (fun (k, cb) -> k, f (na, cb)) lb in
+          | _, DChoice(_, vb, lb) ->
+            let kl = List.map (fun (k, cb) -> k, f_rec na cb) lb in
             dq vb kl
-
-          | DVal u, DVal v ->
-            let x = ND.join (Hashtbl.find a.leaves u) (Hashtbl.find b.leaves v) in
-            get_leaf x
         in
-        { leaves; ve; root = memo2 f a.root b.root }
+        { leaves; ve; root = time "join" (fun () -> memo2 f a.root b.root) }
 
     (*
       edd_meet : edd_v -> edd_v -> edd_v
@@ -223,7 +249,7 @@ end = struct
     let edd_meet a b =
         let ve = a.ve in
 
-        let n = ref 0 in
+        let lc = ref 0 in
         let leaves = Hashtbl.create 12 in
 
         let get_leaf x = 
@@ -233,59 +259,59 @@ end = struct
             match !id with
             | Some i -> DVal i
             | None ->
-              incr n;
-              Hashtbl.add leaves !n x;
-              DVal (!n)
+              incr lc;
+              Hashtbl.add leaves !lc x;
+              DVal (!lc)
           end
         in
 
-        let memo = Hashtbl.create 12 in
-        let rec f (na, nb) =
-          try Hashtbl.find memo (na, nb)
-          with Not_found -> let r =
-            let dq v l =
-              let _, x0 = List.hd l in
-              if List.exists (fun (_, x) -> x <> x0) l
-                then DChoice(v, l)
-                else x0
+        let nc = ref 0 in
+        let f f_rec na nb =
+          let dq v l =
+            let _, x0 = List.hd l in
+            if List.exists (fun (_, x) -> not (edd_node_eq (x, x0))) l
+              then begin
+                incr nc; DChoice(!nc, v, l)
+              end else x0
+          in
+          match na, nb with
+          | DBot, _ | _, DBot -> DBot
+          | DVal u, DVal v ->
+            let x = ND.meet (Hashtbl.find a.leaves u) (Hashtbl.find b.leaves v) in
+            get_leaf x
+
+          | DChoice(_, va, la), DChoice(_, vb, lb) when va = vb ->
+            let kl = List.map2
+                (fun (ta, ba) (tb, bb) -> assert (ta = tb);
+                  ta, f_rec ba bb)
+                la lb
             in
-            match na, nb with
-            | DBot, _ | _, DBot -> DBot
-            | DChoice(va, la), DChoice(vb, lb) when va = vb ->
-              let kl = List.map2
-                  (fun (ta, ba) (tb, bb) -> assert (ta = tb);
-                    ta, f (ba, bb))
-                  la lb
-              in
-              dq va kl
-            | DChoice(va, la), DChoice(vb, lb) ->
-              let v, kl =
-                if Hashtbl.find ve.ev_order va < Hashtbl.find ve.ev_order vb then
-                  va, List.map (fun (k, ca) -> k, f (ca, nb)) la
-                else
-                  vb, List.map (fun (k, cb) -> k, f (na, cb)) lb
-              in
-              dq v kl
-            | DChoice(va, la), _ ->
-              let kl = List.map (fun (k, ca) -> k, f (ca, nb)) la in
-              dq va kl
-            | _, DChoice(vb, lb) ->
-              let kl = List.map (fun (k, cb) -> k, f (na, cb)) lb in
-              dq vb kl
-            | DVal u, DVal v ->
-              let x = ND.meet (Hashtbl.find a.leaves u) (Hashtbl.find b.leaves v) in
-              get_leaf x
-          in Hashtbl.add memo (na, nb) r; r
+            dq va kl
+          | DChoice(_, va, la), DChoice(_, vb, lb) ->
+            let v, kl =
+              if Hashtbl.find ve.ev_order va < Hashtbl.find ve.ev_order vb then
+                va, List.map (fun (k, ca) -> k, f_rec ca nb) la
+              else
+                vb, List.map (fun (k, cb) -> k, f_rec na cb) lb
+            in
+            dq v kl
+          | DChoice(_, va, la), _ ->
+            let kl = List.map (fun (k, ca) -> k, f_rec ca nb) la in
+            dq va kl
+          | _, DChoice(_, vb, lb) ->
+            let kl = List.map (fun (k, cb) -> k, f_rec na cb) lb in
+            dq vb kl
         in
-        { leaves; ve; root = f (a.root, b.root) }
+        { leaves; ve; root = time "meet" (fun () -> memo2 f a.root b.root) }
 
     (*
+      edd_num_apply : edd_v -> (ND.t -> ND.t) -> edd_v
       edd_apply_ncl : edd_v -> num_cons list -> edd_v
     *)
-    let edd_apply_ncl v ncl =
+    let edd_num_apply v nfun =
         let ve = v.ve in
 
-        let n = ref 0 in
+        let lc = ref 0 in
         let leaves = Hashtbl.create 12 in
 
         let get_leaf x = 
@@ -295,36 +321,48 @@ end = struct
             match !id with
             | Some i -> DVal i
             | None ->
-              incr n;
-              Hashtbl.add leaves !n x;
-              DVal (!n)
+              incr lc;
+              Hashtbl.add leaves !lc x;
+              DVal (!lc)
           end
         in
 
-        let memo = Hashtbl.create 12 in
-        let rec f n =
-          try Hashtbl.find memo n
-          with Not_found -> let r =
-            match n with
-            | DBot -> DBot
-            | DVal i -> get_leaf (ND.apply_cl (Hashtbl.find v.leaves i) ncl)
-            | DChoice(var, l) ->
-              let l = List.map (fun (k, v) -> k, f v) l in
-              let _, x0 = List.hd l in
-              if List.exists (fun (_, x) -> x <> x0) l
-                then DChoice(var, l)
-                else x0
-          in Hashtbl.add memo n r; r
+        let f f_rec n =
+          match n with
+          | DBot -> DBot
+          | DVal i -> get_leaf (nfun (Hashtbl.find v.leaves i))
+          | DChoice(n, var, l) ->
+            let l = List.map (fun (k, v) -> k, f_rec v) l in
+            let _, x0 = List.hd l in
+            if List.exists (fun (_, x) -> not (edd_node_eq (x, x0))) l
+              then DChoice(n, var, l)
+              else x0
+        in
+        { leaves; ve; root = memo f v.root }
+
+    let edd_apply_ncl v ncl =
+        edd_num_apply v (fun n -> ND.apply_cl n ncl)
+
+    (*
+      edd_apply_ecl : edd_v -> enum_cons list -> edd_v
+    *)
+    let edd_apply_ecl v ec =
+        let rec cl_k = function
+          | [] -> edd_top v.ve
+          | [a] -> edd_of_cons v.ve a
+          | l ->
+            let n = ref 0 in
+            let la, lb = List.partition (fun _ -> incr n; !n mod 2 = 0) l in
+            edd_meet (cl_k la) (cl_k lb)
         in
-        { leaves; ve; root = f v.root }
+        let cons_edd = cl_k ec in
+        edd_meet v cons_edd
 
     (*
       edd_apply_cl : edd_v -> conslist -> edd_v
     *)
     let rec edd_apply_cl v (ec, nc, r) =
-        let v = List.fold_left
-            (fun v cons -> edd_meet v (edd_of_cons v.ve cons))
-            v ec in
+        let v = edd_apply_ecl v ec in
         match r with
         | CLTrue ->
           edd_apply_ncl v nc
@@ -340,23 +378,100 @@ end = struct
       edd_eq : edd_v -> edd_v -> bool
     *)
     let edd_eq a b =
+        let f f_rec na nb =
+          match na, nb with
+          | DBot, DBot -> true
+          | DVal i, DVal j ->
+            ND.eq (Hashtbl.find a.leaves i) (Hashtbl.find b.leaves j)
+          | DChoice(_, va, la), DChoice(_, vb, lb) when va = vb ->
+            List.for_all2 (fun (ca, na) (cb, nb) -> assert (ca = cb); f_rec na nb)
+                la lb
+          | _ -> false
+        in memo2 f a.root b.root
+
+
+    (*
+      edd_forget_vars : edd_v -> id list -> edd_v
+    *)
+    let edd_forget_vars v vars =
+        let ve = v.ve in
+
+        let leaves = Hashtbl.create 12 in
+        let lc = ref 0 in
+
+        let get_leaf x = 
+          let id = ref None in
+          Hashtbl.iter (fun i v -> if ND.eq v x then id := Some i) leaves;
+          begin match !id with
+          | Some i -> DVal i
+          | None ->
+            incr lc;
+            Hashtbl.add leaves !lc x;
+            DVal (!lc)
+          end
+        in
+
+        let nc = ref 0 in
         let memo = Hashtbl.create 12 in
-        let rec f (na, nb) =
-          try Hashtbl.find memo (na, nb)
-          with Not_found -> let r =
-            match na, nb with
-            | DBot, DBot -> true
-            | DVal i, DVal j ->
-              ND.eq (Hashtbl.find a.leaves i) (Hashtbl.find b.leaves j)
-            | DChoice(va, la), DChoice(vb, lb) when va = vb ->
-              List.for_all2 (fun (ca, na) (cb, nb) -> assert (ca = cb); f (na, nb))
-                  la lb
-            | _ -> false
-          in Hashtbl.add memo (na, nb) r; r
-        in f (a.root, b.root)
+        let rec f l =
+            let kl = List.sort Pervasives.compare (List.map key l) in
+            try Hashtbl.find memo kl
+            with Not_found -> let r =
+              let cn, fn = List.fold_left
+                (fun (cn, fn) node -> match node with
+                  | DBot -> cn, fn
+                  | DVal i -> cn, i::fn
+                  | DChoice (n, v, l) -> (n, v, l)::cn, fn)
+                ([], []) l in
+              let cn = List.sort
+                (fun (n, v1, _) (n, v2, _) -> Pervasives.compare
+                    (Hashtbl.find ve.ev_order v1) (Hashtbl.find ve.ev_order v2))
+                cn in
+              if cn = [] then
+                if fn = [] then DBot
+                else
+                  let x = list_fold_op ND.join
+                      (List.map (Hashtbl.find v.leaves) fn)
+                  in get_leaf x
+              else
+                let _, dv, cl = List.hd cn in
+                let d, nd = List.partition (fun (_, v, _) -> v = dv) cn in
+                let ch1 = List.map (fun (a, b, c) -> DChoice(a, b, c)) nd in
+                let ch2 = List.map (fun i -> DVal i) fn in
+                if List.mem dv vars then
+                  (* Do union of all branches branching from nodes on variable dv *)
+                  let ch3 = List.flatten
+                    (List.map (fun (_, _, c) -> List.map snd c) d) in
+                  f (ch1@ch2@ch3)
+                else
+                  (* Keep disjunction on variable dv *)
+                  let d, nd = List.partition (fun (_, v, _) -> v = dv) cn in
+                  let cc = List.map
+                    (fun (c, _) ->
+                      let ch3 = List.map (fun (_, _, cl) -> List.assoc c cl) d in
+                      c, f (ch1@ch2@ch3))
+                    cl in
+                  let _, x0 = List.hd cc in
+                  if List.exists (fun (_, x) -> not (edd_node_eq (x, x0))) cc
+                  then begin
+                    incr nc; DChoice(!nc, dv, cc)
+                  end else x0
+            in Hashtbl.add memo kl r; r
+        in
+        { leaves; ve; root = f [v.root] }
+
+    (*
+      edd_eassign : edd_v -> (id * id) list -> edd_v
+    *)
+    let edd_eassign v ids =
+      let v = edd_forget_vars v (List.map fst ids) in
+      edd_apply_ecl v
+        (List.map (fun (x, y) -> (E_EQ, x, EIdent y)) ids)
 
 
     (*
+        Just a function to test EDDs
+    *)
     let test () =
         let ve = {
             evars = ["x", ["tt"; "ff"]; "y", ["tt"; "ff"]; "z", ["tt"; "ff"]];
@@ -372,8 +487,11 @@ end = struct
         let w = edd_meet u v in
         Format.printf "x = y && y != z : @[%a@]@." edd_print w;
         let t = edd_join u v in
-        Format.printf "x = y || y != z : @[%a@]@." edd_print t
-    *)
+        Format.printf "x = y || y != z : @[%a@]@." edd_print t;
+        let e = edd_forget_vars w ["y"] in
+        Format.printf "x = y && y != z ; forget y : @[%a@]@." edd_print e;
+        let f = edd_forget_vars t ["y"] in
+        Format.printf "x = y || y != z ; forget y : @[%a@]@." edd_print f
 
 
     (* ******************************
@@ -399,6 +517,29 @@ end = struct
         mutable data  : edd_v;
     }
 
+
+    (*
+      pass_cycle : env -> edd_v -> edd_v
+    *)
+    let pass_cycle env v =
+        let assign_e, assign_n = List.fold_left
+          (fun (ae, an) (a, b, t) -> match t with
+            | TEnum _ -> (a, b)::ae, an
+            | TInt | TReal -> ae, (a, NIdent b)::an)
+          ([], []) env.cycle in
+
+        let v = edd_eassign v assign_e in
+        let v = edd_num_apply v (fun nv -> ND.assign nv assign_n) in
+
+        let ef, nf = List.fold_left
+            (fun (ef, nf) (var, t) -> match t with
+              | TEnum _ -> var::ef, nf
+              | TReal | TInt -> ef, var::nf)
+            ([], []) env.forget in
+
+        let v = edd_forget_vars v ef in
+        edd_num_apply v (fun nv -> List.fold_left ND.forgetvar nv nf)
+
     (*
       extract_linked_evars : conslist -> (id * id) list
 
@@ -554,7 +695,7 @@ end = struct
              (List.sort Pervasives.compare (List.map ord_couple lv1)) in
         let lv2 = uniq_sorted
              (List.sort Pervasives.compare (List.map ord_couple lv2)) in
-        let evars_ord = scope_constrict evars (lv0 @ lv1 @ lv2) in
+        let evars_ord = List.rev @@  scope_constrict evars ( lv1 ) in
 
         let ev_order = Hashtbl.create (List.length evars) in
         List.iteri (fun i x -> Hashtbl.add ev_order x i) evars_ord;
@@ -591,8 +732,35 @@ end = struct
 
     let do_prog opt rp =
         let e = init_env opt rp in
-        let d2 = edd_apply_cl e.data e.cl in
-        Format.printf " -> @[<hov>%a@]@." edd_print d2
+        let rec f x =
+          Format.printf "Apply formula...@.";
+          let d2 = edd_apply_cl x e.cl in
+          Format.printf "Pass cycle...@.";
+          let dc = pass_cycle e d2 in
+          Format.printf "Join with init...@.";
+          let dcc = edd_join dc e.data in
+          Format.printf "@[<hov>%a@]@.@." edd_print dcc;
+          if not (edd_eq x dcc) then f dcc else dcc
+        in
+        
+        let final = edd_apply_cl (f e.data) e.cl in
+        (*Format.printf "@.Final:@.@[<hov>%a@]@." edd_print final;*)
+
+        let check_guarantee (id, f) =
+          let cl = Formula.conslist_of_f f in
+          Format.printf "@[<hv 4>%s:@ %a ⇒ ⊥  @ "
+            id Formula_printer.print_conslist cl;
+          let z = edd_apply_cl final cl in
+          if z.root = DBot then
+            Format.printf "OK@]@ "
+          else
+            Format.printf "FAIL@]@ "
+        in
+        if e.guarantees <> [] then begin
+          Format.printf "Guarantee @[<v 0>";
+          List.iter check_guarantee e.guarantees;
+          Format.printf "@]@."
+        end;
 
 end