Safe HaskellSafe

Data.Algorithm.SatSolver.Lit

Contents

Synopsis

Type

data Lit a Source #

Lit type

Constructors

Neg (Var a) 
Pos (Var a) 
Instances
Eq a => Eq (Lit a) Source # 
Instance details

Defined in Data.Algorithm.SatSolver.Lit

Methods

(==) :: Lit a -> Lit a -> Bool

(/=) :: Lit a -> Lit a -> Bool

Ord a => Ord (Lit a) Source #

Ord instance

Instance details

Defined in Data.Algorithm.SatSolver.Lit

Methods

compare :: Lit a -> Lit a -> Ordering

(<) :: Lit a -> Lit a -> Bool

(<=) :: Lit a -> Lit a -> Bool

(>) :: Lit a -> Lit a -> Bool

(>=) :: Lit a -> Lit a -> Bool

max :: Lit a -> Lit a -> Lit a

min :: Lit a -> Lit a -> Lit a

Show a => Show (Lit a) Source #

Show instance

Instance details

Defined in Data.Algorithm.SatSolver.Lit

Methods

showsPrec :: Int -> Lit a -> ShowS

show :: Lit a -> String

showList :: [Lit a] -> ShowS

Constructing

mkNeg :: Var a -> Lit a Source #

mkNeg v makes a negative literal from propositionalvariable v.

>>> import qualified Data.Algoritm.SatSolver.Var as Var
>>> mkNeg (Var.mk "x1")
-"x1"

mkPos :: Var a -> Lit a Source #

mkPos v makes a positive literal from propositional variable v.

>>> import qualified Data.Algoritm.SatSolver.Var as Var
>>> mkPos (Var.mk "x1")
+"x1"

mkNeg' :: a -> Lit a Source #

mkNeg' n makes a propositional variable with name n and next makes a negative literal from this propositional variable.

>>> mkNeg' "x1"
-"x1"

mkPos' :: a -> Lit a Source #

mkPos' n makes a propositional variable with name n and next makes a positive literal from this propositional variable.

>>> mkPos' "x1"
+"x1"

fromString :: String -> Lit String Source #

fromString s makes a literal from a string. The first character must be either - or + (leading and trailing whitespaces are removed).

>>> fromString "-x1"
-"x1"
>>> :type fromString "-x1"
fromString "-x1" :: Lit String
>>> fromString "+x1"
+"x1"
>>> :type fromString "+x1"
fromString "+x1" :: Lit String

neg :: Lit a -> Lit a Source #

neg l returns the opposite literal of literal l.

>>> neg $ mkNeg' "x1"
+"x1"
>>> neg $ mkNeg' "x1"
-"x1"

Transforming

getVar :: Lit a -> Var a Source #

getVar l return the propositional variable literal l is defined on.

>>> getVar $ L.mkNeg' "x1"
"x1"
>>> getVar $ L.mkPos' "x1"
"x1"

toBool :: Lit a -> Bool Source #

toBool l returns true if literal is positive and false otherwise.

>>> toBool  $ L.mkNeg' "x1"
False
>>> toBool  $ L.mkPos' "x1"
True