funsat-0.5: A modern DPLL-style SAT solverSource codeContentsIndex
Funsat.Types
Contents
Basic Types
Assignments
Model
Helpers
Description
Data types used when dealing with SAT problems in funsat.
Synopsis
newtype Var = V {
unVar :: Int
}
newtype Lit = L {
unLit :: Int
}
litSign :: Lit -> Bool
var :: Lit -> Var
type Clause = [Lit]
data GenCNF a = CNF {
numVars :: Int
numClauses :: Int
clauses :: Set a
}
type CNF = GenCNF 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]
class Model a m where
statusUnder :: a -> m -> Either () Bool
isUndefUnder :: Model a m => a -> m -> Bool
isTrueUnder :: Model a m => a -> m -> Bool
isFalseUnder :: Model a m => a -> m -> Bool
isUnitUnder :: Model a m => [a] -> m -> Bool
getUnit :: (Model a m, Show a) => [a] -> m -> a
Basic Types
newtype Var Source
Constructors
V
unVar :: Int
show/hide Instances
newtype Lit Source
Constructors
L
unLit :: Int
show/hide Instances
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 GenCNF a Source
''Generic'' conjunctive normal form. It's ''generic'' because the elements of the clause set are polymorphic. And they are polymorphic so that I can easily get a Foldable instance.
Constructors
CNF
numVars :: Int
numClauses :: Int
clauses :: Set a
show/hide Instances
Foldable GenCNF
Eq a => Eq (GenCNF a)
(Ord a, Read a) => Read (GenCNF a)
Show a => Show (GenCNF a)
type CNF = GenCNF ClauseSource
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 (Set a) a
(Ord a, Hash a) => Setlike (BitSet a) 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.
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
isUndefUnder :: Model a m => a -> m -> BoolSource
True if and only if the object is undefined in the model.
isTrueUnder :: Model a m => a -> m -> BoolSource
True if and only if the object is true in the model.
isFalseUnder :: Model a m => a -> m -> BoolSource
True if and only if the object is false in the model.
Helpers
isUnitUnder :: Model a m => [a] -> m -> BoolSource
Whether all the elements of the model in the list are false but one, and none is true, under the model.
getUnit :: (Model a m, Show a) => [a] -> m -> aSource
Get the element of the list which is not false under the model. If no such element, throws an error.
Produced by Haddock version 2.1.0