Module Biabduction.Propgraph

Propositions seen as graphs

type 'a t

prop considered as a graph

val from_prop : 'a Prop.t -> 'a t

create a graph from a prop

type 'a diff

Graph annotated with the differences w.r.t. a previous graph

val compute_diff : IStdlib.Pp.color -> 'a t -> 'a t -> 'a diff

compute_diff default_color oldgraph newgraph returns the list of edges which are only in newgraph

val diff_get_colormap : bool -> 'a diff -> IStdlib.Pp.colormap

diff_get_colormap footprint_part diff returns the colormap of a computed diff, selecting the footprint colormap if footprint_part is true.

val pp_proplist : IStdlib.Pp.env -> string -> ('a Prop.t * bool) -> Stdlib.Format.formatter -> 'b Prop.t list -> unit

Print a list of propositions, prepending each one with the given string, If !Config.pring_using_diff is true, print the diff w.r.t. the given prop, extracting its local stack vars if the boolean is true.

val d_proplist : 'a Prop.t -> 'b Prop.t list -> unit

dump a prop list coming form the given initial prop