jukebox-0.1.4: A first-order reasoning toolbox
Jukebox.SatEq
data SolverEq Source
Constructors
Fields
Instances
newSolverEq :: Solver -> IO SolverEq Source
class SatSolver s => EqSolver s where Source
Methods
getSolverEq :: s -> SolverEq Source
newtype Elt Source
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