package codex

  1. Overview
  2. Docs
package codex
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Module Condition.ConditionDomSource

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).

Sourcemodule Literal : sig ... end
Sourcemodule Path : sig ... end
Sourcetype t =
  1. | False
  2. | Literal of Literal.t
  3. | Path of Path.t
  4. | Complement of t
Sourceval hash : t -> int
Sourceval pretty : Format.formatter -> t -> unit
Sourceval equal : t -> t -> bool
Sourceval _equal : t -> t -> bool
Sourceval var : unit -> t
Sourceval empty : t
Sourceval all : t
Sourceval one : t
Sourceval complement : t -> t
Sourceval (!~) : t -> t
Sourceval is_included : t -> t -> bool
Sourceval union : t -> t -> t
Sourceval (||~) : t -> t -> t
Sourceval nearest_common_ancestor : t -> t -> t
Sourceval is_prefix : t -> t -> bool
Sourceval inter : t -> t -> t
Sourceval (&&~) : t -> t -> t
Sourceval is_empty : t -> bool
Sourceval disjoint : t -> t -> bool
Sourcemodule Log : sig ... end