Copyright	(c) Stéphane Vialette, 2015
License	MIT
Maintainer	vialette@gmail.com
Stability	experimental
Safe Haskell	Safe-Inferred

Clause

Description

Synopsis

Documentation

data Clause a

Clause type

Constructors

Clause [Literal a]

Instances

Eq a => Eq (Clause a)
Ord a => Ord (Clause a)
Show a => Show (Clause a)

makeClause :: Ord a => [Literal a] -> Clause a

The makeClause function constructs a clause from a list of literals. Clauses are sorted by literals and duplicate literals are removed.

>>> let p1 = L.Positive (V.Variable "x1")
>>> let n2 = L.Negative (V.Variable "x2")
>>> let p3 = L.Positive (V.Variable "x3")
>>> let n1 = L.Negative (V.Variable "x1")
>>> makeClause [p1,n2,p3,n1]
Clause [Negative (Variable "x1"),Negative (Variable "x2"),
        Positive (Variable "x1"),Positive (Variable "x3")]

>>> makeClause []
Clause []

empty :: Ord a => Clause a

The empty function returns the empty clause (i.e., the clause with no literal).

literals :: Clause a -> [Literal a]

The literals function returns the list of the literals that occur in a clause.

>>> let p1 = L.Positive (V.Variable "x1")
>>> let n2 = L.Negative (V.Variable "x2")
>>> let p3 = L.Positive (V.Variable "x3")
>>> let n1 = L.Negative (V.Variable "x1")
>>> literals $ makeClause [p1,n2,p3,n1]
[Negative (Variable "x1"),Negative (Variable "x2"),
 Positive (Variable "x1"),Positive (Variable "x3")]

numberOfLiterals :: Clause a -> Int

The numberOfLiterals function returns the number of literals in a clause.

null :: Clause a -> Bool

The null function return True is the clause contains no literal.

>>> null empty
True
>>> null $ makeClause [L.Positive (V.Variable "x1")]
False

isUnit :: Clause a -> Bool

The isUnit function return True if the clause contains exactly one literal.

>>> isUnit empty
False
>>> isUnit $ makeClause [L.Positive (V.Variable "x1")]
True
>>> isUnit $ makeClause [L.Negative (V.Variable "x1")]
True
>>> isUnit $ makeClause [L.Positive (V.Variable "x1"), L.Negative (V.Variable "x2")]
False

isTautology :: Eq a => Clause a -> Bool

The isTautology function return True if the clause contains two opposite literals.

>>> isTautology empty
False
>>> isTautology $ makeClause [p1]
False
>>> isTautology $ makeClause [p1,n2]
False
>>> isTautology $ makeClause [p1,n2,n1]
True
>>>

containsLiteral :: Eq a => Clause a -> Literal a -> Bool

The containsLiteral function return True if the clause contains an occurrence of a given literal.

>>> let p1 = L.Positive (V.Variable "x1")
>>> let n2 = L.Negative (V.Variable "x2")
>>> let p3 = L.Positive (V.Variable "x3")
>>> containsLiteral empty p1
False
>>> containsLiteral (makeClause [p1,n2]) p1
True
>>> containsLiteral (makeClause [p1,n2]) n2
True
>>> containsLiteral (makeClause [p1,n2]) p3
False

containsVariable :: Eq a => Clause a -> Variable a -> Bool

The containsVariable function return True if the clause contains an occurrence of a given variable (that is an occurrence of the positive or the negative literal associated to the variable).

>>> let p1 = L.Positive (V.Variable "x1")
>>> let n2 = L.Negative (V.Variable "x2")
>>> containsVariable empty (V.Variable "x1")
False
>>> containsVariable (makeClause [p1,n2]) (V.Variable "x1")
True
>>> containsVariable (makeClause [p1,n2]) (V.Variable "x2")
True
>>> containsVariable (makeClause [p1,n2]) (V.Variable "x3")
False

deleteLiteral :: Ord a => Clause a -> Literal a -> Clause a

The deleteLiteral function delete a literal in a clause.

example1 :: Clause [Char]

example2 :: Clause [Char]

example3 :: Clause [Char]

example4 :: Clause [Char]

example5 :: Clause [Char]

example6 :: Clause [Char]

example7 :: Clause [Char]

example8 :: Clause [Char]

example9 :: Clause [Char]