satchmo 2.9.9.3 → 2.9.9.4

raw patch · 112 files changed

+4061/−4072 lines, 112 filesdep −memoizedep ~basePVP: major bump suggested

API removals or changes: PVP suggests a major version bump

Dependencies removed: memoize

Dependency ranges changed: base

API changes (from Hackage documentation)

Files

• Satchmo/Array.hs +0/−39
• Satchmo/Binary.hs +0/−10
• Satchmo/Binary/Data.hs +0/−70
• Satchmo/Binary/Numeric.hs +0/−19
• Satchmo/Binary/Op/Common.hs +0/−202
• Satchmo/Binary/Op/Fixed.hs +0/−113
• Satchmo/Binary/Op/Flexible.hs +0/−79
• Satchmo/Binary/Op/Times.hs +0/−87
• Satchmo/BinaryTwosComplement.hs +0/−7
• Satchmo/BinaryTwosComplement/Data.hs +0/−98
• Satchmo/BinaryTwosComplement/Numeric.hs +0/−17
• Satchmo/BinaryTwosComplement/Op/Common.hs +0/−38
• Satchmo/BinaryTwosComplement/Op/Fixed.hs +0/−94
• Satchmo/Boolean.hs +0/−14
• Satchmo/Boolean/Data.hs +0/−149
• Satchmo/Boolean/Op.hs +0/−143
• Satchmo/Code.hs +0/−54
• Satchmo/Counting.hs +0/−12
• Satchmo/Counting/Binary.hs +0/−77
• Satchmo/Counting/Direct.hs +0/−59
• Satchmo/Counting/Unary.hs +0/−59
• Satchmo/Data.hs +0/−79
• Satchmo/Integer.hs +0/−10
• Satchmo/Integer/Data.hs +0/−76
• Satchmo/Integer/Difference.hs +0/−58
• Satchmo/Integer/Op.hs +0/−176
• Satchmo/Map.hs +0/−8
• Satchmo/Map/Data.hs +0/−51
• Satchmo/MonadSAT.hs +0/−128
• Satchmo/Numeric.hs +0/−21
• Satchmo/Polynomial.hs +0/−177
• Satchmo/Polynomial/Numeric.hs +0/−84
• Satchmo/PolynomialN.hs +0/−96
• Satchmo/PolynomialSOS.hs +0/−49
• Satchmo/Relation.hs +0/−14
• Satchmo/Relation/Data.hs +0/−91
• Satchmo/Relation/Op.hs +0/−85
• Satchmo/Relation/Prop.hs +0/−131
• Satchmo/SAT.hs +0/−9
• Satchmo/SAT/External.hs +0/−179
• Satchmo/SAT/Mini.hs +0/−157
• Satchmo/SAT/Tmpfile.hs +0/−127
• Satchmo/Set.hs +0/−10
• Satchmo/Set/Data.hs +0/−69
• Satchmo/Set/Op.hs +0/−45
• Satchmo/Unary.hs +0/−10
• Satchmo/Unary/Data.hs +0/−55
• Satchmo/Unary/Op/Common.hs +0/−211
• Satchmo/Unary/Op/Fixed.hs +0/−37
• Satchmo/Unary/Op/Flexible.hs +0/−35
• examples/AIS.hs +65/−0
• examples/Hidoku.hs +65/−0
• examples/Langford.hs +59/−0
• examples/Oscillator.hs +1/−1
• examples/PP.hs +1/−1
• examples/Pigeon.hs +40/−0
• examples/Pythagoras.hs +50/−0
• examples/Ramsey.hs +1/−1
• examples/Spaceship.hs +2/−2
• examples/Sudoku.hs +1/−1
• gpl-2.0.txt +0/−339
• satchmo.cabal +58/−9
• src/Satchmo/Array.hs +39/−0
• src/Satchmo/Binary.hs +10/−0
• src/Satchmo/Binary/Data.hs +70/−0
• src/Satchmo/Binary/Numeric.hs +19/−0
• src/Satchmo/Binary/Op/Common.hs +202/−0
• src/Satchmo/Binary/Op/Fixed.hs +113/−0
• src/Satchmo/Binary/Op/Flexible.hs +79/−0
• src/Satchmo/Binary/Op/Times.hs +87/−0
• src/Satchmo/BinaryTwosComplement.hs +7/−0
• src/Satchmo/BinaryTwosComplement/Data.hs +98/−0
• src/Satchmo/BinaryTwosComplement/Numeric.hs +17/−0
• src/Satchmo/BinaryTwosComplement/Op/Common.hs +38/−0
• src/Satchmo/BinaryTwosComplement/Op/Fixed.hs +94/−0
• src/Satchmo/Boolean.hs +14/−0
• src/Satchmo/Boolean/Data.hs +149/−0
• src/Satchmo/Boolean/Op.hs +143/−0
• src/Satchmo/Code.hs +54/−0
• src/Satchmo/Counting.hs +12/−0
• src/Satchmo/Counting/Binary.hs +77/−0
• src/Satchmo/Counting/Direct.hs +59/−0
• src/Satchmo/Counting/Unary.hs +59/−0
• src/Satchmo/Data.hs +79/−0
• src/Satchmo/Integer.hs +10/−0
• src/Satchmo/Integer/Data.hs +76/−0
• src/Satchmo/Integer/Difference.hs +58/−0
• src/Satchmo/Integer/Op.hs +176/−0
• src/Satchmo/Map.hs +8/−0
• src/Satchmo/Map/Data.hs +51/−0
• src/Satchmo/MonadSAT.hs +128/−0
• src/Satchmo/Numeric.hs +21/−0
• src/Satchmo/Polynomial.hs +177/−0
• src/Satchmo/Polynomial/Numeric.hs +84/−0
• src/Satchmo/PolynomialN.hs +96/−0
• src/Satchmo/PolynomialSOS.hs +49/−0
• src/Satchmo/Relation.hs +14/−0
• src/Satchmo/Relation/Data.hs +91/−0
• src/Satchmo/Relation/Op.hs +85/−0
• src/Satchmo/Relation/Prop.hs +131/−0
• src/Satchmo/SAT.hs +9/−0
• src/Satchmo/SAT/External.hs +179/−0
• src/Satchmo/SAT/Mini.hs +157/−0
• src/Satchmo/SAT/Tmpfile.hs +127/−0
• src/Satchmo/Set.hs +10/−0
• src/Satchmo/Set/Data.hs +69/−0
• src/Satchmo/Set/Op.hs +45/−0
• src/Satchmo/Unary.hs +10/−0
• src/Satchmo/Unary/Data.hs +55/−0
• src/Satchmo/Unary/Op/Common.hs +211/−0
• src/Satchmo/Unary/Op/Fixed.hs +37/−0
• src/Satchmo/Unary/Op/Flexible.hs +35/−0

