diff options
Diffstat (limited to 'abstract/abs_interp.ml')
| -rw-r--r-- | abstract/abs_interp.ml | 18 |
1 files changed, 7 insertions, 11 deletions
diff --git a/abstract/abs_interp.ml b/abstract/abs_interp.ml index c3b2d79..0db128f 100644 --- a/abstract/abs_interp.ml +++ b/abstract/abs_interp.ml @@ -174,9 +174,7 @@ end = struct num_vars : (id * bool) list; (* program expressions *) - f : bool_expr; cl : conslist; - f_g : bool_expr; cl_g : conslist; guarantees : (id * bool_expr) list; @@ -237,14 +235,12 @@ end = struct (print_list Ast_printer.print_typed_var ", ") rp.all_vars; - let enum_vars = List.fold_left - (fun v (_, id, t) -> match t with - | TEnum ch -> (id, ch)::v | _ -> v) - [] rp.all_vars in - let num_vars = List.fold_left - (fun v (_, id, t) -> match t with - | TInt -> (id, false)::v | TReal -> (id, true)::v | _ -> v) - [] rp.all_vars in + let num_vars, enum_vars = List.fold_left + (fun (nv, ev) (_, id, t) -> match t with + | TEnum ch -> nv, (id, ch)::ev + | TInt -> (id, false)::nv, ev + | TReal -> (id, true)::nv, ev) + ([], []) rp.all_vars in let init_f = Transform.init_f_of_prog rp in Format.printf "Init formula: %a@.@." Formula_printer.print_expr init_f; @@ -317,7 +313,7 @@ end = struct let st = { rp; opt; enum_vars; num_vars; - f; cl; f_g; cl_g; guarantees; + cl; cl_g; guarantees; cycle; forget; d_vars; top; env; delta; widen } in |