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

6 files changed, 107 insertions, 61 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
diff --git a/main.ml b/main.ml
index 96fb95e..303723d 100644
--- a/main.ml
+++ b/main.ml
@@ -23,6 +23,10 @@ module AI_S_Itv_DP = Abs_interp_dynpart.I
       (Enum_domain.MultiValuation)(ItvND)
 module AI_S_Rel_DP = Abs_interp_dynpart.I
       (Enum_domain.MultiValuation)(Apron_domain.ND)
+module AI_EDD_Itv_DP = Abs_interp_dynpart.I
+      (Enum_domain_edd.EDD)(ItvND)
+module AI_EDD_Rel_DP = Abs_interp_dynpart.I
+      (Enum_domain_edd.EDD)(Apron_domain.ND)
 
 (* command line options *)
 let times = ref false
@@ -36,6 +40,8 @@ let ai_itv_edd = ref false
 let ai_rel_edd = ref false
 let ai_s_itv_dp = ref false
 let ai_s_rel_dp = ref false
+let ai_edd_itv_dp = ref false
+let ai_edd_rel_dp = ref false
 let ai_root = ref "test"
 let ai_widen_delay = ref 5
 let ai_no_time_scopes = ref "all"
@@ -50,28 +56,41 @@ let usage = "usage: analyzer [options] file.scade"
 let options = [
     "--exec-times", Arg.Set times,
         "Show time spent in each function of the analyzer, for some functions";
+
     "--dump", Arg.Set dump, "Dump program source.";
     "--dump-rn", Arg.Set dumprn, "Dump program source, after renaming.";
+
     "--vtest", Arg.Set vtest, "Verbose testing (direct interpret).";
     "--test", Arg.Set test, "Simple testing (direct interpret).";
+
     "--ai-itv", Arg.Set ai_itv, "Do abstract analysis using intervals.";
     "--ai-rel", Arg.Set ai_rel, "Do abstract analysis using Apron.";
+
     "--ai-itv-edd", Arg.Set ai_itv_edd,
         "Do abstract analysis using intervals and EDD disjunction domain.";
     "--ai-rel-edd", Arg.Set ai_rel_edd,
         "Do abstract analysis using Apron and EDD disjunction domain.";
+
     "--ai-s-itv-dp", Arg.Set ai_s_itv_dp,
         "Do abstract analysis using dynamic partitionning method, "^
         "with intervals and valuation domain for enums.";
     "--ai-s-rel-dp", Arg.Set ai_s_rel_dp,
         "Do abstract analysis using dynamic partitionning method, "^
         "with Apron and valuation domain for enums.";
+    "--ai-edd-itv-dp", Arg.Set ai_edd_itv_dp,
+        "Do abstract analysis using dynamic partitionning method, "^
+        "with intervals and EDD domain for enums.";
+    "--ai-edd-rel-dp", Arg.Set ai_edd_rel_dp,
+        "Do abstract analysis using dynamic partitionning method, "^
+        "with Apron and EDD domain for enums.";
+        
     "--ai-vci", Arg.Set ai_vci,
         "Verbose chaotic iterations (show state at each iteration)";
     "--ai-vvci", Arg.Set ai_vvci,
         "Very verbose chaotic iterations (show everything all the time)";
-    "--wd", Arg.Set_int ai_widen_delay,
+    "--ai-wd", Arg.Set_int ai_widen_delay,
         "Widening delay in abstract analysis of loops (default: 3).";
+
     "--root", Arg.Set_string ai_root,
         "Root node for abstract analysis (default: test).";
     "--no-time", Arg.Set_string ai_no_time_scopes,
@@ -132,7 +151,8 @@ let () =
 
       if !ai_itv || !ai_rel
           || !ai_itv_edd || !ai_rel_edd
-          || !ai_s_itv_dp || !ai_s_rel_dp then
+          || !ai_s_itv_dp || !ai_s_rel_dp
+          || !ai_edd_itv_dp || !ai_edd_rel_dp then
       begin
           let comma_split = Str.split (Str.regexp ",") in
           let select_f x =
@@ -168,6 +188,8 @@ let () =
 
           if !ai_s_itv_dp then AI_S_Itv_DP.do_prog opt rp;
           if !ai_s_rel_dp then AI_S_Rel_DP.do_prog opt rp;
+          if !ai_edd_itv_dp then AI_EDD_Itv_DP.do_prog opt rp;
+          if !ai_edd_rel_dp then AI_EDD_Rel_DP.do_prog opt rp;
       end;
 
       if !vtest then do_test_interpret prog true
diff --git a/tests/source/half.scade b/tests/source/half.scade
index 541e81c..7e0df60 100644
--- a/tests/source/half.scade
+++ b/tests/source/half.scade
@@ -25,5 +25,5 @@ let
   c = a - b;
 
   guarantee c_bounded: c >= 0 and c <= 1;
-  guarantee link_c_half: (half and c = 1) or ((not half) and c = 0);
+  guarantee link_c_half: if half then (c = 1) else (c = 0);
 tel
diff --git a/tests/source/updown2.scade b/tests/source/updown2.scade
index 29c34ff..72d5bed 100644
--- a/tests/source/updown2.scade
+++ b/tests/source/updown2.scade
@@ -30,7 +30,7 @@ let
     guarantee y_bounded: y >= -bound and y <= bound;
 
     z = x + y;
-    guarantee x_y_opp: z = 0 and (true -> pre (z = 0));
+    guarantee x_y_opp: z = 0;
 tel
 
 node test(i: int) returns(a, b, c: int; exit: bool)