satchmo 1.1.1 → 1.2

raw patch · 8 files changed

+120/−34 lines, 8 files

Files

• Satchmo/Binary/Data.hs +0/−17
• Satchmo/Binary/Op/Common.hs +50/−0
• Satchmo/Binary/Op/Fixed.hs +8/−4
• Satchmo/Binary/Op/Flexible.hs +8/−4
• Satchmo/Boolean/Op.hs +46/−5
• satchmo.cabal +2/−1
• test/Binary.hs +1/−1
• test/VC.hs +5/−2

@@ -4,7 +4,6 @@  ( Number, bits, make , width, number, constant-, equals, iszero )  where@@ -55,20 +54,4 @@ constant n = do     xs <- mapM B.constant $ toBinary n     return $ make xs--iszero :: Number -> SAT Boolean-iszero a = equals a $ make []--equals :: Number -> Number -> SAT Boolean-equals a b = do-    equals' ( bits a ) ( bits b )--equals' :: Booleans -> Booleans -> SAT 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 

@@ -0,0 +1,50 @@+module Satchmo.Binary.Op.Common++( iszero+, equals+, full_adder, half_adder+)++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.Binary.Data++import Satchmo.Counting++iszero :: Number -> SAT Boolean+iszero a = equals a $ make []++equals :: Number -> Number -> SAT Boolean+equals a b = do+    equals' ( bits a ) ( bits b )++equals' :: Booleans -> Booleans -> SAT 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++full_adder :: Boolean -> Boolean -> Boolean+           -> SAT ( Boolean, Boolean )+full_adder 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+    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+    return ( r, d )

@@ -11,6 +11,7 @@ ( restricted , add, times , module Satchmo.Binary.Data+, module Satchmo.Binary.Op.Common )  where@@ -21,6 +22,7 @@  import Satchmo.Boolean import Satchmo.Binary.Data+import Satchmo.Binary.Op.Common import qualified Satchmo.Binary.Op.Flexible as Flexible  import Satchmo.Counting@@ -49,14 +51,16 @@         return []     ( [] , [] ) -> return [ c ]     ( [], y : ys) -> do-        r <- xor [ c, y ]-        d <- and [ c, y ]+        -- 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 <- 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 

@@ -8,6 +8,7 @@ ( add, times , add_with_carry, times1, shift , module Satchmo.Binary.Data+, module Satchmo.Binary.Op.Common )  where@@ -17,6 +18,7 @@ import Satchmo.Boolean import qualified Satchmo.Code as C import Satchmo.Binary.Data+import Satchmo.Binary.Op.Common import Satchmo.Counting  add :: Number -> Number -> SAT Number@@ -30,15 +32,17 @@                -> SAT ( Booleans, Boolean ) add_with_carry cin [] [] = return ( [], cin ) add_with_carry cin (x:xs) [] = do-    z <- xor [ cin, x ]-    c <- and [ cin, x ]+    -- 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  <- 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 ) 

@@ -2,17 +2,21 @@  ( constant , and, or, xor+, fun2, fun3 , monadic )  where  import Prelude hiding ( and, or, not )+import qualified Prelude  import Satchmo.Internal import Satchmo.Code import Satchmo.Boolean.Data +import Control.Monad ( foldM )+ and :: [ Boolean ] -> SAT Boolean and xs = do     y <- boolean@@ -28,14 +32,51 @@     return $ not y  xor :: [ Boolean ] -> SAT Boolean-xor [x] = return x-xor (x : xs) = do-    rest <- xor xs-    xor2 x rest+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 )+     -> Boolean -> Boolean +     -> SAT Boolean+fun2 f x y = do+    r <- boolean+    sequence_ $ do+        a <- [ False, True ]+        b <- [ False, True ]+        let pack flag var = if flag then not var else var+        return $ assert +            [ pack a x, pack b y, pack (Prelude.not $ f a b) r ]+    return r++-- | implement the function by giving a full CNF+-- that determines the outcome+fun3 :: ( Bool -> Bool -> Bool -> Bool )+     -> Boolean -> Boolean -> Boolean+     -> SAT Boolean+fun3 f x y z = do+    r <- boolean+    sequence_ $ do+        a <- [ False, True ]+        b <- [ False, True ]+        c <- [ False, True ]+        let pack flag var = if flag then not var else var+        return $ assert +            [ pack a x, pack b y, pack c z+            , pack (Prelude.not $ f a b c) r +            ]+    return r+ xor2 :: Boolean -> Boolean -> SAT Boolean-xor2 x y = do+xor2 = fun2 (/=)++-- for historic reasons:+xor2_orig :: Boolean -> Boolean -> SAT Boolean+xor2_orig x y = do     a <- and [ x, not y ]     b <- and [ not x, y ]     or [ a, b ]+ 

@@ -1,5 +1,5 @@ Name:           satchmo-Version:        1.1.1+Version:        1.2 License:        GPL License-file:	gpl-2.0.txt Author:         Johannes Waldmann@@ -16,6 +16,7 @@ 	Satchmo.Counting 	Satchmo.Code 	Satchmo.Binary+	Satchmo.Binary.Op.Common 	Satchmo.Binary.Op.Fixed 	Satchmo.Binary.Op.Flexible Other-modules:

@@ -1,4 +1,4 @@--- | run tests like this: "solve test2"+-- | run tests (in ghci) like this: "solve test2"  import Prelude hiding ( not ) 

@@ -18,12 +18,15 @@     argv <- getArgs     let [ n, s ] = map read argv     -- this is just to check whether time-outing works-    Just (Just a) <- timeout (10^6) $ solve $ knight n s+    -- Just (Just a) <- timeout (10^6) $ solve $ knight n s++    Just a <- solve $ knight n s     putStrLn $ table a  knight n s = do     a <- relation ((1,1),(n,n))-    m <- atmost s $ do i <- indices a ; return $ a ! i+    m <- atmost s $ do +           i <- indices a ; return $ a ! i     assert [m]     sequence_ $ do         p <- indices a