open Misc;; type econd = | Ein of string * Iset.t | Eand of econd list | Eor of econd list | Etrue | Efalse ;; let rec possible_values v econd = match econd with | Ein (w, l) when w = v -> l | Ein (_, l) -> Iset.Neg [] | Eand l -> List.fold_left Iset.conj (Iset.Neg []) (list_rmap (possible_values v) l) | Eor l -> List.fold_left Iset.disj (Iset.Pos []) (list_rmap (possible_values v) l) | Etrue -> Iset.Neg [] | Efalse -> Iset.Pos [] ;; exception Nocollapse;; let rec implies x y = match x, y with | Ein (v1, s1), Ein (v2, s2) when v1 = v2 -> Iset.included s1 s2 | _, Eor l -> List.exists (fun z -> implies x z) l | Eand l, _ -> List.exists (fun z -> implies z y) l | _, Eand l -> List.for_all (fun z -> implies x z) l | Eor l, _ -> List.for_all (fun z -> implies z y) l | Efalse, _ -> true | _, Etrue -> true | _, _ -> false ;; let implied x y = implies y x;; let equiv x y = implies x y && implies y x;; let factor l1 l2 = let (l1a, l1b) = List.partition (fun x -> List.exists (equiv x) l2) l1 in if List.length l1b <> 1 then raise Nocollapse; let (l2a, l2b) = List.partition (fun x -> List.exists (equiv x) l1) l2 in if List.length l2b <> 1 then raise Nocollapse; (List.hd l1b, List.hd l2b, l2a) ;; let minimize_ein v = function | Iset.Pos [] -> Efalse | Iset.Neg [] -> Etrue | Iset.Pos s -> Ein (v, Iset.Pos (list_sortu s)) | Iset.Neg s -> Ein (v, Iset.Neg (list_sortu s)) ;; let rec collapse_and ec1 ec2 = if implies ec1 ec2 then ec1 else if implies ec2 ec1 then ec2 else match ec1, ec2 with | Ein (v1, s1), Ein (v2, s2) when v1 = v2 -> minimize_ein v1 (Iset.conj s1 s2) | Eor l1, Eor l2 -> let (x1, x2, l) = factor l1 l2 in (* may raise Nocollapse *) let minand = minimize_and [x1;x2] in minimize_or (minand :: l) | Etrue, _ -> ec2 | _, Etrue -> ec1 | _, _ -> raise Nocollapse and collapse_or ec1 ec2 = if implies ec1 ec2 then ec2 else if implies ec2 ec1 then ec1 else match ec1, ec2 with | Ein (v1, s1), Ein (v2, s2) when v1 = v2 -> minimize_ein v1 (Iset.disj s1 s2) | Eand l1, Eand l2 -> let (x1, x2, l) = factor l1 l2 in (* may raise Nocollapse *) let minor = minimize_or [x1;x2] in minimize_and (minor::l) | Etrue, _ -> Etrue | _, Etrue -> Etrue | _, _ -> raise Nocollapse and incorporate_and ec = function | [] -> [ec] | ec1::ecs -> try match (collapse_and ec ec1) with | Efalse -> [Efalse] | Etrue -> ecs | ec2 -> ec2 :: ecs with Nocollapse -> ec1 :: (incorporate_and ec ecs) and incorporate_or ec = function | [] -> [ec] | ec1::ecs -> try match (collapse_or ec ec1) with | Etrue -> [Etrue] | Efalse -> ecs | ec2 -> ec2 :: ecs with Nocollapse -> ec1 :: (incorporate_or ec ecs) and minimize_and_aux accu = function | [] -> accu | Etrue::ecs -> minimize_and_aux accu ecs | Efalse::_ -> [Efalse] | ec::ecs -> minimize_and_aux (incorporate_and ec accu) ecs and minimize_or_aux accu = function | [] -> accu | Efalse::ecs -> minimize_or_aux accu ecs | Etrue::_ -> [Etrue] | ec::ecs -> minimize_or_aux (incorporate_or ec accu) ecs and unnest_and accu = function | [] -> accu | Eand l :: ecs -> unnest_and accu (l @@ ecs) | ec :: ecs -> unnest_and (ec :: accu) ecs and unnest_or accu = function | [] -> accu | Eor l :: ecs -> unnest_or accu (l @@ ecs) | ec :: ecs -> unnest_or (ec :: accu) ecs and minimize_econd ec = match ec with | Etrue | Efalse -> ec | Ein (v, l) -> minimize_ein v l | Eand l -> minimize_and (list_rmap minimize_econd l) | Eor l -> minimize_or (list_rmap minimize_econd l) and minimize_and l = let l = unnest_and [] l in match minimize_and_aux [] l with | [] -> Etrue | [ec] -> ec | l -> Eand l and minimize_or l = let l = unnest_or [] l in match minimize_or_aux [] l with | [] -> Efalse | [ec] -> ec | l -> Eor l ;; let rec evaluate_aux cond v s = match cond with | Ein (w, Iset.Neg []) -> Etrue | Ein (w, Iset.Pos []) -> Efalse | Ein (w, l) when w = v -> if Iset.included s l then Etrue else begin match Iset.conj l s with | Iset.Pos [] -> Efalse | Iset.Neg [] -> Etrue | s -> Ein (w, s) end | Ein (_, _) -> cond | Eand cs -> let l = list_rmap (fun x -> evaluate_aux x v s) cs in if List.mem Efalse l then Efalse else if l = [] then Etrue else Eand l | Eor cs -> let l = list_rmap (fun x -> evaluate_aux x v s) cs in if List.mem Etrue l then Etrue else if l = [] then Efalse else Eor l | Etrue -> Etrue | Efalse -> Efalse ;; let evaluate cond v s = minimize_econd (evaluate_aux cond v s);; let rec pos_cond = function | Ein (v, Iset.Pos l) -> true | Ein (v, Iset.Neg l) -> false | Eand l -> List.for_all pos_cond l | Eor l -> List.for_all pos_cond l | Efalse -> true | Etrue -> true ;;