package minisat

You can search for identifiers within the package.

in-package search v0.2.0

minisat
- Library minisat
  - Minisat
    
    Lit
    
    Debug
- Sources
  - minisat
    
    minisat.ml

Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Module `Minisat.Lit`Source

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

Sourceval equal : t -> t -> bool

since 0.6

Sourceval compare : t -> t -> int

since 0.6

Sourceval hash : t -> int

since 0.6

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 apply_sign : bool -> t -> t

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

since 0.6

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

package minisat

Module Minisat.LitSource

Module `Minisat.Lit`Source