packages feed

ersatz 0.4.7 → 0.4.8

raw patch · 15 files changed

+121/−90 lines, 15 filesdep ~mtlPVP: major bump suggested

API removals or changes: PVP suggests a major version bump

Dependency ranges changed: mtl

API changes (from Hackage documentation)

+ Ersatz.Problem: type MonadQSAT s m = (HasQSAT s, MonadState s m)
+ Ersatz.Problem: type MonadSAT s m = (HasSAT s, MonadState s m)
- Ersatz.Bit: Run :: (forall m s. (MonadState s m, HasSAT s) => m Bit) -> Bit
+ Ersatz.Bit: Run :: (forall m s. MonadSAT s m => m Bit) -> Bit
- Ersatz.Bit: assert :: (MonadState s m, HasSAT s) => Bit -> m ()
+ Ersatz.Bit: assert :: MonadSAT s m => Bit -> m ()
- Ersatz.Problem: assertFormula :: (MonadState s m, HasSAT s) => Formula -> m ()
+ Ersatz.Problem: assertFormula :: MonadSAT s m => Formula -> m ()
- Ersatz.Problem: generateLiteral :: (MonadState s m, HasSAT s) => a -> (Literal -> m ()) -> m Literal
+ Ersatz.Problem: generateLiteral :: MonadSAT s m => a -> (Literal -> m ()) -> m Literal
- Ersatz.Problem: literalExists :: (MonadState s m, HasSAT s) => m Literal
+ Ersatz.Problem: literalExists :: MonadSAT s m => m Literal
- Ersatz.Problem: literalForall :: (MonadState s m, HasQSAT s) => m Literal
+ Ersatz.Problem: literalForall :: MonadQSAT s m => m Literal
- Ersatz.Relation: relation :: (Ix a, Ix b, MonadState s m, HasSAT s) => ((a, b), (a, b)) -> m (Relation a b)
+ Ersatz.Relation: relation :: (Ix a, Ix b, MonadSAT s m) => ((a, b), (a, b)) -> m (Relation a b)
- Ersatz.Relation: symmetric_relation :: (HasSAT s, MonadState s m, Ix b) => ((b, b), (b, b)) -> m (Relation b b)
+ Ersatz.Relation: symmetric_relation :: (MonadSAT s m, Ix b) => ((b, b), (b, b)) -> m (Relation b b)
- Ersatz.Variable: exists :: (Variable a, MonadState s m, HasSAT s) => m a
+ Ersatz.Variable: exists :: (Variable a, MonadSAT s m) => m a
- Ersatz.Variable: forall :: (Variable a, MonadState s m, HasQSAT s) => m a
+ Ersatz.Variable: forall :: (Variable a, MonadQSAT s m) => m a
- Ersatz.Variable: genericLiterally :: (HasSAT s, MonadState s m, Generic t, GVariable (Rep t)) => m Literal -> m t
+ Ersatz.Variable: genericLiterally :: (MonadSAT s m, Generic t, GVariable (Rep t)) => m Literal -> m t
- Ersatz.Variable: gliterally :: (GVariable f, MonadState s m, HasSAT s) => m Literal -> m (f a)
+ Ersatz.Variable: gliterally :: (GVariable f, MonadSAT s m) => m Literal -> m (f a)
- Ersatz.Variable: literally :: (Variable t, HasSAT s, MonadState s m, Generic t, GVariable (Rep t)) => m Literal -> m t
+ Ersatz.Variable: literally :: (Variable t, MonadSAT s m, Generic t, GVariable (Rep t)) => m Literal -> m t

Files

