Fix a few things, this doesn't work well.

3 files changed, 81 insertions, 57 deletions

diff --git a/abstract/abs_interp_dynpart.ml b/abstract/abs_interp_dynpart.ml
index c47fdc7..1adc430 100644
--- a/abstract/abs_interp_dynpart.ml
+++ b/abstract/abs_interp_dynpart.ml
@@ -62,7 +62,7 @@ end = struct
     *)
     let top e = (ED.top e.ve.evars, ND.top e.ve.nvars)
     let bottom e = (ED.top e.ve.evars, ND.bottom e.ve.nvars)
-    let is_bot (e, n) = ND.is_bot n
+    let is_bot (e, n) = ED.is_bot e || ND.is_bot n
 
     let print_v fmt (enum, num) =
       if is_bot (enum, num) then
@@ -75,32 +75,34 @@ end = struct
       widen : abs_v -> abs_v -> abs_v
       meet : abs_v -> abs_v -> abs_v
     *)
-    let join (e1, n1) (e2, n2) =
-      if is_bot (e1, n1) then (e2, n2)
-      else if is_bot (e2, n2) then (e1, n1)
-      else (ED.join e1 e2, ND.join n1 n2)
+    let join a b =
+      if is_bot a then b
+      else if is_bot b then a
+      else (ED.join (fst a) (fst b), ND.join (snd a) (snd b))
 
-    let widen (e1, n1) (e2, n2) =
-      if is_bot (e1, n1) then (e2, n2)
-      else if is_bot (e2, n2) then (e1, n1)
-      else (ED.join e1 e2, ND.widen n1 n2)
+    let widen a b =
+      if is_bot a then b
+      else if is_bot b then a
+      else (ED.join (fst a) (fst b), ND.widen (snd a) (snd b))
 
     let meet (e1, n1) (e2, n2) =
       if is_bot (e1, n1) then ED.vtop e1, ND.vbottom n1
       else if is_bot (e2, n2) then ED.vtop e2, ND.vbottom n2
       else
         try (ED.meet e1 e2 , ND.meet n1 n2)
-        with Bot -> e1, ND.vbottom n1
+        with Bot -> ED.vtop e1, ND.vbottom n1
 
     (*
       eq_v : abs_v -> abs_v -> bool
       subset_v : abs_v -> abs_v -> bool
     *)
-    let eq_v (a, b) (c, d) = (ND.is_bot b && ND.is_bot d) || (ED.eq a c && ND.eq b d)
+    let eq_v (a, b) (c, d) =
+        (is_bot (a, b) && is_bot (c, d)) 
+          || (ED.eq a c && ND.eq b d)
 
     let subset_v (a, b) (c, d) =
