diff options
Diffstat (limited to 'abstract')
| -rw-r--r-- | abstract/abs_interp.ml | 7 | ||||
| -rw-r--r-- | abstract/abs_interp_edd.ml | 31 | ||||
| -rw-r--r-- | abstract/formula.ml | 51 | ||||
| -rw-r--r-- | abstract/varenv.ml | 21 |
4 files changed, 96 insertions, 14 deletions
diff --git a/abstract/abs_interp.ml b/abstract/abs_interp.ml index cb5ae9c..2597a63 100644 --- a/abstract/abs_interp.ml +++ b/abstract/abs_interp.ml @@ -171,7 +171,6 @@ end = struct (* program expressions *) cl : conslist; - cl_g : conslist; guarantees : (id * bool_expr) list; (* abstract interpretation *) @@ -275,13 +274,11 @@ end = struct *) let init_state opt rp = let init_f, f = Transform.f_of_prog rp false in - let _, f_g = Transform.f_of_prog rp true in Format.printf "Init formula: %a@.@." Formula_printer.print_expr init_f; Format.printf "Cycle formula:@.%a@.@." Formula_printer.print_expr f; let init_cl = conslist_of_f init_f in let cl = Formula.conslist_of_f f in - let cl_g = Formula.conslist_of_f f_g in Format.printf "Cycle conslist:@.%a@.@." Formula_printer.print_conslist cl; let guarantees = Transform.guarantees_of_prog rp in @@ -294,7 +291,7 @@ end = struct (* add variables from LASTs *) let last_vars = uniq_sorted - (List.sort compare (Transform.extract_last_vars f_g)) in + (List.sort compare (Transform.extract_last_vars f)) in let last_vars = List.map (fun id -> let (_, _, ty) = List.find (fun (_, u, _) -> id = "L"^u) rp.all_vars @@ -336,7 +333,7 @@ end = struct let st = { rp; opt; enum_vars; num_vars; all_vars; - cl; cl_g; guarantees; + cl; guarantees; cycle; forget; acc_d_vars; d_vars; top; env = Hashtbl.create 12; delta; widen } in diff --git a/abstract/abs_interp_edd.ml b/abstract/abs_interp_edd.ml index 56b366e..a439995 100644 --- a/abstract/abs_interp_edd.ml +++ b/abstract/abs_interp_edd.ml @@ -779,6 +779,37 @@ end = struct (* HERE POSSIBILITY OF SIMPLIFYING EQUATIONS SUCH AS x = y OR x = v *) (* IF SUCH AN EQUATION APPEARS IN get_root_true f THEN IT IS ALWAYS TRUE *) + let facts = get_root_true f in + let f, rp, _ = List.fold_left + (fun (f, (rp : rooted_prog), repls) eq -> + match eq with + | BEnumCons(E_EQ, a, EIdent b) + when a.[0] <> 'L' && b.[0] <> 'L' -> + + let a = try List.assoc a repls with Not_found -> a in + let b = try List.assoc b repls with Not_found -> b in + + if a = b then + f, rp, repls + else begin + let keep, repl = + if String.length a <= String.length b + then a, b + else b, a + in + Format.printf "Replacing %s with %s@." repl keep; + let f = formula_replace_evars [repl, keep; "L"^repl, "L"^keep] f in + let rp = + { rp with all_vars = + List.filter (fun (_, id, _) -> id <> repl) rp.all_vars } in + let repls = (repl, keep):: + (List.map (fun (r, k) -> r, if k = repl then keep else k) repls) in + f, rp, repls + end + | _ -> f, rp, repls) + (f, rp, []) facts in + Format.printf "Complete formula after simpl:@.%a@.@." + Formula_printer.print_expr f; let init_f = simplify_k [BEnumCons(E_EQ, "L/must_reset", EItem bool_true)] f in let f = simplify_k [BEnumCons(E_NE, "L/must_reset", EItem bool_true)] f in diff --git a/abstract/formula.ml b/abstract/formula.ml index 4c2c397..f2a3bd1 100644 --- a/abstract/formula.ml +++ b/abstract/formula.ml @@ -212,15 +212,10 @@ let rec simplify true_eqs e = (simplify true_eqs a) (simplify true_eqs b) | BTernary(c, a, b) -> - let c, a, b = - simplify true_eqs c, - simplify true_eqs a, - simplify true_eqs b in - begin match c with - | BConst true -> a - | BConst false -> b - | _ -> BTernary(c, a, b) - end + f_ternary + (simplify true_eqs c) + (simplify true_eqs a) + (simplify true_eqs b) | BNot(n) -> begin match simplify true_eqs n with | BConst e -> BConst (not e) @@ -230,3 +225,41 @@ let rec simplify true_eqs e = let rec simplify_k true_eqs e = List.fold_left f_and (simplify true_eqs e) true_eqs + + + +(* + Simplify a formula replacing a variable with another +*) + +let rec formula_replace_evars repls e = + let new_name x = + try List.assoc x repls + with Not_found -> x + in + match e with + | BOr(a, b) -> + f_or (formula_replace_evars repls a) (formula_replace_evars repls b) + | BAnd(a, b) -> + f_and (formula_replace_evars repls a) (formula_replace_evars repls b) + | BTernary(c, a, b) -> + f_ternary + (formula_replace_evars repls c) + (formula_replace_evars repls a) + (formula_replace_evars repls b) + | BNot(n) -> + begin match formula_replace_evars repls n with + | BConst e -> BConst (not e) + | x -> BNot x + end + | BEnumCons (op, a, EIdent b) -> + let a', b' = new_name a, new_name b in + if a' = b' then + match op with | E_EQ -> BConst true | E_NE -> BConst false + else + BEnumCons(op, a', EIdent b') + | BEnumCons (op, a, EItem x) -> + BEnumCons (op, new_name a, EItem x) + | x -> x + + diff --git a/abstract/varenv.ml b/abstract/varenv.ml index 1aa17b4..5d51837 100644 --- a/abstract/varenv.ml +++ b/abstract/varenv.ml @@ -49,6 +49,26 @@ let rec extract_const_vars_root (ecl, _, _) = [] ecl +let extract_choice_groups f = + let rec aux w = function + | BNot n -> aux w n + | BRel _ | BConst _ -> [], [] + | BEnumCons(_, x, EItem _) -> [], [x] + | BEnumCons(_, x, EIdent y) -> [], [y] + | BAnd(a, b) | BOr(a, b) -> + let ga, va = aux w a in + let gb, vb = aux w b in + ga@gb, va@vb + | BTernary(c, a, b) -> + let gc, vc = aux (w /. 3.) c in + let ga, va = aux (w /. 2.) a in + let gb, vb = aux (w /. 2.) b in + let v = uniq_sorted (List.sort compare (vc@va@vb)) in + (w, v)::(gc@ga@gb), v + in + fst (aux 0.6 f) + + (* scope_constrict : id list -> (id * id) list -> id list @@ -215,6 +235,7 @@ let mk_varenv (rp : rooted_prog) f cl = let lv_f = lv_f @ (List.map (fun v -> (0.7, [v; "L"^v])) (List.filter (fun n -> List.mem ("L"^n) evars) evars)) in + let lv_f = lv_f @ (extract_choice_groups f) in let evars_ord = if true then time "FORCE" (fun () -> force_ordering evars lv_f) |