funsat-0.5.1: A modern DPLL-style SAT solverSource codeContentsIndex
Funsat.Types
Contents
Basic Types
Assignments
Model
Internal data types
Description
Data types used when dealing with SAT problems in funsat.
Synopsis
newtype Var = V {
unVar :: Int
}
newtype Lit = L {
unLit :: Int
}
inLit :: (Int -> Int) -> Lit -> Lit
litSign :: Lit -> Bool
var :: Lit -> Var
type Clause = [Lit]
data CNF = CNF {
numVars :: Int
numClauses :: Int
clauses :: Set Clause
}
class Ord a => Setlike t a where
without :: t -> a -> t
with :: t -> a -> t
contains :: t -> a -> Bool
type IAssignment = UArray Var Int
type MAssignment s = STUArray s Var Int
freezeAss :: MAssignment s -> ST s IAssignment
unsafeFreezeAss :: MonadST s m => MAssignment s -> m IAssignment
thawAss :: IAssignment -> ST s (MAssignment s)
unsafeThawAss :: IAssignment -> ST s (MAssignment s)
assign :: MAssignment s -> Lit -> ST s (MAssignment s)
unassign :: MAssignment s -> Lit -> ST s (MAssignment s)
litAssignment :: IAssignment -> [Lit]
data Cut f gr a b = Cut {
reasonSide :: f Node
conflictSide :: f Node
cutUIP :: Node
cutGraph :: gr a b
}
data CGNodeAnnot = CGNA Lit Int
class Model a m where
statusUnder :: a -> m -> Either () Bool
type Level = Int
type LevelArray s = STUArray s Var Level
type FrozenLevelArray = UArray Var Level
newtype VarOrder s = VarOrder {
varOrderArr :: STUArray s Var Double
}
newtype FrozenVarOrder = FrozenVarOrder (UArray Var Double)
type WatchedPair s = (STRef s (Lit, Lit), Clause, ClauseId)
type WatchArray s = STArray s Lit [WatchedPair s]
data PartialResolutionTrace = PartialResolutionTrace {
resTraceIdCount :: !Int
resTrace :: ![Int]
resTraceOriginalSingles :: ![(Clause, ClauseId)]
resSourceMap :: Map ClauseId [ClauseId]
}
type ReasonMap = Map Var (Clause, ClauseId)
type ClauseId = Int
Basic Types
newtype Var Source
Constructors
V
unVar :: Int
show/hide Instances
newtype Lit Source
Constructors
L
unLit :: Int
show/hide Instances
inLit :: (Int -> Int) -> Lit -> LitSource
litSign :: Lit -> BoolSource
The polarity of the literal. Negative literals are false; positive literals are true. The 0-literal is an error.
var :: Lit -> VarSource
The variable for the given literal.
type Clause = [Lit]Source
data CNF Source
Constructors
CNF
numVars :: Int
numClauses :: Int
clauses :: Set Clause
show/hide Instances
class Ord a => Setlike t a whereSource

Represents a container of type t storing elements of type a that support membership, insertion, and deletion.

There are various data structures used in funsat which are essentially used as ''set-like'' objects. I've distilled their interface into three methods. These methods are used extensively in the implementation of the solver.

Methods
without :: t -> a -> tSource
The set-like object with an element removed.
with :: t -> a -> tSource
The set-like object with an element included.
contains :: t -> a -> BoolSource
Whether the set-like object contains a certain element.
show/hide Instances
Setlike IAssignment Lit
Setlike IAssignment Lit
Ord a => Setlike ([] a) a
(Ord a, Hash a) => Setlike (BitSet a) a
Ord a => Setlike (Set a) a
(Ord k, Ord a) => Setlike (Map k a) ((,) k a)
(Ord k, Ord a) => Setlike (Map k a) ((,) k a)
Assignments
type IAssignment = UArray Var IntSource

