diff --git a/.travis.yml b/.travis.yml --- a/.travis.yml +++ b/.travis.yml @@ -1,12 +1,28 @@ language: haskell +env: + - GHCVER=7.8.3 + before_install: + - | + if [ $GHCVER = `ghc --numeric-version` ]; then + # Try installing some of the build-deps with apt-get for speed. + travis/cabal-apt-install --enable-tests $MODE + export CABAL=cabal + else + # Install the GHC we want from hvr's PPA + travis_retry sudo add-apt-repository -y ppa:hvr/ghc + travis_retry sudo apt-get update + travis_retry sudo apt-get install cabal-install-1.18 ghc-$GHCVER happy + export CABAL=cabal-1.18 + export PATH=/opt/ghc/$GHCVER/bin:$PATH + fi + # Uncomment whenever hackage is down. # - mkdir -p ~/.cabal && cp travis/config ~/.cabal/config && cabal update - cabal update # Try installing some of the build-deps with apt-get for speed. - travis/cabal-apt-install $mode - - cabal install happy packunused packdeps - export PATH=~/.cabal/bin:$PATH install: @@ -15,9 +31,6 @@ script: - $script - - packdeps ersatz.cabal - - packunused - - hlint src --cpp-define HLINT notifications: irc: diff --git a/AUTHORS.md b/AUTHORS.md --- a/AUTHORS.md +++ b/AUTHORS.md @@ -6,6 +6,8 @@ It was revived by [Johan Kiviniemi](mailto:ersatz@johan.kiviniemi.name) [@ion1](https://github.com/ion1) who got it into a working condition by implementing some missing parts, which inspired the original author into polishing it up and releasing it. +Eric Mertens (@glguy](https://github.com/glguy) has been pouring code into it ever since then. + Omission from this page is by no means an attempt to discount your contributions! Thank you for all of your help! -Edward Kmett diff --git a/CHANGELOG.md b/CHANGELOG.md --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1,3 +1,20 @@ +0.3 +----- +* Unified `Encoding` and `Decoding` into `Codec` +* Unified the `forall` and `exists` implementations into a single `literally` + method in `Variable` class. +* Added `Orderable` type class and instances +* Added `Ersatz.Bits.Bits` for variable-sized bit arithmetic. +* Renamed `Ersatz.Bits.half_adder` to `halfAdder` +* Renamed `Ersatz.Bits.full_adder` to `fullAdder` +* Added new examples +* Dropped `blaze` package dependency in favor of newer `bytestring` +* Significantly shrank the number of "Trustworthy" modules +* Added various generic `V1` instances +* Added `Equatable` instances for `Map` and `IntMap` +* Added `Ersatz.BitChar` module for computing with `Char` and `String` +* Wider version bounds for `transformers` and `mtl`. + 0.2.6.1 ----- * Exported `Ersatz.Variable.GVariable` diff --git a/HLint.hs b/HLint.hs deleted file mode 100644 --- a/HLint.hs +++ /dev/null @@ -1,1 +0,0 @@ -import "hint" HLint.Default diff --git a/LICENSE b/LICENSE --- a/LICENSE +++ b/LICENSE @@ -1,4 +1,5 @@ -Copyright © 2010-2014 Edward Kmett +Copyright © 2010-2015 Edward Kmett +Copyright © 2014-2015 Eric Mertens Copyright © 2013 Johan Kiviniemi All rights reserved. diff --git a/ersatz.cabal b/ersatz.cabal --- a/ersatz.cabal +++ b/ersatz.cabal @@ -1,10 +1,10 @@ name: ersatz -version: 0.2.6.1 +version: 0.3 license: BSD3 license-file: LICENSE -author: Edward A. Kmett, Johan Kiviniemi +author: Edward A. Kmett, Eric Mertens, Johan Kiviniemi maintainer: Edward A. Kmett -copyright: © 2010-2014 Edward Kmett, © 2013 Johan Kiviniemi +copyright: © 2010-2015 Edward A. Kmett, © 2014-2015 Eric Mertens, © 2013 Johan Kiviniemi stability: experimental homepage: http://github.com/ekmett/ersatz bug-reports: http://github.com/ekmett/ersatz/issues @@ -82,7 +82,6 @@ .travis.yml AUTHORS.md CHANGELOG.md - HLint.hs README.md notes/SPOILER.html notes/grid.pdf @@ -157,24 +156,28 @@ default: True manual: True +-- You can enable the hlint test suite with -ftest-hlint +flag test-hlint + default: False + manual: True + + library ghc-options: -Wall hs-source-dirs: src default-language: Haskell2010 build-depends: - array >= 0.2 && < 0.6, - base >= 4 && < 5, - blaze-builder == 0.3.*, - blaze-textual == 0.2.*, - bytestring >= 0.9 && < 0.12, - containers >= 0.2.0.1 && < 0.6, - data-default >= 0.5 && < 0.6, - lens >= 3.8 && < 5, - mtl >= 1.1 && < 2.2, - process >= 1.1 && < 1.3, - temporary >= 1.1 && < 1.3, - transformers == 0.3.*, + array >= 0.2 && < 0.6, + base >= 4 && < 5, + bytestring >= 0.10.4.0 && < 0.12, + containers >= 0.2.0.1 && < 0.6, + data-default >= 0.5 && < 0.6, + lens >= 3.8 && < 5, + mtl >= 1.1 && < 2.3, + process >= 1.1 && < 1.3, + temporary >= 1.1 && < 1.3, + transformers >= 0.3 && < 0.5, unordered-containers == 0.2.* if impl(ghc >= 7.4 && < 7.6) @@ -184,11 +187,12 @@ Ersatz Ersatz.Bit Ersatz.Bits - Ersatz.Decoding + Ersatz.BitChar + Ersatz.Codec Ersatz.Equatable - Ersatz.Encoding Ersatz.Internal.Formula Ersatz.Internal.Literal + Ersatz.Orderable Ersatz.Problem Ersatz.Solution Ersatz.Solver @@ -245,26 +249,26 @@ ghc-options: -Wall hs-source-dirs: examples/sudoku -test-suite properties - type: exitcode-stdio-1.0 - ghc-options: -Wall - default-language: Haskell2010 - build-depends: - array, - base < 5, - containers, - data-reify >= 0.5 && < 0.7, - ersatz, - mtl, - transformers, - test-framework >= 0.2.4 && < 0.9, - test-framework-quickcheck >= 0.2.4 && < 0.4, - test-framework-hunit >= 0.2.4 && < 0.4, - QuickCheck >= 1.2.0.0 && < 2.6, - HUnit >= 1.2.2.1 && < 1.3 - - hs-source-dirs: tests - Main-is: properties.hs +-- test-suite properties +-- type: exitcode-stdio-1.0 +-- ghc-options: -Wall +-- default-language: Haskell2010 +-- build-depends: +-- array, +-- base < 5, +-- containers, +-- data-reify >= 0.5 && < 0.7, +-- ersatz, +-- mtl, +-- transformers, +-- test-framework >= 0.2.4 && < 0.9, +-- test-framework-quickcheck >= 0.2.4 && < 0.4, +-- test-framework-hunit >= 0.2.4 && < 0.4, +-- QuickCheck >= 1.2.0.0 && < 2.6, +-- HUnit >= 1.2.2.1 && < 1.3 +-- +-- hs-source-dirs: tests +-- Main-is: properties.hs test-suite doctests type: exitcode-stdio-1.0 @@ -279,3 +283,17 @@ if impl(ghc<7.6.1) ghc-options: -Werror hs-source-dirs: tests + +test-suite hlint + type: exitcode-stdio-1.0 + main-is: hlint.hs + ghc-options: -w -threaded -rtsopts -with-rtsopts=-N + hs-source-dirs: tests + default-language: Haskell2010 + + if !flag(test-hlint) + buildable: False + else + build-depends: + base, + hlint >= 1.7 diff --git a/examples/regexp-grid/RegexpGrid/Types.hs b/examples/regexp-grid/RegexpGrid/Types.hs --- a/examples/regexp-grid/RegexpGrid/Types.hs +++ b/examples/regexp-grid/RegexpGrid/Types.hs @@ -37,12 +37,9 @@ instance Variable Field instance Equatable Field -instance Decoding Field where +instance Codec Field where type Decoded Field = Char decode s (Field f) = chr . (+ origin) . fromIntegral <$> decode s f - -instance Encoding Field where - type Encoded Field = Char encode = Field . encode . fromIntegral . subtract origin . ord -- Encode 0 as the character preceding A. diff --git a/examples/sudoku/Sudoku/Cell.hs b/examples/sudoku/Sudoku/Cell.hs --- a/examples/sudoku/Sudoku/Cell.hs +++ b/examples/sudoku/Sudoku/Cell.hs @@ -18,11 +18,8 @@ instance Variable Cell instance Equatable Cell -instance Decoding Cell where +instance Codec Cell where type Decoded Cell = Word8 decode s (Cell b) = decode s b - -instance Encoding Cell where - type Encoded Cell = Word8 encode n | 1 <= n && n <= 9 = Cell (encode n) | otherwise = error ("Cell encode: invalid value " ++ show n) diff --git a/src/Ersatz.hs b/src/Ersatz.hs --- a/src/Ersatz.hs +++ b/src/Ersatz.hs @@ -11,9 +11,9 @@ module Ersatz ( module Ersatz.Bit , module Ersatz.Bits - , module Ersatz.Decoding + , module Ersatz.Codec , module Ersatz.Equatable - , module Ersatz.Encoding + , module Ersatz.Orderable , module Ersatz.Problem , module Ersatz.Solution , module Ersatz.Solver @@ -22,9 +22,9 @@ import Ersatz.Bit import Ersatz.Bits -import Ersatz.Decoding +import Ersatz.Codec import Ersatz.Equatable -import Ersatz.Encoding +import Ersatz.Orderable import Ersatz.Problem import Ersatz.Solution import Ersatz.Solver diff --git a/src/Ersatz/Bit.hs b/src/Ersatz/Bit.hs --- a/src/Ersatz/Bit.hs +++ b/src/Ersatz/Bit.hs @@ -1,6 +1,5 @@ {-# LANGUAGE CPP #-} {-# LANGUAGE TypeFamilies #-} -{-# LANGUAGE DeriveGeneric #-} {-# LANGUAGE TypeOperators #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE DefaultSignatures #-} @@ -34,8 +33,7 @@ import Data.Sequence (Seq, (<|), (|>), (><)) import qualified Data.Sequence as Seq import Data.Typeable -import Ersatz.Decoding -import Ersatz.Encoding +import Ersatz.Codec import Ersatz.Internal.Formula import Ersatz.Internal.Literal import Ersatz.Internal.StableName @@ -110,16 +108,15 @@ choose f t s = Mux f t s instance Variable Bit where - exists = liftM Var exists -#ifndef HLINT - forall = liftM Var forall -#endif + literally = liftM Var . literally -- a Bit you don't assert is actually a boolean function that you can evaluate later after compilation -instance Decoding Bit where +instance Codec Bit where type Decoded Bit = Bool + encode = bool decode sol b - = solutionStableName sol (unsafePerformIO (makeStableName' b)) + = maybe (pure False <|> pure True) pure $ + solutionStableName sol (unsafePerformIO (makeStableName' b)) -- The StableName didn’t have an associated literal with a solution, -- recurse to compute the value. <|> case b of @@ -154,10 +151,6 @@ go Nothing ~(ns, js) = (():ns, js) go (Just a) ~(ns, js) = (ns, a:js) -instance Encoding Bit where - type Encoded Bit = Bool - encode = bool - -- | Assert claims that 'Bit' must be 'true' in any satisfying interpretation -- of the current problem. assert :: (MonadState s m, HasSAT s) => Bit -> m () @@ -188,6 +181,15 @@ gall :: Foldable t => (a -> f b) -> t a -> f b gany :: Foldable t => (a -> f b) -> t a -> f b gxor :: f a -> f a -> f a + +instance GBoolean V1 where + gbool x = x `seq` error "GBoolean[V1].gbool" + x &&# y = x `seq` y `seq` error "GBoolean[V1].&&#" + x ||# y = x `seq` y `seq` error "GBoolean[V1].||#" + gnot x = x `seq` error "GBoolean[V1].gnot" + gall x y = x `seq` y `seq` error "GBoolean[V1].gall" + gany x y = x `seq` y `seq` error "GBoolean[V1].gany" + gxor x y = x `seq` y `seq` error "GBoolean[V1].gxor" instance GBoolean U1 where gbool _ = U1 diff --git a/src/Ersatz/BitChar.hs b/src/Ersatz/BitChar.hs new file mode 100644 --- /dev/null +++ b/src/Ersatz/BitChar.hs @@ -0,0 +1,56 @@ +{-# LANGUAGE DeriveDataTypeable #-} +{-# LANGUAGE TypeFamilies #-} +-------------------------------------------------------------------- +-- | +-- Copyright : © Eric Mertens 2010-2014 +-- License : BSD3 +-- Maintainer: Edward Kmett +-- Stability : experimental +-- Portability: non-portable +-- +-------------------------------------------------------------------- +module Ersatz.BitChar where + +import Data.Char (chr,ord) +import Control.Monad (liftM, replicateM) +import Prelude hiding ((&&)) +import Data.Typeable (Typeable) + +import Ersatz.Bit +import Ersatz.Bits +import Ersatz.Codec +import Ersatz.Equatable +import Ersatz.Orderable +import Ersatz.Variable + +-- | List of 'BitChar' intended to be used as the representation for 'String'. +type BitString = [BitChar] + +-- | Encoding of the full range of 'Char' values. +newtype BitChar = BitChar Bits + deriving (Show,Typeable) + +instance Codec BitChar where + type Decoded BitChar = Char + encode = BitChar . fromIntegral . ord + decode s (BitChar xs) = liftM (chr . fromIntegral) (decode s xs) + +instance Equatable BitChar where + BitChar xs === BitChar ys = xs === ys + BitChar xs /== BitChar ys = xs /== ys + +instance Orderable BitChar where + BitChar xs -- Stability : experimental -- Portability: non-portable -- +-- 'Bits' is an arbitrary length natural number type -------------------------------------------------------------------- module Ersatz.Bits - ( Bit1(..), Bit2(..), Bit3(..), Bit4(..), Bit5(..), Bit6(..), Bit7(..), Bit8(..) - , full_adder, half_adder + ( + -- * Fixed length bit vectors + Bit1(..), Bit2(..), Bit3(..), Bit4(..), Bit5(..), Bit6(..), Bit7(..), Bit8(..) + -- * Variable length bit vectors + , Bits(Bits) + , HasBits(..) + , isEven + , isOdd + , sumBit + , sumBits + -- * Adders + , fullAdder, halfAdder ) where -import Prelude hiding ((&&), (||), and, or, not) - import Control.Applicative -import Data.Bits (Bits, (.&.), (.|.), shiftL, shiftR) -import Data.List (foldl') -import Data.Typeable +import Control.Monad.Trans.State (State, runState, get, put) +import Data.Bits ((.&.), (.|.), shiftL, shiftR) +import qualified Data.Bits as Data +import Data.Foldable (Foldable, toList) +import Data.List (unfoldr, foldl') +import Data.Traversable (traverse) +import Data.Typeable (Typeable) import Data.Word (Word8) import Ersatz.Bit -import Ersatz.Decoding +import Ersatz.Codec import Ersatz.Equatable -import Ersatz.Encoding +import Ersatz.Orderable import Ersatz.Variable import GHC.Generics +import Prelude hiding (and, or, not, (&&), (||)) -- | A container of 1 'Bit' that 'encode's from and 'decode's to 'Word8' newtype Bit1 = Bit1 Bit deriving (Show,Typeable,Generic) @@ -65,6 +79,15 @@ instance Equatable Bit7 instance Equatable Bit8 +instance Orderable Bit1 +instance Orderable Bit2 +instance Orderable Bit3 +instance Orderable Bit4 +instance Orderable Bit5 +instance Orderable Bit6 +instance Orderable Bit7 +instance Orderable Bit8 + instance Variable Bit1 instance Variable Bit2 instance Variable Bit3 @@ -74,68 +97,44 @@ instance Variable Bit7 instance Variable Bit8 -instance Decoding Bit1 where +instance Codec Bit1 where type Decoded Bit1 = Word8 decode s (Bit1 a) = boolsToNum1 <$> decode s a + encode i = Bit1 a where (a:_) = bitsOf i -instance Decoding Bit2 where +instance Codec Bit2 where type Decoded Bit2 = Word8 decode s (Bit2 a b) = boolsToNum2 <$> decode s a <*> decode s b + encode i = Bit2 a b where (b:a:_) = bitsOf i -instance Decoding Bit3 where +instance Codec Bit3 where type Decoded Bit3 = Word8 decode s (Bit3 a b c) = boolsToNum3 <$> decode s a <*> decode s b <*> decode s c + encode i = Bit3 a b c where (c:b:a:_) = bitsOf i -instance Decoding Bit4 where +instance Codec Bit4 where type Decoded Bit4 = Word8 decode s (Bit4 a b c d) = boolsToNum4 <$> decode s a <*> decode s b <*> decode s c <*> decode s d + encode i = Bit4 a b c d where (d:c:b:a:_) = bitsOf i -instance Decoding Bit5 where +instance Codec Bit5 where type Decoded Bit5 = Word8 decode s (Bit5 a b c d e) = boolsToNum5 <$> decode s a <*> decode s b <*> decode s c <*> decode s d <*> decode s e + encode i = Bit5 a b c d e where (e:d:c:b:a:_) = bitsOf i -instance Decoding Bit6 where +instance Codec Bit6 where type Decoded Bit6 = Word8 decode s (Bit6 a b c d e f) = boolsToNum6 <$> decode s a <*> decode s b <*> decode s c <*> decode s d <*> decode s e <*> decode s f + encode i = Bit6 a b c d e f where (f:e:d:c:b:a:_) = bitsOf i -instance Decoding Bit7 where +instance Codec Bit7 where type Decoded Bit7 = Word8 decode s (Bit7 a b c d e f g) = boolsToNum7 <$> decode s a <*> decode s b <*> decode s c <*> decode s d <*> decode s e <*> decode s f <*> decode s g + encode i = Bit7 a b c d e f g where (g:f:e:d:c:b:a:_) = bitsOf i -instance Decoding Bit8 where +instance Codec Bit8 where type Decoded Bit8 = Word8 decode s (Bit8 a b c d e f g h) = boolsToNum8 <$> decode s a <*> decode s b <*> decode s c <*> decode s d <*> decode s e <*> decode s f <*> decode s g <*> decode s h - -instance Encoding Bit1 where - type Encoded Bit1 = Word8 - encode i = Bit1 a where (a:_) = bitsOf i - -instance Encoding Bit2 where - type Encoded Bit2 = Word8 - encode i = Bit2 a b where (b:a:_) = bitsOf i - -instance Encoding Bit3 where - type Encoded Bit3 = Word8 - encode i = Bit3 a b c where (c:b:a:_) = bitsOf i - -instance Encoding Bit4 where - type Encoded Bit4 = Word8 - encode i = Bit4 a b c d where (d:c:b:a:_) = bitsOf i - -instance Encoding Bit5 where - type Encoded Bit5 = Word8 - encode i = Bit5 a b c d e where (e:d:c:b:a:_) = bitsOf i - -instance Encoding Bit6 where - type Encoded Bit6 = Word8 - encode i = Bit6 a b c d e f where (f:e:d:c:b:a:_) = bitsOf i - -instance Encoding Bit7 where - type Encoded Bit7 = Word8 - encode i = Bit7 a b c d e f g where (g:f:e:d:c:b:a:_) = bitsOf i - -instance Encoding Bit8 where - type Encoded Bit8 = Word8 encode i = Bit8 a b c d e f g h where (h:g:f:e:d:c:b:a:_) = bitsOf i boolsToNum1 :: Bool -> Word8 @@ -162,7 +161,7 @@ boolsToNum8 :: Bool -> Bool -> Bool -> Bool -> Bool -> Bool -> Bool -> Bool -> Word8 boolsToNum8 a b c d e f g h = boolsToNum [a,b,c,d,e,f,g,h] -bitsOf :: (Num a, Bits a) => a -> [Bit] +bitsOf :: (Num a, Data.Bits a) => a -> [Bit] bitsOf n = bool (numToBool (n .&. 1)) : bitsOf (n `shiftR` 1) {-# INLINE bitsOf #-} @@ -171,7 +170,7 @@ numToBool _ = True {-# INLINE numToBool #-} -boolsToNum :: (Num a, Bits a) => [Bool] -> a +boolsToNum :: (Num a, Data.Bits a) => [Bool] -> a boolsToNum = foldl' (\n a -> (n `shiftL` 1) .|. boolToNum a) 0 {-# INLINE boolsToNum #-} @@ -189,18 +188,20 @@ signum a = a fromInteger = Bit1 . bool . odd -full_adder :: Bit -> Bit -> Bit -> (Bit, Bit) -full_adder a b cin = (s2, c1 || c2) - where (s1,c1) = half_adder a b - (s2,c2) = half_adder s1 cin +-- | Compute the sum and carry bit from adding three bits. +fullAdder :: Bit -> Bit -> Bit -> (Bit, Bit) -- ^ (sum, carry) +fullAdder a b cin = (s2, c1 || c2) + where (s1,c1) = halfAdder a b + (s2,c2) = halfAdder s1 cin -half_adder :: Bit -> Bit -> (Bit, Bit) -half_adder a b = (a `xor` b, a && b) +-- | Compute the sum and carry bit from adding two bits. +halfAdder :: Bit -> Bit -> (Bit, Bit) -- ^ (sum, carry) +halfAdder a b = (a `xor` b, a && b) instance Num Bit2 where Bit2 a2 a1 + Bit2 b2 b1 = Bit2 s2 s1 where - (s1,c2) = half_adder a1 b1 - (s2,_) = full_adder a2 b2 c2 + (s1,c2) = halfAdder a1 b1 + (s2,_) = fullAdder a2 b2 c2 Bit2 a2 a1 * Bit2 b2 b1 = Bit2 ((a1 && b2) `xor` (a2 && b1)) (a1 && b1) -- wallace tree -- @@ -217,3 +218,186 @@ abs a = a signum (Bit2 a b) = Bit2 false (a || b) fromInteger k = Bit2 (bool (k .&. 2 /= 0)) (bool (k .&. 1 /= 0)) + +-- suitable for comparisons and arithmetic. Bits are stored +-- in little-endian order to enable phantom 'false' values +-- to be truncated. +newtype Bits = Bits { _getBits :: [Bit] } + deriving Typeable + +instance Show Bits where + showsPrec d (Bits xs) = showParen (d > 10) $ + showString "Bits " . showsPrec 11 xs + +instance Equatable Bits where + Bits xs === Bits ys = and (zipWithBits (===) xs ys) + Bits xs /== Bits ys = or (zipWithBits (/==) xs ys) + +-- | Zip the component bits of a 'Bits' extending the +-- shorter argument with 'false' values. +zipWithBits :: (Bit -> Bit -> a) -> [Bit] -> [Bit] -> [a] +zipWithBits _ [] [] = [] +zipWithBits f (x:xs) (y:ys) = f x y : zipWithBits f xs ys +zipWithBits f xs [] = map (`f` false) xs +zipWithBits f [] ys = map (false `f`) ys + +instance Orderable Bits where + Bits xs [Bit] -> [Bit] -> Bit +orderHelper c0 xs ys = foldl aux c0 (zipWithBits (,) xs ys) + where + aux c (x,y) = c && x === y || x if x then 1 else 0) ys + -- Integers to Integer + return (foldr (\x acc -> x + 2 * acc) 0 zs) + + encode = Bits . unfoldr step + where + step x = + case compare x 0 of + LT -> error "Bits/encode: Negative number" + EQ -> Nothing + GT -> Just (if odd x then true else false, x `div` 2) + +unbits :: HasBits a => a -> [Bit] +unbits a = case bits a of Bits xs -> xs + +-- | Add two 'Bits' values given an incoming carry bit. +addBits :: (HasBits a, HasBits b) => Bit -> a -> b -> Bits +addBits c xs0 ys0 = Bits (add2 c (unbits xs0) (unbits ys0)) where + add2 cin [] ys = add1 cin ys + add2 cin xs [] = add1 cin xs + add2 cin (x:xs) (y:ys)= s : add2 cout xs ys where + (s,cout) = fullAdder x y cin + + add1 cin [] = [cin] + add1 cin (x:xs) = s : add1 cout xs where + (s,cout) = halfAdder cin x + +-- | Compute the sum of a source of 'Bits' values. +sumBits :: (Foldable t, HasBits a) => t a -> Bits +sumBits = sumBits' . map bits . toList + +sumBits' :: [Bits] -> Bits +sumBits' [] = Bits [] +sumBits' [x] = x +sumBits' xs0 = sumBits (merge xs0) where + merge [x] = [x] + merge [] = [] + merge (x1:x2:xs) = addBits false x1 x2 : merge xs + +-- | Optimization of 'sumBits' enabled when summing +-- individual 'Bit's. +sumBit :: Foldable t => t Bit -> Bits +sumBit t = + case runState (merge (map bits h2)) h1 of + (s,[]) -> s + _ -> error "Bits.betterSumBits: OOPS! Bad algorithm!" + + where + ts = toList t + (h1,h2) = splitAt ((length ts-1) `div` 2) ts + + spareBit = do + xs <- get + case xs of + [] -> return false + y:ys -> put ys >> return y + + merge :: [Bits] -> State [Bit] Bits + merge [x] = return x + merge [] = return (Bits []) + merge xs = merge =<< merge' xs + + merge' :: [Bits] -> State [Bit] [Bits] + merge' [] = return [] + merge' [x] = return [x] + merge' (x1:x2:xs) = + do cin <- spareBit + xs' <- merge' xs + return (addBits cin x1 x2 : xs') + +-- | Predicate for odd-valued 'Bits's. +isOdd :: HasBits b => b -> Bit +isOdd b = case unbits b of + [] -> false + (x:_) -> x + +-- | Predicate for even-valued 'Bits's. +isEven :: HasBits b => b -> Bit +isEven = not . isOdd + +-- | 'HasBits' provides the 'bits' method for embedding +-- fixed with numeric encoding types into the arbitrary width +-- 'Bits' type. +class HasBits a where + bits :: a -> Bits + +instance HasBits Bit where + bits x = Bits [x] + +instance HasBits Bit1 where + bits (Bit1 x0) = Bits [x0] + +instance HasBits Bit2 where + bits (Bit2 x1 x0) = Bits [x0,x1] + +instance HasBits Bit3 where + bits (Bit3 x2 x1 x0) = Bits [x0,x1,x2] + +instance HasBits Bit4 where + bits (Bit4 x3 x2 x1 x0) = Bits [x0,x1,x2,x3] + +instance HasBits Bit5 where + bits (Bit5 x4 x3 x2 x1 x0) = Bits [x0,x1,x2,x3,x4] + +instance HasBits Bit6 where + bits (Bit6 x5 x4 x3 x2 x1 x0) = Bits [x0,x1,x2,x3,x4,x5] + +instance HasBits Bit7 where + bits (Bit7 x6 x5 x4 x3 x2 x1 x0) = Bits [x0,x1,x2,x3,x4,x5,x6] + +instance HasBits Bit8 where + bits (Bit8 x7 x6 x5 x4 x3 x2 x1 x0) = Bits [x0,x1,x2,x3,x4,x5,x6,x7] + +instance HasBits Bits where + bits = id + +mulBits :: Bits -> Bits -> Bits +mulBits (Bits xs) (Bits ys0) + = sumBits + $ zipWith aux xs (iterate times2 ys0) + where + times2 = (false:) + aux x ys = Bits (map (x &&) ys) + +instance Num Bits where + (+) = addBits false + (*) = mulBits + (-) = subBits + fromInteger = encode + signum (Bits xs) = Bits [or xs] + abs x = x + +fullSubtract :: Bit -> Bit -> Bit -> (Bit,Bit) +fullSubtract c x y = + (x `xor` y `xor` c, x && y && c || not x && y || not x && c) + +subBits :: (HasBits a, HasBits b) => a -> b -> Bits +subBits xs0 ys0 = Bits (map (not cN &&) ss) where + (cN, ss) = aux false (unbits xs0) (unbits ys0) + + aux c [] [] = (c, []) + aux c [] ys = aux c [false] ys + aux c xs [] = aux c xs [false] + aux c (x:xs) (y:ys) = fmap (z :) (aux cout xs ys) where + (z,cout) = fullSubtract c x y diff --git a/src/Ersatz/Codec.hs b/src/Ersatz/Codec.hs new file mode 100644 --- /dev/null +++ b/src/Ersatz/Codec.hs @@ -0,0 +1,128 @@ +{-# LANGUAGE Rank2Types #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE Safe #-} +-------------------------------------------------------------------- +-- | +-- Copyright : © Edward Kmett 2010-2014, Johan Kiviniemi 2013 +-- License : BSD3 +-- Maintainer: Edward Kmett +-- Stability : experimental +-- Portability: non-portable +-- +-------------------------------------------------------------------- +module Ersatz.Codec + ( Codec(..) + ) where + +import Control.Applicative +import Control.Monad hiding (mapM) +import Data.Array +import Data.HashMap.Lazy (HashMap) +import Data.IntMap (IntMap) +import Data.Map (Map) +import Data.Sequence (Seq) +import Data.Traversable +import Data.Tree (Tree) +import Ersatz.Internal.Literal +import Ersatz.Solution +import Prelude hiding (mapM) + +-- | This class describes data types that can be marshaled to or from a SAT solver. +class Codec a where + type Decoded a :: * + -- | Return a value based on the solution if one can be determined. + decode :: (Alternative f, MonadPlus f) => Solution -> a -> f (Decoded a) + encode :: Decoded a -> a + +instance Codec Literal where + type Decoded Literal = Bool + decode s a = maybe (pure False <|> pure True) pure (solutionLiteral s a) + encode True = literalTrue + encode False = literalFalse + +instance Codec () where + type Decoded () = () + decode _ () = pure () + encode () = () + +instance (Codec a, Codec b) => Codec (a,b) where + type Decoded (a,b) = (Decoded a, Decoded b) + decode s (a,b) = (,) <$> decode s a <*> decode s b + encode (a,b) = (encode a, encode b) + +instance (Codec a, Codec b, Codec c) => Codec (a,b,c) where + type Decoded (a,b,c) = (Decoded a, Decoded b, Decoded c) + decode s (a,b,c) = (,,) <$> decode s a <*> decode s b <*> decode s c + encode (a,b,c) = (encode a, encode b, encode c) + +instance (Codec a, Codec b, Codec c, Codec d) => Codec (a,b,c,d) where + type Decoded (a,b,c,d) = (Decoded a, Decoded b, Decoded c, Decoded d) + decode s (a,b,c,d) = (,,,) <$> decode s a <*> decode s b <*> decode s c <*> decode s d + encode (a,b,c,d) = (encode a, encode b, encode c, encode d) + +instance (Codec a, Codec b, Codec c, Codec d, Codec e) => Codec (a,b,c,d,e) where + type Decoded (a,b,c,d,e) = (Decoded a, Decoded b, Decoded c, Decoded d, Decoded e) + decode s (a,b,c,d,e) = (,,,,) <$> decode s a <*> decode s b <*> decode s c <*> decode s d <*> decode s e + encode (a,b,c,d,e) = (encode a, encode b, encode c, encode d, encode e) + +instance (Codec a, Codec b, Codec c, Codec d, Codec e, Codec f) => Codec (a,b,c,d,e,f) where + type Decoded (a,b,c,d,e,f) = (Decoded a, Decoded b, Decoded c, Decoded d, Decoded e, Decoded f) + decode s (a,b,c,d,e,f) = (,,,,,) <$> decode s a <*> decode s b <*> decode s c <*> decode s d <*> decode s e <*> decode s f + encode (a,b,c,d,e,f) = (encode a, encode b, encode c, encode d, encode e, encode f) + +instance (Codec a, Codec b, Codec c, Codec d, Codec e, Codec f, Codec g) => Codec (a,b,c,d,e,f,g) where + type Decoded (a,b,c,d,e,f,g) = (Decoded a, Decoded b, Decoded c, Decoded d, Decoded e, Decoded f, Decoded g) + decode s (a,b,c,d,e,f,g) = (,,,,,,) <$> decode s a <*> decode s b <*> decode s c <*> decode s d <*> decode s e <*> decode s f <*> decode s g + encode (a,b,c,d,e,f,g) = (encode a, encode b, encode c, encode d, encode e, encode f, encode g) + +instance (Codec a, Codec b, Codec c, Codec d, Codec e, Codec f, Codec g, Codec h) => Codec (a,b,c,d,e,f,g,h) where + type Decoded (a,b,c,d,e,f,g,h) = (Decoded a, Decoded b, Decoded c, Decoded d, Decoded e, Decoded f, Decoded g, Decoded h) + decode s (a,b,c,d,e,f,g,h) = (,,,,,,,) <$> decode s a <*> decode s b <*> decode s c <*> decode s d <*> decode s e <*> decode s f <*> decode s g <*> decode s h + encode (a,b,c,d,e,f,g,h) = (encode a, encode b, encode c, encode d, encode e, encode f, encode g, encode h) + +instance Codec a => Codec [a] where + type Decoded [a] = [Decoded a] + decode = mapM . decode + encode = map encode + +instance (Ix i, Codec e) => Codec (Array i e) where + type Decoded (Array i e) = Array i (Decoded e) + decode = mapM . decode + encode = fmap encode + +instance (Codec a, Codec b) => Codec (Either a b) where + type Decoded (Either a b) = Either (Decoded a) (Decoded b) + decode s (Left a) = Left <$> decode s a + decode s (Right b) = Right <$> decode s b + encode (Left a) = Left (encode a) + encode (Right b) = Right (encode b) + +instance Codec a => Codec (HashMap k a) where + type Decoded (HashMap k a) = HashMap k (Decoded a) + decode = mapM . decode + encode = fmap encode + +instance Codec a => Codec (IntMap a) where + type Decoded (IntMap a) = IntMap (Decoded a) + decode = mapM . decode + encode = fmap encode + +instance Codec a => Codec (Map k a) where + type Decoded (Map k a) = Map k (Decoded a) + decode = mapM . decode + encode = fmap encode + +instance Codec a => Codec (Maybe a) where + type Decoded (Maybe a) = Maybe (Decoded a) + decode = mapM . decode + encode = fmap encode + +instance Codec a => Codec (Seq a) where + type Decoded (Seq a) = Seq (Decoded a) + decode = mapM . decode + encode = fmap encode + +instance Codec a => Codec (Tree a) where + type Decoded (Tree a) = Tree (Decoded a) + decode = mapM . decode + encode = fmap encode diff --git a/src/Ersatz/Decoding.hs b/src/Ersatz/Decoding.hs deleted file mode 100644 --- a/src/Ersatz/Decoding.hs +++ /dev/null @@ -1,104 +0,0 @@ -{-# LANGUAGE Rank2Types #-} -{-# LANGUAGE TypeFamilies #-} -{-# LANGUAGE Safe #-} --------------------------------------------------------------------- --- | --- Copyright : © Edward Kmett 2010-2014, Johan Kiviniemi 2013 --- License : BSD3 --- Maintainer: Edward Kmett --- Stability : experimental --- Portability: non-portable --- --------------------------------------------------------------------- -module Ersatz.Decoding - ( Decoding(..) - ) where - -import Control.Applicative -import Data.Array -import Data.HashMap.Lazy (HashMap) -import Data.IntMap (IntMap) -import Data.Map (Map) -import Data.Sequence (Seq) -import Data.Traversable -import Data.Tree (Tree) -import Ersatz.Internal.Literal -import Ersatz.Solution - -class Decoding a where - type Decoded a :: * - -- | Return a value based on the solution if one can be determined. - decode :: Solution -> a -> Maybe (Decoded a) - -instance Decoding Literal where - type Decoded Literal = Bool - decode = solutionLiteral - -instance Decoding () where - type Decoded () = () - decode _ () = Just () - -instance (Decoding a, Decoding b) => Decoding (a,b) where - type Decoded (a,b) = (Decoded a, Decoded b) - decode s (a,b) = (,) <$> decode s a <*> decode s b - -instance (Decoding a, Decoding b, Decoding c) => Decoding (a,b,c) where - type Decoded (a,b,c) = (Decoded a, Decoded b, Decoded c) - decode s (a,b,c) = (,,) <$> decode s a <*> decode s b <*> decode s c - -instance (Decoding a, Decoding b, Decoding c, Decoding d) => Decoding (a,b,c,d) where - type Decoded (a,b,c,d) = (Decoded a, Decoded b, Decoded c, Decoded d) - decode s (a,b,c,d) = (,,,) <$> decode s a <*> decode s b <*> decode s c <*> decode s d - -instance (Decoding a, Decoding b, Decoding c, Decoding d, Decoding e) => Decoding (a,b,c,d,e) where - type Decoded (a,b,c,d,e) = (Decoded a, Decoded b, Decoded c, Decoded d, Decoded e) - decode s (a,b,c,d,e) = (,,,,) <$> decode s a <*> decode s b <*> decode s c <*> decode s d <*> decode s e - -instance (Decoding a, Decoding b, Decoding c, Decoding d, Decoding e, Decoding f) => Decoding (a,b,c,d,e,f) where - type Decoded (a,b,c,d,e,f) = (Decoded a, Decoded b, Decoded c, Decoded d, Decoded e, Decoded f) - decode s (a,b,c,d,e,f) = (,,,,,) <$> decode s a <*> decode s b <*> decode s c <*> decode s d <*> decode s e <*> decode s f - -instance (Decoding a, Decoding b, Decoding c, Decoding d, Decoding e, Decoding f, Decoding g) => Decoding (a,b,c,d,e,f,g) where - type Decoded (a,b,c,d,e,f,g) = (Decoded a, Decoded b, Decoded c, Decoded d, Decoded e, Decoded f, Decoded g) - decode s (a,b,c,d,e,f,g) = (,,,,,,) <$> decode s a <*> decode s b <*> decode s c <*> decode s d <*> decode s e <*> decode s f <*> decode s g - -instance (Decoding a, Decoding b, Decoding c, Decoding d, Decoding e, Decoding f, Decoding g, Decoding h) => Decoding (a,b,c,d,e,f,g,h) where - type Decoded (a,b,c,d,e,f,g,h) = (Decoded a, Decoded b, Decoded c, Decoded d, Decoded e, Decoded f, Decoded g, Decoded h) - decode s (a,b,c,d,e,f,g,h) = (,,,,,,,) <$> decode s a <*> decode s b <*> decode s c <*> decode s d <*> decode s e <*> decode s f <*> decode s g <*> decode s h - -instance Decoding a => Decoding [a] where - type Decoded [a] = [Decoded a] - decode = traverse . decode - -instance (Ix i, Decoding e) => Decoding (Array i e) where - type Decoded (Array i e) = Array i (Decoded e) - decode = traverse . decode - -instance (Decoding a, Decoding b) => Decoding (Either a b) where - type Decoded (Either a b) = Either (Decoded a) (Decoded b) - decode s (Left a) = Left <$> decode s a - decode s (Right b) = Right <$> decode s b - -instance Decoding a => Decoding (HashMap k a) where - type Decoded (HashMap k a) = HashMap k (Decoded a) - decode = traverse . decode - -instance Decoding a => Decoding (IntMap a) where - type Decoded (IntMap a) = IntMap (Decoded a) - decode = traverse . decode - -instance Decoding a => Decoding (Map k a) where - type Decoded (Map k a) = Map k (Decoded a) - decode = traverse . decode - -instance Decoding a => Decoding (Maybe a) where - type Decoded (Maybe a) = Maybe (Decoded a) - decode = traverse . decode - -instance Decoding a => Decoding (Seq a) where - type Decoded (Seq a) = Seq (Decoded a) - decode = traverse . decode - -instance Decoding a => Decoding (Tree a) where - type Decoded (Tree a) = Tree (Decoded a) - decode = traverse . decode diff --git a/src/Ersatz/Encoding.hs b/src/Ersatz/Encoding.hs deleted file mode 100644 --- a/src/Ersatz/Encoding.hs +++ /dev/null @@ -1,103 +0,0 @@ -{-# LANGUAGE Rank2Types #-} -{-# LANGUAGE TypeFamilies #-} --------------------------------------------------------------------- --- | --- Copyright : © Edward Kmett 2010-2014, Johan Kiviniemi 2013 --- License : BSD3 --- Maintainer: Edward Kmett --- Stability : experimental --- Portability: non-portable --- --------------------------------------------------------------------- -module Ersatz.Encoding - ( Encoding(..) - ) where - -import Data.Array -import Data.HashMap.Lazy (HashMap) -import Data.IntMap (IntMap) -import Data.Map (Map) -import Data.Sequence (Seq) -import Data.Tree (Tree) -import Ersatz.Internal.Literal - -class Encoding a where - type Encoded a :: * - -- | A counterpart to 'Ersatz.Decoding.decode'. Can encode e.g. a 'Bool' as a - -- 'Ersatz.Bit.Bit', a 'Data.Word.Word8' as a 'Ersatz.Bits.Bit8', or a - -- @[Word8]@ as a @[Bit8]@. - encode :: Encoded a -> a - -instance Encoding Literal where - type Encoded Literal = Bool - encode False = literalFalse - encode True = literalTrue - -instance Encoding () where - type Encoded () = () - encode () = () - -instance (Encoding a, Encoding b) => Encoding (a,b) where - type Encoded (a,b) = (Encoded a, Encoded b) - encode (a,b) = (encode a, encode b) - -instance (Encoding a, Encoding b, Encoding c) => Encoding (a,b,c) where - type Encoded (a,b,c) = (Encoded a, Encoded b, Encoded c) - encode (a,b,c) = (encode a, encode b, encode c) - -instance (Encoding a, Encoding b, Encoding c, Encoding d) => Encoding (a,b,c,d) where - type Encoded (a,b,c,d) = (Encoded a, Encoded b, Encoded c, Encoded d) - encode (a,b,c,d) = (encode a, encode b, encode c, encode d) - -instance (Encoding a, Encoding b, Encoding c, Encoding d, Encoding e) => Encoding (a,b,c,d,e) where - type Encoded (a,b,c,d,e) = (Encoded a, Encoded b, Encoded c, Encoded d, Encoded e) - encode (a,b,c,d,e) = (encode a, encode b, encode c, encode d, encode e) - -instance (Encoding a, Encoding b, Encoding c, Encoding d, Encoding e, Encoding f) => Encoding (a,b,c,d,e,f) where - type Encoded (a,b,c,d,e,f) = (Encoded a, Encoded b, Encoded c, Encoded d, Encoded e, Encoded f) - encode (a,b,c,d,e,f) = (encode a, encode b, encode c, encode d, encode e, encode f) - -instance (Encoding a, Encoding b, Encoding c, Encoding d, Encoding e, Encoding f, Encoding g) => Encoding (a,b,c,d,e,f,g) where - type Encoded (a,b,c,d,e,f,g) = (Encoded a, Encoded b, Encoded c, Encoded d, Encoded e, Encoded f, Encoded g) - encode (a,b,c,d,e,f,g) = (encode a, encode b, encode c, encode d, encode e, encode f, encode g) - -instance (Encoding a, Encoding b, Encoding c, Encoding d, Encoding e, Encoding f, Encoding g, Encoding h) => Encoding (a,b,c,d,e,f,g,h) where - type Encoded (a,b,c,d,e,f,g,h) = (Encoded a, Encoded b, Encoded c, Encoded d, Encoded e, Encoded f, Encoded g, Encoded h) - encode (a,b,c,d,e,f,g,h) = (encode a, encode b, encode c, encode d, encode e, encode f, encode g, encode h) - -instance Encoding a => Encoding [a] where - type Encoded [a] = [Encoded a] - encode = fmap encode - -instance (Ix i, Encoding e) => Encoding (Array i e) where - type Encoded (Array i e) = Array i (Encoded e) - encode = fmap encode - -instance (Encoding a, Encoding b) => Encoding (Either a b) where - type Encoded (Either a b) = Either (Encoded a) (Encoded b) - encode (Left a) = Left (encode a) - encode (Right b) = Right (encode b) - -instance Encoding a => Encoding (HashMap k a) where - type Encoded (HashMap k a) = HashMap k (Encoded a) - encode = fmap encode - -instance Encoding a => Encoding (IntMap a) where - type Encoded (IntMap a) = IntMap (Encoded a) - encode = fmap encode - -instance Encoding a => Encoding (Map k a) where - type Encoded (Map k a) = Map k (Encoded a) - encode = fmap encode - -instance Encoding a => Encoding (Maybe a) where - type Encoded (Maybe a) = Maybe (Encoded a) - encode = fmap encode - -instance Encoding a => Encoding (Seq a) where - type Encoded (Seq a) = Seq (Encoded a) - encode = fmap encode - -instance Encoding a => Encoding (Tree a) where - type Encoded (Tree a) = Tree (Encoded a) - encode = fmap encode diff --git a/src/Ersatz/Equatable.hs b/src/Ersatz/Equatable.hs --- a/src/Ersatz/Equatable.hs +++ b/src/Ersatz/Equatable.hs @@ -1,11 +1,9 @@ {-# LANGUAGE CPP #-} {-# LANGUAGE TypeFamilies #-} -{-# LANGUAGE DeriveGeneric #-} {-# LANGUAGE TypeOperators #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE DefaultSignatures #-} {-# LANGUAGE FlexibleInstances #-} -{-# LANGUAGE DeriveDataTypeable #-} {-# LANGUAGE UndecidableInstances #-} {-# LANGUAGE Safe #-} @@ -21,12 +19,17 @@ -------------------------------------------------------------------- module Ersatz.Equatable ( Equatable(..) + , GEquatable(..) ) where import Prelude hiding ((&&),(||),not,and,or,all,any) import Ersatz.Bit import GHC.Generics +import Data.IntMap (IntMap) +import Data.Map (Map) +import qualified Data.Map as Map +import qualified Data.IntMap as IntMap infix 4 ===, /== @@ -48,6 +51,16 @@ a === b = not (xor a b) (/==) = xor +instance (Eq k, Equatable v) => Equatable (Map k v) where + x === y + | Map.keys x == Map.keys y = Map.elems x === Map.elems y + | otherwise = false + +instance Equatable v => Equatable (IntMap v) where + x === y + | IntMap.keys x == IntMap.keys y = IntMap.elems x === IntMap.elems y + | otherwise = false + instance (Equatable a, Equatable b) => Equatable (a,b) instance (Equatable a, Equatable b, Equatable c) => Equatable (a,b,c) instance (Equatable a, Equatable b, Equatable c, Equatable d) => Equatable (a,b,c,d) @@ -63,6 +76,9 @@ instance GEquatable U1 where U1 ===# U1 = true + +instance GEquatable V1 where + x ===# y = x `seq` y `seq` error "GEquatable[V1].===#" instance (GEquatable f, GEquatable g) => GEquatable (f :*: g) where (a :*: b) ===# (c :*: d) = (a ===# c) && (b ===# d) diff --git a/src/Ersatz/Internal/Formula.hs b/src/Ersatz/Internal/Formula.hs --- a/src/Ersatz/Internal/Formula.hs +++ b/src/Ersatz/Internal/Formula.hs @@ -5,8 +5,7 @@ {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE DeriveDataTypeable #-} {-# LANGUAGE MultiParamTypeClasses #-} -{-# LANGUAGE GeneralizedNewtypeDeriving #-} -{-# LANGUAGE Trustworthy #-} +{-# LANGUAGE Safe #-} {-# OPTIONS_HADDOCK not-home #-} -------------------------------------------------------------------- @@ -45,19 +44,27 @@ -- | A disjunction of possibly negated atoms. Negated atoms are represented -- by negating the identifier. newtype Clause = Clause { clauseSet :: IntSet } - deriving (Eq, Ord, Monoid, Typeable) + deriving (Eq, Ord, Typeable) -- | Extract the (possibly negated) atoms referenced by a 'Clause'. clauseLiterals :: Clause -> [Literal] clauseLiterals (Clause is) = Literal <$> IntSet.toList is +instance Monoid Clause where + mempty = Clause mempty + mappend (Clause x) (Clause y) = Clause (mappend x y) + ------------------------------------------------------------------------------ -- Formulas ------------------------------------------------------------------------------ -- | A conjunction of clauses newtype Formula = Formula { formulaSet :: Set Clause } - deriving (Eq, Ord, Monoid, Typeable) + deriving (Eq, Ord, Typeable) + +instance Monoid Formula where + mempty = Formula mempty + mappend (Formula x) (Formula y) = Formula (mappend x y) instance Show Formula where showsPrec p = showParen (p > 2) . foldr (.) id diff --git a/src/Ersatz/Internal/Literal.hs b/src/Ersatz/Internal/Literal.hs --- a/src/Ersatz/Internal/Literal.hs +++ b/src/Ersatz/Internal/Literal.hs @@ -1,5 +1,5 @@ {-# LANGUAGE DeriveDataTypeable #-} -{-# LANGUAGE Trustworthy #-} +{-# LANGUAGE Safe #-} -------------------------------------------------------------------- -- | -- Copyright : © Edward Kmett 2010-2014, Johan Kiviniemi 2013 diff --git a/src/Ersatz/Orderable.hs b/src/Ersatz/Orderable.hs new file mode 100644 --- /dev/null +++ b/src/Ersatz/Orderable.hs @@ -0,0 +1,116 @@ +{-# LANGUAGE CPP #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE DefaultSignatures #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE UndecidableInstances #-} +{-# LANGUAGE Safe #-} + +{-# OPTIONS_HADDOCK not-home #-} +-------------------------------------------------------------------- +-- | +-- Copyright : © Edward Kmett 2010-2014, Johan Kiviniemi 2013 +-- License : BSD3 +-- Maintainer: Edward Kmett +-- Stability : experimental +-- Portability: non-portable +-- +-------------------------------------------------------------------- +module Ersatz.Orderable + ( Orderable(..) + , GOrderable(..) + ) where + +import Prelude hiding ((&&),(||),not,and,or,all,any) + +import Ersatz.Bit +import Ersatz.Equatable +import GHC.Generics + +infix 4 =?, >? + +-- | Instances for this class for arbitrary types can be automatically derived from 'Generic'. +class Equatable t => Orderable t where + -- | Compare for less-than within the SAT problem. + ( t -> Bit + + -- | Compare for less-than or equal-to within the SAT problem. + (<=?) :: t -> t -> Bit + x <=? y = x === y || x t -> t -> Bit + a =?) :: t -> t -> Bit + x >=? y = y <=? x + + -- | Compare for greater-than within the SAT problem. + (>?) :: t -> t -> Bit + x >? y = y Orderable (a,b) +instance (Orderable a, Orderable b, Orderable c) => Orderable (a,b,c) +instance (Orderable a, Orderable b, Orderable c, Orderable d) => Orderable (a,b,c,d) +instance (Orderable a, Orderable b, Orderable c, Orderable d, Orderable e) => Orderable (a,b,c,d,e) +instance (Orderable a, Orderable b, Orderable c, Orderable d, Orderable e, Orderable f) => Orderable (a,b,c,d,e,f) +instance (Orderable a, Orderable b, Orderable c, Orderable d, Orderable e, Orderable f, Orderable g) => Orderable (a,b,c,d,e,f,g) +instance Orderable a => Orderable (Maybe a) +instance (Orderable a, Orderable b) => Orderable (Either a b) + +-- | Lexicographic order +instance Orderable a => Orderable [a] where +#ifndef HLINT + [] GOrderable f where + ( f a -> Bit + (<=?#) :: f a -> f a -> Bit + +instance GOrderable U1 where + U1 GOrderable (f :*: g) where + (a :*: b) GOrderable (f :+: g) where + L1 _ GOrderable (M1 i c f) where + M1 x GOrderable (K1 i a) where + K1 a problem <> clauses where comments = foldMap bComment (dimacsComments t) - problem = bLine [ copyByteString "p cnf" - , integral (dimacsNumVariables t) - , integral (Set.size tClauses) + problem = bLine [ string7 "p cnf" + , intDec (dimacsNumVariables t) + , intDec (Set.size tClauses) ] clauses = foldMap bClause tClauses @@ -248,14 +243,14 @@ qdimacs t = comments <> problem <> quantified <> clauses where comments = foldMap bComment (qdimacsComments t) - problem = bLine [ copyByteString "p cnf" - , integral (qdimacsNumVariables t) - , integral (Set.size tClauses) + problem = bLine [ string7 "p cnf" + , intDec (qdimacsNumVariables t) + , intDec (Set.size tClauses) ] quantified = foldMap go tQuantGroups - where go ls = bLine0 (q (head ls) : map (integral . getQuant) ls) - q Exists{} = fromChar 'e' - q Forall{} = fromChar 'a' + where go ls = bLine0 (q (head ls) : map (intDec . getQuant) ls) + q Exists{} = char7 'e' + q Forall{} = char7 'a' clauses = foldMap bClause tClauses tQuantGroups = List.groupBy eqQuant (qdimacsQuantified t) @@ -271,29 +266,29 @@ wdimacs t = comments <> problem <> clauses where comments = foldMap bComment (wdimacsComments t) - problem = bLine [ copyByteString "p wcnf" - , integral (wdimacsNumVariables t) - , integral (Set.size tClauses) - , integral (wdimacsTopWeight t) + problem = bLine [ string7 "p wcnf" + , intDec (wdimacsNumVariables t) + , intDec (Set.size tClauses) + , int64Dec (wdimacsTopWeight t) ] clauses = foldMap (uncurry bWClause) tClauses tClauses = wdimacsClauses t bComment :: ByteString -> Builder -bComment bs = bLine [ fromChar 'c', fromByteString bs ] +bComment bs = bLine [ char7 'c', byteString bs ] bClause :: IntSet -> Builder -bClause ls = bLine0 (map integral (IntSet.toList ls)) +bClause ls = bLine0 (map intDec (IntSet.toList ls)) bWClause :: Int64 -> IntSet -> Builder -bWClause w ls = bLine0 (integral w : map integral (IntSet.toList ls)) +bWClause w ls = bLine0 (int64Dec w : map intDec (IntSet.toList ls)) bLine0 :: [Builder] -> Builder -bLine0 = bLine . (++ [fromChar '0']) +bLine0 = bLine . (++ [char7 '0']) bLine :: [Builder] -> Builder -bLine bs = mconcat (List.intersperse (fromChar ' ') bs) <> fromChar '\n' +bLine bs = mconcat (List.intersperse (char7 ' ') bs) <> char7 '\n' -- | An explicit prenex quantifier data Quant diff --git a/src/Ersatz/Solution.hs b/src/Ersatz/Solution.hs --- a/src/Ersatz/Solution.hs +++ b/src/Ersatz/Solution.hs @@ -1,7 +1,7 @@ {-# LANGUAGE Rank2Types #-} {-# LANGUAGE DeriveDataTypeable #-} {-# LANGUAGE ImpredicativeTypes #-} -{-# LANGUAGE Trustworthy #-} -- Safe if lens is Safe +{-# LANGUAGE Safe #-} -------------------------------------------------------------------- -- | -- Copyright : © Edward Kmett 2010-2014, Johan Kiviniemi 2013 @@ -64,4 +64,10 @@ minBound = Unsolved maxBound = Satisfied +-- | A @'Solver' s m@ is responsible for invoking a solver and +-- returning a 'Result' and a map of determined results. +-- +-- * @s@ is typically 'SAT' or 'QSAT' +-- +-- * @m@ is typically 'IO' type Solver s m = s -> m (Result, IntMap Bool) diff --git a/src/Ersatz/Solver.hs b/src/Ersatz/Solver.hs --- a/src/Ersatz/Solver.hs +++ b/src/Ersatz/Solver.hs @@ -13,15 +13,17 @@ , solveWith ) where +import Control.Applicative +import Control.Monad import Control.Monad.State import Data.Default -import Ersatz.Decoding +import Ersatz.Codec import Ersatz.Problem import Ersatz.Solution import Ersatz.Solver.DepQBF import Ersatz.Solver.Minisat -solveWith :: (Monad m, HasSAT s, Default s, Decoding a) => Solver s m -> StateT s m a -> m (Result, Maybe (Decoded a)) +solveWith :: (Monad m, Alternative n, MonadPlus n, HasSAT s, Default s, Codec a) => Solver s m -> StateT s m a -> m (Result, n (Decoded a)) solveWith solver m = do (a, problem) <- runStateT m def (res, litMap) <- solver problem diff --git a/src/Ersatz/Solver/DepQBF.hs b/src/Ersatz/Solver/DepQBF.hs --- a/src/Ersatz/Solver/DepQBF.hs +++ b/src/Ersatz/Solver/DepQBF.hs @@ -1,4 +1,4 @@ -{-# LANGUAGE Trustworthy #-} +{-# LANGUAGE Safe #-} -------------------------------------------------------------------- -- | -- Copyright : © Edward Kmett 2010-2014, Johan Kiviniemi 2013 @@ -7,32 +7,47 @@ -- Stability : experimental -- Portability: non-portable -- +-- is a solver capable of +-- solving quantified boolean formulae ('QBF'). -------------------------------------------------------------------- module Ersatz.Solver.DepQBF ( depqbf , depqbfPath ) where -import Blaze.ByteString.Builder -- not Trustworthy +import Data.ByteString.Builder import Control.Monad.IO.Class -import qualified Data.ByteString as BS import Ersatz.Problem import Ersatz.Solution import Ersatz.Solver.Common -import qualified Data.IntMap as IntMap +import qualified Data.IntMap as I import System.IO import System.Process (readProcessWithExitCode) +-- | This is a 'Solver' for 'QSAT' problems that runs the @depqbf@ solver using +-- the current @PATH@, it tries to run an executable named @depqbf@. depqbf :: MonadIO m => Solver QSAT m depqbf = depqbfPath "depqbf" +parseLiteral :: String -> (Int, Bool) +parseLiteral ('-':xs) = (read xs, False) +parseLiteral xs = (read xs, True) + +-- | This is a 'Solver' for 'QSAT' problems that lets you specify the path to the @depqbf@ executable. depqbfPath :: MonadIO m => FilePath -> Solver QSAT m depqbfPath path problem = liftIO $ withTempFiles ".cnf" "" $ \problemPath _ -> do withFile problemPath WriteMode $ \fh -> - toByteStringIO (BS.hPut fh) (qdimacs problem) + hPutBuilder fh (qdimacs problem) - (exit, _out, _err) <- - readProcessWithExitCode path [problemPath] [] + (exit, out, _err) <- + readProcessWithExitCode path [problemPath, "--qdo"] [] - return (resultOf exit, IntMap.empty) + let result = resultOf exit + + return $ (,) result $ + case result of + Satisfied -> + I.fromList $ map (parseLiteral . head . tail . words) $ tail $ lines out + _ -> + I.empty diff --git a/src/Ersatz/Solver/Minisat.hs b/src/Ersatz/Solver/Minisat.hs --- a/src/Ersatz/Solver/Minisat.hs +++ b/src/Ersatz/Solver/Minisat.hs @@ -1,4 +1,4 @@ -{-# LANGUAGE Trustworthy #-} +{-# LANGUAGE Safe #-} -------------------------------------------------------------------- -- | -- Copyright : © Edward Kmett 2010-2014, Johan Kiviniemi 2013 @@ -14,12 +14,11 @@ , minisatPath ) where -import Blaze.ByteString.Builder -- not Trustworthy +import Data.ByteString.Builder import Control.Applicative import Control.Exception (IOException, handle) import Control.Monad import Control.Monad.IO.Class -import qualified Data.ByteString as BS import Data.IntMap (IntMap) import Ersatz.Internal.Parser import Ersatz.Problem @@ -29,17 +28,22 @@ import System.IO import System.Process (readProcessWithExitCode) +-- | 'Solver' for 'SAT' problems that tries to invoke the @minisat@ executable from the @PATH@ minisat :: MonadIO m => Solver SAT m minisat = minisatPath "minisat" +-- | 'Solver' for 'SAT' problems that tries to invoke the @cryptominisat@ executable from the @PATH@ cryptominisat :: MonadIO m => Solver SAT m cryptominisat = minisatPath "cryptominisat" +-- | 'Solver' for 'SAT' problems that tries to invoke a program that takes @minisat@ compatible arguments. +-- +-- The 'FilePath' refers to the path to the executable. minisatPath :: MonadIO m => FilePath -> Solver SAT m minisatPath path problem = liftIO $ withTempFiles ".cnf" "" $ \problemPath solutionPath -> do withFile problemPath WriteMode $ \fh -> - toByteStringIO (BS.hPut fh) (dimacs problem) + hPutBuilder fh (dimacs problem) (exit, _out, _err) <- readProcessWithExitCode path [problemPath, solutionPath] [] diff --git a/src/Ersatz/Variable.hs b/src/Ersatz/Variable.hs --- a/src/Ersatz/Variable.hs +++ b/src/Ersatz/Variable.hs @@ -14,7 +14,13 @@ -------------------------------------------------------------------- module Ersatz.Variable ( Variable(..) +#ifndef HLINT + , forall +#endif + , exists + , GVariable(..) + , genericLiterally ) where import Control.Monad @@ -23,49 +29,48 @@ import Ersatz.Problem import GHC.Generics +exists :: (Variable a, MonadState s m, HasSAT s) => m a +exists = literally literalExists + +#ifndef HLINT +forall :: (Variable a, MonadState s m, HasQSAT s) => m a +forall = literally literalForall +#endif + class GVariable f where - gexists :: (MonadState s m, HasSAT s) => m (f a) - gforall :: (MonadState s m, HasQSAT s) => m (f a) + gliterally :: (MonadState s m, HasSAT s) => m Literal -> m (f a) instance GVariable U1 where - gexists = return U1 - gforall = return U1 + gliterally _ = return U1 instance (GVariable f, GVariable g) => GVariable (f :*: g) where - gexists = liftM2 (:*:) gexists gexists - gforall = liftM2 (:*:) gforall gforall + gliterally m = liftM2 (:*:) (gliterally m) (gliterally m) instance Variable a => GVariable (K1 i a) where - gexists = liftM K1 exists -#ifndef HLINT - gforall = liftM K1 forall -#endif + gliterally = liftM K1 . literally instance GVariable f => GVariable (M1 i c f) where - gexists = liftM M1 gexists - gforall = liftM M1 gforall + gliterally = liftM M1 . gliterally -- | Instances for this class for product-like types can be automatically derived -- for any type that is an instance of 'Generic'. class Variable t where - exists :: (MonadState s m, HasSAT s) => m t -#ifndef HLINT - forall :: (MonadState s m, HasQSAT s) => m t -#endif + literally :: (HasSAT s, MonadState s m) => m Literal -> m t #ifndef HLINT - default exists :: (MonadState s m, HasSAT s, Generic t, GVariable (Rep t)) => m t - exists = liftM to gexists - - default forall :: (MonadState s m, HasQSAT s, Generic t, GVariable (Rep t)) => m t - forall = liftM to gforall + default literally :: + (HasSAT s, MonadState s m, Generic t, GVariable (Rep t)) => + m Literal -> m t + literally = genericLiterally #endif +genericLiterally :: + (HasSAT s, MonadState s m, Generic t, GVariable (Rep t)) => + m Literal -> m t +genericLiterally = liftM to . gliterally + instance Variable Literal where - exists = literalExists -#ifndef HLINT - forall = literalForall -#endif + literally = id instance (Variable a, Variable b) => Variable (a,b) instance (Variable a, Variable b, Variable c) => Variable (a,b,c) diff --git a/tests/hlint.hs b/tests/hlint.hs new file mode 100644 --- /dev/null +++ b/tests/hlint.hs @@ -0,0 +1,23 @@ +----------------------------------------------------------------------------- +-- | +-- Module : Main (hlint) +-- Copyright : (C) 2013-2014 Edward Kmett +-- License : BSD-style (see the file LICENSE) +-- Maintainer : Edward Kmett +-- Stability : provisional +-- Portability : portable +-- +-- This module runs HLint on the lens source tree. +----------------------------------------------------------------------------- +module Main where + +import Control.Monad +import Language.Haskell.HLint +import System.Environment +import System.Exit + +main :: IO () +main = do + args <- getArgs + hints <- hlint $ ["src", "--cpp-define=HLINT", "--cpp-ansi"] ++ args + unless (null hints) exitFailure diff --git a/tests/properties.hs b/tests/properties.hs deleted file mode 100644 --- a/tests/properties.hs +++ /dev/null @@ -1,45 +0,0 @@ -module Main where - -import Prelude hiding ((||),(&&)) - -import Test.Framework (Test) -import Test.Framework (defaultMain, testGroup) -import Test.Framework.Providers.HUnit --- import Test.Framework.Providers.QuickCheck (testProperty) --- import Test.HUnit hiding (Test) --- import Test.QuickCheck hiding ((==>)) - -import Ersatz - -main :: IO () -main = defaultMain tests - -ignore :: Functor f => f a -> f () -ignore = fmap (const ()) - -tests :: [Test] -tests = - [ testGroup "sat" $ zipWith (testCase . show) [1 :: Int ..] $ - [ -- showSAT (return ()) @?= "p cnf 0 0\n" - -- , showSAT (ignore litExists) @?= "p cnf 1 0\n" - -- , showSAT (ignore litForall) @?= "p cnf 2 0\na 1\n" - -- , showSAT (do x <- forall; y <- exists; assertLits [x,y]) @?= "p cnf 2 1\na 1\ne 2\n1 2 0\n" - ] - ] - -full_adder :: Bit -> Bit -> Bit -> (Bit, Bit) -full_adder a b cin = (s2, c1 || c2) - where (s1,c1) = half_adder a b - (s2,c2) = half_adder s1 cin - -half_adder :: Bit -> Bit -> (Bit, Bit) -half_adder a b = (a `xor` b, a && b) - -{- -currying_works :: SAT s () -currying_works = do - x <- forall - y <- forall - z <- forall - assert $ (x && y) ==> z === x ==> y ==> z --}