module Defs: sig
.. end
type
t = Lang.F.Tset.t Lang.F.Vmap.t
val empty : 'a Lang.F.Vmap.t
val merge : Lang.F.Tset.t Lang.F.Vmap.t ->
Lang.F.Tset.t Lang.F.Vmap.t -> Lang.F.Tset.t Lang.F.Vmap.t
val add_def : t Pervasives.ref -> Lang.F.Vmap.key -> Lang.F.Tset.elt -> unit
val diff : Lang.F.term list -> Lang.F.var -> Lang.F.term list -> Lang.F.term list
val add_linear : t Pervasives.ref ->
Lang.F.Vmap.key -> Lang.F.term list -> Lang.F.term list -> unit
val terms : Lang.F.term -> Lang.F.term list
val atoms : Lang.F.term list -> Lang.F.var list
val defs : t Pervasives.ref -> Lang.F.term -> unit
val defs_affine : t Pervasives.ref -> Lang.F.Tset.elt -> Lang.F.Tset.elt -> unit
val defs_eq : t Pervasives.ref -> Lang.F.Tset.elt -> Lang.F.Tset.elt -> unit
: Lang.F.pred -> t
val domain : 'a Lang.F.Vmap.t -> Lang.F.Vars.t