jukebox-0.4.2: A first-order reasoning toolbox
Jukebox.Sat.Equality
data SolverEq Source #
Constructors
Fields
Defined in Jukebox.Sat.Equality
Methods
getSolver :: SolverEq -> Solver Source #
getSolverEq :: SolverEq -> SolverEq Source #
newSolverEq :: Solver -> IO SolverEq Source #
class SatSolver s => EqSolver s where Source #
Minimal complete definition
getSolverEq
getSolverEq :: s -> SolverEq Source #
newtype Elt Source #
(==) :: Elt -> Elt -> Bool #
(/=) :: Elt -> Elt -> Bool #
compare :: Elt -> Elt -> Ordering #
(<) :: Elt -> Elt -> Bool #
(<=) :: Elt -> Elt -> Bool #
(>) :: Elt -> Elt -> Bool #
(>=) :: Elt -> Elt -> Bool #
max :: Elt -> Elt -> Elt #
min :: Elt -> Elt -> Elt #
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 #