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


module Satchmo.SAT.Mini 

( SAT
, fresh
, emit
, SolveOptions(..)
, defaultSolveOptions
, solve
, solveSilently
, solveWith
, solve_with_timeout
)

where

import qualified MiniSat as API

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

import Control.Concurrent
import Control.Concurrent.MVar
import Control.Exception
import Control.Monad ( when )
import Control.Monad.Fix
import Control.Monad.IO.Class
import Control.Applicative
import System.IO

import Control.Concurrent.Async

deriving instance Enum API.Lit

newtype SAT a 
      = SAT { forall a. SAT a -> Solver -> IO a
unSAT :: API.Solver -> IO a
            } 

instance Functor SAT where
    fmap :: forall a b. (a -> b) -> SAT a -> SAT b
fmap a -> b
f ( SAT Solver -> IO a
m ) = forall a. (Solver -> IO a) -> SAT a
SAT forall a b. (a -> b) -> a -> b
$ \ Solver
s -> forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> b
f ( Solver -> IO a
m Solver
s )

instance Monad SAT where
    return :: forall a. a -> SAT a
return a
x = forall a. (Solver -> IO a) -> SAT a
SAT forall a b. (a -> b) -> a -> b
$ \ Solver
s -> forall (m :: * -> *) a. Monad m => a -> m a
return a
x
    SAT Solver -> IO a
m >>= :: forall a b. SAT a -> (a -> SAT b) -> SAT b
>>= a -> SAT b
f = forall a. (Solver -> IO a) -> SAT a
SAT forall a b. (a -> b) -> a -> b
$ \ Solver
s -> do 
        a
x <- Solver -> IO a
m Solver
s ; let { SAT Solver -> IO b
n = a -> SAT b
f a
x } ; Solver -> IO b
n Solver
s

-- | need this for hashtables
instance MonadIO SAT where
  liftIO :: forall a. IO a -> SAT a
liftIO IO a
comp = forall a. (Solver -> IO a) -> SAT a
SAT forall a b. (a -> b) -> a -> b
$ \ Solver
s -> IO a
comp

instance Applicative SAT where
    pure :: forall a. a -> SAT a
pure = forall (m :: * -> *) a. Monad m => a -> m a
return
    SAT (a -> b)
a <*> :: forall a b. SAT (a -> b) -> SAT a -> SAT b
<*> SAT a
b = SAT (a -> b)
a forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \ a -> b
f -> forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> b
f SAT a
b

instance MonadFix SAT where
    mfix :: forall a. (a -> SAT a) -> SAT a
mfix a -> SAT a
f = forall a. (Solver -> IO a) -> SAT a
SAT forall a b. (a -> b) -> a -> b
$ \ Solver
s -> forall (m :: * -> *) a. MonadFix m => (a -> m a) -> m a
mfix ( \ a
a -> forall a. SAT a -> Solver -> IO a
unSAT (a -> SAT a
f a
a) Solver
s )

instance MonadSAT SAT where
  fresh :: SAT Literal
fresh = forall a. (Solver -> IO a) -> SAT a
SAT forall a b. (a -> b) -> a -> b
$ \ Solver
s -> do 
      Lit
x <- Solver -> IO Lit
API.newLit Solver
s
      let l :: Literal
l = Bool -> Int -> Literal
literal Bool
True forall a b. (a -> b) -> a -> b
$ forall a. Enum a => a -> Int
fromEnum Lit
x
      -- hPutStrLn stderr $ "fresh: " ++ show (x, l)
      forall (m :: * -> *) a. Monad m => a -> m a
return Literal
l

  emit :: Clause -> SAT ()
emit Clause
cl = forall a. (Solver -> IO a) -> SAT a
SAT forall a b. (a -> b) -> a -> b
$ \ Solver
s -> do
      let conv :: Literal -> Lit
conv Literal
l = ( if Literal -> Bool
positive Literal
l then forall a. a -> a
id else Lit -> Lit
API.neg ) 
                 forall a b. (a -> b) -> a -> b
$ forall a. Enum a => Int -> a
toEnum
                 forall a b. (a -> b) -> a -> b
