Module Mc2_core.ClauseSource

Boolean Clauses

Sourcetype t
Sourceval make : ?tag:int -> Mc2_core__.Solver_types.atom list -> Mc2_core__.Solver_types.premise -> t

make atoms premise creates a clause with the given attributes.

Sourceval make_arr : ?tag:int -> Mc2_core__.Solver_types.atom array -> Mc2_core__.Solver_types.premise -> t

make_arr atoms premise creates a clause with the given attributes. Consumes the array.

Sourceval equal : t -> t -> bool
Sourceval hash : t -> int
Sourceval visited : t -> bool
Sourceval mark_visited : t -> unit
Sourceval clear_visited : t -> unit
Sourceval attached : t -> bool
Sourceval set_attached : t -> unit
Sourceval deleted : t -> bool
Sourceval set_deleted : t -> unit
Sourceval atoms : t -> Mc2_core__.Solver_types.atom array
Sourceval activity : t -> float
Sourceval name : t -> int
Sourceval premise : t -> Mc2_core__.Solver_types.premise
Sourceval get_tag : t -> int option

Recover tag from a clause, if any

Sourceval gc_mark : t -> unit
Sourceval gc_unmark : t -> unit
Sourceval gc_marked : t -> bool

nice printer

nice printer

very verbose printer

Sourceval pp_atoms : Mc2_core__.Solver_types.atom list CCFormat.printer
Sourceval debug_atoms : Mc2_core__.Solver_types.atom list CCFormat.printer
Sourceval debug_atoms_a : Mc2_core__.Solver_types.atom array CCFormat.printer
Sourceval pp_dimacs : t CCFormat.printer
Sourcemodule Tbl : CCHashtbl.S with type key = Mc2_core__.Solver_types.clause
Sourcemodule Set : CCSet.S with type elt = Mc2_core__.Solver_types.clause