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

Dune Dependency

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

Authors

Maintainers

S

simon.cruanes.2007@m4x.org

Sources

v0.1.tar.gz

md5=92de696251ec76fbf3eba6ee917fd80f

sha512=e88ba0cfc23186570a52172a0bd7c56053273941eaf3cda0b80fb6752e05d1b75986b01a4e4d46d9711124318e57cba1cd92d302e81d34f9f1ae8b49f39114f0

doc/mc2.core/Mc2_core/Solver/Sat_state/index.html

Module `Solver.Sat_state`Source

Sourcetype t = [ `SAT ] state

Sourceval eval : t -> atom -> bool

Returns the valuation of a formula in the current state of the sat solver.

raises UndecidedLit
if the literal is not decided

Sourceval eval_opt : t -> atom -> bool option

Returns the valuation of a formula in the current state of the sat solver.

Sourceval eval_level : t -> atom -> bool * int

Return the current assignment of the literals, as well as its decision level. If the level is 0, then it is necessary for the atom to have this value; otherwise it is due to choices that can potentially be backtracked.

raises UndecidedLit
if the literal is not decided

Sourceval iter_trail : t -> Mc2_core__.Solver_types.term Iter.t

Iterate through the formulas and terms in order of decision/propagation (starting from the first propagation, to the last propagation).

Sourceval model : t -> Mc2_core__.Solver_types.assignment_view list

Returns the model found if the formula is satisfiable.

Sourceval check_model : t -> bool

Check model, or fail