package mc2

You can search for identifiers within the package.

in-package search v0.2.0

A mcsat-based SMT solver in pure OCaml

Install

md5=92de696251ec76fbf3eba6ee917fd80f

sha512=e88ba0cfc23186570a52172a0bd7c56053273941eaf3cda0b80fb6752e05d1b75986b01a4e4d46d9711124318e57cba1cd92d302e81d34f9f1ae8b49f39114f0

Sourcetype t

Sourceval both_atoms_marked : t -> bool

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

Sourceval 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

Sourceval assigned_atom_exn : t -> Mc2_core__.Solver_types.atom

if assigned and bool, return corresponding atom

Sourceval pa_unsafe : t -> Mc2_core__.Solver_types.atom

Positive atom (assumes has_var t)

Sourceval na_unsafe : t -> Mc2_core__.Solver_types.atom

Positive atom (assumes has_var t)

Negative atom (assumes has_var t)

Sourceval pa : t -> Mc2_core__.Solver_types.atom

safe version of pa_unsafe, call setup_var

Sourceval 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

Sourceval is_true : t -> bool

Sourceval is_false : t -> bool