jukebox-0.1.2: A first-order reasoning toolbox
Jukebox.Sat
data Solver
Instances
newSolver :: IO SolverSource
deleteSolver :: Solver -> IO ()
data Lit
neg :: Lit -> Lit
false :: LitSource
true :: LitSource
class SatSolver s whereSource
Methods
getSolver :: s -> SolverSource
newLit :: SatSolver s => s -> IO LitSource
addClause :: SatSolver s => s -> [Lit] -> IO ()Source
solve :: SatSolver s => s -> [Lit] -> IO BoolSource
conflict :: SatSolver s => s -> IO [Lit]Source
modelValue :: SatSolver s => s -> Lit -> IO (Maybe Bool)Source
value :: SatSolver s => s -> Lit -> IO (Maybe Bool)Source