jukebox-0.1.2: A first-order reasoning toolbox

Safe HaskellNone

Jukebox.Sat

Documentation

data Solver

Instances

newSolver :: IO SolverSource

deleteSolver :: Solver -> IO ()

data Lit

Instances

Eq Lit 
Ord Lit 
Show Lit 

neg :: Lit -> Lit

false :: LitSource

true :: LitSource

class SatSolver s whereSource

Methods

getSolver :: s -> SolverSource

Instances

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