{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE DoAndIfThenElse #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# language TemplateHaskell #-}

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

module Satchmo.SAT.External

( SAT
, fresh
, emit
, solve
-- , solve_with_timeout
)

where

import Satchmo.Data
import Satchmo.Boolean hiding ( not )
import Satchmo.Code
-- import Satchmo.MonadSAT

import Control.Monad.Reader
import Control.Monad.State
-- import Control.Monad.IO.Class
import System.IO
import Control.Lens
import Control.Applicative

import Control.Concurrent
import Control.DeepSeq (rnf)

import Foreign.C
-- import System.Exit (ExitCode(..))
import System.Process
-- import System.IO.Error
-- import System.Posix.Types
import Control.Exception
import GHC.IO.Exception ( IOErrorType(..), IOException(..) )
-- import System.Posix.Signals

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
      -- liftIO $ BS.putStrLn s
      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  -- ^ command, e.g., glucose
      -> [String] -- ^ options, e.g., -model
      -> SAT (Dec a) -- ^ action that builds the formula and returns the decoder
      -> 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

       -- fork off a thread to start consuming the output
       String
output  <- Handle -> IO String
hGetContents Handle
sout -- lazy IO
       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

-- * code from System.Process 
-- http://hackage.haskell.org/package/process-1.2.3.0/docs/src/System-Process.html#readProcess
-- but they are not exporting withForkWait, so I have to copy it

-- | Fork a thread while doing something else, but kill it if there's an
-- exception.
--
-- This is important in the cases above because we want to kill the thread
-- that is holding the Handle lock, because when we clean up the process we
-- try to close that handle, which could otherwise deadlock.
--
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