Module Condition.ConditionDom

This uses the structure of the dominator tree as conditions. It observes the fact that we never perform intersection on arbitrary conditions, as conditions represent set of paths, we either assume a new condition or join existing ones.

This works together with skiplist.ml (fast implementation of useful algorithms like online nearest_common_ancestor) and treemap.ml (mapping from tree relations to lattices).

It is a good candidate for introducing scopes and getting rid of Cudd. Still, when I tested these conditions with Domain_non_relational, it worked for most benchmarks, but the performance gains were not fantastic compared to cudd (sometimes less time, some times more; sometimes a lot less memory, but sometimes more).

module Literal : sig ... end

module Path : sig ... end

type t =

1. | False
2. | Literal of Literal.t
3. | Path of Path.t
4. | Complement of t

val hash : t -> int

val pretty : Stdlib.Format.formatter -> t -> unit

val equal : t -> t -> bool

val _equal : t -> t -> bool

val var : unit -> t

val empty : t

val all : t

val one : t

val complement : t -> t

val (!~) : t -> t

val is_included : t -> t -> bool

val union : t -> t -> t

val (||~) : t -> t -> t

val nearest_common_ancestor : t -> t -> t

val is_prefix : t -> t -> bool

val inter : t -> t -> t

val (&&~) : t -> t -> t

val is_empty : t -> bool

val disjoint : t -> t -> bool

module Log : sig ... end