ToySolver.SAT

The Solver type

data Solver

newSolver

newSolverWithConfig

Basic data structures

type Var

type Lit

literal

litNot

litVar

litPolarity

evalLit

Problem specification

newVar

newVars

newVars_

resizeVarCapacity

Clauses

class AddClause m a

type Clause

evalClause

Cardinality constraints

class AddCardinality m a

type AtLeast

type Exactly

evalAtLeast

evalExactly

(Linear) pseudo-boolean constraints

class AddPBLin m a

type PBLinTerm

type PBLinSum

type PBLinAtLeast

type PBLinExactly

evalPBLinSum

evalPBLinAtLeast

evalPBLinExactly

XOR clauses

class AddXORClause m a

type XORClause

evalXORClause

Theory

setTheory

Solving

solve

solveWith

data BudgetExceeded

cancel

data Canceled

Extract results

class IModel a

type Model

getModel

getFailedAssumptions

getAssumptionsImplications

Solver configulation

getConfig

setConfig

modifyConfig

setVarPolarity

setLogger

setRandomGen

getRandomGen

setConfBudget

Deprecated

setRestartStrategy

setRestartFirst

setRestartInc

setLearntSizeFirst

setLearntSizeInc

setCCMin

setLearningStrategy

setEnablePhaseSaving

getEnablePhaseSaving

setEnableForwardSubsumptionRemoval

getEnableForwardSubsumptionRemoval

setEnableBackwardSubsumptionRemoval

getEnableBackwardSubsumptionRemoval

setCheckModel

setRandomFreq

setPBHandlerType

setPBSplitClausePart

getPBSplitClausePart

Read state

getNVars

getNConstraints

getNLearntConstraints

getVarFixed

getLitFixed

getFixedLiterals

Read state (deprecated)

nVars

nAssigns

nConstraints

nLearnt

Internal API

varBumpActivity

varDecayActivity