




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 0literal 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 ''setlike'' objects. I've distilled their interface into three
methods. These methods are used extensively in the implementation of the
solver.
  Methods   The setlike object with an element removed.
   The setlike object with an element included.
   Whether the setlike 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 newlyassigned 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
truthfunctional 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 