diff --git a/Satchmo/Counting/Direct.hs b/Satchmo/Counting/Direct.hs --- a/Satchmo/Counting/Direct.hs +++ b/Satchmo/Counting/Direct.hs @@ -34,14 +34,26 @@ that <- atmost k xs this B.&& that +-- | (and ys) implies (atmost k xs) assert_implies_atmost ys k xs | k >= 0 = forM_ (select (k+1) xs) $ \ sub -> do B.assert $ map B.not ys ++ map B.not sub assert_implies_atmost ys k _ = B.assert $ map B.not ys --- | asserting that (or ys) implies (exactly k xs) +assert_implies_atleast ys k xs = + assert_implies_atmost ys (length xs - k) (map B.not xs) + +-- | asserting that (and ys) implies (exactly k xs) assert_implies_exactly ys k xs = do assert_implies_atmost ys k xs - assert_implies_atmost ys (length xs - k) $ map B.not xs + assert_implies_atleast ys k xs +-- | (atmost k xs) implies (or ys) +assert_atmost_implies xs k ys = + assert_implies_atleast (map B.not ys) (k+1) xs + +assert_atleast_implies xs k ys = + assert_implies_atmost (map B.not ys) (k+1) xs + + diff --git a/Satchmo/Data.hs b/Satchmo/Data.hs --- a/Satchmo/Data.hs +++ b/Satchmo/Data.hs @@ -1,10 +1,14 @@ +-- | this module just defines types for formulas, +-- it is not meant to contain efficient implementations +-- for formula manipulation. + {-# language TypeFamilies #-} {-# language GeneralizedNewtypeDeriving #-} module Satchmo.Data -( CNF, cnf, singleton, clauses, foldr, filter, size -, Clause (CTrue), clause, literals, without +( CNF, cnf, clauses, size +, Clause, clause, literals , Literal, literal, nicht, positive, variable , Variable ) @@ -20,6 +24,8 @@ import Data.Monoid import Data.List ( nub ) +-- * variables and literals + type Variable = Int data Literal = @@ -38,58 +44,26 @@ nicht :: Literal -> Literal nicht x = x { positive = not $ positive x } -newtype CNF = CNF ( S.Set Clause ) - deriving ( Monoid ) - -foldr f x (CNF s) = F.foldr f x s -filter p (CNF s) = CNF $ S.filter p s - -size (CNF s) = S.size s - -clauses (CNF s) = F.toList s - -instance Show CNF where - show cnf = unlines $ map show $ clauses cnf - -cnf :: [ Clause ] -> CNF -cnf cs = CNF $ S.fromList $ Prelude.filter ( /= CTrue) cs +-- * clauses -singleton c = CNF $ S.singleton c +newtype Clause = Clause { literals :: [Literal] } + deriving ( Eq, Ord ) +instance Show ( Clause ) where + show c = unwords ( map show (literals c) ++ [ "0" ] ) -data Clause = Clause ! ( M.Map Variable Bool ) | CTrue - deriving ( Eq, Ord ) +clause :: [ Literal ] -> Clause +clause ls = Clause ls -literals :: Clause -> [ Literal ] -literals c = case c of - Clause m -> map ( \ (v,p) -> literal p v ) $ M.toList m +-- * formulas -instance Monoid Clause where - mempty = Clause M.empty - mappend c1 c2 = case c1 of - CTrue -> CTrue - Clause m1 -> case c2 of - CTrue -> CTrue - Clause m2 -> - let common = M.intersection m1 m2 - in if M.isSubmapOf common m1 && M.isSubmapOf common m2 - then Clause $ M.union m1 m2 - else CTrue +newtype CNF = CNF { clauses :: [ Clause ] } -instance Show ( Clause ) where - show c = case c of - CTrue -> "# True" - Clause m -> unwords ( map show (literals c) ++ [ "0" ] ) +size (CNF s) = length s + +instance Show CNF where + show cnf = unlines $ map show $ clauses cnf -clause :: [ Literal ] -> Clause -clause ls = Prelude.foldr - ( \ l c -> case c of - CTrue -> CTrue - Clause m -> case M.lookup (variable l) m of - Nothing -> Clause $ M.insert (variable l) (positive l) m - Just p -> if p == positive l then Clause m else CTrue - ) mempty ls +cnf :: [ Clause ] -> CNF +cnf cs = CNF cs -without c w = case c of - -- CTrue -> CTrue -- ? - Clause m -> Clause $ M.filterWithKey ( \ v p -> w /= v ) m diff --git a/Satchmo/Fourier_Motzkin.hs b/Satchmo/Fourier_Motzkin.hs deleted file mode 100644 --- a/Satchmo/Fourier_Motzkin.hs +++ /dev/null @@ -1,106 +0,0 @@ -{-# language TupleSections #-} - -module Satchmo.Fourier_Motzkin where - -import Satchmo.Data - -import qualified Data.Map.Strict as M -import qualified Data.Set as S -import Control.Monad ( guard ) -import Data.Monoid -import Data.List ( sortBy, nub ) -import Data.Function (on) -import System.IO - -type Solver = CNF -> IO (Maybe (M.Map Variable Bool)) - -fomo :: Solver -fomo cnf = do - print_info "fomo" cnf - ( remove_satisfied $ trivial $ onesided $ eliminate fomo ) cnf - -print_info msg cnf = do - hPutStrLn stderr $ unwords [ msg, show $ size cnf, "\n" ] - -- hPutStrLn stderr $ show cnf ++ "\n" - -remove_satisfied cont cnf = do - print_info "remove_satisfied" cnf - let vars polar cl = S.fromList $ do - lit <- literals cl; - guard $ positive lit == polar - return $ variable lit - remaining = Satchmo.Data.filter - ( \ cl -> disjoint ( vars True cl ) ( vars False cl )) - cnf - cont cnf - -trivial :: Solver -> Solver -trivial cont cnf = do - print_info "trivial" cnf - if null $ clauses cnf - then return $ Just M.empty - else if clause [] `elem` clauses cnf - then return $ Nothing - else cont cnf - -onesided :: Solver -> Solver -onesided cont cnf = do - print_info "onesided" cnf - let pos = occurrences True cnf - neg = occurrences False cnf - onlypos = M.keys $ M.difference pos neg - onlyneg = M.keys $ M.difference neg pos - assigned = M.fromList - $ map (,True) onlypos ++ map (,False) onlyneg - ks = M.keysSet assigned - others = Satchmo.Data.filter - ( \ cl -> disjoint ks - $ S.fromList $ map variable $ literals cl) - cnf - hPutStrLn stderr $ unwords [ "assigned", show assigned , "\n" ] - later <- ( if size others < size cnf then fomo else cont ) others - return $ fmap ( M.union assigned ) later - -disjoint s t = S.null $ S.intersection s t - -eliminate :: Solver -> Solver -eliminate cont nf = do - print_info "eliminate" nf - let pos = occurrences True nf - neg = occurrences False nf - reductions = M.intersectionWith - ( \ xs ys -> let lx = length xs - ly = length xs - in lx*ly - lx - ly - ) pos neg - resolve v = cnf $ do - cp <- pos M.! v - let cpv = cp `without` v - cn <- neg M.! v - let cnv = cn `without` v - return $ cpv <> cnv - others v = Satchmo.Data.filter - ( \ cl -> not $ elem v $ map variable $ literals cl ) - nf - reconstruct v m = Prelude.or $ do - cp <- pos M.! v - return $ Prelude.not $ Prelude.or $ do - lit <- literals $ cp `without` v - let v = M.findWithDefault False ( variable lit ) m - return $ if positive lit then v else Prelude.not v - case sortBy (compare `on` snd) $ M.toList reductions of - (v,c): _ -> do - hPutStrLn stderr $ unwords [ "completely resolve", show v, "count", show c ] - later <- cont $ others v <> resolve v - return $ fmap - ( \ m -> M.insert v (reconstruct v m) m) - later - --- | map each var to list of clauses where it occurs -occurrences :: Bool -> CNF -> M.Map Variable [Clause] -occurrences polarity = - flip Satchmo.Data.foldr M.empty $ \ cl -> - M.unionWith (++) $ M.fromList $ do - lit <- literals cl - guard $ positive lit == polarity - return ( variable lit, [cl] ) diff --git a/Satchmo/SAT/CNF.hs b/Satchmo/SAT/CNF.hs deleted file mode 100644 --- a/Satchmo/SAT/CNF.hs +++ /dev/null @@ -1,87 +0,0 @@ --- | use this module to get the actual --- conjunctive normal form (a list of clauses). --- You can then send this to minisat, --- and do your own statistics and preprocessing first - -{-# LANGUAGE GeneralizedNewtypeDeriving #-} -{-# LANGUAGE TypeFamilies #-} -{-# LANGUAGE MultiParamTypeClasses #-} -{-# LANGUAGE FlexibleInstances #-} -{-# LANGUAGE DoAndIfThenElse #-} -{-# LANGUAGE PatternSignatures #-} -{-# LANGUAGE StandaloneDeriving #-} -{-# LANGUAGE TemplateHaskell #-} - - -module Satchmo.SAT.CNF - -( SAT -, fresh -, emit -, solve -) - -where - -import qualified MiniSat as API - -import Satchmo.Data -import Satchmo.Boolean hiding ( not ) -import Satchmo.Code -import Satchmo.MonadSAT -import Satchmo.Fourier_Motzkin ( fomo ) - -import Control.Monad -import Control.Monad.State.Strict -import Control.Monad.Reader - -import Control.Applicative -import Control.Lens -import Data.Monoid -import Data.Foldable -import qualified Data.Map.Strict as M -import System.IO - -data S = S { _next :: ! Variable - , _output :: ! CNF - -- , _assignment :: ! (M.Map Variable Bool) - } - -$(makeLenses ''S) - -newtype SAT a = SAT { unSAT :: StateT S IO a } - deriving ( Functor, Applicative, Monad, MonadIO, MonadState S ) - -instance MonadFix SAT -- dummy - -instance MonadSAT SAT where - fresh = do - x <- get - modify ( next %~ succ ) - return $ literal True $ x ^. next - - emit cl = do - modify ( output %~ ( singleton cl <> ) ) - - note msg = liftIO $ hPutStrLn stderr msg - - type Decoder SAT = Reader (M.Map Variable Bool) - decode_variable v = do m <- ask ; return $ m M.! v - -instance Decode (Reader (M.Map Variable Bool)) Boolean Bool where - decode b = case b of - Constant c -> return c - Boolean l -> do - v <- -- decode_variable $ variable l - do m <- ask ; return $ M.findWithDefault False ( variable l ) m - return $ if positive l then v else not v - -solve :: SAT (Decoder SAT a) -> IO (Maybe a) -solve action = do - (a,s) <- runStateT (unSAT action) - $ S { _next = 1, _output = cnf [] } - mm <- fomo $ s^.output - return $ case mm of - Nothing -> Nothing - Just m -> Just $ runReader a m - diff --git a/Satchmo/SAT/Mini.hs b/Satchmo/SAT/Mini.hs --- a/Satchmo/SAT/Mini.hs +++ b/Satchmo/SAT/Mini.hs @@ -32,6 +32,7 @@ import Control.Applicative import System.IO +import Control.Concurrent.Async deriving instance Enum API.Lit @@ -61,7 +62,6 @@ -- hPutStrLn stderr $ "fresh: " ++ show (x, l) return l - emit CTrue = return () emit cl = SAT $ \ s -> do let conv l = ( if positive l then id else API.neg ) $ toEnum @@ -105,7 +105,7 @@ return Nothing solve :: SAT (SAT a) -> IO (Maybe a) -solve action = API.withNewSolverAsync $ \ s -> do +solve action = withNewSolverAsync $ \ s -> do hPutStrLn stderr $ "start producing CNF" SAT decoder <- unSAT action s v <- API.minisat_num_vars s @@ -121,3 +121,15 @@ hPutStrLn stderr $ "decoder finished" return $ Just out else return Nothing + + +withNewSolverAsync h = + bracket newSolver API.deleteSolver $ \ s -> do + mask_ $ withAsync (h s) $ \ a -> do + wait a `onException` API.minisat_interrupt s + +newSolver = + do s <- API.minisat_new + -- https://github.com/niklasso/minisat-haskell-bindings/issues/6 + -- eliminate s True + return s diff --git a/examples/Oscillator.hs b/examples/Oscillator.hs new file mode 100644 --- /dev/null +++ b/examples/Oscillator.hs @@ -0,0 +1,107 @@ +-- | compute oscillator for Conway's game of life, +-- cf. http://www.conwaylife.com/wiki/Category:Oscillators +-- example usage: ./dist/build/Life/Life 3 9 9 20 +-- arguments are: period, width, height, number of life start cells + +{-# language PatternSignatures #-} +{-# language FlexibleContexts #-} + +import Prelude hiding ( not, or, and ) +import qualified Prelude + +import Satchmo.Relation +import Satchmo.Code +import Satchmo.Boolean hiding ( equals, implies ) +import Satchmo.Counting.Binary + +import Satchmo.SAT.Mini + +import Data.List (sort) +import qualified Data.Array as A +import Control.Monad ( guard, when, forM, foldM, void ) +import System.Environment +import Data.Ix ( range, inRange ) + +main :: IO () +main = void $ do + argv <- getArgs + Just gs <- case map read argv of + [] -> solve $ osc 3 9 9 (Just 20) + [ p, w ] -> solve $ osc p w w Nothing + [ p, w, h ] -> solve $ osc p w h Nothing + [ p, w, h, c ] -> solve $ osc p w h $ Just c + forM ( zip [ 0.. ] gs ) $ \ (t, g) -> do + putStrLn $ unwords [ "time", show t ] + printA g + +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 -> ". " + +osc :: Int -> Int -> Int -> Maybe Int + -> SAT ( SAT [ A.Array (Int,Int) Bool ] ) +osc p w h mc = do + g0 <- relation ((1,1),(w,h)) + case mc of + Just c -> monadic assert [ atmost c $ map snd $ assocs g0 ] + Nothing -> return () + let handle 0 gs = return gs + handle k (g:gs) = do g' <- next g ; handle (k-1) (g' : g : gs) + gs <- handle p [ g0 ] + forM gs bordered + monadic assert [ equals ( head gs ) ( last gs ) ] + forM [ d | d <- [1 .. p - 1] , 0 == mod p d ] $ \ d -> + monadic assert [ fmap not $ equals ( gs !! 0 ) ( gs !! d ) ] + return $ decode $ reverse gs + +bordered g = do + let ((u,l),(d,r)) = bounds g + forM [ u .. d ] $ \ x -> forM [ l , r ] $ \ y -> assert [ not $ g!(x,y) ] + forM [ u , d ] $ \ x -> forM [ l .. r ] $ \ y -> assert [ not $ g!(x,y) ] + + +next g = do + f <- constant False + let bnd = bounds g + let neighbours (i,j) = do + i' <- [ i-1, i, i+1 ] + j' <- [ j-1, j, j+1 ] + guard $ i /= i' Prelude.|| j /= j' + return $ if inRange bnd (i',j') + then g ! (i', j') + else f + pairs <- forM ( assocs g ) $ \ (p, x) -> do + y <- step x $ neighbours p + return (p, y) + return $ build bnd pairs + +step x xs = do + cs <- counts 3 xs + keep <- and [ x, cs !! 2 ] + let birth = cs !! 3 + or [ keep, birth ] + + +-- | output !! k == True +-- if exactly k of the inputs are True +counts :: MonadSAT m + => Int -> [ Boolean ] + -> m [ Boolean ] +counts w xs = do + t <- constant True ; f <- constant False + let handle cs x = do + ds <- forM cs $ \ c -> boolean + forM ( zip cs ds ) $ \ (c,d) -> do + assert_fun3 ( \ c d x -> Prelude.not x <= ( c == d ) ) c d x + forM ( zip ( f : cs) ds ) $ \ (c,d) -> do + assert_fun3 ( \ c d x -> x <= ( c == d ) ) c d x + return ds + foldM handle ( t : replicate w f ) xs + + + diff --git a/examples/PP.hs b/examples/PP.hs new file mode 100644 --- /dev/null +++ b/examples/PP.hs @@ -0,0 +1,90 @@ +-- | find incidence matrix of projective plane of given order +-- example usage: ./dist/build/PP/PP 2 + +{-# language PatternSignatures #-} +{-# language FlexibleContexts #-} + +import Prelude hiding ( not, and, or ) +import qualified Prelude + +import Satchmo.Relation +import Satchmo.Code +import Satchmo.Boolean + +import qualified Satchmo.Counting.Binary as CB +import qualified Satchmo.Counting.Unary as CU +import qualified Satchmo.Counting.Direct as CD + +import qualified Satchmo.Binary as B + +import Satchmo.SAT.Mini + +import Data.List (sort) +import qualified Data.Array as A +import Control.Monad ( guard, when, forM, void ) +import System.Environment +import Data.Ix ( range) + + +main :: IO () +main = do + argv <- getArgs + let [ o ] = case argv of + [] -> [5] + _ -> map read argv + Just ( a :: A.Array (Int,Int) Bool ) <- solve $ pp o + putStrLn $ unlines $ do + let ((u,l),(o,r)) = A.bounds a + x <- [ u .. o ] + return $ unwords $ do + y <- [ l .. r ] + return $ if a A.! (x,y) then "* " else ". " + +fill k cs = replicate (k - length cs) ' ' ++ cs + +pp o = do + let n = o*o + o + 1 + points = [ 1 .. n ] ; lines = [ 1 .. n ] + i :: Relation Int Int <- relation ((1,1),(n,n)) + contains (o+1) i + contains (o+1) $ mirror i + any_two_determine_one i + any_two_determine_one $ mirror i + monotone i + monotone $ transpose i + return $ decode i + +transpose a = + let ((1,1),(h,w)) = bounds a + in build ((1,1),(w,h)) $ do + ((x,y),v) <- assocs a + return ((y,x),v) + +-- | see http://www.maa.org/programs/maa-awards/writing-awards/the-search-for-a-finite-projective-plane-of-order-10 +fixed_start o i = do + let n = o*o + o + 1 + return () + +monotone i = assertM $ do + let ((1,1),(points, lines)) = bounds i + rows = for [ 1 .. points ] $ \ p -> + B.make $ for [ 1 .. lines ] $ \ l -> i ! (p,l) + monadic and $ for ( zip rows $ tail rows ) $ \ (r, r') -> + B.lt r r' + +contains o i = assertM $ do + let ((1,1),(points, lines)) = bounds i + monadic and $ for [ 1 .. points ] $ \ p -> + monadic ( CB.exactly o ) $ for [ 1 .. lines ] $ \ l -> + return $ i ! (p, l) + +any_two_determine_one i = assertM $ do + let ((1,1),(points, lines)) = bounds i + monadic and $ for [1..points] $ \ p -> + monadic and $ for [p+1 .. points] $ \ q -> + monadic ( CB.exactly 1 ) $ for [1 .. lines] $ \ l -> + and [ i ! (p,l), i ! (q,l) ] + +for = flip map + +assertM this = do x <- this ; assert [x] diff --git a/examples/Ramsey.hs b/examples/Ramsey.hs --- a/examples/Ramsey.hs +++ b/examples/Ramsey.hs @@ -4,6 +4,7 @@ -- earlier numbers are sizes of forbidden cliques {-# language PatternSignatures #-} +{-# language FlexibleContexts #-} import Prelude hiding ( not, and, or, product ) import qualified Prelude diff --git a/examples/RamseyFM.hs b/examples/RamseyFM.hs deleted file mode 100644 --- a/examples/RamseyFM.hs +++ /dev/null @@ -1,105 +0,0 @@ --- | find colouring without complete subgraphs --- example usage: ./dist/build/Ramsey/Ramsey 3 3 3 16 --- last number is size of graph, --- earlier numbers are sizes of forbidden cliques - -{-# language PatternSignatures #-} - -import Prelude hiding ( not, and, or, product ) -import qualified Prelude - -import Satchmo.Relation -import Satchmo.Code -import Satchmo.Boolean hiding ( implies ) -import Satchmo.Counting - -import qualified Satchmo.Binary as B - -import Satchmo.SAT.CNF - -import Data.List (sort, tails) -import qualified Data.Array as A -import Control.Monad ( guard, when, forM, foldM, void ) -import System.Environment -import Data.Ix ( range) - - -main :: IO () -main = do - argv <- getArgs - let ns = map read $ case argv of - [] -> [ "3", "3", "5" ] -- small numbers, else it will blow up - _ -> argv - cs = init ns - n = last ns - Just ( p : fs ) <- solve $ ramsey cs n - forM ( zip [ 1.. ] fs ) $ \ (k, f) -> do - putStrLn $ unwords [ "colour", show k ] - printA f - putStrLn "with isomorphism" ; printA p - -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 -> ". " - -ramsey (cs :: [Int]) (n :: Int) = do - fs <- forM cs $ \ c -> - relation ((1 :: Int,1 :: Int),(n,n)) - - p <- relation ((1,1),(n,n)) - -- forM fs $ isomorphism p - - -- forM fs $ cyclic 3 - - when False $ void $ do - forM [ 1 .. n ] $ \ x -> - forM [ x + 1 .. n ] $ \ y -> - assertM $ exactly 1 $ - for fs $ \ f -> f ! (x,y) - when True $ void $ do - forM [ 1 .. n ] $ \ x -> - forM [ x + 1 .. n ] $ \ y -> - assert $ for fs $ \ f -> f ! (x,y) - - forM ( zip cs fs ) $ \ (c,f) -> - forM ( cliquesA c [1..n] ) $ \ xs -> - assert $ for ( cliquesA 2 xs ) $ \ [x,y] -> not $ f ! (x,y) - return $ forM (p : fs) decode - -isomorphism p e = do - assertM $ regular 1 p - assertM $ regular 1 $ mirror p - e' <- foldM product ( mirror p ) [ e, p ] - assertM $ implies e e' - assertM $ implies e' e - -cyclic off f = forM ( indices f ) $ \ (i,j) -> - when ( off < i Prelude.&& i < j ) - $ assert_fun2 (==) ( f!(i,j) ) (f!(i-off,j-off)) - -cliquesA k xs = - let -- spec: c!(i,j) == cliques i (drop j xs) - bnd = ((0,0),(k, length xs)) - c = A.array bnd $ do - (i,j) <- A.range bnd - return ( (i,j) - , if i == 0 then [ [] ] - else if i > length xs - j then [] - else c A.! (i,j+1) - ++ map (xs !! j : ) ( c A.! (i-1,j+1)) - ) - in c A.! (k,0) - -cliques 0 xs = return [] -cliques k xs | k > length xs = [] -cliques k (x:xs) = - cliques k xs ++ map (x :) ( cliques (k-1) xs ) - -for = flip map - -assertM this = do x <- this ; assert [x] diff --git a/examples/Spaceship.hs b/examples/Spaceship.hs new file mode 100644 --- /dev/null +++ b/examples/Spaceship.hs @@ -0,0 +1,145 @@ +-- | compute spaceship for Conway's game of life, +-- cf. http://www.conwaylife.com/wiki/Category:Oscillators +-- arguments are: distanceX, distanceY, exact period +-- width [, height, [number of life start cells]] +-- example usage: +-- ./Spaceship 1 1 4 6 -- glider +-- ./Spaceship 0 2 4 7 9 9 -- Conway's lightweight spaceship + +{-# language PatternSignatures #-} +{-# language FlexibleContexts #-} + +import Prelude hiding ( not, or, and ) +import qualified Prelude + +import Satchmo.Relation +import Satchmo.Code +import Satchmo.Boolean hiding ( equals, implies ) +import qualified Satchmo.Binary as B + +import qualified Satchmo.Counting.Direct as CD +import qualified Satchmo.Counting.Unary as CU +import qualified Satchmo.Counting.Binary as CB + +import Satchmo.SAT.Mini + +import Data.List (sort) +import qualified Data.Array as A +import Control.Monad ( guard, when, forM, foldM + , void, replicateM ) +import System.Environment +import Data.Ix ( range, inRange ) + +main :: IO () +main = void $ do + argv <- getArgs + Just gs <- case map read argv of + [] -> + solve $ glide 0 2 4 7 9 (Just 9) + [ dx, dy, p, w ] -> + solve $ glide dx dy p w w Nothing + [ dx, dy, p, w, h ] -> + solve $ glide dx dy p w h Nothing + [ dx, dy, p, w, h, c ] -> + solve $ glide dx dy p w h $ Just c + forM ( zip [ 0.. ] gs ) $ \ (t, g) -> do + putStrLn $ unwords [ "time", show t ] + printA g + +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 -> ". " + +for = flip map + +glide :: Int -> Int -> Int -> Int -> Int -> Maybe Int + -> SAT ( SAT [A.Array (Int,Int) Bool] ) +glide dx dy p w h mc = do + g0 <- relation ((1,1),(w,h)) + assert $ map snd $ assocs g0 + case mc of + Just c -> monadic assert [ CB.atmost c $ map snd $ assocs g0 ] + Nothing -> return () + let handle 0 g = return [g] + handle k g = do g' <- next g ; gs <- handle (k-1) g' ; return $ g : gs + gs <- handle p g0 + forM gs bordered + + -- ms <- forM ( tail gs ) $ \ h -> moved (dx,dy) ( head gs ) h + -- assert $ ms + m <- moved (dx,dy) (head gs) (last gs) + assert [m] + + return $ decode gs + +equals r s = monadic and [ implies r s, implies s r ] + +moved (dx,dy) g h = do + f <- constant False + let bnd @ ((l,o),(r,u)) = bounds g + get g p = if inRange bnd p then g ! p else f + monadic and $ for ( range bnd ) $ \ (x,y) -> do + fun2 (==) ( get g (x,y) ) ( get h (x+dx, y+dy) ) + + +bordered g = do + let ((u,l),(d,r)) = bounds g + forM [ u .. d ] $ \ x -> forM [ l , r ] $ \ y -> assert [ not $ g!(x,y) ] + forM [ u , d ] $ \ x -> forM [ l .. r ] $ \ y -> assert [ not $ g!(x,y) ] + + +next g = do + f <- constant False + let bnd = bounds g + let neighbours (i,j) = do + i' <- [ i-1, i, i+1 ] + j' <- [ j-1, j, j+1 ] + guard $ i /= i' Prelude.|| j /= j' + return $ if inRange bnd (i',j') + then g ! (i', j') + else f + pairs <- forM ( assocs g ) $ \ (p, x) -> do + y <- step x $ neighbours p + return (p, y) + return $ build bnd pairs + +step = step_mod + +step_mod x xs = do + c <- CB.count xs + drei <- B.constant 3 + birth <- B.equals drei c + zwei <- B.constant 2 + keep <- B.equals zwei c + keepx <- and [keep, x] + or [ keepx, birth ] + +step_orig x xs = do + cs <- counts 3 xs + keep <- and [ x, cs !! 2 ] + let birth = cs !! 3 + or [ keep, birth ] + +-- | output !! k == True +-- if exactly k of the inputs are True +counts :: MonadSAT m + => Int -> [ Boolean ] + -> m [ Boolean ] +counts w xs = do + t <- constant True ; f <- constant False + let handle cs x = do + ds <- forM cs $ \ c -> boolean + forM ( zip cs ds ) $ \ (c,d) -> do + assert_fun3 ( \ c d x -> Prelude.not x <= ( c == d ) ) c d x + forM ( zip ( f : cs) ds ) $ \ (c,d) -> do + assert_fun3 ( \ c d x -> x <= ( c == d ) ) c d x + return ds + foldM handle ( t : replicate w f ) xs + + + diff --git a/satchmo.cabal b/satchmo.cabal --- a/satchmo.cabal +++ b/satchmo.cabal @@ -1,5 +1,5 @@ Name: satchmo -Version: 2.9.7.1 +Version: 2.9.7.3 License: GPL License-file: gpl-2.0.txt @@ -21,7 +21,8 @@ Library ghc-options: -funbox-strict-fields Build-depends: mtl, process, containers, base == 4.*, - lens, array, bytestring, directory, minisat >= 0.1 + -- lens, + array, bytestring, directory, minisat >= 0.1, async Exposed-modules: Satchmo.Data -- Satchmo.Data.Default @@ -55,8 +56,7 @@ Satchmo.SAT Satchmo.SAT.Tmpfile Satchmo.SAT.Mini - Satchmo.SAT.CNF - Satchmo.Fourier_Motzkin + -- Satchmo.SAT.CNF -- Satchmo.SAT.BS -- Satchmo.SAT.Seq -- Satchmo.SAT.Sequence @@ -99,16 +99,31 @@ hs-source-dirs: . extensions: +Test-Suite PP + Type: exitcode-stdio-1.0 + hs-source-dirs: examples + Main-Is: PP.hs + Build-Depends: base, array, satchmo + ghc-options: -rtsopts + Test-Suite Ramsey Type: exitcode-stdio-1.0 hs-source-dirs: examples Main-Is: Ramsey.hs Build-Depends: base, array, satchmo - -Test-Suite RamseyFM + ghc-options: -rtsopts + +Test-Suite Spaceship Type: exitcode-stdio-1.0 hs-source-dirs: examples - Main-Is: RamseyFM.hs + Main-Is: Spaceship.hs Build-Depends: base, array, satchmo - + ghc-options: -rtsopts + +Test-Suite Oscillator + Type: exitcode-stdio-1.0 + hs-source-dirs: examples + Main-Is: Oscillator.hs + Build-Depends: base, array, satchmo + ghc-options: -rtsopts