Module `Batsat`Source

Bindings to Batsat

Sourcetype t

An instance of batsat (stateful)

Sourcetype 'a printer = Format.formatter -> 'a -> unit

Sourcemodule Lit : sig ... end

Sourcetype assumptions = Lit.t array

Sourceval create : unit -> t

Sourceexception Unsat

Sourceval add_clause_l : t -> Lit.t list -> unit

raises Unsat
if the problem is unsat

Sourceval add_clause_a : t -> Lit.t array -> unit

raises Unsat
if the problem is unsat

Sourceval pp_clause : Lit.t list printer

Sourceval simplify : t -> unit

raises Unsat
if the problem is unsat

Sourceval solve : ?assumptions:assumptions -> t -> unit

Solve the problem made by adding clauses using add_clause_l or add_clause_a.

raises Unsat
if the problem is unsat

Sourceval solve_is_sat : ?assumptions:assumptions -> t -> bool

Same as solve but does not raise if unsat.

since 0.6

Sourceval n_vars : t -> int

Sourceval n_clauses : t -> int

Sourceval n_conflicts : t -> int

Sourceval n_props : t -> int

Number of SAT propagations

since 0.4

Sourceval n_decisions : t -> int

Number of SAT decisions

since 0.4

Sourceval 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

Sourceval unsat_core : t -> Lit.t array

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

Sourceval n_proved_lvl_0 : t -> int

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

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

Get the n-th proved literal

Sourceval proved_lvl_0 : t -> Lit.t array

All literals currently proved at level 0

Sourcetype value =

| V_undef
| V_true
| V_false

Sourceval pp_value : value printer

Sourceval string_of_value : value -> string

Sourceval value : t -> Lit.t -> value

Sourceval 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

package batsat

Module BatsatSource

Bindings to Batsat

Module `Batsat`Source