Jukebox.SatEq

Documentation

data SolverEq

Constructors

SolverEq

Fields

satSolver :: Solver

counter :: IORef Int

table :: IORef (Map (Elt, Elt) Lit3)

model :: IORef (Maybe (Map Elt Elt))

Instances

SatSolver SolverEq

EqSolver SolverEq

newSolverEq :: Solver -> IO SolverEq

class SatSolver s => EqSolver s where

Methods

getSolverEq :: s -> SolverEq

Instances

EqSolver SolverEq

newtype Elt

Constructors

Elt Int

Instances

Eq Elt

Ord Elt

Show Elt

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

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

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

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