Module `Condition_map`

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

exception Never_refined

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

module type L = sig ... end

The type of lattice elements.

module type CONDITION = sig ... end

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

module type LConditionMap = sig ... end

module type LConditionMapFold = sig ... end

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

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

module type TRANSFER_FUNCTIONS = sig ... end

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

Module Condition_map