package libzipperposition
Install
Dune Dependency
Authors
Maintainers
Sources
md5=97cdb2f90468e9e27c7bbe3b4fb160bb
sha512=fee73369f673a91dfa9e265fc69be08b32235e10a495f3af6477d404fcd01e3452a0d012b150f3d7f97c00af2f6045019ad039164bf698f70d771231cc4efe5d
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)