SAT.CAMUS

Description

Synopsis

• type MUS = [Lit]
• type MCS = [Lit]
• data Options = Options {
  • optLogger :: String -> IO ()
  • optCallback :: MCS -> IO ()
  }
• defaultOptions :: Options
• allMCSAssumptions :: Solver -> [Lit] -> Options -> IO [MCS]
• allMUSAssumptions :: Solver -> [Lit] -> Options -> IO [MCS]
• enumMCSAssumptions :: Solver -> [Lit] -> Options -> IO ()
• hittingSetDual :: [MCS] -> [MUS]

Documentation