ersatz 0.2.6.1 → 0.3

raw patch · 27 files changed

+802/−451 lines, 27 filesdep +hlintdep −HUnitdep −QuickCheckdep −blaze-builderdep ~arraydep ~basedep ~bytestringPVP ok

version bump matches the API change (PVP)

Dependencies added: hlint

Dependencies removed: HUnit, QuickCheck, blaze-builder, blaze-textual, data-reify, test-framework, test-framework-hunit, test-framework-quickcheck

Dependency ranges changed: array, base, bytestring, containers, lens, mtl, transformers

API changes (from Hackage documentation)

Files

• .travis.yml +17/−4
• AUTHORS.md +2/−0
• CHANGELOG.md +17/−0
• HLint.hs +0/−1
• LICENSE +2/−1
• ersatz.cabal +56/−38
• examples/regexp-grid/RegexpGrid/Types.hs +1/−4
• examples/sudoku/Sudoku/Cell.hs +1/−4
• src/Ersatz.hs +4/−4
• src/Ersatz/Bit.hs +15/−13
• src/Ersatz/BitChar.hs +56/−0
• src/Ersatz/Bits.hs +243/−59
• src/Ersatz/Codec.hs +128/−0
• src/Ersatz/Decoding.hs +0/−104
• src/Ersatz/Encoding.hs +0/−103
• src/Ersatz/Equatable.hs +18/−2
• src/Ersatz/Internal/Formula.hs +11/−4
• src/Ersatz/Internal/Literal.hs +1/−1
• src/Ersatz/Orderable.hs +116/−0
• src/Ersatz/Problem.hs +19/−24
• src/Ersatz/Solution.hs +7/−1
• src/Ersatz/Solver.hs +4/−2
• src/Ersatz/Solver/DepQBF.hs +23/−8
• src/Ersatz/Solver/Minisat.hs +8/−4
• src/Ersatz/Variable.hs +30/−25
• tests/hlint.hs +23/−0
• tests/properties.hs +0/−45

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

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

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

@@ -1,1 +0,0 @@-import "hint" HLint.Default

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

@@ -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 <ekmett@gmail.com>-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

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

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

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

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

