Documentation

withNewSolverAsync :: (Solver -> IO a) -> IO a Source

withNewSolver :: (Solver -> IO a) -> IO a Source

newSolver :: IO Solver Source

deleteSolver :: Solver -> IO () Source

newLit :: Solver -> IO Lit Source

neg :: Lit -> Lit Source

addClause :: Solver -> [Lit] -> IO Bool Source

simplify :: Solver -> IO Bool Source

eliminate :: Solver -> Bool -> IO Bool Source

setFrozen :: Solver -> Var -> Bool -> IO () Source

isEliminated :: Solver -> Var -> IO Bool Source

solve :: Solver -> [Lit] -> IO Bool Source

limited_solve :: Solver -> [Lit] -> IO LBool Source

value :: Solver -> Lit -> IO (Maybe Bool) Source

modelValue :: Solver -> Lit -> IO (Maybe Bool) Source

conflict :: Solver -> IO [Lit] Source

l_True :: LBool Source

l_Undef :: LBool Source

l_False :: LBool Source

newtype Solver Source

newtype Var Source

newtype Lit Source

newtype LBool Source

minisat_new :: IO Solver Source

minisat_delete :: Solver -> IO () Source

minisat_newVar :: Solver -> IO Var Source

minisat_newLit :: Solver -> IO Lit Source

minisat_mkLit :: Var -> Lit Source

minisat_mkLit_args :: Var -> Int -> Lit Source

minisat_negate :: Lit -> Lit Source

minisat_var :: Lit -> Var Source

minisat_sign :: Lit -> Bool Source

minisat_addClause :: Solver -> Int -> Ptr Lit -> IO Bool Source

minisat_addClause_begin :: Solver -> IO () Source

minisat_addClause_addLit :: Solver -> Lit -> IO () Source

minisat_addClause_commit :: Solver -> IO Bool Source

minisat_simplify :: Solver -> IO Bool Source

minisat_solve :: Solver -> Int -> Ptr Lit -> IO Bool Source

minisat_solve_begin :: Solver -> IO () Source

minisat_solve_addLit :: Solver -> Lit -> IO () Source

minisat_solve_commit :: Solver -> IO Bool Source

minisat_limited_solve_commit :: Solver -> IO LBool Source

minisat_interrupt :: Solver -> IO () Source

minisat_clearInterrupt :: Solver -> IO () Source

minisat_okay :: Solver -> IO Bool Source

minisat_setPolarity :: Solver -> Var -> Int -> IO () Source

minisat_setDecisionVar :: Solver -> Var -> Int -> IO () Source

minisat_value_Var :: Solver -> Var -> IO LBool Source

minisat_value_Lit :: Solver -> Lit -> IO LBool Source

minisat_modelValue_Var :: Solver -> Var -> IO LBool Source

minisat_modelValue_Lit :: Solver -> Lit -> IO LBool Source

minisat_get_l_True :: LBool Source

minisat_get_l_False :: LBool Source

minisat_get_l_Undef :: LBool Source

minisat_setFrozen :: Solver -> Var -> Bool -> IO () Source

minisat_isEliminated :: Solver -> Var -> IO Bool Source

minisat_eliminate :: Solver -> Bool -> IO Bool Source

minisat_num_assigns :: Solver -> IO Int Source

minisat_num_clauses :: Solver -> IO Int Source

minisat_num_learnts :: Solver -> IO Int Source

minisat_num_vars :: Solver -> IO Int Source

minisat_num_freeVars :: Solver -> IO Int Source

minisat_num_conflicts :: Solver -> IO Int Source

minisat_conflict_len :: Solver -> IO Int Source

minisat_conflict_nthLit :: Solver -> Int -> IO Lit Source

minisat_set_verbosity :: Solver -> Int -> IO () Source