incremental-sat-solver 0.1 → 0.1.1

raw patch · 3 files changed

+22/−20 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 +10/−8
• Data/Boolean/SatSolver.hs +11/−11
• incremental-sat-solver.cabal +1/−1

@@ -75,8 +75,8 @@ --  booleanToCNF :: Boolean -> CNF booleanToCNF-  = map (map literal . flatDisjunction)-  . flatConjunction+  = map (map literal . disjunction)+  . conjunction   . asLongAsPossible distribute   . asLongAsPossible pushNots   . asLongAsPossible elim@@ -108,14 +108,16 @@  -- private helper functions -flatConjunction :: Boolean -> [Boolean]-flatConjunction b = flat b []- where flat (x:&&:y) = flat x . flat y+conjunction :: Boolean -> [Boolean]+conjunction b = flat b []+ where flat Yes      = id+       flat (x:&&:y) = flat x . flat y        flat x        = (x:) -flatDisjunction :: Boolean -> [Boolean]-flatDisjunction b = flat b []- where flat (x:||:y) = flat x . flat y+disjunction :: Boolean -> [Boolean]+disjunction b = flat b []+ where flat No       = id+       flat (x:||:y) = flat x . flat y        flat x        = (x:)  asLongAsPossible :: (Boolean -> Maybe Boolean) -> Boolean -> Boolean

@@ -23,7 +23,7 @@    newSatSolver, isSolved,  -  lookupVar, assertTrue, branchOnVar, satisfy, selectBranchVar+  lookupVar, assertTrue, branchOnVar, selectBranchVar, solve    ) where @@ -76,22 +76,22 @@         (const (return solver))         (lookupVar name solver) --- | --- This function guesses values for variables such that the stored--- constraints are satisfied. The result may be non-deterministic and--- is, hence, returned in an instance of @MonadPlus@.--- -satisfy :: MonadPlus m => SatSolver -> m SatSolver-satisfy solver-  | isSolved solver = return solver-  | otherwise = branchOnUnbound (selectBranchVar solver) solver >>= satisfy- -- | -- We select a variable from the shortest clause hoping to produce a -- unit clause. -- selectBranchVar :: SatSolver -> Int selectBranchVar = literalVar . head . head . sortBy shorter . clauses++-- | +-- This function guesses values for variables such that the stored+-- constraints are satisfied. The result may be non-deterministic and+-- is, hence, returned in an instance of @MonadPlus@.+-- +solve :: MonadPlus m => SatSolver -> m SatSolver+solve solver+  | isSolved solver = return solver+  | otherwise = branchOnUnbound (selectBranchVar solver) solver >>= solve   -- private helper functions

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