Module Cfg.PSource

Relocatable predicate

Sourcetype t
Sourceval pretty : Format.formatter -> t -> unit
Sourceval create : S.t Node.Map.t -> Lang.F.pred -> t

Bundle an equation with the sigma sequence that created it. | create m p | = | p |

Sourceval get : t -> Lang.F.pred
Sourceval reads : t -> S.domain Node.Map.t
Sourceval nodes : t -> Node.Set.t
Sourceval relocate : S.t Node.Map.t -> t -> t

| relocate m' (create m p) | = | p{ } |

Sourceval to_condition : t -> (C.t * Node.t option) option