| Copyright | (c) Masahiro Sakai 2012 |
|---|---|
| License | BSD-style |
| Maintainer | masahiro.sakai@gmail.com |
| Stability | provisional |
| Portability | non-portable |
| Safe Haskell | None |
| Language | Haskell2010 |
ToySolver.SAT.MUS
Description
Minimal Unsatifiable Subset (MUS) Finder
- module ToySolver.SAT.MUS.Types
- data Options = Options {
- optLogger :: String -> IO ()
- optUpdateBest :: [Lit] -> IO ()
- optLitPrinter :: Lit -> String
- defaultOptions :: Options
- findMUSAssumptions :: Solver -> Options -> IO MUS
Documentation
module ToySolver.SAT.MUS.Types
Options for findMUSAssumptions function
Constructors
| Options | |
Fields
| |
defaultOptions :: Options Source
default Options value
findMUSAssumptions :: Solver -> Options -> IO MUS Source
Find a minimal set of assumptions that causes a conflict.
Initial set of assumptions is taken from getFailedAssumptions.