Satchmo.SAT.External

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

Documentation

data SAT a

Instances

Monad SAT

Functor SAT

Applicative SAT

MonadIO SAT

MonadSAT SAT

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)