package libzipperposition

  1. Overview
  2. Docs
package libzipperposition
Legend:
Library
Module
Module type
Parameter
Class
Class type
exception UndecidedLit
type clause = Lit.t list
val add_clause : proof:Libzipperposition.Sat_solver.proof_step -> Lit.t list -> unit

add_clause ~tag ~proof c adds the constraint c to the SAT solver, annotated with proof. tag is a unique identifier for this constraint and must not have been already used.

val add_clauses : proof:Libzipperposition.Sat_solver.proof_step -> Lit.t list list -> unit
val add_clause_seq : proof:Libzipperposition.Sat_solver.proof_step -> Lit.t list Iter.t -> unit
val check : full:bool -> unit -> Libzipperposition.Sat_solver.result

Is the current problem satisfiable?

  • parameter full

    if true, check unconditionally

val last_result : unit -> Libzipperposition.Sat_solver.result

Last computed result. This does not compute a new result

val valuation : Lit.t -> bool

Assuming the last call to check returned Sat, get the boolean valuation for this (positive) literal in the current model.

  • raises WrongState

    if the last result wasn't Sat

val valuation_level : Lit.t -> bool * int

Gives the value of a literal in the model, as well as its decision level. If decision level is 0, the literal has been proved, rather than decided/propagated

  • raises WrongState

    if the last result wasn't Sat

val proved_at_0 : Lit.t -> bool option

If the literal has been propagated at decision level 0, return its value (which does not depend on the model). Otherwise return None

val all_proved : unit -> Lit.Set.t

Set of (signed) proved literals

val set_printer : Lit.t CCFormat.printer -> unit

How to print literals?

val get_proof : unit -> Libzipperposition.Sat_solver.proof

Return a proof of false, assuming check returned Unsat. The leaves of the proof are input clauses' proofs, the internal nodes are clauses deduced by the SAT solver.

  • raises WrongState

    if the last result isn't Unsat

val get_proof_opt : unit -> Libzipperposition.Sat_solver.proof option

Obtain the proof, if any

val get_proof_of_lit : Lit.t -> Libzipperposition.Sat_solver.proof

get_proof_of_lit lit returns the proof of lit, assuming it has been proved true at level 0 (see valuation_level)

val setup : unit -> unit
val clear : ?size:[ `Big | `Small | `Tiny ] -> unit -> unit

Reset the SAT solver state

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