Safe HaskellSafe

Data.Algorithm.SatSolver.Clause

Contents

Synopsis

type

newtype Clause a Source #

Clause type

Constructors

Clause 

Fields

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"]