jukebox-0.4.2: A first-order reasoning toolbox

Safe HaskellNone
LanguageHaskell98

Jukebox.Sat

Documentation

data Solver #

Instances
SatSolver Solver Source # 
Instance details

Defined in Jukebox.Sat

Methods

getSolver :: Solver -> Solver Source #

newSolver :: IO Solver Source #

deleteSolver :: Solver -> IO () #

data Lit #

Instances
Eq Lit 
Instance details

Defined in MiniSat

Methods

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

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

Ord Lit 
Instance details

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 
Instance details

Defined in MiniSat

Methods

showsPrec :: Int -> Lit -> ShowS #

show :: Lit -> String #

showList :: [Lit] -> ShowS #

neg :: Lit -> Lit #

false :: Lit Source #

true :: Lit Source #

class SatSolver s where Source #

Minimal complete definition

getSolver

Methods

getSolver :: s -> Solver Source #

Instances
SatSolver Solver Source # 
Instance details

Defined in Jukebox.Sat

Methods

getSolver :: Solver -> Solver Source #

SatSolver SolverEq Source # 
Instance details

Defined in Jukebox.Sat.Equality

Methods

getSolver :: SolverEq -> 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 #