Safe Haskell	Safe

Data.Algorithm.SatSolver.Clause

Contents

type
constructing
properties
querying

Synopsis

newtype Clause a = Clause {
- getLits :: [Lit a]
}
mk :: Ord a => [Lit a] -> Clause a
fromString :: String -> Clause String
isEmpty :: Clause a -> Bool
isUnit :: Clause a -> Bool
isMonotone :: Clause a -> Bool
isNegMonotone :: Clause a -> Bool
isPosMonotone :: Clause a -> Bool
size :: Clause a -> Int
getVars :: Eq a => Clause a -> [Var a]

type

newtype Clause a Source #

Clause type

Constructors

Clause
Fields getLits :: [Lit a]

Instances

Eq a => Eq (Clause a) Source #
Instance details Defined in Data.Algorithm.SatSolver.Clause Methods (==) :: Clause a -> Clause a -> Bool (/=) :: Clause a -> Clause a -> Bool
Ord a => Ord (Clause a) Source #
Instance details Defined in Data.Algorithm.SatSolver.Clause Methods compare :: Clause a -> Clause a -> Ordering (<) :: Clause a -> Clause a -> Bool (<=) :: Clause a -> Clause a -> Bool (>) :: Clause a -> Clause a -> Bool (>=) :: Clause a -> Clause a -> Bool max :: Clause a -> Clause a -> Clause a min :: Clause a -> Clause a -> Clause a
Show a => Show (Clause a) Source #	Show instance
Instance details Defined in Data.Algorithm.SatSolver.Clause Methods showsPrec :: Int -> Clause a -> ShowS show :: Clause a -> String showList :: [Clause a] -> ShowS

constructing

mk :: Ord a => [Lit a] -> Clause a Source #

mk cs makes a clause from a list of literals. Clauses are sorted and duplicate literals are removed. Opposite literals are not removed.

>>> import qualified Data.Algoritm.SatSolver.Lit as Lit
>>> mk []
[]
>>> mk [Lit.mkNeg' "x1"]
[-"x1"]
>>> mk [Lit.mkNeg' "x1", Lit.mkPos' "x2", Lit.mkNeg' "x3"]
[-"x1",+"x2",-"x3"]
>>> mk [Lit.mkNeg' "x1", Lit.mkPos' "x2", Lit.mkNeg' "x3", Lit.mkPos' "x1"]
[-"x1",+"x1",+"x2",-"x3"]
>>> mk [Lit.mkNeg' "x3", Lit.mkPos' "x2", Lit.mkNeg' "x1"]
[-"x1",+"x2",-"x3"]
>>> mk [Lit.mkPos' "x1", Lit.mkNeg' "x1"]
[-"x1",+"x1"]

fromString :: String -> Clause String Source #

fromString c makes a clause from a string. The first character must be '[' and the last character must be ']' (leading and trailing whitespaces are removed).

>>> fromString "[]"
[]
>>> :type Clause.fromString "[]"
Clause.fromString "[]" :: Clause.Clause String
>>> Clause.fromString "[+x1, -x3, +x2, -x4]"
[+"x1",+"x2",-"x3",-"x4"]
>>> :type Clause.fromString "[+x1, -x3, +x2, -x4]"
Clause.fromString "[+x1, -x3, +x2, -x4]" :: Clause.Clause String

properties

isEmpty :: Clause a -> Bool Source #

isEmpty c returns true iff clause c contains no literal.

>>> import qualified Data.Algoritm.SatSolver.Lit as Lit
>>> let c = mk [] in isEmpty c
True
>>> let c = mk [Lit.mkNeg' "x1"] in isEmpty c
False

isUnit :: Clause a -> Bool Source #

isUnit c returns true iff clause c contains exactly one literal.

>>> import qualified Data.Algoritm.SatSolver.Lit as Lit
>>> let c = mk [] in isUnit c
False
>>> let c = mk [Lit.mkNeg' "x1"] in isUnit c
True
>>> let c = mk [Lit.mkNeg' "x1", Lit.mkPos' "x2"] in isUnit c
False

isMonotone :: Clause a -> Bool Source #

isMonotone c returns true iff clause c is monotone. A clause is monotone if all literals are either positive or negative. An empty clause is monotone.

>>> import qualified Data.Algoritm.SatSolver.Lit as Lit
>>> isMonotone $ mk []
True
>>> isMonotone $ mk [Lit.mkPos' "x1", Lit.mkPos' "x2", Lit.mkPos' "x3"]
True
>>> isMonotone $ mk [Lit.mkNeg' "x1", Lit.mkPos' "x2", Lit.mkNeg' "x3"]
False
>>> isMonotone $ mk [Lit.mkNeg' "x1", Lit.mkNeg' "x2", Lit.mkNeg' "x3"]
True

isNegMonotone :: Clause a -> Bool Source #

isNegMonotone c returns true iff clause c is negative monotone. A clause is negative monotone if all literals are negative. An empty clause is negative monotone.

>>> import qualified Data.Algoritm.SatSolver.Lit as Lit
>>> isNegMonotone $ mk []
True
>>> isNegMonotone $ mk [Lit.mkPos' "x1", Lit.mkPos' "x2", Lit.mkPos' "x3"]
False
>>> isNegMonotone $ mk [Lit.mkNeg' "x1", Lit.mkPos' "x2", Lit.mkNeg' "x3"]
False
>>> isNegMonotone $ mk [Lit.mkNeg' "x1", Lit.mkNeg' "x2", Lit.mkNeg' "x3"]
True

isPosMonotone :: Clause a -> Bool Source #

isPosMonotone c returns true iff clause c is positive monotone. A clause is negative monotone if all literals are positive. An empty clause is positive monotone.

>>> import qualified Data.Algoritm.SatSolver.Lit as Lit
>>> isPosMonotone $ mk []
True
>>> isPosMonotone $ mk [Lit.mkPos' "x1", Lit.mkPos' "x2", Lit.mkPos' "x3"]
True
>>> isPosMonotone $ mk [Lit.mkNeg' "x1", Lit.mkPos' "x2", Lit.mkNeg' "x3"]
False
>>> isPosMonotone $ mk [Lit.mkNeg' "x1", Lit.mkNeg' "x2", Lit.mkNeg' "x3"]
False

querying

size :: Clause a -> Int Source #

size c returns the number of literals in clause c.

>>> import qualified Data.Algoritm.SatSolver.Lit as Lit
>>> let c mk [] in size c
0
>>> let c = mk [Lit.mkPos' "x1"] in size c
1
>>> let c = mk [Lit.mkPos' "x1", Lit.mkPos' "x1"] in size c
1
>>> let c = mk [Lit.mkPos' i | i <- [1..100]] in size c
100

getVars :: Eq a => Clause a -> [Var a] Source #

getVars c returns the distinct propositional variables that occur in clause c.

>>> import qualified Data.Algoritm.SatSolver.Lit as Lit
>>> let c = mk [] in getVars c
[]
>>> let c = mk [Lit.mkPos' "x1"] in getVars c
["x1"]
>>> let c = mk [Lit.mkPos' "x1", Lit.mkNeg' "x2", Lit.mkPos' "x3"] in getVars c
["x1","x2","x3"]
>>> let c = mk [Lit.mkPos' "x1", Lit.mkNeg' "x2", Lit.mkNeg' "x1"] in getVars c
["x1","x2"]