satchmo 2.6.0 → 2.8.1

raw patch · 27 files changed

+231/−575 lines, 27 filesPVP ok

version bump matches the API change (PVP)

API changes (from Hackage documentation)

Files

• Satchmo/Boolean/Op.hs +5/−2
• Satchmo/Integer/Data.hs +4/−3
• Satchmo/Map.hs +8/−0
• Satchmo/Map/Data.hs +39/−0
• Satchmo/MonadSAT.hs +2/−1
• Satchmo/Relation/Data.hs +5/−4
• Satchmo/Relation/Prop.hs +15/−1
• Satchmo/SAT/Mini.hs +5/−0
• Satchmo/SAT/Tmpfile.hs +2/−1
• Satchmo/SMT/Exotic/Arctic.hs +0/−69
• Satchmo/SMT/Exotic/Arctic/Integer.hs +0/−93
• Satchmo/SMT/Exotic/Dict.hs +0/−17
• Satchmo/SMT/Exotic/Domain.hs +0/−4
• Satchmo/SMT/Exotic/Fuzzy.hs +0/−63
• Satchmo/SMT/Exotic/Natural.hs +0/−80
• Satchmo/SMT/Exotic/Semiring.hs +0/−10
• Satchmo/SMT/Exotic/Semiring/Arctic.hs +0/−32
• Satchmo/SMT/Exotic/Semiring/Class.hs +0/−18
• Satchmo/SMT/Exotic/Semiring/Fuzzy.hs +0/−28
• Satchmo/SMT/Exotic/Semiring/Natural.hs +0/−9
• Satchmo/SMT/Exotic/Semiring/Rational.hs +0/−13
• Satchmo/SMT/Exotic/Semiring/Tropical.hs +0/−32
• Satchmo/SMT/Exotic/Tropical.hs +0/−80
• Satchmo/Set.hs +10/−0
• Satchmo/Set/Data.hs +71/−0
• Satchmo/Set/Op.hs +45/−0
• satchmo.cabal +20/−15

