sig
  module Lit = BBox.Lit
  type t
  val equal : Trail.t -> Trail.t -> bool
  val hash : Trail.t -> int
  val compare : Trail.t -> Trail.t -> int
  type bool_lit = Lit.t
  val empty : Trail.t
  val singleton : Trail.bool_lit -> Trail.t
  val mem : Trail.bool_lit -> Trail.t -> bool
  val add : Trail.bool_lit -> Trail.t -> Trail.t
  val remove : Trail.bool_lit -> Trail.t -> Trail.t
  val map : (Trail.bool_lit -> Trail.bool_lit) -> Trail.t -> Trail.t
  val fold : ('a -> Trail.bool_lit -> 'a) -> 'a -> Trail.t -> 'a
  val length : Trail.t -> int
  val for_all : (Trail.bool_lit -> bool) -> Trail.t -> bool
  val exists : (Trail.bool_lit -> bool) -> Trail.t -> bool
  val of_list : Trail.bool_lit list -> Trail.t
  val add_list : Trail.t -> Trail.bool_lit list -> Trail.t
  val to_list : Trail.t -> Trail.bool_lit list
  val to_seq : Trail.t -> Trail.bool_lit Sequence.t
  val labels : Trail.t -> Logtk.Index_intf.labels
  val subsumes : Trail.t -> Trail.t -> bool
  val is_empty : Trail.t -> bool
  val is_trivial : Trail.t -> bool
  val merge : Trail.t -> Trail.t -> Trail.t
  val merge_l : Trail.t list -> Trail.t
  val filter : (Trail.bool_lit -> bool) -> Trail.t -> Trail.t
  type valuation = Trail.bool_lit -> bool
  val is_active : Trail.t -> v:Trail.valuation -> bool
  val to_s_form : Trail.t -> Logtk.TypedSTerm.Form.t
end