satchmo-toysat (empty) → 0.2.0.0

raw patch · 6 files changed

+259/−0 lines, 6 filesdep +arraydep +basedep +containerssetup-changed

Dependencies added: array, base, containers, satchmo, toysolver

Files

.travis.yml +64/−0
LICENSE +30/−0
README.md +6/−0
Setup.hs +2/−0
satchmo-toysat.cabal +37/−0
src/Satchmo/SAT/Toysat.hs +120/−0

+ .travis.yml view

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

+ LICENSE view

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

+ README.md view

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

+ Setup.hs view

@@ -0,0 +1,2 @@+import Distribution.Simple+main = defaultMain

+ satchmo-toysat.cabal view

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

+ src/Satchmo/SAT/Toysat.hs view

@@ -0,0 +1,120 @@+{-# LANGUAGE ScopedTypeVariables, TypeFamilies, MultiParamTypeClasses, TypeSynonymInstances #-}+{-# OPTIONS_GHC -Wall #-}+--------------------------------------------------------------------+-- |+-- Copyright :  © Masahiro Sakai 2014+-- License   :  BSD3+-- Maintainer:  Masahiro Sakai <masahiro.sakai@gmail.com>+-- 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