ToySolver.SAT.Encoder.Cardinality

Documentation

data Encoder m

Instances

PrimMonad m => AddCardinality m (Encoder m)

Defined in ToySolver.SAT.Encoder.Cardinality

Methods

addAtLeast :: Encoder m -> [Lit] -> Int -> m ()

addAtMost :: Encoder m -> [Lit] -> Int -> m ()

addExactly :: Encoder m -> [Lit] -> Int -> m ()

Monad m => AddClause m (Encoder m)

Defined in ToySolver.SAT.Encoder.Cardinality

Methods

addClause :: Encoder m -> Clause -> m ()

Monad m => NewVar m (Encoder m)

Defined in ToySolver.SAT.Encoder.Cardinality

Methods

newVar :: Encoder m -> m Var

newVars :: Encoder m -> Int -> m [Var]

newVars_ :: Encoder m -> Int -> m ()

data Strategy

Constructors

Naive

ParallelCounter

Instances

Bounded Strategy

Defined in ToySolver.SAT.Encoder.Cardinality

Methods

minBound :: Strategy

maxBound :: Strategy

Enum Strategy

Defined in ToySolver.SAT.Encoder.Cardinality

Methods

succ :: Strategy -> Strategy

pred :: Strategy -> Strategy

toEnum :: Int -> Strategy

fromEnum :: Strategy -> Int

enumFrom :: Strategy -> [Strategy]

enumFromThen :: Strategy -> Strategy -> [Strategy]

enumFromTo :: Strategy -> Strategy -> [Strategy]

enumFromThenTo :: Strategy -> Strategy -> Strategy -> [Strategy]

Eq Strategy

Defined in ToySolver.SAT.Encoder.Cardinality

Methods

(==) :: Strategy -> Strategy -> Bool

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

Ord Strategy

Defined in ToySolver.SAT.Encoder.Cardinality

Methods

compare :: Strategy -> Strategy -> Ordering

(<) :: Strategy -> Strategy -> Bool

(<=) :: Strategy -> Strategy -> Bool

(>) :: Strategy -> Strategy -> Bool

(>=) :: Strategy -> Strategy -> Bool

max :: Strategy -> Strategy -> Strategy

min :: Strategy -> Strategy -> Strategy

Show Strategy

Defined in ToySolver.SAT.Encoder.Cardinality

Methods

showsPrec :: Int -> Strategy -> ShowS

show :: Strategy -> String

showList :: [Strategy] -> ShowS

newEncoder :: Monad m => Encoder m -> m (Encoder m)

newEncoderWithStrategy :: Monad m => Encoder m -> Strategy -> m (Encoder m)

encodeAtLeast :: PrimMonad m => Encoder m -> AtLeast -> m Lit