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

addClause

type Clause

evalClause

Cardinality constraints

addAtLeast

addAtMost

addExactly

type AtLeast

type Exactly

evalAtLeast

evalExactly

(Linear) pseudo-boolean constraints

addPBAtLeast

addPBAtMost

addPBExactly

addPBAtLeastSoft

addPBAtMostSoft

addPBExactlySoft

type PBLinTerm

type PBLinSum

type PBLinAtLeast

type PBLinExactly

evalPBLinSum

evalPBLinAtLeast

evalPBLinExactly

XOR clauses

addXORClause

addXORClauseSoft

type XORClause

evalXORClause

Thery

setTheory

Solving

solve

solveWith

data BudgetExceeded

Extract results

class IModel a

type Model

getModel

getFailedAssumptions

getAssumptionsImplications

Solver configulation

data Config

getConfig

setConfig

modifyConfig

data RestartStrategy

data LearningStrategy

setVarPolarity

setLogger

setRandomGen

getRandomGen

setConfBudget

data PBHandlerType

Deprecated

setRestartStrategy

setRestartFirst

defaultRestartFirst

setRestartInc

defaultRestartInc

setLearntSizeFirst

defaultLearntSizeFirst

setLearntSizeInc

defaultLearntSizeInc

setCCMin

defaultCCMin

setLearningStrategy

setEnablePhaseSaving

getEnablePhaseSaving

defaultEnablePhaseSaving

setEnableForwardSubsumptionRemoval

getEnableForwardSubsumptionRemoval

defaultEnableForwardSubsumptionRemoval

setEnableBackwardSubsumptionRemoval

getEnableBackwardSubsumptionRemoval

defaultEnableBackwardSubsumptionRemoval

setCheckModel

setRandomFreq

defaultRandomFreq

setPBHandlerType

setPBSplitClausePart

getPBSplitClausePart

defaultPBSplitClausePart

Read state

getNVars

getNConstraints

getNLearntConstraints

getVarFixed

getLitFixed

getFixedLiterals

Read state (deprecated)

nVars

nAssigns

nConstraints

nLearnt

Internal API

varBumpActivity

varDecayActivity