satchmo 1.8.1 → 1.9.1

raw patch · 17 files changed

+431/−136 lines, 17 filesPVP ok

version bump matches the API change (PVP)

API changes (from Hackage documentation)

Files

• Satchmo/Binary/Op/Common.hs +54/−11
• Satchmo/Boolean/Data.hs +25/−9
• Satchmo/Boolean/Op.hs +9/−0
• Satchmo/Code.hs +5/−5
• Satchmo/Data.hs +4/−1
• Satchmo/MonadSAT.hs +13/−0
• Satchmo/Relation/Data.hs +4/−1
• Satchmo/Relation/Op.hs +5/−0
• Satchmo/Relation/Prop.hs +8/−0
• Satchmo/SAT.hs +8/−100
• Satchmo/SAT/BS.hs +67/−0
• Satchmo/SAT/Seq.hs +70/−0
• Satchmo/SAT/Sequence.hs +26/−0
• Satchmo/SAT/Tmpfile.hs +116/−0
• Satchmo/SAT/Weighted.hs +3/−2
• Satchmo/Solve.hs +8/−6
• satchmo.cabal +6/−1

@@ -17,6 +17,8 @@  import Satchmo.Counting +import Control.Monad ( forM )+ iszero :: (MonadSAT m) =>  Number -> m Boolean iszero a = equals a $ make [] @@ -26,13 +28,12 @@   equals' :: (MonadSAT m) =>  Booleans -> Booleans -> m Boolean-equals' [] [] = B.constant True-equals' (x:xs) (y:ys) = do-    z <- xor [x, y]-    rest <- equals' xs ys-    and [ not z, rest ]-equals' xs [] = and $ map not xs-equals' [] ys = and $ map not ys+equals' xs ys = do+    let n = min ( length xs ) ( length ys )+        (a,b) = splitAt n xs+        (c,d) = splitAt n ys+    ac <- forM ( zip a c ) $ \ (x,y) -> fun2 (==) x y+    and $ map not (b++d) ++ ac  le,lt,ge,gt,eq :: MonadSAT m => Number -> Number -> m Boolean le x y = do (l,e) <- compare x y ; or [l,e]@@ -71,9 +72,35 @@  full_adder :: (MonadSAT m)             => Boolean -> Boolean -> Boolean-           -> m ( Boolean, Boolean )-full_adder p1 p2 p3 = do+           -> m ( Boolean , Boolean ) -- ^ (result, carry)+full_adder = full_adder_1++full_adder_1 p1 p2 p3 = do     p4 <- boolean ; p5 <- boolean+    assert [not p1, not p2, p5]+    assert [not p1, not p3, p5]+    assert [not p1, p4, p5]+    assert [p1, p2, not p5]+    assert [p1, p3, not p5]+    assert [p1, not p4, not p5]+    assert [not p2, not p3, p5]+    assert [not p2, p4, p5]+    assert [p2, p3, not p5]+    assert [p2, not p4, not p5]+    assert [not p3, p4, p5]+    assert [p3, not p4, not p5]+    assert [not p1, not p2, not p3, p4]+    assert [not p1, not p2, p3, not p4]+    assert [not p1, p2, not p3, not p4]+    assert [not p1, p2, p3, p4]+    assert [p1, not p2, not p3, not p4]+    assert [p1, not p2, p3, p4]+    assert [p1, p2, not p3, p4]+    assert [p1, p2, p3, not p4]+    return ( p4, p5 )+       +full_adder_0 p1 p2 p3 = do+    p4 <- boolean ; p5 <- boolean     assert [not p2,p4,p5]     assert [p2,not p4,not p5]     assert [not p1,not p3,p5]@@ -94,8 +121,24 @@  half_adder :: (MonadSAT m)             => Boolean -> Boolean -           -> m ( Boolean, Boolean )-half_adder p1 p2 = do+           -> m ( Boolean, Boolean ) -- ^ (result, carry)+half_adder = half_adder_1++half_adder_1 p1 p2 = do+    p3 <- boolean ; p4 <- boolean+    assert [p1, not p4]+    assert [p2, not p4]+    assert [not p3, not p4]+    assert [not p1, not p2, not p3]+    assert [not p1, not p2, p4]+    assert [not p1, p2, p3]+    assert [not p1, p3, p4]+    assert [p1, not p2, p3]+    assert [p1, p2, not p3]+    assert [not p2, p3, p4]+    return (p3,p4)++half_adder_0 p1 p2 = do     p3 <- boolean ; p4 <- boolean     assert [not p2,p3,p4]     assert [p2,not p4]

