summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
authorAlex Auvolat <alex.auvolat@ansys.com>2014-07-09 09:40:37 +0200
committerAlex Auvolat <alex.auvolat@ansys.com>2014-07-09 09:40:37 +0200
commit26846118dc8038e12d46800e89b6fab5fecef948 (patch)
tree23089831c0ccf5bff220c9436a159fd888878838
parent4ecc11528b3490df5e2b8ea2c602d291b19c6bf0 (diff)
downloadscade-analyzer-26846118dc8038e12d46800e89b6fab5fecef948.tar.gz
scade-analyzer-26846118dc8038e12d46800e89b6fab5fecef948.zip
Add simplification pass && better heuristic for BDDs based on ternaries.
-rw-r--r--Makefile1
-rw-r--r--abstract/abs_interp.ml7
-rw-r--r--abstract/abs_interp_edd.ml31
-rw-r--r--abstract/formula.ml51
-rw-r--r--abstract/varenv.ml21
5 files changed, 97 insertions, 14 deletions
diff --git a/Makefile b/Makefile
index a6cc2d8..ffa531c 100644
--- a/Makefile
+++ b/Makefile
@@ -24,6 +24,7 @@ SRC= main.ml \
abstract/formula_printer.ml \
abstract/transform.ml \
\
+ abstract/varenv.ml \
abstract/abs_interp.ml \
abstract/abs_interp_edd.ml \
interpret/interpret.ml \
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)