satchmo 1.3 → 1.4

raw patch · 6 files changed

+87/−11 lines, 6 filesPVP ok

version bump matches the API change (PVP)

API changes (from Hackage documentation)

Files

• Satchmo/Binary/Op/Common.hs +32/−2
• Satchmo/Boolean/Data.hs +14/−2
• Satchmo/Code.hs +2/−0
• Satchmo/Internal.hs +32/−4
• Satchmo/Solve.hs +3/−0
• satchmo.cabal +4/−3

@@ -1,13 +1,13 @@ module Satchmo.Binary.Op.Common  ( iszero-, equals+, equals, lt, le, ge, eq, gt , full_adder, half_adder )  where -import Prelude hiding ( and, or, not )+import Prelude hiding ( and, or, not, compare )  import qualified Satchmo.Code as C @@ -24,6 +24,7 @@ equals a b = do     equals' ( bits a ) ( bits b ) + equals' :: Booleans -> Booleans -> SAT Boolean equals' [] [] = B.constant True equals' (x:xs) (y:ys) = do@@ -32,6 +33,35 @@     and [ not z, rest ] equals' xs [] = and $ map not xs equals' [] ys = and $ map not ys++le x y = do (l,e) <- compare x y ; or [l,e]+lt x y = do (l,e) <- compare x y ; return l+ge x y = le y x+gt x y = lt y x+eq = equals++compare :: Number -> Number +        -> SAT ( Boolean, Boolean )+compare a b = compare' ( bits a ) ( bits b )++compare' :: Booleans +         -> Booleans +         -> SAT ( Boolean, Boolean ) -- ^ (less, equals)+compare' [] [] = do +    f <- B.constant False ; t <- B.constant True ; return ( f, t )+compare' (x:xs) (y:ys) = do+    l <- and [ not x, y ]+    e <- fmap not $ xor [ x, y ]+    ( ll, ee ) <- compare' xs ys+    lee <- and [l,ee]+    l' <- or [ l, lee ] ; e' <- and [ e, ee ]+    return ( l', e' )+compare' xs [] = do+    x <- or xs+    return ( not x, not x )+compare' [] ys = do+    y <- or ys+    return ( y, not y )  full_adder :: Boolean -> Boolean -> Boolean            -> SAT ( Boolean, Boolean )

@@ -3,7 +3,8 @@ module Satchmo.Boolean.Data   ( Boolean, Booleans-, boolean, constant+, boolean, exists, forall+, constant , not, assert, monadic ) @@ -42,11 +43,22 @@         Constant {} -> return $ value b  boolean :: SAT Boolean-boolean = do+boolean = exists++exists :: SAT Boolean+exists = do     x <- fresh     return $ Boolean             { encode = x            , decode = asks $ \ fm -> fromJust $ M.lookup x fm+           }++forall :: SAT Boolean+forall = do+    x <- fresh_forall+    return $ Boolean +           { encode = x+           , decode = error "Boolean.forall cannot be decoded"            }  constant :: Bool -> SAT Boolean

@@ -22,6 +22,8 @@  type Decoder a = Reader ( Map Literal Bool ) a +instance Decode () () where+    decode () = return ()  instance ( Decode c a, Decode d b ) => Decode ( c,d) (a,b) where     decode (c,d) = do a <- decode c; b <- decode d; return ( a,b)

@@ -1,7 +1,8 @@ module Satchmo.Internal   ( SAT-, fresh, emit+, fresh, fresh_forall+, emit , sat ) @@ -12,14 +13,18 @@ import Control.Monad.State.Strict import Control.Monad.Writer.Strict +data Quantified = Forall [ Int ] | Exists [ Int ]+ data Accu = Accu            { next :: ! Int+          , quantified :: [ Quantified ]           , size :: ! Int           }  start :: Accu start = Accu        { next = 1+      , quantified = []       , size = 0       } @@ -29,15 +34,38 @@ sat m =      let ~( ~(a,w), accu) = runState ( runWriterT m ) start     in  ( unlines $ unwords [ "p", "cnf", show ( next accu - 1), show ( size accu ) ]-                    : map show w+                  : do q <- reverse $ interesting $ quantified accu+                       return $ case q of +                           Forall xs -> unwords $ "a" : map show ( reverse xs ++ [0] )+                           Exists xs -> unwords $ "e" : map show ( reverse xs ++ [0] )+                  ++ map show w         , a         )     +interesting [ Exists _ ] = []+interesting xs = xs++-- | existentially quantified (implicitely so, before first fresh_forall) fresh :: SAT Literal fresh = do     a <- get-    put $ a { next = next a + 1 }-    return $ literal $ next a+    let n = next a+    let q = case quantified a of+              Exists xs : rest -> Exists (n : xs) : rest+              rest -> Exists [n] : rest+    put $ a { next = n + 1, quantified = q }+    return $ literal n++-- | universally quantified+fresh_forall :: SAT Literal+fresh_forall = do+    a <- get+    let n = next a+    let q = case quantified a of+              Forall xs : rest -> Forall (n : xs) : rest+              rest -> Forall [n] : rest+    put $ a { next = n + 1, quantified = q }+    return $ literal n  emit :: Clause -> SAT () emit clause = do

@@ -1,3 +1,6 @@+-- | This is the API for plugging in solver implementations.+-- Actual implementations are in the (separate) package @satchmo-backends@+ module Satchmo.Solve  ( solve

@@ -1,5 +1,5 @@ Name:           satchmo-Version:        1.3+Version:        1.4  License:        GPL License-file:	gpl-2.0.txt@@ -7,9 +7,10 @@ Maintainer:	Johannes Waldmann Homepage:       http://dfa.imn.htwk-leipzig.de/satchmo/ Synopsis:       SAT encoding monad-description:	Encoding for boolean and integral constraints into CNF-SAT.+description:	Encoding for boolean and integral constraints into (QBF-)CNF-SAT. 		The encoder is provided as a State monad (hence the "mo" in "satchmo").-		requires a backend (e.g. satchmo-minisat, satchmo-funsat)+		requires a backend (e.g. satchmo-backends, satchmo-funsat)+Category:	Algorithms Build-depends:  mtl, process, containers, base, array Exposed-modules: 	Satchmo.Data