module FO:S
with type term = FOTerm.t
type
term
type
t
val create : ?size:int -> unit -> t
size
: a hint for the initial size of the hashtable.val clear : t -> unit
val push : t -> unit
Congruence.S.pop
will restore the congruence to its current state.val pop : t -> unit
Invalid_argument
if there is no checkpoint to restore to
(ie if no call to Congruence.S.push
matches this call to Congruence.S.pop
)val stack_size : t -> int
Congruence.S.push
that lead to the current state of the
congruence. Also, how many times Congruence.S.pop
can be called.val find : t -> term -> term
val iter : t ->
(mem:term -> repr:term -> unit) -> unit
mem
, the term itself, and repr
,
the current representative of the term mem
.
Invariant: when calling iter cc f
, if f ~mem ~repr
is called,
then find cc mem == repr
holds.
val iter_roots : t -> (term -> unit) -> unit
val mk_eq : t -> term -> term -> unit
mk_eq congruence t1 t2
asserts that t1 = t2
belongs to
the congruenceval mk_less : t -> term -> term -> unit
mk_less congruence t1 t2
asserts that t1 < t2
belongs to
the congruenceval is_eq : t -> term -> term -> bool
val is_less : t -> term -> term -> bool
val cycles : t -> bool
mk_eq
and mk_less
entail a cycle in
the ordering (hence contradicting irreflexivity/transitivity of less)