Module Dpll_literal.Literal

module Literal: Id.T

Literals are unique identifiers.

The compare operation on literals has the property that no literal is considered between a literal and the negation of that literal. That is, if you sort a list of literals then literals and their negations (if present) will be adjacent.

type t

An abstract type of identifiers.

val invalid : t

A distinguished invalid identifier, useful for dummy values.

val is_valid : t -> bool

Is an identifier valid?

Ensure is_valid x = (x != Id.T.invalid)

val equal : t -> t -> bool

Are two identifiers equal?

Ensure equal x y = (x = y)

val hash : t -> int

hash x is the hash code for x

Require Id.T.is_valid x

val compare : t -> t -> int

compare x y is an arbitrary order for x and y

Require Id.T.is_valid x
Require Id.T.is_valid y
Ensure (compare x y = 0) = (x = y)

Hosted by the

^* web site.
^*Other names and brands may be claimed as the property of others.