Jukebox.Sat.Equality

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

Defined in Jukebox.Sat.Equality

Methods

getSolver :: SolverEq -> Solver

EqSolver SolverEq

Defined in Jukebox.Sat.Equality

Methods

getSolverEq :: SolverEq -> SolverEq

newSolverEq :: Solver -> IO SolverEq

class SatSolver s => EqSolver s where

Minimal complete definition

getSolverEq

Methods

getSolverEq :: s -> SolverEq

Instances

EqSolver SolverEq

Defined in Jukebox.Sat.Equality

Methods

getSolverEq :: SolverEq -> SolverEq

newtype Elt

Constructors

Elt Int

Instances

Eq Elt

Defined in Jukebox.Sat.Equality

Methods

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

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

Ord Elt

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

Defined in Jukebox.Sat.Equality

Methods

showsPrec :: Int -> Elt -> ShowS

show :: Elt -> String

showList :: [Elt] -> ShowS

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)