satchmo 1.9.1 → 2.6.0

raw patch · 58 files changed

+2250/−756 lines, 58 filesdep +minisatsetup-changedPVP ok

version bump matches the API change (PVP)

Dependencies added: minisat

API changes (from Hackage documentation)

Files

• Satchmo/Binary/Data.hs +20/−7
• Satchmo/Binary/Numeric.hs +19/−0
• Satchmo/Binary/Op/Common.hs +68/−28
• Satchmo/Binary/Op/Fixed.hs +42/−58
• Satchmo/Binary/Op/Flexible.hs +8/−31
• Satchmo/Binary/Op/Times.hs +73/−0
• Satchmo/BinaryTwosComplement.hs +7/−0
• Satchmo/BinaryTwosComplement/Data.hs +98/−0
• Satchmo/BinaryTwosComplement/Numeric.hs +17/−0
• Satchmo/BinaryTwosComplement/Op/Common.hs +38/−0
• Satchmo/BinaryTwosComplement/Op/Fixed.hs +94/−0
• Satchmo/Boolean/Data.hs +30/−29
• Satchmo/Boolean/Op.hs +58/−15
• Satchmo/Code.hs +22/−13
• Satchmo/Counting.hs +12/−26
• Satchmo/Data.hs +22/−38
• Satchmo/Integer/Data.hs +3/−5
• Satchmo/Integer/Difference.hs +58/−0
• Satchmo/Integer/Op.hs +3/−3
• Satchmo/MonadSAT.hs +18/−6
• Satchmo/Numeric.hs +21/−0
• Satchmo/Polynomial.hs +137/−97
• Satchmo/Polynomial/Numeric.hs +84/−0
• Satchmo/PolynomialN.hs +96/−0
• Satchmo/PolynomialSOS.hs +49/−0
• Satchmo/Relation/Data.hs +17/−3
• Satchmo/Relation/Op.hs +14/−1
• Satchmo/Relation/Prop.hs +7/−1
• Satchmo/SAT.hs +2/−2
• Satchmo/SAT/BS.hs +0/−67
• Satchmo/SAT/Mini.hs +117/−0
• Satchmo/SAT/Seq.hs +0/−70
• Satchmo/SAT/Sequence.hs +0/−26
• Satchmo/SAT/Tmpfile.hs +41/−31
• Satchmo/SAT/Weighted.hs +0/−89
• Satchmo/SMT/Exotic/Arctic.hs +69/−0
• Satchmo/SMT/Exotic/Arctic/Integer.hs +93/−0
• Satchmo/SMT/Exotic/Dict.hs +17/−0
• Satchmo/SMT/Exotic/Domain.hs +4/−0
• Satchmo/SMT/Exotic/Fuzzy.hs +63/−0
• Satchmo/SMT/Exotic/Natural.hs +80/−0
• Satchmo/SMT/Exotic/Semiring.hs +10/−0
• Satchmo/SMT/Exotic/Semiring/Arctic.hs +32/−0
• Satchmo/SMT/Exotic/Semiring/Class.hs +18/−0
• Satchmo/SMT/Exotic/Semiring/Fuzzy.hs +28/−0
• Satchmo/SMT/Exotic/Semiring/Natural.hs +9/−0
• Satchmo/SMT/Exotic/Semiring/Rational.hs +13/−0
• Satchmo/SMT/Exotic/Semiring/Tropical.hs +32/−0
• Satchmo/SMT/Exotic/Tropical.hs +80/−0
• Satchmo/Simple.hs +0/−30
• Satchmo/Solve.hs +0/−63
• Satchmo/Unary.hs +10/−0
• Satchmo/Unary/Data.hs +55/−0
• Satchmo/Unary/Op/Common.hs +211/−0
• Satchmo/Unary/Op/Fixed.hs +37/−0
• Satchmo/Unary/Op/Flexible.hs +35/−0
• Setup.hs +4/−0
• satchmo.cabal +55/−17

@@ -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

@@ -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 

@@ -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

@@ -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 

@@ -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)

@@ -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]) ] ++

@@ -0,0 +1,7 @@+module Satchmo.BinaryTwosComplement++( module Satchmo.BinaryTwosComplement.Op.Fixed )++where++import Satchmo.BinaryTwosComplement.Op.Fixed 

@@ -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

@@ -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 

@@ -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

@@ -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

@@ -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 #-}+

@@ -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 ]- 

@@ -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

@@ -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

@@ -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 #-}

@@ -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

@@ -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 }

@@ -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  ----------------------------------------------------

@@ -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++-}

@@ -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+    

@@ -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+      

@@ -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++

@@ -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]

@@ -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'

@@ -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 

@@ -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 

@@ -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 #-}      

@@ -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

@@ -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 )--

@@ -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

@@ -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 )--

@@ -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)-        

@@ -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}

@@ -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"-

@@ -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+  }+

@@ -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+  }+

@@ -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+    }+++

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

@@ -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+  }

@@ -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

@@ -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+

@@ -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         

@@ -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++

@@ -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

@@ -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

@@ -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

@@ -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         

@@ -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

@@ -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 }---        

@@ -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

@@ -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

@@ -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

@@ -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 ]

@@ -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+++    

@@ -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

@@ -1,2 +1,6 @@+module Main (main) where+ import Distribution.Simple++main :: IO () main = defaultMain

@@ -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