package libzipperposition

  1. Overview
  2. Docs
Library for Zipperposition

Install 

dune-project
 Dependency

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

Authors

  1. S
    Simon Cruanes
  2. P
    Petar Vukmirovic
  3. A
    Alexander Bentkamp
  4. S
    Sophie Tourret
  5. V
    Visa Nummelin

Maintainers

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

Sources

2.0.tar.gz
md5=7a8e57388083ed763d12d18324c8a086
sha512=5c5ac312ada6b42907d1e91e349454a8375f7bf8165d3459721a40b707a840a3d6b3dc968a66f1040cb4de7aedf5c1c13f3e90b51337eae5ea6de41651d7bd63

doc/libzipperposition.avatar/Libzipperposition_avatar/Make/argument-2-Sat/index.html

Parameter Make.Sat

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