ersatz-0.6: A monad for expressing SAT or QSAT problems using observable sharing.
Safe HaskellNone
LanguageHaskell2010

Ersatz.Solver.Lingeling

Synopsis

Documentation

lingeling :: MonadIO m => Solver SAT m Source #

Solver for SAT problems that tries to invoke the lingeling executable from the PATH.

plingeling :: MonadIO m => Solver SAT m Source #

Solver for SAT problems that tries to invoke the plingeling executable from the PATH.

treengeling :: MonadIO m => Solver SAT m Source #

Solver for SAT problems that tries to invoke the treengeling executable from the PATH.

lingelingPath :: MonadIO m => FilePath -> Solver SAT m Source #

Solver for SAT problems that tries to invoke a program that takes lingeling compatible arguments.

The FilePath refers to the path to the executable.

plingelingPath :: MonadIO m => FilePath -> Solver SAT m Source #

Solver for SAT problems that tries to invoke a program that takes plingeling compatible arguments.

The FilePath refers to the path to the executable.

treengelingPath :: MonadIO m => FilePath -> Solver SAT m Source #

Solver for SAT problems that tries to invoke a program that takes treengeling compatible arguments.

The FilePath refers to the path to the executable.