package batsat

  1. Overview
  2. Docs
OCaml bindings for batsat, a SAT solver in rust

Install 

dune-project
 Dependency

github.com Readme Edit opam file Versions (4)

Authors

  1. S
    simon.cruanes.2007@m4x.org

Maintainers

  1. S
    simon.cruanes.2007@m4x.org

Sources

0.5.tar.gz
md5=3a2a576ef335ff73ca4004f507271049
sha512=5be97404493b1decc1ca5be6a56d162dd58cb908a9c74c8828f8a74007c12156526d5c9da67b78707da846a95b65c0914ede0cc5e7a52b1ed5d3dfa14860e3e9

doc/batsat/Batsat/index.html

Module BatsatSource

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
  • raises Unsat

    if the problem is unsat

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 =
  1. | V_undef
  2. | V_true
  3. | 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