sig
  module Config :
    sig
      type 'a t = G.t * 'a * Partition.t
      val empty : 'a -> 'a Infsys.Config.t
      val is_empty : ('a -> bool) -> 'a Infsys.Config.t -> bool
      val pp : 'a Pretty.printer -> 'a Infsys.Config.t Pretty.printer
    end
  val g : G.t Pervasives.ref
  val p : Partition.t Pervasives.ref
  module type EQ =
    sig
      type e
      val current : unit -> Infsys.EQ.e
      val initialize : Infsys.EQ.e -> unit
      val finalize : unit -> Infsys.EQ.e
      val abstract : Term.t -> unit
      val merge : Fact.Equal.t -> unit
      val propagate : Fact.Equal.t -> unit
      val dismerge : Fact.Diseq.t -> unit
      val propagate_diseq : Fact.Diseq.t -> unit
      val branch : unit -> unit
      val normalize : unit -> unit
    end
  module type ARITH =
    sig
      type e
      val current : unit -> Infsys.ARITH.e
      val initialize : Infsys.ARITH.e -> unit
      val finalize : unit -> Infsys.ARITH.e
      val abstract : Term.t -> unit
      val merge : Fact.Equal.t -> unit
      val propagate : Fact.Equal.t -> unit
      val dismerge : Fact.Diseq.t -> unit
      val propagate_diseq : Fact.Diseq.t -> unit
      val branch : unit -> unit
      val normalize : unit -> unit
      val nonneg : Fact.Nonneg.t -> unit
      val pos : Fact.Pos.t -> unit
    end
  module Empty : EQ
  val difference : bool Pervasives.ref
  module type LEVEL =
    sig
      type t
      val level : Trace.level
      val eq : Infsys.LEVEL.t -> Infsys.LEVEL.t -> bool
      val diff : Infsys.LEVEL.t -> Infsys.LEVEL.t -> Infsys.LEVEL.t
      val pp : Infsys.LEVEL.t Pretty.printer
    end
  module Trace :
    functor (I : EQ) ->
      functor
        (L : sig
               type t = I.e
               val level : Trace.level
               val eq : Infsys.LEVEL.t -> Infsys.LEVEL.t -> bool
               val diff : Infsys.LEVEL.t -> Infsys.LEVEL.t -> Infsys.LEVEL.t
               val pp : Infsys.LEVEL.t Pretty.printer
             end) ->
        sig
          type e = I.e
          val current : unit -> Infsys.EQ.e
          val initialize : Infsys.EQ.e -> unit
          val finalize : unit -> Infsys.EQ.e
          val abstract : Term.t -> unit
          val merge : Fact.Equal.t -> unit
          val propagate : Fact.Equal.t -> unit
          val dismerge : Fact.Diseq.t -> unit
          val propagate_diseq : Fact.Diseq.t -> unit
          val branch : unit -> unit
          val normalize : unit -> unit
        end
  module TraceArith :
    functor (I : ARITH) ->
      functor
        (L : sig
               type t = I.e
               val level : Trace.level
               val eq : Infsys.LEVEL.t -> Infsys.LEVEL.t -> bool
               val diff : Infsys.LEVEL.t -> Infsys.LEVEL.t -> Infsys.LEVEL.t
               val pp : Infsys.LEVEL.t Pretty.printer
             end) ->
        sig
          type e = I.e
          val current : unit -> Infsys.ARITH.e
          val initialize : Infsys.ARITH.e -> unit
          val finalize : unit -> Infsys.ARITH.e
          val abstract : Term.t -> unit
          val merge : Fact.Equal.t -> unit
          val propagate : Fact.Equal.t -> unit
          val dismerge : Fact.Diseq.t -> unit
          val propagate_diseq : Fact.Diseq.t -> unit
          val branch : unit -> unit
          val normalize : unit -> unit
          val nonneg : Fact.Nonneg.t -> unit
          val pos : Fact.Pos.t -> unit
        end
end