jukebox-0.4.2: A first-order reasoning toolbox

Safe HaskellNone
LanguageHaskell98

Jukebox.Sat.Equality

Documentation

data SolverEq Source #

Constructors

SolverEq 
Instances
SatSolver SolverEq Source # 
Instance details

Defined in Jukebox.Sat.Equality

EqSolver SolverEq Source # 
Instance details

Defined in Jukebox.Sat.Equality

class SatSolver s => EqSolver s where Source #

Minimal complete definition

getSolverEq

Methods

getSolverEq :: s -> SolverEq Source #

Instances
EqSolver SolverEq Source # 
Instance details

Defined in Jukebox.Sat.Equality

newtype Elt Source #

Constructors

Elt Int 
Instances
Eq Elt Source # 
Instance details

Defined in Jukebox.Sat.Equality

Methods

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

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

Ord Elt Source # 
Instance details

Defined in Jukebox.Sat.Equality

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

Defined in Jukebox.Sat.Equality

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 #