jukebox-0.1.4: A first-order reasoning toolbox

Safe HaskellNone
LanguageHaskell98

Jukebox.Sat

Documentation

data Solver :: *

Instances

newSolver :: IO Solver Source

deleteSolver :: Solver -> IO ()

data Lit :: *

Instances

neg :: Lit -> Lit

false :: Lit Source

true :: Lit Source

class SatSolver s where Source

Methods

getSolver :: s -> Solver Source

Instances

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