package libzipperposition
Install
Dune Dependency
Authors
Maintainers
Sources
md5=cc320f66f10555c54822da624419e003
sha512=f8d5f7a5ae790bf0388d74261673803cf375f91f92f7b413b70db1ce5841ef55343a208f98727c8551d66f1840ab892f1c0c943a34861d14d79ce469b235a2f2
doc/libzipperposition.calculi/Libzipperposition_calculi/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)