mc2.core
Mc2_core.Atom
mc2.backend
mc2.dimacs
mc2.lra
mc2.propositional
mc2.smtlib
mc2.uf
mc2.unin_sort
type t
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
Negative atom?
val neg : t -> t
Negation
val abs : t -> t
Positive version
val value : t -> Mc2_core__.Solver_types.value option
val mark : t -> unit
Mark the atom as seen, using fields in the variable.
val marked : t -> bool
Returns wether the atom has been marked as seen.
val unmark : t -> unit
val mark_neg : t -> unit
Mark negation of the atom
val unmark_neg : t -> unit
Unmark negation of the atom
val level : t -> int
decision level of the variable
val reason : t -> Mc2_core__.Solver_types.reason option
val reason_exn : t -> Mc2_core__.Solver_types.reason
val is_true : t -> bool
True in current model?
val is_false : t -> bool
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
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
very verbose printer
module Tbl : CCHashtbl.S with type key = t
module Set : CCSet.S with type elt = t