Module D

module D: sig  end

Known disequalities; x |-> {y,z} is interpreted as x <> y & x <> z. The function is closed in that forall x, y such that x |-> {...,y,...} then also y |-> {....,x,....}

Known disequalities; x |-> {y,z} is interpreted as x <> y & x <> z. The function is closed in that forall x, y such that x |-> {...,y,...} then also y |-> {....,x,....}

type t = Term.Set.t Term.Map.t

val empty : 'a Term.Map.t

val eq : 'a -> 'a -> bool

Parameters:

s	:	`'a`
t	:	`'a`

val deq_of : 'a -> 'a

Parameters:

s : 'a

val to_list : Term.Set.t Term.Map.t -> (Term.Map.key * Term.Set.elt) list

Parameters:

s : Term.Set.t Term.Map.t

val pp : Format.formatter -> Term.Set.t Term.Map.t -> unit

Parameters:

fmt	:	`Format.formatter`
s	:	`Term.Set.t Term.Map.t`

All terms known to be disequal to a.

val deq : Term.Set.t Term.Map.t -> Term.Map.key -> Term.Set.t

Parameters:

s	:	`Term.Set.t Term.Map.t`
a	:	`Term.Map.key`

Check if two terms are known to be disequal.

val is_diseq : Term.Set.t Term.Map.t -> Term.Map.key -> Term.Set.elt -> bool

Parameters:

s	:	`Term.Set.t Term.Map.t`
a	:	`Term.Map.key`
b	:	`Term.Set.elt`

Adding a disequality over variables

val add : Fact.diseq -> Term.Set.t Term.Map.t -> Term.Set.t * Term.Set.t Term.Map.t

Parameters:

d	:	`Fact.diseq`
s	:	`Term.Set.t Term.Map.t`

Propagating an equality between variables.

val merge : Fact.equal -> Term.Set.t Term.Map.t -> Term.Set.t * Term.Set.t Term.Map.t

Parameters:

e	:	`Fact.equal`
s	:	`Term.Set.t Term.Map.t`

Return disequalities for x.

val d : Term.Set.t Term.Map.t -> Term.Map.key -> (Term.Set.elt * 'a option) list

Parameters:

s	:	`Term.Set.t Term.Map.t`
x	:	`Term.Map.key`