package mc2

  1. Overview
  2. Docs
A mcsat-based SMT solver in pure OCaml

Install 

dune-project
 Dependency

github.com Readme Changelog Edit opam file Versions (1)

Authors

  1. S
    Simon Cruanes
  2. G
    Guillaume Bury

Maintainers

  1. S
    simon.cruanes.2007@m4x.org

Sources

v0.1.tar.gz
md5=92de696251ec76fbf3eba6ee917fd80f
sha512=e88ba0cfc23186570a52172a0bd7c56053273941eaf3cda0b80fb6752e05d1b75986b01a4e4d46d9711124318e57cba1cd92d302e81d34f9f1ae8b49f39114f0

doc/mc2.core/Mc2_core/Term/Bool/index.html

Module Term.BoolSource

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

Sourceval mk_eq : Mc2_core__.Solver_types.term -> Mc2_core__.Solver_types.term -> Mc2_core__.Solver_types.atom
Sourceval 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