sig
  type symbol_status =
    LogtkPrecedence_intf.symbol_status =
      Multiset
    | Lexicographic
  module type S = LogtkPrecedence_intf.S
  module type SYMBOL =
    sig
      type t
      val eq : LogtkPrecedence.SYMBOL.t -> LogtkPrecedence.SYMBOL.t -> bool
      val hash : LogtkPrecedence.SYMBOL.t -> int
      val cmp : LogtkPrecedence.SYMBOL.t -> LogtkPrecedence.SYMBOL.t -> int
      val false_ : LogtkPrecedence.SYMBOL.t
      val true_ : LogtkPrecedence.SYMBOL.t
      val pp : Buffer.t -> LogtkPrecedence.SYMBOL.t -> unit
      val pp_debug : Buffer.t -> LogtkPrecedence.SYMBOL.t -> unit
    end
  module Make :
    functor (Sym : SYMBOL->
      sig
        type symbol = Sym.t
        type t
        type precedence = t
        val eq : t -> t -> bool
        val snapshot : t -> symbol list
        val compare : t -> symbol -> symbol -> int
        val mem : t -> symbol -> bool
        val status : t -> symbol -> LogtkPrecedence_intf.symbol_status
        val weight : t -> symbol -> int
        val add_list : t -> symbol list -> t
        val add_seq : t -> symbol Sequence.t -> t
        val declare_status :
          t -> symbol -> LogtkPrecedence_intf.symbol_status -> t
        module Seq : sig val symbols : t -> symbol Sequence.t end
        val pp_snapshot : Buffer.t -> symbol list -> unit
        val pp_debug : Buffer.t -> t -> unit
        val pp : Buffer.t -> t -> unit
        val fmt : Format.formatter -> t -> unit
        val to_string : t -> string
        module Constr :
          sig
            type t = symbol -> symbol -> LogtkComparison.t
            val cluster : symbol list list -> t
            val of_list : symbol list -> t
            val of_precedence : precedence -> t
            val arity : (symbol -> int) -> t
            val invfreq : symbol Sequence.t -> t
            val max : symbol list -> t
            val min : symbol list -> t
            val alpha : t
          end
        type weight_fun = symbol -> int
        val weight_modarity : arity:(symbol -> int) -> weight_fun
        val weight_constant : weight_fun
        val set_weight : t -> weight_fun -> t
        val create : ?weight:weight_fun -> Constr.t list -> symbol list -> t
        val create_sort :
          ?weight:weight_fun -> (int * Constr.t) list -> symbol list -> t
        val default : symbol list -> t
        val default_seq : symbol Sequence.t -> t
        val constr_list : t -> Constr.t list
        val with_constr_list : t -> Constr.t list -> t
      end
  module Default :
    sig
      type symbol = LogtkSymbol.t
      type t
      type precedence = t
      val eq : t -> t -> bool
      val snapshot : t -> symbol list
      val compare : t -> symbol -> symbol -> int
      val mem : t -> symbol -> bool
      val status : t -> symbol -> LogtkPrecedence_intf.symbol_status
      val weight : t -> symbol -> int
      val add_list : t -> symbol list -> t
      val add_seq : t -> symbol Sequence.t -> t
      val declare_status :
        t -> symbol -> LogtkPrecedence_intf.symbol_status -> t
      module Seq : sig val symbols : t -> symbol Sequence.t end
      val pp_snapshot : Buffer.t -> symbol list -> unit
      val pp_debug : Buffer.t -> t -> unit
      val pp : Buffer.t -> t -> unit
      val fmt : Format.formatter -> t -> unit
      val to_string : t -> string
      module Constr :
        sig
          type t = symbol -> symbol -> LogtkComparison.t
          val cluster : symbol list list -> t
          val of_list : symbol list -> t
          val of_precedence : precedence -> t
          val arity : (symbol -> int) -> t
          val invfreq : symbol Sequence.t -> t
          val max : symbol list -> t
          val min : symbol list -> t
          val alpha : t
        end
      type weight_fun = symbol -> int
      val weight_modarity : arity:(symbol -> int) -> weight_fun
      val weight_constant : weight_fun
      val set_weight : t -> weight_fun -> t
      val create : ?weight:weight_fun -> Constr.t list -> symbol list -> t
      val create_sort :
        ?weight:weight_fun -> (int * Constr.t) list -> symbol list -> t
      val default : symbol list -> t
      val default_seq : symbol Sequence.t -> t
      val constr_list : t -> Constr.t list
      val with_constr_list : t -> Constr.t list -> t
    end
  type symbol = LogtkSymbol.t
  type t = Default.t
  type precedence = t
  val eq : t -> t -> bool
  val snapshot : t -> symbol list
  val compare : t -> symbol -> symbol -> int
  val mem : t -> symbol -> bool
  val status : t -> symbol -> LogtkPrecedence_intf.symbol_status
  val weight : t -> symbol -> int
  val add_list : t -> symbol list -> t
  val add_seq : t -> symbol Sequence.t -> t
  val declare_status : t -> symbol -> LogtkPrecedence_intf.symbol_status -> t
  module Seq : sig val symbols : t -> symbol Sequence.t end
  val pp_snapshot : Buffer.t -> symbol list -> unit
  val pp_debug : Buffer.t -> t -> unit
  val pp : Buffer.t -> t -> unit
  val fmt : Format.formatter -> t -> unit
  val to_string : t -> string
  module Constr :
    sig
      type t = symbol -> symbol -> LogtkComparison.t
      val cluster : symbol list list -> t
      val of_list : symbol list -> t
      val of_precedence : precedence -> t
      val arity : (symbol -> int) -> t
      val invfreq : symbol Sequence.t -> t
      val max : symbol list -> t
      val min : symbol list -> t
      val alpha : t
    end
  type weight_fun = symbol -> int
  val weight_modarity : arity:(symbol -> int) -> weight_fun
  val weight_constant : weight_fun
  val set_weight : t -> weight_fun -> t
  val create : ?weight:weight_fun -> Constr.t list -> symbol list -> t
  val create_sort :
    ?weight:weight_fun -> (int * Constr.t) list -> symbol list -> t
  val default : symbol list -> t
  val default_seq : symbol Sequence.t -> t
  val constr_list : t -> Constr.t list
  val with_constr_list : t -> Constr.t list -> t
end