satchmo 2.9.3 → 2.9.4

raw patch · 4 files changed

+151/−3 lines, 4 filesdep +satchmodep ~basePVP ok

version bump matches the API change (PVP)

Dependencies added: satchmo

Dependency ranges changed: base

API changes (from Hackage documentation)

Files

• Satchmo/Boolean/Op.hs +1/−1
• Satchmo/Counting/Direct.hs +35/−0
• examples/Ramsey.hs +105/−0
• satchmo.cabal +10/−2

@@ -1,7 +1,7 @@ module Satchmo.Boolean.Op  ( constant-, and, or, xor, equals2, equals, implies, (||), (&&)+, and, or, xor, xor2, equals2, equals, implies, (||), (&&) , fun2, fun3 , ifThenElse, ifThenElseM , assert_fun2, assert_fun3

@@ -0,0 +1,35 @@+-- | functions in this module have no extra variables but exponential cost.++module Satchmo.Counting.Direct ++( atleast+, atmost+, exactly+)++where++import Satchmo.Boolean ( Boolean, MonadSAT )  +import qualified Satchmo.Boolean as B++import Control.Monad ( forM )++select :: Int -> [a] -> [[a]]+select 0 xs = [[]]+select k [] = []+select k (x:xs) =+  select k xs ++ (map (x:) $ select (k-1) xs)++atleast :: MonadSAT m => Int -> [ Boolean ] -> m Boolean+atleast k xs = B.or =<< forM (select k xs) B.and++atmost :: MonadSAT m => Int -> [ Boolean ] -> m Boolean+atmost k xs = atleast (length xs - k) $ map B.not xs++exactly :: MonadSAT m => Int -> [ Boolean ] -> m Boolean+exactly k xs = do+  this <- atleast k xs+  that <- atmost k xs+  this B.&& that+  +        

@@ -0,0 +1,105 @@+-- | 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.Mini++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", "3", "16" ]+          _ -> 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]

@@ -1,5 +1,5 @@ Name:           satchmo-Version:        2.9.3+Version:        2.9.4  License:        GPL License-file:	gpl-2.0.txt@@ -12,7 +12,7 @@ 		(hence the "mo" in "satchmo").  Category:	Logic-cabal-version:  >= 1.6+cabal-version:  >= 1.8 build-type: Simple source-repository head     type: git@@ -30,6 +30,7 @@         Satchmo.Counting         Satchmo.Counting.Unary         Satchmo.Counting.Binary+        Satchmo.Counting.Direct         Satchmo.Code         Satchmo.Integer         Satchmo.Binary@@ -96,3 +97,10 @@     hs-source-dirs:     .     extensions:  +Test-Suite Ramsey+  Type: exitcode-stdio-1.0+  hs-source-dirs: examples+  Main-Is: Ramsey.hs+  Build-Depends: base, array, satchmo++