package mc2

  1. Overview
  2. Docs
type t
val both_atoms_marked : t -> bool

Did we see both polarities of this var in the same clause?

val assigned_atom : t -> Mc2_core__.Solver_types.atom option

Did we see both polarities of this var in the same clause?

if assigned and bool, return corresponding atom

val assigned_atom_exn : t -> Mc2_core__.Solver_types.atom

if assigned and bool, return corresponding atom

val pa_unsafe : t -> Mc2_core__.Solver_types.atom

Positive atom (assumes has_var t)

val na_unsafe : t -> Mc2_core__.Solver_types.atom

Positive atom (assumes has_var t)

Negative atom (assumes has_var t)

val pa : t -> Mc2_core__.Solver_types.atom

safe version of pa_unsafe, call setup_var

val na : t -> Mc2_core__.Solver_types.atom

safe version of pa_unsafe, call setup_var

safe version of na_unsafe, call setup_var

val mk_eq : Mc2_core__.Solver_types.term -> Mc2_core__.Solver_types.term -> Mc2_core__.Solver_types.atom
val mk_neq : Mc2_core__.Solver_types.term -> Mc2_core__.Solver_types.term -> Mc2_core__.Solver_types.atom
val is_true : t -> bool
val is_false : t -> bool