diff --git a/.gitignore b/.gitignore
--- a/.gitignore
+++ b/.gitignore
@@ -8,6 +8,10 @@
 .*.swp
 .*.swo
 *.o
+*.p_o
 *.hi
+*.p_hi
 *~
 *#
+*.prof
+*.hp
diff --git a/.travis.yml b/.travis.yml
--- a/.travis.yml
+++ b/.travis.yml
@@ -1,40 +1,90 @@
+# This file has been generated -- see https://github.com/hvr/multi-ghc-travis
 language: c
 sudo: false
 
+cache:
+  directories:
+    - $HOME/.cabsnap
+    - $HOME/.cabal/packages
+
+before_cache:
+  - rm -fv $HOME/.cabal/packages/hackage.haskell.org/build-reports.log
+  - rm -fv $HOME/.cabal/packages/hackage.haskell.org/00-index.tar
+
 matrix:
   include:
-    - env: CABALVER=1.18 GHCVER=7.8.4 GHCOPTS="-Werror" JOPTS="-j2"
-      addons: {apt: {packages: [cabal-install-1.18, ghc-7.8.4], sources: [hvr-ghc]}}
-    - env: CABALVER=1.22 GHCVER=7.10.1 GHCOPTS="" JOPTS="-j2"
-      addons: {apt: {packages: [cabal-install-1.22, ghc-7.10.1],sources: [hvr-ghc]}}
+    - env: CABALVER=1.24 GHCVER=7.10.3 GHCOPTS="" JOPTS="-j2"
+      compiler: ": #GHC 7.10.3"
+      addons: {apt: {packages: [cabal-install-1.24,ghc-7.10.3,minisat],sources: [hvr-ghc]}}
+    - env: CABALVER=1.24 GHCVER=8.0.2 GHCOPTS="" JOPTS="-j2"
+      compiler: ": #GHC 8.0.2"
+      addons: {apt: {packages: [cabal-install-1.24,ghc-8.0.2,minisat],sources: [hvr-ghc]}}
+    - env: CABALVER=1.24 GHCVER=8.2.1 GHCOPTS="" JOPTS="-j2"
+      compiler: ": #GHC 8.2.1"
+      addons: {apt: {packages: [cabal-install-1.24,ghc-8.2.1,minisat],sources: [hvr-ghc]}}
     - env: CABALVER=head GHCVER=head GHCOPTS="" JOPTS="-j2"
-      addons: {apt: {packages: [cabal-install-head,ghc-head],  sources: [hvr-ghc]}}
+      compiler: ": #GHC head"
+      addons: {apt: {packages: [cabal-install-head,ghc-head,minisat],sources: [hvr-ghc]}}
 
   allow_failures:
    - env: CABALVER=head GHCVER=head GHCOPTS="" JOPTS="-j2"
 
 before_install:
- - export PATH=/opt/ghc/$GHCVER/bin:/opt/cabal/$CABALVER/bin:$PATH
- - export CABAL=cabal-$CABALVER
- - $CABAL --version
- - travis_retry $CABAL update
+ - unset CC
+ - export HAPPYVER=1.19.5
+ - export ALEXVER=3.1.7
+ - export PATH=~/.cabal/bin:/opt/ghc/$GHCVER/bin:/opt/cabal/$CABALVER/bin:/opt/happy/$HAPPYVER/bin:/opt/alex/$ALEXVER/bin:$PATH
 
 install:
- - |    
-   if [ $GHCVER = "head" ] || [ $GHCVER = "7.8.4" ] || [ $GHCVER = "7.10.1" ]; then
-     $CABAL install --constraint=transformers\ installed happy alex
-     export PATH=$HOME/.cabal/bin:$PATH
+ - cabal --version
+ - echo "$(ghc --version) [$(ghc --print-project-git-commit-id 2> /dev/null || echo '?')]"
+ - if [ -f $HOME/.cabal/packages/hackage.haskell.org/00-index.tar.gz ];
+   then
+     zcat $HOME/.cabal/packages/hackage.haskell.org/00-index.tar.gz >
+          $HOME/.cabal/packages/hackage.haskell.org/00-index.tar;
    fi
- - $CABAL install $JOPTS --enable-tests --only-dependencies --force
+ - travis_retry cabal update
+ - "sed -i  's/^jobs:.*$/jobs: 2/' $HOME/.cabal/config"
+ - cabal install --only-dependencies --enable-tests --enable-benchmarks --dry -v > installplan.txt
+ - sed -i -e '1,/^Resolving /d' installplan.txt; cat installplan.txt
 
-script:
- - $CABAL configure -v2 --enable-tests
- - $CABAL build $JOPTS --ghc-options=$GHCOPTS
- - |
-   if [ $GHCVER != "head" ]; then
-     $CABAL test
+# check whether current requested install-plan matches cached package-db snapshot
+ - if diff -u installplan.txt $HOME/.cabsnap/installplan.txt;
+   then
+     echo "cabal build-cache HIT";
+     rm -rfv .ghc;
+     cp -a $HOME/.cabsnap/ghc $HOME/.ghc;
+     cp -a $HOME/.cabsnap/lib $HOME/.cabsnap/share $HOME/.cabsnap/bin $HOME/.cabal/;
+   else
+     echo "cabal build-cache MISS";
+     rm -rf $HOME/.cabsnap;
+     mkdir -p $HOME/.ghc $HOME/.cabal/lib $HOME/.cabal/share $HOME/.cabal/bin;
+     cabal install --only-dependencies --enable-tests --enable-benchmarks;
    fi
 
+# snapshot package-db on cache miss
+ - if [ ! -d $HOME/.cabsnap ];
+   then
+      echo "snapshotting package-db to build-cache";
+      mkdir $HOME/.cabsnap;
+      cp -a $HOME/.ghc $HOME/.cabsnap/ghc;
+      cp -a $HOME/.cabal/lib $HOME/.cabal/share $HOME/.cabal/bin installplan.txt $HOME/.cabsnap/;
+   fi
+
+# Here starts the actual work to be performed for the package under test;
+# any command which exits with a non-zero exit code causes the build to fail.
+script:
+ - cabal configure --enable-tests --enable-benchmarks -v2  # -v2 provides useful information for debugging
+ - cabal build $JOPTS --ghc-options=$GHCOPTS # this builds all libraries and executables (including tests)
+ - cabal test
+ - cabal sdist   # tests that a source-distribution can be generated
+
+# Check that the resulting source distribution can be built & installed.
+# If there are no other `.tar.gz` files in `dist`, this can be even simpler:
+# `cabal install --force-reinstalls dist/*-*.tar.gz`
+ - SRC_TGZ=$(cabal info . | awk '{print $2;exit}').tar.gz &&
+   (cd dist && cabal install $JOPTS --ghc-options=$GHCOPTS --force-reinstalls "$SRC_TGZ")
+
 notifications:
   irc:
     channels:
@@ -42,3 +92,4 @@
     skip_join: true
     template:
       - "\x0313ersatz\x0f/\x0306%{branch}\x0f \x0314%{commit}\x0f %{message} \x0302\x1f%{build_url}\x0f"
+# EOF
diff --git a/CHANGELOG.md b/CHANGELOG.md
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -1,3 +1,14 @@
+0.4
+---
+* Performance improvements for CNF printing and parsing
+* Add the `Ersatz.Counting`, `Ersatz.Relation`, `Ersatz.Relation.Data`,
+  `Ersatz.Relation.Prop`, and `Ersatz.Relation.Op` modules
+* Eliminate the `Or` constructor from `Bit` towards using AIG
+* Fix error in the SAT encoding of the `choose` function
+* Revamp `Setup.hs` to use `cabal-doctest`. This makes it build
+  with `Cabal-2.0`, and makes the `doctest`s work with `cabal new-build` and
+  sandboxes.
+
 0.3.1
 -----
 * Removed the explicit `Safe` annotations. They can't be maintained by mere mortals. Patches to mark packages upstream as `Trustworthy` will be accepted as needed.
