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

v0.6.tar.gz
md5=4f0c3d560103914306496f51edf263a2
sha512=a184d4649b5a8a72495413a483c7bd8509da42f11b099f22ebc76da58f523e7bb4903679a5a0c3686633d9fe57a6801d923e88c68de6e4f316ab2cb2626a9cc6

doc/batsat/Batsat/Lit/index.html

Module Batsat.LitSource

Sourcetype t = private int

Some representation of literals that will be accepted by the SAT solver.

Sourceval equal : t -> t -> bool
Sourceval hash : t -> int
Sourceval compare : t -> t -> int
Sourceval make : int -> t

make n creates the literal whose index is n. NOTE n must be strictly positive. Use neg to obtain the negation of a literal.

Sourceval make_with_sign : bool -> int -> t

make_with_sign b x is if b then make x else neg (make x). It applies the given sign to make x.

  • since 0.6
Sourceval neg : t -> t

Negation of a literal. Invariant: neg (neg x) = x

Sourceval abs : t -> t

Absolute value (removes negation if any).

Sourceval sign : t -> bool

Sign: true if the literal is positive, false for a negated literal. Invariants: sign (abs x) = true sign (neg x) = not (sign x)

Sourceval to_int : t -> int
Sourceval to_string : t -> string
Sourceval pp : t printer