Module Terms.Condition

Possible implementations of conditions for the terms.

module Bed : sig ... end

module ConditionMy : sig ... end

module ConditionDom : sig ... end

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.

module ConditionInt : sig ... end

A dummy Condition, which creates a new int each time.

module ConditionCudd : sig ... end

Condition using Cudd binary-decision diagrams.

module MakeConditionCudd (T : sig ... end) : Condition_map.CONDITION

module MakeConditionMapMTBDD (Lattice : sig ... end) : sig ... end

module type SCONDITIONMAP_MTBDD = sig ... end

module ConditionMapMTBDD : sig ... end

module MakeConditionMapPartitionPI (Condition : Condition_map.CONDITION) : sig ... end

module MakeConditionMapTreePI (Condition : Condition_map.CONDITION) : sig ... end

module CuddMTBDD : sig ... end

module type SCONDITIONMAP_CUDD_MTBDD = sig ... end

module MakeConditionMapCuddMTBDD (L : Condition_map.L) : sig ... end

module CuddTree : sig ... end

module type SCONDITIONMAP_CUDD_TREE = sig ... end

module MakeConditionMapCuddTree (L : Condition_map.L) : sig ... end

module CuddPIPartition : sig ... end

module DomPIPartition : sig ... end

module CuddPITree : sig ... end

module CuddPIMTBDD : sig ... end

module HomeMadeBDDPartitionPI : sig ... end

module HomeMadeMTBDD : sig ... end