Module `Make_cdcl_t.Clause`

type t = clause

val make_a : flags:int -> atom array -> premise -> clause
val make : flags:int -> atom list -> premise -> clause
val empty : flags:int -> clause
val name : clause -> string
val equal : clause -> clause -> bool
val hash : clause -> int
val atoms : clause -> atom array
val atoms_seq : clause -> atom Iter.t
val atoms_l : clause -> atom list
val flag_attached : int
val flag_visited : int
val flag_removable : int
val flag_dead : int
val make_removable : atom list -> premise -> clause
val make_removable_a : atom array -> premise -> clause
val make_permanent : atom list -> premise -> clause
val visited : clause -> bool
val set_visited : clause -> bool -> unit
val attached : clause -> bool
val set_attached : clause -> bool -> unit
val removable : clause -> bool
val set_removable : clause -> bool -> unit
val dead : clause -> bool
val set_dead : clause -> unit
val activity : clause -> float
val set_activity : clause -> float -> unit

module Tbl : sig ... end

val pp : Format.formatter -> clause -> unit
val debug_premise : Format.formatter -> premise -> unit
val debug : Format.formatter -> clause -> unit