Disequalities (goblint.Goblint_lib.CongruenceClosure.Disequalities)

type t = TSet.t ZMap.t TMap.t

val equal : t -> t -> Ppx_deriving_runtime.bool

val compare : t -> t -> Ppx_deriving_runtime.int

val hash : t -> int

type arg_t = (T.t * Z.t) ZMap.t TMap.t

val empty : 'a TMap.t

val is_empty : 'a TMap.t -> bool

val remove : TMap.key -> 'a TMap.t -> 'a TMap.t

Returns a list of tuples, which each represent a disequality

val bindings : TSet.t ZMap.t TMap.t -> (TMap.key * ZMap.key * TSet.elt) list

Returns a list of tuples, which each represent a disequality

val map_set_add : 
  (TMap.key * ZMap.key) ->
  TSet.elt ->
  t ->
  TSet.t ZMap.t TMap.t

adds a mapping v -> r -> size -> v' to the map, or if there are already elements in v -> r -> .. then v' is added to the previous set

val map_set_mem : (TMap.key * ZMap.key) -> TSet.elt -> t -> bool

val comp_map : 
  ((Goblint_lib__UnionFind.term * ZMap.key) * int) TUF.ValMap.t ->
  t * ((Goblint_lib__UnionFind.term * ZMap.key) * int) TUF.ValMap.t

Map of partition, transform union find to a map of type V -> Z -> V set with reference variable |-> offset |-> all terms that are in the union find with this ref var and offset.

val comp_t : 
  ((Goblint_lib__UnionFind.term * Z.t) * int) TUF.ValMap.t ->
  TUF.ValMap.key ->
  (TUF.ValMap.key * Z.t) list

Find all elements that are in the same equivalence class as t.

val get_args : 
  ((Goblint_lib__UnionFind.term * ZMap.key) * int) TUF.ValMap.t ->
  ((Goblint_lib__UnionFind.term * ZMap.key) * int) TUF.ValMap.t
  * t
  * (Goblint_lib__UnionFind.term * Z.t) list ZMap.t TMap.t

Returns: "arg" map:

maps each representative term t to a map that maps an integer Z to a list of representatives t' of v where *(v + z') is in the representative class of t.

It basically maps each state in the automata to its predecessors.

val fold_left2 : ('a -> 'b -> 'c -> 'd) -> 'e -> 'f list -> 'g list -> 'h

val map2 : ('a -> 'b -> 'c) -> 'd list -> 'b list -> 'e list

val map_find_opt : (TMap.key * ZMap.key) -> 'a ZMap.t TMap.t -> 'a option

val map_find_all : TMap.key -> 'a list ZMap.t TMap.t -> 'a list

val add_diseq : 
  (T.t * T.t * Z.t) list ->
  (T.t * Z.t) ->
  (T.t * Z.t) ->
  (T.t * T.t * Z.t) list

val check_neq : 
  ('a * (T.t * Z.t) list ZMap.t TMap.t) ->
  (T.t * T.t * Z.t) list ->
  (TMap.key * 'b ZMap.t) ->
  (T.t * T.t * Z.t) list

Find all disequalities of the form t1 != z2-z1 + t2 that can be inferred from equalities of the form *(z1 + t1) = *(z2 + t2).

val check_neq_bl : 
  ('a * (T.t * Z.t) list ZMap.t TMap.t) ->
  (T.t * T.t * Z.t) list ->
  (TMap.key * TSet.t) ->
  (T.t * T.t * Z.t) list

Find all disequalities of the form t1 != z2-z1 + t2 that can be inferred from block equalities of the form bl( *(z1 + t1) ) = bl( *(z2 + t2) ).

val init_neq : 
  ('a * 'b ZMap.t TMap.t * (T.t * Z.t) list ZMap.t TMap.t) ->
  (T.t * T.t * Z.t) list

Initialize the list of disequalities taking only implicit dis-equalities into account.

Returns: List of dis-equalities implied by the equalities.

val init_neg_block_diseq : 
  ('a * TSet.t TMap.t * 'b * (T.t * Z.t) list ZMap.t TMap.t) ->
  (T.t * T.t * Z.t) list

Initialize the list of disequalities taking only implicit dis-equalities into account.

Returns: List of dis-equalities implied by the block disequalities.

val init_list_neq : 
  ((Goblint_lib__UnionFind.term * Z.t) * int) TUF.ValMap.t ->
  (TUF.ValMap.key * TUF.ValMap.key * Z.t) list ->
  ((Goblint_lib__UnionFind.term * Z.t) * int) TUF.ValMap.t
  * (Goblint_lib__UnionFind.term * Goblint_lib__UnionFind.term * Z.t) list

Initialize the list of disequalities taking explicit dis-equalities into account.

Parameters: union-find partition, explicit disequalities.

Returns: list of normalized provided dis-equalities

val propagate_neq : 
  ('a * TSet.t ZMap.t TMap.t * (T.t * Z.t) list ZMap.t TMap.t * t) ->
  BlDis.t ->
  (T.t * T.t * ZMap.key) list ->
  t

Parameter: list of disequalities (t1, t2, z), where t1 and t2 are roots.

Returns: map `neq` where each representative is mapped to a set of representatives it is not equal to.

val show_number : Z.t -> string

Produces a string for the number used as offset; helper function for show* functions below.

val show_neq : TSet.t ZMap.t TMap.t -> string

val get_disequalities : TSet.t ZMap.t TMap.t -> prop list

val element_closure : 
  (Goblint_lib__UnionFind.term * Goblint_lib__UnionFind.term * Z.t) list ->
  BatSet.Make(Goblint_lib__UnionFind.T).t BatMap.Make(Z).t
    BatMap.Make(Goblint_lib__UnionFind.T).t ->
  'a ->
  (Goblint_lib__UnionFind.term * Goblint_lib__UnionFind.term * Z.t) list

For each disequality t1 != z + t2 we add all disequalities that follow from equalities. I.e., if t1 = z1 + t1' and t2 = z2 + t2', then we add the disequaity t1' != z + z2 - z1 + t2'.