Qlogic.SatSolver

Synopsis

• newtype SatSolver s l r = SatSolver (ErrorT SatError (StateT (State l) s) r)
• class Monad s => Solver s l | s -> l where
  • solve :: s Bool
  • run :: s a -> IO a
  • newLit :: s l
  • negate :: l -> s l
  • addClause :: Clause l -> s Bool
  • getModelValue :: l -> s Bool
• newtype Clause l = Clause {
  • clauseToList :: [l]
  }
• class Typeable a => Decoder e a | e -> a, a -> e where
  • extract :: PA -> Maybe a
  • add :: a -> e -> e
• data SatError
  • = Unsatisfiable
  • | AssertFailed
  • | OtherError String
• data a :&: b = a :&: b
• addFormula :: (Show l, Eq l, Solver s l) => PropFormula l -> SatSolver s l ()
• fix :: (Eq l, Solver s l) => l -> PropFormula l -> SatSolver s l ()
• value :: (Ord l, Decoder e a, Solver s l) => SatSolver s l () -> e -> IO (Either SatError e)
• assignment :: (Ord l, Solver s l) => SatSolver s l () -> IO (Either SatError (Assign l))
• checkFormula :: Solver s l => PropFormula l -> SatSolver s l ()
• freshLit :: Solver s l => SatSolver s l l
• getAssign :: (Ord l, Solver s l) => SatSolver s l (Assign l)
• runSolver :: Solver s l => SatSolver s l r -> IO (Either SatError r)
• liftS :: Solver s l => s r -> SatSolver s l r
• liftIO :: MonadIO m => forall a. IO a -> m a

Documentation