Module InvGenDomain

exception TrivialRelation

Exception thrown when a domain is asked to build a trivial implication.

module type Domain = sig ... end

Signature of the modules describing an order relation over some values.

module Bool : Domain

Boolean domain with implication.

module Int : Domain

Integer domain with less than or equal to.

module BV (L : sig ... end) : Domain

BV domain with less than or equal to.

module UBV (L : sig ... end) : Domain

UBV domain with less than or equal to.

module Real : Domain

Real domain with less than or equal to.