diff --git a/Satchmo/Array.hs b/Satchmo/Array.hs deleted file mode 100644 --- a/Satchmo/Array.hs +++ /dev/null @@ -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) diff --git a/Satchmo/Binary.hs b/Satchmo/Binary.hs deleted file mode 100644 --- a/Satchmo/Binary.hs +++ /dev/null @@ -1,10 +0,0 @@ -{-# language MultiParamTypeClasses #-} - -module Satchmo.Binary - -( module Satchmo.Binary.Op.Flexible -) - -where - -import Satchmo.Binary.Op.Flexible diff --git a/Satchmo/Binary/Data.hs b/Satchmo/Binary/Data.hs deleted file mode 100644 --- a/Satchmo/Binary/Data.hs +++ /dev/null @@ -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 diff --git a/Satchmo/Binary/Numeric.hs b/Satchmo/Binary/Numeric.hs deleted file mode 100644 --- a/Satchmo/Binary/Numeric.hs +++ /dev/null @@ -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 diff --git a/Satchmo/Binary/Op/Common.hs b/Satchmo/Binary/Op/Common.hs deleted file mode 100644 --- a/Satchmo/Binary/Op/Common.hs +++ /dev/null @@ -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 ) diff --git a/Satchmo/Binary/Op/Fixed.hs b/Satchmo/Binary/Op/Fixed.hs deleted file mode 100644 --- a/Satchmo/Binary/Op/Fixed.hs +++ /dev/null @@ -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 - diff --git a/Satchmo/Binary/Op/Flexible.hs b/Satchmo/Binary/Op/Flexible.hs deleted file mode 100644 --- a/Satchmo/Binary/Op/Flexible.hs +++ /dev/null @@ -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 - - diff --git a/Satchmo/Binary/Op/Times.hs b/Satchmo/Binary/Op/Times.hs deleted file mode 100644 --- a/Satchmo/Binary/Op/Times.hs +++ /dev/null @@ -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]) ] - - diff --git a/Satchmo/BinaryTwosComplement.hs b/Satchmo/BinaryTwosComplement.hs deleted file mode 100644 --- a/Satchmo/BinaryTwosComplement.hs +++ /dev/null @@ -1,7 +0,0 @@ -module Satchmo.BinaryTwosComplement - -( module Satchmo.BinaryTwosComplement.Op.Fixed ) - -where - -import Satchmo.BinaryTwosComplement.Op.Fixed diff --git a/Satchmo/BinaryTwosComplement/Data.hs b/Satchmo/BinaryTwosComplement/Data.hs deleted file mode 100644 --- a/Satchmo/BinaryTwosComplement/Data.hs +++ /dev/null @@ -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 diff --git a/Satchmo/BinaryTwosComplement/Numeric.hs b/Satchmo/BinaryTwosComplement/Numeric.hs deleted file mode 100644 --- a/Satchmo/BinaryTwosComplement/Numeric.hs +++ /dev/null @@ -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 diff --git a/Satchmo/BinaryTwosComplement/Op/Common.hs b/Satchmo/BinaryTwosComplement/Op/Common.hs deleted file mode 100644 --- a/Satchmo/BinaryTwosComplement/Op/Common.hs +++ /dev/null @@ -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 diff --git a/Satchmo/BinaryTwosComplement/Op/Fixed.hs b/Satchmo/BinaryTwosComplement/Op/Fixed.hs deleted file mode 100644 --- a/Satchmo/BinaryTwosComplement/Op/Fixed.hs +++ /dev/null @@ -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 diff --git a/Satchmo/Boolean.hs b/Satchmo/Boolean.hs deleted file mode 100644 --- a/Satchmo/Boolean.hs +++ /dev/null @@ -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 diff --git a/Satchmo/Boolean/Data.hs b/Satchmo/Boolean/Data.hs deleted file mode 100644 --- a/Satchmo/Boolean/Data.hs +++ /dev/null @@ -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 - diff --git a/Satchmo/Boolean/Op.hs b/Satchmo/Boolean/Op.hs deleted file mode 100644 --- a/Satchmo/Boolean/Op.hs +++ /dev/null @@ -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 ] - diff --git a/Satchmo/Code.hs b/Satchmo/Code.hs deleted file mode 100644 --- a/Satchmo/Code.hs +++ /dev/null @@ -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 diff --git a/Satchmo/Counting.hs b/Satchmo/Counting.hs deleted file mode 100644 --- a/Satchmo/Counting.hs +++ /dev/null @@ -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 - - diff --git a/Satchmo/Counting/Binary.hs b/Satchmo/Counting/Binary.hs deleted file mode 100644 --- a/Satchmo/Counting/Binary.hs +++ /dev/null @@ -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 - - - - diff --git a/Satchmo/Counting/Direct.hs b/Satchmo/Counting/Direct.hs deleted file mode 100644 --- a/Satchmo/Counting/Direct.hs +++ /dev/null @@ -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 - - diff --git a/Satchmo/Counting/Unary.hs b/Satchmo/Counting/Unary.hs deleted file mode 100644 --- a/Satchmo/Counting/Unary.hs +++ /dev/null @@ -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 - diff --git a/Satchmo/Data.hs b/Satchmo/Data.hs deleted file mode 100644 --- a/Satchmo/Data.hs +++ /dev/null @@ -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 - diff --git a/Satchmo/Integer.hs b/Satchmo/Integer.hs deleted file mode 100644 --- a/Satchmo/Integer.hs +++ /dev/null @@ -1,10 +0,0 @@ -module Satchmo.Integer - -( module Satchmo.Integer.Data -, module Satchmo.Integer.Op -) - -where - -import Satchmo.Integer.Data -import Satchmo.Integer.Op diff --git a/Satchmo/Integer/Data.hs b/Satchmo/Integer/Data.hs deleted file mode 100644 --- a/Satchmo/Integer/Data.hs +++ /dev/null @@ -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 diff --git a/Satchmo/Integer/Difference.hs b/Satchmo/Integer/Difference.hs deleted file mode 100644 --- a/Satchmo/Integer/Difference.hs +++ /dev/null @@ -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 } diff --git a/Satchmo/Integer/Op.hs b/Satchmo/Integer/Op.hs deleted file mode 100644 --- a/Satchmo/Integer/Op.hs +++ /dev/null @@ -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 ] - ] - diff --git a/Satchmo/Map.hs b/Satchmo/Map.hs deleted file mode 100644 --- a/Satchmo/Map.hs +++ /dev/null @@ -1,8 +0,0 @@ -module Satchmo.Map - -( module Satchmo.Map.Data -) - -where - -import Satchmo.Map.Data diff --git a/Satchmo/Map/Data.hs b/Satchmo/Map/Data.hs deleted file mode 100644 --- a/Satchmo/Map/Data.hs +++ /dev/null @@ -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 ) - - diff --git a/Satchmo/MonadSAT.hs b/Satchmo/MonadSAT.hs deleted file mode 100644 --- a/Satchmo/MonadSAT.hs +++ /dev/null @@ -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 - diff --git a/Satchmo/Numeric.hs b/Satchmo/Numeric.hs deleted file mode 100644 --- a/Satchmo/Numeric.hs +++ /dev/null @@ -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 - diff --git a/Satchmo/Polynomial.hs b/Satchmo/Polynomial.hs deleted file mode 100644 --- a/Satchmo/Polynomial.hs +++ /dev/null @@ -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 - diff --git a/Satchmo/Polynomial/Numeric.hs b/Satchmo/Polynomial/Numeric.hs deleted file mode 100644 --- a/Satchmo/Polynomial/Numeric.hs +++ /dev/null @@ -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 - - diff --git a/Satchmo/PolynomialN.hs b/Satchmo/PolynomialN.hs deleted file mode 100644 --- a/Satchmo/PolynomialN.hs +++ /dev/null @@ -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] diff --git a/Satchmo/PolynomialSOS.hs b/Satchmo/PolynomialSOS.hs deleted file mode 100644 --- a/Satchmo/PolynomialSOS.hs +++ /dev/null @@ -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' diff --git a/Satchmo/Relation.hs b/Satchmo/Relation.hs deleted file mode 100644 --- a/Satchmo/Relation.hs +++ /dev/null @@ -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 diff --git a/Satchmo/Relation/Data.hs b/Satchmo/Relation/Data.hs deleted file mode 100644 --- a/Satchmo/Relation/Data.hs +++ /dev/null @@ -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 "." - - diff --git a/Satchmo/Relation/Op.hs b/Satchmo/Relation/Op.hs deleted file mode 100644 --- a/Satchmo/Relation/Op.hs +++ /dev/null @@ -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 - - diff --git a/Satchmo/Relation/Prop.hs b/Satchmo/Relation/Prop.hs deleted file mode 100644 --- a/Satchmo/Relation/Prop.hs +++ /dev/null @@ -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 diff --git a/Satchmo/SAT.hs b/Satchmo/SAT.hs deleted file mode 100644 --- a/Satchmo/SAT.hs +++ /dev/null @@ -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 diff --git a/Satchmo/SAT/External.hs b/Satchmo/SAT/External.hs deleted file mode 100644 --- a/Satchmo/SAT/External.hs +++ /dev/null @@ -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 diff --git a/Satchmo/SAT/Mini.hs b/Satchmo/SAT/Mini.hs deleted file mode 100644 --- a/Satchmo/SAT/Mini.hs +++ /dev/null @@ -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 diff --git a/Satchmo/SAT/Tmpfile.hs b/Satchmo/SAT/Tmpfile.hs deleted file mode 100644 --- a/Satchmo/SAT/Tmpfile.hs +++ /dev/null @@ -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} - diff --git a/Satchmo/Set.hs b/Satchmo/Set.hs deleted file mode 100644 --- a/Satchmo/Set.hs +++ /dev/null @@ -1,10 +0,0 @@ -module Satchmo.Set - -( module Satchmo.Set.Data -, module Satchmo.Set.Op -) - -where - -import Satchmo.Set.Data -import Satchmo.Set.Op diff --git a/Satchmo/Set/Data.hs b/Satchmo/Set/Data.hs deleted file mode 100644 --- a/Satchmo/Set/Data.hs +++ /dev/null @@ -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) ) - diff --git a/Satchmo/Set/Op.hs b/Satchmo/Set/Op.hs deleted file mode 100644 --- a/Satchmo/Set/Op.hs +++ /dev/null @@ -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) ) - - - diff --git a/Satchmo/Unary.hs b/Satchmo/Unary.hs deleted file mode 100644 --- a/Satchmo/Unary.hs +++ /dev/null @@ -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 diff --git a/Satchmo/Unary/Data.hs b/Satchmo/Unary/Data.hs deleted file mode 100644 --- a/Satchmo/Unary/Data.hs +++ /dev/null @@ -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 diff --git a/Satchmo/Unary/Op/Common.hs b/Satchmo/Unary/Op/Common.hs deleted file mode 100644 --- a/Satchmo/Unary/Op/Common.hs +++ /dev/null @@ -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 --- -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) - --- | -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 - --- | - -oe_merge [] ys = return ys -oe_merge xs [] = return xs -oe_merge [x] [y] = do - comparator x y -oe_merge xs ys = do - let ( xo, xe ) = divide xs - ( yo, ye ) = divide ys - m : mo <- oe_merge xo yo - me <- oe_merge xe ye - re <- repair me mo - return $ m : re - -divide (x : xs) = - let ( this, that ) = divide xs - in ( x : that, this ) -divide [] = ( [], [] ) - -repair (x:xs) (y:ys) = do - here <- comparator x y - later <- repair xs ys - return $ here ++ later -repair [] [] = return [] -repair [x] [] = return [x] -repair [] [y] = return [y] - -comparator x y = do - hi <- Satchmo.Boolean.or [x, y] - lo <- Satchmo.Boolean.and [x, y] - return [ hi, lo ] diff --git a/Satchmo/Unary/Op/Fixed.hs b/Satchmo/Unary/Op/Fixed.hs deleted file mode 100644 --- a/Satchmo/Unary/Op/Fixed.hs +++ /dev/null @@ -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 - - - diff --git a/Satchmo/Unary/Op/Flexible.hs b/Satchmo/Unary/Op/Flexible.hs deleted file mode 100644 --- a/Satchmo/Unary/Op/Flexible.hs +++ /dev/null @@ -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 diff --git a/examples/AIS.hs b/examples/AIS.hs new file mode 100644 --- /dev/null +++ b/examples/AIS.hs @@ -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 ) diff --git a/examples/Hidoku.hs b/examples/Hidoku.hs new file mode 100644 --- /dev/null +++ b/examples/Hidoku.hs @@ -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] diff --git a/examples/Langford.hs b/examples/Langford.hs new file mode 100644 --- /dev/null +++ b/examples/Langford.hs @@ -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 ) diff --git a/examples/Oscillator.hs b/examples/Oscillator.hs --- a/examples/Oscillator.hs +++ b/examples/Oscillator.hs @@ -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 ) diff --git a/examples/PP.hs b/examples/PP.hs --- a/examples/PP.hs +++ b/examples/PP.hs @@ -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 ) diff --git a/examples/Pigeon.hs b/examples/Pigeon.hs new file mode 100644 --- /dev/null +++ b/examples/Pigeon.hs @@ -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] + diff --git a/examples/Pythagoras.hs b/examples/Pythagoras.hs new file mode 100644 --- /dev/null +++ b/examples/Pythagoras.hs @@ -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 + diff --git a/examples/Ramsey.hs b/examples/Ramsey.hs --- a/examples/Ramsey.hs +++ b/examples/Ramsey.hs @@ -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 ) diff --git a/examples/Spaceship.hs b/examples/Spaceship.hs --- a/examples/Spaceship.hs +++ b/examples/Spaceship.hs @@ -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) ) diff --git a/examples/Sudoku.hs b/examples/Sudoku.hs --- a/examples/Sudoku.hs +++ b/examples/Sudoku.hs @@ -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 diff --git a/gpl-2.0.txt b/gpl-2.0.txt deleted file mode 100644 --- a/gpl-2.0.txt +++ /dev/null @@ -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. - - - Copyright (C) - - 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. - - , 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. diff --git a/satchmo.cabal b/satchmo.cabal --- a/satchmo.cabal +++ b/satchmo.cabal @@ -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 diff --git a/src/Satchmo/Array.hs b/src/Satchmo/Array.hs new file mode 100644 --- /dev/null +++ b/src/Satchmo/Array.hs @@ -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) diff --git a/src/Satchmo/Binary.hs b/src/Satchmo/Binary.hs new file mode 100644 --- /dev/null +++ b/src/Satchmo/Binary.hs @@ -0,0 +1,10 @@ +{-# language MultiParamTypeClasses #-} + +module Satchmo.Binary + +( module Satchmo.Binary.Op.Flexible +) + +where + +import Satchmo.Binary.Op.Flexible diff --git a/src/Satchmo/Binary/Data.hs b/src/Satchmo/Binary/Data.hs new file mode 100644 --- /dev/null +++ b/src/Satchmo/Binary/Data.hs @@ -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 diff --git a/src/Satchmo/Binary/Numeric.hs b/src/Satchmo/Binary/Numeric.hs new file mode 100644 --- /dev/null +++ b/src/Satchmo/Binary/Numeric.hs @@ -0,0 +1,19 @@ +module Satchmo.Binary.Numeric where + +-- import qualified Satchmo.Binary.Op.Flexible as F +import qualified Satchmo.Binary.Op.Fixed as F + +import qualified Satchmo.Numeric as N + +instance N.Constant F.Number where + constant = F.constant + +instance N.Create F.Number where + create = F.number + +instance N.Numeric F.Number where + equal = F.equals + greater_equal = F.ge + plus = F.add + minus = error "Satchmo.Binary does not implement minus" + times = F.times diff --git a/src/Satchmo/Binary/Op/Common.hs b/src/Satchmo/Binary/Op/Common.hs new file mode 100644 --- /dev/null +++ b/src/Satchmo/Binary/Op/Common.hs @@ -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 ) diff --git a/src/Satchmo/Binary/Op/Fixed.hs b/src/Satchmo/Binary/Op/Fixed.hs new file mode 100644 --- /dev/null +++ b/src/Satchmo/Binary/Op/Fixed.hs @@ -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 + diff --git a/src/Satchmo/Binary/Op/Flexible.hs b/src/Satchmo/Binary/Op/Flexible.hs new file mode 100644 --- /dev/null +++ b/src/Satchmo/Binary/Op/Flexible.hs @@ -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 + + diff --git a/src/Satchmo/Binary/Op/Times.hs b/src/Satchmo/Binary/Op/Times.hs new file mode 100644 --- /dev/null +++ b/src/Satchmo/Binary/Op/Times.hs @@ -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]) ] + + diff --git a/src/Satchmo/BinaryTwosComplement.hs b/src/Satchmo/BinaryTwosComplement.hs new file mode 100644 --- /dev/null +++ b/src/Satchmo/BinaryTwosComplement.hs @@ -0,0 +1,7 @@ +module Satchmo.BinaryTwosComplement + +( module Satchmo.BinaryTwosComplement.Op.Fixed ) + +where + +import Satchmo.BinaryTwosComplement.Op.Fixed diff --git a/src/Satchmo/BinaryTwosComplement/Data.hs b/src/Satchmo/BinaryTwosComplement/Data.hs new file mode 100644 --- /dev/null +++ b/src/Satchmo/BinaryTwosComplement/Data.hs @@ -0,0 +1,98 @@ +{-# language MultiParamTypeClasses, FlexibleInstances, FlexibleContexts, UndecidableInstances #-} + +module Satchmo.BinaryTwosComplement.Data + ( Number, bits, fromBooleans, number, toUnsigned, fromUnsigned + , width, isNull, msb, constant, constantWidth) + +where + +import Control.Applicative ((<$>)) +import Satchmo.MonadSAT (MonadSAT) +import Satchmo.Boolean (Boolean) +import qualified Satchmo.Boolean as Boolean +import qualified Satchmo.Code as C +import qualified Satchmo.Binary.Data as B + +import Debug.Trace + +data Number = Number + { bits :: [Boolean] -- LSB first + } + + +instance (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 diff --git a/src/Satchmo/BinaryTwosComplement/Numeric.hs b/src/Satchmo/BinaryTwosComplement/Numeric.hs new file mode 100644 --- /dev/null +++ b/src/Satchmo/BinaryTwosComplement/Numeric.hs @@ -0,0 +1,17 @@ +module Satchmo.BinaryTwosComplement.Numeric where + +import qualified Satchmo.BinaryTwosComplement.Op.Fixed as F +import qualified Satchmo.Numeric as N + +instance N.Constant F.Number where + constant = F.constantWidth 1 + +instance N.Create F.Number where + create = F.number + +instance N.Numeric F.Number where + equal = F.equals + greater_equal = F.ge + plus = F.add + minus = F.subtract + times = F.times diff --git a/src/Satchmo/BinaryTwosComplement/Op/Common.hs b/src/Satchmo/BinaryTwosComplement/Op/Common.hs new file mode 100644 --- /dev/null +++ b/src/Satchmo/BinaryTwosComplement/Op/Common.hs @@ -0,0 +1,38 @@ +module Satchmo.BinaryTwosComplement.Op.Common + (equals, eq, lt, le, ge, gt, positive, negative, nonNegative) +where + +import Prelude hiding (and,or,not) +import Satchmo.MonadSAT (MonadSAT) +import Satchmo.BinaryTwosComplement.Data (Number,toUnsigned,msb,bits) +import Satchmo.Boolean (Boolean,and,or,not,ifThenElseM) +import qualified Satchmo.Boolean as Boolean +import qualified Satchmo.Binary.Op.Common as B + +sameSign, negativePositive :: MonadSAT m => Number -> Number -> m Boolean +sameSign a b = Boolean.equals [msb a, msb b] +negativePositive a b = and [msb a, not $ msb b] + +equals,eq,lt,le,ge,gt :: MonadSAT m => Number -> Number -> m Boolean +equals a b = B.equals (toUnsigned a) (toUnsigned b) +eq = equals + +lt a b = ifThenElseM ( sameSign a b ) + ( B.lt (toUnsigned a) (toUnsigned b) ) + ( negativePositive a b ) + +le a b = ifThenElseM ( sameSign a b ) + ( B.le (toUnsigned a) (toUnsigned b) ) + ( negativePositive a b ) + +ge = flip le +gt = flip lt + +positive,negative,nonNegative :: MonadSAT m => Number -> m Boolean +positive a = do + one <- or $ bits a + and [not $ msb a, one] + +negative = return . msb + +nonNegative = return . not . msb diff --git a/src/Satchmo/BinaryTwosComplement/Op/Fixed.hs b/src/Satchmo/BinaryTwosComplement/Op/Fixed.hs new file mode 100644 --- /dev/null +++ b/src/Satchmo/BinaryTwosComplement/Op/Fixed.hs @@ -0,0 +1,94 @@ +{-# language MultiParamTypeClasses #-} + +-- | Operations with fixed bit width. +-- Still they are non-overflowing: +-- if overflow occurs, the constraints are not satisfiable. +-- The bit width of the result of binary operations +-- is the max of the bit width of the inputs. + +module Satchmo.BinaryTwosComplement.Op.Fixed + ( add, subtract, times, increment, negate, linear + , module Satchmo.BinaryTwosComplement.Data + , module Satchmo.BinaryTwosComplement.Op.Common + ) +where + +import Prelude hiding (not,negate, subtract) +import Control.Applicative ((<$>)) +import Satchmo.MonadSAT (MonadSAT) +import Satchmo.BinaryTwosComplement.Op.Common +import Satchmo.BinaryTwosComplement.Data +import qualified Satchmo.Binary.Op.Common as C +import qualified Satchmo.Binary.Op.Flexible as F +import Satchmo.Binary.Op.Fixed (restrictedTimes) +import Satchmo.Boolean (Boolean,monadic,assertOr,equals2,implies,not) +import qualified Satchmo.Boolean as Boolean + +-- | Sign extension +extendMsb :: Int -> Number -> Number +extendMsb i n = fromBooleans $ bits n ++ (replicate i $ msb n) + +add :: (MonadSAT m) => Number -> Number -> m Number +add a b = do + let maxWidth = max (width a) (width b) + widthDiff = abs $ (width a) - (width b) + extend x = if width x == maxWidth then extendMsb 1 x + else extendMsb (widthDiff + 1) x + a' = extend a + b' = extend b + + flexibleResult <- fromUnsigned <$> F.add (toUnsigned a') (toUnsigned b') + let (low, high) = splitAt maxWidth $ bits flexibleResult + + e <- Boolean.equals [last low, head high] + assertOr [ e ] + return $ fromBooleans low + +times :: MonadSAT m => Number -> Number -> m Number +times a b = do + let a' = extendMsb (width b) a + b' = extendMsb (width a) b + unsignedResultWidth = (width a) + (width b) + resultWidth = max (width a) (width b) + + unsignedResult <- fromUnsigned <$> + restrictedTimes (toUnsigned a') (toUnsigned b') + let (low, high) = splitAt resultWidth $ bits unsignedResult + allHighOne <- Boolean.and $ high + allHighZero <- Boolean.and $ map not high + assertOr [allHighOne, allHighZero] + + e <- Boolean.equals [ last low, head high ] + assertOr [e] + return $ fromBooleans low + +increment :: MonadSAT m => Number -> m Number +increment n = + let inc [] z = return ( [], z ) + inc (y:ys) z = do + ( r, c ) <- C.half_adder y z + ( rAll, cAll ) <- inc ys c + return ( r : rAll, cAll ) + in do + add1 <- Boolean.constant True + (n', _) <- inc (bits n) add1 + e <- (not $ msb n) `implies` (not $ last n') + assertOr [ e ] + return $ fromBooleans n' + +subtract :: MonadSAT m => Number -> Number -> m Number +subtract a b = do + b' <- negate b + add a b' + +negate :: MonadSAT m => Number -> m Number +negate n = + let invN = fromBooleans $ map not $ bits n + in do + n' <- increment invN + e <- (msb n) `implies` (not $ msb n') + assertOr [ e ] + return n' + +linear :: MonadSAT m => Number -> Number -> Number -> m Number +linear m x n = m `times` x >>= add n diff --git a/src/Satchmo/Boolean.hs b/src/Satchmo/Boolean.hs new file mode 100644 --- /dev/null +++ b/src/Satchmo/Boolean.hs @@ -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 diff --git a/src/Satchmo/Boolean/Data.hs b/src/Satchmo/Boolean/Data.hs new file mode 100644 --- /dev/null +++ b/src/Satchmo/Boolean/Data.hs @@ -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 + diff --git a/src/Satchmo/Boolean/Op.hs b/src/Satchmo/Boolean/Op.hs new file mode 100644 --- /dev/null +++ b/src/Satchmo/Boolean/Op.hs @@ -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 ] + diff --git a/src/Satchmo/Code.hs b/src/Satchmo/Code.hs new file mode 100644 --- /dev/null +++ b/src/Satchmo/Code.hs @@ -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 diff --git a/src/Satchmo/Counting.hs b/src/Satchmo/Counting.hs new file mode 100644 --- /dev/null +++ b/src/Satchmo/Counting.hs @@ -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 + + diff --git a/src/Satchmo/Counting/Binary.hs b/src/Satchmo/Counting/Binary.hs new file mode 100644 --- /dev/null +++ b/src/Satchmo/Counting/Binary.hs @@ -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 + + + + diff --git a/src/Satchmo/Counting/Direct.hs b/src/Satchmo/Counting/Direct.hs new file mode 100644 --- /dev/null +++ b/src/Satchmo/Counting/Direct.hs @@ -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 + + diff --git a/src/Satchmo/Counting/Unary.hs b/src/Satchmo/Counting/Unary.hs new file mode 100644 --- /dev/null +++ b/src/Satchmo/Counting/Unary.hs @@ -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 + diff --git a/src/Satchmo/Data.hs b/src/Satchmo/Data.hs new file mode 100644 --- /dev/null +++ b/src/Satchmo/Data.hs @@ -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 + diff --git a/src/Satchmo/Integer.hs b/src/Satchmo/Integer.hs new file mode 100644 --- /dev/null +++ b/src/Satchmo/Integer.hs @@ -0,0 +1,10 @@ +module Satchmo.Integer + +( module Satchmo.Integer.Data +, module Satchmo.Integer.Op +) + +where + +import Satchmo.Integer.Data +import Satchmo.Integer.Op diff --git a/src/Satchmo/Integer/Data.hs b/src/Satchmo/Integer/Data.hs new file mode 100644 --- /dev/null +++ b/src/Satchmo/Integer/Data.hs @@ -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 diff --git a/src/Satchmo/Integer/Difference.hs b/src/Satchmo/Integer/Difference.hs new file mode 100644 --- /dev/null +++ b/src/Satchmo/Integer/Difference.hs @@ -0,0 +1,58 @@ +{-# language MultiParamTypeClasses, FlexibleContexts, FlexibleInstances #-} + +module Satchmo.Integer.Difference where + +import Satchmo.Code +import Satchmo.Numeric + +data Number a = Difference { top :: a, bot :: a } + +instance Decode m a Integer + => Decode m ( Number a ) Integer where + decode n = do + t <- decode $ top n + b <- decode $ bot n + return $ t - b + +instance Constant a => Constant ( Number a ) where + constant n = + if n >= 0 then do + t <- constant n + b <- constant 0 + return $ Difference { top = t, bot = b } + else do + t <- constant 0 + b <- constant $ negate n + return $ Difference { top = t, bot = b } + +instance Create a => Create ( Number a ) where + create bits = do + t <- create bits + b <- create bits + return $ Difference { top = t, bot = b } + +instance Numeric a => Numeric ( Number a ) where + equal a b = do + t <- plus ( top a ) ( bot b ) + b <- plus ( bot a ) ( top b ) + equal t b + greater_equal a b = do + t <- plus ( top a ) ( bot b ) + b <- plus ( bot a ) ( top b ) + greater_equal t b + plus a b = do + t <- plus ( top a ) ( top b ) + b <- plus ( bot a ) ( bot b ) + return $ Difference { top = t, bot = b } + minus a b = do + t <- plus ( top a ) ( bot b ) + b <- plus ( bot a ) ( top b ) + return $ Difference { top = t, bot = b } + times a b = do + tt <- times ( top a ) ( top b ) + bb <- times ( bot a ) ( bot b ) + t <- plus tt bb + tb <- times ( top a ) ( bot b ) + bt <- times ( bot a ) ( top b ) + b <- plus tb bt + return $ Difference { top = t, bot = b } diff --git a/src/Satchmo/Integer/Op.hs b/src/Satchmo/Integer/Op.hs new file mode 100644 --- /dev/null +++ b/src/Satchmo/Integer/Op.hs @@ -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 ] + ] + diff --git a/src/Satchmo/Map.hs b/src/Satchmo/Map.hs new file mode 100644 --- /dev/null +++ b/src/Satchmo/Map.hs @@ -0,0 +1,8 @@ +module Satchmo.Map + +( module Satchmo.Map.Data +) + +where + +import Satchmo.Map.Data diff --git a/src/Satchmo/Map/Data.hs b/src/Satchmo/Map/Data.hs new file mode 100644 --- /dev/null +++ b/src/Satchmo/Map/Data.hs @@ -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 ) + + diff --git a/src/Satchmo/MonadSAT.hs b/src/Satchmo/MonadSAT.hs new file mode 100644 --- /dev/null +++ b/src/Satchmo/MonadSAT.hs @@ -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 + diff --git a/src/Satchmo/Numeric.hs b/src/Satchmo/Numeric.hs new file mode 100644 --- /dev/null +++ b/src/Satchmo/Numeric.hs @@ -0,0 +1,21 @@ +{-# language FlexibleContexts #-} + +module Satchmo.Numeric where + +import Satchmo.Boolean +import Satchmo.Code + +class Constant a where + constant :: MonadSAT m => Integer -> m a + +class Create a where + -- | Parameter: bit width + create :: MonadSAT m => Int -> m a + +class Numeric a where + equal :: MonadSAT m => a -> a -> m Boolean + greater_equal :: MonadSAT m => a -> a -> m Boolean + plus :: MonadSAT m => a -> a -> m a + minus :: MonadSAT m => a -> a -> m a + times :: MonadSAT m => a -> a -> m a + diff --git a/src/Satchmo/Polynomial.hs b/src/Satchmo/Polynomial.hs new file mode 100644 --- /dev/null +++ b/src/Satchmo/Polynomial.hs @@ -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 + diff --git a/src/Satchmo/Polynomial/Numeric.hs b/src/Satchmo/Polynomial/Numeric.hs new file mode 100644 --- /dev/null +++ b/src/Satchmo/Polynomial/Numeric.hs @@ -0,0 +1,84 @@ +{-# language MultiParamTypeClasses, FlexibleInstances #-} + +module Satchmo.Polynomial.Numeric where + +import qualified Satchmo.Boolean as B +import Satchmo.Code +import Satchmo.Numeric + +import Control.Monad ( forM ) + +data Poly a = Poly [a] deriving Show + +instance Decode m a b => Decode m ( Poly a ) ( Poly b ) where + decode ( Poly xs ) = do + ys <- forM xs decode + return $ Poly ys + +derive ( Poly xs ) = do + ys <- forM ( drop 1 $ zip [ 0 .. ] xs ) $ \ (k,x) -> do + f <- constant k + times f x + return $ Poly ys + +constantTerm ( Poly xs ) = head xs + +polynomial :: ( Create a , B.MonadSAT m ) + => Int -> Int + -> m ( Poly a ) +polynomial bits degree = do + xs <- forM [ 0 .. degree ] $ \ k -> create bits + return $ Poly xs + +compose ( Poly xs ) q = case xs of + [] -> return $ Poly [] + x : xs -> do + p <- compose ( Poly xs ) q + pq <- times p q + plus ( Poly [x] ) pq + + +instance ( Create a, Constant a, Numeric a ) + => Numeric ( Poly a ) where + equal ( Poly xs ) ( Poly ys ) = do + z <- create 0 + bs <- forM ( fullZip xs ys ) $ \ xy -> case xy of + ( Just x, Just y ) -> equal x y + ( Just x, Nothing ) -> equal x z + ( Nothing, Just y ) -> equal z y + B.and bs + greater_equal ( Poly xs ) ( Poly ys ) = do + z <- create 0 + bs <- forM ( fullZip xs ys ) $ \ xy -> case xy of + ( Just x, Just y ) -> greater_equal x y + ( Just x, Nothing ) -> greater_equal x z + ( Nothing, Just y ) -> greater_equal z y + B.and bs + plus ( Poly xs ) ( Poly ys ) = do + bs <- forM ( fullZip xs ys ) $ \ xy -> case xy of + ( Just x, Just y ) -> plus x y + ( Just x, Nothing ) -> return x + ( Nothing, Just y ) -> return y + return $ Poly bs + minus ( Poly xs ) ( Poly ys ) = do + z <- create 0 + bs <- forM ( fullZip xs ys ) $ \ xy -> case xy of + ( Just x, Just y ) -> minus x y + ( Just x, Nothing ) -> return x + ( Nothing, Just y ) -> minus z y + return $ Poly bs + times ( Poly xs ) ( Poly ys ) = case xs of + [] -> return $ Poly [] + x : xs -> do + xys <- forM ys $ times x + z <- constant 0 + Poly rest <- times (Poly xs) (Poly ys) + plus ( Poly xys ) ( Poly $ z : rest ) + +fullZip :: [a] -> [b] -> [ (Maybe a, Maybe b) ] +fullZip [] [] = [] +fullZip [] (y:ys) = (Nothing, Just y) : fullZip [] ys +fullZip (x:xs) [] = (Just x, Nothing) : fullZip xs [] +fullZip (x:xs) (y:ys) = (Just x, Just y) : fullZip xs ys + + diff --git a/src/Satchmo/PolynomialN.hs b/src/Satchmo/PolynomialN.hs new file mode 100644 --- /dev/null +++ b/src/Satchmo/PolynomialN.hs @@ -0,0 +1,96 @@ +{-# language FlexibleInstances #-} +{-# language MultiParamTypeClasses #-} +{-# language FlexibleContexts #-} + +module Satchmo.PolynomialN + ( Coefficient, Exponents, PolynomialN (), NumPolynomialN + , fromMonomials, add, equals) +where + +import Control.Monad (forM,foldM) +import Data.List (partition,sortBy) +import qualified Satchmo.Binary.Op.Fixed as F +import Satchmo.Code (Decode (..),decode) +import Satchmo.MonadSAT (MonadSAT) +import Satchmo.Boolean (Boolean) +import qualified Satchmo.Boolean as B + +type Coefficient a = a + +type Exponents = [Integer] + +data Monomial a = Monomial (Coefficient a, Exponents) deriving (Show) +type NumMonomial = Monomial F.Number + +data PolynomialN a = PolynomialN [Monomial a] deriving (Show) +type NumPolynomialN = PolynomialN F.Number + +instance Decode m a Integer => Decode m (Monomial a) (Monomial Integer) where + decode (Monomial (coeff,vars)) = do + decodedCoeff <- decode coeff + return $ Monomial (decodedCoeff,vars) + +instance Decode m a Integer => Decode m (PolynomialN a) (PolynomialN Integer) where + decode (PolynomialN monomials) = do + decodedMonomials <- forM monomials decode + return $ PolynomialN decodedMonomials + +fromMonomials :: MonadSAT m + => Int -- ^ bit width of coefficients + -> [(Coefficient Integer,Exponents)] -- ^ monomials + -> m NumPolynomialN +fromMonomials bits monomials = do + monomials' <- forM monomials $ \(c,es) -> do + coefficient <- F.constantWidth bits c + return $ Monomial (coefficient,es) + reduce $ PolynomialN monomials' + +coefficient :: Monomial a -> Coefficient a +coefficient (Monomial (c,_)) = c + +exponents :: Monomial a -> Exponents +exponents (Monomial (_,e)) = e + +monomials :: PolynomialN a -> [Monomial a] +monomials (PolynomialN xs) = xs + +sameExponents :: Monomial a -> Monomial a -> Bool +sameExponents m1 m2 = exponents m1 == exponents m2 + +add :: MonadSAT m => NumPolynomialN -> NumPolynomialN -> m NumPolynomialN +add (PolynomialN xs) (PolynomialN ys) = + reduce $ PolynomialN $ xs ++ ys + +addMonomial :: MonadSAT m => NumMonomial -> NumMonomial -> m NumMonomial +addMonomial m1 m2 = + if sameExponents m1 m2 then + do c <- F.add (coefficient m1) (coefficient m2) + return $ Monomial (c, exponents m1) + else + error "PolynomialN.addMonomial" + +strictOrdering :: Monomial a -> Monomial a -> Ordering +strictOrdering (Monomial (_,xs)) (Monomial (_,ys)) = compare xs ys + +reduce :: MonadSAT m => NumPolynomialN -> m NumPolynomialN +reduce (PolynomialN []) = return $ PolynomialN [] +reduce (PolynomialN (x:xs)) = + let (reducable,notReducable) = partition (sameExponents x) xs + strictOrd (Monomial (_,xs)) (Monomial (_,ys)) = compare xs ys + in do + newMonomial <- foldM addMonomial x reducable + PolynomialN rest <- reduce $ PolynomialN notReducable + return $ PolynomialN $ sortBy strictOrd $ newMonomial : rest + +equalsMonomial :: MonadSAT m => NumMonomial -> NumMonomial -> m Boolean +equalsMonomial m1 m2 = do + equalsCoefficient <- F.equals (coefficient m1) (coefficient m2) + equalsExponents <- B.constant $ (exponents m1) == (exponents m2) + B.and [equalsCoefficient,equalsExponents] + +equals :: MonadSAT m => NumPolynomialN -> NumPolynomialN -> m Boolean +equals (PolynomialN []) (PolynomialN []) = B.constant True +equals (PolynomialN (x:xs)) (PolynomialN (y:ys)) = do + e <- equalsMonomial x y + es <- equals (PolynomialN xs) (PolynomialN ys) + B.and [e,es] diff --git a/src/Satchmo/PolynomialSOS.hs b/src/Satchmo/PolynomialSOS.hs new file mode 100644 --- /dev/null +++ b/src/Satchmo/PolynomialSOS.hs @@ -0,0 +1,49 @@ +module Satchmo.PolynomialSOS + +(nonNegative, positive, strictlyMonotone) + +where + +import Prelude hiding (null,and) +import Control.Monad (foldM,replicateM) + +import Satchmo.MonadSAT (MonadSAT) +import Satchmo.Polynomial + (NumPoly,Poly,times,add,polynomial,null,equals,constantTerm,derive) +import Satchmo.Boolean (Boolean,and) +import qualified Satchmo.BinaryTwosComplement.Op.Fixed as F + +sqr :: MonadSAT m => NumPoly -> m NumPoly +sqr p = p `times` p + +sumOfSquares :: MonadSAT m => Int -> Int -> Int -> m NumPoly +sumOfSquares coefficientBitWidth degree numPoly = do + sqrs <- replicateM numPoly + $ polynomial coefficientBitWidth degree >>= sqr + foldM add null sqrs + +nonNegative :: MonadSAT m => Int -- ^ Bit width of coefficients + -> Int -- ^ Maximum degree + -> Int -- ^ Maximum number of polynomials + -> NumPoly -> m Boolean +nonNegative coefficientBitWidth degree numPoly p = do + sos <- sumOfSquares coefficientBitWidth degree numPoly + equals sos p + +positive :: MonadSAT m => Int -- ^ Bit width of coefficients + -> Int -- ^ Maximum degree + -> Int -- ^ Maximum number of polynomials + -> NumPoly -> m Boolean +positive coefficientBitWidth degree numPoly p = do + sos <- sumOfSquares coefficientBitWidth degree numPoly + e1 <- equals sos p + e2 <- F.positive $ constantTerm sos + and [e1, e2] + +strictlyMonotone :: MonadSAT m => Int -- ^ Bit width of coefficients + -> Int -- ^ Maximum degree + -> Int -- ^ Maximum number of polynomials + -> NumPoly -> m Boolean +strictlyMonotone coefficientBitWidth degree numPoly p = do + p' <- derive p + positive coefficientBitWidth degree numPoly p' diff --git a/src/Satchmo/Relation.hs b/src/Satchmo/Relation.hs new file mode 100644 --- /dev/null +++ b/src/Satchmo/Relation.hs @@ -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 diff --git a/src/Satchmo/Relation/Data.hs b/src/Satchmo/Relation/Data.hs new file mode 100644 --- /dev/null +++ b/src/Satchmo/Relation/Data.hs @@ -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 "." + + diff --git a/src/Satchmo/Relation/Op.hs b/src/Satchmo/Relation/Op.hs new file mode 100644 --- /dev/null +++ b/src/Satchmo/Relation/Op.hs @@ -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 + + diff --git a/src/Satchmo/Relation/Prop.hs b/src/Satchmo/Relation/Prop.hs new file mode 100644 --- /dev/null +++ b/src/Satchmo/Relation/Prop.hs @@ -0,0 +1,131 @@ + +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 diff --git a/src/Satchmo/SAT.hs b/src/Satchmo/SAT.hs new file mode 100644 --- /dev/null +++ b/src/Satchmo/SAT.hs @@ -0,0 +1,9 @@ +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 diff --git a/src/Satchmo/SAT/External.hs b/src/Satchmo/SAT/External.hs new file mode 100644 --- /dev/null +++ b/src/Satchmo/SAT/External.hs @@ -0,0 +1,179 @@ +{-# LANGUAGE GeneralizedNewtypeDeriving #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE DoAndIfThenElse #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# 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 diff --git a/src/Satchmo/SAT/Mini.hs b/src/Satchmo/SAT/Mini.hs new file mode 100644 --- /dev/null +++ b/src/Satchmo/SAT/Mini.hs @@ -0,0 +1,157 @@ +{-# LANGUAGE GeneralizedNewtypeDeriving #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE DoAndIfThenElse #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# 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 diff --git a/src/Satchmo/SAT/Tmpfile.hs b/src/Satchmo/SAT/Tmpfile.hs new file mode 100644 --- /dev/null +++ b/src/Satchmo/SAT/Tmpfile.hs @@ -0,0 +1,127 @@ +{-# 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} + diff --git a/src/Satchmo/Set.hs b/src/Satchmo/Set.hs new file mode 100644 --- /dev/null +++ b/src/Satchmo/Set.hs @@ -0,0 +1,10 @@ +module Satchmo.Set + +( module Satchmo.Set.Data +, module Satchmo.Set.Op +) + +where + +import Satchmo.Set.Data +import Satchmo.Set.Op diff --git a/src/Satchmo/Set/Data.hs b/src/Satchmo/Set/Data.hs new file mode 100644 --- /dev/null +++ b/src/Satchmo/Set/Data.hs @@ -0,0 +1,69 @@ +{-# 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) ) + diff --git a/src/Satchmo/Set/Op.hs b/src/Satchmo/Set/Op.hs new file mode 100644 --- /dev/null +++ b/src/Satchmo/Set/Op.hs @@ -0,0 +1,45 @@ +{-# language NoMonomorphismRestriction #-} + +module Satchmo.Set.Op where + +import Satchmo.Set.Data +import qualified Satchmo.Boolean as B +import qualified Satchmo.Counting as C + +import qualified Data.Set as S +import Data.List ( tails ) + +import Control.Monad ( guard, forM, liftM2 ) +import Control.Applicative ( (<$>), (<*>) ) + +null :: (Ord a, B.MonadSAT m) => Set a -> m B.Boolean +null s = B.not <$> B.or ( elems s ) + +equals :: (Ord a, B.MonadSAT m) => Set a -> Set a -> m B.Boolean +equals = all2 B.equals2 + +isSubsetOf :: (Ord a, B.MonadSAT m) => Set a -> Set a -> m B.Boolean +isSubsetOf = all2 $ B.implies + +isSupersetOf :: (Ord a, B.MonadSAT m) => Set a -> Set a -> m B.Boolean +isSupersetOf = flip isSubsetOf + +isSingleton :: (Ord a, B.MonadSAT m) => Set a -> m B.Boolean +isSingleton s = do + C.exactly 1 $ elems s + +isDisjoint :: (Ord a, B.MonadSAT m) => Set a -> Set a -> m B.Boolean +isDisjoint = all2 + $ \ x y -> B.or [ B.not x, B.not y ] + +union :: (Ord a, B.MonadSAT m) => Set a -> Set a -> m (Set a) +union = common2 (B.||) + +intersection :: (Ord a, B.MonadSAT m) => Set a -> Set a -> m (Set a) +intersection = common2 (B.&&) + +difference :: (Ord a, B.MonadSAT m) => Set a -> Set a -> m (Set a) +difference = common2 ( \ x y -> x B.&& (B.not y) ) + + + diff --git a/src/Satchmo/Unary.hs b/src/Satchmo/Unary.hs new file mode 100644 --- /dev/null +++ b/src/Satchmo/Unary.hs @@ -0,0 +1,10 @@ +module Satchmo.Unary + +( module Satchmo.Unary.Data +, module Satchmo.Unary.Op.Flexible +) + +where + +import Satchmo.Unary.Data +import Satchmo.Unary.Op.Flexible diff --git a/src/Satchmo/Unary/Data.hs b/src/Satchmo/Unary/Data.hs new file mode 100644 --- /dev/null +++ b/src/Satchmo/Unary/Data.hs @@ -0,0 +1,55 @@ +{-# language MultiParamTypeClasses #-} +{-# language FlexibleInstances #-} +{-# language FlexibleContexts #-} +{-# language UndecidableInstances #-} + +module Satchmo.Unary.Data + +( Number, bits, make +, width, number, constant ) + +where + +import Prelude hiding ( and, or, not ) + +import qualified Satchmo.Code as C + +import Satchmo.Boolean hiding ( constant ) +import qualified Satchmo.Boolean as B + +import Control.Monad ( forM, when ) + +data Number = Number + { bits :: [ Boolean ] + -- ^ contents is [ 1 .. 1 0 .. 0 ] + -- number of 1 is value of number + } + +instance (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 diff --git a/src/Satchmo/Unary/Op/Common.hs b/src/Satchmo/Unary/Op/Common.hs new file mode 100644 --- /dev/null +++ b/src/Satchmo/Unary/Op/Common.hs @@ -0,0 +1,211 @@ +{-# language NoMonomorphismRestriction #-} +{-# language ScopedTypeVariables #-} + +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 +-- +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) + +-- | +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 + +-- | + +oe_merge [] ys = return ys +oe_merge xs [] = return xs +oe_merge [x] [y] = do + comparator x y +oe_merge xs ys = do + let ( xo, xe ) = divide xs + ( yo, ye ) = divide ys + ~(m : mo) <- oe_merge xo yo + me <- oe_merge xe ye + re <- repair me mo + return $ m : re + +divide (x : xs) = + let ( this, that ) = divide xs + in ( x : that, this ) +divide [] = ( [], [] ) + +repair (x:xs) (y:ys) = do + here <- comparator x y + later <- repair xs ys + return $ here ++ later +repair [] [] = return [] +repair [x] [] = return [x] +repair [] [y] = return [y] + +comparator x y = do + hi <- Satchmo.Boolean.or [x, y] + lo <- Satchmo.Boolean.and [x, y] + return [ hi, lo ] diff --git a/src/Satchmo/Unary/Op/Fixed.hs b/src/Satchmo/Unary/Op/Fixed.hs new file mode 100644 --- /dev/null +++ b/src/Satchmo/Unary/Op/Fixed.hs @@ -0,0 +1,37 @@ +module Satchmo.Unary.Op.Fixed + +( module Satchmo.Unary.Op.Common +, add +, add_quadratic +, add_by_odd_even_merge +, add_by_bitonic_sort +) + +where + +import Prelude hiding ( not, and, or ) +import qualified Prelude + +import Satchmo.Boolean +import Satchmo.Unary.Data +import qualified Satchmo.Unary.Op.Common as C +import Satchmo.Unary.Op.Common hiding + (add_quadratic, add_by_odd_even_merge, add_by_bitonic_sort) + +import Control.Monad ( forM, when, guard ) +import qualified Data.Map as M + +add :: MonadSAT m => Number -> Number -> m Number +add = add_quadratic + +add_quadratic a b = + C.add_quadratic (Just $ Prelude.max ( width a ) ( width b )) a b + +add_by_odd_even_merge a b = + C.add_by_odd_even_merge (Just $ Prelude.max ( width a ) ( width b )) a b + +add_by_bitonic_sort a b = + C.add_by_bitonic_sort (Just $ Prelude.max ( width a ) ( width b )) a b + + + diff --git a/src/Satchmo/Unary/Op/Flexible.hs b/src/Satchmo/Unary/Op/Flexible.hs new file mode 100644 --- /dev/null +++ b/src/Satchmo/Unary/Op/Flexible.hs @@ -0,0 +1,35 @@ +module Satchmo.Unary.Op.Flexible + +( module Satchmo.Unary.Op.Common +, add +, add_quadratic +, add_by_odd_even_merge +, add_by_bitonic_sort +) + +where + +import Prelude hiding ( not, and, or ) +import qualified Prelude + +import Satchmo.Boolean +import Satchmo.Unary.Data +import qualified Satchmo.Unary.Op.Common as C +import Satchmo.Unary.Op.Common hiding + (add_quadratic, add_by_odd_even_merge, add_by_bitonic_sort) + +import Control.Monad ( forM ) +import qualified Data.Map as M + +-- | Unary addition. Output bit length is sum of input bit lengths. +add :: MonadSAT m => Number -> Number -> m Number +add = add_by_odd_even_merge + +add_quadratic a b = + C.add_quadratic (Just $ (+) ( width a ) ( width b )) a b + +add_by_odd_even_merge a b = + C.add_by_odd_even_merge (Just $ (+) ( width a ) ( width b )) a b + +add_by_bitonic_sort a b = + C.add_by_bitonic_sort (Just $ (+) ( width a ) ( width b )) a b