package mc2

  1. Overview
  2. Docs
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

Positive atom?

Negative atom?

val neg : t -> t

Negative atom?

Negation

val abs : t -> t

Negation

Positive version

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

nice printer

val debug : t CCFormat.printer

nice printer

very verbose printer

module Tbl : CCHashtbl.S with type key = t
module Set : CCSet.S with type elt = t