An ''immutable assignment''. Stores the current assignment according to the following convention. A literal L i is in the assignment if in location (abs i) in the array, i is present. Literal L i is absent if in location (abs i) there is 0. It is an error if the location (abs i) is any value other than 0 or i or negate i.

Note that the Model instance for Lit and IAssignment takes constant time to execute because of this representation for assignments. Also updating an assignment with newly-assigned literals takes constant time, and can be done destructively, but safely.

type MAssignment s = STUArray s Var IntSource
Mutable array corresponding to the IAssignment representation.
freezeAss :: MAssignment s -> ST s IAssignmentSource
Same as freeze, but at the right type so GHC doesn't yell at me.
unsafeFreezeAss :: MonadST s m => MAssignment s -> m IAssignmentSource
See freezeAss.
thawAss :: IAssignment -> ST s (MAssignment s)Source
unsafeThawAss :: IAssignment -> ST s (MAssignment s)Source
assign :: MAssignment s -> Lit -> ST s (MAssignment s)Source
Destructively update the assignment with the given literal.
unassign :: MAssignment s -> Lit -> ST s (MAssignment s)Source
Destructively undo the assignment to the given literal.
litAssignment :: IAssignment -> [Lit]Source
The assignment as a list of signed literals.
data Cut f gr a b Source
The union of the reason side and the conflict side are all the nodes in the cutGraph (excepting, perhaps, the nodes on the reason side at decision level 0, which should never be present in a learned clause).
Constructors
Cut
reasonSide :: f NodeThe reason side contains at least the decision variables.
conflictSide :: f NodeThe conflict side contains the conflicting literal.
cutUIP :: Node
cutGraph :: gr a b
show/hide Instances
(Show (f Node), Show (gr a b)) => Show (Cut f gr a b)
data CGNodeAnnot Source
Annotate each variable in the conflict graph with literal (indicating its assignment) and decision level. The only reason we make a new datatype for this is for its Show instance.
Constructors
CGNA Lit Int
show/hide Instances
Model
class Model a m whereSource

An instance of this class is able to answer the question, Is a truth-functional object x true under the model m? Or is m a model for x? There are three possible answers for this question: True (''the object is true under m''), False (''the object is false under m''), and undefined, meaning its status is uncertain or unknown (as is the case with a partial assignment).

The only method in this class is so named so it reads well when used infix. Also see: isTrueUnder, isFalseUnder, isUndefUnder.

Methods
statusUnder :: a -> m -> Either () BoolSource
x `statusUnder` m should use Right if the status of x is defined, and Left otherwise.
show/hide Instances
Internal data types
type Level = IntSource
type LevelArray s = STUArray s Var LevelSource

A level array maintains a record of the decision level of each variable in the solver. If level is such an array, then level[i] == j means the decision level for var number i is j. j must be non-negative when the level is defined, and noLevel otherwise.

Whenever an assignment of variable v is made at decision level i, level[unVar v] is set to i.

type FrozenLevelArray = UArray Var LevelSource
Immutable version.
newtype VarOrder s Source
The VSIDS-like dynamic variable ordering.
Constructors
VarOrder
varOrderArr :: STUArray s Var Double
show/hide Instances
newtype FrozenVarOrder Source
Constructors
FrozenVarOrder (UArray Var Double)
show/hide Instances
type WatchedPair s = (STRef s (Lit, Lit), Clause, ClauseId)Source
Each pair of watched literals is paired with its clause and id.
type WatchArray s = STArray s Lit [WatchedPair s]Source
data PartialResolutionTrace Source
Constructors
PartialResolutionTrace
resTraceIdCount :: !Int
resTrace :: ![Int]
resTraceOriginalSingles :: ![(Clause, ClauseId)]
resSourceMap :: Map ClauseId [ClauseId]
show/hide Instances
type ReasonMap = Map Var (Clause, ClauseId)Source
type ClauseId = IntSource
Produced by Haddock version 2.3.0