jukebox-0.1.6: A first-order reasoning toolbox

Safe Haskell	None
Language	Haskell98

Jukebox.SatEq

Documentation

data SolverEq Source

Constructors

SolverEq
Fields satSolver :: Solver counter :: IORef Int table :: IORef (Map (Elt, Elt) Lit3) model :: IORef (Maybe (Map Elt Elt))

Instances

SatSolver SolverEq Source
EqSolver SolverEq Source

newSolverEq :: Solver -> IO SolverEq Source

class SatSolver s => EqSolver s where Source

Methods

getSolverEq :: s -> SolverEq Source

Instances

EqSolver SolverEq Source

newtype Elt Source

Constructors

Instances

Eq Elt Source
Ord Elt Source
Show 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