sig
exception InvalidDecl of string
type cst
type case
type path_cell = private {
path_cst : Ind_cst.cst;
path_case : Ind_cst.case;
path_clauses : ClauseContext.t list;
}
type path = Ind_cst.path_cell list
type cover_set = Ind_cst.case list
val case_equal : Ind_cst.case -> Ind_cst.case -> bool
val case_compare : Ind_cst.case -> Ind_cst.case -> int
val case_hash : Ind_cst.case -> int
val pp_case : Ind_cst.case CCFormat.printer
val case_to_term : Ind_cst.case -> Libzipperposition.FOTerm.t
val case_is_rec : Ind_cst.case -> bool
val case_is_base : Ind_cst.case -> bool
val case_sub_constants : Ind_cst.case -> Ind_cst.cst Sequence.t
val cover_set_cases :
?which:[ `All | `Base | `Rec ] ->
Ind_cst.cover_set -> Ind_cst.case Sequence.t
exception Payload_cst of Ind_cst.cst
val as_cst : Libzipperposition.ID.t -> Ind_cst.cst option
val as_cst_exn : Libzipperposition.ID.t -> Ind_cst.cst
val is_cst : Libzipperposition.ID.t -> bool
val on_new_cst : Ind_cst.cst Signal.t
val declare_cst :
?cover_set_depth:int ->
Libzipperposition.ID.t -> ty:Libzipperposition.Type.t -> Ind_cst.cst
val cst_of_term : Libzipperposition.FOTerm.t -> Ind_cst.cst option
val cst_of_id :
Libzipperposition.ID.t -> Libzipperposition.Type.t -> Ind_cst.cst
val declarations_of_cst :
Ind_cst.cst ->
(Libzipperposition.ID.t * Libzipperposition.Type.t) Sequence.t
val cst_equal : Ind_cst.cst -> Ind_cst.cst -> bool
val cst_compare : Ind_cst.cst -> Ind_cst.cst -> int
val cst_hash : Ind_cst.cst -> int
val cst_id : Ind_cst.cst -> Libzipperposition.ID.t
val cst_to_term : Ind_cst.cst -> Libzipperposition.FOTerm.t
val cst_ty : Ind_cst.cst -> Libzipperposition.Type.t
val cst_same_type : Ind_cst.cst -> Ind_cst.cst -> bool
val pp_cst : Ind_cst.cst CCFormat.printer
val cst_depth : Ind_cst.cst -> int
val cst_cover_set : Ind_cst.cst -> Ind_cst.cover_set option
val find_cst_in_term : Libzipperposition.FOTerm.t -> Ind_cst.cst Sequence.t
val is_sub_cst : Libzipperposition.ID.t -> bool
val is_sub_cst_of : Libzipperposition.ID.t -> Ind_cst.cst -> bool
val as_sub_cst_of :
Libzipperposition.ID.t -> Ind_cst.cst -> Ind_cst.cst option
val cover_set_sub_constants : Ind_cst.cover_set -> Ind_cst.cst Sequence.t
val dominates : Ind_cst.cst -> Ind_cst.cst -> bool
val path_equal : Ind_cst.path -> Ind_cst.path -> bool
val path_compare : Ind_cst.path -> Ind_cst.path -> int
val path_hash : Ind_cst.path -> int
val path_empty : Ind_cst.path
val path_cons :
Ind_cst.cst ->
Ind_cst.case -> ClauseContext.t list -> Ind_cst.path -> Ind_cst.path
val path_length : Ind_cst.path -> int
val path_dominates : Ind_cst.path -> Ind_cst.path -> bool
val path_contains_cst : Ind_cst.path -> Ind_cst.cst -> bool
val pp_path : Ind_cst.path CCFormat.printer
val lits_of_path : Ind_cst.path -> Literals.t
val max_depth_ : int Pervasives.ref
end