diff --git a/.travis.yml b/.travis.yml new file mode 100644 --- /dev/null +++ b/.travis.yml @@ -0,0 +1,64 @@ +# NB: don't set `language: haskell` here + +# The following enables several GHC versions to be tested; often it's enough to test only against the last release in a major GHC version. Feel free to omit lines listings versions you don't need/want testing for. +env: +# - CABALVER=1.16 GHCVER=6.12.3 +# - CABALVER=1.16 GHCVER=7.0.1 +# - CABALVER=1.16 GHCVER=7.0.2 +# - CABALVER=1.16 GHCVER=7.0.3 +# - CABALVER=1.16 GHCVER=7.0.4 +# - CABALVER=1.16 GHCVER=7.2.1 +# - CABALVER=1.16 GHCVER=7.2.2 +# - CABALVER=1.16 GHCVER=7.4.1 +# - CABALVER=1.16 GHCVER=7.4.2 +# - CABALVER=1.16 GHCVER=7.6.1 +# - CABALVER=1.16 GHCVER=7.6.2 + - CABALVER=1.18 GHCVER=7.6.3 +# - CABALVER=1.18 GHCVER=7.8.1 # see note about Alex/Happy for GHC >= 7.8 +# - CABALVER=1.18 GHCVER=7.8.2 + - CABALVER=1.18 GHCVER=7.8.3 + - CABALVER=1.22 GHCVER=7.10.1 +# - CABALVER=head GHCVER=head # see section about GHC HEAD snapshots + +matrix: + allow_failures: + - env: CABALVER=1.22 GHCVER=7.10.1 + +# Note: the distinction between `before_install` and `install` is not important. +before_install: + - travis_retry sudo add-apt-repository -y ppa:hvr/ghc + - travis_retry sudo apt-get update + - travis_retry sudo apt-get install cabal-install-$CABALVER ghc-$GHCVER # see note about happy/alex + - export PATH=/opt/ghc/$GHCVER/bin:/opt/cabal/$CABALVER/bin:$PATH + - | + if [ $GHCVER = "head" ] || [ ${GHCVER%.*} = "7.8" ] || [ ${GHCVER%.*} = "7.10" ]; then + travis_retry sudo apt-get install happy-1.19.4 alex-3.1.3 + export PATH=/opt/alex/3.1.3/bin:/opt/happy/1.19.4/bin:$PATH + else + travis_retry sudo apt-get install happy alex + fi + +install: + - cabal --version + - echo "$(ghc --version) [$(ghc --print-project-git-commit-id 2> /dev/null || echo '?')]" + - travis_retry cabal update + - cabal install --only-dependencies --enable-tests --enable-benchmarks + +# 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: + - if [ -f configure.ac ]; then autoreconf -i; fi + - cabal configure --enable-tests --enable-benchmarks -v2 # -v2 provides useful information for debugging + - cabal build # this builds all libraries and executables (including tests/benchmarks) + - cabal test + - cabal check + - cabal sdist # tests that a source-distribution can be generated + +# The following scriptlet checks that the resulting source distribution can be built & installed + - export SRC_TGZ=$(cabal info . | awk '{print $2 ".tar.gz";exit}') ; + cd dist/; + if [ -f "$SRC_TGZ" ]; then + cabal install --force-reinstalls "$SRC_TGZ"; + else + echo "expected '$SRC_TGZ' not found"; + exit 1; + fi diff --git a/LICENSE b/LICENSE new file mode 100644 --- /dev/null +++ b/LICENSE @@ -0,0 +1,30 @@ +Copyright (c) 2015, Masahiro Sakai + +All rights reserved. + +Redistribution and use in source and binary forms, with or without +modification, are permitted provided that the following conditions are met: + + * Redistributions of source code must retain the above copyright + notice, this list of conditions and the following disclaimer. + + * Redistributions in binary form must reproduce the above + copyright notice, this list of conditions and the following + disclaimer in the documentation and/or other materials provided + with the distribution. + + * Neither the name of Masahiro Sakai nor the names of other + contributors may be used to endorse or promote products derived + from this software without specific prior written permission. + +THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS +"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT +LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR +A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT +OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, +SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT +LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, +DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY +THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT +(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE +OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. diff --git a/README.md b/README.md new file mode 100644 --- /dev/null +++ b/README.md @@ -0,0 +1,6 @@ +satchmo-toysat +============== + +[![Build Status](https://secure.travis-ci.org/msakai/satchmo-toysat.png?branch=master)](http://travis-ci.org/msakai/satchmo-toysat) + +toysat driver as backend for satchmo diff --git a/Setup.hs b/Setup.hs new file mode 100644 --- /dev/null +++ b/Setup.hs @@ -0,0 +1,2 @@ +import Distribution.Simple +main = defaultMain diff --git a/satchmo-toysat.cabal b/satchmo-toysat.cabal new file mode 100644 --- /dev/null +++ b/satchmo-toysat.cabal @@ -0,0 +1,37 @@ +-- Initial satchmo-toysat.cabal generated by cabal init. For further documentation, see +-- http://haskell.org/cabal/users-guide/ + +name: satchmo-toysat +version: 0.2.0.0 +synopsis: toysat driver as backend for satchmo +description: toysat driver as backend for satchmo +homepage: https://github.com/msakai/satchmo-toysat +license: BSD3 +license-file: LICENSE +author: Masahiro Sakai +maintainer: masahiro.sakai@gmail.com +copyright: (c) 2014 Masahiro Sakai +category: Logic, Algorithms +build-type: Simple +extra-source-files: README.md, .travis.yml +cabal-version: >=1.10 + +source-repository head + type: git + location: git://github.com/msakai/satchmo-toysat.git + +library + exposed-modules: Satchmo.SAT.Toysat + build-depends: + base >=4.5 && <4.9, + array >= 0.4 && < 0.6, + containers >= 0.5.0.0 && < 0.6, + satchmo >=2.8.1 && <2.9, + toysolver >=0.2.0 && <0.3.0 + hs-source-dirs: src + default-language: Haskell2010 + other-extensions: + ScopedTypeVariables, + MultiParamTypeClasses, + TypeFamilies, + TypeSynonymInstances diff --git a/src/Satchmo/SAT/Toysat.hs b/src/Satchmo/SAT/Toysat.hs new file mode 100644 --- /dev/null +++ b/src/Satchmo/SAT/Toysat.hs @@ -0,0 +1,120 @@ +{-# LANGUAGE ScopedTypeVariables, TypeFamilies, MultiParamTypeClasses, TypeSynonymInstances #-} +{-# OPTIONS_GHC -Wall #-} +-------------------------------------------------------------------- +-- | +-- Copyright : © Masahiro Sakai 2014 +-- License : BSD3 +-- Maintainer: Masahiro Sakai +-- Stability : experimental +-- Portability: portable +-- +-------------------------------------------------------------------- + +module Satchmo.SAT.Toysat + +( SAT +, fresh +, emit +, solve +, solve_with_timeout +) + +where + +import qualified ToySolver.SAT as API + +import Satchmo.Data +import Satchmo.Boolean hiding ( not ) +import Satchmo.Code + +import Control.Concurrent +import Control.Exception +import Control.Monad.Fix +import Control.Applicative +import Data.Array.IArray +import System.IO + +newtype SAT a + = SAT { unSAT :: API.Solver -> IO a + } + +instance Functor SAT where + fmap f ( SAT m ) = SAT $ \ s -> fmap f ( m s ) + +instance Monad SAT where + return x = SAT $ \ _ -> return x + SAT m >>= f = SAT $ \ s -> do + x <- m s ; let { SAT n = f x } ; n s + +instance Applicative SAT where + pure = return + a <*> b = a >>= \ f -> fmap f b + +instance MonadFix SAT where + mfix f = SAT $ \ s -> mfix ( \ a -> unSAT (f a) s ) + +instance MonadSAT SAT where + fresh = SAT $ \ s -> do + x <- API.newVar s + let l = literal True x + -- hPutStrLn stderr $ "fresh: " ++ show (x, l) + return l + + emit cl = SAT $ \ s -> do + let conv l = if positive l then variable l else negate (variable l) + apicl = map conv $ literals cl + API.addClause s apicl + -- hPutStrLn stderr $ "adding clause " ++ show (cl, apicl, res) + return () + + note msg = SAT $ \ _ -> hPutStrLn stderr msg + + type Decoder SAT = SAT + decode_variable v = SAT $ \ s -> do + m <- API.getModel s + return $ m ! v + +instance Decode SAT Boolean Bool where + decode b = case b of + Constant c -> return c + Boolean l -> do + let dv v = SAT $ \ s -> do + m <- API.getModel s + return $ m ! v + v <- dv $ variable l + return $ if positive l then v else not v + +solve_with_timeout :: Maybe Int -> SAT (SAT a) -> IO (Maybe a) +solve_with_timeout mto action = do + accu <- newEmptyMVar + worker <- forkIO $ do res <- solve action ; putMVar accu res + timer <- forkIO $ case mto of + Just to -> do + threadDelay ( 10^(6::Int) * to ) + killThread worker + putMVar accu Nothing + _ -> return () + takeMVar accu `Control.Exception.catch` \ ( _ :: AsyncException ) -> do + hPutStrLn stderr "caught" + killThread worker + killThread timer + return Nothing + +solve :: SAT (SAT a) -> IO (Maybe a) +solve action = do + s <- API.newSolver + hPutStrLn stderr $ "start producing CNF" + SAT decoder <- unSAT action s + v <- API.nVars s + c <- API.nConstraints s + hPutStrLn stderr + $ unwords [ "CNF finished", "vars", show v, "clauses", show c ] + hPutStrLn stderr $ "starting solver" + status <- API.solve s + hPutStrLn stderr $ "solver finished, result: " ++ show status + if status then do + hPutStrLn stderr $ "starting decoder" + out <- decoder s + hPutStrLn stderr $ "decoder finished" + return $ Just out + else return Nothing