package batsat

You can search for identifiers within the package.

in-package search v0.2.0

Legend:
Library
Module
Module type
Parameter
Class
Class type

type t = private int

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

val equal : t -> t -> bool

val hash : t -> int

val compare : t -> t -> int

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

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

val neg : t -> t

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

val abs : t -> t

Absolute value (removes negation if any).

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

val to_int : t -> int

val to_string : t -> string

val pp : t printer