package minisat

You can search for identifiers within the package.

in-package search v0.2.0

minisat
- Minisat
  - Debug
  - Lit

Legend:
Library
Module
Module type
Parameter
Class
Class type

type t = private int

Some representation of literals that will be accepted by minisat. NOTE the representation used by minisat is not based on sign but parity. Do not try to encode negative literals as negative integers.

val equal : t -> t -> bool

since 0.6

val compare : t -> t -> int

since 0.6

val hash : t -> int

since 0.6

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 neg : t -> t

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

val abs : t -> t

Absolute value (removes negation if any).

val apply_sign : bool -> t -> t

apply_sign true lit is lit; apply_sign false lit is neg lit

since 0.6

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