module Partition: sig end
Equalities and disequalities over variables and constraints on variables
Equalities and disequalities over variables and constraints on variables
type t = {
|
mutable v : V.t; |
|
mutable d : D.t; |
|
mutable c : C.t; |
}
val empty : t
Empty partition.
val pp : Format.formatter -> t -> unit
Pretty-printing
| Parameters: |
|
fmt |
: |
Format.formatter
|
|
s |
: |
t
|
|
val eq : t -> t -> bool
Test if states are unchanged.
type changed = {
|
chv : Term.Set.t; |
|
chd : Term.Set.t; |
|
chc : Term.Set.t; |
}
val nochange : changed
val is_unchanged : changed -> bool
val v_of : t -> V.t
val d_of : t -> D.t
val c_of : t -> C.t
val v : t -> Term.t -> Term.t * Fact.justification option
Canonical variables module s.
val d : t -> Term.t -> (Term.t * Fact.justification option) list
All disequalities of some variable x.
val c : t -> Term.t -> Sign.t * Fact.justification option
Constraint of a variable.
val is_equal : t -> Term.t -> Term.t -> Three.t
val update_v : t -> V.t -> t
val update_d : t -> D.t -> t
val update_c : t -> C.t -> t
val copy : t -> t
Shallow copy for protecting against destructive updates.
val merge : Fact.equal -> t -> changed * t
Merge a variable equality.
val add : Fact.cnstrnt -> t -> changed * t
Adding a constraint
val diseq : Fact.diseq -> t -> changed * t
Add and propagate disequalities of the form x <> y.
val gc : (Term.t -> bool) -> t -> t
Garbage collection.