Module Batsat

Bindings to Batsat

type t

An instance of batsat (stateful)

type 'a printer = Format.formatter -> 'a -> unit
module Lit : sig ... end
type assumptions = Lit.t array
val create : unit -> t
exception Unsat
val add_clause_l : t -> Lit.t list -> unit
raises Unsat

if the problem is unsat

val add_clause_a : t -> Lit.t array -> unit
raises Unsat

if the problem is unsat

val pp_clause : Lit.t list printer
val simplify : t -> unit
raises Unsat

if the problem is unsat

val solve : ?⁠assumptions:assumptions -> t -> unit
raises Unsat

if the problem is unsat

val n_vars : t -> int
val n_clauses : t -> int
val n_conflicts : t -> int
val n_props : t -> int

Number of SAT propagations

since
0.4
val n_decisions : t -> int

Number of SAT decisions

since
0.4
val is_in_unsat_core : t -> Lit.t -> bool

is_in_unsat_core s lit checks whether abs(lit) is part of the unsat core (if it was an assumption) precondition: last call to solve raised Unsat

val unsat_core : t -> Lit.t array

Access the whole unsat core precondition: last call to solve raised Unsat

val n_proved_lvl_0 : t -> int

Number of literals true at level0 (ie proved unconditionally). Can only grow.

val get_proved_lvl_0 : t -> int -> Lit.t

Get the n-th proved literal

val proved_lvl_0 : t -> Lit.t array

All literals currently proved at level 0

type value =
| V_undef
| V_true
| V_false
val pp_value : value printer
val string_of_value : value -> string
val value : t -> Lit.t -> value
val value_lvl_0 : t -> Lit.t -> value

value_lvl_0 solver lit returns the value of lit if it has this value at level 0 (proved), or V_undef otherwise