@@ -1,39 +0,0 @@-{-# language TupleSections #-}-{-# language FlexibleInstances #-}-{-# language MultiParamTypeClasses #-}--module Satchmo.Array--( Array-, array, unknown, constant-, (!), elems, indices, bounds, range, assocs-)-       -where--import Satchmo.Code as C-  -import qualified Data.Array as A-import Control.Applicative-import Control.Monad ( forM )--newtype Array i v = Array (A.Array i v)--unknown bnd build = -  Array <$> A.array bnd <$> forM (A.range bnd) ( \ i ->-    (i,) <$> build )--constant a = Array a--instance (Functor m, A.Ix i, Decode m c d )-         => Decode m (Array i c) (A.Array i d) where-  decode (Array a) = A.array (A.bounds a) <$> -    forM (A.assocs a) ( \(k,v) -> (k,) <$> decode v )--Array a ! i = a A.! i-elems (Array a) = A.elems a-indices (Array a) = A.indices a-bounds (Array a) = A.bounds a-range bnd = A.range bnd-assocs (Array a) = A.assocs a-array bnd kvs = Array (A.array bnd kvs)

@@ -1,10 +0,0 @@-{-# language MultiParamTypeClasses #-}--module Satchmo.Binary --( module Satchmo.Binary.Op.Flexible-)--where--import Satchmo.Binary.Op.Flexible

@@ -1,70 +0,0 @@-{-# language MultiParamTypeClasses, FlexibleInstances, FlexibleContexts, UndecidableInstances #-}---module Satchmo.Binary.Data--( Number, bits, make-, width, number, constant, constantWidth-, fromBinary, toBinary, toBinaryWidth-)--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 Satchmo.Counting--data Number = Number -            { bits :: [ Boolean ] -- lsb first-            }--instance (Monad m, 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---- | declare a number variable (bit width)-number :: MonadSAT m => Int -> m Number-number w = do-    xs <- sequence $ replicate w boolean-    return $ make xs--make :: [ Boolean ] -> Number-make xs = Number-           { bits = xs-           }--fromBinary :: [ Bool ] -> Integer-fromBinary xs = foldr ( \ x y -> 2*y + if x then 1 else 0 ) 0 xs--toBinary :: Integer -> [ Bool ]-toBinary 0 = []-toBinary n  = -    let (d,m) = divMod n 2-    in  toEnum ( fromIntegral m ) : toBinary d---- | @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

@@ -1,19 +0,0 @@-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 

@@ -1,202 +0,0 @@-module Satchmo.Binary.Op.Common--( iszero-, equals, lt, le, ge, eq, gt-, full_adder, half_adder-, select-, max, min, maximum-)--where--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, assertOr, assert, boolean)-import qualified  Satchmo.Boolean as B-import Satchmo.Binary.Data (Number, number, make, bits, width)--import Control.Monad ( forM, foldM )---- import Satchmo.Counting--import Control.Monad ( forM )--iszero :: (MonadSAT m) =>  Number -> m Boolean-iszero a = equals a $ make []--equals :: (MonadSAT m) =>  Number -> Number -> m Boolean-equals a b = do-    -- 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' [] [] = 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]-lt x y = do (l,e) <- compare x y ; return l-ge x y = le y x-gt x y = lt y x-eq = equals--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 )--compare' :: (MonadSAT m) => Booleans -         -> Booleans -         -> m ( Boolean, Boolean ) -- ^ (less, equals)--compare' [] [] = do -    f <- B.constant False -    t <- B.constant True -    return ( f, t )-compare' (x:xs) (y:ys) = do-    l <- and [ not x, y ]-    e <- fmap not $ xor [ x, y ]-    ( ll, ee ) <- compare' xs ys-    lee <- and [l,ee]-    l' <- or [ ll, lee ]-    e' <- and [ e, ee ]-    return ( l', e' )-compare' xs [] = do-    x <- or xs-    never <- B.constant False-    return ( never, not x )-compare' [] ys = do-    y <- or ys-    return ( y, not y )--full_adder :: (MonadSAT m) -           => Boolean -> Boolean -> Boolean-           -> m ( Boolean , Boolean ) -- ^ (result, carry)-full_adder = full_adder_0--full_adder_1 p1 p2 p3 = do-    p4 <- boolean ; p5 <- boolean-    assert [not p1, not p2, p5]-    assert [not p1, not p3, p5]-    assert [not p1, p4, p5]-    assert [p1, p2, not p5]-    assert [p1, p3, not p5]-    assert [p1, not p4, not p5]-    assert [not p2, not p3, p5]-    assert [not p2, p4, p5]-    assert [p2, p3, not p5]-    assert [p2, not p4, not p5]-    assert [not p3, p4, p5]-    assert [p3, not p4, not p5]-    assert [not p1, not p2, not p3, p4]-    assert [not p1, not p2, p3, not p4]-    assert [not p1, p2, not p3, not p4]-    assert [not p1, p2, p3, p4]-    assert [p1, not p2, not p3, not p4]-    assert [p1, not p2, p3, p4]-    assert [p1, p2, not p3, p4]-    assert [p1, p2, p3, not p4]-    return ( p4, p5 )-       -full_adder_0 p1 p2 p3 = do-    p4 <- boolean ; p5 <- boolean-    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-    let s x y z = sum $ map fromEnum [x,y,z]-    r <- fun3 ( \ x y z -> odd $ s x y z ) a b c-    d <- fun3 ( \ x y z -> 1   < s x y z ) a b c-    return ( r, d )--full_adder_from_half a b c = do-    (p,q) <- half_adder_plain a b-    (r,s) <- half_adder_plain p c-    qs <- or [q,s]-    return ( r, qs )--half_adder :: (MonadSAT m) -           => Boolean -> Boolean -           -> m ( Boolean, Boolean ) -- ^ (result, carry)-half_adder = half_adder_plain--half_adder_1 p1 p2 = do-    p3 <- boolean ; p4 <- boolean-    assert [p1, not p4]-    assert [p2, not p4]-    assert [not p3, not p4]-    assert [not p1, not p2, not p3]-    assert [not p1, not p2, p4]-    assert [not p1, p2, p3]-    assert [not p1, p3, p4]-    assert [p1, not p2, p3]-    assert [p1, p2, not p3]-    assert [not p2, p3, p4]-    return (p3,p4)--half_adder_0 p1 p2 = do-    p3 <- boolean ; p4 <- boolean-    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-    let s x y = sum $ map fromEnum [x,y]-    r <- fun2 ( \ x y -> odd $ s x y ) a b-    -- d <- fun2 ( \ x y -> 1   < s x y ) a b-    d <- and [ a, b ] -- makes three clauses (not four)-    return ( r, d )

@@ -1,113 +0,0 @@-{-# 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.Binary.Op.Fixed--( restricted-, add, times, dot_product, dot_product'-, module Satchmo.Binary.Data-, module Satchmo.Binary.Op.Common-, restrictedTimes-)--where--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---- | give only lower k bits, upper bits must be zero,--- (else unsatisfiable)-restricted :: (MonadSAT m) => Int -> Number -> m Number-restricted w a = do-    let ( low, high ) = splitAt w $ bits a-    sequence $ do x <- high ; return $ assertOr [ not x ]-    return $ make low---- | result bit width is max of argument bit widths.--- if overflow occurs, then formula is unsatisfiable.-add :: (MonadSAT m) => Number -> Number -> m Number-add a b = do-    false <- Satchmo.Boolean.constant False-    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 $ assertOr [ not p ]-        return []-    ( [] , [] ) -> return [ c ]-    ( [], y : ys) -> do-        (r,d) <- half_adder c y-        rest <- add_with_carry (w-1) d [] ys-        return $ r : rest-    ( x : xs, [] ) -> add_with_carry w c yys xxs-    (x : xs, y:ys) -> do-        (r,d) <- full_adder c x y-        rest <- add_with_carry (w-1) d xs ys-        return $ r : rest---- | result bit width is at most max of argument bit widths.--- if overflow occurs, then formula is unsatisfiable.-times :: (MonadSAT m) => Number -> Number -> m Number-times a b = do -    let w = Prelude.max ( width a ) ( width b ) -    T.times (Just w) a b--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    ----- 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---- 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)---- 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-

@@ -1,79 +0,0 @@-{-# language MultiParamTypeClasses, PatternGuards #-}---- | operations from this module cannot overflow.--- instead they increase the bit width.--module Satchmo.Binary.Op.Flexible--( add, times, dot_product-, add_with_carry, times1, shift-, module Satchmo.Binary.Data-, module Satchmo.Binary.Op.Common-)--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 Satchmo.Binary.Op.Times as T-import Satchmo.Counting.Unary--import qualified Data.Map as M--add :: (MonadSAT m) => Number -> Number -> m Number-add a b = do-    false <- Satchmo.Boolean.constant False-    ( zs, carry ) <- -        add_with_carry false (bits a) (bits b)-    return $ make $ zs ++ [carry]--add_with_carry :: (MonadSAT m) => Boolean -               -> Booleans -> Booleans-               -> m ( Booleans, Boolean )-add_with_carry cin [] [] = return ( [], cin )-add_with_carry cin (x:xs) [] = do-    (z, c) <- half_adder cin x-    ( zs, cout ) <- add_with_carry c xs []-    return ( z : zs, cout )-add_with_carry cin [] (y:ys) = do-    add_with_carry cin (y:ys) []-add_with_carry cin (x:xs ) (y:ys) = do-    (z, c) <- full_adder cin x y-    ( zs, cout ) <- add_with_carry c xs ys-    return ( z : zs, cout )--times :: (MonadSAT m) => Number -> Number -> m Number-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-plain_times a b | [x] <- bits a = times1 x b-plain_times a b | [y] <- bits b = times1 y a-plain_times a b | x:xs <- bits a = do-    xys  <- times1 x b-    xsys <- plain_times (make xs) b-    zs <- shift xsys-    add xys zs---- | multiply by 2-shift :: (MonadSAT m) => Number -> m Number-shift a = do-    false <- Satchmo.Boolean.constant False -    return $ make $ false : bits a--times1 :: (MonadSAT m) => Boolean -> Number -> m Number-times1 x b = do-    zs <- mapM ( \ y -> and [x,y] ) $ bits b-    return $ make zs--

@@ -1,87 +0,0 @@-module Satchmo.Binary.Op.Times--( times, dot_product-, Overflow (..), 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 )-import Control.Applicative--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 Refuse bound (bits x) (bits y)-    make <$> export Refuse bound ( concat cs )--data Overflow = Ignore | Refuse--times :: (MonadSAT m) -             => Maybe Int-             -> Number -> Number -> m Number-times bound a b =-  make <$> times' Refuse bound (bits a) (bits b)--times' over bound a b = do-    kzs <- product_components over bound a b-    export over bound kzs--product_components over bound a b = sequence $ do-    ( i , x ) <- zip [ 0 .. ] a-    ( j , y ) <- zip [ 0 .. ] b        -    return $ do-        z <- and [ x, y ]-        if ( case bound of Nothing -> False ; Just b -> i+j >= b )-             then do-                case over of-                  Ignore -> return ()-                  Refuse -> assert [ not z ]-                return ( i+j , [ ] )-             else do-                return ( i+j , [z] ) --export over bound kzs = do -    m <- reduce over bound $ M.fromListWith (++) kzs-    case M.maxViewWithKey m of-        Nothing -> return []-        Just ((k,_) , _) -> do -              return $ do -                    i <- [ 0 .. k ] -                    let { [ b ] = m M.! i }  -                    return b--reduce over 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 -> case over of-              Refuse -> assert [ not b ]-              Ignore -> return ()-            reduce over bound rest-        else case bs of-            [] -> reduce over bound rest-            [x] -> do-                m' <- reduce over bound rest-                return $ M.unionWith (error "huh") m' -                       $ M.fromList [(k,[x])] -            [x,y] -> do-                (r,c) <- half_adder x y-                reduce over bound $ M.unionWith (++) rest-                       $ M.fromList [ (k,[r]), (k+1, [c]) ] -            (x:y:z:more) -> do-                (r,c) <- full_adder x y z-                reduce over bound $ M.unionWith (++) rest-                       $ M.fromList [ (k, more ++ [r]), (k+1, [c]) ] --

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

@@ -1,98 +0,0 @@-{-# 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 (Monad m, 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

@@ -1,17 +0,0 @@-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 

@@ -1,38 +0,0 @@-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

@@ -1,94 +0,0 @@-{-# 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,14 +0,0 @@-module Satchmo.Boolean--( MonadSAT(..)-, module Satchmo.Boolean.Data-, module Satchmo.Boolean.Op-)--where--import qualified Prelude--import Satchmo.MonadSAT-import Satchmo.Boolean.Data-import Satchmo.Boolean.Op

@@ -1,149 +0,0 @@-{-# language MultiParamTypeClasses #-}-{-# language TypeSynonymInstances #-}-{-# language FlexibleInstances #-}-{-# language NoMonomorphismRestriction #-}-{-# language TemplateHaskell #-}-{-# language DeriveGeneric #-}--module Satchmo.Boolean.Data--( Boolean(..), Booleans, encode-, boolean, exists, forall-, constant-, not, monadic-, assertOr -- , assertOrW-, assertAnd -- , assertAndW-, assert -- for legacy code-)--where--import Prelude hiding ( not )-import qualified Prelude--import qualified Satchmo.Code as C--import Satchmo.Data-import Satchmo.MonadSAT--import Data.Function.Memoize-import Data.Array-import Data.Maybe ( fromJust )-import Data.List ( partition )--import Control.Monad.Reader--import GHC.Generics (Generic)-import Data.Hashable--data Boolean = Boolean { encode :: ! Literal }-     | Constant { value :: ! Bool }-  deriving (Eq, Ord, Show, Generic)--instance Hashable Boolean--$(deriveMemoizable ''Boolean)--{----- FIXME: @Pepe: what is the reason for these instances?--instance Eq Boolean where-  b1@Boolean{}  == b2@Boolean{}  = encode b1 == encode b2-  b1@Constant{} == b2@Constant{} = value  b1 == value  b2-  _ == _ = False--instance Ord Boolean where-  b1@Boolean{}  `compare` b2@Boolean{}  = encode b1 `compare` encode b2-  b1@Constant{} `compare` b2@Constant{} = value  b1 `compare` value  b2-  Boolean{} `compare` Constant{} = GT-  Constant{} `compare` Boolean{} = LT--instance Enum Boolean where-  fromEnum (Constant True)  = -1-  fromEnum (Constant False) = 0-  fromEnum (Boolean (Literal lit) dec) = lit--  toEnum 0    = Constant False-  toEnum (-1) = Constant True-  toEnum l    = let x = literal l in Boolean x (asks $ \fm -> fromJust (M.lookup x fm))---}--type Booleans = [ Boolean ]--isConstant :: Boolean -> Bool-isConstant ( Constant {} ) = True-isConstant _ = False---boolean :: MonadSAT m => m ( Boolean )-boolean = exists--exists :: MonadSAT m => m ( Boolean )-exists = do-    x <- fresh-    return $ Boolean -           { encode = x-{-                      -           , decode = asks $ \ fm -> -                      ( positive x == )-                    $ fromJust-                    $ M.lookup ( variable x ) fm--}-           }--forall :: MonadSAT m => m ( Boolean )-forall = do-    x <- fresh_forall-    return $ Boolean -           { encode = x---           , decode = error "Boolean.forall cannot be decoded"-           }--constant :: MonadSAT m => Bool -> m (Boolean)-constant v = do-    return $ Constant { value = v } -{-# INLINABLE constant #-}---- not :: Boolean -> Boolean-not b = case b of-    Boolean {} -> Boolean -      { encode = nicht $ encode b-      -- , decode = do x <- decode b ; return $ Prelude.not x-      }-    Constant {} -> Constant { value = Prelude.not $ value b }-{-# INLINABLE not #-}---- assertOr, assertAnd :: MonadSAT m => [ Boolean (Literal m ) ] -> m ()-assertOr = assert--assert :: MonadSAT m => [ Boolean ] -> m ()-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 #-}---- 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 )-monadic f ms = do-    xs <- sequence ms-    f xs-

@@ -1,143 +0,0 @@-module Satchmo.Boolean.Op--( constant-, and, or, xor, xor2, equals2, equals, implies, (||), (&&)-, fun2, fun3-, ifThenElse, ifThenElseM-, assert_fun2, assert_fun3-, monadic-)--where--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 Control.Monad ( foldM, when )--and :: MonadSAT m => [ Boolean ] -> m Boolean--and [] = constant True-and [x]= return x-and xs = do-    y <- boolean-    sequence_ $ do-        x <- xs-        return $ assertOr [ not y, x ]-    assertOr $ y : map not xs-    return y--or :: MonadSAT m => [ Boolean ] -> m Boolean-or [] = constant False-or [x]= return x-or xs = do-    y <- and $ map not xs-    return $ not y--x && y = and [x,y]-x || y = or [x,y]--xor :: MonadSAT m => [ Boolean ] -> m Boolean-xor [] = constant False-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-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 $ 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-fun3 f x y z = do-    r <- boolean-    sequence_ $ do-        a <- [ False, True ]-        b <- [ False, True ]-        c <- [ False, True ]-        let pack flag var = if flag then not var else var-        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-xor2 = fun2 (/=)--- xor2 = xor2_orig---- for historic reasons:-xor2_orig :: MonadSAT m => Boolean -> Boolean -> m Boolean-xor2_orig x y = do-    a <- and [ x, not y ]-    b <- and [ not x, y ]-    or [ a, b ]-

@@ -1,54 +0,0 @@-{-# language MultiParamTypeClasses, FunctionalDependencies #-}-{-# language FlexibleInstances, UndecidableInstances, FlexibleContexts #-}--module Satchmo.Code --( Decode (..)--- , Decoder-)--where--import Satchmo.Data--import Data.Array--import Control.Monad.Reader-import qualified Data.Map as M--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--instance Monad m => Decode m () () where-    decode () = return ()--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 m c a ) => Decode m [c] [a] where-    decode = mapM decode --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 m c a) => Decode m ( Array i c) ( Array i a ) where-    decode x = do-        pairs <- sequence $ do-            (i,e) <- assocs x-            return $ do-                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

@@ -1,12 +0,0 @@--- | Re-exports @Satchmo.Binary.Counting@--- because that implementation seems best overall.--module Satchmo.Counting--( module Satchmo.Counting.Binary )--where--import Satchmo.Counting.Binary--

@@ -1,77 +0,0 @@-module Satchmo.Counting.Binary--( atleast-, atmost-, exactly-, count-)--where--import Prelude hiding ( and, or, not )--import Satchmo.Boolean-import Satchmo.Binary--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 #-}-{-# specialize inline count :: [ Boolean] -> SAT Number #-}--count :: MonadSAT m => [ Boolean ] -> m Number-count bits-  = collect (Satchmo.Binary.constant 0) Satchmo.Binary.add-  $ map ( \ bit -> Satchmo.Binary.make [bit] )-  $ bits--data NumCarries =-  NumCarries { num:: Number,carries:: [Boolean]}--zro = NumCarries {num=make [], carries=[] }-mke 0 b = NumCarries {num=make[],carries=[b]}-mke w b | w > 0 = NumCarries {num=make[b],carries=[]}-pls w x y = do-  z <- Satchmo.Binary.add (num x) (num y)-  let (pre,post) = splitAt w $ bits z-  return $ NumCarries-     { num = make pre-     , carries = post ++ carries x ++ carries y-     }--count_and_carry width bits -  = collect (return zro) (pls width) $ map (mke width) bits-  -collect :: Monad m => m a -> (a -> a -> m a) -> [a] -> m a-collect z b xs = case xs of-  [] -> z-  [x] -> return x-  (x:y:zs) -> b x y >>= \ c -> collect z b (zs ++ [c])--atleast :: MonadSAT m => Int -> [ Boolean ] -> m Boolean-atleast k xs = common True ge k xs--atmost :: MonadSAT m => Int -> [ Boolean ] -> m Boolean-atmost k xs = common False le k xs-        -exactly :: MonadSAT m => Int -> [ Boolean ] -> m Boolean-exactly k xs = common False eq k xs--common :: MonadSAT m-       => Bool -       -> (Number -> Number -> m Boolean)-       -> Int -> [ Boolean ] -> m Boolean-common may_overflow cmp k xs = do-  let bk = Satchmo.Binary.toBinary $ fromIntegral k-  NumCarries { num=n,carries=cs} <--    count_and_carry (length bk) xs-  goal <- Satchmo.Binary.constant $ fromIntegral k-  ok <- cmp n goal -  if may_overflow-    then or $ ok : cs-    else and $ ok : map not cs-         -    --

@@ -1,59 +0,0 @@--- | functions in this module have no extra variables but exponential cost.--module Satchmo.Counting.Direct --( atleast-, atmost-, exactly-, assert_implies_atmost-, assert_implies_exactly-)--where--import Satchmo.Boolean ( Boolean, MonadSAT )  -import qualified Satchmo.Boolean as B--import Control.Monad ( forM, forM_ )--select :: Int -> [a] -> [[a]]-select 0 xs = [[]]-select k [] = []-select k (x:xs) =-  select k xs ++ (map (x:) $ select (k-1) xs)--atleast :: MonadSAT m => Int -> [ Boolean ] -> m Boolean-atleast k xs = B.or =<< forM (select k xs) B.and--atmost :: MonadSAT m => Int -> [ Boolean ] -> m Boolean-atmost k xs = atleast (length xs - k) $ map B.not xs--exactly :: MonadSAT m => Int -> [ Boolean ] -> m Boolean-exactly k xs = do-  this <- atleast k xs-  that <- atmost k xs-  this B.&& that---- | (and ys) implies (atmost k xs)-assert_implies_atmost ys k xs | k >= 0 = -  forM_ (select (k+1) xs) $ \ sub -> do-    B.assert $ map B.not ys ++ map B.not sub-assert_implies_atmost ys k _ =-  B.assert $ map B.not ys--assert_implies_atleast ys k xs =-  assert_implies_atmost ys (length xs - k) (map B.not xs)---- | asserting that  (and ys)  implies  (exactly k xs)-assert_implies_exactly ys k xs = do-  assert_implies_atmost ys k xs-  assert_implies_atleast ys k xs---- | (atmost k xs) implies (or ys)-assert_atmost_implies xs k ys =-  assert_implies_atleast (map B.not ys) (k+1) xs--assert_atleast_implies xs k ys =-  assert_implies_atmost (map B.not ys) (k+1) xs--  

@@ -1,59 +0,0 @@-module Satchmo.Counting.Unary--( atleast-, atmost-, exactly-)--where--import Prelude hiding ( and, or, not )--import Satchmo.Boolean--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 = fmap not $ atmost (k-1) xs-        --atmost_block :: MonadSAT m => Int -> [ Boolean ] -> m [ Boolean ]-atmost_block k [] = do-    t <- constant $ True-    return $ replicate (k+1) t-atmost_block k (x:xs) = do-    cs <- atmost_block k xs-    f <- constant False-    sequence $ do-        (p,q) <- zip cs ( f : cs )-        return $ do-            fun3  ( \ x p q -> if x then q else p ) x p q--atmost :: MonadSAT m => Int -> [ Boolean ] -> m Boolean-atmost k xs = do-    cs <- atmost_block k xs-    return $ cs !! k-        --exactly_block :: MonadSAT m => Int -> [ Boolean ] -> m [ Boolean ]-exactly_block k [] = do-    t <- constant True-    f <- constant False-    return $ t : replicate k f-exactly_block k (x:xs) = do-    f <- constant False-    cs <- exactly_block k xs-    sequence $ do-        (p,q) <- zip cs ( f : cs )-        return $ do-            fun3 ( \ x p q -> if x then q else p ) x p q--exactly :: MonadSAT m => Int -> [ Boolean ] -> m Boolean-exactly k xs = do-    cs <- exactly_block k xs-    return $ cs !! k-        

@@ -1,79 +0,0 @@--- | this module just defines types for formulas,--- it is not meant to contain efficient implementations--- for formula manipulation.--{-# language TypeFamilies #-}-{-# language GeneralizedNewtypeDeriving #-}-{-# language TemplateHaskell #-}-{-# language DeriveGeneric #-}--module Satchmo.Data --( CNF, cnf, clauses, size-, Clause, clause, literals-, Literal, literal, nicht, positive, variable-, Variable -)--where--import Prelude hiding ( foldr, filter )-import qualified Prelude-  -import qualified Data.Set as S-import qualified Data.Map as M-import qualified Data.Foldable as F-import Data.Monoid-import Data.List ( nub )-import Data.Function.Memoize--import GHC.Generics (Generic)-import Data.Hashable---- * variables and literals--type Variable = Int--data Literal =-     Literal { variable :: ! Variable-             , positive :: ! Bool-             }-     deriving ( Eq, Ord, Generic )--instance Hashable Literal--$(deriveMemoizable ''Literal)--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 }--nicht :: Literal -> Literal -nicht x = x { positive = not $ positive x }---- * clauses--newtype Clause = Clause { literals :: [Literal] }-   deriving ( Eq, Ord )--instance Show ( Clause ) where-  show c = unwords ( map show (literals c) ++ [ "0" ] )--clause ::  [ Literal ] -> Clause -clause ls = Clause ls ---- * formulas--newtype CNF  = CNF { clauses :: [ Clause ] }--size (CNF s) = length s-                   -instance Show CNF  where-    show cnf = unlines $ map show $ clauses cnf--cnf :: [ Clause ] -> CNF -cnf cs = CNF cs-

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

@@ -1,76 +0,0 @@-{-# language MultiParamTypeClasses, FlexibleInstances, FlexibleContexts, UndecidableInstances #-}--module Satchmo.Integer.Data --( Number, make, number-, constant, decode-, bits, width, sign-)--where--import Prelude hiding ( and, or, not, (&&), (||) )-import qualified Prelude --import qualified Satchmo.Code as C--import Satchmo.Boolean hiding ( constant )-import qualified  Satchmo.Boolean as B--import Satchmo.Counting-import Control.Monad--data Number = Number -            { bits :: [ Boolean ] -- ^ lsb first,-	         -- using two's complement-            }--instance (Monad m, 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--sign :: Number -> Boolean-sign n = case bits n of-  [] -> error "Satchmo.Integer.Data:sign no bits"-  bs -> last bs---- | declare a number variable (bit width)-number :: MonadSAT m => Int -> m Number-number w = do-    xs <- sequence $ replicate w boolean-    return $ make xs--make :: [ Boolean ] -> Number-make xs = Number-           { bits = xs-           }--fromBinary :: [ Bool ] -> Integer-fromBinary xs = foldr ( \ x y -> 2*y + if x then 1 else 0 ) 0 xs--toBinary :: Integer -> [ Bool ]-toBinary 0 = []-toBinary n  = -    let (d,m) = divMod n 2-    in  toEnum ( fromIntegral m ) : toBinary d---- | declare a number constant -constant :: MonadSAT m -	 => Int -- ^ bit width-	 -> Integer -- ^ value-	 -> m Number-constant w n = do-    xs <- if 0 <= n Prelude.&& n < 2^(w-1)-          then mapM B.constant $ toBinary n-	  else if negate ( 2^(w-1)) <= n Prelude.&& n < 0-	  then mapM B.constant $ toBinary (n + 2^w)-	  else error "Satchmo.Integer.Data.constant"-    z <- B.constant False-    return $ make $ take w $ xs ++ repeat z--decode w n = do-  bs <- forM (bits n) C.decode-  return $ fromBinary bs-         - if last bs then 2^w else 0

@@ -1,58 +0,0 @@-{-# 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 }

@@ -1,176 +0,0 @@--- | all operations have fixed bit length,--- and are unsatisfiable in case of overflows.--module Satchmo.Integer.Op --( negate, add, sub, times-, gt, ge, eq -)--where--import Satchmo.Integer.Data-import Prelude hiding ( and, or, not, negate )-import Satchmo.Boolean hiding ( constant )-import qualified  Satchmo.Boolean as B--import qualified Satchmo.Binary.Op.Common as C-import qualified Satchmo.Binary.Op.Flexible as F-import qualified Satchmo.Binary.Op.Times as T--import Control.Monad ( forM, when )---- | negate. Unsatisfiable if value is lowest negatve.-negate :: MonadSAT m -       => Number -> m Number-negate n = do-    let ys = map B.not $ bits n -    o <- B.constant True-    ( zs, c ) <- increment ys o-    assertOr [ last $ ys, B.not $ last zs ]-    return $ make zs--increment [] z = return ( [], z )-increment (y:ys) z = do-    ( r, d ) <- C.half_adder y z-    ( rs, c ) <- increment ys d-    return ( r : rs, c )--add :: MonadSAT m -    => Number -> Number -    -> m Number-add a0 b0 = do--    let w = max (width a0) (width b0)-        a = sextn w a0 ; b = sextn w b0--    cin <- B.constant False-    ( zs, cout ) <- -        F.add_with_carry cin ( bits a ) ( bits b )-    let c = make zs-    sab <- B.fun2 (==) (sign a) (sign b)-    sac <- B.fun2 (==) (sign a) (sign c)-    B.assert [ B.not sab , sac ]-    return c--sub :: MonadSAT m -    => Number -> Number -    -> m Number-sub a b = do-    when ( width a /= width b ) -    	 $ error "Satchmo.Integer.Op.sub"-    c <- negate b-    add a c--sextn w n = make $ sext n w--times :: MonadSAT m -    => Number -> Number -    -> m Number-times a0 b0 = do--    let w = max (width a0) (width b0)-        a = sextn w a0 ; b = sextn w b0-        -    cs <- T.times' T.Ignore (Just w) (bits a) (bits b)--    nza <- or $ bits a ; nzb <- or $ bits b-    result_should_be_nonzero <- and [ nza, nzb ]-    result_is_nonzero <- or cs--    assert [ not result_should_be_nonzero, result_is_nonzero ]--    xs <- forM (bits a) $ \ x -> fun2 (/=) x (sign a)-    ys <- forM (bits b) $ \ y -> fun2 (/=) y (sign b)-    -    forM (zip [0..w-2] xs) $ \ (i,x) ->-      forM (zip [0..w-2] ys) $ \ (j,y) ->-        when (i+j>=w-1) $ assert [ not x, not y ]--    let c = make cs--    s <- fun2 (/=) (sign a) (sign b)-    ok <- fun2 (==) s (sign c)-    -    assert [ not result_is_nonzero, ok ]-    -    return c---- | inefficient (used double-bit width computation)-times_model :: MonadSAT m -    => Number -> Number -    -> m Number-times_model a b = do-    when ( width a /= width b ) -    	 $ error "Satchmo.Integer.Op.times"-    let w = width a-    cs <- T.times' T.Ignore (Just (2*w)) (sext a w) (sext b w)-    let (small, large) = splitAt w cs-    allone <- B.and large ; allzero <- B.and ( map B.not large )-    B.assert [ allone, allzero ]-    e <- B.fun2 (==) (last small) (head large)-    B.assert[e]-    return $ make small--sext a w = bits a ++ replicate (w - width a) (sign a)-    --------------------------------------------------------positive :: MonadSAT m-	 => Number -	 -> m Boolean-positive n = do-    ok <- or $ init $ bits n   -    and [ ok, not $ last $ bits n ]--negative :: MonadSAT m-	 => Number -	 -> m Boolean-negative n = do-    return $ last $ bits n--nonnegative :: MonadSAT m-	 => Number -	 -> m Boolean-nonnegative n = do-    return $ not $ last $ bits n--------------------------------------------------------eq :: MonadSAT m -   => Number -> Number-   -> m Boolean-eq a b = do-    when ( width a /= width b ) -    	 $ error "Satchmo.Integer.Op.eq"-    eqs <- forM ( zip ( bits a ) ( bits b ) )-    	   $ \ (x,y) -> fun2 (==) x y-    and eqs--gt :: MonadSAT m -   => Number -> Number-   -> m Boolean-gt a b = do-    diff <- and [ not $ last $ bits a, last $ bits b ]-    same <- fun2 (==) ( last $ bits a )	-     	     	       ( last $ bits b )-    g <- F.gt ( F.make $ bits a ) -      	      ( F.make $ bits b )-    monadic or [ return diff-    	       , and [ same, g ]-	       ]--ge :: MonadSAT m -   => Number -> Number-   -> m Boolean-ge a b = do-    diff <- and [ not $ last $ bits a, last $ bits b ]-    same <- fun2 (==) ( last $ bits a )	-     	     	       ( last $ bits b )-    g <- F.ge ( F.make $ bits a ) -      	      ( F.make $ bits b )-    monadic or [ return diff-    	       , and [ same, g ]-	       ]-    

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

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

@@ -1,128 +0,0 @@-{-# LANGUAGE CPP #-}-{-# LANGUAGE MultiParamTypeClasses #-}-{-# LANGUAGE FlexibleContexts, FlexibleInstances #-}-{-# LANGUAGE GeneralizedNewtypeDeriving #-}-{-# LANGUAGE TypeFamilies #-}---#if (__GLASGOW_HASKELL__ >= 708)-{-# LANGUAGE AllowAmbiguousTypes #-}-#endif--module Satchmo.MonadSAT--( MonadSAT(..), Weight-, Header (..)                -)--where--import Satchmo.Data-import Satchmo.Code--import Control.Applicative-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)-import qualified Control.Monad.State.Strict  as Strict (StateT)-import qualified Control.Monad.Writer.Strict as Strict (WriterT)-import qualified Control.Monad.RWS.Strict    as Strict (RWST)-import Data.Monoid--type Weight = Int--class ( -- MonadFix m,-        Applicative 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--data Header = -     Header { numClauses, numVars :: ! Int-            , universals :: ! [Int]-                     }-     deriving Show---- ---------------------------------------------------------- MonadSAT liftings for standard monad transformers--- ---------------------------------------------------------instance (Monad m, MonadSAT m) => MonadSAT (ListT m) where-  fresh = lift fresh-  fresh_forall = lift fresh_forall-  emit  = lift . emit-  -- emitW = (lift.) . emitW-  note = lift . note--instance (Monad m, MonadSAT m) => MonadSAT (ReaderT r m) where-  fresh = lift fresh-  fresh_forall = lift fresh_forall-  emit  = lift . emit-  -- emitW = (lift.) . emitW-  note = lift . note--instance (Monad m, MonadSAT m) => MonadSAT (Lazy.StateT s m) where-  fresh = lift fresh-  fresh_forall = lift fresh_forall-  emit  = lift . emit-  -- emitW = (lift.) . emitW-  note = lift . note--instance (Monad m, MonadSAT m, Monoid w) => MonadSAT (Lazy.RWST r w s m) where-  fresh = lift fresh-  fresh_forall = lift fresh_forall-  emit  = lift . emit-  -- emitW = (lift.) . emitW-  note = lift . note--instance (Monad m, MonadSAT m, Monoid w) => MonadSAT (Lazy.WriterT w m) where-  fresh = lift fresh-  fresh_forall = lift fresh_forall-  emit  = lift . emit-  -- emitW = (lift.) . emitW-  note = lift . note--instance (Monad m, MonadSAT m) => MonadSAT (Strict.StateT s m) where-  fresh = lift fresh-  fresh_forall = lift fresh_forall-  emit  = lift . emit-  -- emitW = (lift.) . emitW-  note = lift . note--instance (Monad m, MonadSAT m, Monoid w) => MonadSAT (Strict.RWST r w s m) where-  fresh = lift fresh-  fresh_forall = lift fresh_forall-  emit  = lift . emit-  -- emitW = (lift.) . emitW-  note = lift . note--instance (Monad m, MonadSAT m, Monoid w) => MonadSAT (Strict.WriterT w m) where-  fresh = lift fresh-  fresh_forall = lift fresh_forall-  emit  = lift . emit-  -- emitW = (lift.) . emitW-  note = lift . note--instance (Monad m, MonadSAT m) => MonadSAT (ContT s m) where-  fresh = lift fresh-  fresh_forall = lift fresh_forall-  emit  = lift . emit-  -- emitW = (lift.) . emitW-  note = lift . note-

@@ -1,21 +0,0 @@-{-# 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,177 +0,0 @@-{-# language MultiParamTypeClasses #-}-{-# language FlexibleContexts      #-}-{-# language UndecidableInstances  #-}-{-# language FlexibleInstances #-}--module Satchmo.Polynomial --( 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.MonadSAT (MonadSAT)-import Satchmo.Boolean (Boolean,monadic)-import qualified Satchmo.Boolean as B-import Satchmo.Code--import qualified Satchmo.BinaryTwosComplement.Op.Fixed as F---import qualified Satchmo.Binary.Op.Fixed as F--import Control.Monad ( forM )---- | polynomial in one variable,--- coefficients starting from degree zero-data Poly a = Poly [a] deriving ( Eq, Ord, Show )--type NumPoly = Poly F.Number--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--null :: Poly a-null = Poly []--constantTerm :: Poly a -> a-constantTerm (Poly (c:_)) = c--coefficients :: Poly a -> [a]-coefficients (Poly cs) = cs--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)--reverseBoth :: ([a],[b]) -> ([a], [b])-reverseBoth (p1, p2) = (reverse p1, reverse p2)--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--equals p1 p2 = fill p1 p2 >>= uncurry equals'--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-      

@@ -1,84 +0,0 @@-{-# 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--

@@ -1,96 +0,0 @@-{-# 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]

@@ -1,49 +0,0 @@-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,14 +0,0 @@-{-# language FlexibleInstances, MultiParamTypeClasses #-}--module Satchmo.Relation --( module Satchmo.Relation.Data-, module Satchmo.Relation.Op-, module Satchmo.Relation.Prop-)--where--import Satchmo.Relation.Data-import Satchmo.Relation.Op-import Satchmo.Relation.Prop

@@ -1,91 +0,0 @@-{-# language FlexibleInstances, MultiParamTypeClasses, FlexibleContexts #-}--module Satchmo.Relation.Data--( Relation-, relation, symmetric_relation-, build-, identity                      -, bounds, (!), indices, assocs, elems-, table-) --where--import Satchmo.Code-import Satchmo.Boolean--import Satchmo.SAT--import qualified Data.Array as A-import Data.Array ( Array, Ix )-import Data.Functor ((<$>))--import Control.Monad ( guard, forM )--newtype Relation a b = Relation ( Array (a,b) Boolean ) --relation :: ( Ix a, Ix b, MonadSAT m ) -         => ((a,b),(a,b)) -> m ( Relation a b ) -{-# specialize inline relation :: ( Ix a, Ix b) => ((a,b),(a,b)) -> SAT ( Relation a b ) #-} -relation bnd = do-    pairs <- sequence $ do -        p <- A.range bnd-        return $ do-            x <- boolean-            return ( p, x )-    return $ build bnd pairs-    -symmetric_relation bnd = do-    pairs <- sequence $ do-        (p,q) <- A.range bnd-        guard $ p <= q-        return $ do-            x <- boolean-            return $ [ ((p,q), x ) ]-                   ++ [ ((q,p), x) | p /= q ]-    return $ build bnd $ concat 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 $ A.array bnd pairs---bounds :: (Ix a, Ix b) => Relation a b -> ((a,b),(a,b))-bounds ( Relation r ) = A.bounds r--indices ( Relation r ) = A.indices r--assocs ( Relation r ) = A.assocs r--elems ( Relation r ) = A.elems r--Relation r ! p = r A.! p--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--table :: (Enum a, Ix a, Enum b, Ix b) -      => Array (a,b) Bool -> String-table r = unlines $ do-    let ((a,b),(c,d)) = A.bounds r-    x <- [ a .. c ]-    return $ unwords $ do-        y <- [ b .. d ]-        return $ if r A.! (x,y) then "*" else "."--

@@ -1,85 +0,0 @@-{-# language FlexibleInstances, MultiParamTypeClasses #-}--module Satchmo.Relation.Op--( mirror-, union-, complement-, product, power-, intersection-) --where--import Prelude hiding ( and, or, not, product )-import qualified Prelude--import Satchmo.Code-import Satchmo.Boolean-import Satchmo.Counting-import Satchmo.Relation.Data--import Control.Monad ( guard )-import Data.Ix--import Satchmo.SAT--mirror :: ( Ix a , Ix b ) => Relation a b -> Relation b a-mirror r = -    let ((a,b),(c,d)) = bounds r-    in  build ((b,a),(d,c)) $ do (x,y) <- indices r ; return ((y,x), r!(x,y))--complement :: ( Ix a , Ix b ) => Relation a b -> Relation a b-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 )-{-# specialize inline union :: ( Ix a , Ix b ) => Relation a b -> Relation a b -> SAT ( Relation a b ) #-}      -union r s = do-    pairs <- sequence $ do-        i <- indices r-        return $ do o <- or [ r!i, s!i ] ; return ( i, o )-    return $ build ( bounds r ) pairs--product :: ( Ix a , Ix b, Ix c, MonadSAT m ) -        => Relation a b -> Relation b c -> m ( Relation a c )-{-# specialize inline product ::  ( Ix a , Ix b, Ix c ) => Relation a b -> Relation b c -> SAT ( Relation a c ) #-}      -product a b = do-    let ((ao,al),(au,ar)) = bounds a-        ((bo,bl),(bu,br)) = bounds b-        bnd = ((ao,bl),(au,br))-    pairs <- sequence $ do-        i @ (x,z) <- range bnd-        return $ do-            o <- monadic or $ do-                y <- range ( al, ar )-                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 -      -> m ( Relation a b )-{-# specialize inline intersection ::  ( Ix a , Ix b ) => Relation a b -> Relation a b -> SAT ( Relation a b ) #-} -intersection r s = do-    pairs <- sequence $ do-        i <- indices r-        return $ do a <- and [ r!i, s!i ] ; return ( i, a )-    return $ build ( bounds r ) pairs--

@@ -1,131 +0,0 @@--module Satchmo.Relation.Prop--( implies-, symmetric -, transitive-, irreflexive-, reflexive-, regular-, regular_in_degree-, regular_out_degree-, max_in_degree-, min_in_degree-, max_out_degree-, min_out_degree-, empty-, complete-, disjoint-, equals-, is_function-, is_partial_function-, is_bijection-, is_permutation-)--where--import Prelude hiding ( and, or, not, product )-import qualified Prelude--import Satchmo.Code-import Satchmo.Boolean hiding (implies, equals)-import Satchmo.Counting-import Satchmo.Relation.Data-import Satchmo.Relation.Op-import qualified Satchmo.Counting as C--import Control.Monad ( guard )-import Data.Ix--import Satchmo.SAT--implies :: ( Ix a, Ix b, MonadSAT m ) -        => Relation a b -> Relation a b -> m Boolean-{-# specialize inline implies :: ( Ix a, Ix b ) => Relation a b -> Relation a b -> SAT Boolean #-}      -implies r s = monadic and $ do-    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--complete r = empty $ complement r--disjoint r s = do-    i <- intersection r s-    empty i--equals r s = do-    rs <- implies r s-    sr <- implies s r-    and [ rs, sr ]--symmetric :: ( Ix a, MonadSAT m) => Relation a a -> m Boolean-{-# specialize inline symmetric :: ( Ix a ) => Relation a a -> SAT Boolean #-}      -symmetric r = implies r ( mirror r )--irreflexive :: ( Ix a, MonadSAT m) => Relation a a -> m Boolean-{-# specialize inline irreflexive :: ( Ix a ) =>  Relation a a -> SAT Boolean #-}      -irreflexive r = and $ do-    let ((a,b),(c,d)) = bounds r-    x <- range ( a, c)-    return $ Satchmo.Boolean.not $ r ! (x,x) --reflexive :: ( Ix a, MonadSAT m) => Relation a a -> m Boolean-{-# specialize inline reflexive :: ( Ix a ) => Relation a a -> SAT Boolean #-}      -reflexive r = and $ do-    let ((a,b),(c,d)) = bounds r-    x <- range (a,c)-    return $ r ! (x,x) --regular, regular_in_degree, regular_out_degree, max_in_degree, min_in_degree, max_out_degree, min_out_degree-  :: ( Ix a, Ix b, MonadSAT m) => Int -> Relation a b -> m Boolean--regular deg r = monadic and [ regular_in_degree deg r, regular_out_degree deg r ]--regular_out_degree = out_degree_helper exactly-max_out_degree = out_degree_helper atmost-min_out_degree = out_degree_helper atleast-regular_in_degree deg r = regular_out_degree deg $ mirror r-max_in_degree deg r = max_out_degree deg $ mirror r-min_in_degree deg r = min_out_degree deg $ mirror r---out_degree_helper f deg r = monadic and $ do-    let ((a,b),(c,d)) = bounds r-    x <- range ( a , c )-    return $ f deg $ do -        y <- range (b,d)-        return $ r !(x,y)--transitive :: ( Ix a, MonadSAT m ) -           => Relation a a -> m Boolean-{-# specialize inline transitive :: ( Ix a ) => Relation a a -> SAT Boolean #-}      -transitive r = do-    r2 <- product r r-    implies r2 r---- | relation R is a function iff for each x,--- there is exactly one y such that R(x,y)-is_function :: (Ix a, Ix b, MonadSAT m)-         => Relation a b -> m Boolean-is_function r = regular_out_degree 1 r---- | relation R is a partial function iff for each x,--- there is at most one y such that R(x,y)-is_partial_function :: (Ix a, Ix b, MonadSAT m)-         => Relation a b -> m Boolean-is_partial_function r = max_out_degree 1 r---is_bijection :: (Ix a, Ix b, MonadSAT m)-         => Relation a b -> m Boolean-is_bijection r = monadic and [ is_function r , is_function (mirror r) ]--is_permutation :: (Ix a, MonadSAT m)-                  => Relation a a -> m Boolean-is_permutation r = is_bijection r

@@ -1,9 +0,0 @@-module Satchmo.SAT ( -  -- module Satchmo.SAT.BS -  -- module Satchmo.SAT.Seq-  module Satchmo.SAT.Tmpfile-) where---- import Satchmo.SAT.Seq--- import Satchmo.SAT.BS-import Satchmo.SAT.Tmpfile

@@ -1,179 +0,0 @@-{-# LANGUAGE GeneralizedNewtypeDeriving #-}-{-# LANGUAGE TypeFamilies #-}-{-# LANGUAGE MultiParamTypeClasses #-}-{-# LANGUAGE DoAndIfThenElse #-}-{-# LANGUAGE PatternSignatures #-}-{-# LANGUAGE StandaloneDeriving #-}-{-# language TemplateHaskell #-}---- | call an external solver as  separate process,--- communicate via pipes.--module Satchmo.SAT.External--( SAT-, fresh-, emit-, solve--- , solve_with_timeout-)--where--import Satchmo.Data-import Satchmo.Boolean hiding ( not )-import Satchmo.Code--- import Satchmo.MonadSAT--import Control.Monad.Reader-import Control.Monad.State--- import Control.Monad.IO.Class-import System.IO-import Control.Lens-import Control.Applicative--import Control.Concurrent-import Control.DeepSeq (rnf)--import Foreign.C--- import System.Exit (ExitCode(..))-import System.Process--- import System.IO.Error--- import System.Posix.Types-import Control.Exception-import GHC.IO.Exception ( IOErrorType(..), IOException(..) )--- import System.Posix.Signals--import qualified Control.Exception as C-import qualified Data.ByteString.Char8 as BS-import qualified Data.Map.Strict as M-import Data.List (isPrefixOf)--tracing = False-report s = when tracing $ hPutStrLn stderr s--data S = S-       { _next_variable :: ! Int -       , _solver_input :: ! Handle -       }--$(makeLenses ''S)--newtype SAT a = SAT (StateT S IO a)-  deriving (Functor, Applicative, Monad, MonadIO)--type Assignment = M.Map Int Bool--newtype Dec a = Dec (Reader Assignment a)-  deriving (Functor, Applicative, Monad)--instance MonadSAT SAT where-  fresh = SAT $ do -      n <- use next_variable-      next_variable .= succ n-      return $ literal True $ fromEnum n-  emit cl = SAT $ do-      h <- use solver_input-      let s = BS.pack $ show cl-      -- liftIO $ BS.putStrLn s-      liftIO $ BS.hPutStrLn h s --  note msg = SAT $ liftIO $ hPutStrLn stderr msg--  type Decoder SAT = Dec--instance Decode Dec Boolean Bool where-    decode b = case b of-        Constant c -> return c-        Boolean  l -> do-            v <- dv $ variable l -            return $ if positive l then v else not v--dv v = Dec $ do -  assignment <- ask-  return $ case M.lookup v assignment of-    Just v -> v-    Nothing -> error $ unwords [ "unassigned", "variable", show v ]-      --solve :: String  -- ^ command, e.g., glucose-      -> [String] -- ^ options, e.g., -model-      -> SAT (Dec a) -- ^ action that builds the formula and returns the decoder-      -> IO (Maybe a)-solve command opts (SAT action) = bracket-   ( do-     report "Satchmo.SAT.External: creating process"-     createProcess $ (proc command opts) -       { std_in = CreatePipe -       , std_out = CreatePipe-       , create_group = True -       } )-   ( \ (Just sin, Just sout, _, ph) -> do-       report "Satchmo.SAT.External: bracket closing"-       interruptProcessGroupOf ph-   )-   $ \ (Just sin, Just sout, _, ph) -> do--       dec <- newEmptyMVar--       -- fork off a thread to start consuming the output-       output  <- hGetContents sout -- lazy IO-       withForkWait (C.evaluate $ rnf output) $ \ waitOut -> -          ignoreSigPipe $ do-            report $ "S.S.External: waiter forked"--            let s0 = S { _next_variable=1, _solver_input=sin}-            report $ "S.S.External: writing output"-            Dec decoder <- evalStateT action s0-            putMVar dec decoder-            hClose sin--            waitOut-            hClose sout-            report $ "S.S.External: waiter done"--       report "Satchmo.SAT.External: start waiting"-       waitForProcess ph-       decoder <- takeMVar dec-       report "Satchmo.SAT.External: waiting done"--       let vlines = do-             line <- lines output-             guard $ isPrefixOf "v" line-             return line-       report $ show vlines-       let vs = do-             line <- vlines-             w <- tail $ words line-             return (read w :: Int)-       return $ do-         guard $ not $ null vlines-         let m = M.fromList $ do -               v <- vs ; guard $ v /= 0 ; return (abs v, v>0)-         return $ runReader decoder m---- * code from System.Process --- http://hackage.haskell.org/package/process-1.2.3.0/docs/src/System-Process.html#readProcess--- but they are not exporting withForkWait, so I have to copy it---- | Fork a thread while doing something else, but kill it if there's an--- exception.------ This is important in the cases above because we want to kill the thread--- that is holding the Handle lock, because when we clean up the process we--- try to close that handle, which could otherwise deadlock.----withForkWait :: IO () -> (IO () ->  IO a) -> IO a-withForkWait async body = do-  waitVar <- newEmptyMVar :: IO (MVar (Either SomeException ()))-  mask $ \restore -> do-    tid <- forkIO $ try (restore async) >>= putMVar waitVar-    let wait = takeMVar waitVar >>= either throwIO return-    restore (body wait) `C.onException` killThread tid--ignoreSigPipe :: IO () -> IO ()-ignoreSigPipe = C.handle $ \e -> case e of-  IOError { ioe_type  = ResourceVanished-          , ioe_errno = Just ioe }-    | Errno ioe == ePIPE -> return ()-  _ -> throwIO e

@@ -1,157 +0,0 @@-{-# LANGUAGE GeneralizedNewtypeDeriving #-}-{-# LANGUAGE TypeFamilies #-}-{-# LANGUAGE MultiParamTypeClasses #-}-{-# LANGUAGE DoAndIfThenElse #-}-{-# LANGUAGE PatternSignatures #-}-{-# LANGUAGE StandaloneDeriving #-}---module Satchmo.SAT.Mini --( SAT-, fresh-, emit-, SolveOptions(..)-, defaultSolveOptions-, solve-, solveSilently-, solveWith-, 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 Control.Monad.IO.Class-import Control.Applicative-import System.IO--import Control.Concurrent.Async--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---- | need this for hashtables-instance MonadIO SAT where-  liftIO comp = SAT $ \ s -> comp--instance Applicative SAT where-    pure = return-    a <*> b = a >>= \ f -> fmap f b--instance MonadFix SAT where-    mfix f = SAT $ \ s -> mfix ( \ a -> unSAT (f a) s )--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--newtype SolveOptions = SolveOptions {-        verboseOutput :: Bool-    }--defaultSolveOptions :: SolveOptions-defaultSolveOptions = SolveOptions {verboseOutput = True}--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 = solveWith defaultSolveOptions--solveSilently :: SAT (SAT a) -> IO (Maybe a)-solveSilently = solveWith defaultSolveOptions{verboseOutput = False}--solveWith :: SolveOptions -> SAT (SAT a) -> IO (Maybe a)-solveWith options action = withNewSolverAsync $ \ s -> do-    let printIfVerbose = when (verboseOutput options) . hPutStrLn stderr-    printIfVerbose "start producing CNF"-    SAT decoder <- unSAT action s-    v <- API.minisat_num_vars s-    c <- API.minisat_num_clauses s-    printIfVerbose $ unwords [ "CNF finished", "vars", show v, "clauses", show c ]-    printIfVerbose "starting solver"-    status <- API.limited_solve s []-    printIfVerbose $ "solver finished, result: " ++ show status-    if status == API.l_True then do-        printIfVerbose "starting decoder"    -        out <- decoder s-        printIfVerbose "decoder finished"    -        return $ Just out-    else return Nothing---withNewSolverAsync h =-  bracket newSolver API.deleteSolver $ \  s -> do-    mask_ $ withAsync (h s) $ \ a -> do-      wait a `onException` API.minisat_interrupt s--newSolver =-  do s <- API.minisat_new-     -- https://github.com/niklasso/minisat-haskell-bindings/issues/6-     -- eliminate s True -     return s

@@ -1,127 +0,0 @@-{-# LANGUAGE GeneralizedNewtypeDeriving #-}-{-# LANGUAGE TypeFamilies #-}-{-# LANGUAGE MultiParamTypeClasses #-}-{-# LANGUAGE TypeSynonymInstances, FlexibleInstances, FlexibleContexts #-}--module Satchmo.SAT.Tmpfile--( SAT, Header(..)-, fresh, fresh_forall-, emit, Weight-, sat-)--where--import Satchmo.Data hiding ( size )-import Satchmo.Code-import Satchmo.Boolean-import Satchmo.Boolean.Data-import Satchmo.MonadSAT--import Control.Exception-import Control.Monad.RWS.Strict-import Control.Applicative-import qualified  Data.Set as Set---- import qualified Data.ByteString.Lazy.Char8 as BS-import qualified Data.ByteString.Char8 as BS--import System.Directory-import System.Environment-import System.IO--import qualified Data.Map as M--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 = 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--- -----------------data Accu = Accu-          { next :: ! Int-          , universal :: [Int]-          , size :: ! Int-          , notes :: ! [ String ]-          , census :: ! ( M.Map Int Int )-          }--start :: Accu-start = Accu-      { next = 1-      , universal = []-      , size = 0-      , notes = [ "Satchmo.SAT.Tmpfile implementation" ]-      , census = M.empty          -      }--newtype SAT a = SAT {unsat::RWST Handle () Accu IO a}-    deriving (MonadState Accu, MonadReader Handle, Monad, MonadIO, Functor, Applicative, MonadFix)---sat :: SAT a -> IO (BS.ByteString, Header, a )-sat (SAT m) =- bracket-    (getTemporaryDirectory >>= (`openTempFile`  "satchmo"))-    (\(fp, h) -> removeFile fp)-    (\(fp, h) -> do-       hSetBuffering h (BlockBuffering Nothing)-       ~(a, accu, _) <- runRWST m h start-       hClose h-       -       forM ( reverse $ notes accu ) $ hPutStrLn stderr -       hPutStrLn stderr $ unlines -           [ "(clause length, frequency)"-           , show $ sortBy ( comparing ( negate . snd )) -                        $ M.toList $ census accu-           ]  -       -       let header = Header (size accu) (next accu - 1) universals-           universals = reverse $ universal accu--       bs <- BS.readFile fp-       return (bs, header, a))----tellSat x = do {h <- ask; liftIO $ BS.hPut h x}-

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

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

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

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

@@ -1,55 +0,0 @@-{-# 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 (Monad m, 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 (Monad m, 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

@@ -1,211 +0,0 @@-{-# 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 ]

@@ -1,37 +0,0 @@-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---    

@@ -1,35 +0,0 @@-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

@@ -0,0 +1,65 @@+-- | The all-interval series problem.+-- https://ianm.host.cs.st-andrews.ac.uk/CSPLib/prob/prob007/spec.html+-- As I am reading it, the task is to find one (or all) graceful labellings of  a path.+-- Finding one is easy, you can take [0, n, 1, n-1, 2, .. ]+-- for Definition and Background, see+-- http://www.combinatorics.org/ojs/index.php/eljc/article/view/DS6++{-# language ScopedTypeVariables #-}++import Prelude hiding ( not, product, and, or )+import qualified Prelude++import qualified Satchmo.Relation as R+import Satchmo.Code+import Satchmo.Boolean+import qualified Satchmo.Counting as C++import Satchmo.SAT.Mini++import Data.List (inits, tails, sort)+import qualified Data.Array as A+import Control.Monad ( guard, when, forM, foldM, forM_ )+import System.Environment+import Data.Ix ( range)+import Control.Applicative ((<$>))++main :: IO ()+main = do+    argv <- getArgs+    case argv of+      [ ] -> main_with 5+      [s] -> main_with $ read s++main_with :: Int -> IO ()+main_with n = do+    Just a <- solve $ ais n+    let  xs = do+           let ((u,l),(o,r)) = A.bounds a+           x <- A.range (u,o) +           let zs = map (\y -> a A.! (x,y) ) (A.range(l,r))+           return $ length $ takeWhile Prelude.not zs+         ds = map abs $ zipWith (-) xs $ drop 1 xs+    print xs+    print $ sort xs == [0 .. n]+    +    print ds+    print $ sort ds == [1 .. n]++ais :: Int+       -> SAT (SAT (A.Array (Int,Int) Bool))+ais n = do+  r :: R.Relation Int Int <-+    R.relation ((0,0),(n,n))+  assertM $ R.is_bijection r+  forM_ [ 1 .. n-1 ] $ \ d -> do+    occs <- concat <$> ( forM [ 0 .. n-1 ] $ \ x -> do+      forM [0 .. n-d] $ \ v -> do +        up   <- and [ r R.! (x,v), r R.! (x+1,v+d) ]+        down <- and [ r R.! (x,v+d), r R.! (x+1,v) ]+        or [up,down] )+    assertM $ C.exactly 1 occs+  return $ decode r++assertM action = do x <- action ; assert [x]+fromfunc bnd f = R.build bnd $ do i <- A.range bnd ; return (i, f i )

@@ -0,0 +1,65 @@+-- | Simple Hidoku Benchmark:+-- constraints for an empty board (no hints).+-- argument n: board is  n*n.+-- .+-- The encoding here is in a straightforward style, using "one-hot" encoding+-- for numbers, and  @Relation.Prop.is_bijection@+-- which contains @exactly-one@ constraints that use binary counters.+-- .+-- For discussion of a many more encoding options,+-- see 4.2 and 4.4 of http://nbn-resolving.de/urn:nbn:de:bsz:14-qucosa-158672++{-# language ScopedTypeVariables #-}++import Prelude hiding ( not, product )+import qualified Prelude++import qualified Satchmo.Relation as R+import Satchmo.Code+import Satchmo.Boolean++import Satchmo.SAT.Mini++import Data.List (inits, tails)+import qualified Data.Array as A+import Control.Monad ( guard, when, forM, foldM, forM_ )+import System.Environment+import Data.Ix ( range)++main :: IO ()+main = do+    argv <- getArgs+    case argv of+      [ ] -> main_with 10+      [s] -> main_with $ read s++main_with :: Int -> IO ()+main_with n = do+    Just r <- solve $ hidoku n+    printA n r++printA :: Int -> A.Array ((Int,Int),Int) Bool -> IO ()+printA n a = putStrLn $ unlines $ do+  x <- A.range (1,n)+  return $ unwords $ do +    y <- A.range (1,n)+    let zs = map (\z -> a A.! ((x,y),z)) (A.range (1,n^2))+        fill n s = replicate (n - length s) ' ' ++ s+    return $ fill 3 $ show $ succ $ length $ takeWhile Prelude.not zs++hidoku :: Int+       -> SAT (SAT (A.Array ((Int,Int),Int) Bool))+hidoku n = do+  r :: R.Relation (Int,Int) Int <-+    R.relation ( ((1,1),1),((n,n),n^2) )+  assertM $ R.is_bijection r+  forM_ (A.range (1 ,n^2 - 1)) $ \ i -> do+    forM_ (A.range ((1,1),(n,n))) $ \ p@(x,y) -> do+      assert $ not (r R.!((x,y),i)) : do+        (dx,dy) <- A.range ((-1,-1),(1,1))+        let q = (x+dx,y+dy)+        guard $ p /= q Prelude.&& A.inRange (R.bounds r) (q,i+1)+        return $ r R.! ((x+dx,y+dy),i+1)+  return $ decode r++assertM action = do x <- action ; assert [x]

@@ -0,0 +1,59 @@+-- | The Langford Sequence Problem+-- http://www.csplib.org/Problems/prob024/++{-# language ScopedTypeVariables #-}++import Prelude hiding ( not, product, and, or )+import qualified Prelude++import qualified Satchmo.Relation as R+import Satchmo.Code+import Satchmo.Boolean+import qualified Satchmo.Counting as C++import Satchmo.SAT.Mini++import Data.List (inits, tails)+import qualified Data.Array as A+import Control.Monad ( guard, when, forM, foldM, forM_ )+import System.Environment+import Data.Ix ( range)+import Data.List ( sort )++main :: IO ()+main = do+    argv <- getArgs+    case argv of+      [ ] -> main_with 12+      [s] -> main_with $ read s++main_with :: Int -> IO ()+main_with n = do+    Just a <- solve $ langford n+    let  xs = do+           let ((u,l),(o,r)) = A.bounds a+           y <- A.range (l,r) +           let zs = map (\x -> a A.! (x,y) ) (A.range(u,o))+           return $ length $ takeWhile Prelude.not zs+    print $ map (\x -> 1 + div x 2) xs++langford :: Int+       -> SAT (SAT (A.Array (Int,Int) Bool))+langford k = do+  --   r(x,y) <=> number (div x 2) is at position y+  r :: R.Relation Int Int <-+    R.relation ((2,1),(2*k+1,2*k))+  assertM $ R.is_bijection r+  false <- constant False+  forM_ [ 1 .. k ] $ \ x -> do+    forM_ [ 1 .. 2*k ] $ \ y -> do+      assert [ not $ r R.! (2*x+0 , y)+             , if x+y+1<=2*k then r R.! (2*x+1, x+y+1) else false+             ]+      assert [ not $ r R.! (2*x+1, y)+             , if y-x-1 >= 1 then r R.! (2*x, y-x-1) else false+             ]+  return $ decode r++assertM action = do x <- action ; assert [x]+fromfunc bnd f = R.build bnd $ do i <- A.range bnd ; return (i, f i )

@@ -3,7 +3,7 @@ -- example usage: ./dist/build/Life/Life 3 9 9 20 -- arguments are: period, width, height, number of life start cells -{-# language PatternSignatures #-}+{-# language ScopedTypeVariables #-} {-# language FlexibleContexts #-}  import Prelude hiding ( not, or, and )

@@ -1,7 +1,7 @@ -- | find incidence matrix of projective plane of given order -- example usage: ./dist/build/PP/PP 2 -{-# language PatternSignatures #-}+{-# language ScopedTypeVariables #-} {-# language FlexibleContexts #-}  import Prelude hiding ( not, and, or )

@@ -0,0 +1,40 @@+-- | Simple Pigoenhole benchmark:+-- put  p  pigeons in (p-1) holes.++{-# language ScopedTypeVariables #-}++import Prelude hiding ( not, product )+import qualified Prelude++import qualified Satchmo.Counting as C+import Satchmo.Code+import Satchmo.Boolean++import Satchmo.SAT.Mini++import Data.Maybe (isJust)+import Data.List (transpose)+import Control.Monad ( replicateM, forM_ )+import System.Environment++main :: IO ()+main = do+    argv <- getArgs+    case argv of+      [ ] -> main_with 10+      [s] -> main_with $ read s++main_with :: Int -> IO ()+main_with n = do+    s <- solve $ pigeon n+    print $ isJust s++pigeon :: Int -> SAT (SAT ())+pigeon p = do+  xss <- replicateM p $ replicateM (p-1) boolean+  forM_             xss $ \ xs -> assertM $ C.atleast 1 xs+  forM_ (transpose xss) $ \ ys -> assertM $ C.atmost  1 ys+  return $ decode ()++assertM action = do x <- action ; assert [x]+

@@ -0,0 +1,50 @@+-- | Find 2-colouring of [1 .. n ]+-- without Pythagorean triples.+-- This problem got recent attention via+-- http://arxiv.org/abs/1605.00723 .+-- Our encoding here is straightforward.++{-# language FlexibleContexts #-}++import qualified Satchmo.Boolean as B+import Satchmo.Code (decode)	 +import Satchmo.SAT.Mini++import Control.Monad ( guard, forM_, replicateM )+import System.Environment++main = do+  argv <- getArgs+  run $ case argv of+      [] -> 5000+      [s] -> read s++run :: Int -> IO ()+run n = do+  Just xs <- solve $ pyth n+  print $ map fromEnum (xs  :: [Bool])++pyth n = do+  xs <- replicateM n B.boolean+  forM_ (triples n) $ \ (a,b,c) -> do+    let bits = map (xs!!) $ map pred [a,b,c]+    B.assert $ map    id bits+    B.assert $ map B.not bits+  return $ decode xs++triples n = do+  c <- [1 .. n]+  solves 3 (c-1) c++-- | produce triples (a,b,c) of positive numbers+-- with  a < b  and  a^2 + b^2 == c^2.+-- increase a, decrease b, keep c.+-- inefficiencies: we could avoid all ^2.+solves :: Int -> Int -> Int -> [(Int,Int,Int)]+solves a b c =+  if a >= b then []+  else case compare (a^2 + b^2) (c^2) of+    LT ->           solves (a+1)   b   c+    EQ -> (a,b,c) : solves (a+1) (b-1) c+    GT ->           solves   a   (b-1) c+    

@@ -3,7 +3,7 @@ -- last number is size of graph, -- earlier numbers are sizes of forbidden cliques -{-# language PatternSignatures #-}+{-# language ScopedTypeVariables #-} {-# language FlexibleContexts #-}  import Prelude hiding ( not, and, or, product )

@@ -6,7 +6,7 @@ -- ./Spaceship 1 1 4 6     -- glider -- ./Spaceship 0 2 4 7 9 9 -- Conway's lightweight spaceship -{-# language PatternSignatures #-}+{-# language ScopedTypeVariables #-} {-# language FlexibleContexts #-}  import Prelude hiding ( not, or, and )@@ -81,7 +81,7 @@  moved (dx,dy) g h = do     f <- constant False-    let bnd @ ((l,o),(r,u)) = bounds g+    let bnd@((l,o),(r,u)) = bounds g         get g p = if inRange bnd p then g ! p else f     monadic and $ for ( range bnd ) $ \ (x,y) -> do         fun2 (==) ( get g (x,y) ) ( get h (x+dx, y+dy) )

@@ -3,7 +3,7 @@ -- argument n: board is (n^2)x(n^2), -- so standard Sudoku is for n=3 -{-# language PatternSignatures #-}+{-# language ScopedTypeVariables #-}  import Prelude hiding ( not, product ) import qualified Prelude

@@ -1,339 +0,0 @@-		    GNU GENERAL PUBLIC LICENSE-		       Version 2, June 1991-- Copyright (C) 1989, 1991 Free Software Foundation, Inc.,- 51 Franklin Street, Fifth Floor, Boston, MA 02110-1301 USA- Everyone is permitted to copy and distribute verbatim copies- of this license document, but changing it is not allowed.--			    Preamble--  The licenses for most software are designed to take away your-freedom to share and change it.  By contrast, the GNU General Public-License is intended to guarantee your freedom to share and change free-software--to make sure the software is free for all its users.  This-General Public License applies to most of the Free Software-Foundation's software and to any other program whose authors commit to-using it.  (Some other Free Software Foundation software is covered by-the GNU Lesser General Public License instead.)  You can apply it to-your programs, too.--  When we speak of free software, we are referring to freedom, not-price.  Our General Public Licenses are designed to make sure that you-have the freedom to distribute copies of free software (and charge for-this service if you wish), that you receive source code or can get it-if you want it, that you can change the software or use pieces of it-in new free programs; and that you know you can do these things.--  To protect your rights, we need to make restrictions that forbid-anyone to deny you these rights or to ask you to surrender the rights.-These restrictions translate to certain responsibilities for you if you-distribute copies of the software, or if you modify it.--  For example, if you distribute copies of such a program, whether-gratis or for a fee, you must give the recipients all the rights that-you have.  You must make sure that they, too, receive or can get the-source code.  And you must show them these terms so they know their-rights.--  We protect your rights with two steps: (1) copyright the software, and-(2) offer you this license which gives you legal permission to copy,-distribute and/or modify the software.--  Also, for each author's protection and ours, we want to make certain-that everyone understands that there is no warranty for this free-software.  If the software is modified by someone else and passed on, we-want its recipients to know that what they have is not the original, so-that any problems introduced by others will not reflect on the original-authors' reputations.--  Finally, any free program is threatened constantly by software-patents.  We wish to avoid the danger that redistributors of a free-program will individually obtain patent licenses, in effect making the-program proprietary.  To prevent this, we have made it clear that any-patent must be licensed for everyone's free use or not licensed at all.--  The precise terms and conditions for copying, distribution and-modification follow.--		    GNU GENERAL PUBLIC LICENSE-   TERMS AND CONDITIONS FOR COPYING, DISTRIBUTION AND MODIFICATION--  0. This License applies to any program or other work which contains-a notice placed by the copyright holder saying it may be distributed-under the terms of this General Public License.  The "Program", below,-refers to any such program or work, and a "work based on the Program"-means either the Program or any derivative work under copyright law:-that is to say, a work containing the Program or a portion of it,-either verbatim or with modifications and/or translated into another-language.  (Hereinafter, translation is included without limitation in-the term "modification".)  Each licensee is addressed as "you".--Activities other than copying, distribution and modification are not-covered by this License; they are outside its scope.  The act of-running the Program is not restricted, and the output from the Program-is covered only if its contents constitute a work based on the-Program (independent of having been made by running the Program).-Whether that is true depends on what the Program does.--  1. You may copy and distribute verbatim copies of the Program's-source code as you receive it, in any medium, provided that you-conspicuously and appropriately publish on each copy an appropriate-copyright notice and disclaimer of warranty; keep intact all the-notices that refer to this License and to the absence of any warranty;-and give any other recipients of the Program a copy of this License-along with the Program.--You may charge a fee for the physical act of transferring a copy, and-you may at your option offer warranty protection in exchange for a fee.--  2. You may modify your copy or copies of the Program or any portion-of it, thus forming a work based on the Program, and copy and-distribute such modifications or work under the terms of Section 1-above, provided that you also meet all of these conditions:--    a) You must cause the modified files to carry prominent notices-    stating that you changed the files and the date of any change.--    b) You must cause any work that you distribute or publish, that in-    whole or in part contains or is derived from the Program or any-    part thereof, to be licensed as a whole at no charge to all third-    parties under the terms of this License.--    c) If the modified program normally reads commands interactively-    when run, you must cause it, when started running for such-    interactive use in the most ordinary way, to print or display an-    announcement including an appropriate copyright notice and a-    notice that there is no warranty (or else, saying that you provide-    a warranty) and that users may redistribute the program under-    these conditions, and telling the user how to view a copy of this-    License.  (Exception: if the Program itself is interactive but-    does not normally print such an announcement, your work based on-    the Program is not required to print an announcement.)--These requirements apply to the modified work as a whole.  If-identifiable sections of that work are not derived from the Program,-and can be reasonably considered independent and separate works in-themselves, then this License, and its terms, do not apply to those-sections when you distribute them as separate works.  But when you-distribute the same sections as part of a whole which is a work based-on the Program, the distribution of the whole must be on the terms of-this License, whose permissions for other licensees extend to the-entire whole, and thus to each and every part regardless of who wrote it.--Thus, it is not the intent of this section to claim rights or contest-your rights to work written entirely by you; rather, the intent is to-exercise the right to control the distribution of derivative or-collective works based on the Program.--In addition, mere aggregation of another work not based on the Program-with the Program (or with a work based on the Program) on a volume of-a storage or distribution medium does not bring the other work under-the scope of this License.--  3. You may copy and distribute the Program (or a work based on it,-under Section 2) in object code or executable form under the terms of-Sections 1 and 2 above provided that you also do one of the following:--    a) Accompany it with the complete corresponding machine-readable-    source code, which must be distributed under the terms of Sections-    1 and 2 above on a medium customarily used for software interchange; or,--    b) Accompany it with a written offer, valid for at least three-    years, to give any third party, for a charge no more than your-    cost of physically performing source distribution, a complete-    machine-readable copy of the corresponding source code, to be-    distributed under the terms of Sections 1 and 2 above on a medium-    customarily used for software interchange; or,--    c) Accompany it with the information you received as to the offer-    to distribute corresponding source code.  (This alternative is-    allowed only for noncommercial distribution and only if you-    received the program in object code or executable form with such-    an offer, in accord with Subsection b above.)--The source code for a work means the preferred form of the work for-making modifications to it.  For an executable work, complete source-code means all the source code for all modules it contains, plus any-associated interface definition files, plus the scripts used to-control compilation and installation of the executable.  However, as a-special exception, the source code distributed need not include-anything that is normally distributed (in either source or binary-form) with the major components (compiler, kernel, and so on) of the-operating system on which the executable runs, unless that component-itself accompanies the executable.--If distribution of executable or object code is made by offering-access to copy from a designated place, then offering equivalent-access to copy the source code from the same place counts as-distribution of the source code, even though third parties are not-compelled to copy the source along with the object code.--  4. You may not copy, modify, sublicense, or distribute the Program-except as expressly provided under this License.  Any attempt-otherwise to copy, modify, sublicense or distribute the Program is-void, and will automatically terminate your rights under this License.-However, parties who have received copies, or rights, from you under-this License will not have their licenses terminated so long as such-parties remain in full compliance.--  5. You are not required to accept this License, since you have not-signed it.  However, nothing else grants you permission to modify or-distribute the Program or its derivative works.  These actions are-prohibited by law if you do not accept this License.  Therefore, by-modifying or distributing the Program (or any work based on the-Program), you indicate your acceptance of this License to do so, and-all its terms and conditions for copying, distributing or modifying-the Program or works based on it.--  6. Each time you redistribute the Program (or any work based on the-Program), the recipient automatically receives a license from the-original licensor to copy, distribute or modify the Program subject to-these terms and conditions.  You may not impose any further-restrictions on the recipients' exercise of the rights granted herein.-You are not responsible for enforcing compliance by third parties to-this License.--  7. If, as a consequence of a court judgment or allegation of patent-infringement or for any other reason (not limited to patent issues),-conditions are imposed on you (whether by court order, agreement or-otherwise) that contradict the conditions of this License, they do not-excuse you from the conditions of this License.  If you cannot-distribute so as to satisfy simultaneously your obligations under this-License and any other pertinent obligations, then as a consequence you-may not distribute the Program at all.  For example, if a patent-license would not permit royalty-free redistribution of the Program by-all those who receive copies directly or indirectly through you, then-the only way you could satisfy both it and this License would be to-refrain entirely from distribution of the Program.--If any portion of this section is held invalid or unenforceable under-any particular circumstance, the balance of the section is intended to-apply and the section as a whole is intended to apply in other-circumstances.--It is not the purpose of this section to induce you to infringe any-patents or other property right claims or to contest validity of any-such claims; this section has the sole purpose of protecting the-integrity of the free software distribution system, which is-implemented by public license practices.  Many people have made-generous contributions to the wide range of software distributed-through that system in reliance on consistent application of that-system; it is up to the author/donor to decide if he or she is willing-to distribute software through any other system and a licensee cannot-impose that choice.--This section is intended to make thoroughly clear what is believed to-be a consequence of the rest of this License.--  8. If the distribution and/or use of the Program is restricted in-certain countries either by patents or by copyrighted interfaces, the-original copyright holder who places the Program under this License-may add an explicit geographical distribution limitation excluding-those countries, so that distribution is permitted only in or among-countries not thus excluded.  In such case, this License incorporates-the limitation as if written in the body of this License.--  9. The Free Software Foundation may publish revised and/or new versions-of the General Public License from time to time.  Such new versions will-be similar in spirit to the present version, but may differ in detail to-address new problems or concerns.--Each version is given a distinguishing version number.  If the Program-specifies a version number of this License which applies to it and "any-later version", you have the option of following the terms and conditions-either of that version or of any later version published by the Free-Software Foundation.  If the Program does not specify a version number of-this License, you may choose any version ever published by the Free Software-Foundation.--  10. If you wish to incorporate parts of the Program into other free-programs whose distribution conditions are different, write to the author-to ask for permission.  For software which is copyrighted by the Free-Software Foundation, write to the Free Software Foundation; we sometimes-make exceptions for this.  Our decision will be guided by the two goals-of preserving the free status of all derivatives of our free software and-of promoting the sharing and reuse of software generally.--			    NO WARRANTY--  11. BECAUSE THE PROGRAM IS LICENSED FREE OF CHARGE, THERE IS NO WARRANTY-FOR THE PROGRAM, TO THE EXTENT PERMITTED BY APPLICABLE LAW.  EXCEPT WHEN-OTHERWISE STATED IN WRITING THE COPYRIGHT HOLDERS AND/OR OTHER PARTIES-PROVIDE THE PROGRAM "AS IS" WITHOUT WARRANTY OF ANY KIND, EITHER EXPRESSED-OR IMPLIED, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF-MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE.  THE ENTIRE RISK AS-TO THE QUALITY AND PERFORMANCE OF THE PROGRAM IS WITH YOU.  SHOULD THE-PROGRAM PROVE DEFECTIVE, YOU ASSUME THE COST OF ALL NECESSARY SERVICING,-REPAIR OR CORRECTION.--  12. IN NO EVENT UNLESS REQUIRED BY APPLICABLE LAW OR AGREED TO IN WRITING-WILL ANY COPYRIGHT HOLDER, OR ANY OTHER PARTY WHO MAY MODIFY AND/OR-REDISTRIBUTE THE PROGRAM AS PERMITTED ABOVE, BE LIABLE TO YOU FOR DAMAGES,-INCLUDING ANY GENERAL, SPECIAL, INCIDENTAL OR CONSEQUENTIAL DAMAGES ARISING-OUT OF THE USE OR INABILITY TO USE THE PROGRAM (INCLUDING BUT NOT LIMITED-TO LOSS OF DATA OR DATA BEING RENDERED INACCURATE OR LOSSES SUSTAINED BY-YOU OR THIRD PARTIES OR A FAILURE OF THE PROGRAM TO OPERATE WITH ANY OTHER-PROGRAMS), EVEN IF SUCH HOLDER OR OTHER PARTY HAS BEEN ADVISED OF THE-POSSIBILITY OF SUCH DAMAGES.--		     END OF TERMS AND CONDITIONS--	    How to Apply These Terms to Your New Programs--  If you develop a new program, and you want it to be of the greatest-possible use to the public, the best way to achieve this is to make it-free software which everyone can redistribute and change under these terms.--  To do so, attach the following notices to the program.  It is safest-to attach them to the start of each source file to most effectively-convey the exclusion of warranty; and each file should have at least-the "copyright" line and a pointer to where the full notice is found.--    <one line to give the program's name and a brief idea of what it does.>-    Copyright (C) <year>  <name of author>--    This program is free software; you can redistribute it and/or modify-    it under the terms of the GNU General Public License as published by-    the Free Software Foundation; either version 2 of the License, or-    (at your option) any later version.--    This program is distributed in the hope that it will be useful,-    but WITHOUT ANY WARRANTY; without even the implied warranty of-    MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the-    GNU General Public License for more details.--    You should have received a copy of the GNU General Public License along-    with this program; if not, write to the Free Software Foundation, Inc.,-    51 Franklin Street, Fifth Floor, Boston, MA 02110-1301 USA.--Also add information on how to contact you by electronic and paper mail.--If the program is interactive, make it output a short notice like this-when it starts in an interactive mode:--    Gnomovision version 69, Copyright (C) year name of author-    Gnomovision comes with ABSOLUTELY NO WARRANTY; for details type `show w'.-    This is free software, and you are welcome to redistribute it-    under certain conditions; type `show c' for details.--The hypothetical commands `show w' and `show c' should show the appropriate-parts of the General Public License.  Of course, the commands you use may-be called something other than `show w' and `show c'; they could even be-mouse-clicks or menu items--whatever suits your program.--You should also get your employer (if you work as a programmer) or your-school, if any, to sign a "copyright disclaimer" for the program, if-necessary.  Here is a sample; alter the names:--  Yoyodyne, Inc., hereby disclaims all copyright interest in the program-  `Gnomovision' (which makes passes at compilers) written by James Hacker.--  <signature of Ty Coon>, 1 April 1989-  Ty Coon, President of Vice--This General Public License does not permit incorporating your program into-proprietary programs.  If your program is a subroutine library, you may-consider it more useful to permit linking proprietary applications with the-library.  If this is what you want to do, use the GNU Lesser General-Public License instead of this License.

@@ -1,28 +1,33 @@+cabal-version:  3.0+ Name:           satchmo-Version:        2.9.9.3+Version:        2.9.9.4 -License:        GPL-License-file:	gpl-2.0.txt Author:         Pepe Iborra, Johannes Waldmann, Alexander Bau Maintainer:	Johannes Waldmann Homepage:       https://github.com/jwaldmann/satchmo Synopsis:       SAT encoding monad description:	Encoding for boolean and integral constraints into CNF-SAT.-		The encoder is provided as a State monad -		(hence the "mo" in "satchmo").+                The encoder is provided as a State monad+                (hence the "mo" in "satchmo").+License:        GPL-2.0-only  Category:	Logic-cabal-version:  >= 1.8 build-type: Simple++tested-with: GHC==8.10.7, GHC==9.0.2, GHC==9.2.4, GHC==9.4.2+ source-repository head     type: git     location:   https://github.com/jwaldmann/satchmo  Library+    default-language: Haskell2010     ghc-options: -funbox-strict-fields     Build-depends:  mtl, process, containers, base == 4.*,       array, bytestring, directory, minisat >= 0.1, async,-      memoize, hashable, transformers, lens, deepseq+      -- memoize,+      hashable, transformers, lens, deepseq     Exposed-modules:         Satchmo.Data         -- Satchmo.Data.Default@@ -97,8 +102,7 @@         Satchmo.Boolean.Op         Satchmo.Integer.Op         Satchmo.Boolean.Data-    hs-source-dirs:     .-    extensions: +    hs-source-dirs:     src  Test-Suite PP   Type: exitcode-stdio-1.0@@ -106,6 +110,7 @@   Main-Is: PP.hs   Build-Depends: base, array, satchmo   ghc-options: -rtsopts+  default-language: Haskell2010  Test-Suite Ramsey   Type: exitcode-stdio-1.0@@ -113,6 +118,7 @@   Main-Is: Ramsey.hs   Build-Depends: base, array, satchmo   ghc-options: -rtsopts+  default-language: Haskell2010    Test-Suite Spaceship   Type: exitcode-stdio-1.0@@ -120,6 +126,7 @@   Main-Is: Spaceship.hs   Build-Depends: base, array, satchmo   ghc-options: -rtsopts+  default-language: Haskell2010    Test-Suite Oscillator   Type: exitcode-stdio-1.0@@ -127,6 +134,7 @@   Main-Is: Oscillator.hs   Build-Depends: base, array, satchmo   ghc-options: -rtsopts+  default-language: Haskell2010  Test-Suite Moore   Type: exitcode-stdio-1.0@@ -134,6 +142,7 @@   Main-Is: Moore.hs   Build-Depends: base, array, satchmo   ghc-options: -rtsopts+  default-language: Haskell2010  Test-Suite Sudoku   Type: exitcode-stdio-1.0@@ -141,4 +150,44 @@   Main-Is: Sudoku.hs   Build-Depends: base, array, satchmo   ghc-options: -rtsopts+  default-language: Haskell2010 +Test-Suite Hidoku+  Type: exitcode-stdio-1.0+  hs-source-dirs: examples+  Main-Is: Hidoku.hs+  Build-Depends: base, array, satchmo+  ghc-options: -rtsopts+  default-language: Haskell2010++Test-Suite AIS+  Type: exitcode-stdio-1.0+  hs-source-dirs: examples+  Main-Is: AIS.hs+  Build-Depends: base, array, satchmo+  ghc-options: -rtsopts+  default-language: Haskell2010++Test-Suite Langford+  Type: exitcode-stdio-1.0+  hs-source-dirs: examples+  Main-Is: Langford.hs+  Build-Depends: base, array, satchmo+  ghc-options: -rtsopts+  default-language: Haskell2010++Test-Suite Pigeon+  Type: exitcode-stdio-1.0+  hs-source-dirs: examples+  Main-Is: Pigeon.hs+  Build-Depends: base, satchmo+  ghc-options: -rtsopts+  default-language: Haskell2010++Test-Suite Pythagoras+  Type: exitcode-stdio-1.0+  hs-source-dirs: examples+  Main-Is: Pythagoras.hs+  Build-Depends: base, satchmo+  ghc-options: -rtsopts+  default-language: Haskell2010

@@ -0,0 +1,39 @@+{-# language TupleSections #-}+{-# language FlexibleInstances #-}+{-# language MultiParamTypeClasses #-}++module Satchmo.Array++( Array+, array, unknown, constant+, (!), elems, indices, bounds, range, assocs+)+       +where++import Satchmo.Code as C+  +import qualified Data.Array as A+import Control.Applicative+import Control.Monad ( forM )++newtype Array i v = Array (A.Array i v)++unknown bnd build = +  Array <$> A.array bnd <$> forM (A.range bnd) ( \ i ->+    (i,) <$> build )++constant a = Array a++instance (Functor m, A.Ix i, Decode m c d )+         => Decode m (Array i c) (A.Array i d) where+  decode (Array a) = A.array (A.bounds a) <$> +    forM (A.assocs a) ( \(k,v) -> (k,) <$> decode v )++Array a ! i = a A.! i+elems (Array a) = A.elems a+indices (Array a) = A.indices a+bounds (Array a) = A.bounds a+range bnd = A.range bnd+assocs (Array a) = A.assocs a+array bnd kvs = Array (A.array bnd kvs)

@@ -0,0 +1,10 @@+{-# language MultiParamTypeClasses #-}++module Satchmo.Binary ++( module Satchmo.Binary.Op.Flexible+)++where++import Satchmo.Binary.Op.Flexible

@@ -0,0 +1,70 @@+{-# language MultiParamTypeClasses, FlexibleInstances, FlexibleContexts, UndecidableInstances #-}+++module Satchmo.Binary.Data++( Number, bits, make+, width, number, constant, constantWidth+, fromBinary, toBinary, toBinaryWidth+)++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 Satchmo.Counting++data Number = Number +            { bits :: [ Boolean ] -- lsb first+            }++instance (Monad m, 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++-- | declare a number variable (bit width)+number :: MonadSAT m => Int -> m Number+number w = do+    xs <- sequence $ replicate w boolean+    return $ make xs++make :: [ Boolean ] -> Number+make xs = Number+           { bits = xs+           }++fromBinary :: [ Bool ] -> Integer+fromBinary xs = foldr ( \ x y -> 2*y + if x then 1 else 0 ) 0 xs++toBinary :: Integer -> [ Bool ]+toBinary 0 = []+toBinary n  = +    let (d,m) = divMod n 2+    in  toEnum ( fromIntegral m ) : toBinary d++-- | @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 

@@ -0,0 +1,202 @@+module Satchmo.Binary.Op.Common++( iszero+, equals, lt, le, ge, eq, gt+, full_adder, half_adder+, select+, max, min, maximum+)++where++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, assertOr, assert, boolean)+import qualified  Satchmo.Boolean as B+import Satchmo.Binary.Data (Number, number, make, bits, width)++import Control.Monad ( forM, foldM )++-- import Satchmo.Counting++import Control.Monad ( forM )++iszero :: (MonadSAT m) =>  Number -> m Boolean+iszero a = equals a $ make []++equals :: (MonadSAT m) =>  Number -> Number -> m Boolean+equals a b = do+    -- 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' [] [] = 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]+lt x y = do (l,e) <- compare x y ; return l+ge x y = le y x+gt x y = lt y x+eq = equals++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 )++compare' :: (MonadSAT m) => Booleans +         -> Booleans +         -> m ( Boolean, Boolean ) -- ^ (less, equals)++compare' [] [] = do +    f <- B.constant False +    t <- B.constant True +    return ( f, t )+compare' (x:xs) (y:ys) = do+    l <- and [ not x, y ]+    e <- fmap not $ xor [ x, y ]+    ( ll, ee ) <- compare' xs ys+    lee <- and [l,ee]+    l' <- or [ ll, lee ]+    e' <- and [ e, ee ]+    return ( l', e' )+compare' xs [] = do+    x <- or xs+    never <- B.constant False+    return ( never, not x )+compare' [] ys = do+    y <- or ys+    return ( y, not y )++full_adder :: (MonadSAT m) +           => Boolean -> Boolean -> Boolean+           -> m ( Boolean , Boolean ) -- ^ (result, carry)+full_adder = full_adder_0++full_adder_1 p1 p2 p3 = do+    p4 <- boolean ; p5 <- boolean+    assert [not p1, not p2, p5]+    assert [not p1, not p3, p5]+    assert [not p1, p4, p5]+    assert [p1, p2, not p5]+    assert [p1, p3, not p5]+    assert [p1, not p4, not p5]+    assert [not p2, not p3, p5]+    assert [not p2, p4, p5]+    assert [p2, p3, not p5]+    assert [p2, not p4, not p5]+    assert [not p3, p4, p5]+    assert [p3, not p4, not p5]+    assert [not p1, not p2, not p3, p4]+    assert [not p1, not p2, p3, not p4]+    assert [not p1, p2, not p3, not p4]+    assert [not p1, p2, p3, p4]+    assert [p1, not p2, not p3, not p4]+    assert [p1, not p2, p3, p4]+    assert [p1, p2, not p3, p4]+    assert [p1, p2, p3, not p4]+    return ( p4, p5 )+       +full_adder_0 p1 p2 p3 = do+    p4 <- boolean ; p5 <- boolean+    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+    let s x y z = sum $ map fromEnum [x,y,z]+    r <- fun3 ( \ x y z -> odd $ s x y z ) a b c+    d <- fun3 ( \ x y z -> 1   < s x y z ) a b c+    return ( r, d )++full_adder_from_half a b c = do+    (p,q) <- half_adder_plain a b+    (r,s) <- half_adder_plain p c+    qs <- or [q,s]+    return ( r, qs )++half_adder :: (MonadSAT m) +           => Boolean -> Boolean +           -> m ( Boolean, Boolean ) -- ^ (result, carry)+half_adder = half_adder_plain++half_adder_1 p1 p2 = do+    p3 <- boolean ; p4 <- boolean+    assert [p1, not p4]+    assert [p2, not p4]+    assert [not p3, not p4]+    assert [not p1, not p2, not p3]+    assert [not p1, not p2, p4]+    assert [not p1, p2, p3]+    assert [not p1, p3, p4]+    assert [p1, not p2, p3]+    assert [p1, p2, not p3]+    assert [not p2, p3, p4]+    return (p3,p4)++half_adder_0 p1 p2 = do+    p3 <- boolean ; p4 <- boolean+    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+    let s x y = sum $ map fromEnum [x,y]+    r <- fun2 ( \ x y -> odd $ s x y ) a b+    -- d <- fun2 ( \ x y -> 1   < s x y ) a b+    d <- and [ a, b ] -- makes three clauses (not four)+    return ( r, d )

@@ -0,0 +1,113 @@+{-# 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.Binary.Op.Fixed++( restricted+, add, times, dot_product, dot_product'+, module Satchmo.Binary.Data+, module Satchmo.Binary.Op.Common+, restrictedTimes+)++where++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++-- | give only lower k bits, upper bits must be zero,+-- (else unsatisfiable)+restricted :: (MonadSAT m) => Int -> Number -> m Number+restricted w a = do+    let ( low, high ) = splitAt w $ bits a+    sequence $ do x <- high ; return $ assertOr [ not x ]+    return $ make low++-- | result bit width is max of argument bit widths.+-- if overflow occurs, then formula is unsatisfiable.+add :: (MonadSAT m) => Number -> Number -> m Number+add a b = do+    false <- Satchmo.Boolean.constant False+    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 $ assertOr [ not p ]+        return []+    ( [] , [] ) -> return [ c ]+    ( [], y : ys) -> do+        (r,d) <- half_adder c y+        rest <- add_with_carry (w-1) d [] ys+        return $ r : rest+    ( x : xs, [] ) -> add_with_carry w c yys xxs+    (x : xs, y:ys) -> do+        (r,d) <- full_adder c x y+        rest <- add_with_carry (w-1) d xs ys+        return $ r : rest++-- | result bit width is at most max of argument bit widths.+-- if overflow occurs, then formula is unsatisfiable.+times :: (MonadSAT m) => Number -> Number -> m Number+times a b = do +    let w = Prelude.max ( width a ) ( width b ) +    T.times (Just w) a b++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    +++-- 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++-- 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)++-- 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+

@@ -0,0 +1,79 @@+{-# language MultiParamTypeClasses, PatternGuards #-}++-- | operations from this module cannot overflow.+-- instead they increase the bit width.++module Satchmo.Binary.Op.Flexible++( add, times, dot_product+, add_with_carry, times1, shift+, module Satchmo.Binary.Data+, module Satchmo.Binary.Op.Common+)++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 Satchmo.Binary.Op.Times as T+import Satchmo.Counting.Unary++import qualified Data.Map as M++add :: (MonadSAT m) => Number -> Number -> m Number+add a b = do+    false <- Satchmo.Boolean.constant False+    ( zs, carry ) <- +        add_with_carry false (bits a) (bits b)+    return $ make $ zs ++ [carry]++add_with_carry :: (MonadSAT m) => Boolean +               -> Booleans -> Booleans+               -> m ( Booleans, Boolean )+add_with_carry cin [] [] = return ( [], cin )+add_with_carry cin (x:xs) [] = do+    (z, c) <- half_adder cin x+    ( zs, cout ) <- add_with_carry c xs []+    return ( z : zs, cout )+add_with_carry cin [] (y:ys) = do+    add_with_carry cin (y:ys) []+add_with_carry cin (x:xs ) (y:ys) = do+    (z, c) <- full_adder cin x y+    ( zs, cout ) <- add_with_carry c xs ys+    return ( z : zs, cout )++times :: (MonadSAT m) => Number -> Number -> m Number+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+plain_times a b | [x] <- bits a = times1 x b+plain_times a b | [y] <- bits b = times1 y a+plain_times a b | x:xs <- bits a = do+    xys  <- times1 x b+    xsys <- plain_times (make xs) b+    zs <- shift xsys+    add xys zs++-- | multiply by 2+shift :: (MonadSAT m) => Number -> m Number+shift a = do+    false <- Satchmo.Boolean.constant False +    return $ make $ false : bits a++times1 :: (MonadSAT m) => Boolean -> Number -> m Number+times1 x b = do+    zs <- mapM ( \ y -> and [x,y] ) $ bits b+    return $ make zs++

@@ -0,0 +1,87 @@+module Satchmo.Binary.Op.Times++( times, dot_product+, Overflow (..), 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 )+import Control.Applicative++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 Refuse bound (bits x) (bits y)+    make <$> export Refuse bound ( concat cs )++data Overflow = Ignore | Refuse++times :: (MonadSAT m) +             => Maybe Int+             -> Number -> Number -> m Number+times bound a b =+  make <$> times' Refuse bound (bits a) (bits b)++times' over bound a b = do+    kzs <- product_components over bound a b+    export over bound kzs++product_components over bound a b = sequence $ do+    ( i , x ) <- zip [ 0 .. ] a+    ( j , y ) <- zip [ 0 .. ] b        +    return $ do+        z <- and [ x, y ]+        if ( case bound of Nothing -> False ; Just b -> i+j >= b )+             then do+                case over of+                  Ignore -> return ()+                  Refuse -> assert [ not z ]+                return ( i+j , [ ] )+             else do+                return ( i+j , [z] ) ++export over bound kzs = do +    m <- reduce over bound $ M.fromListWith (++) kzs+    case M.maxViewWithKey m of+        Nothing -> return []+        Just ((k,_) , _) -> do +              return $ do +                    i <- [ 0 .. k ] +                    let { [ b ] = m M.! i }  +                    return b++reduce over 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 -> case over of+              Refuse -> assert [ not b ]+              Ignore -> return ()+            reduce over bound rest+        else case bs of+            [] -> reduce over bound rest+            [x] -> do+                m' <- reduce over bound rest+                return $ M.unionWith (error "huh") m' +                       $ M.fromList [(k,[x])] +            [x,y] -> do+                (r,c) <- half_adder x y+                reduce over bound $ M.unionWith (++) rest+                       $ M.fromList [ (k,[r]), (k+1, [c]) ] +            (x:y:z:more) -> do+                (r,c) <- full_adder x y z+                reduce over 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 (Monad m, 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

@@ -0,0 +1,14 @@+module Satchmo.Boolean++( MonadSAT(..)+, module Satchmo.Boolean.Data+, module Satchmo.Boolean.Op+)++where++import qualified Prelude++import Satchmo.MonadSAT+import Satchmo.Boolean.Data+import Satchmo.Boolean.Op

@@ -0,0 +1,149 @@+{-# language MultiParamTypeClasses #-}+{-# language TypeSynonymInstances #-}+{-# language FlexibleInstances #-}+{-# language NoMonomorphismRestriction #-}+{-# language TemplateHaskell #-}+{-# language DeriveGeneric #-}++module Satchmo.Boolean.Data++( Boolean(..), Booleans, encode+, boolean, exists, forall+, constant+, not, monadic+, assertOr -- , assertOrW+, assertAnd -- , assertAndW+, assert -- for legacy code+)++where++import Prelude hiding ( not )+import qualified Prelude++import qualified Satchmo.Code as C++import Satchmo.Data+import Satchmo.MonadSAT++-- import Data.Function.Memoize+import Data.Array+import Data.Maybe ( fromJust )+import Data.List ( partition )++import Control.Monad.Reader++import GHC.Generics (Generic)+import Data.Hashable++data Boolean = Boolean { encode :: !Literal }+     | Constant { value :: !Bool }+  deriving (Eq, Ord, Show, Generic)++instance Hashable Boolean++--  $(deriveMemoizable ''Boolean)++{-++-- FIXME: @Pepe: what is the reason for these instances?++instance Eq Boolean where+  b1@Boolean{}  == b2@Boolean{}  = encode b1 == encode b2+  b1@Constant{} == b2@Constant{} = value  b1 == value  b2+  _ == _ = False++instance Ord Boolean where+  b1@Boolean{}  `compare` b2@Boolean{}  = encode b1 `compare` encode b2+  b1@Constant{} `compare` b2@Constant{} = value  b1 `compare` value  b2+  Boolean{} `compare` Constant{} = GT+  Constant{} `compare` Boolean{} = LT++instance Enum Boolean where+  fromEnum (Constant True)  = -1+  fromEnum (Constant False) = 0+  fromEnum (Boolean (Literal lit) dec) = lit++  toEnum 0    = Constant False+  toEnum (-1) = Constant True+  toEnum l    = let x = literal l in Boolean x (asks $ \fm -> fromJust (M.lookup x fm))++-}++type Booleans = [ Boolean ]++isConstant :: Boolean -> Bool+isConstant ( Constant {} ) = True+isConstant _ = False+++boolean :: MonadSAT m => m ( Boolean )+boolean = exists++exists :: MonadSAT m => m ( Boolean )+exists = do+    x <- fresh+    return $ Boolean +           { encode = x+{-                      +           , decode = asks $ \ fm -> +                      ( positive x == )+                    $ fromJust+                    $ M.lookup ( variable x ) fm+-}+           }++forall :: MonadSAT m => m ( Boolean )+forall = do+    x <- fresh_forall+    return $ Boolean +           { encode = x+--           , decode = error "Boolean.forall cannot be decoded"+           }++constant :: MonadSAT m => Bool -> m (Boolean)+constant v = do+    return $ Constant { value = v } +{-# INLINABLE constant #-}++-- not :: Boolean -> Boolean+not b = case b of+    Boolean {} -> Boolean +      { encode = nicht $ encode b+      -- , decode = do x <- decode b ; return $ Prelude.not x+      }+    Constant {} -> Constant { value = Prelude.not $ value b }+{-# INLINABLE not #-}++-- assertOr, assertAnd :: MonadSAT m => [ Boolean (Literal m ) ] -> m ()+assertOr = assert++assert :: MonadSAT m => [ Boolean ] -> m ()+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 #-}++-- 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 )+monadic f ms = do+    xs <- sequence ms+    f xs+

@@ -0,0 +1,143 @@+module Satchmo.Boolean.Op++( constant+, and, or, xor, xor2, equals2, equals, implies, (||), (&&)+, fun2, fun3+, ifThenElse, ifThenElseM+, assert_fun2, assert_fun3+, monadic+)++where++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 Control.Monad ( foldM, when )++and :: MonadSAT m => [ Boolean ] -> m Boolean++and [] = constant True+and [x]= return x+and xs = do+    y <- boolean+    sequence_ $ do+        x <- xs+        return $ assertOr [ not y, x ]+    assertOr $ y : map not xs+    return y++or :: MonadSAT m => [ Boolean ] -> m Boolean+or [] = constant False+or [x]= return x+or xs = do+    y <- and $ map not xs+    return $ not y++x && y = and [x,y]+x || y = or [x,y]++xor :: MonadSAT m => [ Boolean ] -> m Boolean+xor [] = constant False+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+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 $ 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+fun3 f x y z = do+    r <- boolean+    sequence_ $ do+        a <- [ False, True ]+        b <- [ False, True ]+        c <- [ False, True ]+        let pack flag var = if flag then not var else var+        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+xor2 = fun2 (/=)+-- xor2 = xor2_orig++-- for historic reasons:+xor2_orig :: MonadSAT m => Boolean -> Boolean -> m Boolean+xor2_orig x y = do+    a <- and [ x, not y ]+    b <- and [ not x, y ]+    or [ a, b ]+

@@ -0,0 +1,54 @@+{-# language MultiParamTypeClasses, FunctionalDependencies #-}+{-# language FlexibleInstances, UndecidableInstances, FlexibleContexts #-}++module Satchmo.Code ++( Decode (..)+-- , Decoder+)++where++import Satchmo.Data++import Data.Array++import Control.Monad.Reader+import qualified Data.Map as M++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++instance Monad m => Decode m () () where+    decode () = return ()++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 m c a ) => Decode m [c] [a] where+    decode = mapM decode ++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 m c a) => Decode m ( Array i c) ( Array i a ) where+    decode x = do+        pairs <- sequence $ do+            (i,e) <- assocs x+            return $ do+                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

@@ -0,0 +1,12 @@+-- | Re-exports @Satchmo.Binary.Counting@+-- because that implementation seems best overall.++module Satchmo.Counting++( module Satchmo.Counting.Binary )++where++import Satchmo.Counting.Binary++

@@ -0,0 +1,77 @@+module Satchmo.Counting.Binary++( atleast+, atmost+, exactly+, count+)++where++import Prelude hiding ( and, or, not )++import Satchmo.Boolean+import Satchmo.Binary++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 #-}+{-# specialize inline count :: [ Boolean] -> SAT Number #-}++count :: MonadSAT m => [ Boolean ] -> m Number+count bits+  = collect (Satchmo.Binary.constant 0) Satchmo.Binary.add+  $ map ( \ bit -> Satchmo.Binary.make [bit] )+  $ bits++data NumCarries =+  NumCarries { num:: Number,carries:: [Boolean]}++zro = NumCarries {num=make [], carries=[] }+mke 0 b = NumCarries {num=make[],carries=[b]}+mke w b | w > 0 = NumCarries {num=make[b],carries=[]}+pls w x y = do+  z <- Satchmo.Binary.add (num x) (num y)+  let (pre,post) = splitAt w $ bits z+  return $ NumCarries+     { num = make pre+     , carries = post ++ carries x ++ carries y+     }++count_and_carry width bits +  = collect (return zro) (pls width) $ map (mke width) bits+  +collect :: Monad m => m a -> (a -> a -> m a) -> [a] -> m a+collect z b xs = case xs of+  [] -> z+  [x] -> return x+  (x:y:zs) -> b x y >>= \ c -> collect z b (zs ++ [c])++atleast :: MonadSAT m => Int -> [ Boolean ] -> m Boolean+atleast k xs = common True ge k xs++atmost :: MonadSAT m => Int -> [ Boolean ] -> m Boolean+atmost k xs = common False le k xs+        +exactly :: MonadSAT m => Int -> [ Boolean ] -> m Boolean+exactly k xs = common False eq k xs++common :: MonadSAT m+       => Bool +       -> (Number -> Number -> m Boolean)+       -> Int -> [ Boolean ] -> m Boolean+common may_overflow cmp k xs = do+  let bk = Satchmo.Binary.toBinary $ fromIntegral k+  NumCarries { num=n,carries=cs} <-+    count_and_carry (length bk) xs+  goal <- Satchmo.Binary.constant $ fromIntegral k+  ok <- cmp n goal +  if may_overflow+    then or $ ok : cs+    else and $ ok : map not cs+         +    ++

@@ -0,0 +1,59 @@+-- | functions in this module have no extra variables but exponential cost.++module Satchmo.Counting.Direct ++( atleast+, atmost+, exactly+, assert_implies_atmost+, assert_implies_exactly+)++where++import Satchmo.Boolean ( Boolean, MonadSAT )  +import qualified Satchmo.Boolean as B++import Control.Monad ( forM, forM_ )++select :: Int -> [a] -> [[a]]+select 0 xs = [[]]+select k [] = []+select k (x:xs) =+  select k xs ++ (map (x:) $ select (k-1) xs)++atleast :: MonadSAT m => Int -> [ Boolean ] -> m Boolean+atleast k xs = B.or =<< forM (select k xs) B.and++atmost :: MonadSAT m => Int -> [ Boolean ] -> m Boolean+atmost k xs = atleast (length xs - k) $ map B.not xs++exactly :: MonadSAT m => Int -> [ Boolean ] -> m Boolean+exactly k xs = do+  this <- atleast k xs+  that <- atmost k xs+  this B.&& that++-- | (and ys) implies (atmost k xs)+assert_implies_atmost ys k xs | k >= 0 = +  forM_ (select (k+1) xs) $ \ sub -> do+    B.assert $ map B.not ys ++ map B.not sub+assert_implies_atmost ys k _ =+  B.assert $ map B.not ys++assert_implies_atleast ys k xs =+  assert_implies_atmost ys (length xs - k) (map B.not xs)++-- | asserting that  (and ys)  implies  (exactly k xs)+assert_implies_exactly ys k xs = do+  assert_implies_atmost ys k xs+  assert_implies_atleast ys k xs++-- | (atmost k xs) implies (or ys)+assert_atmost_implies xs k ys =+  assert_implies_atleast (map B.not ys) (k+1) xs++assert_atleast_implies xs k ys =+  assert_implies_atmost (map B.not ys) (k+1) xs++  

@@ -0,0 +1,59 @@+module Satchmo.Counting.Unary++( atleast+, atmost+, exactly+)++where++import Prelude hiding ( and, or, not )++import Satchmo.Boolean++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 = fmap not $ atmost (k-1) xs+        ++atmost_block :: MonadSAT m => Int -> [ Boolean ] -> m [ Boolean ]+atmost_block k [] = do+    t <- constant $ True+    return $ replicate (k+1) t+atmost_block k (x:xs) = do+    cs <- atmost_block k xs+    f <- constant False+    sequence $ do+        (p,q) <- zip cs ( f : cs )+        return $ do+            fun3  ( \ x p q -> if x then q else p ) x p q++atmost :: MonadSAT m => Int -> [ Boolean ] -> m Boolean+atmost k xs = do+    cs <- atmost_block k xs+    return $ cs !! k+        ++exactly_block :: MonadSAT m => Int -> [ Boolean ] -> m [ Boolean ]+exactly_block k [] = do+    t <- constant True+    f <- constant False+    return $ t : replicate k f+exactly_block k (x:xs) = do+    f <- constant False+    cs <- exactly_block k xs+    sequence $ do+        (p,q) <- zip cs ( f : cs )+        return $ do+            fun3 ( \ x p q -> if x then q else p ) x p q++exactly :: MonadSAT m => Int -> [ Boolean ] -> m Boolean+exactly k xs = do+    cs <- exactly_block k xs+    return $ cs !! k+        

@@ -0,0 +1,79 @@+-- | this module just defines types for formulas,+-- it is not meant to contain efficient implementations+-- for formula manipulation.++{-# language TypeFamilies #-}+{-# language GeneralizedNewtypeDeriving #-}+{-# language TemplateHaskell #-}+{-# language DeriveGeneric #-}++module Satchmo.Data ++( CNF, cnf, clauses, size+, Clause, clause, literals+, Literal, literal, nicht, positive, variable+, Variable +)++where++import Prelude hiding ( foldr, filter )+import qualified Prelude+  +import qualified Data.Set as S+import qualified Data.Map as M+import qualified Data.Foldable as F+import Data.Monoid+import Data.List ( nub )+-- import Data.Function.Memoize++import GHC.Generics (Generic)+import Data.Hashable++-- * variables and literals++type Variable = Int++data Literal =+     Literal { variable :: !Variable+             , positive :: !Bool+             }+     deriving ( Eq, Ord, Generic )++instance Hashable Literal++--  $(deriveMemoizable ''Literal)++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 }++nicht :: Literal -> Literal +nicht x = x { positive = not $ positive x }++-- * clauses++newtype Clause = Clause { literals :: [Literal] }+   deriving ( Eq, Ord )++instance Show ( Clause ) where+  show c = unwords ( map show (literals c) ++ [ "0" ] )++clause ::  [ Literal ] -> Clause +clause ls = Clause ls ++-- * formulas++newtype CNF  = CNF { clauses :: [ Clause ] }++size (CNF s) = length s+                   +instance Show CNF  where+    show cnf = unlines $ map show $ clauses cnf++cnf :: [ Clause ] -> CNF +cnf cs = CNF cs+

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

@@ -0,0 +1,76 @@+{-# language MultiParamTypeClasses, FlexibleInstances, FlexibleContexts, UndecidableInstances #-}++module Satchmo.Integer.Data ++( Number, make, number+, constant, decode+, bits, width, sign+)++where++import Prelude hiding ( and, or, not, (&&), (||) )+import qualified Prelude ++import qualified Satchmo.Code as C++import Satchmo.Boolean hiding ( constant )+import qualified  Satchmo.Boolean as B++import Satchmo.Counting+import Control.Monad++data Number = Number +            { bits :: [ Boolean ] -- ^ lsb first,+	         -- using two's complement+            }++instance (Monad m, 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++sign :: Number -> Boolean+sign n = case bits n of+  [] -> error "Satchmo.Integer.Data:sign no bits"+  bs -> last bs++-- | declare a number variable (bit width)+number :: MonadSAT m => Int -> m Number+number w = do+    xs <- sequence $ replicate w boolean+    return $ make xs++make :: [ Boolean ] -> Number+make xs = Number+           { bits = xs+           }++fromBinary :: [ Bool ] -> Integer+fromBinary xs = foldr ( \ x y -> 2*y + if x then 1 else 0 ) 0 xs++toBinary :: Integer -> [ Bool ]+toBinary 0 = []+toBinary n  = +    let (d,m) = divMod n 2+    in  toEnum ( fromIntegral m ) : toBinary d++-- | declare a number constant +constant :: MonadSAT m +	 => Int -- ^ bit width+	 -> Integer -- ^ value+	 -> m Number+constant w n = do+    xs <- if 0 <= n Prelude.&& n < 2^(w-1)+          then mapM B.constant $ toBinary n+	  else if negate ( 2^(w-1)) <= n Prelude.&& n < 0+	  then mapM B.constant $ toBinary (n + 2^w)+	  else error "Satchmo.Integer.Data.constant"+    z <- B.constant False+    return $ make $ take w $ xs ++ repeat z++decode w n = do+  bs <- forM (bits n) C.decode+  return $ fromBinary bs+         - if last bs then 2^w else 0

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

@@ -0,0 +1,176 @@+-- | all operations have fixed bit length,+-- and are unsatisfiable in case of overflows.++module Satchmo.Integer.Op ++( negate, add, sub, times+, gt, ge, eq +)++where++import Satchmo.Integer.Data+import Prelude hiding ( and, or, not, negate )+import Satchmo.Boolean hiding ( constant )+import qualified  Satchmo.Boolean as B++import qualified Satchmo.Binary.Op.Common as C+import qualified Satchmo.Binary.Op.Flexible as F+import qualified Satchmo.Binary.Op.Times as T++import Control.Monad ( forM, when )++-- | negate. Unsatisfiable if value is lowest negatve.+negate :: MonadSAT m +       => Number -> m Number+negate n = do+    let ys = map B.not $ bits n +    o <- B.constant True+    ( zs, c ) <- increment ys o+    assertOr [ last $ ys, B.not $ last zs ]+    return $ make zs++increment [] z = return ( [], z )+increment (y:ys) z = do+    ( r, d ) <- C.half_adder y z+    ( rs, c ) <- increment ys d+    return ( r : rs, c )++add :: MonadSAT m +    => Number -> Number +    -> m Number+add a0 b0 = do++    let w = max (width a0) (width b0)+        a = sextn w a0 ; b = sextn w b0++    cin <- B.constant False+    ( zs, cout ) <- +        F.add_with_carry cin ( bits a ) ( bits b )+    let c = make zs+    sab <- B.fun2 (==) (sign a) (sign b)+    sac <- B.fun2 (==) (sign a) (sign c)+    B.assert [ B.not sab , sac ]+    return c++sub :: MonadSAT m +    => Number -> Number +    -> m Number+sub a b = do+    when ( width a /= width b ) +    	 $ error "Satchmo.Integer.Op.sub"+    c <- negate b+    add a c++sextn w n = make $ sext n w++times :: MonadSAT m +    => Number -> Number +    -> m Number+times a0 b0 = do++    let w = max (width a0) (width b0)+        a = sextn w a0 ; b = sextn w b0+        +    cs <- T.times' T.Ignore (Just w) (bits a) (bits b)++    nza <- or $ bits a ; nzb <- or $ bits b+    result_should_be_nonzero <- and [ nza, nzb ]+    result_is_nonzero <- or cs++    assert [ not result_should_be_nonzero, result_is_nonzero ]++    xs <- forM (bits a) $ \ x -> fun2 (/=) x (sign a)+    ys <- forM (bits b) $ \ y -> fun2 (/=) y (sign b)+    +    forM (zip [0..w-2] xs) $ \ (i,x) ->+      forM (zip [0..w-2] ys) $ \ (j,y) ->+        when (i+j>=w-1) $ assert [ not x, not y ]++    let c = make cs++    s <- fun2 (/=) (sign a) (sign b)+    ok <- fun2 (==) s (sign c)+    +    assert [ not result_is_nonzero, ok ]+    +    return c++-- | inefficient (used double-bit width computation)+times_model :: MonadSAT m +    => Number -> Number +    -> m Number+times_model a b = do+    when ( width a /= width b ) +    	 $ error "Satchmo.Integer.Op.times"+    let w = width a+    cs <- T.times' T.Ignore (Just (2*w)) (sext a w) (sext b w)+    let (small, large) = splitAt w cs+    allone <- B.and large ; allzero <- B.and ( map B.not large )+    B.assert [ allone, allzero ]+    e <- B.fun2 (==) (last small) (head large)+    B.assert[e]+    return $ make small++sext a w = bits a ++ replicate (w - width a) (sign a)+    ++----------------------------------------------------++positive :: MonadSAT m+	 => Number +	 -> m Boolean+positive n = do+    ok <- or $ init $ bits n   +    and [ ok, not $ last $ bits n ]++negative :: MonadSAT m+	 => Number +	 -> m Boolean+negative n = do+    return $ last $ bits n++nonnegative :: MonadSAT m+	 => Number +	 -> m Boolean+nonnegative n = do+    return $ not $ last $ bits n++----------------------------------------------------++eq :: MonadSAT m +   => Number -> Number+   -> m Boolean+eq a b = do+    when ( width a /= width b ) +    	 $ error "Satchmo.Integer.Op.eq"+    eqs <- forM ( zip ( bits a ) ( bits b ) )+    	   $ \ (x,y) -> fun2 (==) x y+    and eqs++gt :: MonadSAT m +   => Number -> Number+   -> m Boolean+gt a b = do+    diff <- and [ not $ last $ bits a, last $ bits b ]+    same <- fun2 (==) ( last $ bits a )	+     	     	       ( last $ bits b )+    g <- F.gt ( F.make $ bits a ) +      	      ( F.make $ bits b )+    monadic or [ return diff+    	       , and [ same, g ]+	       ]++ge :: MonadSAT m +   => Number -> Number+   -> m Boolean+ge a b = do+    diff <- and [ not $ last $ bits a, last $ bits b ]+    same <- fun2 (==) ( last $ bits a )	+     	     	       ( last $ bits b )+    g <- F.ge ( F.make $ bits a ) +      	      ( F.make $ bits b )+    monadic or [ return diff+    	       , and [ same, g ]+	       ]+    

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

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

@@ -0,0 +1,128 @@+{-# LANGUAGE CPP #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE FlexibleContexts, FlexibleInstances #-}+{-# LANGUAGE GeneralizedNewtypeDeriving #-}+{-# LANGUAGE TypeFamilies #-}+++#if (__GLASGOW_HASKELL__ >= 708)+{-# LANGUAGE AllowAmbiguousTypes #-}+#endif++module Satchmo.MonadSAT++( MonadSAT(..), Weight+, Header (..)                +)++where++import Satchmo.Data+import Satchmo.Code++import Control.Applicative+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)+import qualified Control.Monad.State.Strict  as Strict (StateT)+import qualified Control.Monad.Writer.Strict as Strict (WriterT)+import qualified Control.Monad.RWS.Strict    as Strict (RWST)+import Data.Monoid++type Weight = Int++class ( -- MonadFix m,+        Applicative 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++data Header = +     Header { numClauses, numVars :: !Int+            , universals :: ![Int]+                     }+     deriving Show++-- -------------------------------------------------------+-- MonadSAT liftings for standard monad transformers+-- -------------------------------------------------------++instance (Monad m, MonadSAT m) => MonadSAT (ListT m) where+  fresh = lift fresh+  fresh_forall = lift fresh_forall+  emit  = lift . emit+  -- emitW = (lift.) . emitW+  note = lift . note++instance (Monad m, MonadSAT m) => MonadSAT (ReaderT r m) where+  fresh = lift fresh+  fresh_forall = lift fresh_forall+  emit  = lift . emit+  -- emitW = (lift.) . emitW+  note = lift . note++instance (Monad m, MonadSAT m) => MonadSAT (Lazy.StateT s m) where+  fresh = lift fresh+  fresh_forall = lift fresh_forall+  emit  = lift . emit+  -- emitW = (lift.) . emitW+  note = lift . note++instance (Monad m, MonadSAT m, Monoid w) => MonadSAT (Lazy.RWST r w s m) where+  fresh = lift fresh+  fresh_forall = lift fresh_forall+  emit  = lift . emit+  -- emitW = (lift.) . emitW+  note = lift . note++instance (Monad m, MonadSAT m, Monoid w) => MonadSAT (Lazy.WriterT w m) where+  fresh = lift fresh+  fresh_forall = lift fresh_forall+  emit  = lift . emit+  -- emitW = (lift.) . emitW+  note = lift . note++instance (Monad m, MonadSAT m) => MonadSAT (Strict.StateT s m) where+  fresh = lift fresh+  fresh_forall = lift fresh_forall+  emit  = lift . emit+  -- emitW = (lift.) . emitW+  note = lift . note++instance (Monad m, MonadSAT m, Monoid w) => MonadSAT (Strict.RWST r w s m) where+  fresh = lift fresh+  fresh_forall = lift fresh_forall+  emit  = lift . emit+  -- emitW = (lift.) . emitW+  note = lift . note++instance (Monad m, MonadSAT m, Monoid w) => MonadSAT (Strict.WriterT w m) where+  fresh = lift fresh+  fresh_forall = lift fresh_forall+  emit  = lift . emit+  -- emitW = (lift.) . emitW+  note = lift . note++instance (Monad m, MonadSAT m) => MonadSAT (ContT s m) where+  fresh = lift fresh+  fresh_forall = lift fresh_forall+  emit  = lift . emit+  -- emitW = (lift.) . emitW+  note = lift . note+

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

@@ -0,0 +1,177 @@+{-# language MultiParamTypeClasses #-}+{-# language FlexibleContexts      #-}+{-# language UndecidableInstances  #-}+{-# language FlexibleInstances #-}++module Satchmo.Polynomial ++( 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.MonadSAT (MonadSAT)+import Satchmo.Boolean (Boolean,monadic)+import qualified Satchmo.Boolean as B+import Satchmo.Code++import qualified Satchmo.BinaryTwosComplement.Op.Fixed as F+--import qualified Satchmo.Binary.Op.Fixed as F++import Control.Monad ( forM )++-- | polynomial in one variable,+-- coefficients starting from degree zero+data Poly a = Poly [a] deriving ( Eq, Ord, Show )++type NumPoly = Poly F.Number++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++null :: Poly a+null = Poly []++constantTerm :: Poly a -> a+constantTerm (Poly (c:_)) = c++coefficients :: Poly a -> [a]+coefficients (Poly cs) = cs++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)++reverseBoth :: ([a],[b]) -> ([a], [b])+reverseBoth (p1, p2) = (reverse p1, reverse p2)++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++equals p1 p2 = fill p1 p2 >>= uncurry equals'++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'

@@ -0,0 +1,14 @@+{-# language FlexibleInstances, MultiParamTypeClasses #-}++module Satchmo.Relation ++( module Satchmo.Relation.Data+, module Satchmo.Relation.Op+, module Satchmo.Relation.Prop+)++where++import Satchmo.Relation.Data+import Satchmo.Relation.Op+import Satchmo.Relation.Prop

@@ -0,0 +1,91 @@+{-# language FlexibleInstances, MultiParamTypeClasses, FlexibleContexts #-}++module Satchmo.Relation.Data++( Relation+, relation, symmetric_relation+, build+, identity                      +, bounds, (!), indices, assocs, elems+, table+) ++where++import Satchmo.Code+import Satchmo.Boolean++import Satchmo.SAT++import qualified Data.Array as A+import Data.Array ( Array, Ix )+import Data.Functor ((<$>))++import Control.Monad ( guard, forM )++newtype Relation a b = Relation ( Array (a,b) Boolean ) ++relation :: ( Ix a, Ix b, MonadSAT m ) +         => ((a,b),(a,b)) -> m ( Relation a b ) +{-# specialize inline relation :: ( Ix a, Ix b) => ((a,b),(a,b)) -> SAT ( Relation a b ) #-} +relation bnd = do+    pairs <- sequence $ do +        p <- A.range bnd+        return $ do+            x <- boolean+            return ( p, x )+    return $ build bnd pairs+    +symmetric_relation bnd = do+    pairs <- sequence $ do+        (p,q) <- A.range bnd+        guard $ p <= q+        return $ do+            x <- boolean+            return $ [ ((p,q), x ) ]+                   ++ [ ((q,p), x) | p /= q ]+    return $ build bnd $ concat 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 $ A.array bnd pairs+++bounds :: (Ix a, Ix b) => Relation a b -> ((a,b),(a,b))+bounds ( Relation r ) = A.bounds r++indices ( Relation r ) = A.indices r++assocs ( Relation r ) = A.assocs r++elems ( Relation r ) = A.elems r++Relation r ! p = r A.! p++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++table :: (Enum a, Ix a, Enum b, Ix b) +      => Array (a,b) Bool -> String+table r = unlines $ do+    let ((a,b),(c,d)) = A.bounds r+    x <- [ a .. c ]+    return $ unwords $ do+        y <- [ b .. d ]+        return $ if r A.! (x,y) then "*" else "."++

@@ -0,0 +1,85 @@+{-# language FlexibleInstances, MultiParamTypeClasses #-}++module Satchmo.Relation.Op++( mirror+, union+, complement+, product, power+, intersection+) ++where++import Prelude hiding ( and, or, not, product )+import qualified Prelude++import Satchmo.Code+import Satchmo.Boolean+import Satchmo.Counting+import Satchmo.Relation.Data++import Control.Monad ( guard )+import Data.Ix++import Satchmo.SAT++mirror :: ( Ix a , Ix b ) => Relation a b -> Relation b a+mirror r = +    let ((a,b),(c,d)) = bounds r+    in  build ((b,a),(d,c)) $ do (x,y) <- indices r ; return ((y,x), r!(x,y))++complement :: ( Ix a , Ix b ) => Relation a b -> Relation a b+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 )+{-# specialize inline union :: ( Ix a , Ix b ) => Relation a b -> Relation a b -> SAT ( Relation a b ) #-}      +union r s = do+    pairs <- sequence $ do+        i <- indices r+        return $ do o <- or [ r!i, s!i ] ; return ( i, o )+    return $ build ( bounds r ) pairs++product :: ( Ix a , Ix b, Ix c, MonadSAT m ) +        => Relation a b -> Relation b c -> m ( Relation a c )+{-# specialize inline product ::  ( Ix a , Ix b, Ix c ) => Relation a b -> Relation b c -> SAT ( Relation a c ) #-}      +product a b = do+    let ((ao,al),(au,ar)) = bounds a+        ((bo,bl),(bu,br)) = bounds b+        bnd = ((ao,bl),(au,br))+    pairs <- sequence $ do+        i@(x,z) <- range bnd+        return $ do+            o <- monadic or $ do+                y <- range ( al, ar )+                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 +      -> m ( Relation a b )+{-# specialize inline intersection ::  ( Ix a , Ix b ) => Relation a b -> Relation a b -> SAT ( Relation a b ) #-} +intersection r s = do+    pairs <- sequence $ do+        i <- indices r+        return $ do a <- and [ r!i, s!i ] ; return ( i, a )+    return $ build ( bounds r ) pairs++