jukebox-0.3.5: A first-order reasoning toolbox

Safe HaskellNone
LanguageHaskell98

Jukebox.Sat.Equality

Documentation

class SatSolver s => EqSolver s where Source #

Minimal complete definition

getSolverEq

Methods

getSolverEq :: s -> SolverEq Source #

newtype Elt Source #

Constructors

Elt Int 

Instances

Eq Elt Source # 

Methods

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

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

Ord Elt Source # 

Methods

compare :: Elt -> Elt -> Ordering #

(<) :: Elt -> Elt -> Bool #

(<=) :: Elt -> Elt -> Bool #

(>) :: Elt -> Elt -> Bool #

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

max :: Elt -> Elt -> Elt #

min :: Elt -> Elt -> Elt #

Show Elt Source # 

Methods

showsPrec :: Int -> Elt -> ShowS #

show :: Elt -> String #

showList :: [Elt] -> ShowS #

newElt :: EqSolver s => s -> IO Elt Source #

equal :: EqSolver s => s -> Elt -> Elt -> IO Lit3 Source #

solveEq :: EqSolver s => s -> [Lit] -> IO Bool Source #

modelRep :: EqSolver s => s -> Elt -> IO (Maybe Elt) Source #