@@ -0,0 +1,56 @@+{-# LANGUAGE DeriveDataTypeable #-}+{-# LANGUAGE TypeFamilies #-}+--------------------------------------------------------------------+-- |+-- Copyright :  © Eric Mertens 2010-2014+-- License   :  BSD3+-- Maintainer:  Edward Kmett <ekmett@gmail.com>+-- 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 <?  BitChar ys = xs <?  ys+  BitChar xs <=? BitChar ys = xs <=? ys++instance Variable BitChar where+  literally m =+       -- Char upperbound is 0x10ffff, so only set+       -- the high bit when the next 4 bits are 0++    do x:xs <- replicateM 21 (literally m)++       let x' = x && nor (take 4 xs)+           n  = Bits (reverse (x':xs)) -- Bits is little endian++       return (BitChar n)

@@ -4,31 +4,45 @@ {-# LANGUAGE Safe #-} -------------------------------------------------------------------- -- |--- Copyright :  © Edward Kmett 2010-2014, Johan Kiviniemi 2013+-- Copyright :  © Edward Kmett 2010-2015, © Eric Mertens 2014, Johan Kiviniemi 2013 -- License   :  BSD3 -- Maintainer:  Edward Kmett <ekmett@gmail.com> -- 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 <?  Bits ys = orderHelper false xs ys+  Bits xs <=? Bits ys = orderHelper true  xs ys++orderHelper :: Bit -> [Bit] -> [Bit] -> Bit+orderHelper c0 xs ys = foldl aux c0 (zipWithBits (,) xs ys)+    where+    aux c (x,y) = c && x === y || x <? y++instance Codec Bits where+  type Decoded Bits = Integer++  decode s (Bits xs) =+    do ys <- traverse (decode s) xs+       -- bools to Integers+       let zs = map (\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

@@ -0,0 +1,128 @@+{-# LANGUAGE Rank2Types #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE Safe #-}+--------------------------------------------------------------------+-- |+-- Copyright :  © Edward Kmett 2010-2014, Johan Kiviniemi 2013+-- License   :  BSD3+-- Maintainer:  Edward Kmett <ekmett@gmail.com>+-- 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

@@ -1,104 +0,0 @@-{-# LANGUAGE Rank2Types #-}-{-# LANGUAGE TypeFamilies #-}-{-# LANGUAGE Safe #-}------------------------------------------------------------------------ |--- Copyright :  © Edward Kmett 2010-2014, Johan Kiviniemi 2013--- License   :  BSD3--- Maintainer:  Edward Kmett <ekmett@gmail.com>--- 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

@@ -1,103 +0,0 @@-{-# LANGUAGE Rank2Types #-}-{-# LANGUAGE TypeFamilies #-}------------------------------------------------------------------------ |--- Copyright :  © Edward Kmett 2010-2014, Johan Kiviniemi 2013--- License   :  BSD3--- Maintainer:  Edward Kmett <ekmett@gmail.com>--- 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

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

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

@@ -1,5 +1,5 @@ {-# LANGUAGE DeriveDataTypeable #-}-{-# LANGUAGE Trustworthy #-}+{-# LANGUAGE Safe #-} -------------------------------------------------------------------- -- | -- Copyright :  © Edward Kmett 2010-2014, Johan Kiviniemi 2013

@@ -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 <ekmett@gmail.com>+-- 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 -> t -> Bit++  -- | Compare for less-than or equal-to within the SAT problem.+  (<=?) :: t -> t -> Bit+  x <=? y = x === y || x <? y+#ifndef HLINT+  default (<?) :: (Generic t, GOrderable (Rep t)) => t -> t -> Bit+  a <? b = from a <?# from b+#endif++  -- | Compare for greater-than or equal-to within the SAT problem.+  (>=?) :: t -> t -> Bit+  x >=? y = y <=? x++  -- | Compare for greater-than within the SAT problem.+  (>?) :: t -> t -> Bit+  x >? y = y <? x+++instance Orderable Bit where+  a <?  b = not a && b+  a <=? b = not a || b++instance (Orderable a, Orderable b) => 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+  []   <? []   = false+  x:xs <? y:ys = x === y && xs <? ys+              || x <?  y+  []   <? _    = true+  _    <? []   = false++  []   <=? _    = true+  x:xs <=? y:ys = x === y && xs <=? ys+               || x <?  y+  _    <=? []   = false+#endif++class GEquatable f => GOrderable f where+  (<?#) :: f a -> f a -> Bit+  (<=?#) :: f a -> f a -> Bit++instance GOrderable U1 where+  U1 <?#  U1 = false+  U1 <=?# U1 = true++instance GOrderable V1 where+  x <?# y = x `seq` y `seq` error "GOrderable[V1].<?#"+  x <=?# y = x `seq` y `seq` error "GOrderable[V1].<=?#"++instance (GOrderable f, GOrderable g) => GOrderable (f :*: g) where+  (a :*: b) <?#  (c :*: d) = (a <?# c) || (a ===# c && b <?# d)+  (a :*: b) <=?# (c :*: d) = (a <?# c) || (a ===# c && b <=?# d)++instance (GOrderable f, GOrderable g) => GOrderable (f :+: g) where+  L1 _ <?# R1 _ = true+  L1 a <?# L1 b = a <?# b+  R1 a <?# R1 b = a <?# b+  R1 _ <?# L1 _ = false++  L1 _ <=?# R1 _ = true+  L1 a <=?# L1 b = a <=?# b+  R1 a <=?# R1 b = a <=?# b+  R1 _ <=?# L1 _ = false++instance GOrderable f => GOrderable (M1 i c f) where+  M1 x <?#  M1 y = x <?#  y+  M1 x <=?# M1 y = x <=?# y++instance Orderable a => GOrderable (K1 i a) where+  K1 a <?#  K1 b = a <?  b+  K1 a <=?# K1 b = a <=? b

@@ -1,6 +1,5 @@ {-# LANGUAGE CPP #-} {-# LANGUAGE Rank2Types #-}-{-# LANGUAGE BangPatterns #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE PatternGuards #-} {-# LANGUAGE TypeOperators #-}@@ -9,8 +8,6 @@ {-# LANGUAGE OverloadedStrings #-} {-# LANGUAGE DeriveDataTypeable #-} {-# LANGUAGE MultiParamTypeClasses #-}-{-# LANGUAGE FunctionalDependencies #-}-{-# LANGUAGE GeneralizedNewtypeDeriving #-} {-# LANGUAGE Trustworthy #-}  {-# OPTIONS_HADDOCK not-home #-}@@ -47,9 +44,7 @@   , dimacs, qdimacs, wdimacs   ) where -import Blaze.ByteString.Builder-import Blaze.ByteString.Builder.Char8-import Blaze.Text+import Data.ByteString.Builder import Control.Applicative import Control.Lens import Control.Monad@@ -235,9 +230,9 @@ dimacs t = comments <> 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

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

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

@@ -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 --+-- <http://lonsing.github.io/depqbf/ DepQBF> 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

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

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

@@ -0,0 +1,23 @@+-----------------------------------------------------------------------------+-- |+-- Module      :  Main (hlint)+-- Copyright   :  (C) 2013-2014 Edward Kmett+-- License     :  BSD-style (see the file LICENSE)+-- Maintainer  :  Edward Kmett <ekmett@gmail.com>+-- 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

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