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/Actions/index.html

Module `Mc2_core.Actions`Source

Actions for Plugins

Plugins are given a set of possible actions at certain times, such as propagation or first-time addition of watches to a term.

Sourcetype t

Actions available to terms/plugins when doing propagation/model building, including adding clauses, registering actions to do upon backtracking, etc.

Sourceval push_clause : t -> Mc2_core__.Solver_types.clause -> unit

push a new clause. This clause is added to the solver and will not be backtracked.

Sourceval level : t -> int

access current decision level

Source

val propagate_bool_eval : 
  t ->
  Mc2_core__.Solver_types.term ->
  bool ->
  subs:Mc2_core__.Solver_types.term list ->
  unit

propagate_bool_eval t b l propagates the boolean literal t assigned to boolean value b, explained by evaluation with relevant (sub)terms l

parameter subs
subterms used for the propagation

Source

val propagate_bool_lemma : 
  t ->
  Mc2_core__.Solver_types.term ->
  bool ->
  Mc2_core__.Solver_types.atom list ->
  Mc2_core__.Solver_types.lemma ->
  unit

propagate_bool_lemma t b c propagates the boolean literal t assigned to boolean value b, explained by a valid theory lemma c. Precondition: c is a tautology such that c == (c' ∨ t=b), where c' is composed of atoms false in current model.

Source

val raise_conflict : 
  t ->
  Mc2_core__.Solver_types.atom list ->
  Mc2_core__.Solver_types.lemma ->
  'a

Raise a conflict with the given clause, which must be false in the current trail, and with a lemma to explain

Sourceval on_backtrack : t -> (unit -> unit) -> unit

on_backtrack f will call f when the solver backtracks

On This Page

Actions for Plugins

package mc2

Install

Dune Dependency

Authors

Maintainers

Sources

doc/mc2.core/Mc2_core/Actions/index.html

Module Mc2_core.ActionsSource

Actions for Plugins

Module `Mc2_core.Actions`Source