Satchmo.SAT.External

call an external solver as separate process, communicate via pipes.

Documentation

data SAT a

Instances

MonadIO SAT

Defined in Satchmo.SAT.External

Methods

liftIO :: IO a -> SAT a

Applicative SAT

Defined in Satchmo.SAT.External

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

Methods

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

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

Monad SAT

Defined in Satchmo.SAT.External

Methods

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

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

return :: a -> SAT a

MonadSAT SAT

Defined in Satchmo.SAT.External

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

type Decoder SAT

Defined in Satchmo.SAT.External

type Decoder SAT

fresh, fresh_forall :: MonadSAT m => m Literal

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

solve

Arguments

:: String

command, e.g., glucose

-> [String]

options, e.g., -model

-> SAT (Dec a)

action that builds the formula and returns the decoder

-> IO (Maybe a)