|
|
|
|
|
Description |
Data types used when dealing with SAT problems in funsat.
|
|
Synopsis |
|
|
|
|
Basic Types
|
|
|
Constructors | | Instances | |
|
|
|
Constructors | | Instances | |
|
|
|
The polarity of the literal. Negative literals are false; positive
literals are true. The 0-literal is an error.
|
|
|
The variable for the given literal.
|
|
|
|
|
''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 | |
|
| Instances | |
|
|
|
|
|
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 | | The set-like object with an element removed.
| | | The set-like object with an element included.
| | | Whether the set-like object contains a certain element.
|
| | Instances | |
|
|
Assignments
|
|
|
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.
|
|
|
Mutable array corresponding to the IAssignment representation.
|
|
|
Same as freeze, but at the right type so GHC doesn't yell at me.
|
|
|
See freezeAss.
|
|
|
|
|
|
|
Destructively update the assignment with the given literal.
|
|
|
Destructively undo the assignment to the given literal.
|
|
|
The assignment as a list of signed literals.
|
|
Model
|
|
|
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 | | x `statusUnder` m should use Right if the status of x is
defined, and Left otherwise.
|
| | Instances | |
|
|
|
True if and only if the object is undefined in the model.
|
|
|
True if and only if the object is true in the model.
|
|
|
True if and only if the object is false in the model.
|
|
Helpers
|
|
|
Whether all the elements of the model in the list are false but one, and
none is true, under the model.
|
|
|
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 |