// --- Reaching Def --------------------------------------------------------------------------------
// var x defined at label def_l can reach label reach_l on a defined trace t
// NOTE: not a reflexively defined relation, i.e. reaching_def(l1, l2, x, t) is not a valid predicate for l1 == l2
//       EXCEPTION: ReachingDef is reflexive for assign_() as explained there in detail.

.decl reaching_def(def_l:label, reach_l:label, x:var, t:trace)
//.output reaching_def
// base cases
reaching_def(def_l, reach_l, x, t) :- def_(def_l, x), mapped_follows(reach_l, def_l), traces(t), contains(cat("_", def_l), t), contains(cat("_", reach_l), t).
reaching_def(def_l, def_l, x, t) :- assign_(def_l, x), traces(t), contains(cat("_", def_l), t).
reaching_def(def_l, reach_l, x, t) :- assign_(def_l, x), mapped_follows(reach_l, def_l), traces(t), contains(cat("_", def_l), t), contains(cat("_", reach_l), t).
// induction
reaching_def(def_l, reach_l, x, t) :- reaching_def(def_l, l2, x, t), mapped_follows(reach_l, l2), !source(reach_l, x), !assign(l2, x, _, _), !assign_(l2, x), contains(cat("_", reach_l), t).