package msat

  1. Overview
  2. Docs
package msat
Legend:
Library
Module
Module type
Parameter
Class
Class type
type t

The plugin state itself

include Solver_intf.EXPR
type proof

An abstract type for proofs

module Term : sig ... end
module Value : sig ... end

formulas

val push_level : t -> unit

Create a new backtrack level

val pop_levels : t -> int -> unit

Pop n levels of the theory

val partial_check : t -> (Term.t, Formula.t, Value.t, proof) Solver_intf.acts -> unit

Assume the formulas in the slice, possibly using the slice to push new formulas to be propagated or to raising a conflict or to add new lemmas.

val final_check : t -> (Term.t, Formula.t, Value.t, proof) Solver_intf.acts -> unit

Called at the end of the search in case a model has been found. If no new clause is pushed, then proof search ends and "sat" is returned; if lemmas are added, search is resumed; if a conflict clause is added, search backtracks and then resumes.

val assign : t -> Term.t -> Value.t

Returns an assignment value for the given term.

val iter_assignable : t -> (Term.t -> unit) -> Formula.t -> unit

An iterator over the subTerm.ts of a Formula.t that should be assigned a value (usually the poure subTerm.ts)

Returns the evaluation of the Formula.t in the current assignment

OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct