satchmo 2.9.9.1 → 2.9.9.3

raw patch · 13 files changed

+236/−19 lines, 13 filesdep ~base

Dependency ranges changed: base

Files

• Satchmo/Binary/Data.hs +2/−2
• Satchmo/Binary/Op/Common.hs +1/−1
• Satchmo/Binary/Op/Flexible.hs +1/−1
• Satchmo/BinaryTwosComplement/Data.hs +1/−1
• Satchmo/Counting.hs +5/−4
• Satchmo/Integer/Data.hs +1/−1
• Satchmo/MonadSAT.hs +5/−0
• Satchmo/Relation/Data.hs +13/−1
• Satchmo/Relation/Prop.hs +48/−4
• Satchmo/Unary/Data.hs +2/−2
• examples/Moore.hs +72/−0
• examples/Sudoku.hs +69/−0
• satchmo.cabal +16/−2

@@ -17,13 +17,13 @@ import Satchmo.Boolean hiding ( constant ) import qualified  Satchmo.Boolean as B -import Satchmo.Counting+-- import Satchmo.Counting  data Number = Number              { bits :: [ Boolean ] -- lsb first             } -instance C.Decode m Boolean Bool => C.Decode m Number Integer where+instance (Monad m, C.Decode m Boolean Bool) => C.Decode m Number Integer where     decode n = do ys <- mapM C.decode (bits n) ; return $ fromBinary ys  width :: Number -> Int

@@ -22,7 +22,7 @@  import Control.Monad ( forM, foldM ) -import Satchmo.Counting+-- import Satchmo.Counting  import Control.Monad ( forM ) 

@@ -20,7 +20,7 @@ import Satchmo.Binary.Data import Satchmo.Binary.Op.Common import qualified Satchmo.Binary.Op.Times as T-import Satchmo.Counting+import Satchmo.Counting.Unary  import qualified Data.Map as M 

@@ -20,7 +20,7 @@             }  -instance C.Decode m Boolean Bool => C.Decode m Number Integer where+instance (Monad m, C.Decode m Boolean Bool) => C.Decode m Number Integer where     decode n = do bs <- C.decode $ bits n ; return $ fromBinary bs  -- | Make a number from its binary representation

@@ -1,11 +1,12 @@--- | Re-exports @Satchmo.Counting.Unary@--- for backwards compatibility.+-- | Re-exports @Satchmo.Binary.Counting@+-- because that implementation seems best overall.  module Satchmo.Counting -( module Satchmo.Counting.Unary )+( module Satchmo.Counting.Binary )  where -import Satchmo.Counting.Unary+import Satchmo.Counting.Binary+ 

@@ -25,7 +25,7 @@ 	         -- using two's complement             } -instance C.Decode m Boolean Bool => C.Decode m Number Integer where+instance (Monad m, C.Decode m Boolean Bool) => C.Decode m Number Integer where     decode n = do ys <- mapM C.decode (bits n) ; return $ fromBinary ys  width :: Number -> Int

@@ -1,8 +1,13 @@+{-# LANGUAGE CPP #-} {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE FlexibleContexts, FlexibleInstances #-} {-# LANGUAGE GeneralizedNewtypeDeriving #-} {-# LANGUAGE TypeFamilies #-} ++#if (__GLASGOW_HASKELL__ >= 708)+{-# LANGUAGE AllowAmbiguousTypes #-}+#endif  module Satchmo.MonadSAT 

@@ -2,7 +2,9 @@  module Satchmo.Relation.Data -( Relation, relation, build+( Relation+, relation, symmetric_relation+, build , identity                       , bounds, (!), indices, assocs, elems , table@@ -33,6 +35,16 @@             x <- boolean             return ( p, x )     return $ build bnd pairs+    +symmetric_relation bnd = do+    pairs <- sequence $ do+        (p,q) <- A.range bnd+        guard $ p <= q+        return $ do+            x <- boolean+            return $ [ ((p,q), x ) ]+                   ++ [ ((q,p), x) | p /= q ]+    return $ build bnd $ concat pairs            identity :: ( Ix a, MonadSAT m)           => ((a,a),(a,a)) -> m ( Relation a a )

@@ -1,3 +1,4 @@+ module Satchmo.Relation.Prop  ( implies@@ -6,10 +7,20 @@ , irreflexive , reflexive , regular+, regular_in_degree+, regular_out_degree+, max_in_degree+, min_in_degree+, max_out_degree+, min_out_degree , empty , complete , disjoint , equals+, is_function+, is_partial_function+, is_bijection+, is_permutation )  where@@ -22,6 +33,7 @@ import Satchmo.Counting import Satchmo.Relation.Data import Satchmo.Relation.Op+import qualified Satchmo.Counting as C  import Control.Monad ( guard ) import Data.Ix@@ -70,12 +82,23 @@     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+regular, regular_in_degree, regular_out_degree, max_in_degree, min_in_degree, max_out_degree, min_out_degree+  :: ( Ix a, Ix b, MonadSAT m) => Int -> Relation a b -> m Boolean++regular deg r = monadic and [ regular_in_degree deg r, regular_out_degree deg r ]++regular_out_degree = out_degree_helper exactly+max_out_degree = out_degree_helper atmost+min_out_degree = out_degree_helper atleast+regular_in_degree deg r = regular_out_degree deg $ mirror r+max_in_degree deg r = max_out_degree deg $ mirror r+min_in_degree deg r = min_out_degree deg $ mirror r+++out_degree_helper f deg r = monadic and $ do     let ((a,b),(c,d)) = bounds r     x <- range ( a , c )-    return $ exactly deg $ do +    return $ f deg $ do          y <- range (b,d)         return $ r !(x,y) @@ -85,3 +108,24 @@ transitive r = do     r2 <- product r r     implies r2 r++-- | relation R is a function iff for each x,+-- there is exactly one y such that R(x,y)+is_function :: (Ix a, Ix b, MonadSAT m)+         => Relation a b -> m Boolean+is_function r = regular_out_degree 1 r++-- | relation R is a partial function iff for each x,+-- there is at most one y such that R(x,y)+is_partial_function :: (Ix a, Ix b, MonadSAT m)+         => Relation a b -> m Boolean+is_partial_function r = max_out_degree 1 r+++is_bijection :: (Ix a, Ix b, MonadSAT m)+         => Relation a b -> m Boolean+is_bijection r = monadic and [ is_function r , is_function (mirror r) ]++is_permutation :: (Ix a, MonadSAT m)+                  => Relation a a -> m Boolean+is_permutation r = is_bijection r

@@ -25,12 +25,12 @@             -- number of 1 is value of number               }               -instance C.Decode m Boolean Bool => C.Decode m Number Int where            +instance (Monad m, C.Decode m Boolean Bool) => C.Decode m Number Int where                 decode n = do         bs <- forM ( bits n ) C.decode         return $ length $ filter id bs -instance C.Decode m Boolean Bool => C.Decode m Number Integer where +instance (Monad m, C.Decode m Boolean Bool) => C.Decode m Number Integer where      decode n = do         bs <- forM ( bits n ) C.decode         return $ fromIntegral $ length $ filter id bs

@@ -0,0 +1,72 @@+-- | graphs n nodes of degree <= d and diameter <= k +-- see http://combinatoricswiki.org/wiki/The_Degree_Diameter_Problem_for_General_Graphs++-- usage: ./Moore d k n++{-# language FlexibleContexts #-}++import Prelude hiding ( not, or, and )+import qualified Prelude++import qualified Satchmo.Relation as R+import Satchmo.Code+import qualified Satchmo.Boolean as B+import Satchmo.Counting+import Satchmo.SAT.Mini++import qualified Data.Array as A+import System.Environment (getArgs)+import Control.Monad ( void, when, forM )++main :: IO ( )+main = do+  argv <- getArgs+  case argv of+    [ d, k, n ] -> void $ mainf ( read d ) (read k) (read n) Nothing+    [ d, k, n, s ] -> void $ mainf ( read d ) (read k) (read n) (Just $ read s)+    [ d, k ] -> do+      let go d k n ms = do+            ok <- mainf d k n ms+            when ok $ go d k (n+1) ms+      go (read d) (read k) 1 Nothing+    [] -> void $ mainf 3 2 10 Nothing -- petersen++mainf d k n ms = do+  putStrLn $ unwords [ "degree <=", show d, "diameter <=", show k, "nodes ==", show n, "sym", show ms ]+  mg <- solve $ moore d k n ms+  case mg of+    Just g -> do printA g ; return True+    Nothing -> return False++moore :: Int -> Int -> Int -> Maybe Int+      -> SAT (SAT (A.Array (Int,Int) Bool))+moore d k n ms = do+  g <- R.symmetric_relation ((0,0),(n-1,n-1))+  g <- case ms of+    Nothing -> return g+    Just s -> do+      let f x = mod (x + s) n ; f2 (x,y) = (f x, f y)+          normal i = head+                   $ filter (\(x,y) -> y < s)+                   $ iterate f2 i+      return $ R.build (R.bounds g)+             $ map (\(i,x) -> (i, g R.! normal i) )+             $ R.assocs g+  B.monadic B.assert [ R.symmetric g ]+  B.monadic B.assert [ R.reflexive g ]+  B.monadic B.assert [ R.max_in_degree (d+1) g ]+  B.monadic B.assert [ R.max_out_degree (d+1) g ]+  p <- R.power k g+  B.monadic B.assert [ R.complete p ]+  return $ decode g++-- | FIXME: this needs to go into a library+printA :: A.Array (Int,Int) Bool -> IO ()+printA a = putStrLn $ unlines $ do+         let ((u,l),(o,r)) = A.bounds a+         x <- [u .. o]+         return $ unwords $ do +             y <- [ l ..r ]+             return $ case a A.! (x,y) of+                  True -> "* " ; False -> ". "+

@@ -0,0 +1,69 @@+-- | Simple Sudoku Benchmark:+-- constraints for an empty board (no hints).+-- argument n: board is (n^2)x(n^2),+-- so standard Sudoku is for n=3++{-# language PatternSignatures #-}++import Prelude hiding ( not, product )+import qualified Prelude++import qualified Satchmo.Relation as R+import Satchmo.Code+import Satchmo.Boolean++import Satchmo.SAT.Mini++import Data.List (inits, tails)+import qualified Data.Array as A+import Control.Monad ( guard, when, forM, foldM, forM_ )+import System.Environment+import Data.Ix ( range)++main :: IO ()+main = do+    argv <- getArgs+    case argv of+      [ ] -> main_with 5+      [s] -> main_with $ read s++main_with :: Int -> IO ()+main_with n = do+    Just r <- solve $ sudoku n+    printA n r++printA :: Int -> A.Array ((Int,Int,Int,Int),(Int,Int)) Bool -> IO ()+printA n a = putStrLn $ unlines $ do+  (x1,x2) <- A.range ((1,1),(n,n))+  return $ unwords $ do +    (y1,y2) <- A.range ((1,1),(n,n))+    let zs = map (\z -> a A.! ((x1,x2,y1,y2),z) ) (A.range ((1,1),(n,n)) )+        fill n s = replicate (n - length s) ' ' ++ s+    return $ fill 3 $ show $ length $ takeWhile Prelude.not zs++sudoku :: Int+       -> SAT (SAT (A.Array ((Int,Int,Int,Int),(Int,Int)) Bool))+sudoku n = do+  r :: R.Relation (Int,Int,Int,Int) (Int,Int) <-+    R.relation (((1,1,1,1),(1,1)),((n,n,n,n),(n,n)))+  forM_ [ blockA, blockB, blockC ] $ \ bl ->+    forM_ (A.range ((1,1),(n,n))) $ \ (x,y) ->+      assertM $ R.is_bijection $ bl n r (x,y)+  return $ decode r++blockA (n::Int) r (x,y) =+  fromfunc (((1,1),(1,1)),((n,n),(n,n)))+    $ \ ((x1,x2),(y1,y2)) -> r R.! ((x,y,x1,x2),(y1,y2)) ++blockB (n::Int) r (x,y) =+  fromfunc (((1,1),(1,1)),((n,n),(n,n)))+    $ \ ((x1,x2),(y1,y2)) -> r R.! ((x1,x2,x,y),(y1,y2)) ++blockC (n::Int) r (x,y) =+  fromfunc (((1,1),(1,1)),((n,n),(n,n)))+    $ \ ((x1,x2),(y1,y2)) -> r R.! ((x,x1,y,x2),(y1,y2)) +++                             +assertM action = do x <- action ; assert [x]+fromfunc bnd f = R.build bnd $ do i <- A.range bnd ; return (i, f i )

@@ -1,5 +1,5 @@ Name:           satchmo-Version:        2.9.9.1+Version:        2.9.9.3  License:        GPL License-file:	gpl-2.0.txt@@ -127,4 +127,18 @@   Main-Is: Oscillator.hs   Build-Depends: base, array, satchmo   ghc-options: -rtsopts-  ++Test-Suite Moore+  Type: exitcode-stdio-1.0+  hs-source-dirs: examples+  Main-Is: Moore.hs+  Build-Depends: base, array, satchmo+  ghc-options: -rtsopts++Test-Suite Sudoku+  Type: exitcode-stdio-1.0+  hs-source-dirs: examples+  Main-Is: Sudoku.hs+  Build-Depends: base, array, satchmo+  ghc-options: -rtsopts+