jukebox-0.2.6: A first-order reasoning toolbox
Jukebox.Sat
data Solver :: *
Instances
newSolver :: IO Solver Source
deleteSolver :: Solver -> IO ()
data Lit :: *
neg :: Lit -> Lit
false :: Lit Source
true :: Lit Source
class SatSolver s where Source
Methods
getSolver :: s -> Solver Source
newLit :: SatSolver s => s -> IO Lit Source
addClause :: SatSolver s => s -> [Lit] -> IO () Source
solve :: SatSolver s => s -> [Lit] -> IO Bool Source
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