open Ast
open Formula
open Util
module type ENUM_ENVIRONMENT_DOMAIN2 = sig
type t
type item = string
(* construction *)
val top : (id * item list) list -> t
val bottom : (id * item list) list -> t
val is_bot : t -> bool
(* variable management *)
val vars : t -> (id * item list) list
val forgetvar : t -> id -> t
val forgetvars : t -> id list -> t
val project : t -> id -> item list
(* set-theoretic operations *)
val join : t -> t -> t (* union *)
val meet : t -> t -> t (* intersection *)
val subset : t -> t -> bool
val eq : t -> t -> bool
(* abstract operations *)
val apply_cons : t -> enum_cons -> t
val apply_cl : t -> enum_cons list -> t
val assign : t -> (id * id) list -> t
(* pretty-printing *)
val print : Format.formatter -> t -> unit
end
module EDD : ENUM_ENVIRONMENT_DOMAIN2 = struct
exception Top
type item = string
type edd =
| DBot
| DTop
| DChoice of int * id * (item * edd) list
type t = {
vars : (id * item list) list;
order : (id, int) Hashtbl.t;
root : edd;
}
(* Utility functions for memoization *)
let key = function
| DBot -> -1
| DTop -> -2
| DChoice(i, _, _) -> i
let memo f =
let memo = Hashtbl.create 12 in
let rec ff v =
try Hashtbl.find memo (key v)
with Not_found ->
let r = f ff v in
Hashtbl.add memo (key v) r; r
in ff
let memo2 f =
let memo = Hashtbl.create 12 in
let rec ff v1 v2 =
try Hashtbl.find memo (key v1, key v2)
with Not_found ->
let r = f ff v1 v2 in
Hashtbl.add memo (key v1, key v2) r; r
in ff
let edd_node_eq = function
| DBot, DBot -> true
| DTop, DTop -> true
| DChoice(i, _, _), DChoice(j, _, _) -> i = j
| _ -> false
let new_node_fun () =
let nc = ref 0 in
let node_memo = Hashtbl.create 12 in
fun v l ->
let _, x0 = List.hd l in
if List.exists (fun (_, x) -> not (edd_node_eq (x, x0))) l
then begin
let k = (v, List.map (fun (a, b) -> a, key b) l) in
let n =
try Hashtbl.find node_memo k
with _ -> (incr nc; Hashtbl.add node_memo k !nc; !nc)
in
DChoice(n, v, l)
end else x0
let rank v = function
| DChoice(_, x, _) -> Hashtbl.find v.order x
| _ -> 10000000
(*
print : Format.formatter -> t -> unit
*)
let print fmt v =
let print_nodes = Queue.create () in
let a = Hashtbl.create 12 in
let node_pc = Hashtbl.create 12 in
let f f_rec = function
| DChoice(_, _, l) ->
List.iter
(fun (_, c) -> match c with
| DChoice(n, _, _) ->
begin try Hashtbl.add node_pc n (Hashtbl.find node_pc n + 1)
with Not_found -> Hashtbl.add node_pc n 1 end
| _ -> ())
l;
List.iter (fun (_, c) -> f_rec c) l
| _ -> ()
in memo f v.root;
let rec print_n fmt = function
| DBot -> Format.fprintf fmt "⊥";
| DTop -> Format.fprintf fmt "⊤";
| DChoice(_, v, l) ->
match List.filter (fun (_, x) -> x <> DBot) l with
| [(c, nn)] ->
let aux fmt = function
| DChoice(nn, _, _) as i when Hashtbl.find node_pc nn >= 2 ->
if Hashtbl.mem a nn then () else begin
Queue.push i print_nodes;
Hashtbl.add a nn ()
end;
Format.fprintf fmt "n%d" nn
| x -> print_n fmt x
in
Format.fprintf fmt "%a = %s,@ %a" Formula_printer.print_id v c aux nn
| _ ->
Format.fprintf fmt "%a ? " Formula_printer.print_id v;
let print_u fmt (c, i) =
Format.fprintf fmt "%s → " c;
match i with
| DChoice(nn, v, l) ->
if Hashtbl.mem a nn then () else begin
Queue.push i print_nodes;
Hashtbl.add a nn ()
end;
Format.fprintf fmt "n%d" nn
| _ -> Format.fprintf fmt "%a" print_n i
in
Format.fprintf fmt "@[<h>%a@]" (print_list print_u ", ") l;
in
Format.fprintf fmt "@[<v 4>{ @[<hov>%a@]" print_n v.root;
while not (Queue.is_empty print_nodes) do
match Queue.pop print_nodes with
| DChoice(n, v, l) as x ->
Format.fprintf fmt "@ n%d: @[<hov>%a@]" n print_n x
| _ -> assert false
done;
Format.fprintf fmt " }@]"
(*
top : (id * item list) list -> t
bot : (id * item list) list -> t
*)
let top vars =
let order = Hashtbl.create 12 in
List.iteri (fun i (id, _) -> Hashtbl.add order id i) vars;
{ vars; order; root = DTop }
let bottom vars = let t = top vars in { t with root = DBot }
(*
is_bot : t -> bool
*)
let is_bot x = (x.root = DBot)
(*
vars : t -> (id * item list) list
*)
let vars x = x.vars
(*
of_cons : t -> enum_cons -> t
The first t is NOT used as a decision function, here we only use
the variable ordering it provides.
*)
let of_cons v0 (op, vid, r) =
let op = match op with | E_EQ -> (=) | E_NE -> (<>) in
let root = match r with
| EItem x ->
DChoice(0, vid,
List.map (fun v -> if op v x then v, DTop else v, DBot)
(List.assoc vid v0.vars))
| EIdent vid2 ->
let a, b =
if Hashtbl.find v0.order vid < Hashtbl.find v0.order vid2
then vid, vid2
else vid2, vid
in
let nc = ref 0 in
let nb x =
incr nc;
DChoice(!nc, b,
List.map (fun v -> if op v x then v, DTop else v, DBot)
(List.assoc b v0.vars))
in
DChoice(0, a, List.map (fun x -> x, nb x) (List.assoc a v0.vars))
in
{ v0 with root = root }
(*
join : t -> t -> t
meet : t -> t -> t
*)
let join a b =
if a.root = DBot then b else
if b.root = DBot then a else
if a.root = DTop || b.root = DTop then { a with root = DTop } else begin
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 a na < rank a nb ->
let kl = List.map (fun (k, ca) -> k, f_rec ca nb) la in
dq va kl
| _, DChoice(_, vb, lb) when rank a nb < rank a na ->
let kl = List.map (fun (k, cb) -> k, f_rec na cb) lb in
dq vb kl
| _ -> assert false
in
{ a with root = memo2 f a.root b.root }
end
let meet a b =
if a.root = DTop then b else
if b.root = DTop then a else
if a.root = DBot || b.root = DBot then { a with root = DBot } else begin
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 a na < rank a nb ->
let kl = List.map (fun (k, ca) -> k, f_rec ca nb) la in
dq va kl
| _, DChoice(_, vb, lb) when rank a nb < rank a na ->
let kl = List.map (fun (k, cb) -> k, f_rec na cb) lb in
dq vb kl
| _ -> assert false
in
{a with root = memo2 f a.root b.root }
end
(*
apply_cons : t -> enum_cons -> t
apply_cl : t -> enum_cons list -> t
*)
let apply_cons v x =
meet v (of_cons v x)
let apply_cl v ec =
let rec cl_k = function
| [] -> { v with root = DTop }
| [a] -> of_cons v a
| l ->
let n = ref 0 in
let la, lb = List.partition (fun _ -> incr n; !n mod 2 = 0) l in
meet (cl_k la) (cl_k lb)
in
let cons_edd = cl_k ec in
meet v cons_edd
(*
eq : edd_v -> edd_v -> bool
*)
let eq a b =
let f f_rec na nb =
match na, nb with
| DBot, DBot -> true
| DTop, DTop -> true
| 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
(*
subset : edd_v -> edd_v -> bool
*)
let subset a b =
let rank = rank a in
let f f_rec na nb =
match na, nb with
| DBot, _ -> true
| _, DTop -> true
| DTop, DBot -> false
| 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
| DChoice(_, va, la), _ when rank na < rank nb ->
List.for_all (fun (c, n) -> f_rec n nb) la
| _, DChoice(_, vb, lb) when rank na > rank nb ->
List.for_all (fun (c, n) -> f_rec na n) lb
| _ -> assert false
in memo2 f a.root b.root
(*
forgetvars : t -> id list -> t
*)
let forgetvars v vars =
let dq = new_node_fun () in
let memo = Hashtbl.create 12 in
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 =
try
let cn = List.fold_left
(fun cn node -> match node with
| DBot -> cn
| DTop -> raise Top
| DChoice (n, v, l) -> (n, v, l)::cn)
[] l in
let cn = List.sort
(fun (n, v1, _) (n, v2, _) -> Pervasives.compare
(Hashtbl.find v.order v1) (Hashtbl.find v.order v2))
cn in
if cn = [] then
DBot
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
if List.mem dv vars then
(* Do union of all branches branching from nodes on variable dv *)
let ch2 = List.flatten
(List.map (fun (_, _, c) -> List.map snd c) d) in
f (ch1@ch2)
else
(* Keep disjunction on variable dv *)
let cc = List.map
(fun (c, _) ->
let ch2 = List.map (fun (_, _, cl) -> List.assoc c cl) d in
c, f (ch1@ch2))
cl in
dq dv cc
with | Top -> DTop
in Hashtbl.add memo kl r; r
in
{ v with root = f [v.root] }
let forgetvar v x = forgetvars v [x]
(*
project : t -> id -> item list
*)
let project v x =
try
let vals = ref [] in
let f f_rec = function
| DBot -> ()
| DChoice(_, var, l) when
Hashtbl.find v.order var < Hashtbl.find v.order x ->
List.iter (fun (_, c) -> f_rec c) l
| DChoice(_, var, l) when var = x ->
List.iter
(fun (v, l) ->
if l <> DBot && not (List.mem v !vals) then vals := v::(!vals))
l
| _ -> raise Top
in
memo f v.root; !vals
with Top -> List.assoc x v.vars
(*
assign : t -> (id * id) list -> t
*)
let assign v ids =
let v = forgetvars v (List.map fst ids) in
apply_cl v (List.map (fun (x, y) -> (E_EQ, x, EIdent y)) ids)
end
