Previous  Up  Next

Module C


module C: sig  end
update x i s updates the constraint map with the constraint x in i and modifies the use lists accordingly. As a side-effect, C.changed is updated.

type t = (Sign.t * Fact.justification option) Term.Map.t 
val empty : 'a Term.Map.t
val eq : 'a -> 'a -> bool
Parameters:
s : 'a
t : 'a
 
val cnstrnts : 'a -> 'a
Parameters:
s : 'a
 
val to_list : ('a * 'b) Term.Map.t -> (Term.Map.key * 'a) list
Parameters:
s : ('a * 'b) Term.Map.t
 
val pp : Format.formatter -> (Sign.t * 'a) Term.Map.t -> unit
Parameters:
fmt : Format.formatter
s : (Sign.t * 'a) Term.Map.t
 
val apply : 'a Term.Map.t -> Term.Map.key -> 'a
Parameters:
s : 'a Term.Map.t
a : Term.Map.key
 
val cnstrnt : (Sign.t * Fact.justification option) Term.Map.t ->
       Term.Map.key -> Fact.cnstrnt
Parameters:
s : (Sign.t * Fact.justification option) Term.Map.t
x : Term.Map.key
 
val mem : Term.Map.key -> 'a Term.Map.t -> bool
Parameters:
a : Term.Map.key
s : 'a Term.Map.t

update x i s updates the constraint map with the constraint x in i and modifies the use lists accordingly. As a side-effect, C.changed is updated.

val changed : Term.Set.t Pervasives.ref
val update : Fact.cnstrnt ->
       (Sign.t * Fact.justification option) Term.Map.t ->
       (Sign.t * Fact.justification option) Term.Map.t
Parameters:
c : Fact.cnstrnt
s : (Sign.t * Fact.justification option) Term.Map.t
 
val restrict : Term.Map.key -> ('a * 'b) Term.Map.t -> ('a * 'b) Term.Map.t
Restrict the map.
Parameters:
a : Term.Map.key
s : ('a * 'b) Term.Map.t

Asserting an inequality

val add : Fact.cnstrnt ->
       (Sign.t * Fact.justification option) Term.Map.t ->
       Term.Set.t * (Sign.t * Fact.justification option) Term.Map.t
Parameters:
c : Fact.cnstrnt
s : (Sign.t * Fact.justification option) Term.Map.t
 
val merge : Fact.equal ->
       (Sign.t * Fact.justification option) Term.Map.t ->
       Term.Set.t * (Sign.t * Fact.justification option) Term.Map.t
Propagating a variable equality.
Parameters:
e : Fact.equal
s : (Sign.t * Fact.justification option) Term.Map.t
 
val merge1 : Fact.equal ->
       (Sign.t * Fact.justification option) Term.Map.t ->
       (Sign.t * Fact.justification option) Term.Map.t
Parameters:
e : Fact.equal
s : (Sign.t * Fact.justification option) Term.Map.t

Propagate disequalities to the constraint part. The following is not complete and should be extended to all finite constraints, but the disequality sets might become rather large then.

val diseq : Fact.diseq ->
       (Sign.t * 'a) Term.Map.t -> Term.Set.t * (Sign.t * 'a) Term.Map.t
Parameters:
d : Fact.diseq
s : (Sign.t * 'a) Term.Map.t
 
val diseq1 : Fact.diseq -> (Sign.t * 'a) Term.Map.t -> (Sign.t * 'a) Term.Map.t
Parameters:
d : Fact.diseq
s : (Sign.t * 'a) Term.Map.t