{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE TypeSynonymInstances, FlexibleInstances, FlexibleContexts #-}

module Satchmo.SAT.Tmpfile

( SAT, Header(..)
, fresh, fresh_forall
, emit, Weight
, sat
)

where

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

import Control.Exception
import Control.Monad
import Control.Monad.Fix
import Control.Monad.RWS.Strict
import Control.Applicative
import qualified  Data.Set as Set

-- import qualified Data.ByteString.Lazy.Char8 as BS
import qualified Data.ByteString.Char8 as BS

import System.Directory
import System.Environment
import System.IO

import qualified Data.Map as M

import Data.List ( sortBy )
import Data.Ord ( comparing )
import Data.Array
import Control.Monad.Reader

instance Decode (Reader (Array Variable Bool)) Boolean Bool where
    decode :: Boolean -> Reader (Array Variable Bool) Bool
decode Boolean
b = case Boolean
b of
        Constant Bool
c -> Bool -> Reader (Array Variable Bool) Bool
forall a. a -> ReaderT (Array Variable Bool) Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
c
        Boolean Literal
l -> (Array Variable Bool -> Bool) -> Reader (Array Variable Bool) Bool
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks ((Array Variable Bool -> Bool)
 -> Reader (Array Variable Bool) Bool)
-> (Array Variable Bool -> Bool)
-> Reader (Array Variable Bool) Bool
forall a b. (a -> b) -> a -> b
$ \ Array Variable Bool
arr -> Literal -> Bool
positive Literal
l Bool -> Bool -> Bool
forall a. Eq a => a -> a -> Bool
== Array Variable Bool
arr Array Variable Bool -> Variable -> Bool
forall i e. Ix i => Array i e -> i -> e
! Literal -> Variable
variable Literal
l 

instance MonadSAT SAT where
  fresh :: SAT Literal
fresh = do
    Accu
a <- SAT Accu
forall s (m :: * -> *). MonadState s m => m s
get
    let n :: Variable
n = Accu -> Variable
next Accu
a
    Accu -> SAT ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put (Accu -> SAT ()) -> Accu -> SAT ()
forall a b. (a -> b) -> a -> b
$ Accu
a { next = n + 1 }
    Literal -> SAT Literal
forall a. a -> SAT a
forall (m :: * -> *) a. Monad m => a -> m a
return (Literal -> SAT Literal) -> Literal -> SAT Literal
forall a b. (a -> b) -> a -> b
$ Bool -> Variable -> Literal
literal Bool
True Variable
n
  emit :: Clause -> SAT ()
emit Clause
clause = do
    Handle
h <- SAT Handle
forall r (m :: * -> *). MonadReader r m => m r
ask 
    IO () -> SAT ()
forall a. IO a -> SAT a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> SAT ()) -> IO () -> SAT ()
forall a b. (a -> b) -> a -> b
$ Handle -> String -> IO ()
hPutStrLn Handle
h (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ Clause -> String
forall a. Show a => a -> String
show Clause
clause
    Accu
a <- SAT Accu
forall s (m :: * -> *). MonadState s m => m s
get
    -- bshowClause c = BS.pack (show c) `mappend` BS.pack "\n"
    -- tellSat (bshowClause clause)
    Accu -> SAT ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put (Accu -> SAT ()) -> Accu -> SAT ()
forall a b. (a -> b) -> a -> b
$ Accu
a
        { size = size a + 1
        , census = M.insertWith (+) (length $ literals clause) 1 $ census a 
        }
  -- emitW _ _ = return ()

  note :: String -> SAT ()
note String
msg = do Accu
a <- SAT Accu
forall s (m :: * -> *). MonadState s m => m s
get ; Accu -> SAT ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put (Accu -> SAT ()) -> Accu -> SAT ()
forall a b. (a -> b) -> a -> b
$ Accu
a { notes = msg : notes a }

  type Decoder SAT = Reader (Array Int Bool) 
  decode_variable :: Variable -> Decoder SAT Bool
decode_variable Variable
v | Variable
v Variable -> Variable -> Bool
forall a. Ord a => a -> a -> Bool
> Variable
0 = (Array Variable Bool -> Bool) -> Decoder SAT Bool
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks ((Array Variable Bool -> Bool) -> Decoder SAT Bool)
-> (Array Variable Bool -> Bool) -> Decoder SAT Bool
forall a b. (a -> b) -> a -> b
$ \ Array Variable Bool
arr ->  Array Variable Bool
arr Array Variable Bool -> Variable -> Bool
forall i e. Ix i => Array i e -> i -> e
! Variable
v

{-
    readsPrec p = \ cs -> do
        ( i, cs') <- readsPrec p cs
        return ( Literal i , cs' )
-}


-- ---------------
-- Implementation
-- ---------------

data Accu = Accu
          { Accu -> Variable
next :: !Int
          , Accu -> [Variable]
universal :: [Int]
          , Accu -> Variable
size :: !Int
          , Accu -> [String]
notes :: ![ String ]
          , Accu -> Map Variable Variable
census :: !( M.Map Int Int )
          }

start :: Accu
start :: Accu
start = Accu
      { next :: Variable
next = Variable
1
      , universal :: [Variable]
universal = []
      , size :: Variable
size = Variable
0
      , notes :: [String]
notes = [ String
"Satchmo.SAT.Tmpfile implementation" ]
      , census :: Map Variable Variable
census = Map Variable Variable
forall k a. Map k a
M.empty          
      }

newtype SAT a = SAT {forall a. SAT a -> RWST Handle () Accu IO a
unsat::RWST Handle () Accu IO a}
    deriving (MonadState Accu, MonadReader Handle, Applicative SAT
Applicative SAT =>
(forall a b. SAT a -> (a -> SAT b) -> SAT b)
-> (forall a b. SAT a -> SAT b -> SAT b)
-> (forall a. a -> SAT a)
-> Monad 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
$c>>= :: forall a b. SAT a -> (a -> SAT b) -> SAT b
>>= :: forall a b. SAT a -> (a -> SAT b) -> SAT b
$c>> :: forall a b. SAT a -> SAT b -> SAT b
>> :: forall a b. SAT a -> SAT b -> SAT b
$creturn :: forall a. a -> SAT a
return :: forall a. a -> SAT a
Monad, Monad SAT
Monad SAT => (forall a. IO a -> SAT a) -> MonadIO SAT
forall a. IO a -> SAT a
forall (m :: * -> *).
Monad m =>
(forall a. IO a -> m a) -> MonadIO m
$cliftIO :: forall a. IO a -> SAT a
liftIO :: forall a. IO a -> SAT a
MonadIO, (forall a b. (a -> b) -> SAT a -> SAT b)
-> (forall a b. a -> SAT b -> SAT a) -> Functor SAT
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
$cfmap :: forall a b. (a -> b) -> SAT a -> SAT b
fmap :: forall a b. (a -> b) -> SAT a -> SAT b
$c<$ :: forall a b. a -> SAT b -> SAT a
<$ :: forall a b. a -> SAT b -> SAT a
Functor, Functor SAT
Functor SAT =>
(forall a. a -> SAT a)
-> (forall a b. SAT (a -> b) -> SAT a -> SAT b)
-> (forall a b c. (a -> b -> c) -> SAT a -> SAT b -> SAT c)
-> (forall a b. SAT a -> SAT b -> SAT b)
-> (forall a b. SAT a -> SAT b -> SAT a)
-> Applicative 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
$cpure :: forall a. a -> SAT a
pure :: forall a. a -> SAT a
$c<*> :: forall a b. SAT (a -> b) -> SAT a -> SAT b
<*> :: forall a b. SAT (a -> b) -> SAT a -> SAT b
$cliftA2 :: forall a b c. (a -> b -> c) -> SAT a -> SAT b -> SAT c
liftA2 :: forall a b c. (a -> b -> c) -> SAT a -> SAT b -> SAT c
$c*> :: forall a b. SAT a -> SAT b -> SAT b
*> :: forall a b. SAT a -> SAT b -> SAT b
$c<* :: forall a b. SAT a -> SAT b -> SAT a
<* :: forall a b. SAT a -> SAT b -> SAT a
Applicative, Monad SAT
Monad SAT => (forall a. (a -> SAT a) -> SAT a) -> MonadFix SAT
forall a. (a -> SAT a) -> SAT a
forall (m :: * -> *).
Monad m =>
(forall a. (a -> m a) -> m a) -> MonadFix m
$cmfix :: forall a. (a -> SAT a) -> SAT a
mfix :: forall a. (a -> SAT a) -> SAT a
MonadFix)


sat :: SAT a -> IO (BS.ByteString, Header, a )
sat :: forall a. SAT a -> IO (ByteString, Header, a)
sat (SAT RWST Handle () Accu IO a
m) =
 IO (String, Handle)
-> ((String, Handle) -> IO ())
-> ((String, Handle) -> IO (ByteString, Header, a))
-> IO (ByteString, Header, a)
forall a b c. IO a -> (a -> IO b) -> (a -> IO c) -> IO c
bracket
    (IO String
getTemporaryDirectory IO String -> (String -> IO (String, Handle)) -> IO (String, Handle)
forall a b. IO a -> (a -> IO b) -> IO b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= (String -> String -> IO (String, Handle)
`openTempFile`  String
"satchmo"))
    (\(String
fp, Handle
h) -> String -> IO ()
removeFile String
fp)
    (\(String
fp, Handle
h) -> do
       Handle -> BufferMode -> IO ()
hSetBuffering Handle
h (Maybe Variable -> BufferMode
BlockBuffering Maybe Variable
forall a. Maybe a
Nothing)
       ~(a
a, Accu
accu, ()
_) <- RWST Handle () Accu IO a -> Handle -> Accu -> IO (a, Accu, ())
forall r w s (m :: * -> *) a.
RWST r w s m a -> r -> s -> m (a, s, w)
runRWST RWST Handle () Accu IO a
m Handle
h Accu
start
       Handle -> IO ()
hClose Handle
h
       
       [String] -> (String -> IO ()) -> IO [()]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM ( [String] -> [String]
forall a. [a] -> [a]
reverse ([String] -> [String]) -> [String] -> [String]
forall a b. (a -> b) -> a -> b
$ Accu -> [String]
notes Accu
accu ) ((String -> IO ()) -> IO [()]) -> (String -> IO ()) -> IO [()]
forall a b. (a -> b) -> a -> b
$ Handle -> String -> IO ()
hPutStrLn Handle
stderr 
       Handle -> String -> IO ()
hPutStrLn Handle
stderr (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ [String] -> String
unlines 
           [ String
"(clause length, frequency)"
           , [(Variable, Variable)] -> String
forall a. Show a => a -> String
show ([(Variable, Variable)] -> String)
-> [(Variable, Variable)] -> String
forall a b. (a -> b) -> a -> b
$ ((Variable, Variable) -> (Variable, Variable) -> Ordering)
-> [(Variable, Variable)] -> [(Variable, Variable)]
forall a. (a -> a -> Ordering) -> [a] -> [a]
sortBy ( ((Variable, Variable) -> Variable)
-> (Variable, Variable) -> (Variable, Variable) -> Ordering
forall a b. Ord a => (b -> a) -> b -> b -> Ordering
comparing ( Variable -> Variable
forall a. Num a => a -> a
negate (Variable -> Variable)
-> ((Variable, Variable) -> Variable)
-> (Variable, Variable)
-> Variable
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Variable, Variable) -> Variable
forall a b. (a, b) -> b
snd )) 
                        ([(Variable, Variable)] -> [(Variable, Variable)])
-> [(Variable, Variable)] -> [(Variable, Variable)]
forall a b. (a -> b) -> a -> b
$ Map Variable Variable -> [(Variable, Variable)]
forall k a. Map k a -> [(k, a)]
M.toList (Map Variable Variable -> [(Variable, Variable)])
-> Map Variable Variable -> [(Variable, Variable)]
forall a b. (a -> b) -> a -> b
$ Accu -> Map Variable Variable
census Accu
accu
           ]  
       
       let header :: Header
header = Variable -> Variable -> [Variable] -> Header
Header (Accu -> Variable
size Accu
accu) (Accu -> Variable
next Accu
accu Variable -> Variable -> Variable
forall a. Num a => a -> a -> a
- Variable
1) [Variable]
universals
           universals :: [Variable]
universals = [Variable] -> [Variable]
forall a. [a] -> [a]
reverse ([Variable] -> [Variable]) -> [Variable] -> [Variable]
forall a b. (a -> b) -> a -> b
$ Accu -> [Variable]
universal Accu
accu

       ByteString
bs <- String -> IO ByteString
BS.readFile String
fp
       (ByteString, Header, a) -> IO (ByteString, Header, a)
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (ByteString
bs, Header
header, a
a))



tellSat :: ByteString -> m ()
tellSat ByteString
x = do {Handle
h <- m Handle
forall r (m :: * -> *). MonadReader r m => m r
ask; IO () -> m ()
forall a. IO a -> m a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> m ()) -> IO () -> m ()
forall a b. (a -> b) -> a -> b
$ Handle -> ByteString -> IO ()
BS.hPut Handle
h ByteString
x}