Jukebox.Sat

Documentation

data Solver

Instances

SatSolver Solver

Defined in Jukebox.Sat

Methods

getSolver :: Solver -> Solver

newSolver :: IO Solver

deleteSolver :: Solver -> IO ()

data Lit

Instances

Eq Lit

Defined in MiniSat

Methods

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

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

Ord Lit

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

Defined in MiniSat

Methods

showsPrec :: Int -> Lit -> ShowS

show :: Lit -> String

showList :: [Lit] -> ShowS

neg :: Lit -> Lit

false :: Lit

true :: Lit

class SatSolver s where

Minimal complete definition

getSolver

Methods

getSolver :: s -> Solver

Instances

SatSolver Solver

Defined in Jukebox.Sat

Methods

getSolver :: Solver -> Solver

SatSolver SolverEq

Defined in Jukebox.Sat.Equality

Methods

getSolver :: SolverEq -> Solver

newLit :: SatSolver s => s -> IO Lit

addClause :: SatSolver s => s -> [Lit] -> IO ()

solve :: SatSolver s => s -> [Lit] -> IO Bool

conflict :: SatSolver s => s -> IO [Lit]

modelValue :: SatSolver s => s -> Lit -> IO (Maybe Bool)

value :: SatSolver s => s -> Lit -> IO (Maybe Bool)