Module Mc2_core.Atom
type t
= Mc2_core__.Solver_types.atom
val equal : t -> t -> bool
val compare : t -> t -> int
val hash : t -> int
val same_term : t -> t -> bool
same term, ignoring sign?
val is_pos : t -> bool
Positive atom?
val is_neg : t -> bool
Positive atom?
Negative atom?
val value : t -> Mc2_core__.Solver_types.value option
Positive version
val mark : t -> unit
Mark the atom as seen, using fields in the variable.
val marked : t -> bool
Mark the atom as seen, using fields in the variable.
Returns wether the atom has been marked as seen.
val unmark : t -> unit
Returns wether the atom has been marked as seen.
val mark_neg : t -> unit
Mark negation of the atom
val unmark_neg : t -> unit
Mark negation of the atom
Unmark negation of the atom
val level : t -> int
decision level of the variable
val reason : t -> Mc2_core__.Solver_types.reason option
decision level of the variable
val reason_exn : t -> Mc2_core__.Solver_types.reason
val is_true : t -> bool
True in current model?
val is_false : t -> bool
True in current model?
val is_undef : t -> bool
val has_some_value : t -> bool
val eval : t -> Mc2_core__.Solver_types.eval_res
Semantically evaluate atom
val is_absurd : t -> bool
Semantically evaluate atom
val can_eval_to_false : t -> bool
val term : t -> Mc2_core__.Solver_types.term
val watched : t -> Mc2_core__.Solver_types.clause Mc2_core__.Vec.t
val pp : t CCFormat.printer
nice printer
val debug : t CCFormat.printer
nice printer
very verbose printer