satchmo 2.9.7.1 → 2.9.7.3
raw patch · 11 files changed
+417/−359 lines, 11 filesdep +asyncdep −lensdep ~base
Dependencies added: async
Dependencies removed: lens
Dependency ranges changed: base
Files
- Satchmo/Counting/Direct.hs +14/−2
- Satchmo/Data.hs +23/−49
- Satchmo/Fourier_Motzkin.hs +0/−106
- Satchmo/SAT/CNF.hs +0/−87
- Satchmo/SAT/Mini.hs +14/−2
- examples/Oscillator.hs +107/−0
- examples/PP.hs +90/−0
- examples/Ramsey.hs +1/−0
- examples/RamseyFM.hs +0/−105
- examples/Spaceship.hs +145/−0
- satchmo.cabal +23/−8
Satchmo/Counting/Direct.hs view
@@ -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++
Satchmo/Data.hs view
@@ -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
− Satchmo/Fourier_Motzkin.hs
@@ -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] )
− Satchmo/SAT/CNF.hs
@@ -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-
Satchmo/SAT/Mini.hs view
@@ -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
+ examples/Oscillator.hs view
@@ -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++ +
+ examples/PP.hs view
@@ -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]
examples/Ramsey.hs view
@@ -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
− examples/RamseyFM.hs
@@ -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]
+ examples/Spaceship.hs view
@@ -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++ +
satchmo.cabal view
@@ -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