@@ -1,7 +1,7 @@ module Satchmo.Boolean.Op  ( constant-, and, or, xor, equals2, equals, implies+, and, or, xor, equals2, equals, implies, (||), (&&) , fun2, fun3 , ifThenElse, ifThenElseM , assert_fun2, assert_fun3@@ -10,7 +10,7 @@  where -import Prelude hiding ( and, or, not )+import Prelude hiding ( and, or, not, (&&), (||) ) import qualified Prelude import Control.Applicative ((<$>)) import Satchmo.MonadSAT@@ -39,6 +39,9 @@ or xs = do     y <- and $ map not xs     return $ not y++x && y = and [x,y]+x || y = or [x,y]  xor :: MonadSAT m => [ Boolean ] -> m Boolean xor [] = constant False

@@ -9,7 +9,8 @@  where -import Prelude hiding ( and, or, not )+import Prelude hiding ( and, or, not, (&&), (||) )+import qualified Prelude   import qualified Satchmo.Code as C @@ -55,9 +56,9 @@ 	 -> Integer -- ^ value 	 -> m Number constant w n = do-    xs <- if 0 <= n && n < 2^(w-1)+    xs <- if 0 <= n Prelude.&& n < 2^(w-1)           then mapM B.constant $ toBinary n-	  else if negate ( 2^(w-1)) <= n && n < 0+	  else if negate ( 2^(w-1)) <= n Prelude.&& n < 0 	  then mapM B.constant $ toBinary (n + 2^w) 	  else error "Satchmo.Integer.Data.constant"     z <- B.constant False

@@ -0,0 +1,8 @@+module Satchmo.Map ++( module Satchmo.Map.Data+)++where++import Satchmo.Map.Data

@@ -0,0 +1,39 @@+{-# language FlexibleInstances, MultiParamTypeClasses, FlexibleContexts #-}+{-# language TupleSections #-}++module Satchmo.Map.Data++( Map+) ++where++import Satchmo.Code+import qualified Satchmo.Boolean as B++import Satchmo.SAT++import qualified Data.Set as S+import qualified Data.Map.Strict as M++import Control.Monad ( guard, forM )+import Control.Applicative ( (<$>), (<*>) )++newtype Map a b = Map (M.Map a b)++instance ( Functor m, Decode m b c, Ord a )+         => Decode m (Map a b) ( M.Map a c) where+    decode (Map m) = decode m++-- | allocate an unknown map with this domain+unknown :: ( B.MonadSAT m , Ord a )+         => [a] -> m b -> m (Map a b)+unknown xs build = Map <$> M.fromList +     <$> ( forM xs $ \ x -> (x,) <$> build )++constant :: ( B.MonadSAT m , Ord a )+         => [(a,c)] -> (c -> m b) -> m (Map a b)+constant xys encode = Map <$> M.fromList +     <$> ( forM xys $ \ (x,y) -> (x,) <$> encode y )++

@@ -15,6 +15,7 @@ import Satchmo.Data import Satchmo.Code +import Control.Applicative import Control.Monad.Trans (lift) import Control.Monad.Cont  (ContT) import Control.Monad.List  (ListT)@@ -30,7 +31,7 @@  type Weight = Int -class (MonadFix m, Functor m, Monad m) => MonadSAT m where+class (MonadFix m, Applicative m, Monad m) => MonadSAT m where   fresh, fresh_forall :: m  Literal    emit  :: Clause  -> m ()

@@ -4,7 +4,7 @@  ( Relation, relation, build , identity                      -, bounds, (!), indices, assocs+, bounds, (!), indices, assocs, elems , table )  @@ -16,7 +16,7 @@ import Satchmo.SAT  import qualified Data.Array as A-import Data.Array hiding ( bounds, (!), indices, assocs )+import Data.Array ( Array, Ix ) import Data.Functor ((<$>))  import Control.Monad ( guard, forM )@@ -28,7 +28,7 @@ {-# specialize inline relation :: ( Ix a, Ix b) => ((a,b),(a,b)) -> SAT ( Relation a b ) #-}  relation bnd = do     pairs <- sequence $ do -        p <- range bnd+        p <- A.range bnd         return $ do             x <- boolean             return ( p, x )@@ -48,7 +48,7 @@       => ((a,b),(a,b))        -> [ ((a,b), Boolean ) ]       -> Relation a b -build bnd pairs = Relation $ array bnd pairs+build bnd pairs = Relation $ A.array bnd pairs   bounds :: (Ix a, Ix b) => Relation a b -> ((a,b),(a,b))@@ -58,6 +58,7 @@  assocs ( Relation r ) = A.assocs r +elems ( Relation r ) = A.elems r  Relation r ! p = r A.! p 

@@ -7,6 +7,9 @@ , reflexive , regular , empty+, complete+, disjoint+, equals )  where@@ -15,7 +18,7 @@ import qualified Prelude  import Satchmo.Code-import Satchmo.Boolean hiding (implies)+import Satchmo.Boolean hiding (implies, equals) import Satchmo.Counting import Satchmo.Relation.Data import Satchmo.Relation.Op@@ -37,6 +40,17 @@ empty r = and $ do     i <- indices r     return $ not $ r ! i++complete r = empty $ complement r++disjoint r s = do+    i <- intersection r s+    empty i++equals r s = do+    rs <- implies r s+    sr <- implies s r+    and [ rs, sr ]  symmetric :: ( Ix a, MonadSAT m) => Relation a a -> m Boolean {-# specialize inline symmetric :: ( Ix a ) => Relation a a -> SAT Boolean #-}      

@@ -29,6 +29,7 @@ import Control.Exception import Control.Monad ( when ) import Control.Monad.Fix+import Control.Applicative import System.IO  @@ -45,6 +46,10 @@     return x = SAT $ \ s -> return x     SAT m >>= f = SAT $ \ s -> do          x <- m s ; let { SAT n = f x } ; n s++instance Applicative SAT where+    pure = return+    a <*> b = a >>= \ f -> fmap f b  instance MonadFix SAT where     mfix f = SAT $ \ s -> mfix ( \ a -> unSAT (f a) s )

@@ -21,6 +21,7 @@  import Control.Exception import Control.Monad.RWS.Strict+import Control.Applicative import qualified  Data.Set as Set  -- import qualified Data.ByteString.Lazy.Char8 as BS@@ -94,7 +95,7 @@       }  newtype SAT a = SAT {unsat::RWST Handle () Accu IO a}-    deriving (MonadState Accu, MonadReader Handle, Monad, MonadIO, Functor, MonadFix)+    deriving (MonadState Accu, MonadReader Handle, Monad, MonadIO, Functor, Applicative, MonadFix)   sat :: SAT a -> IO (BS.ByteString, Header, a )

@@ -1,69 +0,0 @@-{-# language FlexibleInstances #-}-{-# language FlexibleContexts #-}-{-# language MultiParamTypeClasses #-}--module Satchmo.SMT.Exotic.Arctic where--import Satchmo.SMT.Exotic.Dict-import qualified Satchmo.SMT.Exotic.Domain--import qualified Data.Map as M--import qualified Satchmo.Unary.Op.Flexible as X-import qualified Satchmo.Unary as N-import qualified Satchmo.Boolean as B--import Satchmo.Code-import Satchmo.SAT.Mini (SAT)-import Control.Monad (forM, guard, when)--import qualified Satchmo.SMT.Exotic.Semiring.Arctic as A---data Arctic = Arctic { contents :: N.Number-                     }--minus_infinite = B.not . head . N.bits . contents--instance ( Decode m B.Boolean Bool )-         => Decode m Arctic ( A.Arctic Integer ) where-    decode a = do-        c <- decode $ contents a-        return $ if 0 == c then A.Minus_Infinite else A.Finite (c-1)--make c = do-    return $ Arctic { contents = c }--dict :: Int -     -> Dict SAT Arctic B.Boolean-dict bits = Dict { domain = Satchmo.SMT.Exotic.Domain.Arctic -  , fresh = do-    c <- N.number bits-    make c-  , finite = \ x -> return $ B.not $ minus_infinite x-  , ge = \ l r -> N.ge ( contents l ) ( contents r ) -  , gg = \ l r ->-    B.monadic B.or [ return $ minus_infinite r-                   , N.gt ( contents l ) ( contents r ) -                   ]-  , plus = \ xs -> do -    c <- X.maximum $ map contents xs-    make c-  , times = \ [s,t] -> do-          m <- B.or [ minus_infinite s, minus_infinite t ]-          let a = contents s ; b = contents t-          let width = length $ N.bits a-          when ( length ( N.bits b ) /= width ) -               $ error "Arctic.times: different bit widths"-          pairs <- sequence $ do-              (i,x) <- zip [0 .. ] $ N.bits a-              (j,y) <- zip [0 .. ] $ N.bits b-              guard $ i+j <= width-              return $ do z <- B.and [x,y] ; return (i+j, [z])-          cs <- forM ( map snd $ M.toAscList $ M.fromListWith (++) pairs ) B.or-          -- overflow is not allowed-          B.assert [ B.not $ last cs ]-          ds <- forM (init cs) $ \ c -> B.and [ B.not m, c ]-          make $ N.make ds-  }-

@@ -1,93 +0,0 @@-{-# language FlexibleInstances #-}-{-# language FlexibleContexts #-}-{-# language MultiParamTypeClasses #-}--module Satchmo.SMT.Exotic.Arctic.Integer where--import Satchmo.SMT.Exotic.Dict-import qualified Satchmo.SMT.Exotic.Domain--import qualified Data.Map as M--import qualified Satchmo.Unary.Op.Flexible as X-import qualified Satchmo.Unary as N-import qualified Satchmo.Boolean as B--import Satchmo.Code-import Satchmo.SAT.Mini (SAT)-import Control.Monad (forM, guard, when)--import qualified Satchmo.SMT.Exotic.Semiring.Arctic as A---- | (contents a !! shift a) == (number is > 0)--- (contents a !! 0) == (number is > -infty)--- (so Arctic Natural has shift = 1)-data Arctic = Arctic { contents :: N.Number-                     , shift :: Int  -                     }--minus_infinite = B.not . head . N.bits . contents-not_minus_infinite = head . N.bits . contents---instance ( Decode m B.Boolean Bool )-         => Decode m Arctic ( A.Arctic Integer ) where-    decode a = do-        c <- decode $ contents a-        return $ if 0 == c -                 then A.Minus_Infinite -                 else A.Finite $ fromIntegral (c - shift a)--constant :: Int -> A.Arctic Integer -         -> SAT Arctic-constant bits a = case a of-    A.Minus_Infinite -> do-       cs <- forM [ negate bits + 1 .. bits ] $ \ _ -> -                B.constant False-       make bits $ N.make cs-    A.Finite f -> do-       cs <- forM [ negate bits + 1 .. bits ] $ \ i -> -                B.constant ( i <= fromIntegral f )-       make bits $ N.make cs--make s c = do-    return $ Arctic { contents = c, shift = s }--dict :: Int -     -> Dict SAT Arctic B.Boolean-dict bits = Dict -  { domain = Satchmo.SMT.Exotic.Domain.Arctic -  , fresh = do-    c <- N.number $ 2 * bits-    make bits c-  -- actually the following should be called "positive" -  -- by which we mean ">= 0"  -  , finite = \ x -> -      return $ N.bits (contents x) !! (shift x - 1)-  , ge = \ l r -> N.ge ( contents l ) ( contents r ) -  , gg = \ l r ->-    B.monadic B.or [ return $ minus_infinite r-                   , N.gt ( contents l ) ( contents r ) -                   ]-  , plus = \ xs -> do -    c <- X.maximum $ map contents xs-    make bits c-  , times = \ [s,t] -> do-          m <- B.or [ minus_infinite s-                    , minus_infinite t ]-          let a = contents s ; b = contents t-          pairs <- sequence $ do-              (i,x) <- zip [negate bits + 1 .. ] $ N.bits a-              (j,y) <- zip [negate bits + 1 .. ] $ N.bits b-              guard $ i+j > negate bits -              guard $ i+j <= bits-              return $ do -                  z <- B.and [x,y, B.not m] -                  return (i+j, [z])-          cs <- forM ( map snd $ M.toAscList -                     $ M.fromListWith (++) pairs ) B.or-          B.assert [ m, head cs ] -- no underflow      -          B.assert [ B.not $ last cs ] -- no overflow-          make bits $ N.make $ init cs-  }-

@@ -1,17 +0,0 @@-module Satchmo.SMT.Exotic.Dict where--import Satchmo.SMT.Exotic.Domain--data Dict m e b = Dict -    { info :: String-    , domain :: Domain-    , fresh :: m e-    , finite :: e -> m b-    , gg :: e -> e -> m b-    , ge :: e -> e -> m b-    , plus :: [e] -> m e-    , times :: [e] -> m e-    }---

@@ -1,4 +0,0 @@-module Satchmo.SMT.Exotic.Domain where--data Domain = Natural | Arctic | Tropical | Fuzzy  deriving ( Show, Eq )-

@@ -1,63 +0,0 @@-{-# language FlexibleInstances #-}-{-# language FlexibleContexts #-}-{-# language MultiParamTypeClasses #-}--module Satchmo.SMT.Exotic.Fuzzy where--import Satchmo.SMT.Exotic.Dict-import qualified Satchmo.SMT.Exotic.Domain--import qualified Satchmo.Unary.Op.Flexible as X-import qualified Satchmo.Unary as N-import qualified Satchmo.Boolean as B--import Satchmo.Code--import qualified Data.Map as M-import qualified Satchmo.SMT.Exotic.Semiring as S-import qualified Satchmo.SMT.Exotic.Semiring.Fuzzy as F---import Satchmo.SAT.Mini ( SAT)--data Fuzzy = Fuzzy { contents :: N.Number }--minus_infinite f = B.not $ head $ N.bits $ contents f-plus_infinite f = last $ N.bits $ contents f--make = \ c -> do-    return $ Fuzzy { contents = c }---instance ( Decode m B.Boolean Bool, Decode m N.Number Integer )-         => Decode m Fuzzy ( F.Fuzzy Integer ) where-    decode a = do-        p <- decode $ plus_infinite a-        c <- decode $ contents a-        m <- decode $ minus_infinite a-        return $ if p then F.Plus_Infinite -                 else if m then F.Minus_Infinite-                 else F.Finite c--dict :: Int -> Dict SAT Fuzzy B.Boolean-dict bits = Dict { domain = Satchmo.SMT.Exotic.Domain.Fuzzy -  , fresh = do-    c <- N.number bits-    make c-  , finite = \ x -> return $ B.not $ plus_infinite x-  , ge = \ l r ->-    B.monadic B.or [ return $ plus_infinite l-                   , return $ minus_infinite r-                  , N.gt ( contents l ) ( contents r ) -                 ]-  , gg = \ l r ->-    B.monadic B.or [ return $ plus_infinite l-                  , N.gt ( contents l ) ( contents r ) -                 ]-  , plus = \ xs -> do -- min-    c <- X.minimum $ map contents xs-    make c-  , times = \ xs -> do -- max-    c <- X.maximum $ map contents xs-    make c-  }

@@ -1,80 +0,0 @@-module Satchmo.SMT.Exotic.Natural where--import Prelude hiding ( not, and, or )--import Satchmo.SMT.Exotic.Dict-import qualified Satchmo.SMT.Exotic.Domain--import qualified Satchmo.SAT.Mini-import qualified Satchmo.Boolean as B--import qualified Satchmo.Unary.Op.Fixed-import qualified Satchmo.Unary.Op.Flexible-import qualified Satchmo.Unary as Un--import qualified Satchmo.Binary as Bin-import qualified Satchmo.Binary.Op.Fixed  -import qualified Satchmo.Binary.Op.Flexible--import Control.Monad ( foldM )--data Encoding = Unary | Binary deriving Show-data Unary_Addition = Odd_Even_Merge | Bitonic_Sort | Quadratic deriving Show-data Extension = Fixed | Flexible deriving Show--unary_fixed :: Int -> Unary_Addition -            -> Dict Satchmo.SAT.Mini.SAT Un.Number B.Boolean-unary_fixed bits a = Dict-    { info = unwords [ "unary", "bits:", show bits, "(fixed)", "addition:", show a ]-    , domain = Satchmo.SMT.Exotic.Domain.Natural-    , fresh = Un.number bits-    , plus = foldM1 $ case a of-          Quadratic -> Satchmo.Unary.Op.Fixed.add_quadratic-          Bitonic_Sort -> Satchmo.Unary.Op.Fixed.add_by_bitonic_sort-          Odd_Even_Merge -> Satchmo.Unary.Op.Fixed.add_by_odd_even_merge-    , gg = Un.gt-    , ge = Un.ge-    }--unary_flexible :: Int -> Unary_Addition-               -> Dict Satchmo.SAT.Mini.SAT Un.Number B.Boolean-unary_flexible bits a = Dict-    { info = unwords [ "unary", "bits:", show bits, "(flexible)", "addition:", show a ]-    , domain = Satchmo.SMT.Exotic.Domain.Natural-    , fresh = Un.number bits-    , plus = foldM1 $ case a of-          Quadratic -> Satchmo.Unary.Op.Flexible.add_quadratic-          Bitonic_Sort -> Satchmo.Unary.Op.Flexible.add_by_bitonic_sort-          Odd_Even_Merge -> Satchmo.Unary.Op.Flexible.add_by_odd_even_merge-    , gg = Un.gt-    , ge = Un.ge-    }---binary_fixed :: Int -> Dict Satchmo.SAT.Mini.SAT Bin.Number B.Boolean-binary_fixed bits = Dict-    { info = unwords [ "binary", "bits:", show bits, "(fixed)" ]-    , domain = Satchmo.SMT.Exotic.Domain.Natural-    , fresh = Bin.number bits-    , plus = foldM1 $ Satchmo.Binary.Op.Fixed.add-    , times = foldM1 $ Satchmo.Binary.Op.Fixed.times-    , gg = Bin.gt-    , ge = Bin.ge-    , finite = \ n -> B.or $ Bin.bits n-    }---binary_flexible :: Int -> Dict Satchmo.SAT.Mini.SAT Bin.Number B.Boolean-binary_flexible bits = Dict-    { info = unwords [ "binary", "bits:", show bits, "(flexbible)" ]-    , domain = Satchmo.SMT.Exotic.Domain.Natural-    , fresh = Bin.number bits-    , plus = foldM1 $ Satchmo.Binary.Op.Flexible.add-    , times = foldM1 $ Satchmo.Binary.Op.Flexible.times-    , gg = Bin.gt-    , ge = Bin.ge-    , finite = \ n -> B.or $ Bin.bits n-    }--foldM1 :: Monad m => ( b -> b -> m b ) -> [b] -> m b-foldM1 f (x:xs) = foldM f x xs

@@ -1,10 +0,0 @@-{-# language TypeSynonymInstances, FlexibleInstances, UndecidableInstances #-}--module Satchmo.SMT.Exotic.Semiring --( module Satchmo.SMT.Exotic.Semiring.Class )--where--import Satchmo.SMT.Exotic.Semiring.Class-

@@ -1,32 +0,0 @@-{-# language DeriveDataTypeable #-}--module Satchmo.SMT.Exotic.Semiring.Arctic where--import Satchmo.SMT.Exotic.Semiring.Class--import Data.Typeable--data Arctic a = Minus_Infinite | Finite a deriving (Eq, Ord, Typeable)--instance Functor Arctic where-    fmap f a = case a of-        Minus_Infinite -> Minus_Infinite-        Finite x -> Finite $ f x--instance Show a => Show ( Arctic a ) where -    show a = case a of-        Minus_Infinite -> "-"-        Finite x -> show x--instance (Ord a, Num a) => Semiring (Arctic a) where-    strictness _ = Half-    nonnegative a = True -- ??-    strictly_positive a = case a of Finite x -> x >= 0 ; _ -> False-    ge = (>=)-    gt x y = y == Minus_Infinite || (x > y)-    plus = max-    zero = Minus_Infinite-    times x y = case (x,y) of-        (Finite a, Finite b) -> Finite (a+b)-        _ -> Minus_Infinite-    one = Finite 0         

@@ -1,18 +0,0 @@-{-# language TypeSynonymInstances, FlexibleInstances, UndecidableInstances #-}--module Satchmo.SMT.Exotic.Semiring.Class where--data Strictness = Full | Half deriving ( Eq, Ord, Show )--class Semiring a where-    strictness :: a -> Strictness-    nonnegative :: a -> Bool-    strictly_positive :: a -> Bool-    ge :: a -> a -> Bool-    gt :: a -> a -> Bool-    plus  :: a -> a -> a-    zero  :: a-    times :: a -> a -> a-    one   :: a--

@@ -1,28 +0,0 @@-module Satchmo.SMT.Exotic.Semiring.Fuzzy where--import Satchmo.SMT.Exotic.Semiring.Class--data Fuzzy a = Minus_Infinite | Finite a | Plus_Infinite deriving (Eq, Ord)--instance Functor Fuzzy where-    fmap f a = case a of-        Minus_Infinite -> Minus_Infinite-        Finite x -> Finite $ f x-        Plus_Infinite -> Plus_Infinite--instance Show a => Show ( Fuzzy a ) where -    show a = case a of-        Minus_Infinite -> "-"-        Finite x -> show x-        Plus_Infinite -> "+"--instance (Ord a, Num a) => Semiring (Fuzzy a) where-    strictness _ = Half-    nonnegative a = case a of Plus_Infinite -> False ; _ -> True-    strictly_positive = nonnegative -- CHECK-    ge x y = x == Plus_Infinite || (x > y) || y == Minus_Infinite -    gt x y = x == Plus_Infinite || (x > y)-    plus = min-    zero = Plus_Infinite-    times = max-    one = Minus_Infinite

@@ -1,9 +0,0 @@-module Satchmo.SMT.Exotic.Semiring.Natural where--import Satchmo.SMT.Exotic.Semiring.Class--instance Semiring Integer where    -  strictness _ = Full-  nonnegative x = x >= 0 ; strictly_positive x = x >= 1 -  ge = (>=) ; gt = (>)-  plus = (+) ; zero = 0 ; times = (*) ; one = 1

@@ -1,13 +0,0 @@-{-# language TypeSynonymInstances #-}-{-# language FlexibleInstances #-}--module Satchmo.SMT.Exotic.Semiring.Rational where--import Data.Ratio-import Satchmo.SMT.Exotic.Semiring.Class    --instance Semiring Rational where    -    strictness _ = Full-    nonnegative x = x >= 0 ; strictly_positive x = x >= 1 -    ge = (>=) ; gt = (>)-    plus = (+) ; zero = 0 ; times = (*) ; one = 1

@@ -1,32 +0,0 @@-{-# language DeriveDataTypeable #-}--module Satchmo.SMT.Exotic.Semiring.Tropical where--import Satchmo.SMT.Exotic.Semiring.Class--import Data.Typeable--data Tropical a = Finite a | Plus_Infinite deriving (Eq, Ord, Typeable)--instance Functor Tropical where-    fmap f a = case a of-        Finite x -> Finite $ f x-        Plus_Infinite -> Plus_Infinite--instance Show a => Show ( Tropical a ) where -    show a = case a of-        Plus_Infinite -> "+"-        Finite x -> show x--instance (Ord a, Num a) => Semiring (Tropical a) where-    strictness _ = Half-    nonnegative a = True -- ??-    strictly_positive a = case a of Finite x -> x >= 0 ; _ -> False-    ge = (>=)-    gt x y = x == Plus_Infinite || (x > y)-    plus = min-    zero = Plus_Infinite-    times x y = case (x,y) of-        (Finite a, Finite b) -> Finite (a+b)-        _ -> Plus_Infinite-    one = Finite 0         

@@ -1,80 +0,0 @@--- | fixed bit width tropical numbers,--- table lookup for ring multiplication--{-# language FlexibleInstances #-}-{-# language FlexibleContexts #-}-{-# language MultiParamTypeClasses #-}--module Satchmo.SMT.Exotic.Tropical where--import Satchmo.SMT.Exotic.Dict-import qualified Satchmo.SMT.Exotic.Domain--import qualified Data.Map as M---- see below (implementation of "times") for switching to Fixed--- import qualified Satchmo.Unary.Op.Flexible as X-import qualified Satchmo.Unary.Op.Fixed as X-import qualified Satchmo.Unary as N--import qualified Satchmo.Boolean as B--import Satchmo.Code-import Satchmo.SAT.Mini (SAT)---import Control.Monad ( foldM, forM, guard, when )--import qualified Satchmo.SMT.Exotic.Semiring.Tropical as T---data Tropical = Tropical { contents :: N.Number }--plus_infinite = last . N.bits . contents--instance ( Decode m B.Boolean Bool )-         => Decode m Tropical ( T.Tropical Integer ) where-    decode a = do-        p <- decode $ plus_infinite a-        c <- decode $ contents a-        return $ if p then T.Plus_Infinite else T.Finite c--make c = do-    return $ Tropical { contents = c }--dict :: Int -     -> Dict SAT  Tropical B.Boolean-dict bits = Dict { domain = Satchmo.SMT.Exotic.Domain.Tropical -  , fresh = do-    c <- N.number bits-    make c-  , finite = \ x -> return $ B.not $ plus_infinite x-  , ge = \ l r -> N.ge ( contents l ) ( contents r ) -  , gg = \ l r ->-    B.monadic B.or [ return $ plus_infinite l-                   , N.gt ( contents l ) ( contents r ) -                   ]-  , plus = \ xs -> do -    c <- X.minimum $ for xs contents-    make c-  , times = \ [s,t] -> do-          p <- B.or [ plus_infinite s, plus_infinite t ]-          let a = contents s ; b = contents t-          let width = length $ N.bits a-          when ( length ( N.bits b ) /= width ) -               $ error "Tropical.times: different bit widths"-          t <- B.constant True-          pairs <- sequence $ do-              (i,x) <- zip [0 .. ] $ t : N.bits a-              (j,y) <- zip [0 .. ] $ t : N.bits b-              guard $ i+j > 0-              guard $ i+j <= width-              return $ do z <- B.and [x,y] ; return (i+j, [z])-          cs <- forM ( map snd $ M.toAscList $ M.fromListWith (++) pairs ) B.or-          -- if result is not plus_inf, then overflow is not allowed-          B.assert [ p , B.not $ last cs ]-          make $ N.make cs-  }---for = flip map

@@ -0,0 +1,10 @@+module Satchmo.Set ++( module Satchmo.Set.Data+, module Satchmo.Set.Op+)++where++import Satchmo.Set.Data+import Satchmo.Set.Op

@@ -0,0 +1,71 @@+{-# language FlexibleInstances, MultiParamTypeClasses, FlexibleContexts #-}+{-# language TupleSections #-}++module Satchmo.Set.Data++( Set , unknown, unknownSingleton, constant+, member, keys, keysSet, keys, assocs, elems+, all2, common2+) ++where++import Satchmo.Code+import qualified Satchmo.Boolean as B++import Satchmo.SAT++import qualified Data.Set as S+import qualified Data.Map.Strict as M++import Satchmo.Map++import Control.Monad ( guard, forM )+import Control.Applicative ( (<$>), (<*>) )+import Data.List ( tails )++newtype Set a = Set (M.Map a B.Boolean)++instance ( Functor m, Decode m B.Boolean Bool, Ord a )+         => Decode m (Set a) ( S.Set a) where+    decode (Set m) = +        M.keysSet <$> M.filter id <$> decode m++keys (Set m) = M.keys m+keysSet (Set m) = M.keysSet m+assocs (Set m) = M.assocs m+elems (Set m) = M.elems m++member x (Set m) = case M.lookup x m of+    Nothing -> B.constant False+    Just y  -> return y+++-- | allocate an unknown subset of these elements+unknown :: ( B.MonadSAT m , Ord a )+         => [a] -> m (Set a)+unknown xs = Set <$> M.fromList +     <$> ( forM xs $ \ x -> (x,) <$> B.boolean )++unknownSingleton xs = do+    s <- unknown xs+    B.assert $ elems s+    sequence_ $ do +       x : ys <- tails $ elems s ; y <- ys+       return $ B.assert [ B.not x, B.not y ]+    return s++constant :: ( B.MonadSAT m , Ord a )+         => [a] -> m (Set a)+constant xs = Set <$> M.fromList +     <$> ( forM xs $ \ x -> (x,) <$> B.constant True )++all2 f s t = B.and+ =<< forM ( S.toList $ S.union (keysSet s)(keysSet t))+ ( \ x -> do a <- member x s; b <- member x t; f a b )++common2 f s t = Set <$> M.fromList <$>+ forM ( S.toList $ S.union (keysSet s)(keysSet t))+ ( \ x -> do a <- member x s; b <- member x t+             y <- f a b ; return (x,y) )+

@@ -0,0 +1,45 @@+{-# language NoMonomorphismRestriction #-}++module Satchmo.Set.Op where++import Satchmo.Set.Data+import qualified Satchmo.Boolean as B+import qualified Satchmo.Counting as C++import qualified Data.Set as S+import Data.List ( tails )++import Control.Monad ( guard, forM, liftM2 )+import Control.Applicative ( (<$>), (<*>) )++null :: (Ord a, B.MonadSAT m) => Set a -> m B.Boolean+null s = B.not <$> B.or ( elems s )++equals :: (Ord a, B.MonadSAT m) => Set a -> Set a -> m B.Boolean+equals = all2 B.equals2 ++isSubsetOf :: (Ord a, B.MonadSAT m) => Set a -> Set a -> m B.Boolean+isSubsetOf = all2 $ B.implies++isSupersetOf :: (Ord a, B.MonadSAT m) => Set a -> Set a -> m B.Boolean+isSupersetOf = flip isSubsetOf++isSingleton :: (Ord a, B.MonadSAT m) => Set a -> m B.Boolean+isSingleton s = do+   C.exactly 1 $ elems s++isDisjoint :: (Ord a, B.MonadSAT m) => Set a -> Set a -> m B.Boolean+isDisjoint = all2 +    $ \ x y -> B.or [ B.not x, B.not y ]++union :: (Ord a, B.MonadSAT m) => Set a -> Set a -> m (Set a)+union = common2 (B.||) ++intersection :: (Ord a, B.MonadSAT m) => Set a -> Set a -> m (Set a)+intersection = common2 (B.&&)++difference :: (Ord a, B.MonadSAT m) => Set a -> Set a -> m (Set a)+difference = common2 ( \ x y -> x B.&& (B.not y) )+++

@@ -1,5 +1,5 @@ Name:           satchmo-Version:        2.6.0+Version:        2.8.1  License:        GPL License-file:	gpl-2.0.txt@@ -59,25 +59,30 @@         -- Satchmo.SAT.Sequence         -- Satchmo.Simple         -- Satchmo.SAT.Weighted+        Satchmo.Set+        Satchmo.Set.Data+        Satchmo.Set.Op+        Satchmo.Map+        Satchmo.Map.Data         Satchmo.Numeric         Satchmo.Binary.Numeric         Satchmo.BinaryTwosComplement.Numeric         Satchmo.Integer.Difference         Satchmo.Polynomial.Numeric-        Satchmo.SMT.Exotic.Domain-        Satchmo.SMT.Exotic.Dict-        Satchmo.SMT.Exotic.Arctic-        Satchmo.SMT.Exotic.Arctic.Integer-        Satchmo.SMT.Exotic.Fuzzy-        Satchmo.SMT.Exotic.Tropical-        Satchmo.SMT.Exotic.Natural-        Satchmo.SMT.Exotic.Semiring.Rational-        Satchmo.SMT.Exotic.Semiring.Arctic-        Satchmo.SMT.Exotic.Semiring.Fuzzy-        Satchmo.SMT.Exotic.Semiring.Tropical-        Satchmo.SMT.Exotic.Semiring.Natural-        Satchmo.SMT.Exotic.Semiring.Class-        Satchmo.SMT.Exotic.Semiring+        -- Satchmo.SMT.Exotic.Domain+        -- Satchmo.SMT.Exotic.Dict+        -- Satchmo.SMT.Exotic.Arctic+        -- Satchmo.SMT.Exotic.Arctic.Integer+        -- Satchmo.SMT.Exotic.Fuzzy+        -- Satchmo.SMT.Exotic.Tropical+        -- Satchmo.SMT.Exotic.Natural+        -- Satchmo.SMT.Exotic.Semiring.Rational+        -- Satchmo.SMT.Exotic.Semiring.Arctic+        -- Satchmo.SMT.Exotic.Semiring.Fuzzy+        -- Satchmo.SMT.Exotic.Semiring.Tropical+        -- Satchmo.SMT.Exotic.Semiring.Natural+        -- Satchmo.SMT.Exotic.Semiring.Class+        -- Satchmo.SMT.Exotic.Semiring     Other-modules:         Satchmo.Binary.Data         Satchmo.BinaryTwosComplement.Data