Satchmo.SAT.Mini

Documentation

data SAT a

Instances

MonadFix SAT

Defined in Satchmo.SAT.Mini

Methods

mfix :: (a -> SAT a) -> SAT a

MonadIO SAT

need this for hashtables

Defined in Satchmo.SAT.Mini

Methods

liftIO :: IO a -> SAT a

Applicative SAT

Defined in Satchmo.SAT.Mini

Methods

pure :: a -> SAT a

(<*>) :: SAT (a -> b) -> SAT a -> SAT b

liftA2 :: (a -> b -> c) -> SAT a -> SAT b -> SAT c

(*>) :: SAT a -> SAT b -> SAT b

(<*) :: SAT a -> SAT b -> SAT a

Functor SAT

Defined in Satchmo.SAT.Mini

Methods

fmap :: (a -> b) -> SAT a -> SAT b

(<$) :: a -> SAT b -> SAT a

Monad SAT

Defined in Satchmo.SAT.Mini

Methods

(>>=) :: SAT a -> (a -> SAT b) -> SAT b

(>>) :: SAT a -> SAT b -> SAT b

return :: a -> SAT a

MonadSAT SAT

Defined in Satchmo.SAT.Mini

Associated Types

type Decoder SAT :: Type -> Type

Methods

fresh :: SAT Literal

fresh_forall :: SAT Literal

emit :: Clause -> SAT ()

note :: String -> SAT ()

decode_variable :: Variable -> Decoder SAT Bool

Decode SAT Boolean Bool

Defined in Satchmo.SAT.Mini

Methods

decode :: Boolean -> SAT Bool

type Decoder SAT

Defined in Satchmo.SAT.Mini

type Decoder SAT = SAT

fresh, fresh_forall :: MonadSAT m => m Literal

emit :: MonadSAT m => Clause -> m ()

newtype SolveOptions

Constructors

SolveOptions

Fields

• verboseOutput :: Bool

defaultSolveOptions :: SolveOptions

solve :: SAT (SAT a) -> IO (Maybe a)

solveSilently :: SAT (SAT a) -> IO (Maybe a)

solveWith :: SolveOptions -> SAT (SAT a) -> IO (Maybe a)

solve_with_timeout :: Maybe Int -> SAT (SAT a) -> IO (Maybe a)

Orphan instances

Enum Lit

Methods

succ :: Lit -> Lit

pred :: Lit -> Lit

toEnum :: Int -> Lit

fromEnum :: Lit -> Int

enumFrom :: Lit -> [Lit]

enumFromThen :: Lit -> Lit -> [Lit]

enumFromTo :: Lit -> Lit -> [Lit]

enumFromThenTo :: Lit -> Lit -> Lit -> [Lit]