diff --git a/.travis.yml b/.travis.yml --- a/.travis.yml +++ b/.travis.yml @@ -1,36 +1,39 @@ -language: haskell -env: - - GHCVER=7.8.3 +language: c +sudo: false -before_install: - - | - if [ $GHCVER = `ghc --numeric-version` ]; then - # Try installing some of the build-deps with apt-get for speed. - travis/cabal-apt-install --enable-tests $MODE - export CABAL=cabal - else - # Install the GHC we want from hvr's PPA - travis_retry sudo add-apt-repository -y ppa:hvr/ghc - travis_retry sudo apt-get update - travis_retry sudo apt-get install cabal-install-1.18 ghc-$GHCVER happy - export CABAL=cabal-1.18 - export PATH=/opt/ghc/$GHCVER/bin:$PATH - fi +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=head GHCVER=head GHCOPTS="" JOPTS="-j2" + addons: {apt: {packages: [cabal-install-head,ghc-head], sources: [hvr-ghc]}} - # Uncomment whenever hackage is down. - # - mkdir -p ~/.cabal && cp travis/config ~/.cabal/config && cabal update - - cabal update + allow_failures: + - env: CABALVER=head GHCVER=head GHCOPTS="" JOPTS="-j2" - # Try installing some of the build-deps with apt-get for speed. - - travis/cabal-apt-install $mode - - export PATH=~/.cabal/bin:$PATH +before_install: + - export PATH=/opt/ghc/$GHCVER/bin:/opt/cabal/$CABALVER/bin:$PATH + - export CABAL=cabal-$CABALVER + - $CABAL --version + - travis_retry $CABAL update install: - - cabal configure -flib-Werror $mode - - cabal build + - | + 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 + fi + - $CABAL install $JOPTS --enable-tests --only-dependencies --force script: - - $script + - $CABAL configure -v2 --enable-tests + - $CABAL build $JOPTS --ghc-options=$GHCOPTS + - | + if [ $GHCVER != "head" ]; then + $CABAL test + fi notifications: irc: @@ -38,7 +41,4 @@ - "irc.freenode.org#haskell-lens" skip_join: true template: - - "\x0313ersatz\x03/\x0306%{branch}\x03 \x0314%{commit}\x03 %{build_url} %{message}" - -env: - - mode="--enable-tests" script="cabal test --show-details=always" + - "\x0313ersatz\x0f/\x0306%{branch}\x0f \x0314%{commit}\x0f %{message} \x0302\x1f%{build_url}\x0f" diff --git a/CHANGELOG.md b/CHANGELOG.md --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1,3 +1,7 @@ +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. + 0.3 ----- * Unified `Encoding` and `Decoding` into `Codec` diff --git a/ersatz.cabal b/ersatz.cabal --- a/ersatz.cabal +++ b/ersatz.cabal @@ -1,5 +1,5 @@ name: ersatz -version: 0.3 +version: 0.3.1 license: BSD3 license-file: LICENSE author: Edward A. Kmett, Eric Mertens, Johan Kiviniemi @@ -75,7 +75,7 @@ build-type: Custom cabal-version: >= 1.10 -tested-with: GHC == 7.4.1, GHC == 7.6.2, GHC == 7.8.2 +tested-with: GHC == 7.8.3, GHC == 7.10.1 extra-source-files: .ghci .gitignore @@ -169,15 +169,15 @@ build-depends: array >= 0.2 && < 0.6, - base >= 4 && < 5, + base >= 4.7 && < 5, bytestring >= 0.10.4.0 && < 0.12, containers >= 0.2.0.1 && < 0.6, - data-default >= 0.5 && < 0.6, + data-default >= 0.5 && < 0.8, lens >= 3.8 && < 5, mtl >= 1.1 && < 2.3, - process >= 1.1 && < 1.3, + process >= 1.1 && < 1.5, temporary >= 1.1 && < 1.3, - transformers >= 0.3 && < 0.5, + transformers >= 0.3 && < 0.6, unordered-containers == 0.2.* if impl(ghc >= 7.4 && < 7.6) @@ -198,6 +198,7 @@ Ersatz.Solver Ersatz.Solver.DepQBF Ersatz.Solver.Minisat + Ersatz.Solver.Z3 Ersatz.Variable other-modules: @@ -280,8 +281,6 @@ doctest >= 0.9.1, filepath ghc-options: -Wall -threaded - if impl(ghc<7.6.1) - ghc-options: -Werror hs-source-dirs: tests test-suite hlint diff --git a/examples/regexp-grid/Main.hs b/examples/regexp-grid/Main.hs --- a/examples/regexp-grid/Main.hs +++ b/examples/regexp-grid/Main.hs @@ -11,7 +11,7 @@ main :: IO () main = do - (res, msol) <- solveWith cryptominisat problem + (res, msol) <- solveWith minisat problem when (res /= Satisfied) (fail (show res)) case msol of Nothing -> fail "Sol was Nothing" diff --git a/examples/regexp-grid/RegexpGrid/Regexp.hs b/examples/regexp-grid/RegexpGrid/Regexp.hs --- a/examples/regexp-grid/RegexpGrid/Regexp.hs +++ b/examples/regexp-grid/RegexpGrid/Regexp.hs @@ -1,8 +1,11 @@ +{-# LANGUAGE CPP #-} -- | A parser for a subset of the regular expression syntax. module RegexpGrid.Regexp (Regexp (..), parseRegexp) where +#if __GLASGOW_HASKELL__ < 710 import Control.Applicative hiding ((<|>), many) +#endif import Control.Monad import Data.Char import Text.Parsec diff --git a/examples/regexp-grid/RegexpGrid/Types.hs b/examples/regexp-grid/RegexpGrid/Types.hs --- a/examples/regexp-grid/RegexpGrid/Types.hs +++ b/examples/regexp-grid/RegexpGrid/Types.hs @@ -1,3 +1,4 @@ +{-# LANGUAGE CPP #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE DeriveGeneric #-} {-# LANGUAGE DeriveDataTypeable #-} @@ -7,7 +8,9 @@ , Field (..) ) where +#if __GLASGOW_HASKELL__ < 710 import Control.Applicative +#endif import Data.Char (chr, ord) import Data.Typeable import Ersatz diff --git a/examples/sudoku/Main.hs b/examples/sudoku/Main.hs --- a/examples/sudoku/Main.hs +++ b/examples/sudoku/Main.hs @@ -1,8 +1,11 @@ +{-# LANGUAGE CPP #-} module Main (main) where import Prelude hiding ((&&), (||), not, and, or, all, any) +#if __GLASGOW_HASKELL__ < 710 import Control.Applicative +#endif import Control.Monad import Data.Array (Array, (!)) import qualified Data.Array as Array diff --git a/examples/sudoku/Sudoku/Problem.hs b/examples/sudoku/Sudoku/Problem.hs --- a/examples/sudoku/Sudoku/Problem.hs +++ b/examples/sudoku/Sudoku/Problem.hs @@ -1,8 +1,12 @@ +{-# LANGUAGE CPP #-} +{-# LANGUAGE FlexibleContexts #-} module Sudoku.Problem (problem, range) where import Prelude hiding ((&&), (||), not, and, or, all, any) +#if __GLASGOW_HASKELL__ < 710 import Control.Applicative +#endif import Control.Monad.Reader import Control.Monad.State import Data.Array (Array, (!)) diff --git a/src/Ersatz/Bit.hs b/src/Ersatz/Bit.hs --- a/src/Ersatz/Bit.hs +++ b/src/Ersatz/Bit.hs @@ -28,7 +28,11 @@ import Control.Applicative import Control.Monad.State +#if __GLASGOW_HASKELL__ < 710 import Data.Foldable (Foldable, toList) +#else +import Data.Foldable (toList) +#endif import qualified Data.Foldable as Foldable import Data.Sequence (Seq, (<|), (|>), (><)) import qualified Data.Sequence as Seq @@ -280,10 +284,10 @@ nor = not . or -- | The logical conjunction of the mapping of a function over several values. - all :: (Foldable t, Boolean b) => (a -> b) -> t a -> b + all :: Foldable t => (a -> b) -> t a -> b -- | The logical disjunction of the mapping of a function over several values. - any :: (Foldable t, Boolean b) => (a -> b) -> t a -> b + any :: Foldable t => (a -> b) -> t a -> b -- | Exclusive-or xor :: b -> b -> b diff --git a/src/Ersatz/Bits.hs b/src/Ersatz/Bits.hs --- a/src/Ersatz/Bits.hs +++ b/src/Ersatz/Bits.hs @@ -1,7 +1,7 @@ +{-# LANGUAGE CPP #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE DeriveGeneric #-} {-# LANGUAGE DeriveDataTypeable #-} -{-# LANGUAGE Safe #-} -------------------------------------------------------------------- -- | -- Copyright : © Edward Kmett 2010-2015, © Eric Mertens 2014, Johan Kiviniemi 2013 @@ -31,9 +31,15 @@ import Control.Monad.Trans.State (State, runState, get, put) import Data.Bits ((.&.), (.|.), shiftL, shiftR) import qualified Data.Bits as Data +#if __GLASGOW_HASKELL__ < 710 import Data.Foldable (Foldable, toList) +#else +import Data.Foldable (toList) +#endif import Data.List (unfoldr, foldl') +#if __GLASGOW_HASKELL__ < 710 import Data.Traversable (traverse) +#endif import Data.Typeable (Typeable) import Data.Word (Word8) import Ersatz.Bit diff --git a/src/Ersatz/Codec.hs b/src/Ersatz/Codec.hs --- a/src/Ersatz/Codec.hs +++ b/src/Ersatz/Codec.hs @@ -1,6 +1,6 @@ +{-# LANGUAGE CPP #-} {-# LANGUAGE Rank2Types #-} {-# LANGUAGE TypeFamilies #-} -{-# LANGUAGE Safe #-} -------------------------------------------------------------------- -- | -- Copyright : © Edward Kmett 2010-2014, Johan Kiviniemi 2013 @@ -31,7 +31,11 @@ class Codec a where type Decoded a :: * -- | Return a value based on the solution if one can be determined. +#if __GLASGOW_HASKELL__ < 710 decode :: (Alternative f, MonadPlus f) => Solution -> a -> f (Decoded a) +#else + decode :: MonadPlus f => Solution -> a -> f (Decoded a) +#endif encode :: Decoded a -> a instance Codec Literal where diff --git a/src/Ersatz/Equatable.hs b/src/Ersatz/Equatable.hs --- a/src/Ersatz/Equatable.hs +++ b/src/Ersatz/Equatable.hs @@ -5,7 +5,6 @@ {-# LANGUAGE DefaultSignatures #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE UndecidableInstances #-} -{-# LANGUAGE Safe #-} {-# OPTIONS_HADDOCK not-home #-} -------------------------------------------------------------------- diff --git a/src/Ersatz/Internal/Formula.hs b/src/Ersatz/Internal/Formula.hs --- a/src/Ersatz/Internal/Formula.hs +++ b/src/Ersatz/Internal/Formula.hs @@ -1,3 +1,4 @@ +{-# LANGUAGE CPP #-} {-# LANGUAGE Rank2Types #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeOperators #-} @@ -5,7 +6,6 @@ {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE DeriveDataTypeable #-} {-# LANGUAGE MultiParamTypeClasses #-} -{-# LANGUAGE Safe #-} {-# OPTIONS_HADDOCK not-home #-} -------------------------------------------------------------------- @@ -27,11 +27,15 @@ , formulaNot, formulaAnd, formulaOr, formulaXor, formulaMux ) where +#if __GLASGOW_HASKELL__ < 710 import Control.Applicative +#endif import Data.IntSet (IntSet) import qualified Data.IntSet as IntSet import qualified Data.List as List (intersperse) +#if __GLASGOW_HASKELL__ < 710 import Data.Monoid +#endif import Data.Set (Set) import qualified Data.Set as Set import Data.Typeable diff --git a/src/Ersatz/Internal/Literal.hs b/src/Ersatz/Internal/Literal.hs --- a/src/Ersatz/Internal/Literal.hs +++ b/src/Ersatz/Internal/Literal.hs @@ -1,5 +1,4 @@ {-# LANGUAGE DeriveDataTypeable #-} -{-# LANGUAGE Safe #-} -------------------------------------------------------------------- -- | -- Copyright : © Edward Kmett 2010-2014, Johan Kiviniemi 2013 diff --git a/src/Ersatz/Internal/Parser.hs b/src/Ersatz/Internal/Parser.hs --- a/src/Ersatz/Internal/Parser.hs +++ b/src/Ersatz/Internal/Parser.hs @@ -1,3 +1,4 @@ +{-# LANGUAGE CPP #-} -------------------------------------------------------------------- -- | -- Copyright : © Edward Kmett 2010-2014, Johan Kiviniemi 2013 @@ -21,7 +22,9 @@ import Control.Applicative import Control.Monad.State import Data.Char (isDigit) +#if __GLASGOW_HASKELL__ < 710 import Data.Traversable (traverse) +#endif type Parser t a = StateT [t] [] a @@ -40,14 +43,14 @@ string :: Eq t => [t] -> Parser t [t] string = traverse token -integer :: (Integral i, Read i) => Parser Char i +integer :: (Num i, Read i) => Parser Char i integer = negation <*> natural negation :: Num n => Parser Char (n -> n) negation = negate <$ token '-' <|> pure id -natural :: (Integral i, Read i) => Parser Char i +natural :: Read i => Parser Char i natural = read <$> some (satisfy isDigit) eof :: Parser t () diff --git a/src/Ersatz/Orderable.hs b/src/Ersatz/Orderable.hs --- a/src/Ersatz/Orderable.hs +++ b/src/Ersatz/Orderable.hs @@ -5,7 +5,6 @@ {-# LANGUAGE DefaultSignatures #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE UndecidableInstances #-} -{-# LANGUAGE Safe #-} {-# OPTIONS_HADDOCK not-home #-} -------------------------------------------------------------------- diff --git a/src/Ersatz/Problem.hs b/src/Ersatz/Problem.hs --- a/src/Ersatz/Problem.hs +++ b/src/Ersatz/Problem.hs @@ -45,7 +45,9 @@ ) where import Data.ByteString.Builder +#if __GLASGOW_HASKELL__ < 710 import Control.Applicative +#endif import Control.Lens import Control.Monad #if !(MIN_VERSION_lens(4,0,0)) @@ -55,7 +57,9 @@ import Data.ByteString (ByteString) import qualified Data.ByteString.Lazy as Lazy import Data.Default +#if __GLASGOW_HASKELL__ < 710 import Data.Foldable (foldMap) +#endif import Data.HashMap.Lazy (HashMap) import qualified Data.HashMap.Lazy as HashMap import Data.Int diff --git a/src/Ersatz/Solution.hs b/src/Ersatz/Solution.hs --- a/src/Ersatz/Solution.hs +++ b/src/Ersatz/Solution.hs @@ -1,7 +1,7 @@ +{-# LANGUAGE CPP #-} {-# LANGUAGE Rank2Types #-} {-# LANGUAGE DeriveDataTypeable #-} {-# LANGUAGE ImpredicativeTypes #-} -{-# LANGUAGE Safe #-} -------------------------------------------------------------------- -- | -- Copyright : © Edward Kmett 2010-2014, Johan Kiviniemi 2013 @@ -17,7 +17,9 @@ , Solver ) where +#if __GLASGOW_HASKELL__ < 710 import Control.Applicative +#endif import Control.Lens import qualified Data.HashMap.Lazy as HashMap import Data.IntMap (IntMap) diff --git a/src/Ersatz/Solver.hs b/src/Ersatz/Solver.hs --- a/src/Ersatz/Solver.hs +++ b/src/Ersatz/Solver.hs @@ -1,3 +1,4 @@ +{-# LANGUAGE CPP #-} -------------------------------------------------------------------- -- | -- Copyright : © Edward Kmett 2010-2014, Johan Kiviniemi 2013 @@ -10,6 +11,7 @@ module Ersatz.Solver ( module Ersatz.Solver.DepQBF , module Ersatz.Solver.Minisat + , module Ersatz.Solver.Z3 , solveWith ) where @@ -22,8 +24,13 @@ 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)) +#else +solveWith :: (Monad m, MonadPlus n, HasSAT s, Default s, Codec a) => Solver s m -> StateT s m a -> m (Result, n (Decoded a)) +#endif solveWith solver m = do (a, problem) <- runStateT m def (res, litMap) <- solver problem diff --git a/src/Ersatz/Solver/DepQBF.hs b/src/Ersatz/Solver/DepQBF.hs --- a/src/Ersatz/Solver/DepQBF.hs +++ b/src/Ersatz/Solver/DepQBF.hs @@ -1,4 +1,3 @@ -{-# LANGUAGE Safe #-} -------------------------------------------------------------------- -- | -- Copyright : © Edward Kmett 2010-2014, Johan Kiviniemi 2013 diff --git a/src/Ersatz/Solver/Minisat.hs b/src/Ersatz/Solver/Minisat.hs --- a/src/Ersatz/Solver/Minisat.hs +++ b/src/Ersatz/Solver/Minisat.hs @@ -1,4 +1,3 @@ -{-# LANGUAGE Safe #-} -------------------------------------------------------------------- -- | -- Copyright : © Edward Kmett 2010-2014, Johan Kiviniemi 2013 diff --git a/src/Ersatz/Solver/Z3.hs b/src/Ersatz/Solver/Z3.hs new file mode 100644 --- /dev/null +++ b/src/Ersatz/Solver/Z3.hs @@ -0,0 +1,68 @@ +-------------------------------------------------------------------- +-- | +-- Copyright : © Edward Kmett 2010-2014, Johan Kiviniemi 2013 +-- License : BSD3 +-- Maintainer: Edward Kmett +-- 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)