picosat 0.1.0.1 → 0.1.0.2

raw patch · 2 files changed

+69/−10 lines, 2 files

Files

• picosat.cabal +9/−8
• src/Picosat.hs +60/−2

@@ -1,15 +1,16 @@ name:                picosat-version:             0.1.0.1+version:             0.1.0.2 synopsis:            Bindings to the PicoSAT solver homepage:            https://github.com/sdiehl/haskell-picosat license:             MIT license-file:        LICENSE author:              Stephen Diehl maintainer:          stephen.m.diehl@gmail.com-copyright:           2012 Stephen Diehl+copyright:           2014 Stephen Diehl Category:            Logic build-type:          Simple cabal-version:       >=1.10+tested-with:         GHC == 7.6.1 extra-source-files:     cbits/picosat.h Bug-Reports:         https://github.com/sdiehl/haskell-picosat/issues@@ -25,12 +26,12 @@   other-extensions:     ForeignFunctionInterface -  Cc-options:          -  Ghc-options:        -Wall-  build-depends:       base >=4.6 && <4.7-  default-language:    Haskell2010-  Hs-source-dirs:      src-  Include-dirs:        cbits+  ghc-options:        -Wall -fwarn-tabs+  cc-options:         -funroll-loops+  build-depends:      base >=4.6 && <4.7+  default-language:   Haskell2010+  Hs-source-dirs:     src+  Include-dirs:       cbits    C-sources:     cbits/picosat.c

@@ -1,9 +1,27 @@ {-# LANGUAGE ForeignFunctionInterface #-}+{-# LANGUAGE UnicodeSyntax #-} -{- | The solve function takes a nested list of integers representing variables in clauses and returns the-   solution. Usage: +{- |++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)+@++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+@++We feed this list to the SAT solver using the 'solve' function either in IO or ST monad.++@ import Picosat  main :: IO [Int]@@ -12,12 +30,36 @@   -- Solution [1,-2,3,4,5,6] @ +The solution given we can interpret as:++>  1  A+> -2 ~B+>  3  C+>  4  D+>  5  E+>  6  F++To generate all satisfiable solutions, use 'solveAll' function.:++@+import Picosat+import Control.Monad.ST++main :: [Int]+main = runST $ do+  solveAllST [[1,2]]+  -- [Solution [1,2],Solution [-1,2],Solution [1,-2]]+@+ -}  module Picosat (   solve,   solveST,+  solveAll,+  solveAllST,   unsafeSolve,+  unsafeSolveAll,   Solution(..) ) where @@ -93,10 +135,26 @@   picosat_reset pico   return sol +solveAll :: Integral a => [[a]] -> IO [Solution]+solveAll e = do+  let e' = map (map fromIntegral) e+  s <- solve e'+  case s of+      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+ {-# NOINLINE unsafeSolve #-} unsafeSolve :: Integral a => [[a]] -> Solution unsafeSolve = unsafePerformIO . solve++{-# NOINLINE unsafeSolveAll #-}+unsafeSolveAll :: Integral a => [[a]] -> [Solution]+unsafeSolveAll = unsafePerformIO . solveAll