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 +2/−0
- .travis.yml +68/−50
- CHANGELOG.md +6/−0
- README.md +1/−1
- ersatz.cabal +3/−3
- examples/regexp-grid/RegexpGrid/Problem.hs +3/−3
- examples/sudoku/Sudoku/Problem.hs +4/−6
- src/Ersatz/Bit.hs +3/−3
- src/Ersatz/Problem.hs +15/−6
- src/Ersatz/Relation/Data.hs +3/−3
- src/Ersatz/Relation/Op.hs +1/−1
- src/Ersatz/Relation/Prop.hs +1/−1
- src/Ersatz/Variable.hs +6/−7
- tests/Moore.hs +4/−4
- tests/Z001.hs +1/−2
.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]]