diff --git a/Satchmo/Binary/Data.hs b/Satchmo/Binary/Data.hs
--- a/Satchmo/Binary/Data.hs
+++ b/Satchmo/Binary/Data.hs
@@ -1,9 +1,11 @@
-{-# language MultiParamTypeClasses #-}
+{-# language MultiParamTypeClasses, FlexibleInstances, FlexibleContexts, UndecidableInstances #-}
 
+
 module Satchmo.Binary.Data
 
 ( Number, bits, make
-, width, number, constant
+, width, number, constant, constantWidth
+, fromBinary, toBinary, toBinaryWidth
 )
 
 where
@@ -19,11 +21,10 @@
 
 data Number = Number 
             { bits :: [ Boolean ] -- lsb first
-            , decode :: C.Decoder Integer
             }
 
-instance C.Decode Number Integer where
-    decode = decode
+instance C.Decode m Boolean Bool => C.Decode m Number Integer where
+    decode n = do ys <- mapM C.decode (bits n) ; return $ fromBinary ys
 
 width :: Number -> Int
 width n = length $ bits n
@@ -37,7 +38,6 @@
 make :: [ Boolean ] -> Number
 make xs = Number
            { bits = xs
-           , decode = do ys <- mapM C.decode xs ; return $ fromBinary ys
            }
 
 fromBinary :: [ Bool ] -> Integer
@@ -49,9 +49,22 @@
     let (d,m) = divMod n 2
     in  toEnum ( fromIntegral m ) : toBinary d
 
--- | declare a number constant 
+-- | @toBinaryWidth w@ converts to binary using at least @w@ bits
+toBinaryWidth :: Int -> Integer -> [Bool]
+toBinaryWidth width n =
+    let bs = toBinary n
+        leadingZeros = max 0 $ width - (length bs)
+    in
+      bs ++ (replicate leadingZeros False)
+
+-- | Declare a number constant 
 constant :: MonadSAT m => Integer -> m Number
 constant n = do
     xs <- mapM B.constant $ toBinary n
     return $ make xs
 
+-- | @constantWidth w@ declares a number constant using at least @w@ bits
+constantWidth :: MonadSAT m => Int -> Integer -> m Number
+constantWidth width n = do
+  xs <- mapM B.constant $ toBinaryWidth width n
+  return $ make xs
diff --git a/Satchmo/Binary/Numeric.hs b/Satchmo/Binary/Numeric.hs
new file mode 100644
--- /dev/null
+++ b/Satchmo/Binary/Numeric.hs
@@ -0,0 +1,19 @@
+module Satchmo.Binary.Numeric where
+
+-- import qualified Satchmo.Binary.Op.Flexible as F
+import qualified Satchmo.Binary.Op.Fixed as F
+
+import qualified Satchmo.Numeric as N
+
+instance N.Constant F.Number where
+    constant = F.constant  
+    
+instance N.Create F.Number where    
+    create = F.number
+
+instance N.Numeric F.Number where
+    equal = F.equals
+    greater_equal = F.ge
+    plus = F.add
+    minus = error "Satchmo.Binary does not implement minus"
+    times = F.times 
diff --git a/Satchmo/Binary/Op/Common.hs b/Satchmo/Binary/Op/Common.hs
--- a/Satchmo/Binary/Op/Common.hs
+++ b/Satchmo/Binary/Op/Common.hs
@@ -3,18 +3,25 @@
 ( iszero
 , equals, lt, le, ge, eq, gt
 , full_adder, half_adder
+, select
+, max, min, maximum
 )
 
 where
 
-import Prelude hiding ( and, or, not, compare )
+import Prelude hiding ( and, or, not, compare, max, min, maximum )
+import qualified Prelude
 
 import qualified Satchmo.Code as C
 
-import Satchmo.Boolean (MonadSAT, Boolean, Booleans, fun2, fun3, and, or, not, xor, assert, boolean)
+import Satchmo.Boolean 
+   (MonadSAT, Boolean, Booleans
+   , fun2, fun3, and, or, not, xor, assertOr, assert, boolean)
 import qualified  Satchmo.Boolean as B
-import Satchmo.Binary.Data (Number, make, bits)
+import Satchmo.Binary.Data (Number, number, make, bits, width)
 
+import Control.Monad ( forM, foldM )
+
 import Satchmo.Counting
 
 import Control.Monad ( forM )
@@ -24,16 +31,21 @@
 
 equals :: (MonadSAT m) =>  Number -> Number -> m Boolean
 equals a b = do
-    equals' ( bits a ) ( bits b )
-
-
+    -- equals' ( bits a ) ( bits b )
+    let m = Prelude.min ( width a ) ( width b )
+    let ( a1, a2 ) = splitAt m $ bits a
+    let ( b1, b2 ) = splitAt m $ bits b
+    common <- forM ( zip a1 b1 ) $ \ (x,y) -> fun2 (==) x y
+    and $ common ++ map not ( a2 ++ b2 ) 
+    
 equals' :: (MonadSAT m) =>  Booleans -> Booleans -> m Boolean
-equals' xs ys = do
-    let n = min ( length xs ) ( length ys )
-        (a,b) = splitAt n xs
-        (c,d) = splitAt n ys
-    ac <- forM ( zip a c ) $ \ (x,y) -> fun2 (==) x y
-    and $ map not (b++d) ++ ac
+equals' [] [] = B.constant True
+equals' (x:xs) (y:ys) = do
+    z <- fun2 (==) x y
+    rest <- equals' xs ys
+    and [ z, rest ]
+equals' xs [] = and $ map not xs
+equals' [] ys = and $ map not ys
 
 le,lt,ge,gt,eq :: MonadSAT m => Number -> Number -> m Boolean
 le x y = do (l,e) <- compare x y ; or [l,e]
@@ -42,6 +54,34 @@
 gt x y = lt y x
 eq = equals
 
+max :: MonadSAT m => Number -> Number -> m Number
+max a b = do
+    c <- number $ Prelude.max ( width a ) ( width b )
+    ca <- equals c a
+    cb <- equals c b
+    g <- gt a b
+    assert [ not g , ca ]
+    assert [     g , cb ]
+    return c
+
+min :: MonadSAT m => Number -> Number -> m Number
+min a b = do
+    c <- number $ Prelude.max ( width a ) ( width b )
+    ca <- equals c a
+    cb <- equals c b
+    g <- lt a b
+    assert [ not g , ca ]
+    assert [     g , cb ]
+    return c
+
+maximum (x:xs) = foldM max x xs
+
+-- | i flag is True, then the number itself, and zero otherwise.
+select :: MonadSAT m => Boolean -> Number -> m Number
+select flag a = do
+    bs <- forM ( bits a ) $ \ b -> and [ flag, b ]
+    return $ make bs
+
 compare :: MonadSAT m => Number -> Number 
         -> m ( Boolean, Boolean )
 compare a b = compare' ( bits a ) ( bits b )
@@ -101,16 +141,16 @@
        
 full_adder_0 p1 p2 p3 = do
     p4 <- boolean ; p5 <- boolean
-    assert [not p2,p4,p5]
-    assert [p2,not p4,not p5]
-    assert [not p1,not p3,p5]
-    assert [not p1,not p2,not p3,p4]
-    assert [not p1,not p2,p3,not p4]
-    assert [not p1,p2,p3,p4]
-    assert [p1,p3,not p5]
-    assert [p1,not p2,not p3,not p4]
-    assert [p1,p2,not p3,p4]
-    assert [p1,p2,p3,not p4]
+    assertOr [not p2,p4,p5]
+    assertOr [p2,not p4,not p5]
+    assertOr [not p1,not p3,p5]
+    assertOr [not p1,not p2,not p3,p4]
+    assertOr [not p1,not p2,p3,not p4]
+    assertOr [not p1,p2,p3,p4]
+    assertOr [p1,p3,not p5]
+    assertOr [p1,not p2,not p3,not p4]
+    assertOr [p1,p2,not p3,p4]
+    assertOr [p1,p2,p3,not p4]
     return ( p4, p5 )
 
 full_adder_plain a b c = do
@@ -140,12 +180,12 @@
 
 half_adder_0 p1 p2 = do
     p3 <- boolean ; p4 <- boolean
-    assert [not p2,p3,p4]
-    assert [p2,not p4]
-    assert [not p1,p3,p4]
-    assert [not p1,not p2,not p3]
-    assert [p1,not p4]
-    assert [p1,p2,not p3]
+    assertOr [not p2,p3,p4]
+    assertOr [p2,not p4]
+    assertOr [not p1,p3,p4]
+    assertOr [not p1,not p2,not p3]
+    assertOr [p1,not p4]
+    assertOr [p1,p2,not p3]
     return ( p3, p4 )
 
 half_adder_plain a b = do
diff --git a/Satchmo/Binary/Op/Fixed.hs b/Satchmo/Binary/Op/Fixed.hs
--- a/Satchmo/Binary/Op/Fixed.hs
+++ b/Satchmo/Binary/Op/Fixed.hs
@@ -9,24 +9,30 @@
 module Satchmo.Binary.Op.Fixed
 
 ( restricted
-, add, times
+, add, times, dot_product, dot_product'
 , module Satchmo.Binary.Data
 , module Satchmo.Binary.Op.Common
+, restrictedTimes
 )
 
 where
 
-import Prelude hiding ( and, or, not )
+import Prelude hiding ( and, or, not, min, max )
+import qualified Prelude
+import Control.Monad (foldM)
 
 import qualified Satchmo.Code as C
 
 import Satchmo.Boolean
 import Satchmo.Binary.Data
 import Satchmo.Binary.Op.Common
+import qualified Satchmo.Binary.Op.Times as T
 import qualified Satchmo.Binary.Op.Flexible as Flexible
 
 import Satchmo.Counting
 
+import Control.Monad ( forM, when )
+
 import Data.Map ( Map )
 import qualified Data.Map as M
 
@@ -35,7 +41,7 @@
 restricted :: (MonadSAT m) => Int -> Number -> m Number
 restricted w a = do
     let ( low, high ) = splitAt w $ bits a
-    sequence $ do x <- high ; return $ assert [ not x ]
+    sequence $ do x <- high ; return $ assertOr [ not x ]
     return $ make low
 
 -- | result bit width is max of argument bit widths.
@@ -43,14 +49,14 @@
 add :: (MonadSAT m) => Number -> Number -> m Number
 add a b = do
     false <- Satchmo.Boolean.constant False
-    let w = max ( width a ) ( width b )
+    let w = Prelude.max ( width a ) ( width b )
     zs <- add_with_carry w false ( bits a ) ( bits b )
     return $ make zs 
 
 add_with_carry :: (MonadSAT m) => Int -> Boolean -> Booleans -> Booleans -> m Booleans
 add_with_carry w c xxs yys = case ( xxs, yys ) of
     _ | w <= 0 -> do
-        sequence_ $ do p <- c : xxs ++ yys ; return $ assert [ not p ]
+        sequence_ $ do p <- c : xxs ++ yys ; return $ assertOr [ not p ]
         return []
     ( [] , [] ) -> return [ c ]
     ( [], y : ys) -> do
@@ -67,63 +73,41 @@
 -- if overflow occurs, then formula is unsatisfiable.
 times :: (MonadSAT m) => Number -> Number -> m Number
 times a b = do 
-    let w = max ( width a ) ( width b ) 
-    -- restricted_times w a b
-    better_times w a b
+    let w = Prelude.max ( width a ) ( width b ) 
+    T.times (Just w) a b
 
-restricted_times :: (MonadSAT m) 
-                 => Int 
-                 -> Number -> Number -> m Number
-restricted_times w a b = case bits a of
-    [] -> return $ make []
-    _ | w <= 0 -> do
-        monadic assert [ Flexible.iszero a, Flexible.iszero b ]
-        return $ make []
-    x : xs -> do 
-        xys  <- Flexible.times1 x b
-        xsys <- if null $ bits b 
-                then return $ make [] 
-                else do
-                       zs <- restricted_times (w-1) b (make xs)
-                       Flexible.shift zs
-        s <- Flexible.add xys xsys
-        restricted w s
+dot_product :: (MonadSAT m) 
+             => Int -> [ Number ] -> [ Number ] -> m Number
+dot_product w xs ys = do
+    T.dot_product (Just w) xs ys
 
--------------------------------------------------- 
+dot_product' xs ys = do
+    let l = length . bits
+        w = Prelude.maximum $ 0 : map l ( xs ++ ys )
+    dot_product w xs ys    
 
-better_times w a b = do
-    kzs <- sequence $ do
-          ( i , x ) <- zip [ 0 .. ] $ bits a
-          ( j , y ) <- zip [ 0 .. ] $ bits b
-          return $ 
-              if i+j >= w 
-              then do 
-                  assert [ not x, not y ]
-                  return ( i+j, [] )
-              else do 
-                  z <- and [ x, y ]
-                  return ( i+j , [z] ) 
-    zs <- reduce $ take w
-                 $ M.elems $ M.fromListWith (++) kzs
-    return $ make zs
 
+-- Ignores overflows
+restrictedAdd :: (MonadSAT m) => Number -> Number -> m Number
+restrictedAdd a b = do
+  zero <- Satchmo.Boolean.constant False
+  (result, _) <- Flexible.add_with_carry zero (bits a) (bits b)
+  return $ make result
 
-reduce ( ( x:y:z:ps) : qss ) = do
-    ( r, c ) <- full_adder x y z
-    qss' <- plugin c qss
-    reduce $ ( ps ++ [r] ) : qss' 
-reduce ( ( x:y:[]) : qss ) = do
-    ( r, c ) <- half_adder x y 
-    qss' <- plugin c qss
-    reduce $ [r] : qss' 
-reduce ( ( x:[]) : qss ) = do
-    xs <- reduce qss
-    return $ x : xs
-reduce [] = return []
+-- Ignores overflows
+restrictedShift :: (MonadSAT m) => Number -> m Number
+restrictedShift a = do
+  zero <- Satchmo.Boolean.constant False
+  return $ make $ zero : (take (width a - 1) $ bits a)
 
-plugin c [] = do
-    assert [ not c ]
-    return []
-plugin c (qs : qss) = 
-    return ((c:qs) : qss)
+-- Ignores overflows
+restrictedTimes :: (MonadSAT m) => Number -> Number -> m Number
+restrictedTimes as bs = do
+  result <- foldM (\(as',sum) b -> do
+                       summand <- Flexible.times1 b as'
+                       sum' <- sum `restrictedAdd` summand
+                       nextAs' <- restrictedShift as'
+                       return (nextAs', sum')
+                  ) (as, make []) $ bits bs
+  return $ snd result
 
diff --git a/Satchmo/Binary/Op/Flexible.hs b/Satchmo/Binary/Op/Flexible.hs
--- a/Satchmo/Binary/Op/Flexible.hs
+++ b/Satchmo/Binary/Op/Flexible.hs
@@ -5,7 +5,7 @@
 
 module Satchmo.Binary.Op.Flexible
 
-( add, times
+( add, times, dot_product
 , add_with_carry, times1, shift
 , module Satchmo.Binary.Data
 , module Satchmo.Binary.Op.Common
@@ -19,6 +19,7 @@
 import qualified Satchmo.Code as C
 import Satchmo.Binary.Data
 import Satchmo.Binary.Op.Common
+import qualified Satchmo.Binary.Op.Times as T
 import Satchmo.Counting
 
 import qualified Data.Map as M
@@ -46,8 +47,13 @@
     return ( z : zs, cout )
 
 times :: (MonadSAT m) => Number -> Number -> m Number
-times = better_times
+times = -- plain_times 
+      T.times Nothing
 
+dot_product :: (MonadSAT m) 
+             => [ Number ] -> [ Number ] -> m Number
+dot_product = T.dot_product Nothing
+
 plain_times :: (MonadSAT m) => Number -> Number -> m Number
 plain_times a b | [] <- bits a = return a
 plain_times a b | [] <- bits b = return b
@@ -71,32 +77,3 @@
     return $ make zs
 
 
-better_times a b = do
-    kzs <- sequence $ do
-          ( i , x ) <- zip [ 0 .. ] $ bits a
-          ( j , y ) <- zip [ 0 .. ] $ bits b
-          return $ do
-                  z <- and [ x, y ]
-                  return ( i+j , [z] ) 
-    zs <- reduce $ M.elems $ M.fromListWith (++) kzs
-    return $ make zs
-
-
-reduce ( ( x:y:z:ps) : qss ) = do
-    ( r, c ) <- full_adder x y z
-    qss' <- plugin c qss
-    reduce $ ( ps ++ [r] ) : qss' 
-reduce ( ( x:y:[]) : qss ) = do
-    ( r, c ) <- half_adder x y 
-    qss' <- plugin c qss
-    reduce $ [r] : qss' 
-reduce ( ( x:[]) : qss ) = do
-    xs <- reduce qss
-    return $ x : xs
-reduce [] = return []
-
-plugin c [] = do
-    assert [ not c ]
-    return []
-plugin c (qs : qss) = 
-    return ((c:qs) : qss)
diff --git a/Satchmo/Binary/Op/Times.hs b/Satchmo/Binary/Op/Times.hs
new file mode 100644
--- /dev/null
+++ b/Satchmo/Binary/Op/Times.hs
@@ -0,0 +1,73 @@
+module Satchmo.Binary.Op.Times where
+
+import Prelude hiding ( and, or, not )
+
+import Satchmo.Boolean
+import qualified Satchmo.Code as C
+import Satchmo.Binary.Data
+import Satchmo.Binary.Op.Common
+
+import qualified Data.Map as M
+import Control.Monad ( forM )
+
+
+dot_product :: (MonadSAT m) 
+             => ( Maybe Int) 
+            -> [ Number ] -> [ Number ] -> m Number
+dot_product bound xs ys = do
+    cs <- forM ( zip xs ys ) $ \ (x,y) -> product_components bound x y
+    export bound $ concat cs
+
+times :: (MonadSAT m) 
+             => Maybe Int
+             -> Number -> Number -> m Number
+times bound a b = do
+    kzs <- product_components bound a b
+    export bound kzs
+
+product_components :: MonadSAT m
+    => Maybe Int
+    -> Number -> Number -> m [ (Int, [Boolean]) ]
+product_components bound a b = sequence $ do
+    ( i , x ) <- zip [ 0 .. ] $ bits a
+    ( j , y ) <- zip [ 0 .. ] $ bits b        
+    return $ do
+        z <- and [ x, y ]
+        if ( case bound of Nothing -> False ; Just b -> i+j >= b )
+             then do assert [ not z ] ; return ( i+j , [ ] )
+             else do                    return ( i+j , [z] ) 
+
+export :: MonadSAT m => Maybe Int -> [(Int,[Boolean])] -> m Number
+export bound kzs = do 
+    m <- reduce bound $ M.fromListWith (++) kzs
+    case M.maxViewWithKey m of
+        Nothing -> return $ make []
+        Just ((k,_) , _) -> do 
+              return $ make $ do 
+                    i <- [ 0 .. k ] 
+                    let { [ b ] = m M.! i }  
+                    return b
+
+reduce bound m = case M.minViewWithKey m of
+    Nothing -> return M.empty
+    Just ((k, bs), rest ) -> 
+        if ( case bound of Nothing -> False ; Just b -> k >= b )
+        then do
+            forM bs $ \ b -> assert [ not b ]
+            reduce bound rest
+        else case bs of
+            [] -> reduce bound rest
+            [x] -> do
+                m' <- reduce bound rest
+                return $ M.unionWith (error "huh") m' 
+                       $ M.fromList [(k,[x])] 
+            [x,y] -> do
+                (r,c) <- half_adder x y
+                reduce bound $ M.unionWith (++) rest
+                       $ M.fromList [ (k,[r]), (k+1, [c]) ] 
+            (x:y:z:more) -> do
+                (r,c) <- full_adder x y z
+                reduce bound $ M.unionWith (++) rest
+                       $ M.fromList [ (k, more ++ [r]), (k+1, [c]) ] 
+
+
diff --git a/Satchmo/BinaryTwosComplement.hs b/Satchmo/BinaryTwosComplement.hs
new file mode 100644
--- /dev/null
+++ b/Satchmo/BinaryTwosComplement.hs
@@ -0,0 +1,7 @@
+module Satchmo.BinaryTwosComplement
+
+( module Satchmo.BinaryTwosComplement.Op.Fixed )
+
+where
+
+import Satchmo.BinaryTwosComplement.Op.Fixed 
diff --git a/Satchmo/BinaryTwosComplement/Data.hs b/Satchmo/BinaryTwosComplement/Data.hs
new file mode 100644
--- /dev/null
+++ b/Satchmo/BinaryTwosComplement/Data.hs
@@ -0,0 +1,98 @@
+{-# language MultiParamTypeClasses, FlexibleInstances, FlexibleContexts, UndecidableInstances #-}
+
+module Satchmo.BinaryTwosComplement.Data
+    ( Number, bits, fromBooleans, number, toUnsigned, fromUnsigned
+    , width, isNull, msb, constant, constantWidth)
+
+where
+
+import Control.Applicative ((<$>))
+import Satchmo.MonadSAT (MonadSAT)
+import Satchmo.Boolean (Boolean)
+import qualified Satchmo.Boolean as Boolean
+import qualified Satchmo.Code as C
+import qualified Satchmo.Binary.Data as B 
+
+import Debug.Trace
+
+data Number = Number 
+            { bits :: [Boolean] -- LSB first
+            }
+
+
+instance C.Decode m Boolean Bool => C.Decode m Number Integer where
+    decode n = do bs <- C.decode $ bits n ; return $ fromBinary bs
+
+-- | Make a number from its binary representation
+fromBooleans :: [Boolean] -> Number
+fromBooleans xs = Number xs
+
+
+-- | Convert to unsigned number (see "Satchmo.Binary.Op.Flexible")
+toUnsigned :: Number -> B.Number
+toUnsigned = B.make . bits
+
+-- | Convert from unsigned number (see "Satchmo.Binary.Op.Flexible").
+-- The result is interpreted as a positive or negative number,
+-- depending on its most significant bit.
+fromUnsigned :: B.Number -> Number
+fromUnsigned = fromBooleans . B.bits
+
+-- | Get bit width
+width :: Number -> Int
+width = length . bits
+
+-- | Most significant bit
+msb :: Number -> Boolean
+msb n = if isNull n then error "Satchmo.BinaryTwosComplement.Data.msb"
+        else bits n !! (width n - 1)
+
+-- | @isNull n == True@ if @width n == 0@
+isNull :: Number -> Bool
+isNull n = width n == 0
+
+-- | Get a number variable of given bit width
+number :: MonadSAT m => Int -> m Number
+number width = do
+  xs <- sequence $ replicate width Boolean.boolean
+  return $ fromBooleans xs
+
+fromBinary :: [Bool] -> Integer
+fromBinary xs =
+    let w = length xs
+        (bs, [msb]) = splitAt (w - 1) xs
+    in                    
+      if msb then -(2^(w-1)) + (B.fromBinary bs)
+      else B.fromBinary bs
+
+toBinary :: Maybe Int -- ^ Minimal bit width
+         -> Integer -> [Bool]
+toBinary width i = 
+    let i' = abs i
+        binary = maybe (B.toBinary i') (B.toBinaryWidth `flip` i') width
+        flipBits (firstOne,result) x =
+            if firstOne then (True, result ++ [not x]) 
+            else (x, result ++ [x])
+    in
+      if i == 0 then
+          replicate (maybe 1 id width) False
+      else if i < 0 then 
+               let flipped = snd $ foldl flipBits (False,[]) binary
+               in
+                 if last flipped == False then flipped ++ [True]
+                 else flipped
+           else 
+               if i > 0 && last binary == True then binary ++ [False]
+               else binary
+
+-- | Get a number constant
+constant :: MonadSAT m => Integer -> m Number
+constant i = do
+  bs <- mapM Boolean.constant $ toBinary Nothing i
+  return $ fromBooleans bs
+    
+-- | @constantWidth w@ declares a number constant using at least @w@ bits
+constantWidth :: MonadSAT m => Int -> Integer -> m Number
+constantWidth width i = do
+  bs <- mapM Boolean.constant $ toBinary (Just width) i
+  return $ fromBooleans bs
diff --git a/Satchmo/BinaryTwosComplement/Numeric.hs b/Satchmo/BinaryTwosComplement/Numeric.hs
new file mode 100644
--- /dev/null
+++ b/Satchmo/BinaryTwosComplement/Numeric.hs
@@ -0,0 +1,17 @@
+module Satchmo.BinaryTwosComplement.Numeric where
+
+import qualified Satchmo.BinaryTwosComplement.Op.Fixed as F
+import qualified Satchmo.Numeric as N
+
+instance N.Constant F.Number where
+    constant = F.constantWidth 1  
+    
+instance N.Create F.Number where    
+    create = F.number
+
+instance N.Numeric F.Number where
+    equal = F.equals
+    greater_equal = F.ge
+    plus = F.add
+    minus = F.subtract
+    times = F.times 
diff --git a/Satchmo/BinaryTwosComplement/Op/Common.hs b/Satchmo/BinaryTwosComplement/Op/Common.hs
new file mode 100644
--- /dev/null
+++ b/Satchmo/BinaryTwosComplement/Op/Common.hs
@@ -0,0 +1,38 @@
+module Satchmo.BinaryTwosComplement.Op.Common
+    (equals, eq, lt, le, ge, gt, positive, negative, nonNegative)
+where
+
+import Prelude hiding (and,or,not)
+import Satchmo.MonadSAT (MonadSAT)
+import Satchmo.BinaryTwosComplement.Data (Number,toUnsigned,msb,bits)
+import Satchmo.Boolean (Boolean,and,or,not,ifThenElseM)
+import qualified Satchmo.Boolean as Boolean
+import qualified Satchmo.Binary.Op.Common as B
+
+sameSign, negativePositive :: MonadSAT m => Number -> Number -> m Boolean
+sameSign a b = Boolean.equals [msb a, msb b]
+negativePositive a b = and [msb a, not $ msb b]
+
+equals,eq,lt,le,ge,gt :: MonadSAT m => Number -> Number -> m Boolean
+equals a b = B.equals (toUnsigned a) (toUnsigned b)
+eq = equals
+
+lt a b = ifThenElseM ( sameSign a b )
+                     ( B.lt (toUnsigned a) (toUnsigned b) )
+                     ( negativePositive a b )
+
+le a b = ifThenElseM ( sameSign a b )
+                     ( B.le (toUnsigned a) (toUnsigned b) )
+                     ( negativePositive a b )
+
+ge = flip le
+gt = flip lt
+
+positive,negative,nonNegative :: MonadSAT m => Number -> m Boolean
+positive a = do
+  one <- or $ bits a
+  and [not $ msb a, one]
+
+negative = return . msb
+
+nonNegative = return . not . msb
diff --git a/Satchmo/BinaryTwosComplement/Op/Fixed.hs b/Satchmo/BinaryTwosComplement/Op/Fixed.hs
new file mode 100644
--- /dev/null
+++ b/Satchmo/BinaryTwosComplement/Op/Fixed.hs
@@ -0,0 +1,94 @@
+{-# language MultiParamTypeClasses #-}
+
+-- | Operations with fixed bit width.
+-- Still they are non-overflowing:
+-- if overflow occurs, the constraints are not satisfiable.
+-- The bit width of the result of binary operations
+-- is the max of the bit width of the inputs.
+
+module Satchmo.BinaryTwosComplement.Op.Fixed
+    ( add, subtract, times, increment, negate, linear
+    , module Satchmo.BinaryTwosComplement.Data
+    , module Satchmo.BinaryTwosComplement.Op.Common
+    )
+where
+
+import Prelude hiding (not,negate, subtract)
+import Control.Applicative ((<$>))
+import Satchmo.MonadSAT (MonadSAT)
+import Satchmo.BinaryTwosComplement.Op.Common
+import Satchmo.BinaryTwosComplement.Data
+import qualified Satchmo.Binary.Op.Common as C
+import qualified Satchmo.Binary.Op.Flexible as F
+import Satchmo.Binary.Op.Fixed (restrictedTimes)
+import Satchmo.Boolean (Boolean,monadic,assertOr,equals2,implies,not)
+import qualified Satchmo.Boolean as Boolean
+
+-- | Sign extension
+extendMsb :: Int -> Number -> Number
+extendMsb i n = fromBooleans $ bits n ++ (replicate i $ msb n)
+
+add :: (MonadSAT m) => Number -> Number -> m Number
+add a b = do
+  let maxWidth  = max (width a) (width b)
+      widthDiff = abs $ (width a) - (width b)
+      extend x = if width x == maxWidth then extendMsb 1 x
+                 else extendMsb (widthDiff + 1) x
+      a' = extend a
+      b' = extend b
+
+  flexibleResult <- fromUnsigned <$> F.add (toUnsigned a') (toUnsigned b')
+  let (low, high) = splitAt maxWidth $ bits flexibleResult
+
+  e <- Boolean.equals [last low, head high]
+  assertOr [ e ]
+  return $ fromBooleans low
+
+times :: MonadSAT m => Number -> Number -> m Number
+times a b = do
+  let a' = extendMsb (width b) a
+      b' = extendMsb (width a) b
+      unsignedResultWidth = (width a) + (width b)
+      resultWidth = max (width a) (width b)
+
+  unsignedResult <- fromUnsigned <$> 
+                    restrictedTimes (toUnsigned a') (toUnsigned b')
+  let (low, high) = splitAt resultWidth $ bits unsignedResult
+  allHighOne  <- Boolean.and $ high
+  allHighZero <- Boolean.and $ map not high
+  assertOr [allHighOne, allHighZero]
+
+  e <- Boolean.equals [ last low, head high ]
+  assertOr [e]
+  return $ fromBooleans low
+
+increment :: MonadSAT m => Number -> m Number
+increment n =
+    let inc [] z = return ( [], z )
+        inc (y:ys) z = do
+          ( r, c ) <- C.half_adder y z
+          ( rAll, cAll ) <- inc ys c
+          return ( r : rAll, cAll )
+    in do
+      add1 <- Boolean.constant True
+      (n', _) <- inc (bits n) add1
+      e <- (not $ msb n) `implies` (not $ last n')
+      assertOr [ e ]
+      return $ fromBooleans n'
+
+subtract :: MonadSAT m => Number -> Number -> m Number
+subtract a b = do
+    b' <- negate b
+    add a b'
+
+negate :: MonadSAT m => Number -> m Number
+negate n =
+    let invN = fromBooleans $ map not $ bits n
+    in do
+      n' <- increment invN
+      e <- (msb n) `implies` (not $ msb n')
+      assertOr [ e ]
+      return n'
+      
+linear :: MonadSAT m => Number -> Number -> Number -> m Number
+linear m x n = m `times` x >>= add n
diff --git a/Satchmo/Boolean/Data.hs b/Satchmo/Boolean/Data.hs
--- a/Satchmo/Boolean/Data.hs
+++ b/Satchmo/Boolean/Data.hs
@@ -1,11 +1,17 @@
 {-# language MultiParamTypeClasses #-}
+{-# language TypeSynonymInstances #-}
+{-# language FlexibleInstances #-}
+{-# language NoMonomorphismRestriction #-}
 
 module Satchmo.Boolean.Data
 
-( Boolean(Constant), Booleans, encode
+( Boolean(..), Booleans, encode
 , boolean, exists, forall
 , constant
-, not, assert, assertW, monadic
+, not, monadic
+, assertOr -- , assertOrW
+, assertAnd -- , assertAndW
+, assert -- for legacy code
 )
 
 where
@@ -18,20 +24,18 @@
 import Satchmo.Data
 import Satchmo.MonadSAT
 
-import Satchmo.SAT (SAT) -- for specializations
 
+
 import Data.Array
 import Data.Maybe ( fromJust )
 import Data.List ( partition )
 
 import Control.Monad.Reader
 
-data Boolean = Boolean
-             { encode :: ! Literal
-             -- , decode :: ! ( C.Decoder Bool )
-             }
+data Boolean = Boolean { encode :: Literal }
      | Constant { value :: ! Bool }
 
+
 {-
 
 -- FIXME: @Pepe: what is the reason for these instances?
@@ -64,21 +68,11 @@
 isConstant ( Constant {} ) = True
 isConstant _ = False
 
-instance C.Decode Boolean Bool where 
-    decode b = case b of
-        -- Boolean {} -> decode b
-        Boolean {} -> asks $ \ arr -> 
-              let x = encode b
-              in  positive x == arr ! ( variable x )
-        Constant {} -> return $ value b
 
-boolean :: MonadSAT m => m Boolean
+boolean :: MonadSAT m => m ( Boolean )
 boolean = exists
-{-# INLINABLE boolean #-}
-{-# specialize inline boolean :: SAT Boolean #-}
 
-exists :: MonadSAT m => m Boolean
-{-# specialize inline exists :: SAT Boolean #-}
+exists :: MonadSAT m => m ( Boolean )
 exists = do
     x <- fresh
     return $ Boolean 
@@ -91,8 +85,7 @@
 -}
            }
 
-forall :: MonadSAT m => m Boolean
-{-# specialize inline forall :: SAT Boolean #-}
+forall :: MonadSAT m => m ( Boolean )
 forall = do
     x <- fresh_forall
     return $ Boolean 
@@ -100,13 +93,12 @@
 --           , decode = error "Boolean.forall cannot be decoded"
            }
 
-constant :: MonadSAT m => Bool -> m Boolean
-{-# specialize inline constant :: Bool -> SAT Boolean #-}
+constant :: MonadSAT m => Bool -> m (Boolean)
 constant v = do
     return $ Constant { value = v } 
 {-# INLINABLE constant #-}
 
-not :: Boolean -> Boolean
+-- not :: Boolean -> Boolean
 not b = case b of
     Boolean {} -> Boolean 
       { encode = nicht $ encode b
@@ -115,26 +107,35 @@
     Constant {} -> Constant { value = Prelude.not $ value b }
 {-# INLINABLE not #-}
 
+-- assertOr, assertAnd :: MonadSAT m => [ Boolean (Literal m ) ] -> m ()
+assertOr = assert
 
 assert :: MonadSAT m => [ Boolean ] -> m ()
-{-# specialize inline assert :: [ Boolean ] -> SAT () #-}
 assert bs = do
     let ( con, uncon ) = partition isConstant bs
     let cval = Prelude.or $ map value con
     when ( Prelude.not cval ) $ emit $ clause $ map encode uncon
 {-# INLINABLE assert #-}
 
-assertW :: MonadSAT m => Weight -> [ Boolean ] -> m ()
-assertW w bs = do
+-- assertAnd :: MonadSAT m => [ Boolean ] -> m ()
+assertAnd bs = forM_ bs $ assertOr . return
+
+{-
+
+assertOrW, assertAndW :: MonadSAT m => Weight -> [ Boolean ] -> m ()
+assertOrW w bs = do
     let ( con, uncon ) = partition isConstant bs
     let cval = Prelude.or $ map value con
     when ( Prelude.not cval ) $ emitW w $ clause $ map encode uncon
 
+assertAndW w bs = forM_ bs $ assertOrW w . return
+
+-}
+
 monadic :: Monad m
         => ( [ a ] -> m b )
         -> ( [ m a ] -> m b )
-{-# specialize inline monadic :: ([a] -> SAT b) -> [SAT a] -> SAT b #-}        
 monadic f ms = do
     xs <- sequence ms
     f xs
-{-# INLINABLE monadic #-}
+
diff --git a/Satchmo/Boolean/Op.hs b/Satchmo/Boolean/Op.hs
--- a/Satchmo/Boolean/Op.hs
+++ b/Satchmo/Boolean/Op.hs
@@ -1,8 +1,10 @@
 module Satchmo.Boolean.Op
 
 ( constant
-, and, or, xor
+, and, or, xor, equals2, equals, implies
 , fun2, fun3
+, ifThenElse, ifThenElseM
+, assert_fun2, assert_fun3
 , monadic
 )
 
@@ -10,29 +12,28 @@
 
 import Prelude hiding ( and, or, not )
 import qualified Prelude
-
+import Control.Applicative ((<$>))
 import Satchmo.MonadSAT
 import Satchmo.Code
 import Satchmo.Boolean.Data
 
-import Satchmo.SAT ( SAT) -- for specializations
+-- import Satchmo.SAT ( SAT) -- for specializations
 
-import Control.Monad ( foldM )
+import Control.Monad ( foldM, when )
 
 and :: MonadSAT m => [ Boolean ] -> m Boolean
-{-# specialize inline and :: [ Boolean ] -> SAT Boolean #-}
+
 and [] = constant True
 and [x]= return x
 and xs = do
     y <- boolean
     sequence_ $ do
         x <- xs
-        return $ assert [ not y, x ]
-    assert $ y : map not xs
+        return $ assertOr [ not y, x ]
+    assertOr $ y : map not xs
     return y
 
 or :: MonadSAT m => [ Boolean ] -> m Boolean
-{-# specialize inline or :: [ Boolean ] -> SAT Boolean #-}
 or [] = constant False
 or [x]= return x
 or xs = do
@@ -40,35 +41,66 @@
     return $ not y
 
 xor :: MonadSAT m => [ Boolean ] -> m Boolean
-{-# specialize inline xor :: [ Boolean ] -> SAT Boolean #-}
 xor [] = constant False
 xor (x:xs) = foldM xor2 x xs
 
+equals :: MonadSAT m => [ Boolean ] -> m Boolean
+equals [] = constant True
+equals [x] = constant True
+equals (x:xs) = foldM equals2 x xs
 
+equals2 :: MonadSAT m => Boolean -> Boolean -> m Boolean
+equals2 a b = not <$> xor2 a b
+
+implies :: MonadSAT m => Boolean -> Boolean -> m Boolean
+implies a b = or [not a, b]
+
+ifThenElse :: MonadSAT m => Boolean -> m Boolean -> m Boolean -> m Boolean
+ifThenElse condition ifTrue ifFalse = do
+  trueBranch <- ifTrue
+  falseBranch <- ifFalse
+  monadic and [ condition `implies` trueBranch
+              , not condition `implies` falseBranch ]
+
+ifThenElseM :: MonadSAT m => m Boolean -> m Boolean -> m Boolean -> m Boolean
+ifThenElseM conditionM ifTrue ifFalse = do
+  c <- conditionM
+  ifThenElse c ifTrue ifFalse
+
 -- | implement the function by giving a full CNF
 -- that determines the outcome
 fun2 :: MonadSAT m => 
         ( Bool -> Bool -> Bool )
      -> Boolean -> Boolean 
      -> m Boolean
-{-# specialize inline fun2 :: (Bool -> Bool -> Bool) -> Boolean -> Boolean -> SAT Boolean #-}
 fun2 f x y = do
     r <- boolean
     sequence_ $ do
         a <- [ False, True ]
         b <- [ False, True ]
         let pack flag var = if flag then not var else var
-        return $ assert 
+        return $ assertOr
             [ pack a x, pack b y, pack (Prelude.not $ f a b) r ]
     return r
 
+assert_fun2 :: MonadSAT m => 
+        ( Bool -> Bool -> Bool )
+     -> Boolean -> Boolean 
+     -> m ()
+assert_fun2 f x y = sequence_ $ do
+        a <- [ False, True ]
+        b <- [ False, True ]
+        let pack flag var = if flag then not var else var
+        return $ when ( Prelude.not $ f a b ) $ assert 
+            [ pack a x, pack b y ]
+     
+
 -- | implement the function by giving a full CNF
 -- that determines the outcome
 fun3 :: MonadSAT m => 
         ( Bool -> Bool -> Bool -> Bool )
      -> Boolean -> Boolean -> Boolean
      -> m Boolean
-{-# specialize inline fun3 :: (Bool -> Bool -> Bool -> Bool) -> Boolean -> Boolean -> Boolean -> SAT Boolean #-}
 fun3 f x y z = do
     r <- boolean
     sequence_ $ do
@@ -76,14 +108,26 @@
         b <- [ False, True ]
         c <- [ False, True ]
         let pack flag var = if flag then not var else var
-        return $ assert 
+        return $ assertOr
             [ pack a x, pack b y, pack c z
             , pack (Prelude.not $ f a b c) r 
             ]
     return r
 
+assert_fun3 :: MonadSAT m => 
+        ( Bool -> Bool -> Bool -> Bool )
+     -> Boolean -> Boolean -> Boolean
+     -> m ()
+assert_fun3 f x y z = sequence_ $ do
+        a <- [ False, True ]
+        b <- [ False, True ]
+        c <- [ False, True ]
+        let pack flag var = if flag then not var else var
+        return $ when ( Prelude.not $ f a b c ) $ assert 
+            [ pack a x, pack b y, pack c z ]
+     
+
 xor2 :: MonadSAT m => Boolean -> Boolean -> m Boolean
-{-# specialize inline  xor2 :: Boolean -> Boolean -> SAT Boolean #-}
 xor2 = fun2 (/=)
 -- xor2 = xor2_orig
 
@@ -93,5 +137,4 @@
     a <- and [ x, not y ]
     b <- and [ not x, y ]
     or [ a, b ]
-
 
diff --git a/Satchmo/Code.hs b/Satchmo/Code.hs
--- a/Satchmo/Code.hs
+++ b/Satchmo/Code.hs
@@ -1,9 +1,10 @@
-{-# language MultiParamTypeClasses, FunctionalDependencies, UndecidableInstances #-}
+{-# language MultiParamTypeClasses, FunctionalDependencies #-}
+{-# language FlexibleInstances, UndecidableInstances, FlexibleContexts #-}
 
 module Satchmo.Code 
 
 ( Decode (..)
-, Decoder
+-- , Decoder
 )
 
 where
@@ -13,29 +14,28 @@
 import Data.Array
 
 import Control.Monad.Reader
-
+import qualified Data.Map as M
 
-class Decode c a where 
-    {-# INLINABLE decode #-}
-    decode :: c -> Decoder a
+class Monad m => Decode m c a where 
+    decode :: c -> m a
 
 -- type Decoder a = Reader ( Map Variable Bool ) a
-type Decoder a = Reader ( Array Variable Bool ) a
+-- type Decoder a = Reader ( Array Variable Bool ) a
 
-instance Decode () () where
+instance Monad m => Decode m () () where
     decode () = return ()
 
-instance ( Decode c a, Decode d b ) => Decode ( c,d) (a,b) where
+instance (  Decode m c a, Decode m d b ) => Decode m ( c,d) (a,b) where
     decode (c,d) = do a <- decode c; b <- decode d; return ( a,b)
 
-instance ( Decode c a ) => Decode [c] [a] where
+instance (  Decode m c a ) => Decode m [c] [a] where
     decode = mapM decode 
 
-instance Decode a b => Decode ( Maybe a ) ( Maybe b ) where
-    decode ( Just b ) = fmap Just $ decode b
+instance Decode m a b => Decode m ( Maybe a ) ( Maybe b ) where
+    decode ( Just b ) = do a <- decode b ; return $ Just a
     decode Nothing = return $ Nothing
 
-instance (Ix i, Decode c a) => Decode ( Array i c) ( Array i a ) where
+instance (Ix i, Decode m c a) => Decode m ( Array i c) ( Array i a ) where
     decode x = do
         pairs <- sequence $ do
             (i,e) <- assocs x
@@ -43,3 +43,12 @@
                 f <- decode e
                 return (i,f)
         return $ array (bounds x) pairs
+
+instance (Ord i, Decode m c a) => Decode m ( M.Map i c) ( M.Map i a ) where
+    decode x = do
+        pairs <- sequence $ do
+            (i,e) <- M.assocs x
+            return $ do
+                f <- decode e
+                return (i,f)
+        return $ M.fromList pairs
diff --git a/Satchmo/Counting.hs b/Satchmo/Counting.hs
--- a/Satchmo/Counting.hs
+++ b/Satchmo/Counting.hs
@@ -11,24 +11,14 @@
 
 import Satchmo.Boolean
 
-atleast_block :: MonadSAT m => Int -> [ Boolean ] -> m [ Boolean ]
-atleast_block k [] = do
-    t <- constant True
-    f <- constant False
-    return $ t : replicate k f
-atleast_block k (x:xs) = do
-    cs <- atleast_block k xs
-    sequence $ do
-        i <- [ 0 .. k ]
-        return $ if i == 0 then return $ cs !! 0
-                 else do
-                     p <- and [ x, cs !! (i-1) ]
-                     or [ cs !! i, p ]
+import Satchmo.SAT ( SAT) -- for specializations
 
+{-# specialize inline atleast :: Int -> [ Boolean] -> SAT Boolean #-}
+{-# specialize inline atmost  :: Int -> [ Boolean] -> SAT Boolean #-}
+{-# specialize inline exactly :: Int -> [ Boolean] -> SAT Boolean #-}
+
 atleast :: MonadSAT m => Int -> [ Boolean ] -> m Boolean
-atleast k xs = do
-    cs <- atleast_block k xs
-    return $ cs !! k
+atleast k xs = fmap not $ atmost (k-1) xs
         
 
 atmost_block :: MonadSAT m => Int -> [ Boolean ] -> m [ Boolean ]
@@ -37,13 +27,11 @@
     return $ replicate (k+1) t
 atmost_block k (x:xs) = do
     cs <- atmost_block k xs
+    f <- constant False
     sequence $ do
-        i <- [ 0 .. k ]
+        (p,q) <- zip cs ( f : cs )
         return $ do
-            f <- constant False
-            p <- and [ x, if i > 0 then cs !! (i-1) else f ]
-            q <- and [ not x, cs !! i ]
-            or [ p, q ]
+            fun3  ( \ x p q -> if x then q else p ) x p q
 
 atmost :: MonadSAT m => Int -> [ Boolean ] -> m Boolean
 atmost k xs = do
@@ -57,14 +45,12 @@
     f <- constant False
     return $ t : replicate k f
 exactly_block k (x:xs) = do
+    f <- constant False
     cs <- exactly_block k xs
     sequence $ do
-        i <- [ 0 .. k ]
+        (p,q) <- zip cs ( f : cs )
         return $ do
-            f <- constant False
-            p <- and [ x, if i > 0 then cs !! (i-1) else f ]
-            q <- and [ not x, cs !! i ]
-            or [ p, q ]
+            fun3 ( \ x p q -> if x then q else p ) x p q
 
 exactly :: MonadSAT m => Int -> [ Boolean ] -> m Boolean
 exactly k xs = do
diff --git a/Satchmo/Data.hs b/Satchmo/Data.hs
--- a/Satchmo/Data.hs
+++ b/Satchmo/Data.hs
@@ -1,62 +1,46 @@
+{-# language TypeFamilies #-}
+
 module Satchmo.Data 
 
 ( CNF, cnf, clauses
 -- FIXME: exports should be abstract
 , Clause(..), clause, literals
-, Literal(..), literal, nicht
-, Variable, variable, positive
+, Literal (..), literal, nicht, positive, variable
+, Variable 
 )
 
 where
 
 import Control.Monad.State.Strict
 
-newtype CNF     = CNF { clauses :: [ Clause  ] }
+type Variable = Int
 
-instance Show CNF where
-    show ( CNF cs ) = unlines $ map show cs
+data Literal = Literal { variable :: Variable , positive :: Bool }
 
-cnf :: [ Clause ] -> CNF
-cnf cs = CNF cs
+instance Show Literal where
+    show l = ( if positive l then "" else "-" ) ++ show ( variable l )
 
+literal :: Bool -> Variable -> Literal
+literal pos v  = Literal { positive = pos, variable = v }
 
-newtype Clause  = Clause { literals :: [ Literal ] }
+nicht :: Literal -> Literal 
+nicht x = x { positive = not $ positive x }
 
-instance Show Clause where
-    show ( Clause xs ) = unwords ( map show xs ++ [ "0" ] )
+newtype CNF     = CNF { clauses :: [ Clause ] }
 
-clause :: [ Literal ] -> Clause
-clause ls = Clause { literals = ls }
+instance Show ( CNF  ) where
+    show ( CNF cs ) = unlines $ map show cs
 
+cnf :: [ Clause ] -> CNF 
+cnf cs = CNF cs
 
-newtype Literal = Literal Int
-    deriving ( Eq, Ord )
 
-instance Show Literal where 
-    show ( Literal i ) = show i
+newtype Clause = Clause { literals :: [ Literal ] }
 
-instance Read Literal where
-    readsPrec p = \ cs -> do
-        ( i, cs') <- readsPrec p cs
-        return ( Literal i , cs' )
+instance Show ( Clause ) where
+    show ( Clause xs ) = unwords ( map show xs ++ [ "0" ] )
 
-literal :: Bool -> Variable -> Literal
-literal p v | v /= 0 = 
-    Literal $ if p then v else negate v
-{-# INLINE literal #-}
+clause ::  [ Literal ] -> Clause 
+clause ls = Clause { literals = ls }
 
-nicht :: Literal -> Literal
-nicht ( Literal i ) = Literal $ negate i
-{-# INLINE nicht #-}
 
--- FIXME: should be newtype
-type Variable = Int
-
-variable :: Literal -> Variable
-variable ( Literal v ) = abs v
-{-# INLINE variable #-}
-
-positive :: Literal -> Bool
-positive ( Literal v ) = 0 < v
-
-{-# INLINE positive #-}
diff --git a/Satchmo/Integer/Data.hs b/Satchmo/Integer/Data.hs
--- a/Satchmo/Integer/Data.hs
+++ b/Satchmo/Integer/Data.hs
@@ -1,4 +1,4 @@
-{-# language MultiParamTypeClasses #-}
+{-# language MultiParamTypeClasses, FlexibleInstances, FlexibleContexts, UndecidableInstances #-}
 
 module Satchmo.Integer.Data 
 
@@ -21,11 +21,10 @@
 data Number = Number 
             { bits :: [ Boolean ] -- ^ lsb first,
 	         -- using two's complement
-            , decode :: C.Decoder Integer
             }
 
-instance C.Decode Number Integer where
-    decode = decode
+instance C.Decode m Boolean Bool => C.Decode m Number Integer where
+    decode n = do ys <- mapM C.decode (bits n) ; return $ fromBinary ys
 
 width :: Number -> Int
 width n = length $ bits n
@@ -39,7 +38,6 @@
 make :: [ Boolean ] -> Number
 make xs = Number
            { bits = xs
-           , decode = do ys <- mapM C.decode xs ; return $ fromBinary ys
            }
 
 fromBinary :: [ Bool ] -> Integer
diff --git a/Satchmo/Integer/Difference.hs b/Satchmo/Integer/Difference.hs
new file mode 100644
--- /dev/null
+++ b/Satchmo/Integer/Difference.hs
@@ -0,0 +1,58 @@
+{-# language MultiParamTypeClasses, FlexibleContexts, FlexibleInstances #-}
+
+module Satchmo.Integer.Difference where
+
+import Satchmo.Code
+import Satchmo.Numeric 
+
+data Number a = Difference { top :: a, bot :: a }
+
+instance Decode m a Integer 
+         => Decode m ( Number a ) Integer where
+    decode n = do
+        t <- decode $ top n
+        b <- decode $ bot n
+        return $ t - b
+        
+instance Constant a => Constant ( Number a ) where
+    constant n = 
+        if n >= 0 then do
+            t <- constant n
+            b <- constant 0
+            return $ Difference { top = t, bot = b }
+        else do    
+            t <- constant 0
+            b <- constant $ negate n
+            return $ Difference { top = t, bot = b }
+
+instance Create a => Create ( Number a ) where
+    create bits = do
+        t <- create bits
+        b <- create bits
+        return $ Difference { top = t, bot = b }
+
+instance Numeric a => Numeric ( Number a ) where        
+    equal a b = do
+        t <- plus ( top a ) ( bot b )
+        b <- plus ( bot a ) ( top b )
+        equal t b
+    greater_equal a b = do
+        t <- plus ( top a ) ( bot b )
+        b <- plus ( bot a ) ( top b )
+        greater_equal t b      
+    plus a b = do 
+        t <- plus ( top a ) ( top b )
+        b <- plus ( bot a ) ( bot b )
+        return $ Difference { top = t, bot = b }
+    minus a b = do 
+        t <- plus ( top a ) ( bot b )
+        b <- plus ( bot a ) ( top b )
+        return $ Difference { top = t, bot = b }
+    times a b = do 
+        tt <- times ( top a ) ( top b )
+        bb <- times ( bot a ) ( bot b )
+        t  <- plus tt bb
+        tb <- times ( top a ) ( bot b )
+        bt <- times ( bot a ) ( top b )
+        b  <- plus tb bt
+        return $ Difference { top = t, bot = b }
diff --git a/Satchmo/Integer/Op.hs b/Satchmo/Integer/Op.hs
--- a/Satchmo/Integer/Op.hs
+++ b/Satchmo/Integer/Op.hs
@@ -26,7 +26,7 @@
     let ys = map B.not $ bits n 
     o <- B.constant True
     ( zs, c ) <- increment ys o
-    assert [ last $ ys, B.not $ last zs ]
+    assertOr [ last $ ys, B.not $ last zs ]
     return $ make zs
 
 increment [] z = return ( [], z )
@@ -44,7 +44,7 @@
     cin <- B.constant False
     ( zs, cout ) <- 
         F.add_with_carry cin ( bits a ) ( bits b )
-    monadic assert [ fun2 (==) cout $ last zs ]
+    monadic assertOr [ fun2 (==) cout $ last zs ]
     return $ make zs
 
 sub :: MonadSAT m 
@@ -65,7 +65,7 @@
     c <- F.times ( F.make $ bits a ) 
       	 	 ( F.make $ bits b )
     let ( pre, post ) = splitAt ( width a ) $ F.bits c
-    monadic assert [ fun2 (==) ( head post) $ last pre ]
+    monadic assertOr [ fun2 (==) ( head post) $ last pre ]
     return $ make pre
 
 ----------------------------------------------------
diff --git a/Satchmo/MonadSAT.hs b/Satchmo/MonadSAT.hs
--- a/Satchmo/MonadSAT.hs
+++ b/Satchmo/MonadSAT.hs
@@ -1,7 +1,9 @@
 {-# LANGUAGE MultiParamTypeClasses #-}
 {-# LANGUAGE FlexibleContexts, FlexibleInstances #-}
 {-# LANGUAGE GeneralizedNewtypeDeriving #-}
+{-# LANGUAGE TypeFamilies #-}
 
+
 module Satchmo.MonadSAT
 
 ( MonadSAT(..), Weight
@@ -11,11 +13,13 @@
 where
 
 import Satchmo.Data
+import Satchmo.Code
 
 import Control.Monad.Trans (lift)
 import Control.Monad.Cont  (ContT)
 import Control.Monad.List  (ListT)
 import Control.Monad.Reader (ReaderT)
+import Control.Monad.Fix ( MonadFix )
 import qualified Control.Monad.State  as Lazy (StateT)
 import qualified Control.Monad.Writer as Lazy (WriterT)
 import qualified Control.Monad.RWS    as Lazy (RWST)
@@ -26,15 +30,19 @@
 
 type Weight = Int
 
-class (Functor m, Monad m) => MonadSAT m where
-  fresh, fresh_forall :: m Literal
-  {-# INLINABLE fresh #-}
-  emit  :: Clause -> m ()
-  {-# INLINABLE emit #-}
-  emitW :: Weight -> Clause -> m ()
+class (MonadFix m, Functor m, Monad m) => MonadSAT m where
+  fresh, fresh_forall :: m  Literal
+
+  emit  :: Clause  -> m ()
+  -- emitW :: Weight -> Clause (Literal m) -> m ()
+
   -- | emit some note (could be printed by the backend)
   note :: String -> m ()
 
+  type Decoder m :: * -> * 
+  decode_variable :: Variable -> Decoder m Bool
+
+
 type NumClauses = Integer
 type NumVars    = Integer
 
@@ -44,6 +52,8 @@
                      }
      deriving Show
 
+{-
+
 -- -------------------------------------------------------
 -- MonadSAT liftings for standard monad transformers
 -- -------------------------------------------------------
@@ -101,3 +111,5 @@
   fresh_forall = lift fresh_forall
   emit  = lift . emit
   emitW = (lift.) . emitW
+
+-}
diff --git a/Satchmo/Numeric.hs b/Satchmo/Numeric.hs
new file mode 100644
--- /dev/null
+++ b/Satchmo/Numeric.hs
@@ -0,0 +1,21 @@
+{-# language FlexibleContexts #-}
+
+module Satchmo.Numeric where
+
+import Satchmo.Boolean
+import Satchmo.Code
+
+class Constant a where
+    constant :: MonadSAT m => Integer -> m a
+    
+class Create a where    
+    -- | Parameter: bit width
+    create :: MonadSAT m => Int -> m a 
+    
+class Numeric a where
+    equal :: MonadSAT m => a -> a -> m Boolean
+    greater_equal :: MonadSAT m => a -> a -> m Boolean
+    plus :: MonadSAT m => a -> a -> m a
+    minus :: MonadSAT m => a -> a -> m a
+    times :: MonadSAT m => a -> a -> m a
+    
diff --git a/Satchmo/Polynomial.hs b/Satchmo/Polynomial.hs
--- a/Satchmo/Polynomial.hs
+++ b/Satchmo/Polynomial.hs
@@ -1,26 +1,31 @@
 {-# language MultiParamTypeClasses #-}
 {-# language FlexibleContexts      #-}
 {-# language UndecidableInstances  #-}
+{-# language FlexibleInstances #-}
 
 module Satchmo.Polynomial 
 
-( Number ()
-, number, constant
-, iszero, equals, ge, gt
-, add, times
+( Poly (Poly), NumPoly, polynomial, constant, fromCoefficients
+, isNull, null, constantTerm, coefficients
+, equals, ge, gt
+, add, times, subtract, compose, apply, derive
 )
 
 where
 
+import Prelude hiding (subtract,null)
 import Data.Map ( Map )
 import qualified Data.Map as M
+import Control.Applicative ((<$>))
+import Control.Monad (foldM)
 
-import Satchmo.SAT
-import Satchmo.Boolean hiding ( constant )
-import qualified Satchmo.Boolean 
+import Satchmo.MonadSAT (MonadSAT)
+import Satchmo.Boolean (Boolean,monadic)
+import qualified Satchmo.Boolean as B
 import Satchmo.Code
 
-import qualified Satchmo.Binary.Op.Fixed as F
+import qualified Satchmo.BinaryTwosComplement.Op.Fixed as F
+--import qualified Satchmo.Binary.Op.Fixed as F
 
 import Control.Monad ( forM )
 
@@ -28,110 +33,145 @@
 -- coefficients starting from degree zero
 data Poly a = Poly [a] deriving ( Eq, Ord, Show )
 
-type Number = Poly F.Number
+type NumPoly = Poly F.Number
 
--- Hohoho:
-instance Decode a Integer => Decode ( Poly a ) Integer where
-    decode ( Poly xs ) = do
-        ys <- forM xs decode 
-        let base = 1000 -- well
-        return $ if all ( < base ) ys
-                 then foldr ( \ y o -> o * base + y ) 0 ys
-                 else error "Satchmo.Polynomial.decode"
+instance Decode m a Integer => Decode m (Poly a) (Poly Integer) where
+    decode (Poly xs) = do
+      decodedXs <- forM xs decode 
+      return $ Poly decodedXs
 
+fromCoefficients :: MonadSAT m => Int -- ^ Bits
+                 -> [Integer]         -- ^ Coefficients
+                 -> m NumPoly
+fromCoefficients width coefficients = 
+    Poly <$> (forM coefficients $ F.constantWidth width)
+
+polynomial :: MonadSAT m => Int -- ^ Bits
+           -> Int -- ^ Degree
+           -> m NumPoly
+polynomial bits deg = 
+    Poly <$> (forM [ 0 .. deg ] $ \ i -> F.number bits)
+
+constant :: MonadSAT m
+         => Integer
+         -> m NumPoly
+constant 0 = return $ Poly []
+constant const = do
+    c <- F.constant const
+    return $ Poly [c]
+
 -- | this is sort of wrong:
 -- null polynomial should have degree -infty
 -- but this function will return -1
 degree :: Poly a -> Int
 degree ( Poly xs ) = pred $ length xs
 
+isNull :: Poly a -> Bool
+isNull (Poly []) = True
+isNull _         = False
 
-number :: MonadSAT m
-       => Int -- ^ bits
-       -> Int -- ^ degree
-       -> m ( Poly F.Number )
-number bits deg = do 
-    xs <- forM [ 0 .. deg ] $ \ i -> F.number bits
-    return $ Poly xs
+null :: Poly a
+null = Poly []
 
-constant :: MonadSAT m
-         => Integer
-         -> m ( Poly F.Number )
-constant 0 = return $ Poly []
-constant c = do
-    z <- F.constant 0
-    o <- F.constant c
-    return $ Poly [ z, o ]
+constantTerm :: Poly a -> a
+constantTerm (Poly (c:_)) = c
 
-iszero  ( Poly xs ) = do
-    ns <- forM xs $ F.iszero
-    Satchmo.Boolean.and ns
+coefficients :: Poly a -> [a]
+coefficients (Poly cs) = cs
 
-equals ( Poly xs ) ( Poly ys ) = do
-          z <- F.constant 0
-          let n = max ( length xs ) ( length ys )
-              fill xs = take n $ xs ++ repeat z
-          let handle xs ys = case ( xs, ys ) of
-                  ( [], [] ) -> Satchmo.Boolean.constant True
-                  (x:xs, y:ys) -> do
-                      e <- F.equals x y
-                      later <- handle xs ys
-                      Satchmo.Boolean.and [ e, later ]
-          handle ( reverse $ fill xs ) ( reverse $ fill ys )
+fill :: MonadSAT m => NumPoly -> NumPoly -> m ([F.Number],[F.Number])
+fill (Poly p1) (Poly p2) = do
+  zero <- F.constant 0
+  let maxL = max (length p1) (length p2)
+      fill' xs = take maxL $ xs ++ repeat zero
+  return (fill' p1, fill' p2)
 
-ge ( Poly xs ) ( Poly ys ) = do
-          z <- F.constant 0
-          let n = max ( length xs ) ( length ys )
-              fill xs = take n $ xs ++ repeat z
-          let handle xs ys = case ( xs, ys ) of
-                  ( [], [] ) -> Satchmo.Boolean.constant True
-                  (x:xs, y:ys) -> do
-                      gt <- F.gt x y
-                      e <- F.equals x y
-                      later <- handle xs ys
-                      monadic Satchmo.Boolean.or 
-                              [ return gt
-                              , Satchmo.Boolean.and [ e, later ]
-                              ]
-          handle ( reverse $ fill xs ) ( reverse $ fill ys )
+reverseBoth :: ([a],[b]) -> ([a], [b])
+reverseBoth (p1, p2) = (reverse p1, reverse p2)
 
-gt  ( Poly xs ) ( Poly ys ) = do
-          z <- F.constant 0
-          let n = max ( length xs ) ( length ys )
-              fill xs = take n $ xs ++ repeat z
-          let handle xs ys = case ( xs, ys ) of
-                  ( [], [] ) -> Satchmo.Boolean.constant False
-                  (x:xs, y:ys) -> do
-                      gt <- F.gt x y
-                      e <- F.equals x y
-                      later <- handle xs ys
-                      monadic Satchmo.Boolean.or 
-                              [ return gt
-                              , Satchmo.Boolean.and [ e, later ]
-                              ]
-          handle ( reverse $ fill xs ) ( reverse $ fill ys )
+binaryOp :: ([a] -> b) -> ([a] -> [a] -> b) -> [a] -> [a] -> b
+binaryOp unary binary p1 p2 =
+    case (p1,p2) of
+      ([],ys) -> unary ys
+      (xs,[]) -> unary xs
+      (xs,ys) -> binary xs ys
 
+equals,  ge,  gt  :: MonadSAT m => NumPoly -> NumPoly -> m Boolean
+equals', ge', gt' :: MonadSAT m => [F.Number] -> [F.Number] -> m Boolean
 
-add ( Poly xs ) ( Poly ys ) = do
-          let handle xs ys = case ( xs, ys ) of
-                  ( [] , ys ) ->  return ys
-                  ( xs, [] ) -> return xs
-                  (x:xs, y:ys) -> do
-                      z <- F.add x y
-                      zs <- handle xs ys
-                      return $ z : zs
-          zs <- handle xs ys
-          return $ Poly zs
+equals p1 p2 = fill p1 p2 >>= uncurry equals'
 
-times p q = do
-          let handle ( Poly xs ) ( Poly ys ) = 
-                  case ( xs, ys ) of
-                      ( [], ys ) -> return $ Poly []
-                      ( xs, [] ) -> return $ Poly []
-                      ( x : xs, ys ) -> do
-                          Poly zs <- handle ( Poly xs ) ( Poly ys )
-                          f : fs  <- forM ys $ F.times x
-                          Poly rest <- add ( Poly zs ) ( Poly fs )
-                          return $ Poly $ f : rest
-          handle p q
+equals' = binaryOp (\_ -> B.constant True)
+          (\(x:xs) (y:ys) -> do e <- F.equals x y
+                                rest <- equals' xs ys
+                                B.and [e,rest]
+          )
 
+ge p1 p2 = fill p1 p2 >>= uncurry ge' . reverseBoth
+
+ge' = binaryOp (\_ -> B.constant True)
+      (\(x:xs) (y:ys) -> do gt <- F.gt x y
+                            eq <- F.equals x y
+                            rest <- ge' xs ys
+                            monadic B.or [ return gt
+                                         , B.and [ eq, rest ]]
+      )
+
+gt p1 p2 = fill p1 p2 >>= uncurry gt' . reverseBoth
+
+gt' = binaryOp (\_ -> B.constant False)
+      (\(x:xs) (y:ys) -> do gt <- F.gt x y
+                            eq <- F.equals x y
+                            rest <- gt' xs ys
+                            monadic B.or [ return gt
+                                         , B.and [ eq, rest ]]
+      )
+
+add,  times, subtract, compose :: MonadSAT m => NumPoly -> NumPoly -> m NumPoly
+add', times' :: MonadSAT m => [F.Number] -> [F.Number] -> m [F.Number]
+
+add (Poly p1) (Poly p2) = Poly <$> add' p1 p2
+add' = binaryOp return 
+       (\(x:xs) (y:ys) -> do z  <- F.add x y
+                             zs <- add' xs ys
+                             return $ z : zs
+       )
+
+times (Poly p1) (Poly p2) = Poly <$> times' p1 p2
+times' = binaryOp (\_ -> return [])
+         (\(x:xs) ys -> do zs   <- times' xs ys
+                           f:fs <- forM ys $ F.times x
+                           rest <- add' zs fs
+                           return $ f : rest
+         )
+
+subtract (Poly p1) (Poly p2) = do
+  p2' <- forM p2 F.negate
+  Poly <$> add' p1 p2'
+
+-- | @compose p(x) q(x) = p(q(x))@
+compose (Poly p1) (Poly p2) = 
+    let p:ps = reverse p1
+    in do
+      Poly <$> compose' [p] ps p2
+
+compose' zs = binaryOp (\_  -> return zs)
+              (\(x:xs) ys -> do zs' <- zs `times'` ys >>= add' [x] 
+                                compose' zs' xs ys
+              )
+
+-- | @apply p x@ applies number @x@ to polynomial @p@
+apply :: MonadSAT m => NumPoly -> F.Number -> m F.Number
+apply (Poly poly) x = 
+    let p:ps = reverse poly
+    in 
+      foldM (\sum -> F.linear sum x) p ps
+
+-- | @derive p@ computes the derivation of @p@
+derive :: MonadSAT m => NumPoly -> m NumPoly
+derive (Poly p) = 
+    let p' = zip p [0..]
+        dx (x,e) = F.constant e >>= F.times x
+    in
+      (Poly . drop 1) <$> forM p' dx
+      
diff --git a/Satchmo/Polynomial/Numeric.hs b/Satchmo/Polynomial/Numeric.hs
new file mode 100644
--- /dev/null
+++ b/Satchmo/Polynomial/Numeric.hs
@@ -0,0 +1,84 @@
+{-# language MultiParamTypeClasses, FlexibleInstances #-}
+
+module Satchmo.Polynomial.Numeric where
+
+import qualified Satchmo.Boolean as B
+import Satchmo.Code
+import Satchmo.Numeric
+
+import Control.Monad ( forM )
+
+data Poly a = Poly [a] deriving Show
+
+instance Decode m a b => Decode m ( Poly a ) ( Poly b ) where
+    decode ( Poly xs ) = do
+        ys <- forM xs decode
+        return $ Poly ys
+
+derive ( Poly xs ) = do
+    ys <- forM ( drop 1 $ zip [ 0 .. ] xs ) $ \ (k,x) -> do
+        f <- constant k
+        times f x
+    return $ Poly ys
+    
+constantTerm ( Poly xs ) = head xs    
+
+polynomial :: ( Create a , B.MonadSAT m )
+           => Int -> Int 
+           -> m ( Poly a )
+polynomial bits degree = do
+    xs <- forM [ 0 .. degree ] $ \ k -> create bits
+    return $ Poly xs
+    
+compose ( Poly xs ) q = case xs of
+    [] -> return $ Poly []
+    x : xs -> do
+        p <- compose ( Poly xs ) q
+        pq <- times p q
+        plus ( Poly [x] ) pq
+    
+
+instance ( Create a, Constant a, Numeric a )
+         => Numeric ( Poly a ) where
+    equal ( Poly xs ) ( Poly ys ) = do
+        z <- create 0
+        bs <- forM ( fullZip xs ys ) $ \ xy -> case xy of
+            ( Just x, Just y ) -> equal x y
+            ( Just x, Nothing ) -> equal x z
+            ( Nothing, Just y ) -> equal z y
+        B.and bs
+    greater_equal  ( Poly xs ) ( Poly ys ) = do
+        z <- create 0
+        bs <- forM ( fullZip xs ys ) $ \ xy -> case xy of
+            ( Just x, Just y ) -> greater_equal x y
+            ( Just x, Nothing ) -> greater_equal x z
+            ( Nothing, Just y ) -> greater_equal z y
+        B.and bs
+    plus  ( Poly xs ) ( Poly ys ) = do
+        bs <- forM ( fullZip xs ys ) $ \ xy -> case xy of
+            ( Just x, Just y ) -> plus x y
+            ( Just x, Nothing ) -> return x
+            ( Nothing, Just y ) -> return y
+        return $ Poly bs
+    minus ( Poly xs ) ( Poly ys ) = do
+        z <- create 0
+        bs <- forM ( fullZip xs ys ) $ \ xy -> case xy of
+            ( Just x, Just y ) -> minus x y
+            ( Just x, Nothing ) -> return x
+            ( Nothing, Just y ) -> minus z y
+        return $ Poly bs
+    times ( Poly xs ) ( Poly ys ) = case xs of
+        [] -> return $ Poly []
+        x : xs -> do
+            xys <- forM ys $ times x
+            z <- constant 0
+            Poly rest <- times (Poly xs) (Poly ys)
+            plus ( Poly xys ) ( Poly $ z : rest )
+
+fullZip :: [a] -> [b] -> [ (Maybe a, Maybe b) ]    
+fullZip [] [] = []
+fullZip [] (y:ys) = (Nothing, Just y) : fullZip [] ys
+fullZip (x:xs) [] = (Just x, Nothing) : fullZip xs []
+fullZip (x:xs) (y:ys) = (Just x, Just y) : fullZip xs ys
+
+
diff --git a/Satchmo/PolynomialN.hs b/Satchmo/PolynomialN.hs
new file mode 100644
--- /dev/null
+++ b/Satchmo/PolynomialN.hs
@@ -0,0 +1,96 @@
+{-# language FlexibleInstances #-}
+{-# language MultiParamTypeClasses #-}
+{-# language FlexibleContexts      #-}
+
+module Satchmo.PolynomialN
+    ( Coefficient, Exponents, PolynomialN (), NumPolynomialN
+    , fromMonomials, add, equals)
+where
+
+import Control.Monad (forM,foldM)
+import Data.List (partition,sortBy)
+import qualified Satchmo.Binary.Op.Fixed as F
+import Satchmo.Code (Decode (..),decode)
+import Satchmo.MonadSAT (MonadSAT)
+import Satchmo.Boolean (Boolean)
+import qualified Satchmo.Boolean as B
+
+type Coefficient a = a
+
+type Exponents = [Integer]
+
+data Monomial a  = Monomial (Coefficient a, Exponents) deriving (Show)
+type NumMonomial = Monomial F.Number
+
+data PolynomialN a  = PolynomialN [Monomial a] deriving (Show)
+type NumPolynomialN = PolynomialN F.Number
+
+instance Decode m a Integer => Decode m (Monomial a) (Monomial Integer) where
+    decode (Monomial (coeff,vars)) = do
+      decodedCoeff <- decode coeff
+      return $ Monomial (decodedCoeff,vars)
+
+instance Decode m a Integer => Decode m (PolynomialN a) (PolynomialN Integer) where
+    decode (PolynomialN monomials) = do
+        decodedMonomials <- forM monomials decode
+        return $ PolynomialN decodedMonomials
+
+fromMonomials :: MonadSAT m 
+              => Int -- ^ bit width of coefficients
+              -> [(Coefficient Integer,Exponents)] -- ^ monomials
+              -> m NumPolynomialN
+fromMonomials bits monomials = do
+  monomials' <- forM monomials $ \(c,es) -> do
+                                 coefficient <- F.constantWidth bits c
+                                 return $ Monomial (coefficient,es)
+  reduce $ PolynomialN monomials'
+
+coefficient :: Monomial a -> Coefficient a
+coefficient (Monomial (c,_)) = c
+
+exponents :: Monomial a -> Exponents
+exponents (Monomial (_,e)) = e
+
+monomials :: PolynomialN a -> [Monomial a]
+monomials (PolynomialN xs) = xs
+
+sameExponents :: Monomial a -> Monomial a -> Bool
+sameExponents m1 m2 = exponents m1 == exponents m2
+
+add :: MonadSAT m => NumPolynomialN -> NumPolynomialN -> m NumPolynomialN
+add (PolynomialN xs) (PolynomialN ys) =
+    reduce $ PolynomialN $ xs ++ ys
+
+addMonomial :: MonadSAT m => NumMonomial -> NumMonomial -> m NumMonomial
+addMonomial m1 m2 =
+    if sameExponents m1 m2 then 
+        do c <- F.add (coefficient m1) (coefficient m2)
+           return $ Monomial (c, exponents m1)
+    else
+        error "PolynomialN.addMonomial"
+
+strictOrdering :: Monomial a -> Monomial a -> Ordering
+strictOrdering (Monomial (_,xs)) (Monomial (_,ys)) = compare xs ys
+
+reduce :: MonadSAT m => NumPolynomialN -> m NumPolynomialN
+reduce (PolynomialN []) = return $ PolynomialN []
+reduce (PolynomialN (x:xs)) =
+    let (reducable,notReducable) = partition (sameExponents x) xs
+        strictOrd (Monomial (_,xs)) (Monomial (_,ys)) = compare xs ys
+    in do
+      newMonomial <- foldM addMonomial x reducable
+      PolynomialN rest <- reduce $ PolynomialN notReducable
+      return $ PolynomialN $ sortBy strictOrd $ newMonomial : rest
+    
+equalsMonomial :: MonadSAT m => NumMonomial -> NumMonomial -> m Boolean
+equalsMonomial m1 m2 = do
+  equalsCoefficient <- F.equals (coefficient m1) (coefficient m2)
+  equalsExponents <- B.constant $ (exponents m1) == (exponents m2)
+  B.and [equalsCoefficient,equalsExponents]
+
+equals :: MonadSAT m => NumPolynomialN -> NumPolynomialN -> m Boolean
+equals (PolynomialN []) (PolynomialN []) = B.constant True
+equals (PolynomialN (x:xs)) (PolynomialN (y:ys)) = do
+  e <- equalsMonomial x y
+  es <- equals (PolynomialN xs) (PolynomialN ys)
+  B.and [e,es]
diff --git a/Satchmo/PolynomialSOS.hs b/Satchmo/PolynomialSOS.hs
new file mode 100644
--- /dev/null
+++ b/Satchmo/PolynomialSOS.hs
@@ -0,0 +1,49 @@
+module Satchmo.PolynomialSOS
+
+(nonNegative, positive, strictlyMonotone)
+
+where
+
+import Prelude hiding (null,and)
+import Control.Monad (foldM,replicateM)
+
+import Satchmo.MonadSAT (MonadSAT)
+import Satchmo.Polynomial 
+    (NumPoly,Poly,times,add,polynomial,null,equals,constantTerm,derive)
+import Satchmo.Boolean (Boolean,and)
+import qualified Satchmo.BinaryTwosComplement.Op.Fixed as F
+
+sqr :: MonadSAT m => NumPoly -> m NumPoly
+sqr p = p `times` p
+  
+sumOfSquares :: MonadSAT m => Int -> Int -> Int -> m NumPoly
+sumOfSquares coefficientBitWidth degree numPoly = do
+  sqrs <- replicateM numPoly 
+          $ polynomial coefficientBitWidth degree >>= sqr
+  foldM add null sqrs
+
+nonNegative :: MonadSAT m => Int -- ^ Bit width of coefficients
+            -> Int -- ^ Maximum degree
+            -> Int -- ^ Maximum number of polynomials
+            -> NumPoly -> m Boolean
+nonNegative coefficientBitWidth degree numPoly p = do
+  sos <- sumOfSquares coefficientBitWidth degree numPoly
+  equals sos p
+  
+positive :: MonadSAT m => Int -- ^ Bit width of coefficients
+            -> Int -- ^ Maximum degree
+            -> Int -- ^ Maximum number of polynomials
+            -> NumPoly -> m Boolean
+positive coefficientBitWidth degree numPoly p = do
+  sos <- sumOfSquares coefficientBitWidth degree numPoly
+  e1 <- equals sos p
+  e2 <- F.positive $ constantTerm sos 
+  and [e1, e2]
+
+strictlyMonotone :: MonadSAT m => Int -- ^ Bit width of coefficients
+            -> Int -- ^ Maximum degree
+            -> Int -- ^ Maximum number of polynomials
+            -> NumPoly -> m Boolean
+strictlyMonotone coefficientBitWidth degree numPoly p = do
+  p' <- derive p
+  positive coefficientBitWidth degree numPoly p'
diff --git a/Satchmo/Relation/Data.hs b/Satchmo/Relation/Data.hs
--- a/Satchmo/Relation/Data.hs
+++ b/Satchmo/Relation/Data.hs
@@ -1,8 +1,9 @@
-{-# language FlexibleInstances, MultiParamTypeClasses #-}
+{-# language FlexibleInstances, MultiParamTypeClasses, FlexibleContexts #-}
 
 module Satchmo.Relation.Data
 
 ( Relation, relation, build
+, identity                      
 , bounds, (!), indices, assocs
 , table
 ) 
@@ -16,8 +17,9 @@
 
 import qualified Data.Array as A
 import Data.Array hiding ( bounds, (!), indices, assocs )
+import Data.Functor ((<$>))
 
-import Control.Monad ( guard )
+import Control.Monad ( guard, forM )
 
 newtype Relation a b = Relation ( Array (a,b) Boolean ) 
 
@@ -32,12 +34,23 @@
             return ( p, x )
     return $ build bnd pairs
 
+identity :: ( Ix a, MonadSAT m) 
+         => ((a,a),(a,a)) -> m ( Relation a a )
+identity bnd = do            
+    f <- constant False
+    t <- constant True
+    return $ build bnd $ for ( A.range bnd ) $ \ (i,j) ->
+        ((i,j), if i == j then t else f )
+
+for = flip map
+
 build :: ( Ix a, Ix b ) 
       => ((a,b),(a,b)) 
       -> [ ((a,b), Boolean ) ]
       -> Relation a b 
 build bnd pairs = Relation $ array bnd pairs
 
+
 bounds :: (Ix a, Ix b) => Relation a b -> ((a,b),(a,b))
 bounds ( Relation r ) = A.bounds r
 
@@ -48,7 +61,8 @@
 
 Relation r ! p = r A.! p
 
-instance (Ix a, Ix b) => Decode ( Relation a b ) ( Array (a,b) Bool ) where
+instance (Ix a, Ix b, Decode m Boolean Bool) 
+    => Decode m  ( Relation a b ) ( Array (a,b) Bool ) where
     decode ( Relation r ) = do
         decode r
 
diff --git a/Satchmo/Relation/Op.hs b/Satchmo/Relation/Op.hs
--- a/Satchmo/Relation/Op.hs
+++ b/Satchmo/Relation/Op.hs
@@ -5,7 +5,7 @@
 ( mirror
 , union
 , complement
-, product
+, product, power
 , intersection
 ) 
 
@@ -33,6 +33,7 @@
 complement r = 
     build (bounds r) $ do i <- indices r ; return ( i, not $ r!i )
 
+
 union :: ( Ix a , Ix b, MonadSAT m ) 
       => Relation a b -> Relation a b 
       -> m ( Relation a b )
@@ -58,6 +59,18 @@
                 return $ and [ a!(x,y), b!(y,z) ]
             return ( i, o )
     return $ build bnd pairs
+
+power  :: ( Ix a , MonadSAT m ) 
+        => Int -> Relation a a -> m ( Relation a a )
+power 0 r = identity ( bounds r ) 
+power 1 r = return r
+power e r = do
+    let (d,m) = divMod e 2
+    s <- power d r
+    s2 <- product s s
+    case m of
+        0 -> return s2
+        1 -> product s2 r
 
 intersection :: ( Ix a , Ix b, MonadSAT m ) 
       => Relation a b -> Relation a b 
diff --git a/Satchmo/Relation/Prop.hs b/Satchmo/Relation/Prop.hs
--- a/Satchmo/Relation/Prop.hs
+++ b/Satchmo/Relation/Prop.hs
@@ -6,6 +6,7 @@
 , irreflexive
 , reflexive
 , regular
+, empty
 )
 
 where
@@ -14,7 +15,7 @@
 import qualified Prelude
 
 import Satchmo.Code
-import Satchmo.Boolean
+import Satchmo.Boolean hiding (implies)
 import Satchmo.Counting
 import Satchmo.Relation.Data
 import Satchmo.Relation.Op
@@ -31,6 +32,11 @@
     i <- indices r
     return $ or [ not $ r ! i, s ! i ]
 
+empty ::  ( Ix a, Ix b, MonadSAT m ) 
+        => Relation a b -> m Boolean
+empty r = and $ do
+    i <- indices r
+    return $ not $ r ! i
 
 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.hs b/Satchmo/SAT.hs
--- a/Satchmo/SAT.hs
+++ b/Satchmo/SAT.hs
@@ -4,6 +4,6 @@
   module Satchmo.SAT.Tmpfile
 ) where
 
-import Satchmo.SAT.Seq
-import Satchmo.SAT.BS
+-- import Satchmo.SAT.Seq
+-- import Satchmo.SAT.BS
 import Satchmo.SAT.Tmpfile
diff --git a/Satchmo/SAT/BS.hs b/Satchmo/SAT/BS.hs
deleted file mode 100644
--- a/Satchmo/SAT/BS.hs
+++ /dev/null
@@ -1,67 +0,0 @@
-{-# LANGUAGE GeneralizedNewtypeDeriving #-}
-
-module Satchmo.SAT.BS
-
-( SAT, Header(..)
-, fresh, fresh_forall
-, emit, Weight
-, sat
-)
-
-where
-
-import Satchmo.Data
-import Satchmo.MonadSAT
-
-import Control.Exception
-
-import Control.Monad.RWS.Strict
--- import Control.Monad.RWS.Lazy
-
--- import qualified Data.ByteString.Lazy.Char8 as BS
-import qualified Data.ByteString.Char8 as BS
-
-import Data.Foldable
-import Data.String
-
-newtype SAT a 
-      = SAT { unSAT :: -- WriterT BS.ByteString ( StateT Header Identity ) 
-                       -- StateT Header ( WriterT BS.ByteString Identity )
-                       RWS () BS.ByteString Header
-                       -- RWS () ( S.Seq BS.ByteString ) Header
-                       a
-            } 
-      deriving ( Functor, Monad
-               , MonadState Header
-               , MonadWriter BS.ByteString
-               -- , MonadWriter ( S.Seq BS.ByteString )
-               )
-
-
-instance MonadSAT SAT where
-  fresh = do 
-      a <- get 
-      let v = numVars a
-      put $ a { numVars = succ v } 
-      return $ literal True $ succ v
-  emit cl = do
-      a <- get
-      put $ a { numClauses = succ $ numClauses a }
-      tell $  fromString $ show  cl ++ "\n"
-  note msg = do
-      return ()
-     
-start :: Header
-start = Header { numClauses = 0, numVars = 0
-               , universals = []
-               }
-
-
-sat :: SAT a -> IO (BS.ByteString, Header, a )
-sat (SAT m) = do
-    let -- ((res,bs),accu) = runState (runWriterT m) start
-        -- ((res,accu),bs) = runWriter ( runStateT m  start )
-        (res, accu, bs) = runRWS m () start 
-    return ( bs , accu, res )
-
-
diff --git a/Satchmo/SAT/Mini.hs b/Satchmo/SAT/Mini.hs
new file mode 100644
--- /dev/null
+++ b/Satchmo/SAT/Mini.hs
@@ -0,0 +1,117 @@
+{-# LANGUAGE GeneralizedNewtypeDeriving #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE DoAndIfThenElse #-}
+{-# LANGUAGE PatternSignatures #-}
+{-# LANGUAGE StandaloneDeriving #-}
+
+
+module Satchmo.SAT.Mini 
+
+( SAT
+, fresh
+, emit
+, solve
+, solve_with_timeout
+)
+
+where
+
+import qualified MiniSat as API
+
+import Satchmo.Data
+import Satchmo.Boolean hiding ( not )
+import Satchmo.Code
+import Satchmo.MonadSAT
+
+import Control.Concurrent
+import Control.Concurrent.MVar
+import Control.Exception
+import Control.Monad ( when )
+import Control.Monad.Fix
+import System.IO
+
+
+deriving instance Enum API.Lit
+
+newtype SAT a 
+      = SAT { unSAT :: API.Solver -> IO a
+            } 
+
+instance Functor SAT where
+    fmap f ( SAT m ) = SAT $ \ s -> fmap f ( m s )
+
+instance Monad SAT where
+    return x = SAT $ \ s -> return x
+    SAT m >>= f = SAT $ \ s -> do 
+        x <- m s ; let { SAT n = f x } ; n s
+
+instance MonadFix SAT where
+    mfix f = SAT $ \ s -> mfix ( \ a -> unSAT (f a) s )
+
+instance MonadSAT SAT where
+  fresh = SAT $ \ s -> do 
+      x <- API.newLit s
+      let l = literal True $ fromEnum x
+      -- hPutStrLn stderr $ "fresh: " ++ show (x, l)
+      return l
+
+  emit cl = SAT $ \ s -> do
+      let conv l = ( if positive l then id else API.neg ) 
+                 $ toEnum
+                 $ variable l
+          apicl = map conv $ literals cl
+      res <- API.addClause s apicl
+      -- hPutStrLn stderr $ "adding clause " ++ show (cl, apicl, res)
+      return ()
+
+  note msg = SAT $ \ s -> hPutStrLn stderr msg
+
+  type Decoder SAT = SAT 
+  decode_variable v = SAT $ \ s -> do
+      Just val <- API.modelValue s $ toEnum $ fromEnum v
+      return val 
+      
+instance Decode SAT Boolean Bool where
+    decode b = case b of
+        Constant c -> return c
+        Boolean  l -> do 
+            let dv v = SAT $ \ s -> do
+                    Just val <- API.modelValue s $ toEnum $ fromEnum v
+                    return val 
+            v <- dv $ variable l
+            return $ if positive l then v else not v
+
+solve_with_timeout :: Maybe Int -> SAT (SAT a) -> IO (Maybe a)
+solve_with_timeout mto action = do
+    accu <- newEmptyMVar 
+    worker <- forkIO $ do res <- solve action ; putMVar accu res
+    timer <- forkIO $ case mto of
+        Just to -> do 
+              threadDelay ( 10^6 * to ) 
+              killThread worker 
+              putMVar accu Nothing
+        _  -> return ()
+    takeMVar accu `Control.Exception.catch` \ ( _ :: AsyncException ) -> do
+        hPutStrLn stderr "caught"
+        killThread worker
+        killThread timer
+        return Nothing
+
+solve :: SAT (SAT a) -> IO (Maybe a)
+solve action = API.withNewSolverAsync $ \ s -> do
+    hPutStrLn stderr $ "start producing CNF"
+    SAT decoder <- unSAT action s
+    v <- API.minisat_num_vars s
+    c <- API.minisat_num_clauses s
+    hPutStrLn stderr 
+        $ unwords [ "CNF finished", "vars", show v, "clauses", show c ]
+    hPutStrLn stderr $ "starting solver"
+    status <- API.limited_solve s []
+    hPutStrLn stderr $ "solver finished, result: " ++ show status
+    if status == API.l_True then do
+        hPutStrLn stderr $ "starting decoder"    
+        out <- decoder s
+        hPutStrLn stderr $ "decoder finished"    
+        return $ Just out
+    else return Nothing
diff --git a/Satchmo/SAT/Seq.hs b/Satchmo/SAT/Seq.hs
deleted file mode 100644
--- a/Satchmo/SAT/Seq.hs
+++ /dev/null
@@ -1,70 +0,0 @@
-{-# LANGUAGE GeneralizedNewtypeDeriving #-}
-
-module Satchmo.SAT.Seq
-
-( SAT, Header(..)
-, fresh, fresh_forall
-, emit, Weight
-, sat
-)
-
-where
-
-import Satchmo.Data
-import Satchmo.MonadSAT
-
-import Control.Exception
-
-import Control.Monad.RWS.Strict
--- import Control.Monad.RWS.Lazy
-
--- import qualified Data.Sequence as S
-import qualified Satchmo.SAT.Sequence as S
-
-import qualified Data.ByteString.Char8 as BS
--- import qualified Data.ByteString.Lazy.Char8 as BS
-
-import Data.Foldable
-import Data.String
-
-newtype SAT a 
-      = SAT { unSAT :: -- WriterT BS.ByteString ( StateT Header Identity ) 
-                       -- StateT Header ( WriterT BS.ByteString Identity )
-                       -- RWS () BS.ByteString Header
-                       RWS () ( S.Seq BS.ByteString ) Header
-                       a
-            } 
-      deriving ( Functor, Monad
-               , MonadState Header
-               , MonadWriter ( S.Seq BS.ByteString )
-               -- , MonadWriter BS.ByteString
-               )
-
-
-instance MonadSAT SAT where
-  note msg = do return ()
-  fresh = do 
-      a <- get 
-      let v = numVars a
-      put $ a { numVars = succ v } 
-      return $ literal True $ succ v
-  emit cl = do
-      a <- get
-      put $ a { numClauses = succ $ numClauses a }
-      tell $  S.singleton $ fromString $ show  cl ++ "\n"
-
-     
-start :: Header
-start = Header { numClauses = 0, numVars = 0
-               , universals = []
-               }
-
-
-sat :: SAT a -> IO (BS.ByteString, Header, a )
-sat (SAT m) = do
-    let -- ((res,bs),accu) = runState (runWriterT m) start
-        -- ((res,accu),bs) = runWriter ( runStateT m  start )
-        (res, accu, bs) = runRWS m () start 
-    return ( fold bs , accu, res )
-
-
diff --git a/Satchmo/SAT/Sequence.hs b/Satchmo/SAT/Sequence.hs
deleted file mode 100644
--- a/Satchmo/SAT/Sequence.hs
+++ /dev/null
@@ -1,26 +0,0 @@
--- | binary trees without any balance
-
-module Satchmo.SAT.Sequence where
-
-import Data.Monoid
-import Data.Foldable
-
-data Seq a = Empty | Leaf !a 
-           | Branch !(Seq a) !(Seq a)
-
-{-# INLINABLE singleton #-}
-singleton x = Leaf x
-
-instance Monoid (Seq a) where
-    {-# INLINABLE mappend #-}
-    mappend = Branch
-    {-# INLINABLE mempty #-}
-    mempty = Empty
-
-instance Foldable Seq where
-    {-# INLINABLE fold #-}
-    fold s = case s of
-        Empty -> mempty
-        Leaf k -> k
-        Branch l r -> mappend (fold l) (fold r)
-        
diff --git a/Satchmo/SAT/Tmpfile.hs b/Satchmo/SAT/Tmpfile.hs
--- a/Satchmo/SAT/Tmpfile.hs
+++ b/Satchmo/SAT/Tmpfile.hs
@@ -1,4 +1,7 @@
 {-# LANGUAGE GeneralizedNewtypeDeriving #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE TypeSynonymInstances, FlexibleInstances #-}
 
 module Satchmo.SAT.Tmpfile
 
@@ -11,6 +14,9 @@
 where
 
 import Satchmo.Data
+import Satchmo.Code
+import Satchmo.Boolean
+import Satchmo.Boolean.Data
 import Satchmo.MonadSAT
 
 import Control.Exception
@@ -28,14 +34,44 @@
 
 import Data.List ( sortBy )
 import Data.Ord ( comparing )
+import Data.Array
+import Control.Monad.Reader
 
+instance Decode (Reader (Array Variable Bool)) Boolean Bool where
+    decode b = case b of
+        Constant c -> return c
+        Boolean l -> asks $ \ arr -> positive l == arr ! variable l 
+
 instance MonadSAT SAT where
-  fresh = satfresh
-  fresh_forall = satfresh_forall
-  emit    = satemit
-  emitW _ _ = return ()
+  fresh = do
+    a <- get
+    let n = next a
+    put $ a { next = n + 1 }
+    return $ literal True n
+  emit clause = do
+    h <- ask 
+    liftIO $ hPutStrLn h $ show clause
+    a <- get
+    -- bshowClause c = BS.pack (show c) `mappend` BS.pack "\n"
+    -- tellSat (bshowClause clause)
+    put $ a
+        { size = size a + 1
+        , census = M.insertWith (+) (length $ literals clause) 1 $ census a 
+        }
+  -- emitW _ _ = return ()
+
   note msg = do a <- get ; put $ a { notes = msg : notes a }
 
+  type Decoder SAT = Reader (Array Int Bool) 
+  decode_variable v | v > 0 = asks $ \ arr ->  arr ! v
+
+{-
+    readsPrec p = \ cs -> do
+        ( i, cs') <- readsPrec p cs
+        return ( Literal i , cs' )
+-}
+
+
 -- ---------------
 -- Implementation
 -- ---------------
@@ -58,7 +94,7 @@
       }
 
 newtype SAT a = SAT {unsat::RWST Handle () Accu IO a}
-    deriving (MonadState Accu, MonadReader Handle, Monad, MonadIO, Functor)
+    deriving (MonadState Accu, MonadReader Handle, Monad, MonadIO, Functor, MonadFix)
 
 
 sat :: SAT a -> IO (BS.ByteString, Header, a )
@@ -84,32 +120,6 @@
        bs <- BS.readFile fp
        return (bs, header, a))
 
--- | existentially quantified (implicitely so, before first fresh_forall)
-satfresh :: SAT Literal
-satfresh = do
-    a <- get
-    let n = next a
-    put $ a { next = n + 1 }
-    return $ literal True n
-
--- | universally quantified
-satfresh_forall :: SAT Literal
-satfresh_forall = do
-    a <- get
-    let n = next a
-    put $ a { next = n + 1, universal = n : universal a }
-    return $ literal True n
-
-satemit :: Clause -> SAT ()
-satemit clause = do
-    h <- ask ; liftIO $ hPutStrLn h $ show clause
-    a <- get
-    -- tellSat (bshowClause clause)
-    put $ a
-        { size = size a + 1
-        , census = M.insertWith (+) (length $ literals clause) 1 $ census a         
-        }
-  where bshowClause c = BS.pack (show c) `mappend` BS.pack "\n"
 
 
 tellSat x = do {h <- ask; liftIO $ BS.hPut h x}
diff --git a/Satchmo/SAT/Weighted.hs b/Satchmo/SAT/Weighted.hs
deleted file mode 100644
--- a/Satchmo/SAT/Weighted.hs
+++ /dev/null
@@ -1,89 +0,0 @@
-{-# LANGUAGE GeneralizedNewtypeDeriving #-}
-module Satchmo.SAT.Weighted (SAT, sat, MaxWeight, Header(..)) where
-
-import Satchmo.Data
-import Satchmo.MonadSAT hiding ( Header )
-
-import Control.Exception
-import Control.Monad.RWS.Strict
-import Data.Maybe
-import qualified  Data.Set as Set
--- import qualified Data.ByteString.Lazy.Char8 as BS
-import qualified Data.ByteString.Char8 as BS
-import System.Directory
-import System.Environment
-import System.IO
-
-
-instance MonadSAT SAT where
-  fresh = satfresh
-  fresh_forall = satfresh_forall
-  emit  = satemit Nothing
-  emitW = satemit . Just
-
--- ---------------
--- Implementation
--- ---------------
-
-data Accu = Accu
-          { next :: ! Int
-          , universal :: [Int]
-          , size :: ! Int
-          }
-
-start :: Accu
-start = Accu
-      { next = 1
-      , universal = []
-      , size = 0
-      }
-
-type MaxWeight  = Int
-
-newtype SAT a = SAT {unsat::RWST (Handle, MaxWeight) () Accu IO a}
-    deriving (MonadState Accu, MonadReader (Handle, MaxWeight), Monad, MonadIO, Functor)
-
-data Header = Header { numClauses, numVars, maxWeight :: Int
-                     , universals :: [Int]
-                     }
-
-sat :: MaxWeight -> SAT a -> IO (BS.ByteString, Header, a )
-sat maxW (SAT m) =
- bracket
-    (getTemporaryDirectory >>= (`openTempFile`  "satchmo"))
-    (\(fp, h) -> removeFile fp)
-    (\(fp, h) -> do
-       hSetBuffering h (BlockBuffering Nothing)
-       ~(a, accu, _) <- runRWST m (h, maxW) start
-       hClose h
-       let header = Header (size accu) (next accu - 1) maxW universals
-           universals = reverse $ universal accu
-
-       bs <- BS.readFile fp
-       return (bs, header, a))
-
--- | existentially quantified (implicitely so, before first fresh_forall)
-satfresh :: SAT Literal
-satfresh = do
-    a <- get
-    let n = next a
-    put $ a { next = n + 1 }
-    return $ literal True n
-
--- | universally quantified
-satfresh_forall :: SAT Literal
-satfresh_forall = do
-    a <- get
-    let n = next a
-    put $ a { next = n + 1, universal = n : universal a }
-    return $ literal True n
-
-satemit :: Maybe Weight -> Clause -> SAT ()
-satemit w (Clause clause) = do
-    a <- get
-    (h,maxW) <- ask
-    liftIO $ BS.hPut h (bshowClause $ Clause(Literal (fromMaybe maxW w) : clause))
-    put $ a { size = size a + 1}
-
-  where bshowClause c = BS.pack (show c) `mappend` BS.pack "\n"
-
diff --git a/Satchmo/SMT/Exotic/Arctic.hs b/Satchmo/SMT/Exotic/Arctic.hs
new file mode 100644
--- /dev/null
+++ b/Satchmo/SMT/Exotic/Arctic.hs
@@ -0,0 +1,69 @@
+{-# 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
new file mode 100644
--- /dev/null
+++ b/Satchmo/SMT/Exotic/Arctic/Integer.hs
@@ -0,0 +1,93 @@
+{-# 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
new file mode 100644
--- /dev/null
+++ b/Satchmo/SMT/Exotic/Dict.hs
@@ -0,0 +1,17 @@
+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
new file mode 100644
--- /dev/null
+++ b/Satchmo/SMT/Exotic/Domain.hs
@@ -0,0 +1,4 @@
+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
new file mode 100644
--- /dev/null
+++ b/Satchmo/SMT/Exotic/Fuzzy.hs
@@ -0,0 +1,63 @@
+{-# 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
new file mode 100644
--- /dev/null
+++ b/Satchmo/SMT/Exotic/Natural.hs
@@ -0,0 +1,80 @@
+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
new file mode 100644
--- /dev/null
+++ b/Satchmo/SMT/Exotic/Semiring.hs
@@ -0,0 +1,10 @@
+{-# 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
new file mode 100644
--- /dev/null
+++ b/Satchmo/SMT/Exotic/Semiring/Arctic.hs
@@ -0,0 +1,32 @@
+{-# 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
new file mode 100644
--- /dev/null
+++ b/Satchmo/SMT/Exotic/Semiring/Class.hs
@@ -0,0 +1,18 @@
+{-# 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
new file mode 100644
--- /dev/null
+++ b/Satchmo/SMT/Exotic/Semiring/Fuzzy.hs
@@ -0,0 +1,28 @@
+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
new file mode 100644
--- /dev/null
+++ b/Satchmo/SMT/Exotic/Semiring/Natural.hs
@@ -0,0 +1,9 @@
+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
new file mode 100644
--- /dev/null
+++ b/Satchmo/SMT/Exotic/Semiring/Rational.hs
@@ -0,0 +1,13 @@
+{-# 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
new file mode 100644
--- /dev/null
+++ b/Satchmo/SMT/Exotic/Semiring/Tropical.hs
@@ -0,0 +1,32 @@
+{-# 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
new file mode 100644
--- /dev/null
+++ b/Satchmo/SMT/Exotic/Tropical.hs
@@ -0,0 +1,80 @@
+-- | 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/Simple.hs b/Satchmo/Simple.hs
deleted file mode 100644
--- a/Satchmo/Simple.hs
+++ /dev/null
@@ -1,30 +0,0 @@
-{-# language GeneralizedNewtypeDeriving #-}
-
-module Satchmo.Simple where
-
-import Satchmo.MonadSAT
-import Satchmo.Data
-
-import Control.Monad.State
-
-data Accu = Accu { next :: ! Int
-                 , pool :: [ Clause ]
-                 }
-
-start = Accu { next = 0, pool = [] }
-
-sat (SAT m) = flip evalState start
-            $ do x <- m; a <- get ; return (cnf $ pool a, x) 
-
-newtype SAT a = SAT { unsat :: State Accu a } 
-    deriving ( Functor, Monad )
-
-instance MonadSAT SAT where
-    fresh = SAT $ do 
-          a <- get ; let n = succ $ next a 
-          put $ a { next = n } ; return $ Literal n
-    emit c = SAT $ do
-          modify $ \ a -> a { pool = c : pool a }
-
-
-        
diff --git a/Satchmo/Solve.hs b/Satchmo/Solve.hs
deleted file mode 100644
--- a/Satchmo/Solve.hs
+++ /dev/null
@@ -1,63 +0,0 @@
--- | This is the API for plugging in solver implementations.
--- Actual implementations are in the (separate) package @satchmo-backends@
-
-module Satchmo.Solve
-
-( solve, solveW
-, Implementation, WeightedImplementation
-, Decoder
-)
-
-where
-
-import Satchmo.Data
-import Satchmo.Code
-import Satchmo.SAT
-import qualified Satchmo.SAT.Weighted as Weighted
-
--- import qualified Data.ByteString.Lazy.Char8 as BS
-import qualified Data.ByteString.Char8 as BS
-
-import Data.Map ( Map )
-import qualified Data.Map as M
-import Data.Array
-import Control.Monad.Reader
-
-import System.IO
-
-type Implementation = BS.ByteString 
-                    -> Header 
-                    -> IO ( Maybe ( Array Variable Bool ) )
-
-type WeightedImplementation = BS.ByteString 
-    -> Weighted.Header 
-    -> IO ( Maybe ( Array Variable Bool ) )
-
-solve :: Implementation
-      -> SAT ( Decoder a ) 
-      -> IO ( Maybe a )
-solve implementation build = do
-    (s, h, a) <- sat build
-    mfm <- implementation s h
-    case mfm of
-        Nothing -> do
-            hPutStrLn stderr "not satisfiable"
-            return Nothing
-        Just fm -> do
-            hPutStrLn stderr "satisfiable"
-            return $ Just $ runReader a fm
-
-solveW :: Weighted.MaxWeight 
-       -> WeightedImplementation 
-       -> Weighted.SAT (Decoder a) 
-       -> IO (Maybe a)
-solveW maxW implementation build = do
-    (s, h, a) <- Weighted.sat maxW build
-    mfm <- implementation s h
-    case mfm of
-        Nothing -> do
-            hPutStrLn stderr "not satisfiable"
-            return Nothing
-        Just fm -> do
-            hPutStrLn stderr "satisfiable"
-            return $ Just $ runReader a fm
diff --git a/Satchmo/Unary.hs b/Satchmo/Unary.hs
new file mode 100644
--- /dev/null
+++ b/Satchmo/Unary.hs
@@ -0,0 +1,10 @@
+module Satchmo.Unary 
+       
+( module Satchmo.Unary.Data
+, module Satchmo.Unary.Op.Flexible
+)       
+       
+where
+
+import Satchmo.Unary.Data
+import Satchmo.Unary.Op.Flexible
diff --git a/Satchmo/Unary/Data.hs b/Satchmo/Unary/Data.hs
new file mode 100644
--- /dev/null
+++ b/Satchmo/Unary/Data.hs
@@ -0,0 +1,55 @@
+{-# language MultiParamTypeClasses #-}
+{-# language FlexibleInstances #-}
+{-# language FlexibleContexts #-}
+{-# language UndecidableInstances #-}
+
+module Satchmo.Unary.Data 
+       
+( Number, bits, make       
+, width, number, constant )                
+       
+where
+
+import Prelude hiding ( and, or, not )
+
+import qualified Satchmo.Code as C
+
+import Satchmo.Boolean hiding ( constant )
+import qualified  Satchmo.Boolean as B
+
+import Control.Monad ( forM, when )
+
+data Number = Number
+            { bits :: [ Boolean ] 
+            -- ^ contents is [ 1 .. 1 0 .. 0 ]
+            -- number of 1 is value of number  
+            }  
+            
+instance C.Decode m Boolean Bool => C.Decode m Number Int where            
+    decode n = do
+        bs <- forM ( bits n ) C.decode
+        return $ length $ filter id bs
+
+instance C.Decode m Boolean Bool => C.Decode m Number Integer where 
+    decode n = do
+        bs <- forM ( bits n ) C.decode
+        return $ fromIntegral $ length $ filter id bs
+
+width :: Number -> Int
+width n = length $ bits n
+
+-- | declare a number with range (0, w)
+number :: MonadSAT m => Int -> m  Number 
+number w = do
+    xs <- sequence $ replicate w boolean
+    forM ( zip xs $ tail xs ) $ \ (p, q) ->
+        assert [ p, not q ]
+    return $ make xs
+    
+make :: [ Boolean ] -> Number 
+make xs = Number { bits = xs }
+
+constant :: MonadSAT m => Integer -> m Number 
+constant k = do
+    xs <- forM [ 1 .. k ] $ \ i -> B.constant True
+    return $ make xs
diff --git a/Satchmo/Unary/Op/Common.hs b/Satchmo/Unary/Op/Common.hs
new file mode 100644
--- /dev/null
+++ b/Satchmo/Unary/Op/Common.hs
@@ -0,0 +1,211 @@
+{-# language NoMonomorphismRestriction #-}
+{-# language PatternSignatures #-}
+
+module Satchmo.Unary.Op.Common 
+       
+( iszero, equals
+, lt, le, ge, eq, gt
+, min, max
+, minimum, maximum
+, select, antiselect
+, add_quadratic, add_by_odd_even_merge, add_by_bitonic_sort
+)          
+       
+where
+
+
+import Prelude 
+  hiding ( and, or, not, compare, min, max, minimum, maximum )
+import qualified Prelude
+
+import qualified Satchmo.Code as C
+
+import Satchmo.Unary.Data 
+    (Number, make, bits, width, constant)
+
+import Satchmo.Boolean (MonadSAT, Boolean, Booleans, fun2, fun3, and, or, not, xor, assert, boolean, monadic)
+import qualified  Satchmo.Boolean as B
+
+import Control.Monad ( forM, when, foldM, guard )
+import qualified Data.Map as M
+import Data.List ( transpose )
+
+iszero n = case bits n of
+    [] -> B.constant True
+    x : xs -> return $ not x
+    
+extended :: MonadSAT m 
+         => ( [(Boolean,Boolean)] -> m a )
+         -> Number -> Number
+         -> m a
+extended action a b = do
+    f <- B.constant False
+    let zipf [] [] = []
+        zipf (x:xs) [] = (x,f) : zipf xs []
+        zipf [] (y:ys) = (f,y) : zipf [] ys
+        zipf (x:xs) (y:ys) = (x,y) : zipf xs ys
+    action $ zipf ( bits a ) ( bits b )    
+        
+
+le, ge, eq, equals, gt, lt 
+  :: MonadSAT m => Number -> Number -> m Boolean
+
+for = flip map
+
+equals = extended $ \ xys -> monadic and $ 
+    for xys $ \ (x,y) -> fun2 (==) x y
+
+le = extended $ \ xys -> monadic and $ 
+    for xys $ \ (x,y) -> fun2 (<=) x y
+
+ge = flip le
+
+eq = equals
+
+lt a b = fmap not $ ge a b
+
+gt = flip lt
+
+min a b = do 
+    cs <- extended ( \ xys -> 
+        forM xys $ \ (x,y) -> and [x,y] ) a b
+    return $ make cs                              
+                          
+max a b = do
+    cs <- extended ( \ xys -> 
+        forM xys $ \ (x,y) -> or [x,y] ) a b
+    return $ make cs                      
+
+-- | maximum (x:xs) = foldM max x xs
+maximum [x] = return x
+maximum xs | Prelude.not ( null xs ) = do
+    f <- B.constant False
+    let w = Prelude.maximum $ map width xs
+        fill x = bits x ++ replicate (w - width x) f
+    ys <- forM ( transpose $ map fill xs ) B.or
+    return $ make ys
+
+-- | minimum (x:xs) = foldM min x xs
+minimum [x] = return x
+minimum xs | Prelude.not ( null xs ) = do
+    f <- B.constant False
+    let w = Prelude.maximum $ map width xs
+        fill x = bits x ++ replicate (w - width x) f
+    ys <- forM ( transpose $ map fill xs ) B.and
+    return $ make ys
+
+
+-- | when f is False, switch off all bits
+select f a = do
+    bs <- forM ( bits a ) $ \ b -> and [f,b]
+    return $ make bs
+
+-- | when p is True, switch ON all bits
+antiselect p n = do
+    bs <- forM ( bits n ) $ \ b -> B.or [p, b]
+    return $ make bs
+
+-- | reduce number to given bit width,
+-- and return also the carry bit
+cutoff_with_carry :: MonadSAT m 
+                  => Maybe Int -> Number -> m (Number, Boolean)
+cutoff_with_carry mwidth n = do
+    f <- B.constant False
+    case mwidth of
+        Nothing -> return (n , f )
+        Just width -> do
+            let ( pre, post ) = splitAt width $ bits n
+            return ( make pre, case post of
+                [] -> f
+                carry : _ -> carry )
+
+cutoff mwidth n = do
+    ( result, carry ) <- cutoff_with_carry mwidth n
+    assert [ not carry ]
+    return result
+
+-- | for both "add" methods: if first arg is Nothing, 
+-- then result length is sum of argument lengths (cannot overflow).
+-- else result is cut off (overflow => unsatisfiable)
+add_quadratic :: MonadSAT m => Maybe Int -> Number -> Number -> m Number
+add_quadratic mwidth a b = do
+    t <- B.constant True
+    pairs <- sequence $ do
+        (i,x) <- zip [0 .. ] $ t : bits a
+        (j,y) <- zip [0 .. ] $ t : bits b
+        guard $ i+j > 0
+        guard $ case mwidth of
+            Just width -> i+j <= width + 1
+            Nothing    -> True
+        return $ do z <- and [x,y] ; return (i+j, [z])
+    cs <- forM ( map snd $ M.toAscList $ M.fromListWith (++) pairs ) or
+    cutoff mwidth $ make cs
+
+
+  
+-- | works for all widths
+add_by_odd_even_merge mwidth a b = do
+    zs <- oe_merge (bits a) (bits b)
+    cutoff mwidth $ make zs
+    
+-- | will fill up the input 
+-- such that length is a power of two.
+-- it seems to be hard to improve this, cf
+-- <http://www.cs.technion.ac.il/users/wwwb/cgi-bin/tr-info.cgi/2009/CS/CS-2009-07>
+add_by_bitonic_sort mwidth a b = do
+    let n = length ( bits a) + length (bits b)
+    f <- B.constant False        
+    let input =    (bits a) -- decreasing
+                ++ replicate (fill n) f
+                ++ (reverse $ bits b) -- increasing
+    zs <- bitonic_sort input
+    cutoff mwidth $ make zs
+
+-- | distance to next power of two
+fill n = if n <= 1 then 0 else
+            let (d,m) = divMod n 2
+            in  m + 2*fill (d+m) 
+
+-- |  <http://www.iti.fh-flensburg.de/lang/algorithmen/sortieren/bitonic/bitonicen.htm>
+bitonic_sort [ ] = return [ ]    
+bitonic_sort [z] = return [z]
+bitonic_sort zs = do 
+    let (h,0) = divMod (length zs) 2
+        (pre, post) = splitAt h zs
+    hi <- forM ( zip pre post ) $ \ (x,y) -> or  [x,y]
+    lo <- forM ( zip pre post ) $ \ (x,y) -> and [x,y]
+    shi <- bitonic_sort hi
+    slo <- bitonic_sort lo
+    return $ shi ++ slo
+    
+-- | <http://www.iti.fh-flensburg.de/lang/algorithmen/sortieren/networks/oemen.htm>
+
+oe_merge  [] ys = return ys
+oe_merge  xs [] = return xs
+oe_merge  [x] [y] = do
+    comparator x y
+oe_merge  xs ys = do
+    let ( xo, xe ) = divide xs
+        ( yo, ye ) = divide ys
+    m : mo <- oe_merge  xo yo
+    me <- oe_merge  xe ye
+    re <- repair me mo
+    return $ m : re
+
+divide (x : xs) = 
+    let ( this, that ) = divide xs
+    in  ( x : that, this )
+divide [] = ( [], [] )
+
+repair (x:xs) (y:ys) = do
+    here <- comparator x y
+    later <- repair xs ys
+    return $ here ++ later
+repair [] [] = return []
+repair [x] [] = return [x]
+repair [] [y] = return [y]
+
+comparator x y = do
+    hi <- Satchmo.Boolean.or [x, y]
+    lo <- Satchmo.Boolean.and [x, y]
+    return [ hi, lo ]
diff --git a/Satchmo/Unary/Op/Fixed.hs b/Satchmo/Unary/Op/Fixed.hs
new file mode 100644
--- /dev/null
+++ b/Satchmo/Unary/Op/Fixed.hs
@@ -0,0 +1,37 @@
+module Satchmo.Unary.Op.Fixed 
+
+( module Satchmo.Unary.Op.Common 
+, add
+, add_quadratic
+, add_by_odd_even_merge
+, add_by_bitonic_sort
+)       
+       
+where
+
+import Prelude hiding ( not, and, or )
+import qualified Prelude
+
+import Satchmo.Boolean
+import   Satchmo.Unary.Data
+import qualified Satchmo.Unary.Op.Common as C
+import Satchmo.Unary.Op.Common hiding
+  (add_quadratic, add_by_odd_even_merge, add_by_bitonic_sort)
+
+import Control.Monad ( forM, when, guard )
+import qualified Data.Map as M
+
+add :: MonadSAT m => Number -> Number -> m Number
+add = add_quadratic
+
+add_quadratic a b = 
+    C.add_quadratic (Just $ Prelude.max ( width a ) ( width b )) a b
+
+add_by_odd_even_merge a b = 
+    C.add_by_odd_even_merge (Just $ Prelude.max ( width a ) ( width b )) a b
+
+add_by_bitonic_sort a b = 
+    C.add_by_bitonic_sort (Just $ Prelude.max ( width a ) ( width b )) a b
+
+
+    
diff --git a/Satchmo/Unary/Op/Flexible.hs b/Satchmo/Unary/Op/Flexible.hs
new file mode 100644
--- /dev/null
+++ b/Satchmo/Unary/Op/Flexible.hs
@@ -0,0 +1,35 @@
+module Satchmo.Unary.Op.Flexible 
+       
+( module Satchmo.Unary.Op.Common 
+, add
+, add_quadratic
+, add_by_odd_even_merge
+, add_by_bitonic_sort
+)       
+       
+where
+
+import Prelude hiding ( not, and, or )
+import qualified Prelude
+
+import Satchmo.Boolean
+import   Satchmo.Unary.Data
+import qualified Satchmo.Unary.Op.Common as C
+import Satchmo.Unary.Op.Common hiding
+  (add_quadratic, add_by_odd_even_merge, add_by_bitonic_sort)
+
+import Control.Monad ( forM )
+import qualified Data.Map as M
+
+-- | Unary addition. Output bit length is sum of input bit lengths.
+add :: MonadSAT m => Number -> Number -> m Number
+add = add_by_odd_even_merge
+
+add_quadratic a b = 
+    C.add_quadratic (Just $ (+) ( width a ) ( width b )) a b
+
+add_by_odd_even_merge a b = 
+    C.add_by_odd_even_merge (Just $ (+) ( width a ) ( width b )) a b
+
+add_by_bitonic_sort a b = 
+    C.add_by_bitonic_sort (Just $ (+) ( width a ) ( width b )) a b
diff --git a/Setup.hs b/Setup.hs
--- a/Setup.hs
+++ b/Setup.hs
@@ -1,2 +1,6 @@
+module Main (main) where
+
 import Distribution.Simple
+
+main :: IO ()
 main = defaultMain
diff --git a/satchmo.cabal b/satchmo.cabal
--- a/satchmo.cabal
+++ b/satchmo.cabal
@@ -1,36 +1,51 @@
 Name:           satchmo
-Version:        1.9.1
+Version:        2.6.0
 
 License:        GPL
 License-file:	gpl-2.0.txt
-Author:         Pepe Iborra, Johannes Waldmann
+Author:         Pepe Iborra, Johannes Waldmann, Alexander Bau
 Maintainer:	Johannes Waldmann
-Homepage:       http://dfa.imn.htwk-leipzig.de/satchmo/
-		http://github.com/pepeiborra/satchmo/
+Homepage:       <https://github.com/jwaldmann/satchmo>
 Synopsis:       SAT encoding monad
-description:	Encoding for boolean and integral constraints into (QBF-)CNF-SAT.
-		The encoder is provided as a State monad (hence the "mo" in "satchmo").
-		This package contains functions that construct problems,
-                to solve them, you need package satchmo-backends.
-Category:	Algorithms
+description:	Encoding for boolean and integral constraints into CNF-SAT.
+		The encoder is provided as a State monad 
+		(hence the "mo" in "satchmo").
+
+		This package depends on minisat-haskell-bindings, see
+		<https://github.com/niklasso/minisat-haskell-bindings>
+Category:	Logic
 cabal-version:  >= 1.6
 build-type: Simple
+source-repository head
+    type: git
+    location:   https://github.com/jwaldmann/satchmo
 
 Library
     ghc-options: -funbox-strict-fields
-    Build-depends:  mtl, process, containers, base == 4.*, array, bytestring, directory
+    Build-depends:  mtl, process, containers, base == 4.*,
+               array, bytestring, directory, minisat >= 0.1
     Exposed-modules:
         Satchmo.Data
-        Satchmo.Solve
+        -- Satchmo.Data.Default
+        -- Satchmo.Solve
         Satchmo.Boolean
         Satchmo.Counting
         Satchmo.Code
-        Satchmo.Binary
         Satchmo.Integer
+        Satchmo.Binary
         Satchmo.Binary.Op.Common
+        Satchmo.Binary.Op.Times
         Satchmo.Binary.Op.Fixed
         Satchmo.Binary.Op.Flexible
+        Satchmo.BinaryTwosComplement.Op.Fixed
+        Satchmo.BinaryTwosComplement
+        Satchmo.Unary
+        Satchmo.Unary.Op.Common
+        Satchmo.Unary.Op.Fixed
+        Satchmo.Unary.Op.Flexible
         Satchmo.Polynomial
+        Satchmo.PolynomialN
+        Satchmo.PolynomialSOS
         Satchmo.Relation
         Satchmo.Relation.Data
         Satchmo.Relation.Op
@@ -38,13 +53,36 @@
         Satchmo.MonadSAT
         Satchmo.SAT
         Satchmo.SAT.Tmpfile
-        Satchmo.SAT.BS
-        Satchmo.SAT.Seq
-        Satchmo.SAT.Sequence
-        Satchmo.Simple
-        Satchmo.SAT.Weighted
+        Satchmo.SAT.Mini
+        -- Satchmo.SAT.BS
+        -- Satchmo.SAT.Seq
+        -- Satchmo.SAT.Sequence
+        -- Satchmo.Simple
+        -- Satchmo.SAT.Weighted
+        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
     Other-modules:
         Satchmo.Binary.Data
+        Satchmo.BinaryTwosComplement.Data
+        Satchmo.BinaryTwosComplement.Op.Common
+        Satchmo.Unary.Data
         Satchmo.Integer.Data
         Satchmo.Boolean.Op
         Satchmo.Integer.Op