Previous  Up  Next

Module Solution


module Solution: sig  end
Fold over the find structure.

type t = {
   find : (Term.t * Fact.justification option) Term.Map.t;
   inv : Term.t Term.Map.t;
   use : Use.t;
} 
val empty : t
val is_empty : t -> bool
Parameters:
s : t
 
val eq : t -> t -> bool
Parameters:
s : t
t : t

Fold over the find structure.

val fold : (Term.Map.key -> Term.t * Fact.justification option -> 'a -> 'a) ->
       t -> 'a -> 'a
Parameters:
f : Term.Map.key -> Term.t * Fact.justification option -> 'a -> 'a
s : t

Solution set

val to_list : t -> (Term.Map.key * Term.t) list
Parameters:
s : t

Pretty-printer.

val pp : Th.t -> Format.formatter -> t -> unit
Parameters:
i : Th.t
fmt : Format.formatter
s : t
 
val apply : t -> Term.Map.key -> Term.t
Parameters:
s : t
x : Term.Map.key
 
val find : t -> Term.Map.key -> Term.Map.key
Parameters:
s : t
x : Term.Map.key
 
val justification : t -> Term.Map.key -> Term.t * Fact.justification option
Parameters:
s : t
x : Term.Map.key
 
val equality : t -> Term.Map.key -> Fact.equal
Parameters:
s : t
x : Term.Map.key
 
val inv : t -> Term.Map.key -> Term.t
Parameters:
s : t
a : Term.Map.key
 
val mem : t -> Term.Map.key -> bool
Parameters:
s : t
x : Term.Map.key
 
val use : t -> Term.t -> Term.Set.t
Parameters:
s : t

Does a variable occur in s.

val occurs : t -> Term.Map.key -> bool
Parameters:
s : t
x : Term.Map.key

union x b s adds new equality x = b to s, possibly overwriting an equality x = ...

val union : Th.t -> Fact.equal -> t -> t
Parameters:
i : Th.t
e : Fact.equal
s : t

Extend with binding x = b, where x is fresh

val extend : Th.t -> Fact.equal -> t -> t
Parameters:
i : Th.t
e : Fact.equal
s : t

Restrict domain.

val restrict : Th.t -> Term.Map.key -> t -> t
Parameters:
i : Th.t
x : Term.Map.key
s : t

name e a returns a variable x if there is a solution x = a. Otherwise, it creates a new name x' and installs a solution x' = a in e.

val name : Th.t -> Term.Map.key * t -> Term.t * t
val replace : (Term.Map.key -> Term.Map.key) -> t -> Term.Map.key -> Term.Map.key
Parameters:
v : Term.Map.key -> Term.Map.key
s : t
 
val nrm : Th.t -> Fact.equal list -> Term.t -> Term.t * Fact.justification option list
Parameters:
i : Th.t
r : Fact.equal list
a : Term.t
 
val norm : Th.t -> Fact.equal list -> Term.t -> Term.t * Fact.justification option list
Parameters:
i : Th.t
r : Fact.equal list
a : Term.t
 
val assoc : Term.t -> Fact.equal list -> Term.t
Parameters:
x : Term.t
?? : Fact.equal list
 
val eqs : Fact.justification option list Pervasives.ref

Fuse.

val fuse : Th.t ->
       t -> Fact.equal list -> Term.Set.t * Fact.Equalset.t * t
Parameters:
i : Th.t
s : t
r : Fact.equal list
 
val update : Term.Set.t Pervasives.ref * Fact.Equalset.t Pervasives.ref ->
       Th.t -> Fact.Equalset.elt -> t -> t
Parameters:
(changed,eqs) : Term.Set.t Pervasives.ref * Fact.Equalset.t Pervasives.ref
i : Th.t
e : Fact.Equalset.elt
s : t

Composition.

val compose : Th.t ->
       t ->
       Fact.Equalset.elt list -> Term.Set.t * Fact.Equalset.t * t
Parameters:
i : Th.t
s : t
r : Fact.Equalset.elt list