incremental-sat-solver 0.1.5 → 0.1.6

raw patch · 2 files changed

+22/−3 lines, 2 filesPVP ok

version bump matches the API change (PVP)

API changes (from Hackage documentation)

Files

• Data/Boolean.hs +21/−2
• incremental-sat-solver.cabal +1/−1

@@ -25,8 +25,11 @@    ) where -import Data.List ( nub )+import Data.Maybe ( mapMaybe )+import qualified Data.IntMap as IM +import Control.Monad ( guard, liftM )+ -- | Boolean formulas are represented as values of type @Boolean@. --  data Boolean@@ -78,7 +81,7 @@ --  booleanToCNF :: Boolean -> CNF booleanToCNF-  = map (nub . map literal . disjunction)+  = mapMaybe (simpleClause . map literal . disjunction)   . conjunction   . asLongAsPossible distribute   . asLongAsPossible pushNots@@ -110,6 +113,22 @@   -- private helper functions++-- remove duplicate literals from clauses and drop clauses that+-- contain one literal both positively and negatively.+--+simpleClause :: Clause -> Maybe Clause+simpleClause = liftM (map lit . IM.toList) . foldl add (Just IM.empty)+ where+  lit (x,True)  = Pos x+  lit (x,False) = Neg x++  add mm l = do+    m <- mm+    let x = literalVar l; kind = isPositiveLiteral l+    maybe (Just (IM.insert x kind m))+          (\b -> guard (b==kind) >> Just m)+          (IM.lookup x m)  conjunction :: Boolean -> [Boolean] conjunction b = flat b []

@@ -1,5 +1,5 @@ Name:          incremental-sat-solver-Version:       0.1.5+Version:       0.1.6 Cabal-Version: >= 1.6 Synopsis:      Simple, Incremental SAT Solving as a Library Description:   This Haskell library provides an implementation of the