Module Term.Bool
type t
= Mc2_core__.Solver_types.bool_term
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
, callsetup_var
val na : t -> Mc2_core__.Solver_types.atom
safe version of
pa_unsafe
, callsetup_var
safe version of
na_unsafe
, callsetup_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