sig
type flag
type t = private {
id : int;
lits : Logtk.Literal.t array;
trail : Trail.t;
mutable flags : SClause.flag;
}
val make : trail:Trail.t -> Logtk.Literal.t array -> SClause.t
val equal : SClause.t -> SClause.t -> bool
val compare : SClause.t -> SClause.t -> int
val hash : SClause.t -> int
val id : SClause.t -> int
val lits : SClause.t -> Logtk.Literal.t array
val trail : SClause.t -> Trail.t
val is_empty : SClause.t -> bool
val length : SClause.t -> int
val update_trail : (Trail.t -> Trail.t) -> SClause.t -> SClause.t
val to_s_form :
?ctx:Logtk.Term.Conv.ctx -> SClause.t -> Logtk.TypedSTerm.Form.t
val flag_lemma : SClause.flag
val flag_persistent : SClause.flag
val flag_redundant : SClause.flag
val flag_backward_simplified : SClause.flag
val set_flag : SClause.flag -> SClause.t -> bool -> unit
val get_flag : SClause.flag -> SClause.t -> bool
val new_flag : unit -> SClause.flag
val mark_redundant : SClause.t -> unit
val is_redundant : SClause.t -> bool
val mark_backward_simplified : SClause.t -> unit
val is_backward_simplified : SClause.t -> bool
val pp_vars : SClause.t CCFormat.printer
val pp : SClause.t CCFormat.printer
val pp_zf : SClause.t CCFormat.printer
val pp_tstp : SClause.t CCFormat.printer
val pp_tstp_full : SClause.t CCFormat.printer
val pp_trail : Trail.t CCFormat.printer
val pp_trail_tstp : Trail.t CCFormat.printer
val pp_in : Logtk.Output_format.t -> SClause.t CCFormat.printer
val proof_tc : SClause.t Logtk.Proof.Result.tc
val mk_proof_res : SClause.t -> Logtk.Proof.Result.t
val adapt : Logtk.Proof.S.t -> SClause.t -> Logtk.Proof.S.t
end