ersatz-0.4.1: A monad for expressing SAT or QSAT problems using observable sharing.

Copyright© Edward Kmett 2010-2014 Johan Kiviniemi 2013
LicenseBSD3
MaintainerEdward Kmett <ekmett@gmail.com>
Stabilityexperimental
Portabilitynon-portable
Safe HaskellTrustworthy
LanguageHaskell2010

Ersatz.Problem

Contents

Description

 

Synopsis

SAT

runSAT :: StateT SAT m a -> m (a, SAT) Source #

Run a SAT-generating state computation. Useful e.g. in ghci for disambiguating the type of a MonadState, HasSAT value.

runSAT' :: StateT SAT Identity a -> (a, SAT) Source #

Run a SAT-generating state computation in the Identity monad. Useful e.g. in ghci for disambiguating the type of a MonadState, HasSAT value.

dimacsSAT :: StateT SAT Identity a -> ByteString Source #

Run a SAT-generating state computation and return the respective DIMACS output. Useful for testing and debugging.

generateLiteral :: (MonadState s m, HasSAT s) => a -> (Literal -> m ()) -> m Literal Source #

QSAT

class HasSAT t => HasQSAT t where Source #

Minimal complete definition

qsat

runQSAT :: StateT QSAT m a -> m (a, QSAT) Source #

Run a QSAT-generating state computation. Useful e.g. in ghci for disambiguating the type of a MonadState, HasQSAT value.

runQSAT' :: StateT QSAT Identity a -> (a, QSAT) Source #

Run a QSAT-generating state computation in the Identity monad. Useful e.g. in ghci for disambiguating the type of a MonadState, HasQSAT value.

qdimacsQSAT :: StateT QSAT Identity a -> ByteString Source #

Run a QSAT-generating state computation and return the respective QDIMACS output. Useful for testing and debugging.

DIMACS pretty printing

class DIMACS t where Source #

DIMACS file format pretty printer

This is used to generate the problem statement for a given SAT Solver.

Minimal complete definition

dimacsComments, dimacsNumVariables, dimacsClauses

class QDIMACS t where Source #

QDIMACS file format pretty printer

This is used to generate the problem statement for a given QSAT Solver.

class WDIMACS t where Source #

WDIMACS file format pretty printer

This is used to generate the problem statement for a given MaxSAT Solver (TODO).

dimacs :: DIMACS t => t -> Builder Source #

Generate a Builder out of a DIMACS problem.

qdimacs :: QDIMACS t => t -> Builder Source #

Generate a Builder out of a QDIMACS problem.

wdimacs :: WDIMACS t => t -> Builder Source #

Generate a Builder out of a WDIMACS problem.