ToySolver.SAT

The Solver type

data Solver

newSolver

Basic data structures

type Var

type Lit

literal

litNot

litVar

litPolarity

type Clause

Problem specification

newVar

newVars

newVars_

resizeVarCapacity

addClause

addAtLeast

addAtMost

addExactly

addPBAtLeast

addPBAtMost

addPBExactly

addPBAtLeastSoft

addPBAtMostSoft

addPBExactlySoft

addXORClause

addXORClauseSoft

Solving

solve

solveWith

data BudgetExceeded

Extract results

type Model

getModel

getFailedAssumptions

Solver configulation

data RestartStrategy

setRestartStrategy

defaultRestartStrategy

setRestartFirst

defaultRestartFirst

setRestartInc

defaultRestartInc

setLearntSizeFirst

defaultLearntSizeFirst

setLearntSizeInc

defaultLearntSizeInc

setCCMin

defaultCCMin

data LearningStrategy

setLearningStrategy

defaultLearningStrategy

setEnablePhaseSaving

getEnablePhaseSaving

defaultEnablePhaseSaving

setEnableForwardSubsumptionRemoval

getEnableForwardSubsumptionRemoval

defaultEnableForwardSubsumptionRemoval

setEnableBackwardSubsumptionRemoval

getEnableBackwardSubsumptionRemoval

defaultEnableBackwardSubsumptionRemoval

setVarPolarity

setLogger

setCheckModel

setRandomFreq

defaultRandomFreq

setRandomGen

getRandomGen

setConfBudget

data PBHandlerType

setPBHandlerType

defaultPBHandlerType

Read state

nVars

nAssigns

nConstraints

nLearnt

getVarFixed

getLitFixed

Internal API

varBumpActivity

varDecayActivity