packages feed

ersatz (empty) → 0.1

raw patch · 25 files changed

+1990/−0 lines, 25 filesdep +HUnitdep +QuickCheckdep +arraybuild-type:Customsetup-changed

Dependencies added: HUnit, QuickCheck, array, base, containers, data-default, data-reify, directory, doctest, ersatz, filepath, ghc-prim, mtl, process, temporary, test-framework, test-framework-hunit, test-framework-quickcheck, transformers, unordered-containers

Files

+ AUTHORS.md view
@@ -0,0 +1,12 @@+Authors+=======++`ersatz` started as a one man project by [Edward Kmett](mailto:ekmett@gmail.com) [@ekmett](https://github.com/ekmett).+However, it then languished for 3 years after Don Stewart [@donsbot](https://github.com/donsbot) released perfectly adequate bindings for yices.++It revived by [Johan Kiviniemi](mailto:lens@johan.kiviniemi.name) [@ion1](https://github.com/ion1) after he+shamed the original author into polishing it up and releasing it.++Omission from this page is by no means an attempt to discount your contributions! Thank you for all of your help!++-Edward Kmett
+ CHANGELOG.md view
@@ -0,0 +1,3 @@+0.1+---+* Repository Initialized
+ LICENSE view
@@ -0,0 +1,32 @@+Copyright (c) 2010-2013 Edward Kmett+Copyright (c) 2013 Johan Kiviniemi++All rights reserved.++Redistribution and use in source and binary forms, with or without+modification, are permitted provided that the following conditions are+met:++    * Redistributions of source code must retain the above copyright+      notice, this list of conditions and the following disclaimer.++    * Redistributions in binary form must reproduce the above+      copyright notice, this list of conditions and the following+      disclaimer in the documentation and/or other materials provided+      with the distribution.++    * Neither the name of Edward Kmett nor the names of other+      contributors may be used to endorse or promote products derived+      from this software without specific prior written permission.++THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS+"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT+LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR+A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT+OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,+SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT+LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,+DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY+THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT+(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE+OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+ README.md view
@@ -0,0 +1,70 @@+# Ersatz++[![Build Status](https://secure.travis-ci.org/ekmett/ersatz.png)](http://travis-ci.org/ekmett/ersatz)++Ersatz is a library for generating QSAT (CNF/QBF) problems using a monad. It takes care of generating the normal form, encoding your problem, marshaling the data to an external solver, and parsing and interpreting the result into Haskell types.++What differentiates Ersatz is the use of observable sharing in the API.++For instance to define a full adder:++```haskell+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)+```++as opposed to the following code in [satchmo](http://dfa.imn.htwk-leipzig.de/satchmo/):+++```haskell+full_adder :: Boolean -> Boolean -> Boolean+           -> SAT ( Boolean, Boolean )+full_adder a b c = do+  let s x y z = sum $ map fromEnum [x,y,z]+  r <- fun3 ( \ x y z -> odd $ s x y z ) a b c+  d <- fun3 ( \ x y z -> 1   < s x y z ) a b c+  return ( r, d )++half_adder :: Boolean -> Boolean+           -> SAT ( Boolean, Boolean )+half_adder a b = do+  let s x y = sum $ map fromEnum [x,y]+  r <- fun2 ( \ x y -> odd $ s x y ) a b+  d <- fun2 ( \ x y -> 1   < s x y ) a b+  return ( r, d )+```++This enables you to use the a much richer subset of Haskell than the purely monadic meta-language, and it becomes much easier to see that the resulting encoding is correct.++To allocate fresh existentially or universally quantified variables or to assert that a Bit is true and add the attendant circuit with sharing to the current problem you use the SAT monad.++```haskell+verify_currying :: SAT m ()+verify_currying = do+  (x::Bit, y::Bit, z::Bit) <- forall+  assert $ ((x && y) ==> z) === (x ==> y ==> z)+```++We can then hand that off to a SAT solver, and get back an answer:++```haskell+main = solveWith minisat verify_currying >>= print+```++Support is offered for decoding various Haskell datatypes from the+solution provided by the SAT solver.++Contact Information+-------------------++Contributions and bug reports are welcome!++Please feel free to contact me through github or on the #haskell IRC channel on irc.freenode.net.++-Edward Kmett+
+ Setup.lhs view
@@ -0,0 +1,44 @@+#!/usr/bin/runhaskell+\begin{code}+{-# OPTIONS_GHC -Wall #-}+module Main (main) where++import Data.List ( nub )+import Data.Version ( showVersion )+import Distribution.Package ( PackageName(PackageName), PackageId, InstalledPackageId, packageVersion, packageName )+import Distribution.PackageDescription ( PackageDescription(), TestSuite(..) )+import Distribution.Simple ( defaultMainWithHooks, UserHooks(..), simpleUserHooks )+import Distribution.Simple.Utils ( rewriteFile, createDirectoryIfMissingVerbose)+import Distribution.Simple.BuildPaths ( autogenModulesDir )+import Distribution.Simple.Setup ( BuildFlags(buildVerbosity), fromFlag)+import Distribution.Simple.LocalBuildInfo ( withLibLBI, withTestLBI, LocalBuildInfo(), ComponentLocalBuildInfo(componentPackageDeps) )+import Distribution.Verbosity ( Verbosity)+import System.FilePath ( (</>) )++main :: IO ()+main = defaultMainWithHooks simpleUserHooks+  { buildHook = \pkg lbi hooks flags -> do+     generateBuildModule (fromFlag (buildVerbosity flags)) pkg lbi+     buildHook simpleUserHooks pkg lbi hooks flags+  }++generateBuildModule :: Verbosity -> PackageDescription -> LocalBuildInfo -> IO ()+generateBuildModule verbosity pkg lbi = do+  let dir = autogenModulesDir lbi+  createDirectoryIfMissingVerbose verbosity True dir+  withLibLBI pkg lbi $ \_ libcfg -> do+    withTestLBI pkg lbi $ \suite suitecfg -> do+      rewriteFile (dir </> "Build_" ++ testName suite ++ ".hs") $ unlines+        [ "module Build_" ++ testName suite ++ " where"+        , "deps :: [String]"+        , "deps = " ++ (show $ formatdeps (testDeps libcfg suitecfg))+        ]+  where+    formatdeps = map (formatone . snd)+    formatone p = case packageName p of+      PackageName n -> n ++ "-" ++ showVersion (packageVersion p)++testDeps :: ComponentLocalBuildInfo -> ComponentLocalBuildInfo -> [(InstalledPackageId, PackageId)]+testDeps xs ys = nub $ componentPackageDeps xs ++ componentPackageDeps ys++\end{code}
+ ersatz.cabal view
@@ -0,0 +1,102 @@+name:           ersatz+version:        0.1+license:        BSD3+license-file:   LICENSE+author:         Edward A. Kmett, Johan Kiviniemi+maintainer:     Edward A. Kmett <ekmett@gmail.com>+stability:      experimental+homepage:       http://comonad.com/reader+category:       Logic, Algorithms+synopsis:       A monad for expressing SAT or QSAT problems using observable sharing.+description:    A monad for expressing SAT or QSAT problems using observable sharing.+  .+  For example, we can express a full-adder with:+  .+  > 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)+copyright:      (c) 2010-2013 Edward Kmett, (c) 2013 Johan Kiviniemi+build-type:     Custom+cabal-version:  >= 1.10+tested-with:    GHC == 7.6.2+extra-source-files:+  AUTHORS.md+  README.md+  CHANGELOG.md++library+  ghc-options: -Wall+  hs-source-dirs: src+  default-language: Haskell2010++  build-depends:+    array >= 0.2 && < 0.5,+    base >= 4 && < 6,+    containers >= 0.2.0.1,+    data-default >= 0.5 && < 0.6,+    ghc-prim,+    mtl >= 1.1 && < 2.2,+    process == 1.1.*,+    temporary == 1.1.*,+    transformers == 0.3.*,+    unordered-containers == 0.2.*++  exposed-modules:+    Ersatz+    Ersatz.Bit+    Ersatz.Bits+    Ersatz.Decoding+    Ersatz.Equatable+    Ersatz.Encoding+    Ersatz.Internal.Circuit+    Ersatz.Internal.Formula+    Ersatz.Internal.Literal+    Ersatz.Monad+    Ersatz.Problem+    Ersatz.Solution+    Ersatz.Solver+    Ersatz.Solver.Minisat+    Ersatz.Variable++  other-modules:+    Ersatz.Internal.Parser+    Ersatz.Internal.StableName++test-suite properties+  type: exitcode-stdio-1.0+  ghc-options: -Wall+  default-language: Haskell2010+  build-depends:+    ersatz,+    base >= 4 && < 6,+    mtl >= 1.1 && < 2.2,+    transformers == 0.3.*,+    containers >= 0.2.0.1,+    array >= 0.2 && < 0.5,+    data-reify >= 0.5 && < 0.7,+    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+  main-is: doctests.hs+  default-language: Haskell2010+  build-depends:+    base < 5,+    directory >= 1.0,+    doctest >= 0.9.1,+    filepath+  ghc-options: -Wall -threaded+  if impl(ghc<7.6.1)+    ghc-options: -Werror+  hs-source-dirs: tests
+ src/Ersatz.hs view
@@ -0,0 +1,32 @@+--------------------------------------------------------------------+-- |+-- Copyright :  (c) Edward Kmett 2010-2013, Johan Kiviniemi 2013+-- License   :  BSD3+-- Maintainer:  Edward Kmett <ekmett@gmail.com>+-- Stability :  experimental+-- Portability: non-portable+--+--------------------------------------------------------------------+module Ersatz+  ( module Ersatz.Bit+  , module Ersatz.Bits+  , module Ersatz.Decoding+  , module Ersatz.Equatable+  , module Ersatz.Encoding+  , module Ersatz.Monad+  , module Ersatz.Problem+  , module Ersatz.Solution+  , module Ersatz.Solver+  , module Ersatz.Variable+  ) where++import Ersatz.Bit+import Ersatz.Bits+import Ersatz.Decoding+import Ersatz.Equatable+import Ersatz.Encoding+import Ersatz.Monad+import Ersatz.Problem+import Ersatz.Solution+import Ersatz.Solver+import Ersatz.Variable
+ src/Ersatz/Bit.hs view
@@ -0,0 +1,284 @@+{-# LANGUAGE TypeFamilies, TypeOperators, FlexibleInstances, DeriveDataTypeable, DeriveGeneric, DefaultSignatures, FlexibleContexts, UndecidableInstances #-}+{-# OPTIONS_HADDOCK not-home #-}+--------------------------------------------------------------------+-- |+-- Copyright :  (c) Edward Kmett 2010-2013, Johan Kiviniemi 2013+-- License   :  BSD3+-- Maintainer:  Edward Kmett <ekmett@gmail.com>+-- Stability :  experimental+-- Portability: non-portable+--+--------------------------------------------------------------------+module Ersatz.Bit+  ( Bit(..)+  , assert+  , Boolean(..)+  ) where++import Prelude hiding ((&&),(||),not,and,or)+import qualified Prelude++import Control.Applicative+import Data.Traversable (Traversable, traverse)+import Data.Typeable+import Ersatz.Decoding+import Ersatz.Encoding+import Ersatz.Monad+import Ersatz.Internal.Circuit+import Ersatz.Internal.Formula+import Ersatz.Internal.Literal+import Ersatz.Internal.StableName+import Ersatz.Solution+import Ersatz.Variable+import GHC.Generics+import System.IO.Unsafe++infixr 3 &&, &&#+infixr 2 ||, ||#+infixr 0 ==>, ==>#++-- Bit++-- | A 'Bit' provides a reference to a possibly indeterminate boolean+-- value that can be determined by an external SAT solver.+newtype Bit = Bit (Circuit Bit)+  deriving (Show, Typeable)++instance Boolean Bit where+  -- improve the stablemap this way+  bool True  = true+  bool False = false+  true  = Bit (Var (lit True))+  false = Bit (Var (lit False))+  Bit (And as) && Bit (And bs) = and (as ++ bs)+  Bit (And as) && b            = and (as ++ [b])+  a            && Bit (And bs) = and (a : bs)+  a            && b            = and [a,b]+  Bit (Or as) || Bit (Or bs) = or (as ++ bs)+  Bit (Or as) || b           = or (as ++ [b])+  a           || Bit (Or bs) = or (a : bs)+  a           || b           = or [a,b]+  x ==> y = not x || y+  not (Bit (Not c)) = c+  not (Bit (Var b)) = Bit (Var (negateLit b))+  not c        = Bit (Not c)+  a `xor` b    = Bit (Xor a b)+  and xs       = Bit (And xs)+  or xs        = Bit (Or xs)+  choose f t s = Bit (Mux f t s)++instance Variable Bit where+  exists = Bit . Var <$> exists+  forall = Bit . Var <$> forall++-- a Bit you don't assert is actually a boolean function that you can evaluate later after compilation+instance Decoding Bit where+  type Decoded Bit = Bool+  decode sol b@(Bit c) +      = solutionStableName sol (unsafePerformIO (makeStableName' b))+     -- The StableName didn’t have an associated literal with a solution,+     -- recurse to compute the value.+    <|> case c of+          And cs  -> andMaybeBools $ decode sol <$> cs+          Or cs   -> orMaybeBools  $ decode sol <$> cs+          Xor x y -> xor <$> decode sol x <*> decode sol y+          Mux cf ct cp -> do+            p <- decode sol cp+            decode sol $ if p then ct else cf+          Not c'  -> not <$> decode sol c'+          Var l   -> decode sol l+    where+      andMaybeBools :: [Maybe Bool] -> Maybe Bool+      andMaybeBools mbs+        | any not knowns = Just False  -- One is known to be false.+        | null unknowns  = Just True   -- All are known to be true.+        | otherwise      = Nothing     -- Unknown.+        where+          (unknowns, knowns) = partitionMaybes mbs++      orMaybeBools :: [Maybe Bool] -> Maybe Bool+      orMaybeBools mbs+        | or knowns     = Just True   -- One is known to be true.+        | null unknowns = Just False  -- All are known to be false.+        | otherwise     = Nothing     -- Unknown.+        where+          (unknowns, knowns) = partitionMaybes mbs++      partitionMaybes :: [Maybe a] -> ([()], [a])+      partitionMaybes = foldr go ([],[])+        where+          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 in any satisf given 'Bit' must be 'true' in any +-- satisfying interpretation of the current problem.+assert :: MonadSAT m => Bit -> m ()+assert b = do+  l <- runBit b+  assertFormula (formulaLiteral l)++-- | Convert a 'Bit' to a 'Literal'.+runBit :: MonadSAT m => Bit -> m Literal+runBit (Bit (Not c)) = negateLiteral <$> runBit c+runBit (Bit (Var (Lit l))) = return l+runBit b@(Bit c) = generateLiteral b $ \out ->+  assertFormula =<< case c of+    And bs    -> formulaAnd out <$> traverse runBit bs+    Or  bs    -> formulaOr  out <$> traverse runBit bs+    Xor x y   -> formulaXor out <$> runBit x <*> runBit y+    Mux x y p -> formulaMux out <$> runBit x <*> runBit y <*> runBit p+    Var (Bool False) -> return $ formulaLiteral (negateLiteral out)+    Var (Bool True)  -> return $ formulaLiteral out++    -- Already handled above but GHC doesn't realize it.+    Not _       -> error "Unreachable"+    Var (Lit _) -> error "Unreachable"++class GBoolean f where+  gbool :: Bool -> f a+  (&&#) :: f a -> f a -> f a+  (||#) :: f a -> f a -> f a+  (==>#) :: f a -> f a -> f a+  gnot :: f a -> f a+  gand :: [f a] -> f a+  gor  :: [f a] -> f a+  gxor :: f a -> f a -> f a++instance GBoolean U1 where+  gbool _    = U1+  U1 &&# U1  = U1+  U1 ||# U1  = U1+  U1 ==># U1 = U1+  gnot U1    = U1+  gand _     = U1+  gor  _     = U1+  gxor _ _   = U1++instance (GBoolean f, GBoolean g) => GBoolean (f :*: g) where+  gbool x = gbool x :*: gbool x+  (a :*: b) &&#  (c :*: d) = (a &&# c)  :*: (b &&# d)+  (a :*: b) ||#  (c :*: d) = (a ||# c)  :*: (b ||# d)+  (a :*: b) ==># (c :*: d) = (a ==># c) :*: (b ==># d)+  gnot (a :*: b) = gnot a :*: gnot b+  gand xs = gand (map (\(x :*: _) -> x) xs) :*: gand (map (\(_ :*: x) -> x) xs)+  gor xs = gor (map (\(x :*: _) -> x) xs) :*: gor (map (\(_ :*: x) -> x) xs)+  gxor (a :*: b) (c :*: d) = gxor a c :*: gxor b d++instance Boolean a => GBoolean (K1 i a) where+  gbool = K1 . bool+  K1 a &&# K1 b = K1 (a && b)+  K1 a ||# K1 b = K1 (a || b)+  K1 a ==># K1 b = K1 (a ==> b)+  gnot (K1 a) = K1 (not a)+  gand as = K1 (and (map (\(K1 a) -> a) as))+  gor as = K1 (or (map (\(K1 a) -> a) as))+  gxor (K1 a) (K1 b) = K1 (xor a b)++instance GBoolean a => GBoolean (M1 i c a) where+  gbool = M1 . gbool+  M1 a &&# M1 b = M1 (a &&# b)+  M1 a ||# M1 b = M1 (a ||# b)+  M1 a ==># M1 b = M1 (a ==># b)+  gnot (M1 a) = M1 (gnot a)+  gand as = M1 (gand (map (\(M1 a) -> a) as))+  gor as = M1 (gor (map (\(M1 a) -> a) as))+  gxor (M1 a) (M1 b) = M1 (gxor a b)++-- | The normal 'Bool' operators in Haskell are not overloaded. This+-- provides a richer set that are.+--+-- Instances for this class for product-like types can be automatically derived+-- for any type that is an instance of @Generic@+class Boolean t where+  -- | Lift a 'Bool'+  bool :: Bool -> t+  default bool :: (Generic t, GBoolean (Rep t)) => Bool -> t+  bool = to . gbool+  -- |+  -- @'true' = 'bool' 'True'@+  true :: t+  true = bool True+  -- |+  -- @'false' = 'bool' 'False'@+  false :: t+  false = bool False++  -- | Logical conjunction.+  (&&) :: t -> t -> t+  default (&&) :: (Generic t, GBoolean (Rep t)) => t -> t -> t+  x && y = to (from x &&# from y)++  -- | Logical disjunction (inclusive or).+  (||) :: t -> t -> t+  default (||) :: (Generic t, GBoolean (Rep t)) => t -> t -> t+  x || y = to (from x ||# from y)++  -- | Logical implication.+  (==>) :: t -> t -> t+  default (==>) :: (Generic t, GBoolean (Rep t)) => t -> t -> t+  x ==> y = to (from x ==># from y)++  -- | Logical negation+  not :: t -> t+  default not :: (Generic t, GBoolean (Rep t)) => t -> t+  not = to . gnot . from++  -- | The logical conjunction of several values.+  and :: [t] -> t+  default and :: (Generic t, GBoolean (Rep t)) => [t] -> t+  and = to . gand . map from++  -- | The logical disjunction of several values.+  or :: [t] -> t+  default or :: (Generic t, GBoolean (Rep t)) => [t] -> t+  or = to . gor . map from++  -- | The negated logical conjunction of several values.+  --+  -- @'nand' = 'not' . 'and'@+  nand :: [t] -> t+  nand = not . and++  -- | The negated logical disjunction of several values.+  --+  -- @'nor' = 'not' . 'or'@+  nor :: [t] -> t+  nor = not . or++  -- | Exclusive-or+  xor :: t -> t -> t+  default xor :: (Generic t, GBoolean (Rep t)) => t -> t -> t+  xor x y = to (from x `gxor` from y)++  -- | Choose between two alternatives based on a selector bit.+  choose :: t  -- ^ False branch+         -> t  -- ^ True branch+         -> t  -- ^ Predicate/selector branch+         -> t+  choose f t s = (f && not s) || (t && s)++instance Boolean Bool where+  bool = id+  true = True+  false = False++  (&&) = (Prelude.&&)+  (||) = (Prelude.||)+  x ==> y = not x || y++  not = Prelude.not++  and = Prelude.and+  or = Prelude.or++  False `xor` False = False+  False `xor` True  = True+  True `xor` False  = True+  True `xor` True   = False++  choose f _ False = f+  choose _ t True  = t
+ src/Ersatz/Bits.hs view
@@ -0,0 +1,169 @@+{-# LANGUAGE TypeFamilies, DeriveDataTypeable, DeriveGeneric #-}+--------------------------------------------------------------------+-- |+-- Copyright :  (c) Edward Kmett 2010-2013, Johan Kiviniemi 2013+-- License   :  BSD3+-- Maintainer:  Edward Kmett <ekmett@gmail.com>+-- Stability :  experimental+-- Portability: non-portable+--+--------------------------------------------------------------------+module Ersatz.Bits+  ( Bit1(..), Bit2(..), Bit3(..), Bit4(..), Bit5(..), Bit6(..), Bit7(..), Bit8(..)+  ) where++import Prelude hiding ((&&), (||), and, or, not)++import Control.Applicative+import Data.Bits (Bits, (.&.), (.|.), shiftL, shiftR)+import Data.List (foldl')+import Data.Typeable+import Data.Word (Word8)+import Ersatz.Bit+import Ersatz.Decoding+import Ersatz.Equatable+import Ersatz.Encoding+import Ersatz.Variable+import GHC.Generics++newtype Bit1 = Bit1 Bit deriving (Show,Typeable,Generic)+data Bit2 = Bit2 Bit Bit deriving (Show,Typeable,Generic)+data Bit3 = Bit3 Bit Bit Bit deriving (Show,Typeable,Generic)+data Bit4 = Bit4 Bit Bit Bit Bit deriving (Show,Typeable,Generic)+data Bit5 = Bit5 Bit Bit Bit Bit Bit deriving (Show,Typeable,Generic)+data Bit6 = Bit6 Bit Bit Bit Bit Bit Bit deriving (Show,Typeable,Generic)+data Bit7 = Bit7 Bit Bit Bit Bit Bit Bit Bit deriving (Show,Typeable,Generic)+data Bit8 = Bit8 Bit Bit Bit Bit Bit Bit Bit Bit deriving (Show,Typeable,Generic)++instance Boolean Bit1+instance Boolean Bit2+instance Boolean Bit3+instance Boolean Bit4+instance Boolean Bit5+instance Boolean Bit6+instance Boolean Bit7+instance Boolean Bit8++instance Equatable Bit1+instance Equatable Bit2+instance Equatable Bit3+instance Equatable Bit4+instance Equatable Bit5+instance Equatable Bit6+instance Equatable Bit7+instance Equatable Bit8++instance Variable Bit1+instance Variable Bit2+instance Variable Bit3+instance Variable Bit4+instance Variable Bit5+instance Variable Bit6+instance Variable Bit7+instance Variable Bit8++instance Decoding Bit1 where+  type Decoded Bit1 = Word8+  decode s (Bit1 a) = boolsToNum1 <$> decode s a++instance Decoding Bit2 where+  type Decoded Bit2 = Word8+  decode s (Bit2 a b) = boolsToNum2 <$> decode s a <*> decode s b++instance Decoding Bit3 where+  type Decoded Bit3 = Word8+  decode s (Bit3 a b c) = boolsToNum3 <$> decode s a <*> decode s b <*> decode s c++instance Decoding 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++instance Decoding 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++instance Decoding 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++instance Decoding 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++instance Decoding 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+boolsToNum1 a = boolToNum a++boolsToNum2 :: Bool -> Bool -> Word8+boolsToNum2 a b = boolsToNum [a,b]++boolsToNum3 :: Bool -> Bool -> Bool -> Word8+boolsToNum3 a b c = boolsToNum [a,b,c]++boolsToNum4 :: Bool -> Bool -> Bool -> Bool -> Word8+boolsToNum4 a b c d = boolsToNum [a,b,c,d]++boolsToNum5 :: Bool -> Bool -> Bool -> Bool -> Bool -> Word8+boolsToNum5 a b c d e = boolsToNum [a,b,c,d,e]++boolsToNum6 :: Bool -> Bool -> Bool -> Bool -> Bool -> Bool -> Word8+boolsToNum6 a b c d e f = boolsToNum [a,b,c,d,e,f]++boolsToNum7 :: Bool -> Bool -> Bool -> Bool -> Bool -> Bool -> Bool -> Word8+boolsToNum7 a b c d e f g = boolsToNum [a,b,c,d,e,f,g]++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 n = bool (numToBool (n .&. 1)) : bitsOf (n `shiftR` 1)+{-# INLINE bitsOf #-}++numToBool :: (Eq a, Num a) => a -> Bool+numToBool 0 = False+numToBool _ = True+{-# INLINE numToBool #-}++boolsToNum :: (Num a, Bits a) => [Bool] -> a+boolsToNum = foldl' (\n a -> (n `shiftL` 1) .|. boolToNum a) 0+{-# INLINE boolsToNum #-}++boolToNum :: Num a => Bool -> a+boolToNum False = 0+boolToNum True  = 1+{-# INLINE boolToNum #-}
+ src/Ersatz/Decoding.hs view
@@ -0,0 +1,107 @@+{-# LANGUAGE TypeFamilies, Rank2Types #-}+--------------------------------------------------------------------+-- |+-- Copyright :  (c) Edward Kmett 2010-2013, 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 s l = solutionLiteral s l++instance Decoding Lit where+  type Decoded Lit = Bool+  decode _ (Bool b) = Just b+  decode s (Lit l)  = decode s l++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
+ src/Ersatz/Encoding.hs view
@@ -0,0 +1,98 @@+{-# LANGUAGE TypeFamilies, Rank2Types #-}+--------------------------------------------------------------------+-- |+-- Copyright :  (c) Edward Kmett 2010-2013, 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 :: *+  encode :: Encoded a -> a++instance Encoding Lit where+  type Encoded Lit = Bool+  encode = Bool++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
+ src/Ersatz/Equatable.hs view
@@ -0,0 +1,68 @@+{-# LANGUAGE TypeFamilies, TypeOperators, FlexibleInstances, DeriveDataTypeable, DeriveGeneric, DefaultSignatures, FlexibleContexts, UndecidableInstances #-}+{-# OPTIONS_HADDOCK not-home #-}+--------------------------------------------------------------------+-- |+-- Copyright :  (c) Edward Kmett 2010-2013, Johan Kiviniemi 2013+-- License   :  BSD3+-- Maintainer:  Edward Kmett <ekmett@gmail.com>+-- Stability :  experimental+-- Portability: non-portable+--+--------------------------------------------------------------------+module Ersatz.Equatable+  ( Equatable(..)+  ) where++import Prelude hiding ((&&),(||),not,and,or)+import qualified Prelude++import Ersatz.Bit+import GHC.Generics++infix  4 ===, /==++-- | Instances for this class for arbitrary types can be automatically derived from @Generic@.+class Equatable t where+  -- | Compare for equality within the SAT problem.+  (===) :: t -> t -> Bit+  default (===) :: (Generic t, GEquatable (Rep t)) => t -> t -> Bit+  a === b = from a ===# from b++  -- | Compare for inequality within the SAT problem.+  (/==) :: t -> t -> Bit++  a /== b = not (a === b)++instance Equatable Bit where+  a === b = not (xor a b)+  (/==) = xor++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)+instance (Equatable a, Equatable b, Equatable c, Equatable d, Equatable e) => Equatable (a,b,c,d,e)+instance (Equatable a, Equatable b, Equatable c, Equatable d, Equatable e, Equatable f) => Equatable (a,b,c,d,e,f)+instance (Equatable a, Equatable b, Equatable c, Equatable d, Equatable e, Equatable f, Equatable g) => Equatable (a,b,c,d,e,f,g)+instance Equatable a => Equatable (Maybe a)+instance Equatable a => Equatable [a]+instance (Equatable a, Equatable b) => Equatable (Either a b)++class GEquatable f where+  (===#) :: f a -> f a -> Bit++instance GEquatable U1 where+  U1 ===# U1 = true++instance (GEquatable f, GEquatable g) => GEquatable (f :*: g) where+  (a :*: b) ===# (c :*: d) = (a ===# c) && (b ===# d)++instance (GEquatable f, GEquatable g) => GEquatable (f :+: g) where+  L1 a ===# L1 b = a ===# b+  R1 a ===# R1 b = a ===# b+  _ ===# _ = false++instance GEquatable f => GEquatable (M1 i c f) where+  M1 x ===# M1 y = x ===# y++instance Equatable a => GEquatable (K1 i a) where+  K1 a ===# K1 b = a === b
+ src/Ersatz/Internal/Circuit.hs view
@@ -0,0 +1,55 @@+{-# LANGUAGE DeriveDataTypeable #-}+--------------------------------------------------------------------+-- |+-- Copyright :  (c) Edward Kmett 2010-2013, Johan Kiviniemi 2013+-- License   :  BSD3+-- Maintainer:  Edward Kmett <ekmett@gmail.com>+-- Stability :  experimental+-- Portability: non-portable+--+--------------------------------------------------------------------+module Ersatz.Internal.Circuit+  ( Circuit(..)+  ) where++import Control.Applicative+import Data.Foldable (Foldable, foldMap)+import Data.Monoid+import Data.Traversable (Traversable, traverse)+import Data.Typeable+import Ersatz.Internal.Literal++-- | This is used to observe the directed graph with sharing of how multiple+-- 'Ersatz.Bit.Bit' values are related.+data Circuit c+  = And [c]+  | Or [c]+  | Xor c c+  | Mux c c c  -- ^ False branch, true branch, predicate/selector branch+  | Not c+  | Var !Lit+  deriving (Show, Typeable)++instance Functor Circuit where+  fmap f (And as) = And (map f as)+  fmap f (Or as) = Or (map f as)+  fmap f (Xor a b) = Xor (f a) (f b)+  fmap f (Mux a b c) = Mux (f a) (f b) (f c)+  fmap f (Not a) = Not (f a)+  fmap _ (Var l) = Var l++instance Foldable Circuit where+  foldMap f (And as) = foldMap f as+  foldMap f (Or as) = foldMap f as+  foldMap f (Xor a b) = f a <> f b+  foldMap f (Mux a b c) = f a <> f b <> f c+  foldMap f (Not a) = f a+  foldMap _ Var{} = mempty++instance Traversable Circuit where+  traverse f (And as) = And <$> traverse f as+  traverse f (Or as) = Or <$> traverse f as+  traverse f (Xor a b) = Xor <$> f a <*> f b+  traverse f (Mux a b c) = Mux <$> f a <*> f b <*> f c+  traverse f (Not a) = Not <$> f a+  traverse _ (Var l) = pure (Var l)
+ src/Ersatz/Internal/Formula.hs view
@@ -0,0 +1,213 @@+{-# LANGUAGE Rank2Types, GeneralizedNewtypeDeriving, TypeOperators, MultiParamTypeClasses, FunctionalDependencies, FlexibleInstances, PatternGuards, DeriveDataTypeable, DefaultSignatures, TypeFamilies, BangPatterns #-}+{-# OPTIONS_HADDOCK not-home #-}+--------------------------------------------------------------------+-- |+-- Copyright :  (c) Edward Kmett 2010-2013, Johan Kiviniemi 2013+-- License   :  BSD3+-- Maintainer:  Edward Kmett <ekmett@gmail.com>+-- Stability :  experimental+-- Portability: non-portable+--+--------------------------------------------------------------------+module Ersatz.Internal.Formula+  (+  -- * Clauses+    Clause(..), clauseLiterals+  -- * Formulas+  , Formula(..)+  , formulaEmpty, formulaLiteral+  , formulaNot, formulaAnd, formulaOr, formulaXor, formulaMux+  ) where++import Control.Applicative+import Data.IntSet (IntSet)+import qualified Data.IntSet as IntSet+import qualified Data.List as List (intersperse)+import Data.Monoid+import Data.Set (Set)+import qualified Data.Set as Set+import Data.Typeable+import Ersatz.Internal.Literal++------------------------------------------------------------------------------+-- Clauses+------------------------------------------------------------------------------++-- | A disjunction of possibly negated atoms. Negated atoms are represented+-- by negating the identifier.+newtype Clause = Clause { clauseSet :: IntSet }+  deriving (Eq, Ord, Monoid, Typeable)++-- | Extract the (possibly negated) atoms referenced by a 'Clause'.+clauseLiterals :: Clause -> [Literal]+clauseLiterals (Clause is) = Literal <$> IntSet.toList is++------------------------------------------------------------------------------+-- Formulas+------------------------------------------------------------------------------++-- | A conjunction of clauses+newtype Formula = Formula { formulaSet :: Set Clause }+  deriving (Eq, Ord, Monoid, Typeable)++instance Show Formula where+  showsPrec p = showParen (p > 2) . foldr (.) id+              . List.intersperse (showString " & ") . map (showsPrec 3)+              . Set.toList . formulaSet++instance Show Clause where+  showsPrec p = showParen (p > 1) . foldr (.) id+              . List.intersperse (showString " | ") . map (showsPrec 2)+              . IntSet.toList . clauseSet+++-- | A formula with no clauses+formulaEmpty :: Formula+formulaEmpty = Formula Set.empty++-- | Assert a literal+formulaLiteral :: Literal -> Formula+formulaLiteral (Literal l) =+  Formula (Set.singleton (Clause (IntSet.singleton l)))++-- | The boolean /not/ operation+--+-- @+-- O ≡ ¬A+-- (O → ¬A) & (¬O → A)+-- (¬O | ¬A) & (O | A)+-- @+formulaNot :: Literal  -- ^ Output+           -> Literal  -- ^ Input+           -> Formula+formulaNot (Literal out) (Literal inp) = formulaFromList cls+  where+    cls = [ [-out, -inp], [out, inp] ]++-- | The boolean /and/ operation+--+-- @+-- O ≡ (A & B & C)+-- (O → (A & B & C)) & (¬O → ¬(A & B & C))+-- (¬O | (A & B & C)) & (O | ¬(A & B & C))+-- (¬O | A) & (¬O | B) & (¬O | C) & (O | ¬A | ¬B | ¬C)+-- @+formulaAnd :: Literal    -- ^ Output+           -> [Literal]  -- ^ Inputs+           -> Formula+formulaAnd (Literal out) inpLs = formulaFromList cls+  where+    cls = (out : map negate inps) : map (\inp -> [-out, inp]) inps+    inps = map literalId inpLs++-- | The boolean /or/ operation+--+-- @+-- O ≡ (A | B | C)+-- (O → (A | B | C)) & (¬O → ¬(A | B | C))+-- (¬O | (A | B | C)) & (O | ¬(A | B | C))+-- (¬O | A | B | C) & (O | (¬A & ¬B & ¬C))+-- (¬O | A | B | C) & (O | ¬A) & (O | ¬B) & (O | ¬C)+-- @+formulaOr :: Literal    -- ^ Output+          -> [Literal]  -- ^ Inputs+          -> Formula+formulaOr (Literal out) inpLs = formulaFromList cls+  where+    cls = (-out : inps)+        : map (\inp -> [out, -inp]) inps+    inps = map literalId inpLs++-- | The boolean /xor/ operation+--+-- @+-- O ≡ A ⊕ B+-- O ≡ ((¬A & B) | (A & ¬B))+-- (O → ((¬A & B) | (A & ¬B))) & (¬O → ¬((¬A & B) | (A & ¬B)))+-- @+--+-- Left hand side:+-- @+-- O → ((¬A & B) | (A & ¬B))+-- ¬O | ((¬A & B) | (A & ¬B))+-- ¬O | ((¬A | A) & (¬A | ¬B) & (A | B) & (¬B | B))+-- ¬O | ((¬A | ¬B) & (A | B))+-- (¬O | ¬A | ¬B) & (¬O | A | B)+-- @+--+-- Right hand side:+--+-- @+-- ¬O → ¬((¬A & B) | (A & ¬B))+-- O | ¬((¬A & B) | (A & ¬B))+-- O | (¬(¬A & B) & ¬(A & ¬B))+-- O | ((A | ¬B) & (¬A | B))+-- (O | ¬A | B) & (O | A | ¬B)+-- @+--+-- Result:+--+-- @+-- (¬O | ¬A | ¬B) & (¬O | A | B) & (O | ¬A | B) & (O | A | ¬B)+-- @+formulaXor :: Literal  -- ^ Output+           -> Literal  -- ^ Input+           -> Literal  -- ^ Input+           -> Formula+formulaXor (Literal out) (Literal inpA) (Literal inpB) = formulaFromList cls+  where+    cls = [ [-out, -inpA, -inpB]+          , [-out,  inpA,  inpB]+          , [ out, -inpA,  inpB]+          , [ out,  inpA, -inpB]+          ]++-- | The boolean /else-then-if/ or /mux/ operation+--+-- @+-- O ≡ (F & ¬P) | (T & P)+-- (O → ((F & ¬P) | (T & P))) & (¬O → ¬((F & ¬P) | (T & P)))+-- @+--+-- Left hand side:+--+-- @+-- O → ((F & ¬P) | (T & P))+-- ¬O | ((F & ¬P) | (T & P))+-- ¬O | ((F | T) & (F | P) & (T | ¬P) & (¬P | P))+-- ¬O | ((F | T) & (F | P) & (T | ¬P))+-- (¬O | F | T) & (¬O | F | P) & (¬O | T | ¬P)+-- @+--+-- Right hand side:+--+-- @+-- ¬O → ¬((F & ¬P) | (T & P))+-- O | ¬((F & ¬P) | (T & P))+-- O | (¬(F & ¬P) & ¬(T & P))+-- O | ((¬F | P) & (¬T | ¬P))+-- (O | ¬F | P) & (O | ¬T | ¬P)+-- @+--+-- Result:+--+-- @+-- (¬O | F | T) & (¬O | F | P) & (¬O | T | ¬P) & (O | ¬F | P) & (O | ¬T | ¬P)+-- @+formulaMux :: Literal  -- ^ Output+           -> Literal  -- ^ False branch+           -> Literal  -- ^ True branch+           -> Literal  -- ^ Predicate/selector+           -> Formula+formulaMux (Literal out) (Literal inpF) (Literal inpT) (Literal inpP) =+  formulaFromList cls+  where+    cls = [ [-out,  inpF,  inpT]+          , [-out,  inpF,  inpP]+          , [-out,  inpT, -inpP]+          , [ out, -inpF,  inpP]+          , [ out, -inpT, -inpP]+          ]++formulaFromList :: [[Int]] -> Formula+formulaFromList = Formula . Set.fromList . map (Clause . IntSet.fromList)
+ src/Ersatz/Internal/Literal.hs view
@@ -0,0 +1,44 @@+{-# LANGUAGE DeriveDataTypeable #-}+--------------------------------------------------------------------+-- |+-- Copyright :  (c) Edward Kmett 2010-2013, Johan Kiviniemi 2013+-- License   :  BSD3+-- Maintainer:  Edward Kmett <ekmett@gmail.com>+-- Stability :  experimental+-- Portability: non-portable+--+--------------------------------------------------------------------+module Ersatz.Internal.Literal+  ( Literal(..)+  , negateLiteral+  , Lit(..)+  , lit+  , negateLit+  ) where++import Data.Typeable++-- | A naked possibly-negated Atom, present in the target 'Ersatz.Solver.Solver'.+newtype Literal = Literal { literalId :: Int } deriving (Eq,Ord,Typeable)++instance Show Literal where+  showsPrec i = showsPrec i . literalId+  show = show . literalId+  showList = showList . map literalId++negateLiteral :: Literal -> Literal+negateLiteral = Literal . negate . literalId++-- | Literals with partial evaluation+data Lit+  = Lit  {-# UNPACK #-} !Literal+  | Bool !Bool+  deriving (Show, Typeable)++-- | Lift a 'Bool' to a 'Lit'+lit :: Bool -> Lit+lit = Bool++negateLit :: Lit -> Lit+negateLit (Bool b) = Bool (not b)+negateLit (Lit l) = Lit (negateLiteral l)
+ src/Ersatz/Internal/Parser.hs view
@@ -0,0 +1,62 @@+--------------------------------------------------------------------+-- |+-- Copyright :  (c) Edward Kmett 2010-2013, Johan Kiviniemi 2013+-- License   :  BSD3+-- Maintainer:  Edward Kmett <ekmett@gmail.com>+-- Stability :  experimental+-- Portability: non-portable+--+-- A trivial, inefficient parser with no support for error reporting.+--------------------------------------------------------------------+module Ersatz.Internal.Parser+  ( Parser+  , runParser+  , sepBy, sepBy1+  , token, string+  , integer, natural+  , eof+  , satisfy+  ) where++import Control.Applicative+import Control.Monad.State+import Data.Char (isDigit)+import Data.Traversable (traverse)++type Parser t a = StateT [t] [] a++runParser :: Parser t a -> [t] -> [a]+runParser = evalStateT++sepBy :: Parser t a -> Parser t sep -> Parser t [a]+sepBy p sep = sepBy1 p sep <|> pure []++sepBy1 :: Parser t a -> Parser t sep -> Parser t [a]+sepBy1 p sep = (:) <$> p <*> many (sep *> p)++token :: Eq t => t -> Parser t t+token t = satisfy (== t)++string :: Eq t => [t] -> Parser t [t]+string = traverse token++integer :: (Integral i, Read i) => Parser Char i+integer = negation <*> natural++negation :: Num n => Parser Char (n -> n)+negation  =  negate <$ token '-'+         <|> pure id++natural :: (Integral i, Read i) => Parser Char i+natural = read <$> some (satisfy isDigit)++eof :: Parser t ()+eof = do+  [] <- get+  return ()++satisfy :: (t -> Bool) -> Parser t t+satisfy f = do+  (t:ts) <- get+  guard (f t)+  t <$ put ts
+ src/Ersatz/Internal/StableName.hs view
@@ -0,0 +1,23 @@+{-# OPTIONS_HADDOCK not-home #-}+--------------------------------------------------------------------+-- |+-- Copyright :  (c) Edward Kmett 2010-2013, Johan Kiviniemi 2013+-- License   :  BSD3+-- Maintainer:  Edward Kmett <ekmett@gmail.com>+-- Stability :  experimental+-- Portability: non-portable+--+--------------------------------------------------------------------+module Ersatz.Internal.StableName+  ( StableName+  , makeStableName'+  ) where++import System.Mem.StableName (StableName, makeStableName)+import Unsafe.Coerce (unsafeCoerce)++makeStableName' :: a -> IO (StableName ())+makeStableName' a = a `seq` fmap coerceStableName (makeStableName a)+  where+    coerceStableName :: StableName a -> StableName ()+    coerceStableName = unsafeCoerce
+ src/Ersatz/Monad.hs view
@@ -0,0 +1,105 @@+{-# LANGUAGE Rank2Types, GeneralizedNewtypeDeriving, TypeOperators, MultiParamTypeClasses, FunctionalDependencies, FlexibleInstances, PatternGuards, DeriveDataTypeable, DefaultSignatures, TypeFamilies, BangPatterns #-}+{-# OPTIONS_HADDOCK not-home #-}+--------------------------------------------------------------------+-- |+-- Copyright :  (c) Edward Kmett 2010-2013, Johan Kiviniemi 2013+-- License   :  BSD3+-- Maintainer:  Edward Kmett <ekmett@gmail.com>+-- Stability :  experimental+-- Portability: non-portable+--+--------------------------------------------------------------------+module Ersatz.Monad+  (+  -- * The SAT Monad+    SAT(..)+  , MonadSAT(..)+  ) where++import Control.Applicative+import Control.Monad+import Control.Monad.Reader+import Control.Monad.RWS.Strict as Strict+import Control.Monad.RWS.Lazy as Lazy+import Control.Monad.State.Lazy as Lazy+import Control.Monad.State.Strict as Strict+import Control.Monad.Writer.Lazy as Lazy+import Control.Monad.Writer.Strict as Strict+import Data.IntSet as IntSet+import Data.HashMap.Strict as HashMap+import Ersatz.Internal.Formula+import Ersatz.Internal.Literal+import Ersatz.Internal.StableName+import Ersatz.Problem+import System.IO.Unsafe++newtype SAT m a = SAT { runSAT :: forall r. (a -> Problem -> m r) -> Problem -> m r }++instance Functor (SAT m) where+  fmap f (SAT m) = SAT $ \k -> m (k . f)+  {-# INLINE fmap #-}++instance Applicative (SAT m) where+  pure a = SAT $ \k -> k a+  {-# INLINE pure #-}++  (<*>) = ap+  {-# INLINE (<*>) #-}++instance Monad (SAT m) where+  return a = SAT $ \k -> k a+  {-# INLINE return #-}++  SAT m >>= f = SAT $ \k -> m (\a -> runSAT (f a) k)+  {-# INLINE (>>=) #-}++instance MonadTrans SAT where+  lift m = SAT $ \k p -> do+    a <- m+    k a p+  {-# INLINE lift #-}++instance MonadIO m => MonadIO (SAT m) where+  liftIO m = SAT $ \k p -> do+    a <- liftIO m+    k a p+  {-# INLINE liftIO #-}++class (Applicative m, Monad m) => MonadSAT m where+  sat :: (Problem -> (a, Problem)) -> m a+  default sat :: (MonadTrans t, MonadSAT n, m ~ t n) => (Problem -> (a, Problem)) -> m a+  sat = lift . sat++  literalExists :: m Literal+  literalExists = sat $ \qbf -> let !qbfLastAtom' = qbfLastAtom qbf + 1 in+    (Literal qbfLastAtom', qbf { qbfLastAtom = qbfLastAtom' })+  {-# INLINE literalExists #-}++  literalForall :: m Literal+  literalForall = sat $ \qbf -> let !qbfLastAtom' = qbfLastAtom qbf + 1 in+    ( Literal qbfLastAtom', qbf { qbfLastAtom = qbfLastAtom', qbfUniversals = IntSet.insert qbfLastAtom' (qbfUniversals qbf) })+  {-# INLINE literalForall #-}++  assertFormula :: Formula -> m ()+  assertFormula formula = sat $ \qbf -> ((), qbf { qbfFormula = qbfFormula qbf <> formula })+  {-# INLINE assertFormula #-}++  generateLiteral :: a -> (forall n. Literal -> SAT n ()) -> m Literal+  generateLiteral a f = sat $ \qbf -> case HashMap.lookup sn (qbfSNMap qbf) of+    Just l  -> (l, qbf)+    Nothing | !qbfLastAtom' <- qbfLastAtom qbf + 1, !l <- Literal qbfLastAtom' ->+      runSAT (f l) (\_ s -> (l, s)) qbf { qbfSNMap = HashMap.insert sn l (qbfSNMap qbf), qbfLastAtom = qbfLastAtom' }+    where sn = unsafePerformIO (makeStableName' a)+  {-# INLINE generateLiteral #-}++instance MonadSAT (SAT m) where+  sat f = SAT $ \k s -> case f s of+    (a, t) -> k a t++instance MonadSAT m => MonadSAT (ReaderT r m)+instance MonadSAT m => MonadSAT (Lazy.StateT s m)+instance MonadSAT m => MonadSAT (Strict.StateT s m)+instance (MonadSAT m, Monoid w) => MonadSAT (Lazy.WriterT w m)+instance (MonadSAT m, Monoid w) => MonadSAT (Strict.WriterT w m)+instance (MonadSAT m, Monoid w) => MonadSAT (Lazy.RWST r w s m)+instance (MonadSAT m, Monoid w) => MonadSAT (Strict.RWST r w s m)
+ src/Ersatz/Problem.hs view
@@ -0,0 +1,112 @@+{-# LANGUAGE Rank2Types, GeneralizedNewtypeDeriving, TypeOperators, MultiParamTypeClasses, FunctionalDependencies, FlexibleInstances, PatternGuards, DeriveDataTypeable, DefaultSignatures, TypeFamilies, BangPatterns #-}+{-# OPTIONS_HADDOCK not-home #-}+--------------------------------------------------------------------+-- |+-- Copyright :  (c) Edward Kmett 2010-2013, Johan Kiviniemi 2013+-- License   :  BSD3+-- Maintainer:  Edward Kmett <ekmett@gmail.com>+-- Stability :  experimental+-- Portability: non-portable+--+--------------------------------------------------------------------+module Ersatz.Problem+  (+  -- * Formulas+    Problem(qbfLastAtom, qbfFormula, qbfUniversals, qbfSNMap)+  -- * QDIMACS pretty printing+  , QDIMACS(..)+  ) where++import Data.Default+import Data.HashMap.Lazy (HashMap)+import qualified Data.HashMap.Lazy as HashMap+import Data.IntSet (IntSet)+import qualified Data.IntSet as IntSet+import qualified Data.List as List (groupBy)+import qualified Data.Set as Set+import Data.Typeable+import Ersatz.Internal.Formula+import Ersatz.Internal.Literal+import Ersatz.Internal.StableName++------------------------------------------------------------------------------+-- Problems+------------------------------------------------------------------------------++-- | A (quantified) boolean formula.+data Problem = Problem+  { qbfLastAtom   :: {-# UNPACK #-} !Int      -- ^ The id of the last atom allocated+  , qbfFormula    :: !Formula                 -- ^ a set of clauses to assert+  , qbfUniversals :: !IntSet                  -- ^ a set indicating which literals are universally quantified+  , qbfSNMap      :: !(HashMap (StableName ()) Literal)  -- ^ a mapping used during 'Bit' expansion+  -- , qbfNameMap    :: !(IntMap String)      -- ^ a map of literals to given names+  } deriving Typeable++-- TODO: instance Monoid Problem++instance Default Problem where+  def = Problem 0 (Formula Set.empty) IntSet.empty HashMap.empty++instance Show Problem where+  showsPrec p qbf = showParen (p > 10)+                  $ showString "Problem .. " . showsPrec 11 (qbfFormula qbf) . showString " .."++------------------------------------------------------------------------------+-- Printing Problems+------------------------------------------------------------------------------++-- | (Q)DIMACS file format pretty printer+--+-- This is used to generate the problem statement for a given 'SAT' 'Ersatz.Solver.Solver'.+class QDIMACS t where+  qdimacs :: t -> String++instance QDIMACS Literal where+  qdimacs (Literal n) = show n++instance QDIMACS Formula where+  qdimacs (Formula cs) = unlines $ map qdimacs (Set.toList cs)++instance QDIMACS Clause where+  qdimacs (Clause xs) = unwords $ map show (IntSet.toList xs) ++ ["0"]++instance QDIMACS Problem where+  qdimacs (Problem vars formula@(Formula cs) qs _) =+    unlines (header : map showGroup quantGroups) ++ qdimacs formula+    where+      header = unwords ["p", "cnf", show (vars + padding), show (Set.size cs) ]++      -- "The innermost quantified set is always of type 'e'" per QDIMACS standard+      padding | Just (n, _) <- IntSet.maxView qs, n == vars = 1+              | otherwise                                   = 0+                    -- no universals means we are a plan DIMACS file+      quantGroups | IntSet.null qs = []+                    -- otherwise, skip to the first universal and show runs+                  | otherwise = List.groupBy eqQuant $ quants [head qlist..vars] qlist+        where qlist = IntSet.toAscList qs++      showGroup :: [Quant] -> String+      showGroup xs = unwords $ q (head xs) : map (show . getQuant) xs++      eqQuant :: Quant -> Quant -> Bool+      eqQuant Exists{} Exists{} = True+      eqQuant Forall{} Forall{} = True+      eqQuant _ _ = False++      q :: Quant -> String+      q Exists{} = "e"+      q Forall{} = "a"++      quants :: [Int] -> [Int] -> [Quant]+      quants [] _ = []+      quants (i:is) []     = Exists i : quants is []+      quants (i:is) jjs@(j:js)+        | i == j    = Forall i : quants is js+        | otherwise = Exists i : quants is jjs++-- | An explicit prenex quantifier+data Quant+  = Exists { getQuant :: {-# UNPACK #-} !Int }+  | Forall { getQuant :: {-# UNPACK #-} !Int }+  deriving Typeable+
+ src/Ersatz/Solution.hs view
@@ -0,0 +1,63 @@+{-# LANGUAGE Rank2Types, ImpredicativeTypes, DeriveDataTypeable #-}+--------------------------------------------------------------------+-- |+-- Copyright :  (c) Edward Kmett 2010-2013, Johan Kiviniemi 2013+-- License   :  BSD3+-- Maintainer:  Edward Kmett <ekmett@gmail.com>+-- Stability :  experimental+-- Portability: non-portable+--+--------------------------------------------------------------------+module Ersatz.Solution+  ( Solution(..), solutionFrom+  , Result(..)+  , Solver+  ) where++import Control.Applicative+import qualified Data.HashMap.Lazy as HashMap+import Data.IntMap (IntMap)+import qualified Data.IntMap as IntMap+import Data.Ix+import Data.Typeable+import Ersatz.Internal.Literal+import Ersatz.Problem+import System.Mem.StableName (StableName)++data Solution = Solution+  { solutionLiteral    :: Literal -> Maybe Bool+  , solutionStableName :: StableName () -> Maybe Bool+  } deriving Typeable++solutionFrom :: IntMap Bool -> Problem -> Solution+solutionFrom litMap qbf = Solution lookupLit lookupSN+  where+    lookupLit l | i >= 0    = IntMap.lookup i litMap+                | otherwise = not <$> IntMap.lookup (-i) litMap+      where i = literalId l++    lookupSN sn = lookupLit =<< HashMap.lookup sn snMap++    snMap = qbfSNMap qbf++data Result+  = Unsolved+  | Unsatisfied+  | Satisfied+  deriving (Eq,Ord,Ix,Show,Read)++instance Enum Result where+  fromEnum Unsolved = (-1)+  fromEnum Unsatisfied = 0+  fromEnum Satisfied = 1++  toEnum (-1) = Unsolved+  toEnum 0 = Unsatisfied+  toEnum 1 = Satisfied+  toEnum _ = error "Enum.toEnum {Ersatz.Solution.Result}: argument of out range"++instance Bounded Result where+  minBound = Unsolved+  maxBound = Satisfied++type Solver m = Problem -> m (Result, IntMap Bool)
+ src/Ersatz/Solver.hs view
@@ -0,0 +1,25 @@+--------------------------------------------------------------------+-- |+-- Copyright :  (c) Edward Kmett 2010-2013, Johan Kiviniemi 2013+-- License   :  BSD3+-- Maintainer:  Edward Kmett <ekmett@gmail.com>+-- Stability :  experimental+-- Portability: non-portable+--+--------------------------------------------------------------------+module Ersatz.Solver+  ( module Ersatz.Solver.Minisat+  , solveWith+  ) where++import Data.Default+import Ersatz.Decoding+import Ersatz.Monad+import Ersatz.Solution+import Ersatz.Solver.Minisat++solveWith :: (Monad m, Decoding a) => Solver m -> SAT m a -> m (Result, Maybe (Decoded a))+solveWith solver m = do+  (a, qbf) <- runSAT m (\a s -> return (a , s)) def+  (res, litMap) <- solver qbf+  return (res, decode (solutionFrom litMap qbf) a)
+ src/Ersatz/Solver/Minisat.hs view
@@ -0,0 +1,86 @@+--------------------------------------------------------------------+-- |+-- Copyright :  (c) Edward Kmett 2010-2013, Johan Kiviniemi 2013+-- License   :  BSD3+-- Maintainer:  Edward Kmett <ekmett@gmail.com>+-- Stability :  experimental+-- Portability: non-portable+--+--------------------------------------------------------------------+module Ersatz.Solver.Minisat+  ( minisat+  , cryptominisat+  , minisatPath+  ) where++import Control.Applicative+import Control.Exception (IOException, handle)+import Control.Monad+import Control.Monad.IO.Class+import Data.IntMap (IntMap)+import qualified Data.IntMap as IntMap+import Ersatz.Internal.Parser+import Ersatz.Problem (qdimacs)+import Ersatz.Solution+import System.Exit (ExitCode(..))+import System.IO.Temp (withSystemTempDirectory)+import System.Process (readProcessWithExitCode)+++minisat :: MonadIO m => Solver m+minisat = minisatPath "minisat"++cryptominisat :: MonadIO m => Solver m+cryptominisat = minisatPath "cryptominisat"++minisatPath :: MonadIO m => FilePath -> Solver m+minisatPath path qbf = liftIO $+  withSystemTempDirectory "ersatz" $ \dir -> do+    let problemPath  = dir ++ "/problem.cnf"+        solutionPath = dir ++ "/solution"++    writeFile problemPath (qdimacs qbf)++    (exit, _out, _err) <-+      readProcessWithExitCode path [problemPath, solutionPath] []++    sol <- parseSolutionFile solutionPath++    return (resultOf exit, sol)++resultOf :: ExitCode -> Result+resultOf (ExitFailure 10) = Satisfied+resultOf (ExitFailure 20) = Unsatisfied+resultOf _                = Unsolved++parseSolutionFile :: FilePath -> IO (IntMap Bool)+parseSolutionFile path = handle handler $ do+  parseSolution <$> readFile path+  where+    handler :: IOException -> IO (IntMap Bool)+    handler _ = return IntMap.empty++parseSolution :: String -> (IntMap Bool)+parseSolution input =+  case runParser solution input of+    (s:_) -> s+    _     -> IntMap.empty++solution :: Parser Char (IntMap Bool)+solution = do+  _ <- string "SAT\n"+  IntMap.fromList <$> values++values :: Parser Char [(Int, Bool)]+values  = (value `sepBy` token ' ')+       <* string " 0"+       <* (() <$ token '\n' <|> eof)++value :: Parser Char (Int, Bool)+value = do+  i <- integer+  guard (i /= 0)+  return (toPair i)+  where+    toPair n | n >= 0    = ( n, True)+             | otherwise = (-n, False)
+ src/Ersatz/Variable.hs view
@@ -0,0 +1,64 @@+{-# LANGUAGE DefaultSignatures, TypeOperators, FlexibleContexts, UndecidableInstances #-}+--------------------------------------------------------------------+-- |+-- Copyright :  (c) Edward Kmett 2010-2013, Johan Kiviniemi 2013+-- License   :  BSD3+-- Maintainer:  Edward Kmett <ekmett@gmail.com>+-- Stability :  experimental+-- Portability: non-portable+--+--------------------------------------------------------------------+module Ersatz.Variable+  ( Variable(..)+  ) where++import Control.Applicative+import Ersatz.Internal.Literal+import Ersatz.Monad+import GHC.Generics++class GVariable f where+  gexists :: MonadSAT m => m (f a)+  gforall :: MonadSAT m => m (f a)++instance GVariable U1 where+  gexists = return U1+  gforall = return U1++instance (GVariable f, GVariable g) => GVariable (f :*: g) where+  gexists = (:*:) <$> gexists <*> gexists+  gforall = (:*:) <$> gforall <*> gforall++instance Variable a => GVariable (K1 i a) where+  gexists = K1 <$> exists+  gforall = K1 <$> forall++instance GVariable f => GVariable (M1 i c f) where+  gexists = M1 <$> gexists+  gforall = M1 <$> gforall++-- | 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 :: MonadSAT m => m t+  default exists :: (MonadSAT m, Generic t, GVariable (Rep t)) => m t+  exists = to <$> gexists++  forall :: MonadSAT m => m t+  default forall :: (MonadSAT m, Generic t, GVariable (Rep t)) => m t+  forall = to <$> gforall++instance Variable Lit where+  exists = Lit <$> exists+  forall = Lit <$> forall++instance Variable Literal where+  exists = literalExists+  forall = literalForall++instance (Variable a, Variable b) => Variable (a,b)+instance (Variable a, Variable b, Variable c) => Variable (a,b,c)+instance (Variable a, Variable b, Variable c, Variable d) => Variable (a,b,c,d)+instance (Variable a, Variable b, Variable c, Variable d, Variable e) => Variable (a,b,c,d,e)+instance (Variable a, Variable b, Variable c, Variable d, Variable e, Variable f) => Variable (a,b,c,d,e,f)+instance (Variable a, Variable b, Variable c, Variable d, Variable e, Variable f, Variable g) => Variable (a,b,c,d,e,f,g)
+ tests/doctests.hsc view
@@ -0,0 +1,72 @@+{-# LANGUAGE CPP #-}+{-# LANGUAGE ForeignFunctionInterface #-}+-----------------------------------------------------------------------------+-- |+-- Module      :  Main (doctests)+-- Copyright   :  (C) 2012-13 Edward Kmett+-- License     :  BSD-style (see the file LICENSE)+-- Maintainer  :  Edward Kmett <ekmett@gmail.com>+-- Stability   :  provisional+-- Portability :  portable+--+-- This module provides doctests for a project based on the actual versions+-- of the packages it was built with. It requires a corresponding Setup.lhs+-- to be added to the project+-----------------------------------------------------------------------------+module Main where++import Build_doctests (deps)+import Control.Applicative+import Control.Monad+import Data.List+import System.Directory+import System.FilePath+import Test.DocTest++##if defined(i386_HOST_ARCH)+##define USE_CP+import Control.Applicative+import Control.Exception+import Foreign.C.Types+foreign import stdcall "windows.h SetConsoleCP" c_SetConsoleCP :: CUInt -> IO Bool+foreign import stdcall "windows.h GetConsoleCP" c_GetConsoleCP :: IO CUInt+##elif defined(x64_64_HOST_ARCH)+##define USE_CP+import Control.Applicative+import Control.Exception+import Foreign.C.Types+foreign import ccall "windows.h SetConsoleCP" c_SetConsoleCP :: CUInt -> IO Bool+foreign import ccall "windows.h GetConsoleCP" c_GetConsoleCP :: IO CUInt+##endif++-- | Run in a modified codepage where we can print UTF-8 values on Windows.+withUnicode :: IO a -> IO a+##ifdef USE_CP+withUnicode m = do+  cp <- c_GetConsoleCP+  (c_SetConsoleCP 65001 >> m) `finally` c_SetConsoleCP cp+##else+withUnicode m = m+##endif++main :: IO ()+main = withUnicode $ getSources >>= \sources -> doctest $+    "-isrc"+  : "-idist/build/autogen"+  : "-optP-include"+  : "-optPdist/build/autogen/cabal_macros.h"+  : "-hide-all-packages"+  : "-Iincludes"+  : map ("-package="++) deps ++ sources++getSources :: IO [FilePath]+getSources = filter (isSuffixOf ".hs") <$> go "src"+  where+    go dir = do+      (dirs, files) <- getFilesAndDirectories dir+      (files ++) . concat <$> mapM go dirs++getFilesAndDirectories :: FilePath -> IO ([FilePath], [FilePath])+getFilesAndDirectories dir = do+  c <- map (dir </>) . filter (`notElem` ["..", "."]) <$> getDirectoryContents dir+  (,) <$> filterM doesDirectoryExist c <*> filterM doesFileExist c
+ tests/properties.hs view
@@ -0,0 +1,45 @@+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+-}