@@ -18,18 +18,19 @@ import Satchmo.Data import Satchmo.MonadSAT -import Data.Map ( Map )-import qualified Data.Map as M+import Satchmo.SAT (SAT) -- for specializations++import Data.Array import Data.Maybe ( fromJust ) import Data.List ( partition )  import Control.Monad.Reader  data Boolean = Boolean-             { encode :: Literal-             , decode :: C.Decoder Bool+             { encode :: ! Literal+             -- , decode :: ! ( C.Decoder Bool )              }-     | Constant { value :: Bool }+     | Constant { value :: ! Bool }  {- @@ -65,49 +66,63 @@  instance C.Decode Boolean Bool where      decode b = case b of-        Boolean {} -> decode b+        -- Boolean {} -> decode b+        Boolean {} -> asks $ \ arr -> +              let x = encode b+              in  positive x == arr ! ( variable x )         Constant {} -> return $ value b  boolean :: MonadSAT m => m Boolean boolean = exists+{-# INLINABLE boolean #-}+{-# specialize inline boolean :: SAT Boolean #-}  exists :: MonadSAT m => m Boolean+{-# specialize inline exists :: SAT Boolean #-} exists = do     x <- fresh     return $ Boolean             { encode = x+{-                                  , decode = asks $ \ fm ->                        ( positive x == )                     $ fromJust                     $ M.lookup ( variable x ) fm+-}            }  forall :: MonadSAT m => m Boolean+{-# specialize inline forall :: SAT Boolean #-} forall = do     x <- fresh_forall     return $ Boolean             { encode = x-           , decode = error "Boolean.forall cannot be decoded"+--           , decode = error "Boolean.forall cannot be decoded"            }  constant :: MonadSAT m => Bool -> m Boolean+{-# specialize inline constant :: Bool -> SAT Boolean #-} constant v = do     return $ Constant { value = v } +{-# INLINABLE constant #-}  not :: Boolean -> Boolean not b = case b of     Boolean {} -> Boolean        { encode = nicht $ encode b-      , decode = do x <- decode b ; return $ Prelude.not x+      -- , decode = do x <- decode b ; return $ Prelude.not x       }     Constant {} -> Constant { value = Prelude.not $ value b }+{-# INLINABLE not #-}   assert :: MonadSAT m => [ Boolean ] -> m ()+{-# specialize inline assert :: [ Boolean ] -> SAT () #-} assert bs = do     let ( con, uncon ) = partition isConstant bs     let cval = Prelude.or $ map value con     when ( Prelude.not cval ) $ emit $ clause $ map encode uncon+{-# INLINABLE assert #-}  assertW :: MonadSAT m => Weight -> [ Boolean ] -> m () assertW w bs = do@@ -118,7 +133,8 @@ monadic :: Monad m         => ( [ a ] -> m b )         -> ( [ m a ] -> m b )+{-# specialize inline monadic :: ([a] -> SAT b) -> [SAT a] -> SAT b #-}         monadic f ms = do     xs <- sequence ms     f xs-+{-# INLINABLE monadic #-}

@@ -15,9 +15,12 @@ import Satchmo.Code import Satchmo.Boolean.Data +import Satchmo.SAT ( SAT) -- for specializations+ import Control.Monad ( foldM )  and :: MonadSAT m => [ Boolean ] -> m Boolean+{-# specialize inline and :: [ Boolean ] -> SAT Boolean #-} and [] = constant True and [x]= return x and xs = do@@ -29,6 +32,7 @@     return y  or :: MonadSAT m => [ Boolean ] -> m Boolean+{-# specialize inline or :: [ Boolean ] -> SAT Boolean #-} or [] = constant False or [x]= return x or xs = do@@ -36,6 +40,7 @@     return $ not y  xor :: MonadSAT m => [ Boolean ] -> m Boolean+{-# specialize inline xor :: [ Boolean ] -> SAT Boolean #-} xor [] = constant False xor (x:xs) = foldM xor2 x xs @@ -46,6 +51,7 @@         ( Bool -> Bool -> Bool )      -> Boolean -> Boolean       -> m Boolean+{-# specialize inline fun2 :: (Bool -> Bool -> Bool) -> Boolean -> Boolean -> SAT Boolean #-} fun2 f x y = do     r <- boolean     sequence_ $ do@@ -62,6 +68,7 @@         ( Bool -> Bool -> Bool -> Bool )      -> Boolean -> Boolean -> Boolean      -> m Boolean+{-# specialize inline fun3 :: (Bool -> Bool -> Bool -> Bool) -> Boolean -> Boolean -> Boolean -> SAT Boolean #-} fun3 f x y z = do     r <- boolean     sequence_ $ do@@ -76,7 +83,9 @@     return r  xor2 :: MonadSAT m => Boolean -> Boolean -> m Boolean+{-# specialize inline  xor2 :: Boolean -> Boolean -> SAT Boolean #-} xor2 = fun2 (/=)+-- xor2 = xor2_orig  -- for historic reasons: xor2_orig :: MonadSAT m => Boolean -> Boolean -> m Boolean

@@ -10,17 +10,17 @@  import Satchmo.Data --import Data.Map ( Map )-import qualified Data.Map as M import Data.Array  import Control.Monad.Reader  -class Decode c a where decode :: c -> Decoder a+class Decode c a where +    {-# INLINABLE decode #-}+    decode :: c -> Decoder a -type Decoder a = Reader ( Map Variable Bool ) a+-- type Decoder a = Reader ( Map Variable Bool ) a+type Decoder a = Reader ( Array Variable Bool ) a  instance Decode () () where     decode () = return ()

@@ -43,17 +43,20 @@ literal :: Bool -> Variable -> Literal literal p v | v /= 0 =      Literal $ if p then v else negate v-+{-# INLINE literal #-}  nicht :: Literal -> Literal nicht ( Literal i ) = Literal $ negate i+{-# INLINE nicht #-}  -- FIXME: should be newtype type Variable = Int  variable :: Literal -> Variable variable ( Literal v ) = abs v+{-# INLINE variable #-}  positive :: Literal -> Bool positive ( Literal v ) = 0 < v +{-# INLINE positive #-}

@@ -5,6 +5,7 @@ module Satchmo.MonadSAT  ( MonadSAT(..), Weight+, Header (..)                 )  where@@ -27,9 +28,21 @@  class (Functor m, Monad m) => MonadSAT m where   fresh, fresh_forall :: m Literal+  {-# INLINABLE fresh #-}   emit  :: Clause -> m ()+  {-# INLINABLE emit #-}   emitW :: Weight -> Clause -> m ()+  -- | emit some note (could be printed by the backend)+  note :: String -> m () +type NumClauses = Integer+type NumVars    = Integer++data Header = +     Header { numClauses, numVars :: ! Int+            , universals :: ! [Int]+                     }+     deriving Show  -- ------------------------------------------------------- -- MonadSAT liftings for standard monad transformers

@@ -12,15 +12,18 @@ import Satchmo.Code import Satchmo.Boolean +import Satchmo.SAT+ import qualified Data.Array as A import Data.Array hiding ( bounds, (!), indices, assocs )  import Control.Monad ( guard ) -data Relation a b = Relation ( Array (a,b) Boolean ) +newtype Relation a b = Relation ( Array (a,b) Boolean )   relation :: ( Ix a, Ix b, MonadSAT m )           => ((a,b),(a,b)) -> m ( Relation a b ) +{-# specialize inline relation :: ( Ix a, Ix b) => ((a,b),(a,b)) -> SAT ( Relation a b ) #-}  relation bnd = do     pairs <- sequence $ do          p <- range bnd

@@ -22,6 +22,8 @@ import Control.Monad ( guard ) import Data.Ix +import Satchmo.SAT+ mirror :: ( Ix a , Ix b ) => Relation a b -> Relation b a mirror r =      let ((a,b),(c,d)) = bounds r@@ -34,6 +36,7 @@ union :: ( Ix a , Ix b, MonadSAT m )        => Relation a b -> Relation a b        -> m ( Relation a b )+{-# specialize inline union :: ( Ix a , Ix b ) => Relation a b -> Relation a b -> SAT ( Relation a b ) #-}       union r s = do     pairs <- sequence $ do         i <- indices r@@ -42,6 +45,7 @@  product :: ( Ix a , Ix b, Ix c, MonadSAT m )          => Relation a b -> Relation b c -> m ( Relation a c )+{-# specialize inline product ::  ( Ix a , Ix b, Ix c ) => Relation a b -> Relation b c -> SAT ( Relation a c ) #-}       product a b = do     let ((ao,al),(au,ar)) = bounds a         ((bo,bl),(bu,br)) = bounds b@@ -58,6 +62,7 @@ intersection :: ( Ix a , Ix b, MonadSAT m )        => Relation a b -> Relation a b        -> m ( Relation a b )+{-# specialize inline intersection ::  ( Ix a , Ix b ) => Relation a b -> Relation a b -> SAT ( Relation a b ) #-}  intersection r s = do     pairs <- sequence $ do         i <- indices r

@@ -22,29 +22,36 @@ import Control.Monad ( guard ) import Data.Ix +import Satchmo.SAT+ implies :: ( Ix a, Ix b, MonadSAT m )          => Relation a b -> Relation a b -> m Boolean+{-# specialize inline implies :: ( Ix a, Ix b ) => Relation a b -> Relation a b -> SAT Boolean #-}       implies r s = monadic and $ do     i <- indices r     return $ or [ not $ r ! i, s ! i ]   symmetric :: ( Ix a, MonadSAT m) => Relation a a -> m Boolean+{-# specialize inline symmetric :: ( Ix a ) => Relation a a -> SAT Boolean #-}       symmetric r = implies r ( mirror r )  irreflexive :: ( Ix a, MonadSAT m) => Relation a a -> m Boolean+{-# specialize inline irreflexive :: ( Ix a ) =>  Relation a a -> SAT Boolean #-}       irreflexive r = and $ do     let ((a,b),(c,d)) = bounds r     x <- range ( a, c)     return $ Satchmo.Boolean.not $ r ! (x,x)   reflexive :: ( Ix a, MonadSAT m) => Relation a a -> m Boolean+{-# specialize inline reflexive :: ( Ix a ) => Relation a a -> SAT Boolean #-}       reflexive r = and $ do     let ((a,b),(c,d)) = bounds r     x <- range (a,c)     return $ r ! (x,x)   regular :: ( Ix a, MonadSAT m) => Int -> Relation a a -> m Boolean+{-# specialize inline regular :: ( Ix a ) => Int -> Relation a a -> SAT Boolean #-}       regular deg r = monadic and $ do     let ((a,b),(c,d)) = bounds r     x <- range ( a , c )@@ -54,6 +61,7 @@  transitive :: ( Ix a, MonadSAT m )             => Relation a a -> m Boolean+{-# specialize inline transitive :: ( Ix a ) => Relation a a -> SAT Boolean #-}       transitive r = do     r2 <- product r r     implies r2 r

@@ -1,101 +1,9 @@-{-# LANGUAGE GeneralizedNewtypeDeriving #-}--module Satchmo.SAT--( SAT, Header(..)-, fresh, fresh_forall-, emit, Weight-, sat-)--where--import Satchmo.Data-import Satchmo.MonadSAT--import Control.Exception-import Control.Monad.RWS.Strict-import qualified  Data.Set as Set-import qualified Data.ByteString.Lazy.Char8 as BS-import System.Directory-import System.Environment-import System.IO---instance MonadSAT SAT where-  fresh = satfresh-  fresh_forall = satfresh_forall-  emit    = satemit-  emitW _ _ = return ()---- ------------------ Implementation--- -----------------data Accu = Accu-          { next :: ! Int-          , universal :: [Int]-          , size :: ! Int-          }--start :: Accu-start = Accu-      { next = 1-      , universal = []-      , size = 0-      }--newtype SAT a = SAT {unsat::RWST Handle () Accu IO a}-    deriving (MonadState Accu, MonadReader Handle, Monad, MonadIO, Functor)--type NumClauses = Integer-type NumVars    = Integer--data Header = Header { numClauses, numVars :: Int-                     , universals :: [Int]-                     }---sat :: SAT a -> IO (BS.ByteString, Header, a )-sat (SAT m) =- bracket-    (getTemporaryDirectory >>= (`openTempFile`  "satchmo"))-    (\(fp, h) -> removeFile fp)-    (\(fp, h) -> do-       hSetBuffering h (BlockBuffering Nothing)-       ~(a, accu, _) <- runRWST m h start-       hClose h-       let header = Header (size accu) (next accu - 1) universals-           universals = reverse $ universal accu--       bs <- BS.readFile fp-       return (bs, header, a))---- | existentially quantified (implicitely so, before first fresh_forall)-satfresh :: SAT Literal-satfresh = do-    a <- get-    let n = next a-    put $ a { next = n + 1 }-    return $ literal True n---- | universally quantified-satfresh_forall :: SAT Literal-satfresh_forall = do-    a <- get-    let n = next a-    put $ a { next = n + 1, universal = n : universal a }-    return $ literal True n--satemit :: Clause -> SAT ()-satemit clause = do-    a <- get-    tellSat (bshowClause clause)-    put $ a-        { size = size a + 1-        }-  where bshowClause c = BS.pack (show c) `mappend` BS.pack "\n"---tellSat x = do {h <- ask; liftIO $ BS.hPut h x}+module Satchmo.SAT ( +  -- module Satchmo.SAT.BS +  -- module Satchmo.SAT.Seq+  module Satchmo.SAT.Tmpfile+) where +import Satchmo.SAT.Seq+import Satchmo.SAT.BS+import Satchmo.SAT.Tmpfile

@@ -0,0 +1,67 @@+{-# LANGUAGE GeneralizedNewtypeDeriving #-}++module Satchmo.SAT.BS++( SAT, Header(..)+, fresh, fresh_forall+, emit, Weight+, sat+)++where++import Satchmo.Data+import Satchmo.MonadSAT++import Control.Exception++import Control.Monad.RWS.Strict+-- import Control.Monad.RWS.Lazy++-- import qualified Data.ByteString.Lazy.Char8 as BS+import qualified Data.ByteString.Char8 as BS++import Data.Foldable+import Data.String++newtype SAT a +      = SAT { unSAT :: -- WriterT BS.ByteString ( StateT Header Identity ) +                       -- StateT Header ( WriterT BS.ByteString Identity )+                       RWS () BS.ByteString Header+                       -- RWS () ( S.Seq BS.ByteString ) Header+                       a+            } +      deriving ( Functor, Monad+               , MonadState Header+               , MonadWriter BS.ByteString+               -- , MonadWriter ( S.Seq BS.ByteString )+               )+++instance MonadSAT SAT where+  fresh = do +      a <- get +      let v = numVars a+      put $ a { numVars = succ v } +      return $ literal True $ succ v+  emit cl = do+      a <- get+      put $ a { numClauses = succ $ numClauses a }+      tell $  fromString $ show  cl ++ "\n"+  note msg = do+      return ()+     +start :: Header+start = Header { numClauses = 0, numVars = 0+               , universals = []+               }+++sat :: SAT a -> IO (BS.ByteString, Header, a )+sat (SAT m) = do+    let -- ((res,bs),accu) = runState (runWriterT m) start+        -- ((res,accu),bs) = runWriter ( runStateT m  start )+        (res, accu, bs) = runRWS m () start +    return ( bs , accu, res )++

@@ -0,0 +1,70 @@+{-# LANGUAGE GeneralizedNewtypeDeriving #-}++module Satchmo.SAT.Seq++( SAT, Header(..)+, fresh, fresh_forall+, emit, Weight+, sat+)++where++import Satchmo.Data+import Satchmo.MonadSAT++import Control.Exception++import Control.Monad.RWS.Strict+-- import Control.Monad.RWS.Lazy++-- import qualified Data.Sequence as S+import qualified Satchmo.SAT.Sequence as S++import qualified Data.ByteString.Char8 as BS+-- import qualified Data.ByteString.Lazy.Char8 as BS++import Data.Foldable+import Data.String++newtype SAT a +      = SAT { unSAT :: -- WriterT BS.ByteString ( StateT Header Identity ) +                       -- StateT Header ( WriterT BS.ByteString Identity )+                       -- RWS () BS.ByteString Header+                       RWS () ( S.Seq BS.ByteString ) Header+                       a+            } +      deriving ( Functor, Monad+               , MonadState Header+               , MonadWriter ( S.Seq BS.ByteString )+               -- , MonadWriter BS.ByteString+               )+++instance MonadSAT SAT where+  note msg = do return ()+  fresh = do +      a <- get +      let v = numVars a+      put $ a { numVars = succ v } +      return $ literal True $ succ v+  emit cl = do+      a <- get+      put $ a { numClauses = succ $ numClauses a }+      tell $  S.singleton $ fromString $ show  cl ++ "\n"++     +start :: Header+start = Header { numClauses = 0, numVars = 0+               , universals = []+               }+++sat :: SAT a -> IO (BS.ByteString, Header, a )+sat (SAT m) = do+    let -- ((res,bs),accu) = runState (runWriterT m) start+        -- ((res,accu),bs) = runWriter ( runStateT m  start )+        (res, accu, bs) = runRWS m () start +    return ( fold bs , accu, res )++

@@ -0,0 +1,26 @@+-- | binary trees without any balance++module Satchmo.SAT.Sequence where++import Data.Monoid+import Data.Foldable++data Seq a = Empty | Leaf !a +           | Branch !(Seq a) !(Seq a)++{-# INLINABLE singleton #-}+singleton x = Leaf x++instance Monoid (Seq a) where+    {-# INLINABLE mappend #-}+    mappend = Branch+    {-# INLINABLE mempty #-}+    mempty = Empty++instance Foldable Seq where+    {-# INLINABLE fold #-}+    fold s = case s of+        Empty -> mempty+        Leaf k -> k+        Branch l r -> mappend (fold l) (fold r)+        

@@ -0,0 +1,116 @@+{-# LANGUAGE GeneralizedNewtypeDeriving #-}++module Satchmo.SAT.Tmpfile++( SAT, Header(..)+, fresh, fresh_forall+, emit, Weight+, sat+)++where++import Satchmo.Data+import Satchmo.MonadSAT++import Control.Exception+import Control.Monad.RWS.Strict+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 )++instance MonadSAT SAT where+  fresh = satfresh+  fresh_forall = satfresh_forall+  emit    = satemit+  emitW _ _ = return ()+  note msg = do a <- get ; put $ a { notes = msg : notes a }++-- ---------------+-- Implementation+-- ---------------++data Accu = Accu+          { next :: ! Int+          , universal :: [Int]+          , size :: ! Int+          , notes :: ! [ String ]+          , census :: ! ( M.Map Int Int )+          }++start :: Accu+start = Accu+      { next = 1+      , universal = []+      , size = 0+      , notes = [ "Satchmo.SAT.Tmpfile implementation" ]+      , census = M.empty          +      }++newtype SAT a = SAT {unsat::RWST Handle () Accu IO a}+    deriving (MonadState Accu, MonadReader Handle, Monad, MonadIO, Functor)+++sat :: SAT a -> IO (BS.ByteString, Header, a )+sat (SAT m) =+ bracket+    (getTemporaryDirectory >>= (`openTempFile`  "satchmo"))+    (\(fp, h) -> removeFile fp)+    (\(fp, h) -> do+       hSetBuffering h (BlockBuffering Nothing)+       ~(a, accu, _) <- runRWST m h start+       hClose h+       +       forM ( reverse $ notes accu ) $ hPutStrLn stderr +       hPutStrLn stderr $ unlines +           [ "(clause length, frequency)"+           , show $ sortBy ( comparing ( negate . snd )) +                        $ M.toList $ census accu+           ]  +       +       let header = Header (size accu) (next accu - 1) universals+           universals = reverse $ universal accu++       bs <- BS.readFile fp+       return (bs, header, a))++-- | existentially quantified (implicitely so, before first fresh_forall)+satfresh :: SAT Literal+satfresh = do+    a <- get+    let n = next a+    put $ a { next = n + 1 }+    return $ literal True n++-- | universally quantified+satfresh_forall :: SAT Literal+satfresh_forall = do+    a <- get+    let n = next a+    put $ a { next = n + 1, universal = n : universal a }+    return $ literal True n++satemit :: Clause -> SAT ()+satemit clause = do+    h <- ask ; liftIO $ hPutStrLn h $ show clause+    a <- get+    -- tellSat (bshowClause clause)+    put $ a+        { size = size a + 1+        , census = M.insertWith (+) (length $ literals clause) 1 $ census a         +        }+  where bshowClause c = BS.pack (show c) `mappend` BS.pack "\n"+++tellSat x = do {h <- ask; liftIO $ BS.hPut h x}+

@@ -2,13 +2,14 @@ module Satchmo.SAT.Weighted (SAT, sat, MaxWeight, Header(..)) where  import Satchmo.Data-import Satchmo.MonadSAT+import Satchmo.MonadSAT hiding ( Header )  import Control.Exception import Control.Monad.RWS.Strict import Data.Maybe import qualified  Data.Set as Set-import qualified Data.ByteString.Lazy.Char8 as BS+-- import qualified Data.ByteString.Lazy.Char8 as BS+import qualified Data.ByteString.Char8 as BS import System.Directory import System.Environment import System.IO

@@ -15,23 +15,25 @@ import Satchmo.SAT import qualified Satchmo.SAT.Weighted as Weighted -import qualified Data.ByteString.Lazy.Char8 as BS+-- import qualified Data.ByteString.Lazy.Char8 as BS+import qualified Data.ByteString.Char8 as BS+ import Data.Map ( Map ) import qualified Data.Map as M-+import Data.Array import Control.Monad.Reader  import System.IO  type Implementation = BS.ByteString                      -> Header -                    -> IO ( Maybe ( Map Variable Bool ) )+                    -> IO ( Maybe ( Array Variable Bool ) )  type WeightedImplementation = BS.ByteString -                            -> Weighted.Header -                            -> IO ( Maybe ( Map Variable Bool ) )+    -> Weighted.Header +    -> IO ( Maybe ( Array Variable Bool ) ) -solve :: Implementation +solve :: Implementation       -> SAT ( Decoder a )        -> IO ( Maybe a ) solve implementation build = do

@@ -1,5 +1,5 @@ Name:           satchmo-Version:        1.8.1+Version:        1.9.1  License:        GPL License-file:	gpl-2.0.txt@@ -17,6 +17,7 @@ build-type: Simple  Library+    ghc-options: -funbox-strict-fields     Build-depends:  mtl, process, containers, base == 4.*, array, bytestring, directory     Exposed-modules:         Satchmo.Data@@ -36,6 +37,10 @@         Satchmo.Relation.Prop         Satchmo.MonadSAT         Satchmo.SAT+        Satchmo.SAT.Tmpfile+        Satchmo.SAT.BS+        Satchmo.SAT.Seq+        Satchmo.SAT.Sequence         Satchmo.Simple         Satchmo.SAT.Weighted     Other-modules: