Ersatz.Problem

SAT

data SAT

Constructors

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

Instances

Show SAT

Defined in Ersatz.Problem

Methods

showsPrec :: Int -> SAT -> ShowS

show :: SAT -> String

showList :: [SAT] -> ShowS

Default SAT

Defined in Ersatz.Problem

Methods

def :: SAT

DIMACS SAT

Defined in Ersatz.Problem

Methods

dimacsComments :: SAT -> [ByteString]

dimacsNumVariables :: SAT -> Int

dimacsClauses :: SAT -> Seq IntSet

HasSAT SAT

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

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

Defined in Ersatz.Problem

Methods

sat :: Lens' SAT SAT

lastAtom :: Lens' SAT Int

formula :: Lens' SAT Formula

stableMap :: Lens' SAT (HashMap (StableName ()) Literal)

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

Constraint synonym for types that carry a SAT state.

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 MonadSAT 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 MonadSAT 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 :: MonadSAT s m => m Literal

assertFormula :: MonadSAT s m => Formula -> m ()

generateLiteral :: MonadSAT s m => a -> (Literal -> m ()) -> m Literal

QSAT

data QSAT

A (quantified) boolean formula.

Constructors

QSAT !IntSet SAT

Instances

Show QSAT

Defined in Ersatz.Problem

Methods

showsPrec :: Int -> QSAT -> ShowS

show :: QSAT -> String

showList :: [QSAT] -> ShowS

Default QSAT

Defined in Ersatz.Problem

Methods

def :: QSAT

QDIMACS QSAT

Defined in Ersatz.Problem

Methods

qdimacsComments :: QSAT -> [ByteString]

qdimacsNumVariables :: QSAT -> Int

qdimacsQuantified :: QSAT -> [Quant]

qdimacsClauses :: QSAT -> Seq IntSet

HasQSAT QSAT

Defined in Ersatz.Problem

Methods

qsat :: Lens' QSAT QSAT

universals :: Lens' QSAT IntSet

HasSAT QSAT

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

Defined in Ersatz.Problem

Methods

qsat :: Lens' QSAT QSAT

universals :: Lens' QSAT IntSet

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

Constraint synonym for types that carry a QSAT state.

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 :: MonadQSAT s m => 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.

Methods

dimacsComments :: t -> [ByteString]

dimacsNumVariables :: t -> Int

dimacsClauses :: t -> Seq IntSet

Instances

DIMACS SAT

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.

Methods

qdimacsComments :: t -> [ByteString]

qdimacsNumVariables :: t -> Int

qdimacsQuantified :: t -> [Quant]

qdimacsClauses :: t -> Seq IntSet

Instances

QDIMACS QSAT

Defined in Ersatz.Problem

Methods

qdimacsComments :: QSAT -> [ByteString]

qdimacsNumVariables :: QSAT -> Int

qdimacsQuantified :: QSAT -> [Quant]

qdimacsClauses :: QSAT -> Seq IntSet

class WDIMACS t where

WDIMACS file format pretty printer

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

Methods

wdimacsComments :: t -> [ByteString]

wdimacsNumVariables :: t -> Int

wdimacsTopWeight

Arguments

:: t

-> Int64

Specified to be 1 ≤ n < 2^63

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

dimacs :: DIMACS t => t -> Builder

Generate a Builder out of a DIMACS problem.

qdimacs :: QDIMACS t => t -> Builder

Generate a Builder out of a QDIMACS problem.

wdimacs :: WDIMACS t => t -> Builder

Generate a Builder out of a WDIMACS problem.