ersatz-0.4.8: 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

data SAT Source #

Constructors

SAT !Int !Formula !(HashMap (StableName ()) Literal) 
Instances
Show SAT Source # 
Instance details

Defined in Ersatz.Problem

Methods

showsPrec :: Int -> SAT -> ShowS #

show :: SAT -> String #

showList :: [SAT] -> ShowS #

Default SAT Source # 
Instance details

Defined in Ersatz.Problem

Methods

def :: SAT #

DIMACS SAT Source # 
Instance details

Defined in Ersatz.Problem

HasSAT SAT Source # 
Instance details

Defined in Ersatz.Problem

type MonadSAT s m = (HasSAT s, MonadState s m) Source #

Constraint synonym for types that carry a SAT state.

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 MonadSAT 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 MonadSAT 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 :: MonadSAT s m => a -> (Literal -> m ()) -> m Literal Source #

QSAT

data QSAT Source #

A (quantified) boolean formula.

Constructors

QSAT !IntSet SAT 
Instances
Show QSAT Source # 
Instance details

Defined in Ersatz.Problem

Methods

showsPrec :: Int -> QSAT -> ShowS #

show :: QSAT -> String #

showList :: [QSAT] -> ShowS #

Default QSAT Source # 
Instance details

Defined in Ersatz.Problem

Methods

def :: QSAT #

QDIMACS QSAT Source # 
Instance details

Defined in Ersatz.Problem

HasQSAT QSAT Source # 
Instance details

Defined in Ersatz.Problem

HasSAT QSAT Source # 
Instance details

Defined in Ersatz.Problem

class HasSAT t => HasQSAT t where Source #

Minimal complete definition

qsat

Instances
HasQSAT QSAT Source # 
Instance details

Defined in Ersatz.Problem

type MonadQSAT s m = (HasQSAT s, MonadState s m) Source #

Constraint synonym for types that carry a QSAT state.

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.

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

Methods

wdimacsComments :: t -> [ByteString] Source #

wdimacsNumVariables :: t -> Int Source #

wdimacsTopWeight Source #

Arguments

:: t 
-> Int64

Specified to be 1 ≤ n < 2^63

wdimacsClauses :: t -> Seq (Int64, IntSet) Source #

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.