package alt-ergo-lib

The type of explanations.

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

Pretty-printer for explanations.

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

The empty explanation. Must satisfy is_empty empty = true.

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.

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.