Add command line option : verbose chaotic iterations.

1 files changed, 17 insertions, 12 deletions

diff --git a/abstract/abs_interp.ml b/abstract/abs_interp.ml
index 8d5f1c9..f526095 100644
--- a/abstract/abs_interp.ml
+++ b/abstract/abs_interp.ml
@@ -7,12 +7,18 @@ open Util
 open Num_domain
 open Enum_domain
 
+type cmdline_opt = {
+    widen_delay       : int;
+    disjunct          : (id -> bool);
+    verbose_ci        : bool;
+}
+
 
 module I (ED : ENUM_ENVIRONMENT_DOMAIN) (ND : NUMERICAL_ENVIRONMENT_DOMAIN) : sig
 
     type st
 
-    val do_prog     : int -> (id -> bool) -> rooted_prog -> unit
+    val do_prog : cmdline_opt -> rooted_prog -> unit
 
 end = struct
 
@@ -161,7 +167,7 @@ end = struct
 
     type st = {
         rp          : rooted_prog;
-        widen_delay : int;
+        opt         : cmdline_opt;
 
         enum_vars   : (id * ED.item list) list;
         num_vars    : (id * bool) list;
@@ -199,7 +205,7 @@ end = struct
             if (not (ED.subset enum e0)) || (not (ND.subset num n0)) then begin
               begin try
                 let n = Hashtbl.find st.widen case in
-                let jw = if n < st.widen_delay then ND.join else ND.widen in
+                let jw = if n < st.opt.widen_delay then ND.join else ND.widen in
                 Hashtbl.replace st.env case (ED.join e0 enum, jw n0 num);
                 Hashtbl.replace st.widen case (n+1);
               with Not_found ->
@@ -225,7 +231,7 @@ end = struct
     (*
       init_state : int -> rooted_prog -> st
     *)
-    let init_state widen_delay disj rp =
+    let init_state opt rp =
       Format.printf "Vars: @[<hov>%a@]@.@."
           (Ast_printer.print_list Ast_printer.print_typed_var ", ")
           rp.all_vars;
@@ -253,8 +259,6 @@ end = struct
       let f = Formula.eliminate_not (Transform.f_of_prog rp false) in
       let f_g = Formula.eliminate_not (Transform.f_of_prog rp true) in
       Format.printf "Cycle formula:@.%a@.@." Formula_printer.print_expr f;
-      Format.printf "Cycle formula with guarantees:@.%a@.@."
-          Formula_printer.print_expr f_g;
 
       let cl = Formula.conslist_of_f f in
       let cl_g = Formula.conslist_of_f f_g in
@@ -288,7 +292,7 @@ end = struct
       in
       let d_vars_0 = calculate_dvars init_cl in
       let d_vars_1 = List.filter
-          (fun id -> disj id && not (List.mem id d_vars_0) && id.[0] <> 'N')
+          (fun id -> opt.disjunct id && not (List.mem id d_vars_0) && id.[0] <> 'N')
           (List.map (fun (id, _) -> id) enum_vars) in
       let d_vars = d_vars_0 @ d_vars_1 in
 
@@ -310,7 +314,7 @@ end = struct
       let env = env_dd.data in
       
       let st = 
-      { rp; widen_delay; enum_vars; num_vars;
+      { rp; opt; enum_vars; num_vars;
         f; cl; f_g; cl_g; guarantees;
         cycle; forget; d_vars; top;
         env; delta; widen } in
@@ -372,8 +376,8 @@ end = struct
     (*
       do_prog : rooted_prog -> unit
     *)
-    let do_prog widen_delay disj rp =
-      let st = init_state widen_delay disj rp in
+    let do_prog opt rp =
+      let st = init_state opt rp in
 
       Format.printf "Init: %a@." print_st st;
 
@@ -400,7 +404,7 @@ end = struct
         let rec iter n (i_enum, i_num) =
           let fi_enum, fi_num = f (i_enum, i_num) in
           let j_enum, j_num =
-            if n < st.widen_delay then
+            if n < st.opt.widen_delay then
               ED.join i_enum fi_enum, ND.join i_num fi_num
             else
               ED.join i_enum fi_enum, ND.widen i_num fi_num
@@ -425,7 +429,8 @@ end = struct
 
         st.delta <- List.filter ((<>) case) st.delta;
 
-        (* Format.printf "Final: %a@." print_st st; *)
+        if st.opt.verbose_ci then
+          Format.printf "-> @[<hov>%a@]@." print_st st;
 
       done;