Ersatz.Solution

Documentation

data Solution

Constructors

Solution

Fields

• solutionLiteral :: Literal -> Maybe Bool
• solutionStableName :: StableName () -> Maybe Bool

solutionFrom :: HasSAT s => IntMap Bool -> s -> Solution

data Result

Constructors

Unsolved

Unsatisfied

Satisfied

Instances

Bounded Result

Methods

minBound :: Result

maxBound :: Result

Enum Result

Methods

succ :: Result -> Result

pred :: Result -> Result

toEnum :: Int -> Result

fromEnum :: Result -> Int

enumFrom :: Result -> [Result]

enumFromThen :: Result -> Result -> [Result]

enumFromTo :: Result -> Result -> [Result]

enumFromThenTo :: Result -> Result -> Result -> [Result]

Eq Result

Methods

(==) :: Result -> Result -> Bool

(/=) :: Result -> Result -> Bool

Ord Result

Methods

compare :: Result -> Result -> Ordering

(<) :: Result -> Result -> Bool

(<=) :: Result -> Result -> Bool

(>) :: Result -> Result -> Bool

(>=) :: Result -> Result -> Bool

max :: Result -> Result -> Result

min :: Result -> Result -> Result

Read Result

Methods

readsPrec :: Int -> ReadS Result

readList :: ReadS [Result]

readPrec :: ReadPrec Result

readListPrec :: ReadPrec [Result]

Show Result

Methods

showsPrec :: Int -> Result -> ShowS

show :: Result -> String

showList :: [Result] -> ShowS

Ix Result

Methods

range :: (Result, Result) -> [Result]

index :: (Result, Result) -> Result -> Int

unsafeIndex :: (Result, Result) -> Result -> Int

inRange :: (Result, Result) -> Result -> Bool

rangeSize :: (Result, Result) -> Int

unsafeRangeSize :: (Result, Result) -> Int

type Solver s m = s -> m (Result, IntMap Bool)

A Solver s m is responsible for invoking a solver and returning a Result and a map of determined results.

• s is typically SAT or QSAT
• m is typically IO