Safe Haskell	Safe

Data.Algorithm.SatSolver.Lit

Contents

Type
Constructing
Transforming

Synopsis

data Lit a
- = Neg (Var a)
- | Pos (Var a)
mkNeg :: Var a -> Lit a
mkPos :: Var a -> Lit a
mkNeg' :: a -> Lit a
mkPos' :: a -> Lit a
fromString :: String -> Lit String
neg :: Lit a -> Lit a
getVar :: Lit a -> Var a
toBool :: Lit a -> Bool

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