{-# 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.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 -> forall (m :: * -> *) a. Monad m => a -> m a
return Bool
c
        Boolean Literal
l -> forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks forall a b. (a -> b) -> a -> b
$ \ Array Variable Bool
arr -> Literal -> Bool
positive Literal
l forall a. Eq a => a -> a -> Bool
== Array Variable Bool
arr 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 <- forall s (m :: * -> *). MonadState s m => m s
get
    let n :: Variable
n = Accu -> Variable
next Accu
a
    forall s (m :: * -> *). MonadState s m => s -> m ()
put forall a b. (a -> b) -> a -> b
$ Accu
a { next :: Variable
next = Variable
n forall a. Num a => a -> a -> a
+ Variable
1 }
    forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Bool -> Variable -> Literal
literal Bool
True Variable
n
  emit :: Clause -> SAT ()
emit Clause
clause = do
    Handle
h <- forall r (m :: * -> *). MonadReader r m => m r
ask 
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ Handle -> String -> IO ()
hPutStrLn Handle
h forall a b. (a -> b) -> a -> b
$ forall a. Show a => a -> String
show Clause
clause
    Accu
a <- forall s (m :: * -> *). MonadState s m => m s
get
    -- bshowClause c = BS.pack (show c) `mappend` BS.pack "\n"
    -- tellSat (bshowClause clause)
    forall s (m :: * -> *). MonadState s m => s -> m ()
put forall a b. (a -> b) -> a -> b
$ Accu
a
        { size :: Variable
size = Accu -> Variable
size Accu
a forall a. Num a => a -> a -> a
+ Variable
1
        , census :: Map Variable Variable
census = forall k a. Ord k => (a -> a -> a) -> k -> a -> Map k a -> Map k a
M.insertWith forall a. Num a => a -> a -> a
(+) (forall (t :: * -> *) a. Foldable t => t a -> Variable
length forall a b. (a -> b) -> a -> b
$ Clause -> [Literal]
literals Clause
clause) Variable
1 forall a b. (a -> b) -> a -> b
$ Accu -> Map Variable Variable
census Accu
a 
        }
  -- emitW _ _ = return ()

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

  type Decoder SAT = Reader (Array Int Bool) 
  decode_variable :: Variable -> Decoder SAT Bool
decode_variable Variable
v | Variable
v forall a. Ord a => a -> a -> Bool
> Variable
0 = forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks forall a b. (a -> b) -> a -> b
$ \ Array Variable Bool
arr ->  Array Variable Bool
arr 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 = 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
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, 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, Monad SAT
forall a. (a -> SAT a) -> SAT a
forall (m :: * -> *).
Monad m -> (forall a. (a -> m a) -> m a) -> MonadFix m
mfix :: forall a. (a -> SAT a) -> SAT a
$cmfix :: 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) =
 forall a b c. IO a -> (a -> IO b) -> (a -> IO c) -> IO c
bracket
    (IO String
getTemporaryDirectory 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 forall a. Maybe a
Nothing)
       ~(a
a, Accu
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
       
       forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM ( forall a. [a] -> [a]
reverse forall a b. (a -> b) -> a -> b
$ Accu -> [String]
notes Accu
accu ) forall a b. (a -> b) -> a -> b
$ Handle -> String -> IO ()
hPutStrLn Handle
stderr 
       Handle -> String -> IO ()
hPutStrLn Handle
stderr forall a b. (a -> b) -> a -> b
$ [String] -> String
unlines 
           [ String
"(clause length, frequency)"
           , forall a. Show a => a -> String
show forall a b. (a -> b) -> a -> b
$ forall a. (a -> a -> Ordering) -> [a] -> [a]
sortBy ( forall a b. Ord a => (b -> a) -> b -> b -> Ordering
comparing ( forall a. Num a => a -> a
negate forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> b
snd )) 
                        forall a b. (a -> b) -> a -> b
$ forall k a. Map k a -> [(k, a)]
M.toList 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 forall a. Num a => a -> a -> a
- Variable
1) [Variable]
universals
           universals :: [Variable]
universals = forall a. [a] -> [a]
reverse forall a b. (a -> b) -> a -> b
$ Accu -> [Variable]
universal Accu
accu

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



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