.hlint.yaml view
@@ -5,3 +5,5 @@  - ignore:     name: Use lambda-case++- ignore: {name: Hoist not, within: [Ersatz.Bit]} # This is how we define `any`, ya dingus
.travis.yml view
@@ -4,7 +4,7 @@ # # For more information, see https://github.com/haskell-CI/haskell-ci #-# version: 0.3.20190521+# version: 0.7.20191105 # language: c dist: xenial@@ -22,6 +22,7 @@   directories:     - $HOME/.cabal/packages     - $HOME/.cabal/store+    - $HOME/.hlint before_cache:   - rm -fv $CABALHOME/packages/hackage.haskell.org/build-reports.log   # remove files that are regenerated by 'cabal update'@@ -35,32 +36,31 @@   include:     - compiler: ghc-8.8.1       addons: {"apt":{"sources":["hvr-ghc"],"packages":["ghc-8.8.1","cabal-install-3.0","minisat"]}}-      env: GHCHEAD=true     - compiler: ghc-8.6.5-      addons: {"apt":{"sources":["hvr-ghc"],"packages":["ghc-8.6.5","cabal-install-2.4","minisat"]}}+      addons: {"apt":{"sources":["hvr-ghc"],"packages":["ghc-8.6.5","cabal-install-3.0","minisat"]}}     - compiler: ghc-8.4.4-      addons: {"apt":{"sources":["hvr-ghc"],"packages":["ghc-8.4.4","cabal-install-2.4","minisat"]}}+      addons: {"apt":{"sources":["hvr-ghc"],"packages":["ghc-8.4.4","cabal-install-3.0","minisat"]}}     - compiler: ghc-8.2.2-      addons: {"apt":{"sources":["hvr-ghc"],"packages":["ghc-8.2.2","cabal-install-2.4","minisat"]}}+      addons: {"apt":{"sources":["hvr-ghc"],"packages":["ghc-8.2.2","cabal-install-3.0","minisat"]}}     - compiler: ghc-8.0.2-      addons: {"apt":{"sources":["hvr-ghc"],"packages":["ghc-8.0.2","cabal-install-2.4","minisat"]}}+      addons: {"apt":{"sources":["hvr-ghc"],"packages":["ghc-8.0.2","cabal-install-3.0","minisat"]}}     - compiler: ghc-7.10.3-      addons: {"apt":{"sources":["hvr-ghc"],"packages":["ghc-7.10.3","cabal-install-2.4","minisat"]}}+      addons: {"apt":{"sources":["hvr-ghc"],"packages":["ghc-7.10.3","cabal-install-3.0","minisat"]}}     - compiler: ghc-head       addons: {"apt":{"sources":["hvr-ghc"],"packages":["ghc-head","cabal-install-head","minisat"]}}-      env: GHCHEAD=true   allow_failures:     - compiler: ghc-head-    - compiler: ghc-8.8.1 before_install:   - HC=$(echo "/opt/$CC/bin/ghc" | sed 's/-/\//')+  - WITHCOMPILER="-w $HC"+  - HADDOCK=$(echo "/opt/$CC/bin/haddock" | sed 's/-/\//')   - HCPKG="$HC-pkg"   - unset CC   - CABAL=/opt/ghc/bin/cabal   - CABALHOME=$HOME/.cabal   - export PATH="$CABALHOME/bin:$PATH"   - TOP=$(pwd)-  - HCNUMVER=$(( $(${HC} --numeric-version|sed -E 's/([0-9]+)\.([0-9]+)\.([0-9]+).*/\1 * 10000 + \2 * 100 + \3/') ))+  - "HCNUMVER=$(${HC} --numeric-version|perl -ne '/^(\\d+)\\.(\\d+)\\.(\\d+)(\\.(\\d+))?$/; print(10000 * $1 + 100 * $2 + ($3 == 0 ? $5 != 1 : $3))')"   - echo $HCNUMVER   - CABAL="$CABAL -vnormal+nowrap+markoutput"   - set -o pipefail@@ -87,56 +87,70 @@   - echo "$(${HC} --version) [$(${HC} --print-project-git-commit-id 2> /dev/null || echo '?')]"   - TEST=--enable-tests   - BENCH=--enable-benchmarks-  - GHCHEAD=${GHCHEAD-false}+  - HEADHACKAGE=false+  - if [ $HCNUMVER -gt 80801 ] ; then HEADHACKAGE=true ; fi   - rm -f $CABALHOME/config   - |-    echo "verbose: normal +nowrap +markoutput"          >> $CABALHOME/config-    echo "remote-build-reporting: anonymous"            >> $CABALHOME/config-    echo "remote-repo-cache: $CABALHOME/packages"       >> $CABALHOME/config-    echo "logs-dir:          $CABALHOME/logs"           >> $CABALHOME/config-    echo "world-file:        $CABALHOME/world"          >> $CABALHOME/config-    echo "extra-prog-path:   $CABALHOME/bin"            >> $CABALHOME/config-    echo "symlink-bindir:    $CABALHOME/bin"            >> $CABALHOME/config-    echo "installdir:        $CABALHOME/bin"            >> $CABALHOME/config-    echo "build-summary:     $CABALHOME/logs/build.log" >> $CABALHOME/config-    echo "store-dir:         $CABALHOME/store"          >> $CABALHOME/config-    echo "install-dirs user"                            >> $CABALHOME/config-    echo "  prefix: $CABALHOME"                         >> $CABALHOME/config-    echo "repository hackage.haskell.org"               >> $CABALHOME/config-    echo "  url: http://hackage.haskell.org/"           >> $CABALHOME/config+    echo "verbose: normal +nowrap +markoutput"                                  >> $CABALHOME/config+    echo "remote-build-reporting: anonymous"                                    >> $CABALHOME/config+    echo "write-ghc-environment-files: always"                                  >> $CABALHOME/config+    echo "remote-repo-cache: $CABALHOME/packages"                               >> $CABALHOME/config+    echo "logs-dir:          $CABALHOME/logs"                                   >> $CABALHOME/config+    echo "world-file:        $CABALHOME/world"                                  >> $CABALHOME/config+    echo "extra-prog-path:   $CABALHOME/bin"                                    >> $CABALHOME/config+    echo "symlink-bindir:    $CABALHOME/bin"                                    >> $CABALHOME/config+    echo "installdir:        $CABALHOME/bin"                                    >> $CABALHOME/config+    echo "build-summary:     $CABALHOME/logs/build.log"                         >> $CABALHOME/config+    echo "store-dir:         $CABALHOME/store"                                  >> $CABALHOME/config+    echo "install-dirs user"                                                    >> $CABALHOME/config+    echo "  prefix: $CABALHOME"                                                 >> $CABALHOME/config+    echo "repository hackage.haskell.org"                                       >> $CABALHOME/config+    echo "  url: http://hackage.haskell.org/"                                   >> $CABALHOME/config+    echo "  secure: True"                                                       >> $CABALHOME/config+    echo "  key-threshold: 3"                                                   >> $CABALHOME/config+    echo "  root-keys:"                                                         >> $CABALHOME/config+    echo "    fe331502606802feac15e514d9b9ea83fee8b6ffef71335479a2e68d84adc6b0" >> $CABALHOME/config+    echo "    1ea9ba32c526d1cc91ab5e5bd364ec5e9e8cb67179a471872f6e26f0ae773d42" >> $CABALHOME/config+    echo "    2c6c3627bd6c982990239487f1abd02e08a02e6cf16edb105a8012d444d870c3" >> $CABALHOME/config+    echo "    0a5c7ea47cd1b15f01f5f51a33adda7e655bc0f0b0615baa8e271f4c3351e21d" >> $CABALHOME/config+    echo "    51f0161b906011b52c6613376b1ae937670da69322113a246a09f807c62f6921" >> $CABALHOME/config   - |-    if $GHCHEAD; then+    if $HEADHACKAGE; then     echo "allow-newer: $($HCPKG list --simple-output | sed -E 's/([a-zA-Z-]+)-[0-9.]+/*:\1/g')" >> $CABALHOME/config-    -    echo "repository head.hackage"                                                        >> $CABALHOME/config-    echo "   url: http://head.hackage.haskell.org/"                                       >> $CABALHOME/config+    echo "repository head.hackage.ghc.haskell.org"                                        >> $CABALHOME/config+    echo "   url: https://ghc.gitlab.haskell.org/head.hackage/"                           >> $CABALHOME/config     echo "   secure: True"                                                                >> $CABALHOME/config-    echo "   root-keys: 07c59cb65787dedfaef5bd5f987ceb5f7e5ebf88b904bbd4c5cbdeb2ff71b740" >> $CABALHOME/config-    echo "              2e8555dde16ebd8df076f1a8ef13b8f14c66bad8eafefd7d9e37d0ed711821fb" >> $CABALHOME/config-    echo "              8f79fd2389ab2967354407ec852cbe73f2e8635793ac446d09461ffb99527f6e" >> $CABALHOME/config+    echo "   root-keys: 7541f32a4ccca4f97aea3b22f5e593ba2c0267546016b992dfadcd2fe944e55d" >> $CABALHOME/config+    echo "              26021a13b401500c8eb2761ca95c61f2d625bfef951b939a8124ed12ecf07329" >> $CABALHOME/config+    echo "              f76d08be13e9a61a377a85e2fb63f4c5435d40f8feb3e12eb05905edb8cdea89" >> $CABALHOME/config     echo "   key-threshold: 3"                                                            >> $CABALHOME/config     fi+  - |+    echo "program-default-options"                >> $CABALHOME/config+    echo "  ghc-options: $GHCJOBS +RTS -M6G -RTS" >> $CABALHOME/config   - cat $CABALHOME/config   - rm -fv cabal.project cabal.project.local cabal.project.freeze   - travis_retry ${CABAL} v2-update -v+  - if [ $HCNUMVER -ge 80800 ] && [ $HCNUMVER -lt 80802 ] ; then HLINTVER=$(cd /tmp && (${CABAL} v2-install -v $WITHCOMPILER --dry-run hlint  --constraint='hlint ==2.2.*' |  perl -ne 'if (/\bhlint-(\d+(\.\d+)*)\b/) { print "$1"; last; }')); echo "HLint version $HLINTVER" ; fi+  - "if [ $HCNUMVER -ge 80800 ] && [ $HCNUMVER -lt 80802 ] ; then if [ ! -e $HOME/.hlint/hlint-$HLINTVER/hlint ]; then echo \"Downloading HLint version $HLINTVER\"; mkdir -p $HOME/.hlint; curl --write-out 'Status Code: %{http_code} Redirects: %{num_redirects} Total time: %{time_total} Total Dsize: %{size_download}\\n' --silent --location --output $HOME/.hlint/hlint-$HLINTVER.tar.gz \"https://github.com/ndmitchell/hlint/releases/download/v$HLINTVER/hlint-$HLINTVER-x86_64-linux.tar.gz\"; tar -xzv -f $HOME/.hlint/hlint-$HLINTVER.tar.gz -C $HOME/.hlint; fi ; fi"+  - if [ $HCNUMVER -ge 80800 ] && [ $HCNUMVER -lt 80802 ] ; then mkdir -p $CABALHOME/bin && ln -sf "$HOME/.hlint/hlint-$HLINTVER/hlint" $CABALHOME/bin/hlint ; fi+  - if [ $HCNUMVER -ge 80800 ] && [ $HCNUMVER -lt 80802 ] ; then hlint --version ; fi   # Generate cabal.project   - rm -rf cabal.project cabal.project.local cabal.project.freeze   - touch cabal.project   - |-    echo 'packages: "."' >> cabal.project+    echo "packages: ." >> cabal.project   - |-    echo "package ersatz"                      >> cabal.project-    echo "  flags: +examples"                  >> cabal.project-    echo ""                                    >> cabal.project-    echo "write-ghc-environment-files: always" >> cabal.project+    echo "package ersatz"     >> cabal.project+    echo "  flags: +examples" >> cabal.project   - "for pkg in $($HCPKG list --simple-output); do echo $pkg | sed 's/-[^-]*$//' | (grep -vE -- '^(ersatz)$' || true) | sed 's/^/constraints: /' | sed 's/$/ installed/' >> cabal.project.local; done"   - cat cabal.project || true   - cat cabal.project.local || true   - if [ -f "./configure.ac" ]; then (cd "." && autoreconf -i); fi-  - ${CABAL} v2-freeze -w ${HC} ${TEST} ${BENCH} | color_cabal_output+  - ${CABAL} v2-freeze $WITHCOMPILER ${TEST} ${BENCH} | color_cabal_output   - "cat cabal.project.freeze | sed -E 's/^(constraints: *| *)//' | sed 's/any.//'"   - rm  cabal.project.freeze-  - ${CABAL} v2-build -w ${HC} ${TEST} ${BENCH} --dep -j2 all | color_cabal_output+  - ${CABAL} v2-build $WITHCOMPILER ${TEST} ${BENCH} --dep -j2 all | color_cabal_output script:   - DISTDIR=$(mktemp -d /tmp/dist-test.XXXX)   # Packaging...@@ -144,29 +158,33 @@   # Unpacking...   - mv dist-newstyle/sdist/*.tar.gz ${DISTDIR}/   - cd ${DISTDIR} || false-  - find . -maxdepth 1 -name '*.tar.gz' -exec tar -xvf '{}' \;+  - find . -maxdepth 1 -type f -name '*.tar.gz' -exec tar -xvf '{}' \;+  - find . -maxdepth 1 -type f -name '*.tar.gz' -exec rm       '{}' \;+  - PKGDIR_ersatz="$(find . -maxdepth 1 -type d -regex '.*/ersatz-[0-9.]*')"   # Generate cabal.project   - rm -rf cabal.project cabal.project.local cabal.project.freeze   - touch cabal.project   - |-    echo 'packages: "ersatz-*/*.cabal"' >> cabal.project+    echo "packages: ${PKGDIR_ersatz}" >> cabal.project   - |-    echo "package ersatz"                      >> cabal.project-    echo "  flags: +examples"                  >> cabal.project-    echo ""                                    >> cabal.project-    echo "write-ghc-environment-files: always" >> cabal.project+    echo "package ersatz"     >> cabal.project+    echo "  flags: +examples" >> cabal.project   - "for pkg in $($HCPKG list --simple-output); do echo $pkg | sed 's/-[^-]*$//' | (grep -vE -- '^(ersatz)$' || true) | sed 's/^/constraints: /' | sed 's/$/ installed/' >> cabal.project.local; done"   - cat cabal.project || true   - cat cabal.project.local || true   # Building with tests and benchmarks...   # build & run tests, build benchmarks-  - ${CABAL} v2-build -w ${HC} ${TEST} ${BENCH} all | color_cabal_output+  - ${CABAL} v2-build $WITHCOMPILER ${TEST} ${BENCH} all | color_cabal_output   # Testing...-  - ${CABAL} v2-test -w ${HC} ${TEST} ${BENCH} all | color_cabal_output+  - ${CABAL} v2-test $WITHCOMPILER ${TEST} ${BENCH} all | color_cabal_output+  # HLint..+  - if [ $HCNUMVER -ge 80800 ] && [ $HCNUMVER -lt 80802 ] ; then (cd ${PKGDIR_ersatz} && hlint src) ; fi+  - if [ $HCNUMVER -ge 80800 ] && [ $HCNUMVER -lt 80802 ] ; then (cd ${PKGDIR_ersatz} && hlint examples/sudoku) ; fi+  - if [ $HCNUMVER -ge 80800 ] && [ $HCNUMVER -lt 80802 ] ; then (cd ${PKGDIR_ersatz} && hlint examples/regexp-grid) ; fi   # cabal check...-  - (cd ersatz-* && ${CABAL} -vnormal check)+  - (cd ${PKGDIR_ersatz} && ${CABAL} -vnormal check)   # haddock...-  - ${CABAL} v2-haddock -w ${HC} ${TEST} ${BENCH} all | color_cabal_output+  - ${CABAL} v2-haddock $WITHCOMPILER --with-haddock $HADDOCK ${TEST} ${BENCH} all | color_cabal_output -# REGENDATA ["--output=.travis.yml","--config=cabal.haskell-ci","cabal.project"]+# REGENDATA ("0.7.20191105",["--output=.travis.yml","--config=cabal.haskell-ci","cabal.project"]) # EOF
CHANGELOG.md view
@@ -1,3 +1,9 @@+0.4.8 [2020.01.29]+------------------+* Add `MonadSAT` and `MonadQSAT`+* Achieve forward compatibility with+  [GHC proposal 229](https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0229-whitespace-bang-patterns.rst).+ 0.4.7 [2019.06.01] ------------------ * Add `anyminisat` and `trySolvers`
README.md view
@@ -44,7 +44,7 @@ To allocate fresh existentially or universally quantified variables or to assert that a Bit is true and add the attendant circuit with sharing to the current problem you use the SAT monad.  ```haskell-verify_currying :: (MonadState s m, HasQSAT s) => m ()+verify_currying :: (MonadQSAT s m) => m () verify_currying = do   (x::Bit, y::Bit, z::Bit) <- forall   assert $ ((x && y) ==> z) === (x ==> y ==> z)
ersatz.cabal view
@@ -1,5 +1,5 @@ name:           ersatz-version:        0.4.7+version:        0.4.8 license:        BSD3 license-file:   LICENSE author:         Edward A. Kmett, Eric Mertens, Johan Kiviniemi@@ -308,12 +308,12 @@   type: exitcode-stdio-1.0   main-is: Moore.hs   hs-source-dirs: tests-  build-depends: base, array, mtl, ersatz+  build-depends: base, array, 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+  build-depends: base, ersatz   default-language: Haskell2010
examples/regexp-grid/RegexpGrid/Problem.hs view
@@ -59,7 +59,7 @@   {-# INLINE mappend #-} #endif -problem :: (Applicative m, Fail.MonadFail m, MonadState s m, HasSAT s)+problem :: (Applicative m, Fail.MonadFail m, MonadSAT s m)         => m (Map Pos Field) problem = do   -- Allocate a literal for each field.@@ -67,7 +67,7 @@   runReaderT problem' fieldMap   return fieldMap -problem' :: (Fail.MonadFail m, MonadState s m, HasSAT s)+problem' :: (Fail.MonadFail m, MonadSAT s m)          => ReaderT (Map Pos Field) m () problem' = do   r [P00,P01,P02,P03,P04,P05,P06] ".*H.*H.*"@@ -112,7 +112,7 @@   r [P7b,P6b,P5a,P49,P38,P27,P16,P05] "[^M]*M[^M]*"   r [P6c,P5b,P4a,P39,P28,P17,P06] "(S|MM|HHH)*" -r :: (Fail.MonadFail m, MonadState s m, HasSAT s)+r :: (Fail.MonadFail m, MonadSAT s m)   => [Pos] -> String -> ReaderT (Map Pos Field) m () r poss regexpStr = do   fieldMap <- ask
examples/sudoku/Sudoku/Problem.hs view
@@ -8,7 +8,6 @@ import Control.Applicative #endif import Control.Monad.Reader-import Control.Monad.State import Data.Array (Array, (!)) import qualified Data.Array as Array import Data.Word@@ -25,7 +24,7 @@                }   deriving Show -problem :: (Applicative m, MonadState s m, HasSAT s)+problem :: (Applicative m, MonadSAT s m)         => Array Index Word8 -> m Grid problem initValues = do   cellArray <-  Array.listArray range@@ -40,13 +39,13 @@    return cellArray -problem' :: (MonadState s m, HasSAT s) => ReaderT Env m ()+problem' :: MonadSAT s m => ReaderT Env m () problem' = do   legalValues   mapM_ allDifferent (subsquares ++ horizontal ++ vertical)  -- | Assert that each cell must have one of the legal values.-legalValues :: (MonadState s m, HasSAT s) => ReaderT Env m ()+legalValues :: MonadSAT s m => ReaderT Env m () legalValues = mapM_ legalValue . Array.elems =<< asks envCellArray   where     legalValue cell = do@@ -54,8 +53,7 @@       assert $ any (cell ===) values  -- | Assert that each cell in a group must have a different value.-allDifferent :: (MonadState s m, HasSAT s)-             => [(Word8,Word8)] -> ReaderT Env m ()+allDifferent :: MonadSAT s m => [(Word8,Word8)] -> ReaderT Env m () allDifferent indices = do   cellArray <- asks envCellArray   let pairs = [ (cellArray ! a, cellArray ! b)
src/Ersatz/Bit.hs view
@@ -63,7 +63,7 @@   | Mux !Bit !Bit !Bit   | Not !Bit   | Var !Literal-  | Run ( forall m s . (MonadState s m, HasSAT s) => m Bit )+  | Run ( forall m s . MonadSAT s m => m Bit )   deriving (Typeable)  instance Show Bit where@@ -160,7 +160,7 @@  -- | Assert claims that 'Bit' must be 'true' in any satisfying interpretation -- of the current problem.-assert :: (MonadState s m, HasSAT s) => Bit -> m ()+assert :: MonadSAT s m => 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@@ -171,7 +171,7 @@   assertFormula (formulaLiteral l)  -- | Convert a 'Bit' to a 'Literal'.-runBit :: (MonadState s m, HasSAT s) => Bit -> m Literal+runBit :: MonadSAT s m => Bit -> m Literal runBit (Not c) = negateLiteral `fmap` runBit c runBit (Var l) = return l runBit (Run action) = action >>= runBit
src/Ersatz/Problem.hs view
@@ -8,6 +8,7 @@ {-# LANGUAGE DeriveDataTypeable #-} {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE Trustworthy #-}+{-# LANGUAGE ConstraintKinds #-}  {-# OPTIONS_HADDOCK not-home #-} #ifndef MIN_VERSION_lens@@ -27,6 +28,7 @@   -- * SAT     SAT(SAT)   , HasSAT(..)+  , MonadSAT   , runSAT, runSAT', dimacsSAT   , literalExists   , assertFormula@@ -34,6 +36,7 @@   -- * QSAT   , QSAT(QSAT)   , HasQSAT(..)+  , MonadQSAT   , runQSAT, runQSAT', qdimacsQSAT   , literalForall   -- * DIMACS pretty printing@@ -77,6 +80,12 @@ import Control.Monad.Identity #endif +-- | Constraint synonym for types that carry a SAT state.+type MonadSAT  s m = (HasSAT  s, MonadState s m)++-- | Constraint synonym for types that carry a QSAT state.+type MonadQSAT s m = (HasQSAT s, MonadState s m)+ ------------------------------------------------------------------------------ -- SAT Problems ------------------------------------------------------------------------------@@ -114,12 +123,12 @@   def = SAT 1 (formulaLiteral literalTrue) HashMap.empty  -- | Run a 'SAT'-generating state computation. Useful e.g. in ghci for--- disambiguating the type of a 'MonadState', 'HasSAT' value.+-- disambiguating the type of a 'MonadSAT' value. runSAT :: StateT SAT m a -> m (a, SAT) runSAT s = runStateT s def  -- | Run a 'SAT'-generating state computation in the 'Identity' monad. Useful--- e.g. in ghci for disambiguating the type of a 'MonadState', 'HasSAT' value.+-- e.g. in ghci for disambiguating the type of a 'MonadSAT' value. runSAT' :: StateT SAT Identity a -> (a, SAT) runSAT' = runIdentity . runSAT @@ -128,15 +137,15 @@ dimacsSAT :: StateT SAT Identity a -> Lazy.ByteString dimacsSAT = toLazyByteString . dimacs . snd . runSAT' -literalExists :: (MonadState s m, HasSAT s) => m Literal+literalExists :: MonadSAT s m => m Literal literalExists = fmap Literal $ lastAtom <+= 1 {-# INLINE literalExists #-} -assertFormula :: (MonadState s m, HasSAT s) => Formula -> m ()+assertFormula :: MonadSAT s m => Formula -> m () assertFormula xs = formula <>= xs {-# INLINE assertFormula #-} -generateLiteral :: (MonadState s m, HasSAT s) => a -> (Literal -> m ()) -> m Literal+generateLiteral :: MonadSAT s m => a -> (Literal -> m ()) -> m Literal generateLiteral a f = do   let sn = unsafePerformIO (makeStableName' a)   use (stableMap.at sn) >>= \ ml -> case ml of@@ -188,7 +197,7 @@ qdimacsQSAT :: StateT QSAT Identity a -> Lazy.ByteString qdimacsQSAT = toLazyByteString . qdimacs . snd . runQSAT' -literalForall :: (MonadState s m, HasQSAT s) => m Literal+literalForall :: MonadQSAT s m => m Literal literalForall = do    l <- lastAtom <+= 1    universals.contains l .= True
src/Ersatz/Relation/Data.hs view
@@ -12,7 +12,7 @@ import Ersatz.Bit import Ersatz.Codec import Ersatz.Variable (exists)-import Ersatz.Problem (HasSAT)+import Ersatz.Problem (MonadSAT)  import qualified Data.Array as A import Data.Array ( Array, Ix )@@ -25,7 +25,7 @@   decode s (Relation a) = decode s a   encode a = Relation $ encode a -relation :: ( Ix a, Ix b, MonadState s m, HasSAT s )+relation :: ( Ix a, Ix b, MonadSAT s m )          => ((a,b),(a,b)) -> m ( Relation a b ) relation bnd = do     pairs <- sequence $ do@@ -36,7 +36,7 @@     return $ build bnd pairs  symmetric_relation ::-  (HasSAT s, MonadState s m, Ix b) =>+  (MonadSAT s m, Ix b) =>   ((b, b), (b, b)) -> m (Relation b b) symmetric_relation bnd = do     pairs <- sequence $ do
src/Ersatz/Relation/Op.hs view
@@ -48,7 +48,7 @@         ((_ ,bl),(_ ,br)) = bounds b         bnd = ((ao,bl),(au,br))     in  build bnd $ do-          i @ (x,z) <- range bnd+          i@(x,z) <- range bnd           return (i, or $ do                 y <- range ( al, ar )                 return $ and [ a!(x,y), b!(y,z) ]
src/Ersatz/Relation/Prop.hs view
@@ -92,7 +92,7 @@     x <- range ( a , c )     return $ f deg $ do         y <- range (b,d)-        return $ r !(x,y)+        return $ r ! (x,y)  transitive :: ( Ix a )            => Relation a a -> Bit
src/Ersatz/Variable.hs view
@@ -24,21 +24,20 @@   ) where  import Control.Monad-import Control.Monad.State.Class import Ersatz.Internal.Literal import Ersatz.Problem import GHC.Generics -exists :: (Variable a, MonadState s m, HasSAT s)  => m a+exists :: (Variable a, MonadSAT s m)  => m a exists = literally literalExists  #ifndef HLINT-forall :: (Variable a, MonadState s m, HasQSAT s)  => m a+forall :: (Variable a, MonadQSAT s m)  => m a forall = literally literalForall #endif  class GVariable f where-  gliterally :: (MonadState s m, HasSAT s) => m Literal -> m (f a)+  gliterally :: MonadSAT s m => m Literal -> m (f a)  instance GVariable U1 where   gliterally _ = return U1@@ -55,14 +54,14 @@ -- | Instances for this class for product-like types can be automatically derived -- for any type that is an instance of 'Generic'. class Variable t where-  literally :: (HasSAT s, MonadState s m) => m Literal -> m t+  literally :: MonadSAT s m => m Literal -> m t   default literally ::-    (HasSAT s, MonadState s m, Generic t, GVariable (Rep t)) =>+    (MonadSAT s m, Generic t, GVariable (Rep t)) =>     m Literal -> m t   literally = genericLiterally  genericLiterally ::-  (HasSAT s, MonadState s m, Generic t, GVariable (Rep t)) =>+  (MonadSAT s m, Generic t, GVariable (Rep t)) =>   m Literal -> m t genericLiterally = fmap to . gliterally 
tests/Moore.hs view
@@ -24,7 +24,6 @@ import qualified Data.Array as A import System.Environment (getArgs) import Control.Monad ( void, when, forM )-import Control.Monad.State  main :: IO ( ) main = do@@ -43,9 +42,10 @@      (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 ::+  MonadSAT s m =>+  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))
tests/Z001.hs view
@@ -12,7 +12,6 @@ import Data.Proxy import Data.List ( transpose ) import Control.Monad ( replicateM, forM_ )-import Control.Monad.State  main = do   (Satisfied, Just ms) <- solveWith anyminisat $ do@@ -39,7 +38,7 @@        $ m ++ encode [ replicate (d-1) 0 ++ [1] ]  class Unknown a where-  unknown :: (MonadState s m, HasSAT s) => m a+  unknown :: MonadSAT s m => m a  -- | square matrices newtype Matrix (dim::Nat)  a = Matrix [[a]]