let roots(r) = domain(r) \ range(r)
let succs (e,r) = range ([e];r)
let mapset2rel f =
let rec map_rec xs = match xs with
|| {} -> 0
|| x ++ xs ->
f x | map_rec xs
end in
map_rec
let mapset2set f =
let rec map_rec xs = match xs with
|| {} -> {}
|| x ++ xs ->
f x | map_rec xs
end in
map_rec
let poDorW = [PoD|W];po;[PoD|W]
let nextDorW = poDorW \ (poDorW;poDorW)
let sibling =
let inv = nextDorW^-1 in
fun s -> ([s];inv;nextDorW;[s])\(id|inv|nextDorW)
let DpoDorW = [PoD];poDorW
let addD d =
let rec do_rec ws = match ws with
|| {} -> fun k -> k
|| w ++ ws ->
let kws = do_rec ws in
fun k -> (d,w) ++ kws k
end in do_rec
let addifequiv (equiv,ws0) = mapset2set (fun w -> succs (w,equiv) & ws0)
let combine (equiv,ws1,ws2) =
addifequiv (equiv,ws1) ws2 | addifequiv (equiv,ws2) ws1
let rec case_disjunction (equiv,e) = match { e } & PoD with
|| {} ->
let (ws,dw) = write_acc (equiv, (succs (e,nextDorW))) in
(e ++ ws,dw)
|| d ++ es ->
let nexts = (succs (d,nextDorW)) in
match sibling(nexts) with
|| {} ->
({},0)
|| _e ++ _es ->
let (ws,dw) = keep_equiv_writes (equiv,nexts) in
(ws,addD d ws dw)
end
end
and write_acc (equiv,es) = match es with
|| {} -> ({},0)
|| e ++ es ->
let (ws_e,dw_e) = case_disjunction (equiv, e)
and (ws_es,dw_es) = write_acc (equiv, es) in
(ws_e|ws_es, dw_e|dw_es)
end
and keep_equiv_writes (equiv,es) = match es with
|| {} -> ({},0)
|| e ++ es ->
match es with
|| {} -> case_disjunction(equiv,e)
|| f ++ fs ->
let (ws_e,dw_e) = case_disjunction(equiv,e)
and (ws_es,dw_es) = keep_equiv_writes(equiv,es) in
(combine (equiv,ws_e,ws_es), dw_e|dw_es)
end
end
let zyva equiv =
mapset2rel
(fun r -> let (ws,dw) = case_disjunction(equiv,r) in dw)
let intrinsic = (iico_data | iico_ctrl)+
let udr r = domain r | range r
let generated-by-stxr = udr(same-instr;[range(lxsx)])
let rf-reg-restrict =
let NW = ~generated-by-stxr in
[NW];rf-reg
let dd = (rf-reg | intrinsic)+
let dd-restrict = (rf-reg-restrict | intrinsic)+
let to-PoD = [R]; dd-restrict; [PoD]
let pre-ctrl = to-PoD; po; [W]
let Dmins = roots(DpoDorW)
let Dm=Dmins*Dmins
let always-exec equiv =
let DW = zyva equiv Dmins in
to-PoD; DW
let ctrlequiv equiv = pre-ctrl \ (always-exec equiv)