Module V
module V: sig end
Context for handling equivalence classes of variables.
Author(s): Harald Ruess
type t
Elements of t represent conjunctions of variable equalities.
These equalities induce an equivalence relation. We say
that x and y are equivalent modulo s, if the equality
x = y follows from the equalities in s by equality reasoning.
val eq : t -> t -> bool
eq s t holds iff s and t are identical. Notice that
eq s t equals false does not imply that these contexts are not
logically equivalent.
val fold : (Term.t -> Term.t * Jst.t -> 'a -> 'a) -> t -> 'a -> 'a
fold f s e applies f x (y, rho) for each x = y with justification
rho in s and accumulates the result starting with e. The order of
application is unspecified.
val pp : t Pretty.printer
Pretty-printing
| Parameters: |
|
fmt |
: |
Format.formatter
|
|
s |
: |
t
|
|
val find : t -> Jst.Eqtrans.t
find s x returns the canonical representative of
x
of the equivalence class in
s containing
x together
with a justification of the equality
find s x = x. The canonical
representative is the smallest variable in this class according
to the variable ordering
Var.cmp. For nonvariable terms
a,
find s a returns
a
| Parameters: |
|
s |
: |
t
|
|
x |
: |
Term.Var.Map.key
|
|
val cnstrnt : t -> Term.t -> Var.Cnstrnt.t * Jst.t
For a canonical variable x, cnstrnt s x returns the
domain constraint associated with the equivalence class x.
Raises Not_found if the interpretation is unconstrained.
val removable : t -> Term.Var.Set.t
Set of removable variables. All variables in removable s
are internal, noncanonical variables.
val is_equal : t -> Term.t -> Term.t -> Jst.t option
For variables x, y[], is_equal s x y holds if and only
if x and y are in the same equivalence class modulo s.
val is_canonical : t -> Term.t -> bool
For a term variable x, is_canonical s x holds
iff find s x returns x.
val empty : t
The empty variable context.
val is_empty : t -> bool
val copy : t -> t
Protect state against destructive updates.
val merge : Fact.Equal.t -> t -> unit
Adding a variable equality
x = y by destructively
updating context
s.
In addition, every non-external variable
v which is canonical in
s but not in
merge e s, is added to
removable s e in order
to prepare it for garbage collection using
V.gc.
val gc : (Term.t -> bool) -> t -> unit
val garbage_collection_enabled : bool Pervasives.ref
Switch for enabling/disabling garbage collection of noncanonical,
internal variables.
val accumulate : t -> (Term.t -> 'a -> 'a) -> Term.t -> 'a -> 'a
Folding over the members of a specific equivalence class.
That is, if {x1,...,xn} is the set of variables with
find s xi equals the variable x', then accumulate s f x e
reduces to f x1 (f x2 ... (f xn e)...) if find s x is x'.
The order of application is unspecified.
val iter : t -> (Term.t -> unit) -> Term.t -> unit
Iterate over the extension of an equivalence class.
val exists : t -> (Term.t -> bool) -> Term.t -> bool
exists s p x holds if p y holds for some y congruent
to x modulo s.
val for_all : t -> (Term.t -> bool) -> Term.t -> bool
for_all s p x holds if p y holds for all y congruent
to x modulo s.
val choose : t -> (Term.t -> 'a option) -> Term.t -> 'a
choose s p x chooses a y which is congruent to x modulo s
which satisfies p. If there is no such y, the exception Not_found
is raised.
val diff : t -> t -> t
diff s1 s2 contains all variable equalities in s1 but not in s2.