Add gilbreath suite ; booleans are not represented in a good way.

1 files changed, 14 insertions, 13 deletions

diff --git a/abstract/abs_interp.ml b/abstract/abs_interp.ml
index 4c3fddb..feaf037 100644
--- a/abstract/abs_interp.ml
+++ b/abstract/abs_interp.ml
@@ -9,12 +9,13 @@ module I (E : ENVIRONMENT_DOMAIN) : sig
 
     type st
 
-    val do_prog     : prog -> id -> unit
+    val do_prog     : int -> prog -> id -> unit
 
 end = struct
 
     type st = {
         p           : prog;
+        widen_delay : int;
         root_scope  : scope;
         all_vars    : var_def list;
         env         : E.t;
@@ -69,7 +70,7 @@ end = struct
         (List.flatten (List.map vars_of_eq eqs))
 
     (* init state *)
-    let init_state p root =
+    let init_state widen_delay p root =
       let root_scope = get_root_scope p root in
 
       let f = Formula.eliminate_not (Transform.f_of_prog p root) in
@@ -86,11 +87,11 @@ end = struct
       Format.printf "Init formula: %a@.@." Formula_printer.print_expr init_f;
       Format.printf "Cycle formula: %a@.@." Formula_printer.print_expr f;
 
-      Format.printf "Vars: %a@.@." (Ast_printer.print_list Ast_printer.print_var_decl ", ") all_vars;
+      Format.printf "Vars: @[<hov>%a@]@.@." (Ast_printer.print_list Ast_printer.print_var_decl ", ") all_vars;
 
       let env = E.apply_f env init_f in
 
-      { p; root_scope; f; cl; all_vars; env }
+      { p; root_scope; widen_delay; f; cl; all_vars; env }
 
     (*
       pass_cycle : var_def list -> E.t -> E.t
@@ -121,13 +122,12 @@ end = struct
 
     (* cycle : st -> cl -> env -> env *)
     let cycle st cl i =
-      E.apply_cl (pass_cycle st.all_vars i) cl
+      (pass_cycle st.all_vars (E.apply_cl i cl)) 
 
     (*
       loop : st -> cl -> env -> env -> env
     *)
     let loop st cycle_cl pnew stay =
-      let pnew = E.apply_cl pnew cycle_cl in
 
       Format.printf "Loop @[<hv>%a@]@.New @[<hv>%a@]@.Stay @[<hv>%a@]@."
         Formula_printer.print_conslist cycle_cl
@@ -142,10 +142,9 @@ end = struct
         E.join acc0 j
       in
 
-      let widen_delay = 10 in
       let rec iter n i =
         let i' =
-          if n < widen_delay
+          if n < st.widen_delay
             then E.join i (fsharp i)
             else E.widen i (fsharp i)
         in
@@ -159,21 +158,23 @@ end = struct
     (*
       do_prog : prog -> id -> unit
     *)
-    let do_prog p root =
-      let st = init_state p root in
+    let do_prog widen_delay p root =
+      let st = init_state widen_delay p root in
 
       let pnew = st.env in
 
       let stay = loop st st.cl pnew (E.vbottom pnew) in
 
-      Format.printf "@[<hov>Final stay %a@]@."
-        E.print_all stay;
+      let final = E.join (E.apply_cl pnew st.cl) (E.apply_cl stay st.cl) in
+
+      Format.printf "@[<hov>Final %a@]@."
+        E.print_all final;
 
       Format.printf "Probes:@[<hov>";
       List.iter (fun (p, id, _) ->
         if p then Format.printf "@ %a ∊ %a,"
               Formula_printer.print_id id
-              E.print_itv (E.var_itv stay id))
+              E.print_itv (E.var_itv final id))
         st.all_vars;
       Format.printf "@]@."