package batsat

  1. Overview
  2. Docs

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 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