sig
  type abstract1
  type abstract2
  type symheap = private {
    eqs : Sl_uf.t;
    deqs : Sl_deqs.t;
    ptos : Sl_ptos.t;
    inds : Sl_tpreds.t;
    mutable _terms : Sl_heap.abstract1;
    mutable _vars : Sl_heap.abstract1;
    mutable _tags : Sl_heap.abstract2;
  }
  type t = symheap
  val compare : t -> t -> int
  val hash : t -> int
  val to_string : t -> string
  val pp : Format.formatter -> t -> unit
  val empty : t
  val vars : t -> Sl_term.Set.t
  val terms : t -> Sl_term.Set.t
  val tags : t -> Tags.t
  val tag_pairs : t -> Tagpairs.t
  val to_melt : t -> Latex.t
  val has_untagged_preds : t -> bool
  val complete_tags : Tags.t -> t -> t
  val equates : t -> Sl_term.t -> Sl_term.t -> bool
  val disequates : t -> Sl_term.t -> Sl_term.t -> bool
  val find_lval : Sl_term.t -> t -> Sl_pto.t option
  val idents : t -> Sl_predsym.MSet.t
  val inconsistent : t -> bool
  val subsumed : ?total:bool -> t -> t -> bool
  val subsumed_upto_tags : ?total:bool -> t -> t -> bool
  val equal : t -> t -> bool
  val equal_upto_tags : t -> t -> bool
  val is_empty : t -> bool
  val parse : ?allow_tags:bool -> ?augment_deqs:bool -> (t, 'a) MParser.t
  val of_string : ?allow_tags:bool -> ?augment_deqs:bool -> string -> t
  val mk_pto : Sl_pto.t -> t
  val mk_eq : Sl_tpair.t -> t
  val mk_deq : Sl_tpair.t -> t
  val mk_ind : Sl_tpred.t -> t
  val mk : Sl_uf.t -> Sl_deqs.t -> Sl_ptos.t -> Sl_tpreds.t -> t
  val dest : t -> Sl_uf.t * Sl_deqs.t * Sl_ptos.t * Sl_tpreds.t
  val with_eqs : t -> Sl_uf.t -> t
  val with_deqs : t -> Sl_deqs.t -> t
  val with_ptos : t -> Sl_ptos.t -> t
  val with_inds : t -> Sl_tpreds.t -> t
  val del_deq : t -> Sl_tpair.t -> t
  val del_pto : t -> Sl_pto.t -> t
  val del_ind : t -> Sl_tpred.t -> t
  val add_eq : t -> Sl_tpair.t -> t
  val add_deq : t -> Sl_tpair.t -> t
  val add_pto : t -> Sl_pto.t -> t
  val add_ind : t -> Sl_tpred.t -> t
  val proj_sp : t -> t
  val proj_pure : t -> t
  val explode_deqs : t -> t
  val star : ?augment_deqs:bool -> t -> t -> t
  val diff : t -> t -> t
  val fixpoint : (t -> t) -> t -> t
  val subst : Sl_subst.t -> t -> t
  val univ : Sl_term.Set.t -> t -> t
  val subst_existentials : t -> t
  val project : t -> Sl_term.t list -> t
  val freshen_tags : t -> t -> t
  val subst_tags : Tagpairs.t -> t -> t
  val unify_partial :
    ?tagpairs:bool ->
    ?update_check:Sl_unify.Unidirectional.update_check ->
    t Sl_unify.Unidirectional.unifier
  val biunify_partial :
    ?tagpairs:bool ->
    ?update_check:Sl_unify.Bidirectional.update_check ->
    t Sl_unify.Bidirectional.unifier
  val classical_unify :
    ?inverse:bool ->
    ?tagpairs:bool ->
    ?update_check:Sl_unify.Unidirectional.update_check ->
    t Sl_unify.Unidirectional.unifier
  val classical_biunify :
    ?tagpairs:bool ->
    ?update_check:Sl_unify.Bidirectional.update_check ->
    t Sl_unify.Bidirectional.unifier
  val norm : t -> t
  val all_subheaps : t -> t list
  val memory_consuming : t -> bool
  val constructively_valued : t -> bool
end