package libzipperposition
Install
Dune Dependency
Authors
Maintainers
Sources
md5=e72de75e9f0f87da9e6e8c0a4d4c89f9
sha512=81becfc9badd686ab3692cd9312172aa4c4e3581b110e81770bb01e0ffbc1eb8495d0dd6d43b98f3d06e6b8c8a338174c13ebafb4e9849a3ddf89f9a3a72c287
doc/libzipperposition.avatar/Libzipperposition_avatar/Make/argument-2-Sat/index.html
Parameter Make.Sat
module Lit = Libzipperposition.BBox.Littype clause = Lit.t listval add_clause :
proof:Libzipperposition.Sat_solver.proof_step ->
Lit.t list ->
unitadd_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 ->
unitval add_clause_seq :
proof:Libzipperposition.Sat_solver.proof_step ->
Lit.t list Iter.t ->
unitval check : full:bool -> unit -> Libzipperposition.Sat_solver.resultIs the current problem satisfiable?
val last_result : unit -> Libzipperposition.Sat_solver.resultLast computed result. This does not compute a new result
val valuation : Lit.t -> boolAssuming the last call to check returned Sat, get the boolean valuation for this (positive) literal in the current model.
val valuation_level : Lit.t -> bool * intGives 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
val proved_at_0 : Lit.t -> bool optionIf 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.tSet of (signed) proved literals
val set_printer : Lit.t CCFormat.printer -> unitHow to print literals?
val get_proof : unit -> Libzipperposition.Sat_solver.proofReturn 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.
val get_proof_opt : unit -> Libzipperposition.Sat_solver.proof optionObtain the proof, if any
val get_proof_of_lit : Lit.t -> Libzipperposition.Sat_solver.proofget_proof_of_lit lit returns the proof of lit, assuming it has been proved true at level 0 (see valuation_level)