picosat 0.1.0.2 → 0.1.1
raw patch · 2 files changed
+24/−38 lines, 2 files
Files
- picosat.cabal +4/−4
- src/Picosat.hs +20/−34
picosat.cabal view
@@ -1,5 +1,5 @@ name: picosat-version: 0.1.0.2+version: 0.1.1 synopsis: Bindings to the PicoSAT solver homepage: https://github.com/sdiehl/haskell-picosat license: MIT@@ -9,8 +9,8 @@ copyright: 2014 Stephen Diehl Category: Logic build-type: Simple-cabal-version: >=1.10-tested-with: GHC == 7.6.1+cabal-version: >=1.20+tested-with: GHC == 7.6.1, GHC == 7.6.3, GHC == 7.8.3 extra-source-files: cbits/picosat.h Bug-Reports: https://github.com/sdiehl/haskell-picosat/issues@@ -26,7 +26,7 @@ other-extensions: ForeignFunctionInterface - ghc-options: -Wall -fwarn-tabs+ ghc-options: -Wall -O2 -fwarn-tabs cc-options: -funroll-loops build-depends: base >=4.6 && <4.7 default-language: Haskell2010
src/Picosat.hs view
@@ -1,23 +1,17 @@ {-# LANGUAGE ForeignFunctionInterface #-}-{-# LANGUAGE UnicodeSyntax #-} - {- | We wish to find a solution that satisifes the following logical condition. -@-(A v ¬B v C) ∧ (B v D v E) ∧ (D v F)-@+> (A v ¬B v C) ∧ (B v D v E) ∧ (D v F) We can specify this as a zero-terminated lists of integers, with integers mapping onto the variable as ordered in the condition and with integer negation corresponding to logical negation of the specific clause. -@-1 -2 3 0-2 4 5 0-4 6 0-@+> 1 -2 3 0+> 2 4 5 0+> 4 6 0 We feed this list to the SAT solver using the 'solve' function either in IO or ST monad. @@ -51,44 +45,40 @@ -- [Solution [1,2],Solution [-1,2],Solution [1,-2]] @ +For a higher level interface see: <http://hackage.haskell.org/package/picologic>+ -} module Picosat ( solve,- solveST, solveAll,- solveAllST, unsafeSolve, unsafeSolveAll, Solution(..) ) where import Control.Monad- import System.IO.Unsafe (unsafePerformIO) -import Control.Monad.ST (ST)-import Control.Monad.ST.Unsafe (unsafeIOToST)- import Foreign.Ptr import Foreign.C.Types -foreign import ccall safe "picosat_init" picosat_init+foreign import ccall unsafe "picosat_init" picosat_init :: IO (Ptr a) -foreign import ccall safe "picosat_reset" picosat_reset+foreign import ccall unsafe "picosat_reset" picosat_reset :: Ptr a -> IO () -foreign import ccall safe "picosat_add" picosat_add+foreign import ccall unsafe "picosat_add" picosat_add :: Ptr a -> CInt -> IO CInt -foreign import ccall safe "picosat_variables" picosat_variables+foreign import ccall unsafe "picosat_variables" picosat_variables :: Ptr a -> IO CInt -foreign import ccall safe "picosat_sat" picosat_sat+foreign import ccall unsafe "picosat_sat" picosat_sat :: Ptr a -> CInt -> IO CInt -foreign import ccall safe "picosat_deref" picosat_deref+foreign import ccall unsafe "picosat_deref" picosat_deref :: Ptr a -> CInt -> IO CInt unknown, satisfiable, unsatisfiable :: CInt@@ -123,10 +113,11 @@ | a == satisfiable -> getSolution pico | otherwise -> error "Picosat error." -toCInts :: Integral a => [[a]] -> [[CInt]]+toCInts :: [[Int]] -> [[CInt]] toCInts = map $ map fromIntegral -solve :: Integral a => [[a]] -> IO Solution+-- | Solve a list of CNF constraints yielding the first solution.+solve :: [[Int]] -> IO Solution solve cls = do let ccls = toCInts cls pico <- picosat_init@@ -135,7 +126,8 @@ picosat_reset pico return sol -solveAll :: Integral a => [[a]] -> IO [Solution]+-- | Solve a list of CNF constraints yielding all possible solutions.+solveAll :: [[Int]] -> IO [Solution] solveAll e = do let e' = map (map fromIntegral) e s <- solve e'@@ -143,18 +135,12 @@ Solution x -> (Solution x :) `fmap` solveAll (map negate x : e') _ -> return [] -{-# NOINLINE solveST #-}-solveST :: Integral a => [[a]] -> ST t Solution-solveST = unsafeIOToST . solve--{-# NOINLINE solveAllST #-}-solveAllST :: [[Int]] -> ST t [Solution]-solveAllST = unsafeIOToST . solveAll+-- Unsafe solver functions are not guaranteed to be memory safe if the solver fails internally. {-# NOINLINE unsafeSolve #-}-unsafeSolve :: Integral a => [[a]] -> Solution+unsafeSolve :: [[Int]] -> Solution unsafeSolve = unsafePerformIO . solve {-# NOINLINE unsafeSolveAll #-}-unsafeSolveAll :: Integral a => [[a]] -> [Solution]+unsafeSolveAll :: [[Int]] -> [Solution] unsafeSolveAll = unsafePerformIO . solveAll