Module type Intervals_intf.Explanations

Type signature for explanations. This is mostly intended for Alt-Ergo's built-in Explanation module, but it can be convenient to use a different module for debugging.

type t

The type of explanations.

Explanation encode predicates that may hold (be true) or not (be false) in a model.

val pp : t Fmt.t

Pretty-printer for explanations.

val is_empty : t -> bool

An explanation is empty if it is true in all models.

val empty : t

The empty explanation. Must satisfy is_empty empty = true.

val union : t -> t -> t

The union union ex ex' of two explanations ex and ex' is true in any model where both ex and ex' are true.

Note that union ex empty = union empty ex = ex.

val compare : t -> t -> int

Arbitrary comparison function on explanations. In case multiple explanations for a given fact are possible, the smaller explanation according to this comparison function is preferred.

It is recommended, but not required, that empty be the lowest explanation for compare.