-      ND.is_bot b ||
-        (not (ND.is_bot d) && ED.subset a c && ND.subset b d)
+      (is_bot (a, b)) ||
+        (not (is_bot (c, d)) && ED.subset a c && ND.subset b d)
 
     (*
       apply_cl : abs_v -> conslist -> abs_v
@@ -109,12 +111,9 @@ end = struct
         try
           begin match r with
           | CLTrue ->
-            let enum =
-              fix ED.eq (fun v -> ED.apply_cl v ec) enum
-            in
-            (enum, ND.apply_cl num nc)
+            (ED.apply_cl enum ec, ND.apply_cl num nc)
           | CLFalse ->
-            (enum, ND.vbottom num)
+            (ED.vtop enum, ND.vbottom num)
           | CLAnd(a, b) ->
             let enum, num = apply_cl (enum, num) (ec, nc, a) in
             let enum, num = apply_cl (enum, num) ([], nc, b) in
@@ -289,6 +288,23 @@ end = struct
         meet v tgt
 
     (*
+      print_locs : env -> unit
+    *)
+
+    let print_locs e =
+        Hashtbl.iter
+          (fun id loc ->
+            Format.printf "@.";
+            Format.printf "q%d: @[<v 2>[ %a ]@]@." id
+              (print_list Formula_printer.print_expr " ∧ ") loc.def;
+            (*Format.printf "  F: (%a)@." Formula_printer.print_expr loc.f;*)
+            Format.printf "    %a@." print_v loc.v;
+            Format.printf " -> @[<hov>[%a]@]@."
+              (print_list (fun fmt i -> Format.fprintf fmt "q%d" i) ", ") loc.out_t;
+            )
+          e.loc
+
+    (*
       chaotic_iter : env -> unit
 
       Fills the values of loc[*].v, and updates out_t and in_t
@@ -309,6 +325,8 @@ end = struct
               loc.v <- bottom e)
           e.loc;
 
+        print_locs e;
+
         (* Iterate *)
         let it_counter = ref 0 in
         while !delta <> [] do
@@ -323,7 +341,10 @@ end = struct
             (*Format.printf "I: %a@." print_v i;*)
             let i' = set_target_case e i loc.def_cl in
             (*Format.printf "I': %a@." print_v i';*)
-            let j = join start (apply_cl (apply_cl (pass_cycle e.ve i') loc.def_cl) loc.cl) in
+            let j = join start
+              (apply_cl
+                (apply_cl (pass_cycle e.ve i') loc.def_cl)
+                loc.cl) in
             (*Format.printf "J: %a@." print_v j;*)
             j
           in
@@ -342,28 +363,30 @@ end = struct
           in
           let y = iter 0 start in
           let z = fix eq_v f y in
-          (*Format.printf "Fixpoint: %a@." print_v z;*)
+          let u = pass_cycle e.ve z in
+
+          if e.opt.verbose_ci then
+            Format.printf "Fixpoint: %a@. mem fp: %a@." print_v z print_v u;
 
           loc.v <- z;
 
           Hashtbl.iter
             (fun t loc2 ->
-                let u = pass_cycle e.ve z in
                 let v = apply_cl u loc2.def_cl in
                 let w = apply_cl v loc2.cl in
                 (*Format.printf "u: %a@.v: %a@. w: %a@." print_v u print_v v print_v w;*)
-                let r_enum, r_num = w in
-                if not (is_bot (r_enum, r_num)) then begin
-                  (*Format.printf "%d -> %d with:@.  %a@." s t print_v (r_enum, r_num);*)
+                if not (is_bot w) then begin
+                  if e.opt.verbose_ci then
+                    Format.printf "%d -> %d with:@.  %a@." s t print_v w;
                   if not (List.mem s loc2.in_t)
                     then loc2.in_t <- s::loc2.in_t;
                   if not (List.mem t loc.out_t)
                     then loc.out_t <- t::loc.out_t;
-                  if not (subset_v (r_enum, r_num) loc2.v) then begin
+                  if not (subset_v w loc2.v) then begin
                     if loc2.in_c < e.opt.widen_delay then
-                      loc2.v <- join (r_enum, r_num) loc2.v
+                      loc2.v <- join w loc2.v
                     else
-                      loc2.v <- widen (r_enum, r_num) loc2.v;
+                      loc2.v <- widen w loc2.v;
                     loc2.in_c <- loc2.in_c + 1;
                     if not (List.mem t !delta)
                       then delta := t::!delta
@@ -383,21 +406,11 @@ end = struct
               useless := i::!useless
             end)
           e.loc;
-        List.iter (Hashtbl.remove e.loc) !useless
+        List.iter (Hashtbl.remove e.loc) !useless;
+
+        print_locs e
 
 
-    let print_locs e =
-        Hashtbl.iter
-          (fun id loc ->
-            Format.printf "@.";
-            Format.printf "q%d: @[<v 2>[ %a ]@]@." id
-              (print_list Formula_printer.print_expr " ∧ ") loc.def;
-            (*Format.printf "  F: (%a)@." Formula_printer.print_expr loc.f;*)
-            Format.printf "    %a@." print_v loc.v;
-            Format.printf " -> @[<hov>[%a]@]@."
-              (print_list (fun fmt i -> Format.fprintf fmt "q%d" i) ", ") loc.out_t;
-            )
-          e.loc
 
     let do_prog opt rp =
         let e = init_env opt rp in
@@ -406,7 +419,6 @@ end = struct
           Format.printf "@.--------------@.Refinement #%d@." n;
 
           chaotic_iter e;
-          print_locs e;
 
           let qc = ref None in
 
@@ -426,8 +438,10 @@ end = struct
                     then BNot cond
                     else cond
                   in
-                  loc.def <- tr::loc.def;
-                  loc.def_cl <- conslist_of_f (f_and_list loc.def);
+                  if not (List.mem tr loc.def) then begin
+                    loc.def <- tr::loc.def;
+                    loc.def_cl <- conslist_of_f (f_and_list loc.def);
+                  end;
                   loc.f <- simplify_k [tr] loc.f;
                   loc.f <- simplify_k (get_root_true loc.f) loc.f;
                   loc.cl <- conslist_of_f loc.f;
@@ -445,17 +459,19 @@ end = struct
                 (fun c ->
                   let split_e_case_fold_aux cases c =
                         match c with
-                        | BEnumCons(_, x, EItem _) ->
+                        | BEnumCons(op, x, EItem _) ->
+                          let op = match op with | E_EQ -> (=) | E_NE -> (<>) in
                           (List.map (fun v -> BEnumCons(E_EQ, x, EItem v))
-                            (List.assoc x e.ve.evars))@cases
+                            (List.filter (op x) (List.assoc x e.ve.evars)))
+                          @cases
                         | _ -> c::cases
                   in
                   let cases_t =
                     List.fold_left split_e_case_fold_aux []
-                      (split_cases [c]) in
+                     [c] in
                   let cases_f =
                     List.fold_left split_e_case_fold_aux []
-                      (split_cases [BNot c]) in
+                     [eliminate_not_negate c] in
                   let cases = cases_t @ cases_f in
                   if
                     List.length 
diff --git a/abstract/enum_domain.ml b/abstract/enum_domain.ml
index 4f6aacd..77d7e3f 100644
--- a/abstract/enum_domain.ml
+++ b/abstract/enum_domain.ml
@@ -119,11 +119,14 @@ module Valuation : ENUM_ENVIRONMENT_DOMAIN = struct
             if cc op s t then [x] else []
 
     let apply_cl x l =
-      List.fold_left
-        (fun k c -> match apply_cons k c with
-          | [] -> raise Bot
-          | p::q -> List.fold_left join p q )
-        x l
+      let f x =
+        List.fold_left
+          (fun k c -> match apply_cons k c with
+            | [] -> raise Bot
+            | p::q -> List.fold_left join p q )
+          x l
+      in
+        fix eq f x
    
     let assign x idl =
         let v = List.fold_left
@@ -242,11 +245,14 @@ module MultiValuation : ENUM_ENVIRONMENT_DOMAIN = struct
             [] v1
 
     let apply_cl x l =
-      List.fold_left
-        (fun k c -> match apply_cons k c with
-          | [] -> raise Bot
-          | p::q -> List.fold_left join p q )
-        x l
+      let f x =
+        List.fold_left
+          (fun k c -> match apply_cons k c with
+            | [] -> raise Bot
+            | p::q -> List.fold_left join p q )
+          x l
+      in
+        fix eq f x
     
     let assign x idl =
         let v = List.fold_left
diff --git a/abstract/formula.ml b/abstract/formula.ml
index 5cbe0c9..a124a84 100644
--- a/abstract/formula.ml
+++ b/abstract/formula.ml
@@ -277,6 +277,8 @@ let rec split_cases c =
       match c with
       | BOr(a, b) ->
         true, a::(BAnd(BNot a, b))::l
+      | BTernary(c, a, b) ->
+        true, (BAnd(c, a))::(BAnd(BNot c, b))::l
       | x -> u, x::l)
     (false, []) c
   in