satchmo 2.8.2 → 2.9.0

raw patch · 9 files changed

+234/−97 lines, 9 filesPVP ok

version bump matches the API change (PVP)

API changes (from Hackage documentation)

Files

• Satchmo/Binary/Op/Times.hs +41/−27
• Satchmo/Counting.hs +6/−54
• Satchmo/Counting/Binary.hs +51/−0
• Satchmo/Counting/Unary.hs +59/−0
• Satchmo/Integer/Data.hs +12/−2
• Satchmo/Integer/Op.hs +58/−11
• Satchmo/Map/Data.hs +4/−0
• Satchmo/Set/Data.hs +0/−2
• satchmo.cabal +3/−1

@@ -1,5 +1,11 @@-module Satchmo.Binary.Op.Times where+module Satchmo.Binary.Op.Times +( times, dot_product+, Overflow (..), times'+)++where+ import Prelude hiding ( and, or, not )  import Satchmo.Boolean@@ -9,65 +15,73 @@  import qualified Data.Map as M import Control.Monad ( forM )-+import Control.Applicative  dot_product :: (MonadSAT m)               => ( Maybe Int)              -> [ Number ] -> [ Number ] -> m Number dot_product bound xs ys = do-    cs <- forM ( zip xs ys ) $ \ (x,y) -> product_components bound x y-    export bound $ concat cs+    cs <- forM ( zip xs ys ) $ \ (x,y) -> product_components Refuse bound (bits x) (bits y)+    make <$> export Refuse bound ( concat cs ) +data Overflow = Ignore | Refuse+ times :: (MonadSAT m)               => Maybe Int              -> Number -> Number -> m Number-times bound a b = do-    kzs <- product_components bound a b-    export bound kzs+times bound a b =+  make <$> times' Refuse bound (bits a) (bits b) -product_components :: MonadSAT m-    => Maybe Int-    -> Number -> Number -> m [ (Int, [Boolean]) ]-product_components bound a b = sequence $ do-    ( i , x ) <- zip [ 0 .. ] $ bits a-    ( j , y ) <- zip [ 0 .. ] $ bits b        +times' over bound a b = do+    kzs <- product_components over bound a b+    export over bound kzs++product_components over bound a b = sequence $ do+    ( i , x ) <- zip [ 0 .. ] a+    ( j , y ) <- zip [ 0 .. ] b             return $ do         z <- and [ x, y ]         if ( case bound of Nothing -> False ; Just b -> i+j >= b )-             then do assert [ not z ] ; return ( i+j , [ ] )-             else do                    return ( i+j , [z] ) +             then do+                case over of+                  Ignore -> return ()+                  Refuse -> assert [ not z ]+                return ( i+j , [ ] )+             else do+                return ( i+j , [z] )  -export :: MonadSAT m => Maybe Int -> [(Int,[Boolean])] -> m Number-export bound kzs = do -    m <- reduce bound $ M.fromListWith (++) kzs+export over bound kzs = do +    m <- reduce over bound $ M.fromListWith (++) kzs     case M.maxViewWithKey m of-        Nothing -> return $ make []+        Nothing -> return []         Just ((k,_) , _) -> do -              return $ make $ do +              return $ do                      i <- [ 0 .. k ]                      let { [ b ] = m M.! i }                       return b -reduce bound m = case M.minViewWithKey m of+reduce over bound m = case M.minViewWithKey m of     Nothing -> return M.empty     Just ((k, bs), rest ) ->          if ( case bound of Nothing -> False ; Just b -> k >= b )         then do-            forM bs $ \ b -> assert [ not b ]-            reduce bound rest+            forM bs $ \ b -> case over of+              Refuse -> assert [ not b ]+              Ignore -> return ()+            reduce over bound rest         else case bs of-            [] -> reduce bound rest+            [] -> reduce over bound rest             [x] -> do-                m' <- reduce bound rest+                m' <- reduce over bound rest                 return $ M.unionWith (error "huh") m'                         $ M.fromList [(k,[x])]              [x,y] -> do                 (r,c) <- half_adder x y-                reduce bound $ M.unionWith (++) rest+                reduce over bound $ M.unionWith (++) rest                        $ M.fromList [ (k,[r]), (k+1, [c]) ]              (x:y:z:more) -> do                 (r,c) <- full_adder x y z-                reduce bound $ M.unionWith (++) rest+                reduce over bound $ M.unionWith (++) rest                        $ M.fromList [ (k, more ++ [r]), (k+1, [c]) ]   

@@ -1,59 +1,11 @@-module Satchmo.Counting --( atleast-, atmost-, exactly-)--where--import Prelude hiding ( and, or, not )--import Satchmo.Boolean--import Satchmo.SAT ( SAT) -- for specializations--{-# specialize inline atleast :: Int -> [ Boolean] -> SAT Boolean #-}-{-# specialize inline atmost  :: Int -> [ Boolean] -> SAT Boolean #-}-{-# specialize inline exactly :: Int -> [ Boolean] -> SAT Boolean #-}+-- | Re-exports @Satchmo.Counting.Unary@+-- for backwards compatibility. -atleast :: MonadSAT m => Int -> [ Boolean ] -> m Boolean-atleast k xs = fmap not $ atmost (k-1) xs-        +module Satchmo.Counting -atmost_block :: MonadSAT m => Int -> [ Boolean ] -> m [ Boolean ]-atmost_block k [] = do-    t <- constant $ True-    return $ replicate (k+1) t-atmost_block k (x:xs) = do-    cs <- atmost_block k xs-    f <- constant False-    sequence $ do-        (p,q) <- zip cs ( f : cs )-        return $ do-            fun3  ( \ x p q -> if x then q else p ) x p q+( module Satchmo.Counting.Unary ) -atmost :: MonadSAT m => Int -> [ Boolean ] -> m Boolean-atmost k xs = do-    cs <- atmost_block k xs-    return $ cs !! k-        +where -exactly_block :: MonadSAT m => Int -> [ Boolean ] -> m [ Boolean ]-exactly_block k [] = do-    t <- constant True-    f <- constant False-    return $ t : replicate k f-exactly_block k (x:xs) = do-    f <- constant False-    cs <- exactly_block k xs-    sequence $ do-        (p,q) <- zip cs ( f : cs )-        return $ do-            fun3 ( \ x p q -> if x then q else p ) x p q+import Satchmo.Counting.Unary -exactly :: MonadSAT m => Int -> [ Boolean ] -> m Boolean-exactly k xs = do-    cs <- exactly_block k xs-    return $ cs !! k-        

@@ -0,0 +1,51 @@+module Satchmo.Counting.Binary++( atleast+, atmost+, exactly+, count+)++where++import Prelude hiding ( and, or, not )++import Satchmo.Boolean+import Satchmo.Binary++import Satchmo.SAT ( SAT) -- for specializations++{-# specialize inline atleast :: Int -> [ Boolean] -> SAT Boolean #-}+{-# specialize inline atmost  :: Int -> [ Boolean] -> SAT Boolean #-}+{-# specialize inline exactly :: Int -> [ Boolean] -> SAT Boolean #-}+{-# specialize inline count :: [ Boolean] -> SAT Number #-}++count :: MonadSAT m => [ Boolean ] -> m Number+count bits+  = collect (Satchmo.Binary.constant 0) Satchmo.Binary.add+  $ map ( \ bit -> Satchmo.Binary.make [bit] )+  $ bits++collect :: Monad m => m a -> (a -> a -> m a) -> [a] -> m a+collect z b xs = case xs of+  [] -> z+  [x] -> return x+  (x:y:zs) -> b x y >>= \ c -> collect z b (zs ++ [c])+    +atleast :: MonadSAT m => Int -> [ Boolean ] -> m Boolean+atleast k xs = common ge k xs++atmost :: MonadSAT m => Int -> [ Boolean ] -> m Boolean+atmost k xs = common le k xs+        +exactly :: MonadSAT m => Int -> [ Boolean ] -> m Boolean+exactly k xs = common eq k xs++common :: MonadSAT m+       => (Number -> Number -> m b)+       -> Int -> [ Boolean ] -> m b+common cmp k xs = do+  c <- count xs+  goal <- Satchmo.Binary.constant $ fromIntegral k+  cmp c goal +

@@ -0,0 +1,59 @@+module Satchmo.Counting.Unary++( atleast+, atmost+, exactly+)++where++import Prelude hiding ( and, or, not )++import Satchmo.Boolean++import Satchmo.SAT ( SAT) -- for specializations++{-# specialize inline atleast :: Int -> [ Boolean] -> SAT Boolean #-}+{-# specialize inline atmost  :: Int -> [ Boolean] -> SAT Boolean #-}+{-# specialize inline exactly :: Int -> [ Boolean] -> SAT Boolean #-}++atleast :: MonadSAT m => Int -> [ Boolean ] -> m Boolean+atleast k xs = fmap not $ atmost (k-1) xs+        ++atmost_block :: MonadSAT m => Int -> [ Boolean ] -> m [ Boolean ]+atmost_block k [] = do+    t <- constant $ True+    return $ replicate (k+1) t+atmost_block k (x:xs) = do+    cs <- atmost_block k xs+    f <- constant False+    sequence $ do+        (p,q) <- zip cs ( f : cs )+        return $ do+            fun3  ( \ x p q -> if x then q else p ) x p q++atmost :: MonadSAT m => Int -> [ Boolean ] -> m Boolean+atmost k xs = do+    cs <- atmost_block k xs+    return $ cs !! k+        ++exactly_block :: MonadSAT m => Int -> [ Boolean ] -> m [ Boolean ]+exactly_block k [] = do+    t <- constant True+    f <- constant False+    return $ t : replicate k f+exactly_block k (x:xs) = do+    f <- constant False+    cs <- exactly_block k xs+    sequence $ do+        (p,q) <- zip cs ( f : cs )+        return $ do+            fun3 ( \ x p q -> if x then q else p ) x p q++exactly :: MonadSAT m => Int -> [ Boolean ] -> m Boolean+exactly k xs = do+    cs <- exactly_block k xs+    return $ cs !! k+        

@@ -3,8 +3,8 @@ module Satchmo.Integer.Data   ( Number, make, number-, constant-, bits, width+, constant, decode+, bits, width, sign )  where@@ -18,6 +18,7 @@ import qualified  Satchmo.Boolean as B  import Satchmo.Counting+import Control.Monad  data Number = Number              { bits :: [ Boolean ] -- ^ lsb first,@@ -30,6 +31,11 @@ width :: Number -> Int width n = length $ bits n +sign :: Number -> Boolean+sign n = case bits n of+  [] -> error "Satchmo.Integer.Data:sign no bits"+  bs -> last bs+ -- | declare a number variable (bit width) number :: MonadSAT m => Int -> m Number number w = do@@ -64,3 +70,7 @@     z <- B.constant False     return $ make $ take w $ xs ++ repeat z +decode w n = do+  bs <- forM (bits n) C.decode+  return $ fromBinary bs+         - if last bs then 2^w else 0

@@ -16,6 +16,7 @@  import qualified Satchmo.Binary.Op.Common as C import qualified Satchmo.Binary.Op.Flexible as F+import qualified Satchmo.Binary.Op.Times as T  import Control.Monad ( forM, when ) @@ -38,14 +39,19 @@ add :: MonadSAT m      => Number -> Number      -> m Number-add a b = do-    when ( width a /= width b ) -    	 $ error "Satchmo.Integer.Op.add"+add a0 b0 = do++    let w = max (width a0) (width b0)+        a = sextn w a0 ; b = sextn w b0+     cin <- B.constant False     ( zs, cout ) <-          F.add_with_carry cin ( bits a ) ( bits b )-    monadic assertOr [ fun2 (==) cout $ last zs ]-    return $ make zs+    let c = make zs+    sab <- B.fun2 (==) (sign a) (sign b)+    sac <- B.fun2 (==) (sign a) (sign c)+    B.assert [ B.not sab , sac ]+    return c  sub :: MonadSAT m      => Number -> Number @@ -56,17 +62,58 @@     c <- negate b     add a c +sextn w n = make $ sext n w+ times :: MonadSAT m      => Number -> Number      -> m Number-times a b = do+times a0 b0 = do++    let w = max (width a0) (width b0)+        a = sextn w a0 ; b = sextn w b0+        +    cs <- T.times' T.Ignore (Just w) (bits a) (bits b)++    nza <- or $ bits a ; nzb <- or $ bits b+    result_should_be_nonzero <- and [ nza, nzb ]+    result_is_nonzero <- or cs++    assert [ not result_should_be_nonzero, result_is_nonzero ]++    xs <- forM (bits a) $ \ x -> fun2 (/=) x (sign a)+    ys <- forM (bits b) $ \ y -> fun2 (/=) y (sign b)+    +    forM (zip [0..w-2] xs) $ \ (i,x) ->+      forM (zip [0..w-2] ys) $ \ (j,y) ->+        when (i+j>=w-1) $ assert [ not x, not y ]++    let c = make cs++    s <- fun2 (/=) (sign a) (sign b)+    ok <- fun2 (==) s (sign c)+    +    assert [ not result_is_nonzero, ok ]+    +    return c++-- | inefficient (used double-bit width computation)+times_model :: MonadSAT m +    => Number -> Number +    -> m Number+times_model 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 assertOr [ fun2 (==) ( head post) $ last pre ]-    return $ make pre+    let w = width a+    cs <- T.times' T.Ignore (Just (2*w)) (sext a w) (sext b w)+    let (small, large) = splitAt w cs+    allone <- B.and large ; allzero <- B.and ( map B.not large )+    B.assert [ allone, allzero ]+    e <- B.fun2 (==) (last small) (head large)+    B.assert[e]+    return $ make small++sext a w = bits a ++ replicate (w - width a) (sign a)+      ---------------------------------------------------- 

@@ -4,6 +4,8 @@ module Satchmo.Map.Data  ( Map+, unknown, constant+, (!),  )   where@@ -20,6 +22,8 @@ import Control.Applicative ( (<$>), (<*>) )  newtype Map a b = Map (M.Map a b)++Map m ! i = m M.! i  instance ( Functor m, Decode m b c, Ord a )          => Decode m (Map a b) ( M.Map a c) where

@@ -18,8 +18,6 @@ import qualified Data.Set as S import qualified Data.Map.Strict as M -import Satchmo.Map- import Control.Monad ( guard, forM ) import Control.Applicative ( (<$>), (<*>) ) import Data.List ( tails )

@@ -1,5 +1,5 @@ Name:           satchmo-Version:        2.8.2+Version:        2.9.0  License:        GPL License-file:	gpl-2.0.txt@@ -28,6 +28,8 @@         -- Satchmo.Solve         Satchmo.Boolean         Satchmo.Counting+        Satchmo.Counting.Unary+        Satchmo.Counting.Binary         Satchmo.Code         Satchmo.Integer         Satchmo.Binary