MiniSat

Documentation

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

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

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

Constructors

MkSolver (Ptr ())

newtype Var

Constructors

MkVar CInt

Instances

Eq Var

Defined in MiniSat

Methods

(==) :: Var -> Var -> Bool

(/=) :: Var -> Var -> Bool

Ord Var

Defined in MiniSat

Methods

compare :: Var -> Var -> Ordering

(<) :: Var -> Var -> Bool

(<=) :: Var -> Var -> Bool

(>) :: Var -> Var -> Bool

(>=) :: Var -> Var -> Bool

max :: Var -> Var -> Var

min :: Var -> Var -> Var

Show Var

Defined in MiniSat

Methods

showsPrec :: Int -> Var -> ShowS

show :: Var -> String

showList :: [Var] -> ShowS

newtype Lit

Constructors

MkLit CInt

Instances

Eq Lit

Defined in MiniSat

Methods

(==) :: Lit -> Lit -> Bool

(/=) :: Lit -> Lit -> Bool

Ord Lit

Defined in MiniSat

Methods

compare :: Lit -> Lit -> Ordering

(<) :: Lit -> Lit -> Bool

(<=) :: Lit -> Lit -> Bool

(>) :: Lit -> Lit -> Bool

(>=) :: Lit -> Lit -> Bool

max :: Lit -> Lit -> Lit

min :: Lit -> Lit -> Lit

Show Lit

Defined in MiniSat

Methods

showsPrec :: Int -> Lit -> ShowS

show :: Lit -> String

showList :: [Lit] -> ShowS

newtype LBool

Constructors

MkLBool CInt

Instances

Eq LBool

Defined in MiniSat

Methods

(==) :: LBool -> LBool -> Bool

(/=) :: LBool -> LBool -> Bool

Ord LBool

Defined in MiniSat

Methods

compare :: LBool -> LBool -> Ordering

(<) :: LBool -> LBool -> Bool

(<=) :: LBool -> LBool -> Bool

(>) :: LBool -> LBool -> Bool

(>=) :: LBool -> LBool -> Bool

max :: LBool -> LBool -> LBool

min :: LBool -> LBool -> LBool

Show LBool

Defined in MiniSat

Methods

showsPrec :: Int -> LBool -> ShowS

show :: LBool -> String

showList :: [LBool] -> ShowS

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 ()