ersatz 0.3.1 → 0.4

raw patch · 26 files changed

+826/−318 lines, 26 filesdep +attoparsecdep ~arraydep ~basedep ~mtlsetup-changednew-uploaderPVP ok

version bump matches the API change (PVP)

Dependencies added: attoparsec

Dependency ranges changed: array, base, mtl, process

API changes (from Hackage documentation)

Files

• .gitignore +4/−0
• .travis.yml +71/−20
• CHANGELOG.md +11/−0
• README.md +2/−2
• Setup.lhs +23/−44
• Warning.hs +5/−0
• ersatz.cabal +40/−8
• examples/regexp-grid/Main.hs +1/−1
• src/Ersatz/Bit.hs +48/−38
• src/Ersatz/Bits.hs +18/−3
• src/Ersatz/Counting.hs +17/−0
• src/Ersatz/Internal/Formula.hs +52/−16
• src/Ersatz/Problem.hs +14/−11
• src/Ersatz/Relation.hs +10/−0
• src/Ersatz/Relation/Data.hs +89/−0
• src/Ersatz/Relation/Op.hs +68/−0
• src/Ersatz/Relation/Prop.hs +92/−0
• src/Ersatz/Solution.hs +1/−1
• src/Ersatz/Solver.hs +0/−3
• src/Ersatz/Solver/Minisat.hs +16/−29
• src/Ersatz/Solver/Z3.hs +0/−68
• tests/Moore.hs +78/−0
• tests/Speed.hs +23/−0
• tests/Z001.hs +118/−0
• tests/doctests.hs +25/−0
• tests/doctests.hsc +0/−74

@@ -8,6 +8,10 @@ .*.swp .*.swo *.o+*.p_o *.hi+*.p_hi *~ *#+*.prof+*.hp

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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