Copyright	© Edward Kmett 2010-2014 Johan Kiviniemi 2013
License	BSD3
Maintainer	Edward Kmett <ekmett@gmail.com>
Stability	experimental
Portability	non-portable
Safe Haskell	Trustworthy
Language	Haskell2010

Ersatz.Problem

Contents

SAT
QSAT
DIMACS pretty printing

Description

Synopsis

data SAT = SAT !Int !Formula !(HashMap (StableName ()) Literal)
class HasSAT s where
runSAT :: StateT SAT m a -> m (a, SAT)
runSAT' :: StateT SAT Identity a -> (a, SAT)
dimacsSAT :: StateT SAT Identity a -> ByteString
literalExists :: (MonadState s m, HasSAT s) => m Literal
assertFormula :: (MonadState s m, HasSAT s) => Formula -> m ()
generateLiteral :: (MonadState s m, HasSAT s) => a -> (Literal -> m ()) -> m Literal
data QSAT = QSAT !IntSet SAT
class HasSAT t => HasQSAT t where
runQSAT :: StateT QSAT m a -> m (a, QSAT)
runQSAT' :: StateT QSAT Identity a -> (a, QSAT)
qdimacsQSAT :: StateT QSAT Identity a -> ByteString
literalForall :: (MonadState s m, HasQSAT s) => m Literal
class DIMACS t where
class QDIMACS t where
class WDIMACS t where
dimacs :: DIMACS t => t -> Builder
qdimacs :: QDIMACS t => t -> Builder
wdimacs :: WDIMACS t => t -> Builder

SAT

data SAT #

Constructors

SAT !Int !Formula !(HashMap (StableName ()) Literal)

Instances

Show SAT #
Instance details Defined in Ersatz.Problem Methods showsPrec :: Int -> SAT -> ShowS # show :: SAT -> String # showList :: [SAT] -> ShowS #
Default SAT #
Instance details Defined in Ersatz.Problem Methods def :: SAT #
DIMACS SAT #
Instance details Defined in Ersatz.Problem Methods dimacsComments :: SAT -> [ByteString] # dimacsNumVariables :: SAT -> Int # dimacsClauses :: SAT -> Seq IntSet #
HasSAT SAT #
Instance details Defined in Ersatz.Problem Methods sat :: Lens' SAT SAT # lastAtom :: Lens' SAT Int # formula :: Lens' SAT Formula # stableMap :: Lens' SAT (HashMap (StableName ()) Literal) #

class HasSAT s where #

Minimal complete definition

sat

Methods

sat :: Lens' s SAT #

lastAtom :: Lens' s Int #

formula :: Lens' s Formula #

stableMap :: Lens' s (HashMap (StableName ()) Literal) #

Instances

HasSAT QSAT #
Instance details Defined in Ersatz.Problem Methods sat :: Lens' QSAT SAT # lastAtom :: Lens' QSAT Int # formula :: Lens' QSAT Formula # stableMap :: Lens' QSAT (HashMap (StableName ()) Literal) #
HasSAT SAT #
Instance details Defined in Ersatz.Problem Methods sat :: Lens' SAT SAT # lastAtom :: Lens' SAT Int # formula :: Lens' SAT Formula # stableMap :: Lens' SAT (HashMap (StableName ()) Literal) #

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

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) #

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 #

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

literalExists :: (MonadState s m, HasSAT s) => m Literal #

assertFormula :: (MonadState s m, HasSAT s) => Formula -> m () #

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

QSAT

data QSAT #

A (quantified) boolean formula.

Constructors

QSAT !IntSet SAT

Instances

Show QSAT #
Instance details Defined in Ersatz.Problem Methods showsPrec :: Int -> QSAT -> ShowS # show :: QSAT -> String # showList :: [QSAT] -> ShowS #
Default QSAT #
Instance details Defined in Ersatz.Problem Methods def :: QSAT #
QDIMACS QSAT #
Instance details Defined in Ersatz.Problem Methods qdimacsComments :: QSAT -> [ByteString] # qdimacsNumVariables :: QSAT -> Int # qdimacsQuantified :: QSAT -> [Quant] # qdimacsClauses :: QSAT -> Seq IntSet #
HasQSAT QSAT #
Instance details Defined in Ersatz.Problem Methods qsat :: Lens' QSAT QSAT # universals :: Lens' QSAT IntSet #
HasSAT QSAT #
Instance details Defined in Ersatz.Problem Methods sat :: Lens' QSAT SAT # lastAtom :: Lens' QSAT Int # formula :: Lens' QSAT Formula # stableMap :: Lens' QSAT (HashMap (StableName ()) Literal) #

class HasSAT t => HasQSAT t where #

Minimal complete definition

qsat

Methods

qsat :: Lens' t QSAT #

universals :: Lens' t IntSet #

Instances

HasQSAT QSAT #
Instance details Defined in Ersatz.Problem Methods qsat :: Lens' QSAT QSAT # universals :: Lens' QSAT IntSet #

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

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) #

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 #

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

literalForall :: (MonadState s m, HasQSAT s) => m Literal #

DIMACS pretty printing

class DIMACS t where #

DIMACS file format pretty printer

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

Minimal complete definition

dimacsComments, dimacsNumVariables, dimacsClauses

Methods

dimacsComments :: t -> [ByteString] #

dimacsNumVariables :: t -> Int #

dimacsClauses :: t -> Seq IntSet #

Instances

DIMACS SAT #
Instance details Defined in Ersatz.Problem Methods dimacsComments :: SAT -> [ByteString] # dimacsNumVariables :: SAT -> Int # dimacsClauses :: SAT -> Seq IntSet #

class QDIMACS t where #

QDIMACS file format pretty printer

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

Minimal complete definition

qdimacsComments, qdimacsNumVariables, qdimacsQuantified, qdimacsClauses

Methods

qdimacsComments :: t -> [ByteString] #

qdimacsNumVariables :: t -> Int #

qdimacsQuantified :: t -> [Quant] #

qdimacsClauses :: t -> Seq IntSet #

Instances

QDIMACS QSAT #
Instance details Defined in Ersatz.Problem Methods qdimacsComments :: QSAT -> [ByteString] # qdimacsNumVariables :: QSAT -> Int # qdimacsQuantified :: QSAT -> [Quant] # qdimacsClauses :: QSAT -> Seq IntSet #