summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorAlex Auvolat <alex.auvolat@ansys.com>2014-06-27 16:59:29 +0200
committerAlex Auvolat <alex.auvolat@ansys.com>2014-06-27 16:59:29 +0200
commitea25c6e61f585b263d3eac44a463e37116ce1e7f (patch)
treec5bd80d45478871dcb245fe9e53e3a7a681cfb34
parent11e7905ba16d4b13b5c2eda50a198391693e5d96 (diff)
downloadscade-analyzer-ea25c6e61f585b263d3eac44a463e37116ce1e7f.tar.gz
scade-analyzer-ea25c6e61f585b263d3eac44a463e37116ce1e7f.zip
More work on EDDs.
-rw-r--r--abstract/abs_interp.ml15
-rw-r--r--abstract/abs_interp_edd.ml458
-rw-r--r--main.ml7
3 files changed, 321 insertions, 159 deletions
diff --git a/abstract/abs_interp.ml b/abstract/abs_interp.ml
index bed2f2c..a612976 100644
--- a/abstract/abs_interp.ml
+++ b/abstract/abs_interp.ml
@@ -328,16 +328,11 @@ end = struct
pass_cycle : st -> case_v -> case_v
*)
let pass_cycle st (enum, num) =
- let assign_e =
- List.map (fun (a, b, _) -> a, b)
- (List.filter
- (fun (_, _, t) -> match t with TEnum _ -> true | _ -> false)
- st.cycle) in
- let assign_n =
- List.map (fun (a, b, _) -> a, NIdent b)
- (List.filter
- (fun (_, _, t) -> match t with TInt | TReal -> true | _ -> false)
- st.cycle) in
+ let assign_e, assign_n = List.fold_left
+ (fun (ae, an) (a, b, t) -> match t with
+ | TEnum _ -> (a, b)::ae, an
+ | TInt | TReal -> ae, (a, NIdent b)::an)
+ ([], []) st.cycle in
let enum = ED.assign enum assign_e in
let num = ND.assign num assign_n in
diff --git a/abstract/abs_interp_edd.ml b/abstract/abs_interp_edd.ml
index 4f2ad81..863a22d 100644
--- a/abstract/abs_interp_edd.ml
+++ b/abstract/abs_interp_edd.ml
@@ -7,10 +7,18 @@ open Util
open Num_domain
open Abs_interp
+let time id f =
+ Format.printf "%s[@?" id;
+ let r = f () in
+ Format.printf "] @?";
+ r
+
module I (ND : NUMERICAL_ENVIRONMENT_DOMAIN) : sig
val do_prog : cmdline_opt -> rooted_prog -> unit
+ val test : unit -> unit
+
end = struct
@@ -29,11 +37,10 @@ end = struct
ev_order : (id, int) Hashtbl.t;
}
- type edd_node =
+ type edd =
| DBot
| DVal of int
- | DChoice of id * (item * edd) list
- and edd = int * edd_node
+ | DChoice of int * id * (item * edd) list
type edd_v = {
ve : varenv;
@@ -45,41 +52,54 @@ end = struct
(*
Utility functions for memoization
- memo : (((int * 'a) -> (int * 'b)) -> 'a -> 'b) -> (int * 'a) -> (int * 'b)
- memo2 : (((int * 'a) -> (int * 'b) -> (int * 'c)) -> 'a -> 'b -> 'c) -> (int * 'a) -> (int * 'b) -> (int * 'c)
+ memo : (('a -> 'b) -> 'a -> 'b) -> 'a -> 'b
+ -> (int * 'a) -> (int * 'b)
+ memo2 : (('a -> 'b -> 'c) -> 'a -> 'b -> 'c)
+ -> 'a -> 'b -> 'c
+
+ Where 'a = 'b = 'c = edd, but it can be adapted.
*)
+ let key = function
+ | DBot -> None
+ | DVal i -> Some (Left i)
+ | DChoice(i, _, _) -> Some (Right i)
+
let memo f =
- let n = ref 0 in
let memo = Hashtbl.create 12 in
- let rec ff (id, v) =
- try Hashtbl.find memo id
+ let rec ff v =
+ try Hashtbl.find memo (key v)
with Not_found ->
let r = f ff v in
- incr n;
- Hashtbl.add memo id (n, r);
- n, r
+ Hashtbl.add memo (key v) r; r
in ff
let memo2 f =
- let n = ref 0 in
let memo = Hashtbl.create 12 in
- let rec ff (id1, v1) (id2, v2) =
- try Hashtbl.find memo (id1, id2)
+ let rec ff v1 v2 =
+ try Hashtbl.find memo (key v1, key v2)
with Not_found ->
let r = f ff v1 v2 in
- incr n;
- Hashtbl.add memo (id1, id2) (n, r);
- n, r
+ Hashtbl.add memo (key v1, key v2) r; r
in ff
+ let edd_node_eq = function
+ | DBot, DBot -> true
+ | DVal i, DVal j when i = j -> true
+ | DChoice(i, _, _), DChoice(j, _, _) when i = j -> true
+ | _ -> false
+
(*
edd_print : Format.formatter -> edd_v -> unit
*)
let edd_print fmt v =
+ let max_n = ref 0 in
+ let max_v = ref 0 in
+
let c_nodes = Hashtbl.create 12 in
let rec add = function
- | n, (DChoice(_, l) as x) ->
+ | DChoice(n, _, l) as x ->
if not (Hashtbl.mem c_nodes n) then begin
+ if n > !max_n then max_n := n;
Hashtbl.add c_nodes n x;
List.iter (fun (_, y) -> add y) l
end
@@ -87,31 +107,35 @@ end = struct
in add v.root;
let print_n fmt = function
- | (_, DBot) -> Format.fprintf fmt "⊥";
- | (_, DVal i) -> Format.fprintf fmt "v%d" i;
- | (n, DChoice _) -> Format.fprintf fmt "n%d" n
+ | DBot -> Format.fprintf fmt "⊥";
+ | DVal i -> if i > !max_v then max_v := i;
+ Format.fprintf fmt "v%d" i;
+ | DChoice(n, _, _) -> Format.fprintf fmt "n%d" n
in
Format.fprintf fmt "Root: %a@." print_n v.root;
- Hashtbl.iter
- (fun id x -> match x with
- | DChoice (var, l) ->
+ for id = !max_n downto 0 do
+ try match Hashtbl.find c_nodes id with
+ | DChoice (_, var, l) ->
let p fmt (c, l) = Format.fprintf fmt "%s → %a" c print_n l in
Format.fprintf fmt "n%d: %a ? @[<hov>%a@]@."
id Formula_printer.print_id var
(print_list p ", ") l
- | _ -> assert false)
- c_nodes;
- Hashtbl.iter
- (fun id v -> Format.fprintf fmt "v%d: %a@." id ND.print v)
- v.leaves
-
+ | _ -> assert false
+ with Not_found -> ()
+ done;
+
+ for id = 0 to !max_v do
+ try let v = Hashtbl.find v.leaves id in
+ Format.fprintf fmt "v%d: %a@." id ND.print v
+ with Not_found -> ()
+ done
(*
edd_bot : varenv -> edd_v
*)
- let edd_bot ve = { ve; root = (0, DBot); leaves = Hashtbl.create 1 }
+ let edd_bot ve = { ve; root = DBot; leaves = Hashtbl.create 1 }
(*
edd_top : evar list -> nvar list -> edd_v
@@ -119,7 +143,7 @@ end = struct
let edd_top ve =
let leaves = Hashtbl.create 1 in
Hashtbl.add leaves 0 (ND.top ve.nvars);
- { ve; root = (1, DVal 0); leaves }
+ { ve; root = DVal 0; leaves }
(*
edd_of_cons : varenv -> enum_cons -> edd_v
@@ -130,12 +154,12 @@ end = struct
let leaves = Hashtbl.create 1 in
Hashtbl.add leaves 0 (ND.top ve.nvars);
- let bot, top = (0, DBot), (1, DVal 0) in
+ let bot, top = DBot, DVal 0 in
let root = match r with
| EItem x ->
- 2, DChoice(vid,
- List.map (fun v -> if op v x then v, bot else v, top)
+ DChoice(0, vid,
+ List.map (fun v -> if op v x then v, top else v, bot)
(List.assoc vid ve.evars))
| EIdent vid2 ->
let a, b =
@@ -143,14 +167,14 @@ end = struct
then vid, vid2
else vid2, vid
in
- let n = ref 2 in
+ let n = ref 0 in
let nb x =
incr n;
- !n, DChoice(b,
+ DChoice(!n, b,
List.map (fun v -> if op v x then v, top else v, bot)
(List.assoc b ve.evars))
in
- 2, DChoice(a, List.map (fun x -> x, nb x) (List.assoc a ve.evars))
+ DChoice(0, a, List.map (fun x -> x, nb x) (List.assoc a ve.evars))
in
{ ve; root; leaves }
@@ -161,61 +185,63 @@ end = struct
let ve = a.ve in
let leaves = Hashtbl.create 12 in
+ let lc = ref 0 in
- let n = ref 0 in
let get_leaf x =
let id = ref None in
Hashtbl.iter (fun i v -> if ND.eq v x then id := Some i) leaves;
begin match !id with
| Some i -> DVal i
| None ->
- incr n;
- Hashtbl.add leaves !n x;
- DVal (!n)
+ incr lc;
+ Hashtbl.add leaves !lc x;
+ DVal (!lc)
end
in
-
+ let nc = ref 0 in
let f f_rec na nb =
let dq v l =
- let _, (i, x0) = List.hd l in
- if List.exists (fun (_, (j, x)) -> j <> i || x <> x0) l
- then DChoice(v, l)
- else x0
+ let _, x0 = List.hd l in
+ if List.exists (fun (_, x) -> not (edd_node_eq (x, x0))) l
+ then begin
+ incr nc; DChoice(!nc, v, l)
+ end else x0
in
match na, nb with
| DBot, DBot -> DBot
- | DBot, DVal i -> get_leaf (Hashtbl.find b.leaves i)
- | x, DBot -> x
+ | DBot, DVal i ->
+ get_leaf (Hashtbl.find b.leaves i)
+ | DVal i, DBot ->
+ get_leaf (Hashtbl.find a.leaves i)
+ | DVal u, DVal v ->
+ let x = ND.join (Hashtbl.find a.leaves u) (Hashtbl.find b.leaves v) in
+ get_leaf x
- | DChoice(va, la), DChoice(vb, lb) when va = vb ->
+ | DChoice(_, va, la), DChoice(_, vb, lb) when va = vb ->
let kl = List.map2
(fun (ta, ba) (tb, bb) -> assert (ta = tb);
- ta, f (ba, bb))
+ ta, f_rec ba bb)
la lb
in
dq va kl
- | DChoice(va, la), DChoice(vb, lb) ->
+ | DChoice(_, va, la), DChoice(_, vb, lb) ->
let v, kl =
if Hashtbl.find ve.ev_order va < Hashtbl.find ve.ev_order vb then
- va, List.map (fun (k, ca) -> k, f (ca, nb)) la
+ va, List.map (fun (k, ca) -> k, f_rec ca nb) la
else
- vb, List.map (fun (k, cb) -> k, f (na, cb)) lb
+ vb, List.map (fun (k, cb) -> k, f_rec na cb) lb
in
dq v kl
- | DChoice(va, la), _ ->
- let kl = List.map (fun (k, ca) -> k, f (ca, nb)) la in
+ | DChoice(_,va, la), _ ->
+ let kl = List.map (fun (k, ca) -> k, f_rec ca nb) la in
dq va kl
- | _, DChoice(vb, lb) ->
- let kl = List.map (fun (k, cb) -> k, f (na, cb)) lb in
+ | _, DChoice(_, vb, lb) ->
+ 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
in
- { leaves; ve; root = memo2 f a.root b.root }
+ { leaves; ve; root = time "join" (fun () -> memo2 f a.root b.root) }
(*
edd_meet : edd_v -> edd_v -> edd_v
@@ -223,7 +249,7 @@ end = struct
let edd_meet a b =
let ve = a.ve in
- let n = ref 0 in
+ let lc = ref 0 in
let leaves = Hashtbl.create 12 in
let get_leaf x =
@@ -233,59 +259,59 @@ end = struct
match !id with
| Some i -> DVal i
| None ->
- incr n;
- Hashtbl.add leaves !n x;
- DVal (!n)
+ incr lc;
+ Hashtbl.add leaves !lc x;
+ DVal (!lc)
end
in
- let memo = Hashtbl.create 12 in
- let rec f (na, nb) =
- try Hashtbl.find memo (na, nb)
- with Not_found -> let r =
- let dq v l =
- let _, x0 = List.hd l in
- if List.exists (fun (_, x) -> x <> x0) l
- then DChoice(v, l)
- else x0
+ let nc = ref 0 in
+ let f f_rec na nb =
+ let dq v l =
+ let _, x0 = List.hd l in
+ if List.exists (fun (_, x) -> not (edd_node_eq (x, x0))) l
+ then begin
+ incr nc; DChoice(!nc, v, l)
+ end else x0
+ in
+ match na, nb with
+ | DBot, _ | _, DBot -> DBot
+ | DVal u, DVal v ->
+ let x = ND.meet (Hashtbl.find a.leaves u) (Hashtbl.find b.leaves v) in
+ get_leaf x
+
+ | 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
- match na, nb with
- | DBot, _ | _, DBot -> DBot
- | DChoice(va, la), DChoice(vb, lb) when va = vb ->
- let kl = List.map2
- (fun (ta, ba) (tb, bb) -> assert (ta = tb);
- ta, f (ba, bb))
- la lb
- in
- dq va kl
- | DChoice(va, la), DChoice(vb, lb) ->
- let v, kl =
- if Hashtbl.find ve.ev_order va < Hashtbl.find ve.ev_order vb then
- va, List.map (fun (k, ca) -> k, f (ca, nb)) la
- else
- vb, List.map (fun (k, cb) -> k, f (na, cb)) lb
- in
- dq v kl
- | DChoice(va, la), _ ->
- let kl = List.map (fun (k, ca) -> k, f (ca, nb)) la in
- dq va kl
- | _, DChoice(vb, lb) ->
- let kl = List.map (fun (k, cb) -> k, f (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
- in Hashtbl.add memo (na, nb) r; r
+ dq va kl
+ | DChoice(_, va, la), DChoice(_, vb, lb) ->
+ let v, kl =
+ if Hashtbl.find ve.ev_order va < Hashtbl.find ve.ev_order vb then
+ va, List.map (fun (k, ca) -> k, f_rec ca nb) la
+ else
+ vb, List.map (fun (k, cb) -> k, f_rec na cb) lb
+ in
+ dq v kl
+ | DChoice(_, va, la), _ ->
+ let kl = List.map (fun (k, ca) -> k, f_rec ca nb) la in
+ dq va kl
+ | _, DChoice(_, vb, lb) ->
+ let kl = List.map (fun (k, cb) -> k, f_rec na cb) lb in
+ dq vb kl
in
- { leaves; ve; root = f (a.root, b.root) }
+ { leaves; ve; root = time "meet" (fun () -> memo2 f a.root b.root) }
(*
+ edd_num_apply : edd_v -> (ND.t -> ND.t) -> edd_v
edd_apply_ncl : edd_v -> num_cons list -> edd_v
*)
- let edd_apply_ncl v ncl =
+ let edd_num_apply v nfun =
let ve = v.ve in
- let n = ref 0 in
+ let lc = ref 0 in
let leaves = Hashtbl.create 12 in
let get_leaf x =
@@ -295,36 +321,48 @@ end = struct
match !id with
| Some i -> DVal i
| None ->
- incr n;
- Hashtbl.add leaves !n x;
- DVal (!n)
+ incr lc;
+ Hashtbl.add leaves !lc x;
+ DVal (!lc)
end
in
- let memo = Hashtbl.create 12 in
- let rec f n =
- try Hashtbl.find memo n
- with Not_found -> let r =
- match n with
- | DBot -> DBot
- | DVal i -> get_leaf (ND.apply_cl (Hashtbl.find v.leaves i) ncl)
- | DChoice(var, l) ->
- let l = List.map (fun (k, v) -> k, f v) l in
- let _, x0 = List.hd l in
- if List.exists (fun (_, x) -> x <> x0) l
- then DChoice(var, l)
- else x0
- in Hashtbl.add memo n r; r
+ let f f_rec n =
+ match n with
+ | DBot -> DBot
+ | DVal i -> get_leaf (nfun (Hashtbl.find v.leaves i))
+ | DChoice(n, var, l) ->
+ let l = List.map (fun (k, v) -> k, f_rec v) l in
+ let _, x0 = List.hd l in
+ if List.exists (fun (_, x) -> not (edd_node_eq (x, x0))) l
+ then DChoice(n, var, l)
+ else x0
+ in
+ { leaves; ve; root = memo f v.root }
+
+ let edd_apply_ncl v ncl =
+ edd_num_apply v (fun n -> ND.apply_cl n ncl)
+
+ (*
+ edd_apply_ecl : edd_v -> enum_cons list -> edd_v
+ *)
+ let edd_apply_ecl v ec =
+ let rec cl_k = function
+ | [] -> edd_top v.ve
+ | [a] -> edd_of_cons v.ve a
+ | l ->
+ let n = ref 0 in
+ let la, lb = List.partition (fun _ -> incr n; !n mod 2 = 0) l in
+ edd_meet (cl_k la) (cl_k lb)
in
- { leaves; ve; root = f v.root }
+ let cons_edd = cl_k ec in
+ edd_meet v cons_edd
(*
edd_apply_cl : edd_v -> conslist -> edd_v
*)
let rec edd_apply_cl v (ec, nc, r) =
- let v = List.fold_left
- (fun v cons -> edd_meet v (edd_of_cons v.ve cons))
- v ec in
+ let v = edd_apply_ecl v ec in
match r with
| CLTrue ->
edd_apply_ncl v nc
@@ -340,23 +378,100 @@ end = struct
edd_eq : edd_v -> edd_v -> bool
*)
let edd_eq a b =
+ let f f_rec na nb =
+ match na, nb with
+ | DBot, DBot -> true
+ | DVal i, DVal j ->
+ ND.eq (Hashtbl.find a.leaves i) (Hashtbl.find b.leaves j)
+ | DChoice(_, va, la), DChoice(_, vb, lb) when va = vb ->
+ List.for_all2 (fun (ca, na) (cb, nb) -> assert (ca = cb); f_rec na nb)
+ la lb
+ | _ -> false
+ in memo2 f a.root b.root
+
+
+ (*
+ edd_forget_vars : edd_v -> id list -> edd_v
+ *)
+ let edd_forget_vars v vars =
+ let ve = v.ve in
+
+ let leaves = Hashtbl.create 12 in
+ let lc = ref 0 in
+
+ let get_leaf x =
+ let id = ref None in
+ Hashtbl.iter (fun i v -> if ND.eq v x then id := Some i) leaves;
+ begin match !id with
+ | Some i -> DVal i
+ | None ->
+ incr lc;
+ Hashtbl.add leaves !lc x;
+ DVal (!lc)
+ end
+ in
+
+ let nc = ref 0 in
let memo = Hashtbl.create 12 in
- let rec f (na, nb) =
- try Hashtbl.find memo (na, nb)
- with Not_found -> let r =
- match na, nb with
- | DBot, DBot -> true
- | DVal i, DVal j ->
- ND.eq (Hashtbl.find a.leaves i) (Hashtbl.find b.leaves j)
- | DChoice(va, la), DChoice(vb, lb) when va = vb ->
- List.for_all2 (fun (ca, na) (cb, nb) -> assert (ca = cb); f (na, nb))
- la lb
- | _ -> false
- in Hashtbl.add memo (na, nb) r; r
- in f (a.root, b.root)
+ let rec f l =
+ let kl = List.sort Pervasives.compare (List.map key l) in
+ try Hashtbl.find memo kl
+ with Not_found -> let r =
+ let cn, fn = List.fold_left
+ (fun (cn, fn) node -> match node with
+ | DBot -> cn, fn
+ | DVal i -> cn, i::fn
+ | DChoice (n, v, l) -> (n, v, l)::cn, fn)
+ ([], []) l in
+ let cn = List.sort
+ (fun (n, v1, _) (n, v2, _) -> Pervasives.compare
+ (Hashtbl.find ve.ev_order v1) (Hashtbl.find ve.ev_order v2))
+ cn in
+ if cn = [] then
+ if fn = [] then DBot
+ else
+ let x = list_fold_op ND.join
+ (List.map (Hashtbl.find v.leaves) fn)
+ in get_leaf x
+ else
+ let _, dv, cl = List.hd cn in
+ let d, nd = List.partition (fun (_, v, _) -> v = dv) cn in
+ let ch1 = List.map (fun (a, b, c) -> DChoice(a, b, c)) nd in
+ let ch2 = List.map (fun i -> DVal i) fn in
+ if List.mem dv vars then
+ (* Do union of all branches branching from nodes on variable dv *)
+ let ch3 = List.flatten
+ (List.map (fun (_, _, c) -> List.map snd c) d) in
+ f (ch1@ch2@ch3)
+ else
+ (* Keep disjunction on variable dv *)
+ let d, nd = List.partition (fun (_, v, _) -> v = dv) cn in
+ let cc = List.map
+ (fun (c, _) ->
+ let ch3 = List.map (fun (_, _, cl) -> List.assoc c cl) d in
+ c, f (ch1@ch2@ch3))
+ cl in
+ let _, x0 = List.hd cc in
+ if List.exists (fun (_, x) -> not (edd_node_eq (x, x0))) cc
+ then begin
+ incr nc; DChoice(!nc, dv, cc)
+ end else x0
+ in Hashtbl.add memo kl r; r
+ in
+ { leaves; ve; root = f [v.root] }
+
+ (*
+ edd_eassign : edd_v -> (id * id) list -> edd_v
+ *)
+ let edd_eassign v ids =
+ let v = edd_forget_vars v (List.map fst ids) in
+ edd_apply_ecl v
+ (List.map (fun (x, y) -> (E_EQ, x, EIdent y)) ids)
(*
+ Just a function to test EDDs
+ *)
let test () =
let ve = {
evars = ["x", ["tt"; "ff"]; "y", ["tt"; "ff"]; "z", ["tt"; "ff"]];
@@ -372,8 +487,11 @@ end = struct
let w = edd_meet u v in
Format.printf "x = y && y != z : @[%a@]@." edd_print w;
let t = edd_join u v in
- Format.printf "x = y || y != z : @[%a@]@." edd_print t
- *)
+ Format.printf "x = y || y != z : @[%a@]@." edd_print t;
+ let e = edd_forget_vars w ["y"] in
+ Format.printf "x = y && y != z ; forget y : @[%a@]@." edd_print e;
+ let f = edd_forget_vars t ["y"] in
+ Format.printf "x = y || y != z ; forget y : @[%a@]@." edd_print f
(* ******************************
@@ -399,6 +517,29 @@ end = struct
mutable data : edd_v;
}
+
+ (*
+ pass_cycle : env -> edd_v -> edd_v
+ *)
+ let pass_cycle env v =
+ let assign_e, assign_n = List.fold_left
+ (fun (ae, an) (a, b, t) -> match t with
+ | TEnum _ -> (a, b)::ae, an
+ | TInt | TReal -> ae, (a, NIdent b)::an)
+ ([], []) env.cycle in
+
+ let v = edd_eassign v assign_e in
+ let v = edd_num_apply v (fun nv -> ND.assign nv assign_n) in
+
+ let ef, nf = List.fold_left
+ (fun (ef, nf) (var, t) -> match t with
+ | TEnum _ -> var::ef, nf
+ | TReal | TInt -> ef, var::nf)
+ ([], []) env.forget in
+
+ let v = edd_forget_vars v ef in
+ edd_num_apply v (fun nv -> List.fold_left ND.forgetvar nv nf)
+
(*
extract_linked_evars : conslist -> (id * id) list
@@ -554,7 +695,7 @@ end = struct
(List.sort Pervasives.compare (List.map ord_couple lv1)) in
let lv2 = uniq_sorted
(List.sort Pervasives.compare (List.map ord_couple lv2)) in
- let evars_ord = scope_constrict evars (lv0 @ lv1 @ lv2) in
+ let evars_ord = List.rev @@ scope_constrict evars ( lv1 ) in
let ev_order = Hashtbl.create (List.length evars) in
List.iteri (fun i x -> Hashtbl.add ev_order x i) evars_ord;
@@ -591,8 +732,35 @@ end = struct
let do_prog opt rp =
let e = init_env opt rp in
- let d2 = edd_apply_cl e.data e.cl in
- Format.printf " -> @[<hov>%a@]@." edd_print d2
+ let rec f x =
+ Format.printf "Apply formula...@.";
+ let d2 = edd_apply_cl x e.cl in
+ Format.printf "Pass cycle...@.";
+ let dc = pass_cycle e d2 in
+ Format.printf "Join with init...@.";
+ let dcc = edd_join dc e.data in
+ Format.printf "@[<hov>%a@]@.@." edd_print dcc;
+ if not (edd_eq x dcc) then f dcc else dcc
+ in
+
+ let final = edd_apply_cl (f e.data) e.cl in
+ (*Format.printf "@.Final:@.@[<hov>%a@]@." edd_print final;*)
+
+ let check_guarantee (id, f) =
+ let cl = Formula.conslist_of_f f in
+ Format.printf "@[<hv 4>%s:@ %a ⇒ ⊥ @ "
+ id Formula_printer.print_conslist cl;
+ let z = edd_apply_cl final cl in
+ if z.root = DBot then
+ Format.printf "OK@]@ "
+ else
+ Format.printf "FAIL@]@ "
+ in
+ if e.guarantees <> [] then begin
+ Format.printf "Guarantee @[<v 0>";
+ List.iter check_guarantee e.guarantees;
+ Format.printf "@]@."
+ end;
end
diff --git a/main.ml b/main.ml
index d526a76..dde682f 100644
--- a/main.ml
+++ b/main.ml
@@ -12,9 +12,7 @@ module ItvND = Nonrelational.ND(Intervals_domain.VD)
module AI_Itv = Abs_interp.I(Enum_domain.MultiValuation)(ItvND)
module AI_Rel = Abs_interp.I(Enum_domain.MultiValuation)(Apron_domain.ND)
-(*
module AI_Itv_EDD = Abs_interp_edd.I(ItvND)
-*)
(* command line options *)
let dump = ref false
@@ -82,6 +80,8 @@ let do_test_interpret prog verbose =
it 0 s0
let () =
+ AI_Itv_EDD.test ();
+
Arg.parse options (fun f -> ifile := f) usage;
if !ifile = "" then begin
@@ -117,9 +117,8 @@ let () =
if !ai_itv then AI_Itv.do_prog opt rp;
if !ai_rel then AI_Rel.do_prog opt rp;
- (*
+
if !ai_itv_edd then AI_Itv_EDD.do_prog opt rp;
- *)
end;
if !vtest then do_test_interpret prog true