package batsat

  1. Overview
  2. Docs
package batsat
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.

  • since 0.6
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