diff --git a/Satchmo/Boolean/Op.hs b/Satchmo/Boolean/Op.hs
--- a/Satchmo/Boolean/Op.hs
+++ b/Satchmo/Boolean/Op.hs
@@ -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
diff --git a/Satchmo/Integer/Data.hs b/Satchmo/Integer/Data.hs
--- a/Satchmo/Integer/Data.hs
+++ b/Satchmo/Integer/Data.hs
@@ -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
diff --git a/Satchmo/Map.hs b/Satchmo/Map.hs
new file mode 100644
--- /dev/null
+++ b/Satchmo/Map.hs
@@ -0,0 +1,8 @@
+module Satchmo.Map 
+
+( module Satchmo.Map.Data
+)
+
+where
+
+import Satchmo.Map.Data
diff --git a/Satchmo/Map/Data.hs b/Satchmo/Map/Data.hs
new file mode 100644
--- /dev/null
+++ b/Satchmo/Map/Data.hs
@@ -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 )
+
+
diff --git a/Satchmo/MonadSAT.hs b/Satchmo/MonadSAT.hs
--- a/Satchmo/MonadSAT.hs
+++ b/Satchmo/MonadSAT.hs
@@ -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 ()
diff --git a/Satchmo/Relation/Data.hs b/Satchmo/Relation/Data.hs
--- a/Satchmo/Relation/Data.hs
+++ b/Satchmo/Relation/Data.hs
@@ -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
 
diff --git a/Satchmo/Relation/Prop.hs b/Satchmo/Relation/Prop.hs
--- a/Satchmo/Relation/Prop.hs
+++ b/Satchmo/Relation/Prop.hs
@@ -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 #-}      
diff --git a/Satchmo/SAT/Mini.hs b/Satchmo/SAT/Mini.hs
--- a/Satchmo/SAT/Mini.hs
+++ b/Satchmo/SAT/Mini.hs
@@ -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 )
diff --git a/Satchmo/SAT/Tmpfile.hs b/Satchmo/SAT/Tmpfile.hs
--- a/Satchmo/SAT/Tmpfile.hs
+++ b/Satchmo/SAT/Tmpfile.hs
@@ -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 )
diff --git a/Satchmo/SMT/Exotic/Arctic.hs b/Satchmo/SMT/Exotic/Arctic.hs
deleted file mode 100644
--- a/Satchmo/SMT/Exotic/Arctic.hs
+++ /dev/null
@@ -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
-  }
-
diff --git a/Satchmo/SMT/Exotic/Arctic/Integer.hs b/Satchmo/SMT/Exotic/Arctic/Integer.hs
deleted file mode 100644
--- a/Satchmo/SMT/Exotic/Arctic/Integer.hs
+++ /dev/null
@@ -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
-  }
-
diff --git a/Satchmo/SMT/Exotic/Dict.hs b/Satchmo/SMT/Exotic/Dict.hs
deleted file mode 100644
--- a/Satchmo/SMT/Exotic/Dict.hs
+++ /dev/null
@@ -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
-    }
-
-
-
diff --git a/Satchmo/SMT/Exotic/Domain.hs b/Satchmo/SMT/Exotic/Domain.hs
deleted file mode 100644
--- a/Satchmo/SMT/Exotic/Domain.hs
+++ /dev/null
@@ -1,4 +0,0 @@
-module Satchmo.SMT.Exotic.Domain where
-
-data Domain = Natural | Arctic | Tropical | Fuzzy  deriving ( Show, Eq )
-
diff --git a/Satchmo/SMT/Exotic/Fuzzy.hs b/Satchmo/SMT/Exotic/Fuzzy.hs
deleted file mode 100644
--- a/Satchmo/SMT/Exotic/Fuzzy.hs
+++ /dev/null
@@ -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
-  }
diff --git a/Satchmo/SMT/Exotic/Natural.hs b/Satchmo/SMT/Exotic/Natural.hs
deleted file mode 100644
--- a/Satchmo/SMT/Exotic/Natural.hs
+++ /dev/null
@@ -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
diff --git a/Satchmo/SMT/Exotic/Semiring.hs b/Satchmo/SMT/Exotic/Semiring.hs
deleted file mode 100644
--- a/Satchmo/SMT/Exotic/Semiring.hs
+++ /dev/null
@@ -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
-
diff --git a/Satchmo/SMT/Exotic/Semiring/Arctic.hs b/Satchmo/SMT/Exotic/Semiring/Arctic.hs
deleted file mode 100644
--- a/Satchmo/SMT/Exotic/Semiring/Arctic.hs
+++ /dev/null
@@ -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         
diff --git a/Satchmo/SMT/Exotic/Semiring/Class.hs b/Satchmo/SMT/Exotic/Semiring/Class.hs
deleted file mode 100644
--- a/Satchmo/SMT/Exotic/Semiring/Class.hs
+++ /dev/null
@@ -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
-
-
diff --git a/Satchmo/SMT/Exotic/Semiring/Fuzzy.hs b/Satchmo/SMT/Exotic/Semiring/Fuzzy.hs
deleted file mode 100644
--- a/Satchmo/SMT/Exotic/Semiring/Fuzzy.hs
+++ /dev/null
@@ -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
diff --git a/Satchmo/SMT/Exotic/Semiring/Natural.hs b/Satchmo/SMT/Exotic/Semiring/Natural.hs
deleted file mode 100644
--- a/Satchmo/SMT/Exotic/Semiring/Natural.hs
+++ /dev/null
@@ -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
diff --git a/Satchmo/SMT/Exotic/Semiring/Rational.hs b/Satchmo/SMT/Exotic/Semiring/Rational.hs
deleted file mode 100644
--- a/Satchmo/SMT/Exotic/Semiring/Rational.hs
+++ /dev/null
@@ -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
diff --git a/Satchmo/SMT/Exotic/Semiring/Tropical.hs b/Satchmo/SMT/Exotic/Semiring/Tropical.hs
deleted file mode 100644
--- a/Satchmo/SMT/Exotic/Semiring/Tropical.hs
+++ /dev/null
@@ -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         
diff --git a/Satchmo/SMT/Exotic/Tropical.hs b/Satchmo/SMT/Exotic/Tropical.hs
deleted file mode 100644
--- a/Satchmo/SMT/Exotic/Tropical.hs
+++ /dev/null
@@ -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
diff --git a/Satchmo/Set.hs b/Satchmo/Set.hs
new file mode 100644
--- /dev/null
+++ b/Satchmo/Set.hs
@@ -0,0 +1,10 @@
+module Satchmo.Set 
+
+( module Satchmo.Set.Data
+, module Satchmo.Set.Op
+)
+
+where
+
+import Satchmo.Set.Data
+import Satchmo.Set.Op
diff --git a/Satchmo/Set/Data.hs b/Satchmo/Set/Data.hs
new file mode 100644
--- /dev/null
+++ b/Satchmo/Set/Data.hs
@@ -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) )
+
diff --git a/Satchmo/Set/Op.hs b/Satchmo/Set/Op.hs
new file mode 100644
--- /dev/null
+++ b/Satchmo/Set/Op.hs
@@ -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) )
+
+
+
diff --git a/satchmo.cabal b/satchmo.cabal
--- a/satchmo.cabal
+++ b/satchmo.cabal
@@ -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