diff --git a/README.md b/README.md
--- a/README.md
+++ b/README.md
@@ -1,6 +1,6 @@
 # Ersatz
 
-[![Build Status](https://secure.travis-ci.org/ekmett/ersatz.png)](http://travis-ci.org/ekmett/ersatz)
+[![Hackage](https://img.shields.io/hackage/v/ersatz.svg)](https://hackage.haskell.org/package/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.
 
@@ -18,7 +18,7 @@
 half_adder a b = (a `xor` b, a && b)
 ```
 
-as opposed to the following code in [satchmo](http://dfa.imn.htwk-leipzig.de/satchmo/):
+as opposed to the following code in [satchmo](https://hackage.haskell.org/package/satchmo/):
 
 
 ```haskell
diff --git a/Setup.lhs b/Setup.lhs
--- a/Setup.lhs
+++ b/Setup.lhs
@@ -1,55 +1,34 @@
-#!/usr/bin/runhaskell
 \begin{code}
+{-# LANGUAGE CPP #-}
 {-# OPTIONS_GHC -Wall #-}
 module Main (main) where
 
-import Data.List ( nub )
-import Data.Version ( showVersion )
-import Distribution.Package ( PackageName(PackageName), Package, PackageId, InstalledPackageId, packageVersion, packageName )
-import Distribution.PackageDescription ( PackageDescription(), TestSuite(..) )
-import Distribution.Simple ( defaultMainWithHooks, UserHooks(..), simpleUserHooks )
-import Distribution.Simple.Utils ( rewriteFile, createDirectoryIfMissingVerbose, copyFiles )
-import Distribution.Simple.BuildPaths ( autogenModulesDir )
-import Distribution.Simple.Setup ( BuildFlags(buildVerbosity), Flag(..), fromFlag, HaddockFlags(haddockDistPref))
-import Distribution.Simple.LocalBuildInfo ( withLibLBI, withTestLBI, LocalBuildInfo(), ComponentLocalBuildInfo(componentPackageDeps) )
-import Distribution.Text ( display )
-import Distribution.Verbosity ( Verbosity, normal )
-import System.FilePath ( (</>) )
+#ifndef MIN_VERSION_cabal_doctest
+#define MIN_VERSION_cabal_doctest(x,y,z) 0
+#endif
 
+#if MIN_VERSION_cabal_doctest(1,0,0)
+
+import Distribution.Extra.Doctest ( defaultMainWithDoctests )
 main :: IO ()
-main = defaultMainWithHooks simpleUserHooks
-  { buildHook = \pkg lbi hooks flags -> do
-     generateBuildModule (fromFlag (buildVerbosity flags)) pkg lbi
-     buildHook simpleUserHooks pkg lbi hooks flags
-  , postHaddock = \args flags pkg lbi -> do
-     copyFiles normal (haddockOutputDir flags pkg) [("notes","SPOILER.html"), ("notes","grid.pdf")]
-     postHaddock simpleUserHooks args flags pkg lbi
-  }
+main = defaultMainWithDoctests "doctests"
 
-haddockOutputDir :: Package p => HaddockFlags -> p -> FilePath
-haddockOutputDir flags pkg = destDir where
-  baseDir = case haddockDistPref flags of
-    NoFlag -> "."
-    Flag x -> x
-  destDir = baseDir </> "doc" </> "html" </> display (packageName pkg)
+#else
 
-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)
+#ifdef MIN_VERSION_Cabal
+-- If the macro is defined, we have new cabal-install,
+-- but for some reason we don't have cabal-doctest in package-db
+--
+-- Probably we are running cabal sdist, when otherwise using new-build
+-- workflow
+import Warning ()
+#endif
 
-testDeps :: ComponentLocalBuildInfo -> ComponentLocalBuildInfo -> [(InstalledPackageId, PackageId)]
-testDeps xs ys = nub $ componentPackageDeps xs ++ componentPackageDeps ys
+import Distribution.Simple
+
+main :: IO ()
+main = defaultMain
+
+#endif
 
 \end{code}
diff --git a/Warning.hs b/Warning.hs
new file mode 100644
--- /dev/null
+++ b/Warning.hs
@@ -0,0 +1,5 @@
+module Warning
+  {-# WARNING ["You are configuring this package without cabal-doctest installed.",
+               "The doctests test-suite will not work as a result.",
+               "To fix this, install cabal-doctest before configuring."] #-}
+  () where
diff --git a/ersatz.cabal b/ersatz.cabal
--- a/ersatz.cabal
+++ b/ersatz.cabal
@@ -1,5 +1,5 @@
 name:           ersatz
-version:        0.3.1
+version:        0.4
 license:        BSD3
 license-file:   LICENSE
 author:         Edward A. Kmett, Eric Mertens, Johan Kiviniemi
@@ -65,7 +65,7 @@
   .
   @ersatz-regexp-grid@
   .
-  This solves the \"regular crossword puzzle\" (<grid.pdf>) from the 2013 MIT mystery hunt.
+  This solves the \"regular crossword puzzle\" (<https://github.com/ekmett/ersatz/raw/master/notes/grid.pdf grid.pdf>) from the 2013 MIT mystery hunt.
   .
   > % time ersatz-regexp-grid
   .
@@ -75,7 +75,7 @@
 
 build-type:     Custom
 cabal-version:  >= 1.10
-tested-with:    GHC == 7.8.3, GHC == 7.10.1
+tested-with:    GHC == 7.10.3, GHC == 8.0.2, GHC == 8.2.1
 extra-source-files:
   .ghci
   .gitignore
@@ -83,6 +83,7 @@
   AUTHORS.md
   CHANGELOG.md
   README.md
+  Warning.hs
   notes/SPOILER.html
   notes/grid.pdf
   notes/papers.md
@@ -147,6 +148,12 @@
   data/dimacs/phole/hole7.cnf
   data/dimacs/phole/hole8.cnf
 
+custom-setup
+  setup-depends:
+    base          >= 4.3 && <5,
+    Cabal         >= 1.10,
+    cabal-doctest >= 1 && <1.1
+
 source-repository head
   type: git
   location: git://github.com/ekmett/ersatz.git
@@ -169,16 +176,17 @@
 
   build-depends:
     array                >= 0.2      && < 0.6,
-    base                 >= 4.7      && < 5,
+    base                 >= 4.8      && < 5,
     bytestring           >= 0.10.4.0 && < 0.12,
     containers           >= 0.2.0.1  && < 0.6,
     data-default         >= 0.5      && < 0.8,
     lens                 >= 3.8      && < 5,
     mtl                  >= 1.1      && < 2.3,
-    process              >= 1.1      && < 1.5,
+    process              >= 1.1      && < 1.7,
     temporary            >= 1.1      && < 1.3,
     transformers         >= 0.3      && < 0.6,
-    unordered-containers == 0.2.*
+    unordered-containers == 0.2.*,
+    attoparsec
 
   if impl(ghc >= 7.4 && < 7.6)
     build-depends: ghc-prim
@@ -198,14 +206,17 @@
     Ersatz.Solver
     Ersatz.Solver.DepQBF
     Ersatz.Solver.Minisat
-    Ersatz.Solver.Z3
     Ersatz.Variable
+    Ersatz.Counting
+    Ersatz.Relation
 
   other-modules:
     Ersatz.Internal.Parser
     Ersatz.Internal.StableName
     Ersatz.Solver.Common
-
+    Ersatz.Relation.Data
+    Ersatz.Relation.Prop
+    Ersatz.Relation.Op
 
 executable ersatz-regexp-grid
   -- description: An example program that solves the regular expression crossword problem <http://www.coinheist.com/rubik/a_regular_crossword/> using Ersatz.
@@ -296,3 +307,24 @@
     build-depends:
       base,
       hlint >= 1.7
+
+test-suite speed
+  type: exitcode-stdio-1.0
+  main-is: Speed.hs
+  hs-source-dirs: tests
+  build-depends: base, ersatz
+  default-language: Haskell2010
+
+test-suite moore
+  type: exitcode-stdio-1.0
+  main-is: Moore.hs
+  hs-source-dirs: tests
+  build-depends: base, array, mtl, ersatz
+  default-language: Haskell2010
+
+test-suite z001
+  type: exitcode-stdio-1.0
+  main-is: Z001.hs
+  hs-source-dirs: tests
+  build-depends: base, mtl, ersatz
+  default-language: Haskell2010
diff --git a/examples/regexp-grid/Main.hs b/examples/regexp-grid/Main.hs
--- a/examples/regexp-grid/Main.hs
+++ b/examples/regexp-grid/Main.hs
@@ -11,7 +11,7 @@
 
 main :: IO ()
 main = do
-  (res, msol) <- solveWith minisat problem
+  (res, msol) <- solveWith cryptominisat problem
   when (res /= Satisfied) (fail (show res))
   case msol of
     Nothing  -> fail "Sol was Nothing"
diff --git a/src/Ersatz/Bit.hs b/src/Ersatz/Bit.hs
--- a/src/Ersatz/Bit.hs
+++ b/src/Ersatz/Bit.hs
@@ -7,6 +7,8 @@
 {-# LANGUAGE DeriveDataTypeable #-}
 {-# LANGUAGE UndecidableInstances #-}
 {-# LANGUAGE Trustworthy #-}
+{-# LANGUAGE Rank2Types #-}
+{-# LANGUAGE StandaloneDeriving #-}
 {-# OPTIONS_HADDOCK not-home #-}
 --------------------------------------------------------------------
 -- |
@@ -34,6 +36,7 @@
 import Data.Foldable (toList)
 #endif
 import qualified Data.Foldable as Foldable
+import qualified Data.Traversable as Traversable
 import Data.Sequence (Seq, (<|), (|>), (><))
 import qualified Data.Sequence as Seq
 import Data.Typeable
@@ -56,14 +59,25 @@
 -- | A 'Bit' provides a reference to a possibly indeterminate boolean
 -- value that can be determined by an external SAT solver.
 data Bit
-  = And (Seq Bit)
-  | Or (Seq Bit)
-  | Xor Bit Bit
-  | Mux Bit Bit Bit
-  | Not Bit
+  = And !(Seq Bit)
+  | Xor !Bit !Bit
+  | Mux !Bit !Bit !Bit
+  | Not !Bit
   | Var !Literal
-  deriving (Show, Typeable)
+  | Run ( forall m s . (MonadState s m, HasSAT s) => m Bit )
+  deriving (Typeable)
 
+instance Show Bit where
+  showsPrec d (And xs)  = showParen (d > 10) $
+    showString "And " . showsPrec 11 xs
+  showsPrec d (Xor x y) = showParen (d > 10) $
+    showString "Xor " . showsPrec 11 x . showChar ' ' . showsPrec 11 y
+  showsPrec d (Mux x y z) = showParen (d > 10) $
+    showString "Mux " . showsPrec 11 x . showChar ' ' . showsPrec 11 y . showChar ' ' . showsPrec 11 z
+  showsPrec d (Not x)  = showParen (d > 10) $ showString "Not " . showsPrec 11 x
+  showsPrec d (Var x)  = showParen (d > 10) $ showString "Var " . showsPrec 11 x
+  showsPrec d (Run _)  = showParen (d > 10) $ showString "Run ..."
+
 instance Boolean Bit where
   -- improve the stablemap this way
   bool True  = true
@@ -71,25 +85,8 @@
   true  = Var literalTrue
   false = Var literalFalse
 
-  a@(Var (Literal (-1))) && _ = a
-  _ && b@(Var (Literal (-1))) = b
-  a && Var (Literal 1) = a
-  Var (Literal 1) && b = b
-  And as && And bs = And (as >< bs)
-  And as && b      = And (as |> b)
-  a            && And bs = And (a <| bs)
-  a            && b      = And (a <| b <| Seq.empty)
-
-  a || Var (Literal (-1)) = a
-  Var (Literal (-1)) || b = b
-
-  a@(Var (Literal 1)) || _ = a
-  _ || b@(Var (Literal 1)) = b
-
-  Or as || Or bs = Or (as >< bs)
-  Or as || b     = Or (as |> b)
-  a     || Or bs = Or (a <| bs)
-  a     || b     = Or (a <| b <| Seq.empty)
+  (&&) = and2
+  a || b = not (not a && not b)
 
   not (Not c) = c
   not (Var l) = Var (negateLiteral l)
@@ -99,18 +96,33 @@
   Var (Literal (-1)) `xor` b = b
   a `xor` Var (Literal 1) = not a
   Var (Literal 1) `xor` b = not b
+  -- following 3 clauses might enable some AIG magic
+  Not a `xor` Not b = Xor a b
+  a `xor` Not b = Not (Xor a b)
+  Not a `xor` b = Not (Xor a b)
   a `xor` b    = Xor a b
 
   and = Foldable.foldl' (&&) true
-  or  = Foldable.foldl' (||) false
+  or  = not . and . map not . toList
 
   all p = Foldable.foldl' (\res b -> res && p b) true
-  any p = Foldable.foldl' (\res b -> res || p b) false
+  any p = not . all (not . p)
 
   choose f _ (Var (Literal (-1))) = f
   choose _ t (Var (Literal 1))    = t
+  choose t f (Not s) = choose f t s 
   choose f t s = Mux f t s
 
+and2 :: Bit -> Bit -> Bit
+and2 a@(Var (Literal (-1))) _ = a
+and2 _ b@(Var (Literal (-1))) = b
+and2 a (Var (Literal 1)) = a
+and2 (Var (Literal 1)) b = b
+and2 (And as) (And bs) = And (as >< bs)
+and2 (And as) b      = And (as |> b)
+and2 a (And bs) = And (a <| bs)
+and2 a b = And (a <| b <| Seq.empty)
+
 instance Variable Bit where
   literally = liftM Var . literally
 
@@ -119,19 +131,19 @@
   type Decoded Bit = Bool
   encode = bool
   decode sol b
-      = maybe (pure False <|> pure True) pure $ 
+      = 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
           And cs  -> andMaybeBools . toList $ decode sol <$> cs
-          Or cs   -> orMaybeBools  . toList $ 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
+          Run _ -> mzero
     where
       andMaybeBools :: [Maybe Bool] -> Maybe Bool
       andMaybeBools mbs
@@ -141,14 +153,6 @@
         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
@@ -158,6 +162,11 @@
 -- | Assert claims that 'Bit' must be 'true' in any satisfying interpretation
 -- of the current problem.
 assert :: (MonadState s m, HasSAT s) => Bit -> m ()
+assert (And bs) = Foldable.for_ bs assert
+-- the following (when switched on, False => True) produces extra clauses, why?
+assert (Not (And bs)) | False = do
+  ls <- Traversable.for bs runBit
+  assertFormula $ fromClause $ foldMap (fromLiteral . negateLiteral) ls
 assert b = do
   l <- runBit b
   assertFormula (formulaLiteral l)
@@ -166,16 +175,17 @@
 runBit :: (MonadState s m, HasSAT s) => Bit -> m Literal
 runBit (Not c) = negateLiteral `liftM` runBit c
 runBit (Var l) = return l
+runBit (Run action) = action >>= runBit
 runBit b = generateLiteral b $ \out ->
   assertFormula =<< case b of
     And bs    -> formulaAnd out `liftM` mapM runBit (toList bs)
-    Or  bs    -> formulaOr  out `liftM` mapM runBit (toList bs)
     Xor x y   -> liftM2 (formulaXor out) (runBit x) (runBit y)
     Mux x y p -> liftM3 (formulaMux out) (runBit x) (runBit y) (runBit p)
 
     -- Already handled above but GHC doesn't realize it.
     Not _ -> error "Unreachable"
     Var _ -> error "Unreachable"
+    Run _ -> error "Unreachable"
 
 class GBoolean f where
   gbool :: Bool -> f a
diff --git a/src/Ersatz/Bits.hs b/src/Ersatz/Bits.hs
--- a/src/Ersatz/Bits.hs
+++ b/src/Ersatz/Bits.hs
@@ -196,9 +196,24 @@
 
 -- | 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
+fullAdder a b c =
+  -- ( full_Adder_Sum a b c , full_Adder_Carry a b c )
+  let (s1,c1) = halfAdder a b ; (s2,c2) = halfAdder s1 c in (s2, c1||c2)
+  -- following does not work (formula generation does not stop), why?
+  {-
+  ( Run $ exists >>= \ x -> do
+      assert (     a ||     b ||     c || not x ) ; assert ( not a || not b || not c || x )
+      assert (     a || not b || not c || not x ) ; assert ( not a ||     b ||     c || x )
+      assert ( not a ||     b || not c || not x ) ; assert (     a || not b ||     c || x )
+      assert ( not a || not b ||     c || not x ) ; assert (     a ||     b || not c || x )
+      return x
+  , Run $ exists >>= \ x -> do
+      assert ( not b || not c || x ) ; assert ( b || c || not x )
+      assert ( not a || not c || x ) ; assert ( a || c || not x )
+      assert ( not a || not b || x ) ; assert ( a || b || not x )
+      return x
+  )
+  -}
 
 -- | Compute the sum and carry bit from adding two bits.
 halfAdder :: Bit -> Bit -> (Bit, Bit) -- ^ (sum, carry)
diff --git a/src/Ersatz/Counting.hs b/src/Ersatz/Counting.hs
new file mode 100644
--- /dev/null
+++ b/src/Ersatz/Counting.hs
@@ -0,0 +1,17 @@
+module Ersatz.Counting where
+
+import Ersatz.Bit
+import Ersatz.Bits
+import Ersatz.Codec
+import Ersatz.Equatable
+import Ersatz.Orderable
+
+exactly :: Int -> [ Bit ] -> Bit
+exactly k bs = encode (fromIntegral k) === sumBit bs
+
+atmost :: Int -> [ Bit ] -> Bit
+atmost k bs = encode (fromIntegral k) >=? sumBits bs
+
+atleast :: Int -> [ Bit ] -> Bit
+atleast k bs = encode (fromIntegral k) <=? sumBits bs
+
diff --git a/src/Ersatz/Internal/Formula.hs b/src/Ersatz/Internal/Formula.hs
--- a/src/Ersatz/Internal/Formula.hs
+++ b/src/Ersatz/Internal/Formula.hs
@@ -20,11 +20,12 @@
 module Ersatz.Internal.Formula
   (
   -- * Clauses
-    Clause(..), clauseLiterals
+    Clause(..), clauseLiterals, fromLiteral
   -- * Formulas
   , Formula(..)
-  , formulaEmpty, formulaLiteral
+  , formulaEmpty, formulaLiteral, fromClause
   , formulaNot, formulaAnd, formulaOr, formulaXor, formulaMux
+  , formulaFAS, formulaFAC
   ) where
 
 #if __GLASGOW_HASKELL__ < 710
@@ -36,11 +37,13 @@
 #if __GLASGOW_HASKELL__ < 710
 import Data.Monoid
 #endif
-import Data.Set (Set)
-import qualified Data.Set as Set
 import Data.Typeable
 import Ersatz.Internal.Literal
 
+import Data.Sequence (Seq)
+import qualified Data.Sequence as Seq
+import Data.Foldable (toList)
+
 ------------------------------------------------------------------------------
 -- Clauses
 ------------------------------------------------------------------------------
@@ -58,12 +61,15 @@
   mempty = Clause mempty
   mappend (Clause x) (Clause y) = Clause (mappend x y)
 
+fromLiteral :: Literal -> Clause
+fromLiteral l = Clause { clauseSet = IntSet.singleton $ literalId l }
+
 ------------------------------------------------------------------------------
 -- Formulas
 ------------------------------------------------------------------------------
 
 -- | A conjunction of clauses
-newtype Formula = Formula { formulaSet :: Set Clause }
+newtype Formula = Formula { formulaSet :: Seq Clause }
   deriving (Eq, Ord, Typeable)
 
 instance Monoid Formula where
@@ -73,7 +79,7 @@
 instance Show Formula where
   showsPrec p = showParen (p > 2) . foldr (.) id
               . List.intersperse (showString " & ") . map (showsPrec 3)
-              . Set.toList . formulaSet
+              . Data.Foldable.toList . formulaSet
 
 instance Show Clause where
   showsPrec p = showParen (p > 1) . foldr (.) id
@@ -83,13 +89,16 @@
 
 -- | A formula with no clauses
 formulaEmpty :: Formula
-formulaEmpty = Formula Set.empty
+formulaEmpty = mempty
 
 -- | Assert a literal
 formulaLiteral :: Literal -> Formula
-formulaLiteral (Literal l) =
-  Formula (Set.singleton (Clause (IntSet.singleton l)))
+formulaLiteral (Literal l) = fromClause (Clause (IntSet.singleton l))
 
+fromClause :: Clause -> Formula
+fromClause c = Formula { formulaSet = Seq.singleton c }
+
+
 -- | The boolean /not/ operation
 --
 -- Derivation of the Tseitin transformation:
@@ -102,6 +111,7 @@
 formulaNot :: Literal  -- ^ Output
            -> Literal  -- ^ Input
            -> Formula
+{-# inlineable formulaNot #-}
 formulaNot (Literal out) (Literal inp) = formulaFromList cls
   where
     cls = [ [-out, -inp], [out, inp] ]
@@ -119,6 +129,7 @@
 formulaAnd :: Literal    -- ^ Output
            -> [Literal]  -- ^ Inputs
            -> Formula
+{-# inlineable formulaAnd #-}
 formulaAnd (Literal out) inpLs = formulaFromList cls
   where
     cls = (out : map negate inps) : map (\inp -> [-out, inp]) inps
@@ -138,6 +149,7 @@
 formulaOr :: Literal    -- ^ Output
           -> [Literal]  -- ^ Inputs
           -> Formula
+{-# inlineable formulaOr #-}
 formulaOr (Literal out) inpLs = formulaFromList cls
   where
     cls = (-out : inps)
@@ -183,6 +195,7 @@
            -> Literal  -- ^ Input
            -> Literal  -- ^ Input
            -> Formula
+{-# inlineable formulaXor #-}
 formulaXor (Literal out) (Literal inpA) (Literal inpB) = formulaFromList cls
   where
     cls = [ [-out, -inpA, -inpB]
@@ -230,15 +243,38 @@
            -> Literal  -- ^ True branch
            -> Literal  -- ^ Predicate/selector
            -> Formula
-formulaMux (Literal out) (Literal inpF) (Literal inpT) (Literal inpP) =
+{-# inlineable formulaMux #-}
+-- | with redundant clauses, cf. discussion in
+--   Een and Sorensen, Translating Pseudo Boolean Constraints ..., p. 7
+-- http://minisat.se/Papers.html
+formulaMux (Literal x) (Literal f) (Literal t) (Literal s) =
   formulaFromList cls
   where
-    cls = [ [-out,  inpF,  inpT]
-          , [-out,  inpF,  inpP]
-          , [-out,  inpT, -inpP]
-          , [ out, -inpF,  inpP]
-          , [ out, -inpT, -inpP]
+    cls = [ [-s, -t,  x], [ s, -f,  x], {- red -} [-t, -f,  x]
+          , [-s,  t, -x], [ s,  f, -x], {- red -} [ t,  f, -x]
           ]
 
+formulaFAS :: Literal -> Literal -> Literal -> Literal -> Formula
+formulaFAS (Literal x) (Literal a) (Literal b) (Literal c) =
+  formulaFromList cls
+  where
+    cls =
+      [ [ a,  b,  c, -x], [-a, -b, -c, x]
+      , [ a, -b, -c, -x], [-a,  b,  c, x]
+      , [-a,  b, -c, -x], [ a, -b,  c, x]
+      , [-a, -b,  c, -x], [ a,  b, -c, x]
+      ]
+
+formulaFAC :: Literal -> Literal -> Literal -> Literal -> Formula
+formulaFAC (Literal x) (Literal a) (Literal b) (Literal c) =
+  formulaFromList cls
+  where
+    cls =
+      [ [ -b, -c, x], [b, c, -x]
+      , [ -a, -c, x], [a, c, -x]
+      , [ -a, -b, x], [a, b, -x]
+      ]
+
 formulaFromList :: [[Int]] -> Formula
-formulaFromList = Formula . Set.fromList . map (Clause . IntSet.fromList)
+{-# inline formulaFromList #-}
+formulaFromList = foldMap (  fromClause . Clause . IntSet.fromList )
diff --git a/src/Ersatz/Problem.hs b/src/Ersatz/Problem.hs
--- a/src/Ersatz/Problem.hs
+++ b/src/Ersatz/Problem.hs
@@ -67,13 +67,13 @@
 import qualified Data.IntSet as IntSet
 import qualified Data.List as List
 import Data.Monoid
-import Data.Set (Set)
-import qualified Data.Set as Set
 import Data.Typeable
 import Ersatz.Internal.Formula
 import Ersatz.Internal.Literal
 import Ersatz.Internal.StableName
 import System.IO.Unsafe
+import Data.Sequence (Seq)
+import qualified Data.Sequence as Seq
 
 ------------------------------------------------------------------------------
 -- SAT Problems
@@ -205,7 +205,7 @@
 class DIMACS t where
   dimacsComments :: t -> [ByteString]
   dimacsNumVariables :: t -> Int
-  dimacsClauses :: t -> Set IntSet
+  dimacsClauses :: t -> Seq IntSet
 
 -- | QDIMACS file format pretty printer
 --
@@ -216,7 +216,7 @@
   qdimacsComments :: t -> [ByteString]
   qdimacsNumVariables :: t -> Int
   qdimacsQuantified :: t -> [Quant]
-  qdimacsClauses :: t -> Set IntSet
+  qdimacsClauses :: t -> Seq IntSet
 
 -- | WDIMACS file format pretty printer
 --
@@ -227,7 +227,7 @@
   wdimacsComments :: t -> [ByteString]
   wdimacsNumVariables :: t -> Int
   wdimacsTopWeight :: t -> Int64  -- ^ Specified to be 1 ≤ n < 2^63
-  wdimacsClauses :: t -> Set (Int64, IntSet)
+  wdimacsClauses :: t -> Seq (Int64, IntSet)
 
 -- | Generate a 'Builder' out of a 'DIMACS' problem.
 dimacs :: DIMACS t => t -> Builder
@@ -236,7 +236,7 @@
     comments = foldMap bComment (dimacsComments t)
     problem = bLine [ string7 "p cnf"
                     , intDec (dimacsNumVariables t)
-                    , intDec (Set.size tClauses)
+                    , intDec (Seq.length tClauses)
                     ]
     clauses = foldMap bClause tClauses
 
@@ -249,7 +249,7 @@
     comments = foldMap bComment (qdimacsComments t)
     problem = bLine [ string7 "p cnf"
                     , intDec (qdimacsNumVariables t)
-                    , intDec (Set.size tClauses)
+                    , intDec (Seq.length tClauses)
                     ]
     quantified = foldMap go tQuantGroups
       where go ls = bLine0 (q (head ls) : map (intDec . getQuant) ls)
@@ -272,7 +272,7 @@
     comments = foldMap bComment (wdimacsComments t)
     problem = bLine [ string7 "p wcnf"
                     , intDec (wdimacsNumVariables t)
-                    , intDec (Set.size tClauses)
+                    , intDec (Seq.length tClauses)
                     , int64Dec (wdimacsTopWeight t)
                     ]
     clauses = foldMap (uncurry bWClause) tClauses
@@ -283,7 +283,7 @@
 bComment bs = bLine [ char7 'c', byteString bs ]
 
 bClause :: IntSet -> Builder
-bClause ls = bLine0 (map intDec (IntSet.toList ls))
+bClause = IntSet.foldl' ( \ e i -> intDec i <> char7 ' ' <> e ) ( char7 '0' <> char7 '\n' )
 
 bWClause :: Int64 -> IntSet -> Builder
 bWClause w ls = bLine0 (int64Dec w : map intDec (IntSet.toList ls))
@@ -332,5 +332,8 @@
         | otherwise = Exists i : quants is jjs
   qdimacsClauses = satClauses
 
-satClauses :: HasSAT s => s -> Set IntSet
-satClauses s = Set.map clauseSet (formulaSet (s^.formula))
+-- | the name is wrong (Does it return Clauses? No - it returns IntSets.)
+-- and it means extra work (traversing, and re-building, the full collection).
+-- Or is this fused away (because of Coercible)?
+satClauses :: HasSAT s => s -> Seq IntSet
+satClauses s = fmap clauseSet (formulaSet (s^.formula))
diff --git a/src/Ersatz/Relation.hs b/src/Ersatz/Relation.hs
new file mode 100644
--- /dev/null
+++ b/src/Ersatz/Relation.hs
@@ -0,0 +1,10 @@
+module Ersatz.Relation
+( module Ersatz.Relation.Data
+, module Ersatz.Relation.Op
+, module Ersatz.Relation.Prop
+) where
+
+import Ersatz.Relation.Data
+import Ersatz.Relation.Op
+import Ersatz.Relation.Prop
+
diff --git a/src/Ersatz/Relation/Data.hs b/src/Ersatz/Relation/Data.hs
new file mode 100644
--- /dev/null
+++ b/src/Ersatz/Relation/Data.hs
@@ -0,0 +1,89 @@
+{-# language TypeFamilies #-}
+
+module Ersatz.Relation.Data ( Relation
+, relation, symmetric_relation
+, build
+, identity
+, bounds, (!), indices, assocs, elems
+, table
+)  where
+
+import Ersatz.Bit
+import Ersatz.Codec
+import Ersatz.Variable (exists)
+import Ersatz.Problem (HasSAT)
+
+import qualified Data.Array as A
+import Data.Array ( Array, Ix )
+import Control.Monad.State
+
+newtype Relation a b = Relation (A.Array (a, b) Bit)
+
+instance (Ix a, Ix b) => Codec (Relation a b) where
+  type Decoded (Relation a b) = A.Array (a, b) Bool
+  decode s (Relation a) = decode s a
+  encode a = Relation $ encode a
+
+relation :: ( Ix a, Ix b, MonadState s m, HasSAT s )
+         => ((a,b),(a,b)) -> m ( Relation a b )
+relation bnd = do
+    pairs <- sequence $ do
+        p <- A.range bnd
+        return $ do
+            x <- exists
+            return ( p, x )
+    return $ build bnd pairs
+
+symmetric_relation ::
+  (HasSAT s, MonadState s m, Ix b) =>
+  ((b, b), (b, b)) -> m (Relation b b)
+symmetric_relation bnd = do
+    pairs <- sequence $ do
+        (p,q) <- A.range bnd
+        guard $ p <= q
+        return $ do
+            x <- exists
+            return $ [ ((p,q), x ) ]
+                   ++ [ ((q,p), x) | p /= q ]
+    return $ build bnd $ concat pairs
+
+identity :: ( Ix a )
+         => ((a,a),(a,a)) ->  Relation a a
+identity bnd = build bnd $ flip map (A.range bnd) $ \ (i,j) ->
+        ((i,j), if i == j then true else false )
+
+build :: ( Ix a, Ix b )
+      => ((a,b),(a,b))
+      -> [ ((a,b), Bit ) ]
+      -> Relation a b
+build bnd pairs = Relation $ A.array bnd pairs
+
+
+bounds :: (Ix a, Ix b) => Relation a b -> ((a,b),(a,b))
+bounds ( Relation r ) = A.bounds r
+
+indices :: (Ix a, Ix b) => Relation a b -> [(a, b)]
+indices ( Relation r ) = A.indices r
+
+assocs :: (Ix a, Ix b) => Relation a b -> [((a, b), Bit)]
+assocs ( Relation r ) = A.assocs r
+
+elems :: (Ix a, Ix b) => Relation a b -> [Bit]
+elems ( Relation r ) = A.elems r
+
+(!) :: (Ix a, Ix b) => Relation a b -> (a, b) -> Bit
+Relation r ! p = r A.! p
+
+
+table :: (Enum a, Ix a, Enum b, Ix b)
+      => Array (a,b) Bool -> String
+table r = unlines $ do
+    let ((a,b),(c,d)) = A.bounds r
+    x <- [ a .. c ]
+    return $ unwords $ do
+        y <- [ b .. d ]
+        return $ if r A.! (x,y) then "*" else "."
+
+
+
+
diff --git a/src/Ersatz/Relation/Op.hs b/src/Ersatz/Relation/Op.hs
new file mode 100644
--- /dev/null
+++ b/src/Ersatz/Relation/Op.hs
@@ -0,0 +1,68 @@
+{-# language FlexibleInstances, MultiParamTypeClasses #-}
+
+module Ersatz.Relation.Op
+
+( mirror
+, union
+, complement
+, product, power
+, intersection
+)
+
+where
+
+import Ersatz.Relation.Data
+
+import Prelude hiding ( and, or, not, product )
+import Ersatz.Bit (and, or, not)
+
+import Data.Ix
+
+mirror :: ( Ix a , Ix b ) => Relation a b -> Relation b a
+mirror r =
+    let ((a,b),(c,d)) = bounds r
+    in  build ((b,a),(d,c)) $ do (x,y) <- indices r ; return ((y,x), r!(x,y))
+
+complement :: ( Ix a , Ix b ) => Relation a b -> Relation a b
+complement r =
+    build (bounds r) $ do i <- indices r ; return ( i, not $ r!i )
+
+
+union :: ( Ix a , Ix b )
+        => Relation a b -> Relation a b ->  Relation a b
+union r s =  build ( bounds r ) $ do
+    i <- indices r
+    return (i, or [ r!i, s!i ] )
+
+product :: ( Ix a , Ix b, Ix c )
+        => Relation a b -> Relation b c ->  Relation a c
+product a b =
+    let ((ao,al),(au,ar)) = bounds a
+        ((_ ,bl),(_ ,br)) = bounds b
+        bnd = ((ao,bl),(au,br))
+    in  build bnd $ do
+          i @ (x,z) <- range bnd
+          return (i, or $ do
+                y <- range ( al, ar )
+                return $ and [ a!(x,y), b!(y,z) ]
+                )
+
+power  :: ( Ix a  )
+        => Int -> Relation a a -> Relation a a
+power 0 r = identity ( bounds r )
+power 1 r = r
+power e r =
+    let (d,m) = divMod e 2
+        s = power d r
+        s2 = product s s
+    in  case m of
+        0 -> s2
+        _ -> product s2 r
+
+intersection :: ( Ix a , Ix b)
+      => Relation a b -> Relation a b
+      -> Relation a b
+intersection r s = build ( bounds r ) $ do
+        i <- indices r
+        return (i, and [ r!i, s!i ] )
+
diff --git a/src/Ersatz/Relation/Prop.hs b/src/Ersatz/Relation/Prop.hs
new file mode 100644
--- /dev/null
+++ b/src/Ersatz/Relation/Prop.hs
@@ -0,0 +1,92 @@
+
+module Ersatz.Relation.Prop
+
+( implies
+, symmetric
+, transitive
+, irreflexive
+, reflexive
+, regular
+, regular_in_degree
+, regular_out_degree
+, max_in_degree
+, min_in_degree
+, max_out_degree
+, min_out_degree
+, empty
+, complete
+, disjoint
+, equals
+)
+
+where
+
+import Prelude hiding ( and, or, not, product )
+import Ersatz.Bit
+import Ersatz.Relation.Data
+import Ersatz.Relation.Op
+import Ersatz.Counting
+
+import Data.Ix
+
+implies :: ( Ix a, Ix b )
+        => Relation a b -> Relation a b -> Bit
+implies r s = and $ do
+    i <- indices r
+    return $ or [ not $ r ! i, s ! i ]
+
+empty ::  ( Ix a, Ix b )
+        => Relation a b -> Bit
+empty r = and $ do
+    i <- indices r
+    return $ not $ r ! i
+
+complete :: (Ix a, Ix b) => Relation a b -> Bit
+complete r = empty $ complement r
+
+disjoint :: (Ix a, Ix b) => Relation a b -> Relation a b -> Bit
+disjoint r s = empty $ intersection r s
+
+equals :: (Ix a, Ix b) => Relation a b -> Relation a b -> Bit
+equals r s = and [implies r s, implies s r]
+
+symmetric :: ( Ix a) => Relation a a -> Bit
+symmetric r = implies r ( mirror r )
+
+irreflexive :: ( Ix a ) => Relation a a -> Bit
+irreflexive r = and $ do
+    let ((a,_),(c,_)) = bounds r
+    x <- range (a, c)
+    return $ not $ r ! (x,x)
+
+reflexive :: ( Ix a ) => Relation a a -> Bit
+reflexive r = and $ do
+    let ((a,_),(c,_)) = bounds r
+    x <- range (a,c)
+    return $ r ! (x,x)
+
+regular, regular_in_degree, regular_out_degree, max_in_degree, min_in_degree, max_out_degree, min_out_degree :: ( Ix a ) => Int -> Relation a a -> Bit
+
+regular deg r = and [ regular_in_degree deg r, regular_out_degree deg r ]
+
+regular_out_degree = out_degree_helper exactly
+max_out_degree = out_degree_helper atmost
+min_out_degree = out_degree_helper atleast
+regular_in_degree deg r = regular_out_degree deg $ mirror r
+max_in_degree deg r = max_out_degree deg $ mirror r
+min_in_degree deg r = min_out_degree deg $ mirror r
+
+out_degree_helper ::
+  (Boolean b, Ix b1, Ix a) =>
+  (t -> [Bit] -> b) -> t -> Relation a b1 -> b
+out_degree_helper f deg r = and $ do
+    let ((a,b),(c,d)) = bounds r
+    x <- range ( a , c )
+    return $ f deg $ do
+        y <- range (b,d)
+        return $ r !(x,y)
+
+transitive :: ( Ix a )
+           => Relation a a -> Bit
+transitive r = implies (product r r) r
+
diff --git a/src/Ersatz/Solution.hs b/src/Ersatz/Solution.hs
--- a/src/Ersatz/Solution.hs
+++ b/src/Ersatz/Solution.hs
@@ -23,7 +23,7 @@
 import Control.Lens
 import qualified Data.HashMap.Lazy as HashMap
 import Data.IntMap (IntMap)
-import qualified Data.IntMap as IntMap
+import qualified Data.IntMap.Strict as IntMap
 import Data.Ix
 import Data.Typeable
 import Ersatz.Internal.Literal
diff --git a/src/Ersatz/Solver.hs b/src/Ersatz/Solver.hs
--- a/src/Ersatz/Solver.hs
+++ b/src/Ersatz/Solver.hs
@@ -11,11 +11,9 @@
 module Ersatz.Solver
   ( module Ersatz.Solver.DepQBF
   , module Ersatz.Solver.Minisat
-  , module Ersatz.Solver.Z3
   , solveWith
   ) where
 
-import Control.Applicative
 import Control.Monad
 import Control.Monad.State
 import Data.Default
@@ -24,7 +22,6 @@
 import Ersatz.Solution
 import Ersatz.Solver.DepQBF
 import Ersatz.Solver.Minisat
-import Ersatz.Solver.Z3
 
 #if __GLASGOW_HASKELL__ < 710
 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))
diff --git a/src/Ersatz/Solver/Minisat.hs b/src/Ersatz/Solver/Minisat.hs
--- a/src/Ersatz/Solver/Minisat.hs
+++ b/src/Ersatz/Solver/Minisat.hs
@@ -7,6 +7,9 @@
 -- Portability: non-portable
 --
 --------------------------------------------------------------------
+
+{-# language OverloadedStrings #-}
+
 module Ersatz.Solver.Minisat
   ( minisat
   , cryptominisat
@@ -14,19 +17,19 @@
   ) where
 
 import Data.ByteString.Builder
-import Control.Applicative
 import Control.Exception (IOException, handle)
-import Control.Monad
 import Control.Monad.IO.Class
 import Data.IntMap (IntMap)
-import Ersatz.Internal.Parser
 import Ersatz.Problem
 import Ersatz.Solution
 import Ersatz.Solver.Common
-import qualified Data.IntMap as IntMap
+import qualified Data.IntMap.Strict as IntMap
 import System.IO
 import System.Process (readProcessWithExitCode)
 
+import qualified Data.ByteString.Char8 as B
+import Data.List ( foldl' )
+
 -- | 'Solver' for 'SAT' problems that tries to invoke the @minisat@ executable from the @PATH@
 minisat :: MonadIO m => Solver SAT m
 minisat = minisatPath "minisat"
@@ -52,32 +55,16 @@
     return (resultOf exit, sol)
 
 parseSolutionFile :: FilePath -> IO (IntMap Bool)
-parseSolutionFile path = handle handler (parseSolution <$> readFile path)
+parseSolutionFile path = handle handler (parseSolution <$> B.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)
+parseSolution :: B.ByteString -> IntMap Bool
+parseSolution s =
+  case B.words s of
+    x : ys | x == "SAT" ->
+          foldl' ( \ m y -> let Just (v,_) = B.readInt y
+                            in  if 0 == v then m else IntMap.insert (abs v) (v>0) m
+                 ) IntMap.empty ys
+    _ -> IntMap.empty -- WRONG (should be Nothing)
diff --git a/src/Ersatz/Solver/Z3.hs b/src/Ersatz/Solver/Z3.hs
deleted file mode 100644
--- a/src/Ersatz/Solver/Z3.hs
+++ /dev/null
@@ -1,68 +0,0 @@
---------------------------------------------------------------------
--- |
--- Copyright :  © Edward Kmett 2010-2014, Johan Kiviniemi 2013
--- License   :  BSD3
--- Maintainer:  Edward Kmett <ekmett@gmail.com>
--- Stability :  experimental
--- Portability: non-portable
---
---------------------------------------------------------------------
-module Ersatz.Solver.Z3
-  ( z3
-  , z3Path
-  ) where
-
-import Data.ByteString.Builder
-import Control.Applicative
-import Control.Monad.IO.Class
-import Data.IntMap (IntMap)
-import Ersatz.Internal.Parser
-import Ersatz.Problem
-import Ersatz.Solution
-import Ersatz.Solver.Common
-import qualified Data.IntMap as IntMap
-import System.IO
-import System.Process (readProcessWithExitCode)
-
--- | 'Solver' for 'SAT' problems that tries to invoke the @z3@ executable from the @PATH@
-z3 :: MonadIO m => Solver SAT m
-z3 = z3Path "z3"
-
--- | 'Solver' for 'SAT' problems that tries to invoke a program that takes @z3@ compatible arguments.
---
--- The 'FilePath' refers to the path to the executable.
-z3Path :: MonadIO m => FilePath -> Solver SAT m
-z3Path path problem = liftIO $
-  withTempFiles ".cnf" "" $ \problemPath _ -> do
-    withFile problemPath WriteMode $ \fh ->
-      hPutBuilder fh (dimacs problem)
-
-    (_exit, out, _err) <-
-      readProcessWithExitCode path ["-dimacs", problemPath] []
-
-    let result = case lines out of
-                    "sat":_   -> Satisfied
-                    "unsat":_ -> Unsatisfied
-                    _         -> Unsolved
-
-    return (result, parseSolution out)
-
-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  = many value <* token '\n' <* eof
-
-value :: Parser Char (Int, Bool)
-value = toPair <$> integer <* token ' '
-  where
-    toPair n | n >= 0    = ( n, True)
-             | otherwise = (-n, False)
diff --git a/tests/Moore.hs b/tests/Moore.hs
new file mode 100644
--- /dev/null
+++ b/tests/Moore.hs
@@ -0,0 +1,78 @@
+-- | graphs n nodes of degree <= d and diameter <= k 
+-- see http://combinatoricswiki.org/wiki/The_Degree_Diameter_Problem_for_General_Graphs
+
+-- usage: ./Moore d k n [s]
+-- d : degree
+-- k : diameter
+-- n : nodes,
+-- s : modulus for symmetry (see periodic_relation below)
+-- s smaller => faster (more symmetries) but may lose solutions
+
+-- test cases:  3 2 10 2  -- petersen graph
+--              5 2 24    
+
+
+{-# language FlexibleContexts #-}
+
+import Prelude hiding ( not, or, and )
+import qualified Prelude
+
+import Ersatz
+import Ersatz.Bit
+import qualified Ersatz.Relation as R
+
+import qualified Data.Array as A
+import System.Environment (getArgs)
+import Control.Monad ( void, when, forM )
+import Control.Monad.State
+
+main :: IO ( )
+main = do
+  argv <- getArgs
+  case argv of
+    [ d, k, n, s ] ->
+      void $ mainf ( read d ) (read k) (read n) (read s)
+    [ d, k, n    ] ->
+      void $ mainf ( read d ) (read k) (read n) (read n)
+    [] -> void $ mainf 3 2 10 5 -- petersen
+
+mainf d k n s = do
+  putStrLn $ unwords [ "degree <=", show d, "diameter <=", show k, "nodes ==", show n, "symmetry ==", show s ]
+  (s, mg) <- solveWith minisat $ moore d k n s
+  case (s, mg) of
+     (Satisfied, Just g) -> do printA g ; return True
+     _ -> do return False
+
+moore :: (MonadState s m, HasSAT s )
+      => Int -> Int -> Int -> Int
+      -> m (R.Relation Int Int)
+moore d k n s = do
+  -- g <- R.symmetric_relation ((0,0),(n-1,n-1))
+  g <- periodic_relation s ((0,0),(n-1,n-1))
+  assert $ R.symmetric g
+  assert $ R.reflexive g 
+  assert $ R.max_in_degree (d+1) g 
+  assert $ R.max_out_degree (d+1) g 
+  let p = R.power k g
+  assert $ R.complete p 
+  return g
+
+periodic_relation s bnd = do
+  r <- R.relation bnd
+  let normal (x,y) =
+        if (x >= s Prelude.&& y >= s)
+        then normal (x-s,y-s)  else (x,y)
+  return $ R.build bnd $ do
+    i <- A.range bnd
+    return (i, r R.! normal i)
+  
+-- | FIXME: this needs to go into a library
+printA :: A.Array (Int,Int) Bool -> IO ()
+printA a = putStrLn $ unlines $ do
+         let ((u,l),(o,r)) = A.bounds a
+         x <- [u .. o]
+         return $ unwords $ do 
+             y <- [ l ..r ]
+             return $ case a A.! (x,y) of
+                  True -> "* " ; False -> ". "
+
diff --git a/tests/Speed.hs b/tests/Speed.hs
new file mode 100644
--- /dev/null
+++ b/tests/Speed.hs
@@ -0,0 +1,23 @@
+import Ersatz
+import Ersatz.Bit
+import Ersatz.Variable (exists)
+
+import System.Environment (getArgs)
+import Control.Monad ( forM_, replicateM )
+
+main :: IO ( )
+main = do
+  argv <- getArgs
+  case argv of
+    [ n ] -> mainf ( read n)
+    [] -> mainf 50000
+
+mainf n = do
+  putStrLn $ unwords [ "n",  show n ]
+  (s, mgs) <- solveWith minisat $ do
+      gs <- replicateM n exists
+      forM_ (zip gs $ tail gs) $ \ (x,y) -> assert ( x /== y )
+      return (gs :: [Bit])
+  case (s, mgs) of
+     (Satisfied, Just gs) -> do print $ length $ filter id gs
+     _ -> do return ()
diff --git a/tests/Z001.hs b/tests/Z001.hs
new file mode 100644
--- /dev/null
+++ b/tests/Z001.hs
@@ -0,0 +1,118 @@
+{-# language KindSignatures, DataKinds, FlexibleContexts #-}
+{-# language GeneralizedNewtypeDeriving #-}
+{-# language TypeFamilies, ScopedTypeVariables #-}
+
+{-# language NoMonomorphismRestriction #-}
+
+import Prelude hiding ( not, and, or, (&&), (||) )
+
+import Ersatz
+
+import GHC.TypeLits
+import Data.Proxy
+import Data.List ( transpose )
+import Control.Monad ( replicateM, forM_ )
+import Control.Monad.State
+
+main = do
+  (Satisfied, Just ms) <- solveWith minisat $ do
+    [ Restricted a, Restricted b ]
+        :: [ Restricted 5 (NBV 3) ] <- replicateM 2 unknown
+    -- assert $ gt (a^2 * b^2) (b^3 * a^3)
+    let a2 = a^2 ; b2 = b^2
+    assert $ gt (a2 * b2) (b2 * b * a * a2)
+    return [a,b]
+  forM_ ms print
+
+unknown_monotone = do
+   m <- unknown ; assert $ monotone m ; return m
+
+newtype Restricted d a = Restricted (Matrix d a)
+
+instance (KnownNat dim, Unknown a, Codec a, Num (Decoded a))
+  => Unknown (Restricted dim a) where
+  unknown = do
+    let d = fromIntegral $ natVal (Proxy :: Proxy dim)
+        row f = ( encode f : ) <$> replicateM (d-1) unknown
+    m <- (:) <$> row 1 <*> replicateM (d-2) (row 0)
+    return $ Restricted $ Matrix
+       $ m ++ encode [ replicate (d-1) 0 ++ [1] ] 
+
+class Unknown a where
+  unknown :: (MonadState s m, HasSAT s) => m a
+
+-- | square matrices
+newtype Matrix (dim::Nat)  a = Matrix [[a]]
+  deriving ( Show, Equatable, Orderable )
+
+instance Codec a => Codec (Matrix dim a) where
+  type Decoded (Matrix dim a) = Matrix dim (Decoded a)
+  decode s (Matrix xss) = Matrix <$> decode s xss
+    
+instance (KnownNat dim, Unknown a) => Unknown (Matrix dim a) where
+  unknown = do
+    let d = fromIntegral $ natVal (Proxy :: Proxy dim)
+    Matrix <$> replicateM d (replicateM d unknown)
+    
+instance Num a => Num (Matrix dim a) where
+  Matrix xss + Matrix yss
+    = Matrix $ zipWith (zipWith (+)) xss yss
+  Matrix xss * Matrix yss
+    = Matrix $ for xss $ \ row ->
+        for (transpose yss) $ \ col ->
+          sum $ zipWith (*) row col
+
+for = flip map
+
+topleft (Matrix xss) = head (head xss)
+botright (Matrix xss) = last (last xss)
+topright (Matrix xss) = last (head xss)
+
+monotone m = positive (topleft m) && positive (botright m)
+
+ge :: Orderable a => Matrix dim a -> Matrix dim a -> Bit
+ge (Matrix xss) (Matrix yss) =
+  and $ zipWith (>=?) (concat xss) (concat yss)
+
+gt :: Orderable a => Matrix dim a -> Matrix dim a -> Bit
+gt a b = ge a b && topright a >? topright b
+
+-- | NBV = Non-overflowing Bitvector
+-- Bitvectors of fixed length, with non-overflowing arithmetics
+-- (if overflow occurs, constraint is unsatisfiable)
+
+newtype NBV ( n :: Nat ) = NBV Bits 
+  deriving ( Show, Equatable, Orderable, HasBits )
+
+instance KnownNat w => Unknown (NBV w) where
+  unknown = do
+    let n = fromIntegral $ natVal (Proxy :: Proxy w)
+    NBV <$> Bits <$> replicateM n exists
+
+positive (NBV (Bits bs)) = or bs
+
+nbv n (Bits bs) = 
+  let (p : re, post) = splitAt n bs
+  in  NBV $ Bits $ Run ( assert (not $ or post) *> return p )
+                 : re 
+
+instance KnownNat n => Num (NBV n) where
+  fromInteger = encode
+  NBV a + NBV b =
+    nbv (fromIntegral (natVal (Proxy :: Proxy n))) $ a + b
+  NBV a * NBV b =
+    nbv (fromIntegral (natVal (Proxy :: Proxy n))) $ a * b
+
+instance KnownNat n => Codec (NBV n) where
+  type Decoded (NBV n) = Integer
+  decode s (NBV bs) = decode s bs
+  encode i =
+    let n = fromIntegral $ natVal (Proxy :: Proxy n)
+        Bits bs = encode i
+        (pre, post) = splitAt n bs
+    in  if null post
+        then NBV (Bits $ take n $ pre ++ repeat false)
+        else error $ unwords
+             [ "cannot encode", show i
+             , "with given bit width", show n
+             ]
diff --git a/tests/doctests.hs b/tests/doctests.hs
new file mode 100644
--- /dev/null
+++ b/tests/doctests.hs
@@ -0,0 +1,25 @@
+-----------------------------------------------------------------------------
+-- |
+-- Module      :  Main (doctests)
+-- Copyright   :  (C) 2012-14 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 (flags, pkgs, module_sources)
+import Data.Foldable (traverse_)
+import Test.DocTest
+
+main :: IO ()
+main = do
+    traverse_ putStrLn args
+    doctest args
+  where
+    args = flags ++ pkgs ++ module_sources
diff --git a/tests/doctests.hsc b/tests/doctests.hsc
deleted file mode 100644
--- a/tests/doctests.hsc
+++ /dev/null
@@ -1,74 +0,0 @@
-{-# LANGUAGE CPP #-}
-{-# LANGUAGE ForeignFunctionInterface #-}
------------------------------------------------------------------------------
--- |
--- Module      :  Main (doctests)
--- Copyright   :  © 2012-2013 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
-
-##ifdef mingw32_HOST_ARCH
-##ifdef 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(x86_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
-##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