packages feed

satchmo 1.4 → 1.8.0

raw patch · 24 files changed

+995/−202 lines, 24 filesdep +bytestringdep +directorydep ~base

Dependencies added: bytestring, directory

Dependency ranges changed: base

Files

Satchmo/Binary/Data.hs view
@@ -29,7 +29,7 @@ width n = length $ bits n  -- | declare a number variable (bit width)-number :: Int -> SAT Number+number :: MonadSAT m => Int -> m Number number w = do     xs <- sequence $ replicate w boolean     return $ make xs@@ -50,7 +50,7 @@     in  toEnum ( fromIntegral m ) : toBinary d  -- | declare a number constant -constant :: Integer -> SAT Number+constant :: MonadSAT m => Integer -> m Number constant n = do     xs <- mapM B.constant $ toBinary n     return $ make xs
Satchmo/Binary/Op/Common.hs view
@@ -11,21 +11,21 @@  import qualified Satchmo.Code as C -import Satchmo.Boolean hiding ( constant )+import Satchmo.Boolean (MonadSAT, Boolean, Booleans, fun2, fun3, and, or, not, xor, assert, boolean) import qualified  Satchmo.Boolean as B-import Satchmo.Binary.Data+import Satchmo.Binary.Data (Number, make, bits)  import Satchmo.Counting -iszero :: Number -> SAT Boolean+iszero :: (MonadSAT m) =>  Number -> m Boolean iszero a = equals a $ make [] -equals :: Number -> Number -> SAT Boolean+equals :: (MonadSAT m) =>  Number -> Number -> m Boolean equals a b = do     equals' ( bits a ) ( bits b )  -equals' :: Booleans -> Booleans -> SAT Boolean+equals' :: (MonadSAT m) =>  Booleans -> Booleans -> m Boolean equals' [] [] = B.constant True equals' (x:xs) (y:ys) = do     z <- xor [x, y]@@ -34,46 +34,78 @@ equals' xs [] = and $ map not xs equals' [] ys = and $ map not ys +le,lt,ge,gt,eq :: MonadSAT m => Number -> Number -> m Boolean le x y = do (l,e) <- compare x y ; or [l,e] lt x y = do (l,e) <- compare x y ; return l ge x y = le y x gt x y = lt y x eq = equals -compare :: Number -> Number -        -> SAT ( Boolean, Boolean )+compare :: MonadSAT m => Number -> Number +        -> m ( Boolean, Boolean ) compare a b = compare' ( bits a ) ( bits b ) -compare' :: Booleans +compare' :: (MonadSAT m) => Booleans           -> Booleans -         -> SAT ( Boolean, Boolean ) -- ^ (less, equals)+         -> m ( Boolean, Boolean ) -- ^ (less, equals)+ compare' [] [] = do -    f <- B.constant False ; t <- B.constant True ; return ( f, t )+    f <- B.constant False +    t <- B.constant True +    return ( f, t ) compare' (x:xs) (y:ys) = do     l <- and [ not x, y ]     e <- fmap not $ xor [ x, y ]     ( ll, ee ) <- compare' xs ys     lee <- and [l,ee]-    l' <- or [ l, lee ] ; e' <- and [ e, ee ]+    l' <- or [ ll, lee ]+    e' <- and [ e, ee ]     return ( l', e' ) compare' xs [] = do     x <- or xs-    return ( not x, not x )+    never <- B.constant False+    return ( never, not x ) compare' [] ys = do     y <- or ys     return ( y, not y ) -full_adder :: Boolean -> Boolean -> Boolean-           -> SAT ( Boolean, Boolean )-full_adder a b c = do+full_adder :: (MonadSAT m) +           => Boolean -> Boolean -> Boolean+           -> m ( Boolean, Boolean )+full_adder 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]+    assert [not p1,not p2,not p3,p4]+    assert [not p1,not p2,p3,not p4]+    assert [not p1,p2,p3,p4]+    assert [p1,p3,not p5]+    assert [p1,not p2,not p3,not p4]+    assert [p1,p2,not p3,p4]+    assert [p1,p2,p3,not p4]+    return ( p4, p5 )++full_adder_plain a b c = do     let s x y z = sum $ map fromEnum [x,y,z]     r <- fun3 ( \ x y z -> odd $ s x y z ) a b c     d <- fun3 ( \ x y z -> 1   < s x y z ) a b c     return ( r, d ) -half_adder :: Boolean -> Boolean -           -> SAT ( Boolean, Boolean )-half_adder a b = do+half_adder :: (MonadSAT m) +           => Boolean -> Boolean +           -> m ( Boolean, Boolean )+half_adder p1 p2 = do+    p3 <- boolean ; p4 <- boolean+    assert [not p2,p3,p4]+    assert [p2,not p4]+    assert [not p1,p3,p4]+    assert [not p1,not p2,not p3]+    assert [p1,not p4]+    assert [p1,p2,not p3]+    return ( p3, p4 )++half_adder_plain a b = do     let s x y = sum $ map fromEnum [x,y]     r <- fun2 ( \ x y -> odd $ s x y ) a b     d <- fun2 ( \ x y -> 1   < s x y ) a b
Satchmo/Binary/Op/Fixed.hs view
@@ -27,9 +27,12 @@  import Satchmo.Counting +import Data.Map ( Map )+import qualified Data.Map as M+ -- | give only lower k bits, upper bits must be zero, -- (else unsatisfiable)-restricted :: Int -> Number -> SAT Number+restricted :: (MonadSAT m) => Int -> Number -> m Number restricted w a = do     let ( low, high ) = splitAt w $ bits a     sequence $ do x <- high ; return $ assert [ not x ]@@ -37,41 +40,40 @@  -- | result bit width is max of argument bit widths. -- if overflow occurs, then formula is unsatisfiable.-add :: Number -> Number -> SAT Number+add :: (MonadSAT m) => Number -> Number -> m Number add a b = do     false <- Satchmo.Boolean.constant False     let w = max ( width a ) ( width b )     zs <- add_with_carry w false ( bits a ) ( bits b )     return $ make zs  -add_with_carry :: Int -> Boolean -> Booleans -> Booleans -> SAT Booleans+add_with_carry :: (MonadSAT m) => Int -> Boolean -> Booleans -> Booleans -> m Booleans add_with_carry w c xxs yys = case ( xxs, yys ) of     _ | w <= 0 -> do         sequence_ $ do p <- c : xxs ++ yys ; return $ assert [ not p ]         return []     ( [] , [] ) -> return [ c ]     ( [], y : ys) -> do-        -- r <- xor [ c, y ]-        -- d <- and [ c, y ]         (r,d) <- half_adder c y         rest <- add_with_carry (w-1) d [] ys         return $ r : rest     ( x : xs, [] ) -> add_with_carry w c yys xxs     (x : xs, y:ys) -> do-        -- r <- xor [c,x,y]-        -- d <- atleast 2 [c,x,y]         (r,d) <- full_adder c x y         rest <- add_with_carry (w-1) d xs ys         return $ r : rest  -- | result bit width is at most max of argument bit widths. -- if overflow occurs, then formula is unsatisfiable.-times :: Number -> Number -> SAT Number+times :: (MonadSAT m) => Number -> Number -> m Number times a b = do      let w = max ( width a ) ( width b ) -    restricted_times w a b+    -- restricted_times w a b+    better_times w a b -restricted_times :: Int -> Number -> Number -> SAT Number+restricted_times :: (MonadSAT m) +                 => Int +                 -> Number -> Number -> m Number restricted_times w a b = case bits a of     [] -> return $ make []     _ | w <= 0 -> do@@ -87,8 +89,41 @@         s <- Flexible.add xys xsys         restricted w s -        +--------------------------------------------------  +better_times w a b = do+    kzs <- sequence $ do+          ( i , x ) <- zip [ 0 .. ] $ bits a+          ( j , y ) <- zip [ 0 .. ] $ bits b+          return $ +              if i+j >= w +              then do +                  assert [ not x, not y ]+                  return ( i+j, [] )+              else do +                  z <- and [ x, y ]+                  return ( i+j , [z] ) +    zs <- reduce $ take w+                 $ M.elems $ M.fromListWith (++) kzs+    return $ make zs  +reduce ( ( x:y:z:ps) : qss ) = do+    ( r, c ) <- full_adder x y z+    qss' <- plugin c qss+    reduce $ ( ps ++ [r] ) : qss' +reduce ( ( x:y:[]) : qss ) = do+    ( r, c ) <- half_adder x y +    qss' <- plugin c qss+    reduce $ [r] : qss' +reduce ( ( x:[]) : qss ) = do+    xs <- reduce qss+    return $ x : xs+reduce [] = return []++plugin c [] = do+    assert [ not c ]+    return []+plugin c (qs : qss) = +    return ((c:qs) : qss)
Satchmo/Binary/Op/Flexible.hs view
@@ -21,47 +21,82 @@ import Satchmo.Binary.Op.Common import Satchmo.Counting -add :: Number -> Number -> SAT Number+import qualified Data.Map as M++add :: (MonadSAT m) => Number -> Number -> m Number add a b = do     false <- Satchmo.Boolean.constant False-    ( zs, carry ) <- add_with_carry false (bits a) (bits b)+    ( zs, carry ) <- +        add_with_carry false (bits a) (bits b)     return $ make $ zs ++ [carry] -add_with_carry :: Boolean +add_with_carry :: (MonadSAT m) => Boolean                 -> Booleans -> Booleans-               -> SAT ( Booleans, Boolean )+               -> m ( Booleans, Boolean ) add_with_carry cin [] [] = return ( [], cin ) add_with_carry cin (x:xs) [] = do-    -- z <- xor [ cin, x ]-    -- c <- and [ cin, x ]     (z, c) <- half_adder cin x     ( zs, cout ) <- add_with_carry c xs []     return ( z : zs, cout ) add_with_carry cin [] (y:ys) = do     add_with_carry cin (y:ys) [] add_with_carry cin (x:xs ) (y:ys) = do-    -- z  <- xor [ cin, x, y ]-    -- c <- atleast 2 [ cin, x, y ]     (z, c) <- full_adder cin x y     ( zs, cout ) <- add_with_carry c xs ys     return ( z : zs, cout ) -times :: Number -> Number -> SAT Number-times a b | [x] <- bits a = times1 x b-times a b | x:xs <- bits a = do+times :: (MonadSAT m) => Number -> Number -> m Number+times = better_times++plain_times :: (MonadSAT m) => Number -> Number -> m Number+plain_times a b | [] <- bits a = return a+plain_times a b | [] <- bits b = return b+plain_times a b | [x] <- bits a = times1 x b+plain_times a b | [y] <- bits b = times1 y a+plain_times a b | x:xs <- bits a = do     xys  <- times1 x b-    xsys <- times (make xs) b+    xsys <- plain_times (make xs) b     zs <- shift xsys     add xys zs  -- | multiply by 2-shift :: Number -> SAT Number+shift :: (MonadSAT m) => Number -> m Number shift a = do     false <- Satchmo.Boolean.constant False      return $ make $ false : bits a -times1 :: Boolean -> Number -> SAT Number+times1 :: (MonadSAT m) => Boolean -> Number -> m Number times1 x b = do     zs <- mapM ( \ y -> and [x,y] ) $ bits b     return $ make zs ++better_times a b = do+    kzs <- sequence $ do+          ( i , x ) <- zip [ 0 .. ] $ bits a+          ( j , y ) <- zip [ 0 .. ] $ bits b+          return $ do+                  z <- and [ x, y ]+                  return ( i+j , [z] ) +    zs <- reduce $ M.elems $ M.fromListWith (++) kzs+    return $ make zs+++reduce ( ( x:y:z:ps) : qss ) = do+    ( r, c ) <- full_adder x y z+    qss' <- plugin c qss+    reduce $ ( ps ++ [r] ) : qss' +reduce ( ( x:y:[]) : qss ) = do+    ( r, c ) <- half_adder x y +    qss' <- plugin c qss+    reduce $ [r] : qss' +reduce ( ( x:[]) : qss ) = do+    xs <- reduce qss+    return $ x : xs+reduce [] = return []++plugin c [] = do+    assert [ not c ]+    return []+plugin c (qs : qss) = +    return ((c:qs) : qss)
Satchmo/Boolean.hs view
@@ -1,14 +1,14 @@-module Satchmo.Boolean +module Satchmo.Boolean -( SAT+( MonadSAT(..) , module Satchmo.Boolean.Data , module Satchmo.Boolean.Op-) +)  where  import qualified Prelude -import Satchmo.Internal+import Satchmo.MonadSAT import Satchmo.Boolean.Data import Satchmo.Boolean.Op
Satchmo/Boolean/Data.hs view
@@ -1,11 +1,11 @@ {-# language MultiParamTypeClasses #-} -module Satchmo.Boolean.Data +module Satchmo.Boolean.Data -( Boolean, Booleans+( Boolean(Constant), Booleans, encode , boolean, exists, forall , constant-, not, assert, monadic+, not, assert, assertW, monadic )  where@@ -15,8 +15,8 @@  import qualified Satchmo.Code as C -import Satchmo.Data -import Satchmo.Internal+import Satchmo.Data+import Satchmo.MonadSAT  import Data.Map ( Map ) import qualified Data.Map as M@@ -31,6 +31,32 @@              }      | Constant { value :: Bool } +{-++-- FIXME: @Pepe: what is the reason for these instances?++instance Eq Boolean where+  b1@Boolean{}  == b2@Boolean{}  = encode b1 == encode b2+  b1@Constant{} == b2@Constant{} = value  b1 == value  b2+  _ == _ = False++instance Ord Boolean where+  b1@Boolean{}  `compare` b2@Boolean{}  = encode b1 `compare` encode b2+  b1@Constant{} `compare` b2@Constant{} = value  b1 `compare` value  b2+  Boolean{} `compare` Constant{} = GT+  Constant{} `compare` Boolean{} = LT++instance Enum Boolean where+  fromEnum (Constant True)  = -1+  fromEnum (Constant False) = 0+  fromEnum (Boolean (Literal lit) dec) = lit++  toEnum 0    = Constant False+  toEnum (-1) = Constant True+  toEnum l    = let x = literal l in Boolean x (asks $ \fm -> fromJust (M.lookup x fm))++-}+ type Booleans = [ Boolean ]  isConstant :: Boolean -> Bool@@ -42,18 +68,21 @@         Boolean {} -> decode b         Constant {} -> return $ value b -boolean :: SAT Boolean+boolean :: MonadSAT m => m Boolean boolean = exists -exists :: SAT Boolean+exists :: MonadSAT m => m Boolean exists = do     x <- fresh     return $ Boolean             { encode = x-           , decode = asks $ \ fm -> fromJust $ M.lookup x fm+           , decode = asks $ \ fm -> +                      ( positive x == )+                    $ fromJust+                    $ M.lookup ( variable x ) fm            } -forall :: SAT Boolean+forall :: MonadSAT m => m Boolean forall = do     x <- fresh_forall     return $ Boolean @@ -61,7 +90,7 @@            , decode = error "Boolean.forall cannot be decoded"            } -constant :: Bool -> SAT Boolean+constant :: MonadSAT m => Bool -> m Boolean constant v = do     return $ Constant { value = v }  @@ -73,11 +102,18 @@       }     Constant {} -> Constant { value = Prelude.not $ value b } -assert :: [ Boolean ] -> SAT ()++assert :: MonadSAT m => [ Boolean ] -> m () 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++assertW :: MonadSAT m => Weight -> [ Boolean ] -> m ()+assertW w bs = do+    let ( con, uncon ) = partition isConstant bs+    let cval = Prelude.or $ map value con+    when ( Prelude.not cval ) $ emitW w $ clause $ map encode uncon  monadic :: Monad m         => ( [ a ] -> m b )
Satchmo/Boolean/Op.hs view
@@ -1,4 +1,4 @@-module Satchmo.Boolean.Op +module Satchmo.Boolean.Op  ( constant , and, or, xor@@ -11,36 +11,41 @@ import Prelude hiding ( and, or, not ) import qualified Prelude -import Satchmo.Internal+import Satchmo.MonadSAT import Satchmo.Code import Satchmo.Boolean.Data  import Control.Monad ( foldM ) -and :: [ Boolean ] -> SAT Boolean+and :: MonadSAT m => [ Boolean ] -> m Boolean+and [] = constant True+and [x]= return x and xs = do     y <- boolean-    sequence $ do+    sequence_ $ do         x <- xs         return $ assert [ not y, x ]     assert $ y : map not xs     return y -or :: [ Boolean ] -> SAT Boolean+or :: MonadSAT m => [ Boolean ] -> m Boolean+or [] = constant False+or [x]= return x or xs = do     y <- and $ map not xs     return $ not y -xor :: [ Boolean ] -> SAT Boolean+xor :: MonadSAT m => [ Boolean ] -> m Boolean xor [] = constant False xor (x:xs) = foldM xor2 x xs   -- | implement the function by giving a full CNF -- that determines the outcome-fun2 :: ( Bool -> Bool -> Bool )+fun2 :: MonadSAT m => +        ( Bool -> Bool -> Bool )      -> Boolean -> Boolean -     -> SAT Boolean+     -> m Boolean fun2 f x y = do     r <- boolean     sequence_ $ do@@ -53,9 +58,10 @@  -- | implement the function by giving a full CNF -- that determines the outcome-fun3 :: ( Bool -> Bool -> Bool -> Bool )+fun3 :: MonadSAT m => +        ( Bool -> Bool -> Bool -> Bool )      -> Boolean -> Boolean -> Boolean-     -> SAT Boolean+     -> m Boolean fun3 f x y z = do     r <- boolean     sequence_ $ do@@ -69,11 +75,11 @@             ]     return r -xor2 :: Boolean -> Boolean -> SAT Boolean+xor2 :: MonadSAT m => Boolean -> Boolean -> m Boolean xor2 = fun2 (/=)  -- for historic reasons:-xor2_orig :: Boolean -> Boolean -> SAT Boolean+xor2_orig :: MonadSAT m => Boolean -> Boolean -> m Boolean xor2_orig x y = do     a <- and [ x, not y ]     b <- and [ not x, y ]
Satchmo/Code.hs view
@@ -18,9 +18,9 @@ import Control.Monad.Reader  -class Decode c a | c -> a where decode :: c -> Decoder a+class Decode c a where decode :: c -> Decoder a -type Decoder a = Reader ( Map Literal Bool ) a+type Decoder a = Reader ( Map Variable Bool ) a  instance Decode () () where     decode () = return ()@@ -30,6 +30,10 @@  instance ( Decode c a ) => Decode [c] [a] where     decode = mapM decode ++instance Decode a b => Decode ( Maybe a ) ( Maybe b ) where+    decode ( Just b ) = fmap Just $ decode b+    decode Nothing = return $ Nothing  instance (Ix i, Decode c a) => Decode ( Array i c) ( Array i a ) where     decode x = do
Satchmo/Counting.hs view
@@ -11,7 +11,7 @@  import Satchmo.Boolean -atleast_block :: Int -> [ Boolean ] -> SAT [ Boolean ]+atleast_block :: MonadSAT m => Int -> [ Boolean ] -> m [ Boolean ] atleast_block k [] = do     t <- constant True     f <- constant False@@ -25,13 +25,13 @@                      p <- and [ x, cs !! (i-1) ]                      or [ cs !! i, p ] -atleast :: Int -> [ Boolean ] -> SAT Boolean+atleast :: MonadSAT m => Int -> [ Boolean ] -> m Boolean atleast k xs = do     cs <- atleast_block k xs     return $ cs !! k          -atmost_block :: Int -> [ Boolean ] -> SAT [ Boolean ]+atmost_block :: MonadSAT m => Int -> [ Boolean ] -> m [ Boolean ] atmost_block k [] = do     t <- constant $ True     return $ replicate (k+1) t@@ -45,13 +45,13 @@             q <- and [ not x, cs !! i ]             or [ p, q ] -atmost :: Int -> [ Boolean ] -> SAT Boolean+atmost :: MonadSAT m => Int -> [ Boolean ] -> m Boolean atmost k xs = do     cs <- atmost_block k xs     return $ cs !! k          -exactly_block :: Int -> [ Boolean ] -> SAT [ Boolean ]+exactly_block :: MonadSAT m => Int -> [ Boolean ] -> m [ Boolean ] exactly_block k [] = do     t <- constant True     f <- constant False@@ -66,7 +66,7 @@             q <- and [ not x, cs !! i ]             or [ p, q ] -exactly :: Int -> [ Boolean ] -> SAT Boolean+exactly :: MonadSAT m => Int -> [ Boolean ] -> m Boolean exactly k xs = do     cs <- exactly_block k xs     return $ cs !! k
Satchmo/Data.hs view
@@ -1,15 +1,17 @@ module Satchmo.Data   ( CNF, cnf, clauses-, Clause, clause, literals-, Literal, literal, nicht+-- FIXME: exports should be abstract+, Clause(..), clause, literals+, Literal(..), literal, nicht+, Variable, variable, positive )  where  import Control.Monad.State.Strict -data CNF     = CNF { clauses :: [ Clause  ] }+newtype CNF     = CNF { clauses :: [ Clause  ] }  instance Show CNF where     show ( CNF cs ) = unlines $ map show cs@@ -18,7 +20,7 @@ cnf cs = CNF cs  -data Clause  = Clause { literals :: [ Literal ] }+newtype Clause  = Clause { literals :: [ Literal ] }  instance Show Clause where     show ( Clause xs ) = unwords ( map show xs ++ [ "0" ] )@@ -27,16 +29,31 @@ clause ls = Clause { literals = ls }  -data Literal = Literal Int +newtype Literal = Literal Int     deriving ( Eq, Ord )  instance Show Literal where      show ( Literal i ) = show i -literal :: Int -> Literal-literal i | i /= 0 = Literal i+instance Read Literal where+    readsPrec p = \ cs -> do+        ( i, cs') <- readsPrec p cs+        return ( Literal i , cs' ) +literal :: Bool -> Variable -> Literal+literal p v | v /= 0 = +    Literal $ if p then v else negate v + nicht :: Literal -> Literal nicht ( Literal i ) = Literal $ negate i++-- FIXME: should be newtype+type Variable = Int++variable :: Literal -> Variable+variable ( Literal v ) = abs v++positive :: Literal -> Bool+positive ( Literal v ) = 0 < v
+ Satchmo/Integer.hs view
@@ -0,0 +1,10 @@+module Satchmo.Integer ++( module Satchmo.Integer.Data +, module Satchmo.Integer.Op +)++where++import Satchmo.Integer.Data+import Satchmo.Integer.Op
+ Satchmo/Integer/Data.hs view
@@ -0,0 +1,67 @@+{-# language MultiParamTypeClasses #-}++module Satchmo.Integer.Data ++( Number, make, number+, constant+, bits, width+)++where++import Prelude hiding ( and, or, not )++import qualified Satchmo.Code as C++import Satchmo.Boolean hiding ( constant )+import qualified  Satchmo.Boolean as B++import Satchmo.Counting++data Number = Number +            { bits :: [ Boolean ] -- ^ lsb first,+	         -- using two's complement+            , decode :: C.Decoder Integer+            }++instance C.Decode Number Integer where+    decode = decode++width :: Number -> Int+width n = length $ bits n++-- | declare a number variable (bit width)+number :: MonadSAT m => Int -> m Number+number w = do+    xs <- sequence $ replicate w boolean+    return $ make xs++make :: [ Boolean ] -> Number+make xs = Number+           { bits = xs+           , decode = do ys <- mapM C.decode xs ; return $ fromBinary ys+           }++fromBinary :: [ Bool ] -> Integer+fromBinary xs = foldr ( \ x y -> 2*y + if x then 1 else 0 ) 0 xs++toBinary :: Integer -> [ Bool ]+toBinary 0 = []+toBinary n  = +    let (d,m) = divMod n 2+    in  toEnum ( fromIntegral m ) : toBinary d++-- | declare a number constant +constant :: MonadSAT m +	 => Int -- ^ bit width+	 -> Integer -- ^ value+	 -> m Number+constant w n = do+    xs <- if 0 <= n && n < 2^(w-1)+          then mapM B.constant $ toBinary n+	  else if negate ( 2^(w-1)) <= n && n < 0+	  then mapM B.constant $ toBinary (n + 2^w)+	  else error "Satchmo.Integer.Data.constant"+    z <- B.constant False+    return $ make $ take w $ xs ++ repeat z+
+ Satchmo/Integer/Op.hs view
@@ -0,0 +1,129 @@+-- | all operations have fixed bit length,+-- and are unsatisfiable in case of overflows.++module Satchmo.Integer.Op ++( negate, add, sub, times+, gt, ge, eq +)++where++import Satchmo.Integer.Data+import Prelude hiding ( and, or, not, negate )+import Satchmo.Boolean hiding ( constant )+import qualified  Satchmo.Boolean as B++import qualified Satchmo.Binary.Op.Common as C+import qualified Satchmo.Binary.Op.Flexible as F++import Control.Monad ( forM, when )++-- | negate. Unsatisfiable if value is lowest negatve.+negate :: MonadSAT m +       => Number -> m Number+negate n = do+    let ys = map B.not $ bits n +    o <- B.constant True+    ( zs, c ) <- increment ys o+    assert [ last $ ys, B.not $ last zs ]+    return $ make zs++increment [] z = return ( [], z )+increment (y:ys) z = do+    ( r, d ) <- C.half_adder y z+    ( rs, c ) <- increment ys d+    return ( r : rs, c )++add :: MonadSAT m +    => Number -> Number +    -> m Number+add a b = do+    when ( width a /= width b ) +    	 $ error "Satchmo.Integer.Op.add"+    cin <- B.constant False+    ( zs, cout ) <- +        F.add_with_carry cin ( bits a ) ( bits b )+    monadic assert [ fun2 (==) cout $ last zs ]+    return $ make zs++sub :: MonadSAT m +    => Number -> Number +    -> m Number+sub a b = do+    when ( width a /= width b ) +    	 $ error "Satchmo.Integer.Op.sub"+    c <- negate b+    add a c++times :: MonadSAT m +    => Number -> Number +    -> m Number+times a b = do+    when ( width a /= width b ) +    	 $ error "Satchmo.Integer.Op.times"+    c <- F.times ( F.make $ bits a ) +      	 	 ( F.make $ bits b )+    let ( pre, post ) = splitAt ( width a ) $ F.bits c+    monadic assert [ fun2 (==) ( head post) $ last pre ]+    return $ make pre++----------------------------------------------------++positive :: MonadSAT m+	 => Number +	 -> m Boolean+positive n = do+    ok <- or $ init $ bits n   +    and [ ok, not $ last $ bits n ]++negative :: MonadSAT m+	 => Number +	 -> m Boolean+negative n = do+    return $ last $ bits n++nonnegative :: MonadSAT m+	 => Number +	 -> m Boolean+nonnegative n = do+    return $ not $ last $ bits n++----------------------------------------------------++eq :: MonadSAT m +   => Number -> Number+   -> m Boolean+eq a b = do+    when ( width a /= width b ) +    	 $ error "Satchmo.Integer.Op.eq"+    eqs <- forM ( zip ( bits a ) ( bits b ) )+    	   $ \ (x,y) -> fun2 (==) x y+    and eqs++gt :: MonadSAT m +   => Number -> Number+   -> m Boolean+gt a b = do+    diff <- and [ not $ last $ bits a, last $ bits b ]+    same <- fun2 (==) ( last $ bits a )	+     	     	       ( last $ bits b )+    g <- F.gt ( F.make $ bits a ) +      	      ( F.make $ bits b )+    monadic or [ return diff+    	       , and [ same, g ]+	       ]++ge :: MonadSAT m +   => Number -> Number+   -> m Boolean+ge a b = do+    diff <- and [ not $ last $ bits a, last $ bits b ]+    same <- fun2 (==) ( last $ bits a )	+     	     	       ( last $ bits b )+    g <- F.ge ( F.make $ bits a ) +      	      ( F.make $ bits b )+    monadic or [ return diff+    	       , and [ same, g ]+	       ]+
− Satchmo/Internal.hs 
@@ -1,78 +0,0 @@-module Satchmo.Internal --( SAT-, fresh, fresh_forall-, emit-, sat-)--where--import Satchmo.Data--import Control.Monad.State.Strict-import Control.Monad.Writer.Strict--data Quantified = Forall [ Int ] | Exists [ Int ]--data Accu = Accu -          { next :: ! Int-          , quantified :: [ Quantified ]-          , size :: ! Int-          }--start :: Accu-start = Accu -      { next = 1-      , quantified = []-      , size = 0-      }--type SAT a = WriterT [ Clause ] (State Accu) a--sat :: SAT a -> ( String, a )-sat m = -    let ~( ~(a,w), accu) = runState ( runWriterT m ) start-    in  ( unlines $ unwords [ "p", "cnf", show ( next accu - 1), show ( size accu ) ]-                  : do q <- reverse $ interesting $ quantified accu-                       return $ case q of -                           Forall xs -> unwords $ "a" : map show ( reverse xs ++ [0] )-                           Exists xs -> unwords $ "e" : map show ( reverse xs ++ [0] )-                  ++ map show w-        , a-        )-    -interesting [ Exists _ ] = []-interesting xs = xs---- | existentially quantified (implicitely so, before first fresh_forall)-fresh :: SAT Literal-fresh = do-    a <- get-    let n = next a-    let q = case quantified a of-              Exists xs : rest -> Exists (n : xs) : rest-              rest -> Exists [n] : rest-    put $ a { next = n + 1, quantified = q }-    return $ literal n---- | universally quantified-fresh_forall :: SAT Literal-fresh_forall = do-    a <- get-    let n = next a-    let q = case quantified a of-              Forall xs : rest -> Forall (n : xs) : rest-              rest -> Forall [n] : rest-    put $ a { next = n + 1, quantified = q }-    return $ literal n--emit :: Clause -> SAT ()-emit clause = do-    a <- get-    tell [ clause ]-    put $ a -        { size = size a + 1 -        }--
+ Satchmo/MonadSAT.hs view
@@ -0,0 +1,90 @@+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE FlexibleContexts, FlexibleInstances #-}+{-# LANGUAGE GeneralizedNewtypeDeriving #-}++module Satchmo.MonadSAT++( MonadSAT(..), Weight+)++where++import Satchmo.Data++import Control.Monad.Trans (lift)+import Control.Monad.Cont  (ContT)+import Control.Monad.List  (ListT)+import Control.Monad.Reader (ReaderT)+import qualified Control.Monad.State  as Lazy (StateT)+import qualified Control.Monad.Writer as Lazy (WriterT)+import qualified Control.Monad.RWS    as Lazy (RWST)+import qualified Control.Monad.State.Strict  as Strict (StateT)+import qualified Control.Monad.Writer.Strict as Strict (WriterT)+import qualified Control.Monad.RWS.Strict    as Strict (RWST)+import Data.Monoid++type Weight = Int++class (Functor m, Monad m) => MonadSAT m where+  fresh, fresh_forall :: m Literal+  emit  :: Clause -> m ()+  emitW :: Weight -> Clause -> m ()+++-- -------------------------------------------------------+-- MonadSAT liftings for standard monad transformers+-- -------------------------------------------------------++instance (Monad m, MonadSAT m) => MonadSAT (ListT m) where+  fresh = lift fresh+  fresh_forall = lift fresh_forall+  emit  = lift . emit+  emitW = (lift.) . emitW++instance (Monad m, MonadSAT m) => MonadSAT (ReaderT r m) where+  fresh = lift fresh+  fresh_forall = lift fresh_forall+  emit  = lift . emit+  emitW = (lift.) . emitW++instance (Monad m, MonadSAT m) => MonadSAT (Lazy.StateT s m) where+  fresh = lift fresh+  fresh_forall = lift fresh_forall+  emit  = lift . emit+  emitW = (lift.) . emitW++instance (Monad m, MonadSAT m, Monoid w) => MonadSAT (Lazy.RWST r w s m) where+  fresh = lift fresh+  fresh_forall = lift fresh_forall+  emit  = lift . emit+  emitW = (lift.) . emitW++instance (Monad m, MonadSAT m, Monoid w) => MonadSAT (Lazy.WriterT w m) where+  fresh = lift fresh+  fresh_forall = lift fresh_forall+  emit  = lift . emit+  emitW = (lift.) . emitW++instance (Monad m, MonadSAT m) => MonadSAT (Strict.StateT s m) where+  fresh = lift fresh+  fresh_forall = lift fresh_forall+  emit  = lift . emit+  emitW = (lift.) . emitW++instance (Monad m, MonadSAT m, Monoid w) => MonadSAT (Strict.RWST r w s m) where+  fresh = lift fresh+  fresh_forall = lift fresh_forall+  emit  = lift . emit+  emitW = (lift.) . emitW++instance (Monad m, MonadSAT m, Monoid w) => MonadSAT (Strict.WriterT w m) where+  fresh = lift fresh+  fresh_forall = lift fresh_forall+  emit  = lift . emit+  emitW = (lift.) . emitW++instance (Monad m, MonadSAT m) => MonadSAT (ContT s m) where+  fresh = lift fresh+  fresh_forall = lift fresh_forall+  emit  = lift . emit+  emitW = (lift.) . emitW
+ Satchmo/Polynomial.hs view
@@ -0,0 +1,137 @@+{-# language MultiParamTypeClasses #-}+{-# language FlexibleContexts      #-}+{-# language UndecidableInstances  #-}++module Satchmo.Polynomial ++( Number ()+, number, constant+, iszero, equals, ge, gt+, add, times+)++where++import Data.Map ( Map )+import qualified Data.Map as M++import Satchmo.SAT+import Satchmo.Boolean hiding ( constant )+import qualified Satchmo.Boolean +import Satchmo.Code++import qualified Satchmo.Binary.Op.Fixed as F++import Control.Monad ( forM )++-- | polynomial in one variable,+-- coefficients starting from degree zero+data Poly a = Poly [a] deriving ( Eq, Ord, Show )++type Number = Poly F.Number++-- Hohoho:+instance Decode a Integer => Decode ( Poly a ) Integer where+    decode ( Poly xs ) = do+        ys <- forM xs decode +        let base = 1000 -- well+        return $ if all ( < base ) ys+                 then foldr ( \ y o -> o * base + y ) 0 ys+                 else error "Satchmo.Polynomial.decode"++-- | this is sort of wrong:+-- null polynomial should have degree -infty+-- but this function will return -1+degree :: Poly a -> Int+degree ( Poly xs ) = pred $ length xs+++number :: MonadSAT m+       => Int -- ^ bits+       -> Int -- ^ degree+       -> m ( Poly F.Number )+number bits deg = do +    xs <- forM [ 0 .. deg ] $ \ i -> F.number bits+    return $ Poly xs++constant :: MonadSAT m+         => Integer+         -> m ( Poly F.Number )+constant 0 = return $ Poly []+constant c = do+    z <- F.constant 0+    o <- F.constant c+    return $ Poly [ z, o ]++iszero  ( Poly xs ) = do+    ns <- forM xs $ F.iszero+    Satchmo.Boolean.and ns++equals ( Poly xs ) ( Poly ys ) = do+          z <- F.constant 0+          let n = max ( length xs ) ( length ys )+              fill xs = take n $ xs ++ repeat z+          let handle xs ys = case ( xs, ys ) of+                  ( [], [] ) -> Satchmo.Boolean.constant True+                  (x:xs, y:ys) -> do+                      e <- F.equals x y+                      later <- handle xs ys+                      Satchmo.Boolean.and [ e, later ]+          handle ( reverse $ fill xs ) ( reverse $ fill ys )++ge ( Poly xs ) ( Poly ys ) = do+          z <- F.constant 0+          let n = max ( length xs ) ( length ys )+              fill xs = take n $ xs ++ repeat z+          let handle xs ys = case ( xs, ys ) of+                  ( [], [] ) -> Satchmo.Boolean.constant True+                  (x:xs, y:ys) -> do+                      gt <- F.gt x y+                      e <- F.equals x y+                      later <- handle xs ys+                      monadic Satchmo.Boolean.or +                              [ return gt+                              , Satchmo.Boolean.and [ e, later ]+                              ]+          handle ( reverse $ fill xs ) ( reverse $ fill ys )++gt  ( Poly xs ) ( Poly ys ) = do+          z <- F.constant 0+          let n = max ( length xs ) ( length ys )+              fill xs = take n $ xs ++ repeat z+          let handle xs ys = case ( xs, ys ) of+                  ( [], [] ) -> Satchmo.Boolean.constant False+                  (x:xs, y:ys) -> do+                      gt <- F.gt x y+                      e <- F.equals x y+                      later <- handle xs ys+                      monadic Satchmo.Boolean.or +                              [ return gt+                              , Satchmo.Boolean.and [ e, later ]+                              ]+          handle ( reverse $ fill xs ) ( reverse $ fill ys )+++add ( Poly xs ) ( Poly ys ) = do+          let handle xs ys = case ( xs, ys ) of+                  ( [] , ys ) ->  return ys+                  ( xs, [] ) -> return xs+                  (x:xs, y:ys) -> do+                      z <- F.add x y+                      zs <- handle xs ys+                      return $ z : zs+          zs <- handle xs ys+          return $ Poly zs++times p q = do+          let handle ( Poly xs ) ( Poly ys ) = +                  case ( xs, ys ) of+                      ( [], ys ) -> return $ Poly []+                      ( xs, [] ) -> return $ Poly []+                      ( x : xs, ys ) -> do+                          Poly zs <- handle ( Poly xs ) ( Poly ys )+                          f : fs  <- forM ys $ F.times x+                          Poly rest <- add ( Poly zs ) ( Poly fs )+                          return $ Poly $ f : rest+          handle p q+
Satchmo/Relation/Data.hs view
@@ -3,7 +3,7 @@ module Satchmo.Relation.Data  ( Relation, relation, build-, bounds, (!), indices+, bounds, (!), indices, assocs , table )  @@ -13,14 +13,14 @@ import Satchmo.Boolean  import qualified Data.Array as A-import Data.Array hiding ( bounds, (!), indices )+import Data.Array hiding ( bounds, (!), indices, assocs )  import Control.Monad ( guard )  data Relation a b = Relation ( Array (a,b) Boolean )  -relation :: ( Ix a, Ix b ) -         => ((a,b),(a,b)) -> SAT ( Relation a b ) +relation :: ( Ix a, Ix b, MonadSAT m ) +         => ((a,b),(a,b)) -> m ( Relation a b )  relation bnd = do     pairs <- sequence $ do          p <- range bnd@@ -39,6 +39,9 @@ bounds ( Relation r ) = A.bounds r  indices ( Relation r ) = A.indices r++assocs ( Relation r ) = A.assocs r+  Relation r ! p = r A.! p
Satchmo/Relation/Op.hs view
@@ -6,6 +6,7 @@ , union , complement , product+, intersection )   where@@ -30,17 +31,17 @@ complement r =      build (bounds r) $ do i <- indices r ; return ( i, not $ r!i ) -union :: ( Ix a , Ix b ) +union :: ( Ix a , Ix b, MonadSAT m )        => Relation a b -> Relation a b -      -> SAT ( Relation a b )+      -> m ( Relation a b ) union r s = do     pairs <- sequence $ do         i <- indices r         return $ do o <- or [ r!i, s!i ] ; return ( i, o )     return $ build ( bounds r ) pairs -product :: ( Ix a , Ix b, Enum b, Ix c ) -        => Relation a b -> Relation b c -> SAT ( Relation a c )+product :: ( Ix a , Ix b, Ix c, MonadSAT m ) +        => Relation a b -> Relation b c -> m ( Relation a c ) product a b = do     let ((ao,al),(au,ar)) = bounds a         ((bo,bl),(bu,br)) = bounds b@@ -49,9 +50,18 @@         i @ (x,z) <- range bnd         return $ do             o <- monadic or $ do-                y <- [ al .. ar ]+                y <- range ( al, ar )                 return $ and [ a!(x,y), b!(y,z) ]             return ( i, o )     return $ build bnd pairs++intersection :: ( Ix a , Ix b, MonadSAT m ) +      => Relation a b -> Relation a b +      -> m ( Relation a b )+intersection r s = do+    pairs <- sequence $ do+        i <- indices r+        return $ do a <- and [ r!i, s!i ] ; return ( i, a )+    return $ build ( bounds r ) pairs
Satchmo/Relation/Prop.hs view
@@ -4,6 +4,7 @@ , symmetric  , transitive , irreflexive+, reflexive , regular ) @@ -21,31 +22,38 @@ import Control.Monad ( guard ) import Data.Ix -implies :: ( Ix a, Ix b ) => Relation a b -> Relation a b -> SAT Boolean+implies :: ( Ix a, Ix b, MonadSAT m ) +        => Relation a b -> Relation a b -> m Boolean implies r s = monadic and $ do     i <- indices r     return $ or [ not $ r ! i, s ! i ]  -symmetric :: (Enum a, Ix a) => Relation a a -> SAT Boolean+symmetric :: ( Ix a, MonadSAT m) => Relation a a -> m Boolean symmetric r = implies r ( mirror r ) -irreflexive :: (Enum a, Ix a) => Relation a a -> SAT Boolean+irreflexive :: ( Ix a, MonadSAT m) => Relation a a -> m Boolean irreflexive r = and $ do     let ((a,b),(c,d)) = bounds r-    x <- [a .. c]+    x <- range ( a, c)     return $ Satchmo.Boolean.not $ r ! (x,x)  -regular :: (Enum a, Ix a) => Int -> Relation a a -> SAT Boolean+reflexive :: ( Ix a, MonadSAT m) => Relation a a -> m 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 regular deg r = monadic and $ do     let ((a,b),(c,d)) = bounds r-    x <- [ a .. c ]+    x <- range ( a , c )     return $ exactly deg $ do -        y <- [ b .. d ]+        y <- range (b,d)         return $ r !(x,y) -transitive :: ( Enum a, Ix a ) -           => Relation a a -> SAT Boolean+transitive :: ( Ix a, MonadSAT m ) +           => Relation a a -> m Boolean transitive r = do     r2 <- product r r     implies r2 r
+ Satchmo/SAT.hs view
@@ -0,0 +1,101 @@+{-# 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}+
+ Satchmo/SAT/Weighted.hs view
@@ -0,0 +1,88 @@+{-# LANGUAGE GeneralizedNewtypeDeriving #-}+module Satchmo.SAT.Weighted (SAT, sat, MaxWeight, Header(..)) where++import Satchmo.Data+import Satchmo.MonadSAT++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 System.Directory+import System.Environment+import System.IO+++instance MonadSAT SAT where+  fresh = satfresh+  fresh_forall = satfresh_forall+  emit  = satemit Nothing+  emitW = satemit . Just++-- ---------------+-- Implementation+-- ---------------++data Accu = Accu+          { next :: ! Int+          , universal :: [Int]+          , size :: ! Int+          }++start :: Accu+start = Accu+      { next = 1+      , universal = []+      , size = 0+      }++type MaxWeight  = Int++newtype SAT a = SAT {unsat::RWST (Handle, MaxWeight) () Accu IO a}+    deriving (MonadState Accu, MonadReader (Handle, MaxWeight), Monad, MonadIO, Functor)++data Header = Header { numClauses, numVars, maxWeight :: Int+                     , universals :: [Int]+                     }++sat :: MaxWeight -> SAT a -> IO (BS.ByteString, Header, a )+sat maxW (SAT m) =+ bracket+    (getTemporaryDirectory >>= (`openTempFile`  "satchmo"))+    (\(fp, h) -> removeFile fp)+    (\(fp, h) -> do+       hSetBuffering h (BlockBuffering Nothing)+       ~(a, accu, _) <- runRWST m (h, maxW) start+       hClose h+       let header = Header (size accu) (next accu - 1) maxW 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 :: Maybe Weight -> Clause -> SAT ()+satemit w (Clause clause) = do+    a <- get+    (h,maxW) <- ask+    liftIO $ BS.hPut h (bshowClause $ Clause(Literal (fromMaybe maxW w) : clause))+    put $ a { size = size a + 1}++  where bshowClause c = BS.pack (show c) `mappend` BS.pack "\n"+
+ Satchmo/Simple.hs view
@@ -0,0 +1,30 @@+{-# language GeneralizedNewtypeDeriving #-}++module Satchmo.Simple where++import Satchmo.MonadSAT+import Satchmo.Data++import Control.Monad.State++data Accu = Accu { next :: ! Int+                 , pool :: [ Clause ]+                 }++start = Accu { next = 0, pool = [] }++sat (SAT m) = flip evalState start+            $ do x <- m; a <- get ; return (cnf $ pool a, x) ++newtype SAT a = SAT { unsat :: State Accu a } +    deriving ( Functor, Monad )++instance MonadSAT SAT where+    fresh = SAT $ do +          a <- get ; let n = succ $ next a +          put $ a { next = n } ; return $ Literal n+    emit c = SAT $ do+          modify $ \ a -> a { pool = c : pool a }+++
Satchmo/Solve.hs view
@@ -3,8 +3,8 @@  module Satchmo.Solve -( solve-, Implementation+( solve, solveW+, Implementation, WeightedImplementation , Decoder ) @@ -12,28 +12,50 @@  import Satchmo.Data import Satchmo.Code-import Satchmo.Internal+import Satchmo.SAT+import qualified Satchmo.SAT.Weighted as Weighted +import qualified Data.ByteString.Lazy.Char8 as BS import Data.Map ( Map ) import qualified Data.Map as M -import Control.Monad.State import Control.Monad.Reader -type Implementation = String -> IO ( Maybe ( Map Literal Bool ) )+import System.IO -solve :: Implementation-      -> SAT ( Decoder a )-    -> IO ( Maybe a )+type Implementation = BS.ByteString +                    -> Header +                    -> IO ( Maybe ( Map Variable Bool ) )++type WeightedImplementation = BS.ByteString +                            -> Weighted.Header +                            -> IO ( Maybe ( Map Variable Bool ) )++solve :: Implementation +      -> SAT ( Decoder a ) +      -> IO ( Maybe a ) solve implementation build = do-    let (s, a) = sat build-    mfm <- implementation s+    (s, h, a) <- sat build+    mfm <- implementation s h     case mfm of         Nothing -> do-            putStrLn "not satisfiable"+            hPutStrLn stderr "not satisfiable"             return Nothing         Just fm -> do-            putStrLn "satisfiable"-            -- print fm+            hPutStrLn stderr "satisfiable"             return $ Just $ runReader a fm-                ++solveW :: Weighted.MaxWeight +       -> WeightedImplementation +       -> Weighted.SAT (Decoder a) +       -> IO (Maybe a)+solveW maxW implementation build = do+    (s, h, a) <- Weighted.sat maxW build+    mfm <- implementation s h+    case mfm of+        Nothing -> do+            hPutStrLn stderr "not satisfiable"+            return Nothing+        Just fm -> do+            hPutStrLn stderr "satisfiable"+            return $ Just $ runReader a fm
satchmo.cabal view
@@ -1,17 +1,19 @@ Name:           satchmo-Version:        1.4+Version:        1.8.0  License:        GPL License-file:	gpl-2.0.txt-Author:         Johannes Waldmann+Author:         Pepe Iborra, Johannes Waldmann Maintainer:	Johannes Waldmann Homepage:       http://dfa.imn.htwk-leipzig.de/satchmo/+		http://github.com/pepeiborra/satchmo/ Synopsis:       SAT encoding monad description:	Encoding for boolean and integral constraints into (QBF-)CNF-SAT. 		The encoder is provided as a State monad (hence the "mo" in "satchmo").-		requires a backend (e.g. satchmo-backends, satchmo-funsat)+		This package contains functions that construct problems,+                to solve them, you need package satchmo-backends. Category:	Algorithms-Build-depends:  mtl, process, containers, base, array+Build-depends:  mtl, process, containers, base >= 3 && <= 4, array, bytestring, directory Exposed-modules: 	Satchmo.Data         Satchmo.Solve@@ -19,18 +21,27 @@ 	Satchmo.Counting 	Satchmo.Code 	Satchmo.Binary+	Satchmo.Integer 	Satchmo.Binary.Op.Common 	Satchmo.Binary.Op.Fixed 	Satchmo.Binary.Op.Flexible+	Satchmo.Polynomial 	Satchmo.Relation 	Satchmo.Relation.Data 	Satchmo.Relation.Op 	Satchmo.Relation.Prop+	Satchmo.MonadSAT+	Satchmo.SAT+	Satchmo.Simple+	Satchmo.SAT.Weighted Other-modules: 	Satchmo.Binary.Data+	Satchmo.Integer.Data         Satchmo.Boolean.Op+        Satchmo.Integer.Op         Satchmo.Boolean.Data-	Satchmo.Internal hs-source-dirs:	. extensions:  build-type: Simple+ghc-options: -funbox-strict-fields+ghc-prof-options: -auto