{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE DoAndIfThenElse #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# language TemplateHaskell #-}
module Satchmo.SAT.External
( SAT
, fresh
, emit
, solve
)
where
import Satchmo.Data
import Satchmo.Boolean hiding ( not )
import Satchmo.Code
import Control.Monad.Reader
import Control.Monad.State
import System.IO
import Control.Lens
import Control.Applicative
import Control.Concurrent
import Control.DeepSeq (rnf)
import Foreign.C
import System.Process
import Control.Exception
import GHC.IO.Exception ( IOErrorType(..), IOException(..) )
import qualified Control.Exception as C
import qualified Data.ByteString.Char8 as BS
import qualified Data.Map.Strict as M
import Data.List (isPrefixOf)
tracing :: Bool
tracing = Bool
False
report :: String -> IO ()
report String
s = forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
tracing forall a b. (a -> b) -> a -> b
$ Handle -> String -> IO ()
hPutStrLn Handle
stderr String
s
data S = S
{ S -> Int
_next_variable :: !Int
, S -> Handle
_solver_input :: !Handle
}
$(makeLenses ''S)
newtype SAT a = SAT (StateT S IO a)
deriving (forall a b. a -> SAT b -> SAT a
forall a b. (a -> b) -> SAT a -> SAT b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: forall a b. a -> SAT b -> SAT a
$c<$ :: forall a b. a -> SAT b -> SAT a
fmap :: forall a b. (a -> b) -> SAT a -> SAT b
$cfmap :: forall a b. (a -> b) -> SAT a -> SAT b
Functor, Functor SAT
forall a. a -> SAT a
forall a b. SAT a -> SAT b -> SAT a
forall a b. SAT a -> SAT b -> SAT b
forall a b. SAT (a -> b) -> SAT a -> SAT b
forall a b c. (a -> b -> c) -> SAT a -> SAT b -> SAT c
forall (f :: * -> *).
Functor f
-> (forall a. a -> f a)
-> (forall a b. f (a -> b) -> f a -> f b)
-> (forall a b c. (a -> b -> c) -> f a -> f b -> f c)
-> (forall a b. f a -> f b -> f b)
-> (forall a b. f a -> f b -> f a)
-> Applicative f
<* :: forall a b. SAT a -> SAT b -> SAT a
$c<* :: forall a b. SAT a -> SAT b -> SAT a
*> :: forall a b. SAT a -> SAT b -> SAT b
$c*> :: forall a b. SAT a -> SAT b -> SAT b
liftA2 :: forall a b c. (a -> b -> c) -> SAT a -> SAT b -> SAT c
$cliftA2 :: forall a b c. (a -> b -> c) -> SAT a -> SAT b -> SAT c
<*> :: forall a b. SAT (a -> b) -> SAT a -> SAT b
$c<*> :: forall a b. SAT (a -> b) -> SAT a -> SAT b
pure :: forall a. a -> SAT a
$cpure :: forall a. a -> SAT a
Applicative, Applicative SAT
forall a. a -> SAT a
forall a b. SAT a -> SAT b -> SAT b
forall a b. SAT a -> (a -> SAT b) -> SAT b
forall (m :: * -> *).
Applicative m
-> (forall a b. m a -> (a -> m b) -> m b)
-> (forall a b. m a -> m b -> m b)
-> (forall a. a -> m a)
-> Monad m
return :: forall a. a -> SAT a
$creturn :: forall a. a -> SAT a
>> :: forall a b. SAT a -> SAT b -> SAT b
$c>> :: forall a b. SAT a -> SAT b -> SAT b
>>= :: forall a b. SAT a -> (a -> SAT b) -> SAT b
$c>>= :: forall a b. SAT a -> (a -> SAT b) -> SAT b
Monad, Monad SAT
forall a. IO a -> SAT a
forall (m :: * -> *).
Monad m -> (forall a. IO a -> m a) -> MonadIO m
liftIO :: forall a. IO a -> SAT a
$cliftIO :: forall a. IO a -> SAT a
MonadIO)
type Assignment = M.Map Int Bool
newtype Dec a = Dec (Reader Assignment a)
deriving (forall a b. a -> Dec b -> Dec a
forall a b. (a -> b) -> Dec a -> Dec b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: forall a b. a -> Dec b -> Dec a
$c<$ :: forall a b. a -> Dec b -> Dec a
fmap :: forall a b. (a -> b) -> Dec a -> Dec b
$cfmap :: forall a b. (a -> b) -> Dec a -> Dec b
Functor, Functor Dec
forall a. a -> Dec a
forall a b. Dec a -> Dec b -> Dec a
forall a b. Dec a -> Dec b -> Dec b
forall a b. Dec (a -> b) -> Dec a -> Dec b
forall a b c. (a -> b -> c) -> Dec a -> Dec b -> Dec c
forall (f :: * -> *).
Functor f
-> (forall a. a -> f a)
-> (forall a b. f (a -> b) -> f a -> f b)
-> (forall a b c. (a -> b -> c) -> f a -> f b -> f c)
-> (forall a b. f a -> f b -> f b)
-> (forall a b. f a -> f b -> f a)
-> Applicative f
<* :: forall a b. Dec a -> Dec b -> Dec a
$c<* :: forall a b. Dec a -> Dec b -> Dec a
*> :: forall a b. Dec a -> Dec b -> Dec b
$c*> :: forall a b. Dec a -> Dec b -> Dec b
liftA2 :: forall a b c. (a -> b -> c) -> Dec a -> Dec b -> Dec c
$cliftA2 :: forall a b c. (a -> b -> c) -> Dec a -> Dec b -> Dec c
<*> :: forall a b. Dec (a -> b) -> Dec a -> Dec b
$c<*> :: forall a b. Dec (a -> b) -> Dec a -> Dec b
pure :: forall a. a -> Dec a
$cpure :: forall a. a -> Dec a
Applicative, Applicative Dec
forall a. a -> Dec a
forall a b. Dec a -> Dec b -> Dec b
forall a b. Dec a -> (a -> Dec b) -> Dec b
forall (m :: * -> *).
Applicative m
-> (forall a b. m a -> (a -> m b) -> m b)
-> (forall a b. m a -> m b -> m b)
-> (forall a. a -> m a)
-> Monad m
return :: forall a. a -> Dec a
$creturn :: forall a. a -> Dec a
>> :: forall a b. Dec a -> Dec b -> Dec b
$c>> :: forall a b. Dec a -> Dec b -> Dec b
>>= :: forall a b. Dec a -> (a -> Dec b) -> Dec b
$c>>= :: forall a b. Dec a -> (a -> Dec b) -> Dec b
Monad)
instance MonadSAT SAT where
fresh :: SAT Literal
fresh = forall a. StateT S IO a -> SAT a
SAT forall a b. (a -> b) -> a -> b
$ do
Int
n <- forall s (m :: * -> *) a. MonadState s m => Getting a s a -> m a
use Lens' S Int
next_variable
Lens' S Int
next_variable forall s (m :: * -> *) a b.
MonadState s m =>
ASetter s s a b -> b -> m ()
.= forall a. Enum a => a -> a
succ Int
n
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Bool -> Int -> Literal
literal Bool
True forall a b. (a -> b) -> a -> b
$ forall a. Enum a => a -> Int
fromEnum Int
n
emit :: Clause -> SAT ()
emit Clause
cl = forall a. StateT S IO a -> SAT a
SAT forall a b. (a -> b) -> a -> b
$ do
Handle
h <- forall s (m :: * -> *) a. MonadState s m => Getting a s a -> m a
use Lens' S Handle
solver_input
let s :: ByteString
s = String -> ByteString
BS.pack forall a b. (a -> b) -> a -> b
$ forall a. Show a => a -> String
show Clause
cl
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ Handle -> ByteString -> IO ()
BS.hPutStrLn Handle
h ByteString
s
note :: String -> SAT ()
note String
msg = forall a. StateT S IO a -> SAT a
SAT forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ Handle -> String -> IO ()
hPutStrLn Handle
stderr String
msg
type Decoder SAT = Dec
instance Decode Dec Boolean Bool where
decode :: Boolean -> Dec Bool
decode Boolean
b = case Boolean
b of
Constant Bool
c -> forall (m :: * -> *) a. Monad m => a -> m a
return Bool
c
Boolean Literal
l -> do
Bool
v <- Int -> Dec Bool
dv forall a b. (a -> b) -> a -> b
$ Literal -> Int
variable Literal
l
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ if Literal -> Bool
positive Literal
l then Bool
v else Bool -> Bool
not Bool
v
dv :: Int -> Dec Bool
dv Int
v = forall a. Reader Assignment a -> Dec a
Dec forall a b. (a -> b) -> a -> b
$ do
Assignment
assignment <- forall r (m :: * -> *). MonadReader r m => m r
ask
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ case forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup Int
v Assignment
assignment of
Just Bool
v -> Bool
v
Maybe Bool
Nothing -> forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$ [String] -> String
unwords [ String
"unassigned", String
"variable", forall a. Show a => a -> String
show Int
v ]
solve :: String
-> [String]
-> SAT (Dec a)
-> IO (Maybe a)
solve :: forall a. String -> [String] -> SAT (Dec a) -> IO (Maybe a)
solve String
command [String]
opts (SAT StateT S IO (Dec a)
action) = forall a b c. IO a -> (a -> IO b) -> (a -> IO c) -> IO c
bracket
( do
String -> IO ()
report String
"Satchmo.SAT.External: creating process"
CreateProcess
-> IO (Maybe Handle, Maybe Handle, Maybe Handle, ProcessHandle)
createProcess forall a b. (a -> b) -> a -> b
$ (String -> [String] -> CreateProcess
proc String
command [String]
opts)
{ std_in :: StdStream
std_in = StdStream
CreatePipe
, std_out :: StdStream
std_out = StdStream
CreatePipe
, create_group :: Bool
create_group = Bool
True
} )
( \ (Just Handle
sin, Just Handle
sout, Maybe Handle
_, ProcessHandle
ph) -> do
String -> IO ()
report String
"Satchmo.SAT.External: bracket closing"
ProcessHandle -> IO ()
interruptProcessGroupOf ProcessHandle
ph
)
forall a b. (a -> b) -> a -> b
$ \ (Just Handle
sin, Just Handle
sout, Maybe Handle
_, ProcessHandle
ph) -> do
MVar (Reader Assignment a)
dec <- forall a. IO (MVar a)
newEmptyMVar
String
output <- Handle -> IO String
hGetContents Handle
sout
forall a. IO () -> (IO () -> IO a) -> IO a
withForkWait (forall a. a -> IO a
C.evaluate forall a b. (a -> b) -> a -> b
$ forall a. NFData a => a -> ()
rnf String
output) forall a b. (a -> b) -> a -> b
$ \ IO ()
waitOut ->
IO () -> IO ()
ignoreSigPipe forall a b. (a -> b) -> a -> b
$ do
String -> IO ()
report forall a b. (a -> b) -> a -> b
$ String
"S.S.External: waiter forked"
let s0 :: S
s0 = S { _next_variable :: Int
_next_variable=Int
1, _solver_input :: Handle
_solver_input=Handle
sin}
String -> IO ()
report forall a b. (a -> b) -> a -> b
$ String
"S.S.External: writing output"
Dec Reader Assignment a
decoder <- forall (m :: * -> *) s a. Monad m => StateT s m a -> s -> m a
evalStateT StateT S IO (Dec a)
action S
s0
forall a. MVar a -> a -> IO ()
putMVar MVar (Reader Assignment a)
dec Reader Assignment a
decoder
Handle -> IO ()
hClose Handle
sin
IO ()
waitOut
Handle -> IO ()
hClose Handle
sout
String -> IO ()
report forall a b. (a -> b) -> a -> b
$ String
"S.S.External: waiter done"
String -> IO ()
report String
"Satchmo.SAT.External: start waiting"
ProcessHandle -> IO ExitCode
waitForProcess ProcessHandle
ph
Reader Assignment a
decoder <- forall a. MVar a -> IO a
takeMVar MVar (Reader Assignment a)
dec
String -> IO ()
report String
"Satchmo.SAT.External: waiting done"
let vlines :: [String]
vlines = do
String
line <- String -> [String]
lines String
output
forall (f :: * -> *). Alternative f => Bool -> f ()
guard forall a b. (a -> b) -> a -> b
$ forall a. Eq a => [a] -> [a] -> Bool
isPrefixOf String
"v" String
line
forall (m :: * -> *) a. Monad m => a -> m a
return String
line
String -> IO ()
report forall a b. (a -> b) -> a -> b
$ forall a. Show a => a -> String
show [String]
vlines
let vs :: [Int]
vs = do
String
line <- [String]
vlines
String
w <- forall a. [a] -> [a]
tail forall a b. (a -> b) -> a -> b
$ String -> [String]
words String
line
forall (m :: * -> *) a. Monad m => a -> m a
return (forall a. Read a => String -> a
read String
w :: Int)
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ do
forall (f :: * -> *). Alternative f => Bool -> f ()
guard forall a b. (a -> b) -> a -> b
$ Bool -> Bool
not forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a. Foldable t => t a -> Bool
null [String]
vlines
let m :: Assignment
m = forall k a. Ord k => [(k, a)] -> Map k a
M.fromList forall a b. (a -> b) -> a -> b
$ do
Int
v <- [Int]
vs ; forall (f :: * -> *). Alternative f => Bool -> f ()
guard forall a b. (a -> b) -> a -> b
$ Int
v forall a. Eq a => a -> a -> Bool
/= Int
0 ; forall (m :: * -> *) a. Monad m => a -> m a
return (forall a. Num a => a -> a
abs Int
v, Int
vforall a. Ord a => a -> a -> Bool
>Int
0)
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall r a. Reader r a -> r -> a
runReader Reader Assignment a
decoder Assignment
m
withForkWait :: IO () -> (IO () -> IO a) -> IO a
withForkWait :: forall a. IO () -> (IO () -> IO a) -> IO a
withForkWait IO ()
async IO () -> IO a
body = do
MVar (Either SomeException ())
waitVar <- forall a. IO (MVar a)
newEmptyMVar :: IO (MVar (Either SomeException ()))
forall b. ((forall a. IO a -> IO a) -> IO b) -> IO b
mask forall a b. (a -> b) -> a -> b
$ \forall a. IO a -> IO a
restore -> do
ThreadId
tid <- IO () -> IO ThreadId
forkIO forall a b. (a -> b) -> a -> b
$ forall e a. Exception e => IO a -> IO (Either e a)
try (forall a. IO a -> IO a
restore IO ()
async) forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall a. MVar a -> a -> IO ()
putMVar MVar (Either SomeException ())
waitVar
let wait :: IO ()
wait = forall a. MVar a -> IO a
takeMVar MVar (Either SomeException ())
waitVar forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either forall e a. Exception e => e -> IO a
throwIO forall (m :: * -> *) a. Monad m => a -> m a
return
forall a. IO a -> IO a
restore (IO () -> IO a
body IO ()
wait) forall a b. IO a -> IO b -> IO a
`C.onException` ThreadId -> IO ()
killThread ThreadId
tid
ignoreSigPipe :: IO () -> IO ()
ignoreSigPipe :: IO () -> IO ()
ignoreSigPipe = forall e a. Exception e => (e -> IO a) -> IO a -> IO a
C.handle forall a b. (a -> b) -> a -> b
$ \IOException
e -> case IOException
e of
IOError { ioe_type :: IOException -> IOErrorType
ioe_type = IOErrorType
ResourceVanished
, ioe_errno :: IOException -> Maybe CInt
ioe_errno = Just CInt
ioe }
| CInt -> Errno
Errno CInt
ioe forall a. Eq a => a -> a -> Bool
== Errno
ePIPE -> forall (m :: * -> *) a. Monad m => a -> m a
return ()
IOException
_ -> forall e a. Exception e => e -> IO a
throwIO IOException
e