$ Literal -> Int
variable Literal
l
          apicl :: [Lit]
apicl = forall a b. (a -> b) -> [a] -> [b]
map Literal -> Lit
conv forall a b. (a -> b) -> a -> b
$ Clause -> [Literal]
literals Clause
cl
      Bool
res <- Solver -> [Lit] -> IO Bool
API.addClause Solver
s [Lit]
apicl
      -- hPutStrLn stderr $ "adding clause " ++ show (cl, apicl, res)
      forall (m :: * -> *) a. Monad m => a -> m a
return ()

  note :: String -> SAT ()
note String
msg = forall a. (Solver -> IO a) -> SAT a
SAT forall a b. (a -> b) -> a -> b
$ \ Solver
s -> Handle -> String -> IO ()
hPutStrLn Handle
stderr String
msg

  type Decoder SAT = SAT 
  decode_variable :: Int -> Decoder SAT Bool
decode_variable Int
v = forall a. (Solver -> IO a) -> SAT a
SAT forall a b. (a -> b) -> a -> b
$ \ Solver
s -> do
      Just Bool
val <- Solver -> Lit -> IO (Maybe Bool)
API.modelValue Solver
s forall a b. (a -> b) -> a -> b
$ forall a. Enum a => Int -> a
toEnum forall a b. (a -> b) -> a -> b
$ forall a. Enum a => a -> Int
fromEnum Int
v
      forall (m :: * -> *) a. Monad m => a -> m a
return Bool
val 
      
instance Decode SAT Boolean Bool where
    decode :: Boolean -> SAT 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 
            let dv :: a -> SAT Bool
dv a
v = forall a. (Solver -> IO a) -> SAT a
SAT forall a b. (a -> b) -> a -> b
$ \ Solver
s -> do
                    Just Bool
val <- Solver -> Lit -> IO (Maybe Bool)
API.modelValue Solver
s forall a b. (a -> b) -> a -> b
$ forall a. Enum a => Int -> a
toEnum forall a b. (a -> b) -> a -> b
$ forall a. Enum a => a -> Int
fromEnum a
v
                    forall (m :: * -> *) a. Monad m => a -> m a
return Bool
val 
            Bool
v <- forall {a}. Enum a => a -> SAT 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

newtype SolveOptions = SolveOptions {
        SolveOptions -> Bool
verboseOutput :: Bool
    }

defaultSolveOptions :: SolveOptions
defaultSolveOptions :: SolveOptions
defaultSolveOptions = SolveOptions {verboseOutput :: Bool
verboseOutput = Bool
True}

solve_with_timeout :: Maybe Int -> SAT (SAT a) -> IO (Maybe a)
solve_with_timeout :: forall a. Maybe Int -> SAT (SAT a) -> IO (Maybe a)
solve_with_timeout Maybe Int
mto SAT (SAT a)
action = do
    MVar (Maybe a)
accu <- forall a. IO (MVar a)
newEmptyMVar 
    ThreadId
worker <- IO () -> IO ThreadId
forkIO forall a b. (a -> b) -> a -> b
$ do Maybe a
res <- forall a. SAT (SAT a) -> IO (Maybe a)
solve SAT (SAT a)
action ; forall a. MVar a -> a -> IO ()
putMVar MVar (Maybe a)
accu Maybe a
res
    ThreadId
timer <- IO () -> IO ThreadId
forkIO forall a b. (a -> b) -> a -> b
$ case Maybe Int
mto of
        Just Int
to -> do 
              Int -> IO ()
threadDelay ( Int
10forall a b. (Num a, Integral b) => a -> b -> a
^Integer
6 forall a. Num a => a -> a -> a
* Int
to ) 
              ThreadId -> IO ()
killThread ThreadId
worker 
              forall a. MVar a -> a -> IO ()
putMVar MVar (Maybe a)
accu forall a. Maybe a
Nothing
        Maybe Int
_  -> forall (m :: * -> *) a. Monad m => a -> m a
return ()
    forall a. MVar a -> IO a
