incremental-sat-solver 0.1.6 → 0.1.7

raw patch · 3 files changed

+22/−4 lines, 3 filesPVP: major bump suggested

API removals or changes: PVP suggests a major version bump

API changes (from Hackage documentation)

Files

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

@@ -21,7 +21,7 @@    Literal(..), literalVar, invLiteral, isPositiveLiteral,  -  CNF, booleanToCNF+  CNF, Clause, booleanToCNF    ) where 

@@ -62,8 +62,11 @@ -- assertion may fail if the resulting constraints are unsatisfiable. --  assertTrue :: MonadPlus m => Boolean -> SatSolver -> m SatSolver-assertTrue formula solver =-  simplify (solver { clauses = booleanToCNF formula ++ clauses solver })+assertTrue formula solver = do+  newClauses <- foldl (addClause (bindings solver))+                      (return (clauses solver))+                      (booleanToCNF formula)+  simplify (solver { clauses = newClauses })  -- | -- This function guesses a value for the given variable, if it is@@ -104,6 +107,21 @@   -- private helper functions++addClause :: MonadPlus m => IM.IntMap Bool -> m [Clause] -> Clause -> m [Clause]+addClause binds mclauses newClause = do+  oldClauses <- mclauses+  let unboundLits = foldl (addUnbound binds) (Just []) newClause+  maybe (return oldClauses)+        (\lits -> guard (not (null lits)) >> return (lits:oldClauses))+        unboundLits++addUnbound :: IM.IntMap Bool -> Maybe Clause -> Literal -> Maybe Clause+addUnbound binds mlits lit = do+  lits <- mlits+  maybe (Just (lit:lits))+        (\b -> guard (b /= isPositiveLiteral lit) >> return lits)+        (IM.lookup (literalVar lit) binds)  updateSolver :: MonadPlus m => CNF -> [(Int,Bool)] -> SatSolver -> m SatSolver updateSolver cs bs solver = do

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