sig
  type t = Ord_constraints.t * Sl_heap.t list
  val compare : t -> t -> int
  val equal : t -> t -> bool
  val hash : t -> int
  val to_string : t -> string
  val pp : Format.formatter -> t -> unit
  val empty : t
  exception Not_symheap
  val is_symheap : t -> bool
  val dest : t -> Ord_constraints.t * Sl_heap.t
  val equal_upto_tags : t -> t -> bool
  val to_melt : t -> Latex.t
  val terms : t -> Sl_term.Set.t
  val vars : t -> Sl_term.Set.t
  val tags : t -> Tags.t
  val tag_pairs : t -> Tagpairs.t
  val complete_tags : Tags.t -> t -> t
  val inconsistent : t -> bool
  val subsumed : ?total:bool -> t -> t -> bool
  val subsumed_upto_constraints : ?total:bool -> t -> t -> bool
  val subsumed_upto_tags : ?total:bool -> t -> t -> bool
  val parse :
    ?null_is_emp:bool ->
    ?allow_tags:bool -> ?augment_deqs:bool -> (t, 'a) MParser.t
  val of_string : ?null_is_emp:bool -> string -> t
  val star : ?augment_deqs:bool -> t -> t -> t
  val disj : t -> t -> t
  val subst : Sl_subst.t -> t -> t
  val subst_existentials : t -> t
  val subst_tags : Tagpairs.t -> t -> t
  val norm : t -> t
  val with_constraints : t -> Ord_constraints.t -> t
  val add_constraints : t -> Ord_constraints.t -> t
  val with_heaps : t -> Sl_heap.t list -> t
  val compute_frame :
    ?freshen_existentials:bool ->
    ?avoid:Tags.t * Sl_term.Set.t -> t -> t -> t option
  val get_tracepairs : t -> t -> Tagpairs.t * Tagpairs.t
end