module type S = sig .. end
module Lit: BBox.Lit
exception UndecidedLit
type Lit.t list
val add_clause : proof:Sat_solver_intf.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:Sat_solver_intf.proof_step -> Lit.t list list -> unit
val add_clause_seq : proof:Sat_solver_intf.proof_step -> Lit.t list Sequence.t -> unit
val check : full:bool -> unit -> Sat_solver_intf.result
Is the current problem satisfiable?
full : if true, check unconditionally
val last_result : unit -> Sat_solver_intf.result
Last computed result. This does not compute a new result
val valuation : Lit.t -> bool
Assuming the last call to
Sat_solver_intf.S.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 -> Sat_solver_intf.proof
Return a proof of
false, assuming
Sat_solver_intf.S.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 -> Sat_solver_intf.proof option
Obtain the proof, if any
val get_proof_of_lit : Lit.t -> Sat_solver_intf.proof
get_proof_of_lit lit returns the proof of
lit, assuming it has been
proved true at level 0 (see
Sat_solver_intf.S.valuation_level)
Raises Invalid_argument if the literal is not at level 0
val setup : unit -> unit