{-# 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.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
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
}
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
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}