summaryrefslogtreecommitdiff
path: root/abstract
diff options
context:
space:
mode:
authorAlex Auvolat <alex.auvolat@ansys.com>2014-07-03 17:52:37 +0200
committerAlex Auvolat <alex.auvolat@ansys.com>2014-07-03 17:52:37 +0200
commitf808eeaf3016f828d71b0f87afb89bb79a869035 (patch)
treea3baddb1e45087512318be680161c09f7949ced2 /abstract
parent79bf56c809e727ed763e698386163706be2db0a7 (diff)
downloadscade-analyzer-f808eeaf3016f828d71b0f87afb89bb79a869035.tar.gz
scade-analyzer-f808eeaf3016f828d71b0f87afb89bb79a869035.zip
Changes to parser ; EDD optimisations ; test cases.
Diffstat (limited to 'abstract')
-rw-r--r--abstract/abs_interp_edd.ml151
1 files changed, 80 insertions, 71 deletions
diff --git a/abstract/abs_interp_edd.ml b/abstract/abs_interp_edd.ml
index fd31670..6220a0a 100644
--- a/abstract/abs_interp_edd.ml
+++ b/abstract/abs_interp_edd.ml
@@ -280,78 +280,86 @@ end = struct
edd_meet : edd_v -> edd_v -> edd_v
*)
let edd_join a b =
- let ve = a.ve in
- let leaves, get_leaf = get_leaf_fun () in
- let dq = new_node_fun () in
-
- let f f_rec na nb =
- match na, nb with
- | DChoice(_, va, la), DChoice(_, vb, lb) when va = vb ->
- let kl = List.map2
- (fun (ta, ba) (tb, bb) -> assert (ta = tb);
- ta, f_rec ba bb)
- la lb
- in
- dq va kl
-
- | DTop, _ | _, DTop -> DTop
- | DBot, DBot -> DBot
-
- | DChoice(_,va, la), _ when rank ve na < rank ve nb ->
- let kl = List.map (fun (k, ca) -> k, f_rec ca nb) la in
- dq va kl
- | _, DChoice(_, vb, lb) when rank ve nb < rank ve na ->
- let kl = List.map (fun (k, cb) -> k, f_rec na cb) lb in
- dq vb kl
-
- | DVal (u, _), DVal (v, _) ->
- let x = ND.join (Hashtbl.find a.leaves u) (Hashtbl.find b.leaves v) in
- get_leaf x
- | DVal(u, _), DBot ->
- get_leaf (Hashtbl.find a.leaves u)
- | DBot, DVal(v, _) ->
- get_leaf (Hashtbl.find b.leaves v)
-
- | _ -> assert false (* so that OCaml won't complain ; all cases ARE handled *)
- in
- { leaves; ve; root = time "join" (fun () -> memo2 f a.root b.root) }
+ if a.root = DBot then b else
+ if b.root = DBot then a else
+ if a.root = DTop || b.root = DTop then edd_top a.ve else begin
+ let ve = a.ve in
+ let leaves, get_leaf = get_leaf_fun () in
+ let dq = new_node_fun () in
+
+ let f f_rec na nb =
+ match na, nb with
+ | DChoice(_, va, la), DChoice(_, vb, lb) when va = vb ->
+ let kl = List.map2
+ (fun (ta, ba) (tb, bb) -> assert (ta = tb);
+ ta, f_rec ba bb)
+ la lb
+ in
+ dq va kl
+
+ | DTop, _ | _, DTop -> DTop
+ | DBot, DBot -> DBot
+
+ | DChoice(_,va, la), _ when rank ve na < rank ve nb ->
+ let kl = List.map (fun (k, ca) -> k, f_rec ca nb) la in
+ dq va kl
+ | _, DChoice(_, vb, lb) when rank ve nb < rank ve na ->
+ let kl = List.map (fun (k, cb) -> k, f_rec na cb) lb in
+ dq vb kl
+
+ | DVal (u, _), DVal (v, _) ->
+ let x = ND.join (Hashtbl.find a.leaves u) (Hashtbl.find b.leaves v) in
+ get_leaf x
+ | DVal(u, _), DBot ->
+ get_leaf (Hashtbl.find a.leaves u)
+ | DBot, DVal(v, _) ->
+ get_leaf (Hashtbl.find b.leaves v)
+
+ | _ -> assert false (* so that OCaml won't complain ; all cases ARE handled *)
+ in
+ { leaves; ve; root = time "join" (fun () -> memo2 f a.root b.root) }
+ end
let edd_meet a b =
- let ve = a.ve in
- let leaves, get_leaf = get_leaf_fun () in
- let dq = new_node_fun () in
-
- let f f_rec na nb =
- match na, nb with
- | DChoice(_, va, la), DChoice(_, vb, lb) when va = vb ->
- let kl = List.map2
- (fun (ta, ba) (tb, bb) -> assert (ta = tb);
- ta, f_rec ba bb)
- la lb
- in
- dq va kl
-
- | DBot, _ | _, DBot -> DBot
- | DTop, DTop -> DTop
-
- | DChoice(_, va, la), _ when rank ve na < rank ve nb ->
- let kl = List.map (fun (k, ca) -> k, f_rec ca nb) la in
- dq va kl
- | _, DChoice(_, vb, lb) when rank ve nb < rank ve na ->
- let kl = List.map (fun (k, cb) -> k, f_rec na cb) lb in
- dq vb kl
-
- | DVal (u, _) , DVal (v, _) ->
- let x = ND.meet (Hashtbl.find a.leaves u) (Hashtbl.find b.leaves v) in
- get_leaf x
- | DVal(u, _), DTop ->
- get_leaf (Hashtbl.find a.leaves u)
- | DTop, DVal(v, _) ->
- get_leaf (Hashtbl.find b.leaves v)
-
- | _ -> assert false (* see above *)
- in
- { leaves; ve; root = time "meet" (fun () -> memo2 f a.root b.root) }
+ if a.root = DTop then b else
+ if b.root = DTop then a else
+ if a.root = DBot || b.root = DBot then edd_bot a.ve else begin
+ let ve = a.ve in
+ let leaves, get_leaf = get_leaf_fun () in
+ let dq = new_node_fun () in
+
+ let f f_rec na nb =
+ match na, nb with
+ | DChoice(_, va, la), DChoice(_, vb, lb) when va = vb ->
+ let kl = List.map2
+ (fun (ta, ba) (tb, bb) -> assert (ta = tb);
+ ta, f_rec ba bb)
+ la lb
+ in
+ dq va kl
+
+ | DBot, _ | _, DBot -> DBot
+ | DTop, DTop -> DTop
+
+ | DChoice(_, va, la), _ when rank ve na < rank ve nb ->
+ let kl = List.map (fun (k, ca) -> k, f_rec ca nb) la in
+ dq va kl
+ | _, DChoice(_, vb, lb) when rank ve nb < rank ve na ->
+ let kl = List.map (fun (k, cb) -> k, f_rec na cb) lb in
+ dq vb kl
+
+ | DVal (u, _) , DVal (v, _) ->
+ let x = ND.meet (Hashtbl.find a.leaves u) (Hashtbl.find b.leaves v) in
+ get_leaf x
+ | DVal(u, _), DTop ->
+ get_leaf (Hashtbl.find a.leaves u)
+ | DTop, DVal(v, _) ->
+ get_leaf (Hashtbl.find b.leaves v)
+
+ | _ -> assert false (* see above *)
+ in
+ { leaves; ve; root = time "meet" (fun () -> memo2 f a.root b.root) }
+ end
@@ -407,7 +415,8 @@ end = struct
| CLFalse -> edd_bot v.ve
| CLAnd (a, b) ->
let v = edd_apply_cl v ([], nc, a) in
- edd_apply_cl v ([], nc, b)
+ if v.root = DBot then v else
+ edd_apply_cl v ([], nc, b)
| CLOr((eca, nca, ra), (ecb, ncb, rb)) ->
edd_join (edd_apply_cl v (eca, nc@nca, ra))
(edd_apply_cl v (ecb, nc@ncb, rb))