| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
MiniSat
Synopsis
- withNewSolverAsync :: (Solver -> IO a) -> IO a
- withNewSolver :: (Solver -> IO a) -> IO a
- newSolver :: IO Solver
- deleteSolver :: Solver -> IO ()
- newLit :: Solver -> IO Lit
- neg :: Lit -> Lit
- addClause :: Solver -> [Lit] -> IO Bool
- simplify :: Solver -> IO Bool
- eliminate :: Solver -> Bool -> IO Bool
- setFrozen :: Solver -> Var -> Bool -> IO ()
- isEliminated :: Solver -> Var -> IO Bool
- solve :: Solver -> [Lit] -> IO Bool
- limited_solve :: Solver -> [Lit] -> IO LBool
- value :: Solver -> Lit -> IO (Maybe Bool)
- modelValue :: Solver -> Lit -> IO (Maybe Bool)
- conflict :: Solver -> IO [Lit]
- l_True :: LBool
- l_False :: LBool
- l_Undef :: LBool
- newtype Solver = MkSolver (Ptr ())
- newtype Var = MkVar CInt
- newtype Lit = MkLit CInt
- newtype LBool = MkLBool CInt
- minisat_new :: IO Solver
- minisat_delete :: Solver -> IO ()
- minisat_newVar :: Solver -> IO Var
- minisat_newLit :: Solver -> IO Lit
- minisat_mkLit :: Var -> Lit
- minisat_mkLit_args :: Var -> Int -> Lit
- minisat_negate :: Lit -> Lit
- minisat_var :: Lit -> Var
- minisat_sign :: Lit -> Bool
- minisat_addClause :: Solver -> Int -> Ptr Lit -> IO Bool
- minisat_addClause_begin :: Solver -> IO ()
- minisat_addClause_addLit :: Solver -> Lit -> IO ()
- minisat_addClause_commit :: Solver -> IO Bool
- minisat_simplify :: Solver -> IO Bool
- minisat_solve :: Solver -> Int -> Ptr Lit -> IO Bool
- minisat_solve_begin :: Solver -> IO ()
- minisat_solve_addLit :: Solver -> Lit -> IO ()
- minisat_solve_commit :: Solver -> IO Bool
- minisat_limited_solve_commit :: Solver -> IO LBool
- minisat_interrupt :: Solver -> IO ()
- minisat_clearInterrupt :: Solver -> IO ()
- minisat_okay :: Solver -> IO Bool
- minisat_setPolarity :: Solver -> Var -> Int -> IO ()
- minisat_setDecisionVar :: Solver -> Var -> Int -> IO ()
- minisat_value_Var :: Solver -> Var -> IO LBool
- minisat_value_Lit :: Solver -> Lit -> IO LBool
- minisat_modelValue_Var :: Solver -> Var -> IO LBool
- minisat_modelValue_Lit :: Solver -> Lit -> IO LBool
- minisat_get_l_True :: LBool
- minisat_get_l_False :: LBool
- minisat_get_l_Undef :: LBool
- minisat_setFrozen :: Solver -> Var -> Bool -> IO ()
- minisat_isEliminated :: Solver -> Var -> IO Bool
- minisat_eliminate :: Solver -> Bool -> IO Bool
- minisat_num_assigns :: Solver -> IO Int
- minisat_num_clauses :: Solver -> IO Int
- minisat_num_learnts :: Solver -> IO Int
- minisat_num_vars :: Solver -> IO Int
- minisat_num_freeVars :: Solver -> IO Int
- minisat_num_conflicts :: Solver -> IO Int
- minisat_conflict_len :: Solver -> IO Int
- minisat_conflict_nthLit :: Solver -> Int -> IO Lit
- minisat_set_verbosity :: Solver -> Int -> IO ()
Documentation
withNewSolverAsync :: (Solver -> IO a) -> IO a Source #
Run a minisat instance in such a way that it is interruptable (by sending killThread). cf. https://github.com/niklasso/minisat-haskell-bindings/issues/1
deleteSolver :: Solver -> IO () Source #
minisat_new :: IO Solver Source #
minisat_delete :: Solver -> IO () Source #
minisat_mkLit :: Var -> Lit Source #
minisat_negate :: Lit -> Lit Source #
minisat_var :: Lit -> Var Source #
minisat_sign :: Lit -> Bool Source #
minisat_addClause_begin :: Solver -> IO () Source #
minisat_solve_begin :: Solver -> IO () Source #
minisat_interrupt :: Solver -> IO () Source #
minisat_clearInterrupt :: Solver -> IO () Source #