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 detailsDefined 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 detailsDefined in Data.Algorithm.SatSolver.Lit Methodscompare :: Lit a -> Lit a -> Ordering(<) :: Lit a -> Lit a -> Bool(<=) :: Lit a -> Lit a -> Bool(>) :: Lit a -> Lit a -> Bool(>=) :: Lit a -> Lit a -> Boolmax :: Lit a -> Lit a -> Lit amin :: Lit a -> Lit a -> Lit a Show a => Show (Lit a) Source # Show instance Instance detailsDefined in Data.Algorithm.SatSolver.Lit MethodsshowsPrec :: Int -> Lit a -> ShowSshow :: Lit a -> StringshowList :: [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