sig
  module type PreDomain =
    sig
      type 'a t
      val pp : Format.formatter -> 'a Iteration.PreDomain.t -> unit
      val show : 'a Iteration.PreDomain.t -> string
      val closure : 'a Iteration.PreDomain.t -> 'a Syntax.formula
      val join :
        'a Iteration.PreDomain.t ->
        'a Iteration.PreDomain.t -> 'a Iteration.PreDomain.t
      val widen :
        'a Iteration.PreDomain.t ->
        'a Iteration.PreDomain.t -> 'a Iteration.PreDomain.t
      val equal :
        'a Iteration.PreDomain.t -> 'a Iteration.PreDomain.t -> bool
      val tr_symbols :
        'a Iteration.PreDomain.t -> (Syntax.symbol * Syntax.symbol) list
    end
  module type Domain =
    sig
      type 'a t
      val pp : Format.formatter -> 'a t -> unit
      val show : 'a t -> string
      val closure : 'a t -> 'a Syntax.formula
      val join : 'a t -> 'a t -> 'a t
      val widen : 'a t -> 'a t -> 'a t
      val equal : 'a t -> 'a t -> bool
      val tr_symbols : 'a t -> (Syntax.symbol * Syntax.symbol) list
      val abstract_iter :
        ?exists:(Syntax.symbol -> bool) ->
        'a Syntax.context ->
        'a Syntax.formula -> (Syntax.symbol * Syntax.symbol) list -> 'a t
    end
  module type DomainPlus =
    sig
      type 'a t
      val pp : Format.formatter -> 'a t -> unit
      val show : 'a t -> string
      val closure : 'a t -> 'a Syntax.formula
      val join : 'a t -> 'a t -> 'a t
      val widen : 'a t -> 'a t -> 'a t
      val equal : 'a t -> 'a t -> bool
      val tr_symbols : 'a t -> (Syntax.symbol * Syntax.symbol) list
      val abstract_iter :
        ?exists:(Syntax.symbol -> bool) ->
        'a Syntax.context ->
        'a Syntax.formula -> (Syntax.symbol * Syntax.symbol) list -> 'a t
      val closure_plus : 'a t -> 'a Syntax.formula
    end
  module WedgeVector : DomainPlus
  module WedgeVectorOCRS : DomainPlus
  module WedgeMatrix : DomainPlus
  module Split : functor (Iter : DomainPlus) -> Domain
  module Sum :
    functor (A : PreDomain) (B : PreDomain) ->
      sig
        type 'a t
        val pp : Format.formatter -> 'a t -> unit
        val show : 'a t -> string
        val closure : 'a t -> 'a Syntax.formula
        val join : 'a t -> 'a t -> 'a t
        val widen : 'a t -> 'a t -> 'a t
        val equal : 'a t -> 'a t -> bool
        val tr_symbols : 'a t -> (Syntax.symbol * Syntax.symbol) list
        val left : 'a A.t -> 'a t
        val right : 'a B.t -> 'a t
      end
end