ToySolver.SAT.Types

Variable

type Var

type VarSet

type VarMap

validVar

Model

class IModel a

type Model

restrictModel

Literal

type Lit

type LitSet

type LitMap

litUndef

validLit

literal

litNot

litVar

litPolarity

evalLit

Clause

type Clause

normalizeClause

instantiateClause

clauseSubsume

evalClause

clauseToPBLinAtLeast

Cardinality Constraint

type AtLeast

type Exactly

normalizeAtLeast

instantiateAtLeast

evalAtLeast

evalExactly

(Linear) Pseudo Boolean Constraint

type PBLinTerm

type PBLinSum

type PBLinAtLeast

type PBLinExactly

normalizePBLinSum

normalizePBLinAtLeast

normalizePBLinExactly

instantiatePBLinAtLeast

instantiatePBLinExactly

cutResolve

cardinalityReduction

negatePBLinAtLeast

evalPBLinSum

evalPBLinAtLeast

evalPBLinExactly

pbLowerBound

pbUpperBound

pbSubsume

evalPBConstraint

Non-linear Pseudo Boolean constraint

type PBTerm

type PBSum

evalPBSum

XOR Clause

type XORClause

normalizeXORClause

instantiateXORClause

evalXORClause

Type classes for solvers

class NewVar m a

class AddClause m a

class AddCardinality m a

class AddPBLin m a

class AddPBNL m a

class AddXORClause m a