module Satchmo.Solve
( solve, solveW
, Implementation, WeightedImplementation
, Decoder
)
where
import Satchmo.Data
import Satchmo.Code
import Satchmo.SAT
import qualified Satchmo.SAT.Weighted as Weighted
import qualified Data.ByteString.Lazy.Char8 as BS
import Data.Map ( Map )
import qualified Data.Map as M
import Control.Monad.Reader
import System.IO
type Implementation = BS.ByteString
-> Header
-> IO ( Maybe ( Map Variable Bool ) )
type WeightedImplementation = BS.ByteString
-> Weighted.Header
-> IO ( Maybe ( Map Variable Bool ) )
solve :: Implementation
-> SAT ( Decoder a )
-> IO ( Maybe a )
solve implementation build = do
(s, h, a) <- sat build
mfm <- implementation s h
case mfm of
Nothing -> do
hPutStrLn stderr "not satisfiable"
return Nothing
Just fm -> do
hPutStrLn stderr "satisfiable"
return $ Just $ runReader a fm
solveW :: Weighted.MaxWeight
-> WeightedImplementation
-> Weighted.SAT (Decoder a)
-> IO (Maybe a)
solveW maxW implementation build = do
(s, h, a) <- Weighted.sat maxW build
mfm <- implementation s h
case mfm of
Nothing -> do
hPutStrLn stderr "not satisfiable"
return Nothing
Just fm -> do
hPutStrLn stderr "satisfiable"
return $ Just $ runReader a fm