takeMVar MVar (Maybe a)
accu forall e a. Exception e => IO a -> (e -> IO a) -> IO a
`Control.Exception.catch` \ ( AsyncException
_ :: AsyncException ) -> do
        Handle -> String -> IO ()
hPutStrLn Handle
stderr String
"caught"
        ThreadId -> IO ()
killThread ThreadId
worker
        ThreadId -> IO ()
killThread ThreadId
timer
        forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Maybe a
Nothing

solve :: SAT (SAT a) -> IO (Maybe a)
solve :: forall a. SAT (SAT a) -> IO (Maybe a)
solve = forall a. SolveOptions -> SAT (SAT a) -> IO (Maybe a)
solveWith SolveOptions
defaultSolveOptions

solveSilently :: SAT (SAT a) -> IO (Maybe a)
solveSilently :: forall a. SAT (SAT a) -> IO (Maybe a)
solveSilently = forall a. SolveOptions -> SAT (SAT a) -> IO (Maybe a)
solveWith SolveOptions
defaultSolveOptions{verboseOutput :: Bool
verboseOutput = Bool
False}

solveWith :: SolveOptions -> SAT (SAT a) -> IO (Maybe a)
solveWith :: forall a. SolveOptions -> SAT (SAT a) -> IO (Maybe a)
solveWith SolveOptions
options SAT (SAT a)
action = forall {c}. (Solver -> IO c) -> IO c
withNewSolverAsync forall a b. (a -> b) -> a -> b
$ \ Solver
s -> do
    let printIfVerbose :: String -> IO ()
printIfVerbose = forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (SolveOptions -> Bool
verboseOutput SolveOptions
options) forall b c a. (b -> c) -> (a -> b) -> a -> c
. Handle -> String -> IO ()
hPutStrLn Handle
stderr
    String -> IO ()
printIfVerbose String
"start producing CNF"
    SAT Solver -> IO a
decoder <- forall a. SAT a -> Solver -> IO a
unSAT SAT (SAT a)
action Solver
s
    Int
v <- Solver -> IO Int
API.minisat_num_vars Solver
s
    Int
c <- Solver -> IO Int
API.minisat_num_clauses Solver
s
    String -> IO ()
printIfVerbose forall a b. (a -> b) -> a -> b
$ [String] -> String
unwords [ String
"CNF finished", String
"vars", forall a. Show a => a -> String
show Int
v, String
"clauses", forall a. Show a => a -> String
show Int
c ]
    String -> IO ()
printIfVerbose String
"starting solver"
    LBool
status <- Solver -> [Lit] -> IO LBool
API.limited_solve Solver
s []
    String -> IO ()
printIfVerbose forall a b. (a -> b) -> a -> b
$ String
"solver finished, result: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show LBool
status
    if LBool
status forall a. Eq a => a -> a -> Bool
== LBool
API.l_True then do
        String -> IO ()
printIfVerbose String
"starting decoder"    
        a
out <- Solver -> IO a
decoder Solver
s
        String -> IO ()
printIfVerbose String
"decoder finished"    
        forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a
Just a
out
    else forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Maybe a
Nothing


withNewSolverAsync :: (Solver -> IO c) -> IO c
withNewSolverAsync Solver -> IO c
h =
  forall a b c. IO a -> (a -> IO b) -> (a -> IO c) -> IO c
bracket IO Solver
newSolver Solver -> IO ()
API.deleteSolver forall a b. (a -> b) -> a -> b
$ \  Solver
s -> do
    forall a. IO a -> IO a
mask_ forall a b. (a -> b) -> a -> b
$ forall a b. IO a -> (Async a -> IO b) -> IO b
withAsync (Solver -> IO c
h Solver
s) forall a b. (a -> b) -> a -> b
$ \ Async c
a -> do
      forall a. Async a -> IO a
wait Async c
a forall a b. IO a -> IO b -> IO a
`onException` Solver -> IO ()
API.minisat_interrupt Solver
s

newSolver :: IO Solver
newSolver =
  do Solver
s <- IO Solver
API.minisat_new
     -- https://github.com/niklasso/minisat-haskell-bindings/issues/6
     -- eliminate s True 
     forall (m :: * -> *) a. Monad m => a -> m a
return Solver
s