diff options
Diffstat (limited to 'abstract/abs_interp.ml')
| -rw-r--r-- | abstract/abs_interp.ml | 29 |
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; |