Module Condition_mapSource

A map from conditions to lattice elements, which is incrementally refined according to the result of some operations.

Sourceexception Never_refined

Raised when using a condition map with a condition for which the value was never refined.

Sourcemodule type L = sig ... end

The type of lattice elements.

Sourcemodule type CONDITION = sig ... end

The type of conditions. This can be viewed as formulas, or as sets of valuations satisfying the formula.

Sourcemodule type LConditionMap = sig ... end
Sourcemodule type LConditionMapFold = sig ... end
Sourcemodule ConditionMapTree (Cond : CONDITION) : sig ... end

One implementation of LConditionMap, where partitions are hierarchically split in two, based on the order in which they were inserted.

Sourcemodule ConditionMapPartition (Cond : CONDITION) : sig ... end

Another implementation of LConditionMap: maintains a flat partition of the possible different values, with the BDD that lead to it.

Sourcemodule type TRANSFER_FUNCTIONS = sig ... end
Sourcemodule MakePathInsensitive (Cond : CONDITION) (M : sig ... end) : TRANSFER_FUNCTIONS with module Cond = Cond and type 'a t = 'a M.t