module Satchmo.Solve
( solve
, Implementation
, Decoder
)
where
import Satchmo.Data
import Satchmo.Code
import Satchmo.Internal
import Data.Map ( Map )
import qualified Data.Map as M
import Control.Monad.State
import Control.Monad.Reader
type Implementation = String -> IO ( Maybe ( Map Literal Bool ) )
solve :: Implementation
-> SAT ( Decoder a )
-> IO ( Maybe a )
solve implementation build = do
let (s, a) = sat build
mfm <- implementation s
case mfm of
Nothing -> do
putStrLn "not satisfiable"
return Nothing
Just fm -> do
putStrLn "satisfiable"
return $ Just $ runReader a fm