Copyright	(c) Jonathan von Schroeder DFKI GmbH 2010
License	GPLv2 or higher, see LICENSE.txt
Maintainer	<jonathan.von_schroeder@dfki.de>
Stability	provisional
Portability	portable
Safe Haskell	Safe

QBF.Tools

Description

folding and simplification of propositional formulas

Synopsis

data FoldRecord a = FoldRecord {
- foldNegation :: a -> Range -> a
- foldConjunction :: [a] -> Range -> a
- foldDisjunction :: [a] -> Range -> a
- foldImplication :: a -> a -> Range -> a
- foldEquivalence :: a -> a -> Range -> a
- foldTrueAtom :: Range -> a
- foldFalseAtom :: Range -> a
- foldPredication :: Token -> a
- foldForAll :: [Token] -> a -> Range -> a
- foldExists :: [Token] -> a -> Range -> a
}
foldFormula :: FoldRecord a -> FORMULA -> a
mapRecord :: FoldRecord FORMULA
isNeg :: FORMULA -> Bool
isQuantified :: FORMULA -> Bool
getLits :: Set FORMULA -> Set FORMULA
bothLits :: Set FORMULA -> Bool
getConj :: FORMULA -> [FORMULA]
getDisj :: FORMULA -> [FORMULA]
flatConj :: [FORMULA] -> Set FORMULA
mkConj :: [FORMULA] -> Range -> FORMULA
flatDisj :: [FORMULA] -> Set FORMULA
mkDisj :: [FORMULA] -> Range -> FORMULA
simplify :: FORMULA -> FORMULA
elimEquiv :: FORMULA -> FORMULA
elimImpl :: FORMULA -> FORMULA
negForm :: Range -> FORMULA -> FORMULA
moveNegIn :: FORMULA -> FORMULA
distributeAndOverOr :: FORMULA -> FORMULA
cnf :: FORMULA -> FORMULA
distributeOrOverAnd :: FORMULA -> FORMULA
dnf :: FORMULA -> FORMULA
combine :: [[a]] -> [[a]]
containsAtoms :: FORMULA -> (Bool, Bool)
getVars :: FORMULA -> [Token]
uniqueQuantifiedVars :: Int -> String -> FORMULA -> (Int, FORMULA)
uniqueQuantifiedVars' :: Int -> Map Token Token -> String -> FORMULA -> (Int, FORMULA)
removeQuantifiers :: FORMULA -> FORMULA
data QuantifiedVars = QuantifiedVars {
- universallyQ :: [Token]
- existentiallyQ :: [Token]
- notQ :: [Token]
}
quantifiedVars :: QuantifiedVars
joinQuantifiedVars :: QuantifiedVars -> QuantifiedVars -> QuantifiedVars
getQuantifiedVars :: FORMULA -> QuantifiedVars
flatten :: FORMULA -> [FORMULA]
flattenDis :: FORMULA -> [FORMULA]
negateFormula :: FORMULA -> FORMULA

Documentation

data FoldRecord a Source #

Constructors

FoldRecord
Fields foldNegation :: a -> Range -> a foldConjunction :: [a] -> Range -> a foldDisjunction :: [a] -> Range -> a foldImplication :: a -> a -> Range -> a foldEquivalence :: a -> a -> Range -> a foldTrueAtom :: Range -> a foldFalseAtom :: Range -> a foldPredication :: Token -> a foldForAll :: [Token] -> a -> Range -> a foldExists :: [Token] -> a -> Range -> a

foldFormula :: FoldRecord a -> FORMULA -> a Source #

mapRecord :: FoldRecord FORMULA Source #

isNeg :: FORMULA -> Bool Source #

isQuantified :: FORMULA -> Bool Source #

getLits :: Set FORMULA -> Set FORMULA Source #

bothLits :: Set FORMULA -> Bool Source #

getConj :: FORMULA -> [FORMULA] Source #

getDisj :: FORMULA -> [FORMULA] Source #

flatConj :: [FORMULA] -> Set FORMULA Source #

mkConj :: [FORMULA] -> Range -> FORMULA Source #

flatDisj :: [FORMULA] -> Set FORMULA Source #

mkDisj :: [FORMULA] -> Range -> FORMULA Source #

simplify :: FORMULA -> FORMULA Source #

elimEquiv :: FORMULA -> FORMULA Source #

elimImpl :: FORMULA -> FORMULA Source #

negForm :: Range -> FORMULA -> FORMULA Source #

moveNegIn :: FORMULA -> FORMULA Source #

distributeAndOverOr :: FORMULA -> FORMULA Source #

cnf :: FORMULA -> FORMULA Source #

distributeOrOverAnd :: FORMULA -> FORMULA Source #

dnf :: FORMULA -> FORMULA Source #

combine :: [[a]] -> [[a]] Source #

containsAtoms :: FORMULA -> (Bool, Bool) Source #

getVars :: FORMULA -> [Token] Source #

uniqueQuantifiedVars :: Int -> String -> FORMULA -> (Int, FORMULA) Source #

uniqueQuantifiedVars' :: Int -> Map Token Token -> String -> FORMULA -> (Int, FORMULA) Source #

removeQuantifiers :: FORMULA -> FORMULA Source #

data QuantifiedVars Source #

Constructors

QuantifiedVars
Fields universallyQ :: [Token] existentiallyQ :: [Token] notQ :: [Token]

Instances

Instances details

Show QuantifiedVars Source #
Instance details Defined in QBF.Tools Methods showsPrec :: Int -> QuantifiedVars -> ShowS show :: QuantifiedVars -> String showList :: [QuantifiedVars] -> ShowS

quantifiedVars :: QuantifiedVars Source #

joinQuantifiedVars :: QuantifiedVars -> QuantifiedVars -> QuantifiedVars Source #

getQuantifiedVars :: FORMULA -> QuantifiedVars Source #

flatten :: FORMULA -> [FORMULA] Source #

the flatten functions use associtivity to "flatten" the syntax tree of the formulae

flatten "flattens" formulae under the assumption of the semantics of basic specs, this means that we put each "clause" into a single formula for CNF we really will obtain clauses

flattenDis :: FORMULA -> [FORMULA] Source #

"flattening" for disjunctions

negateFormula :: FORMULA -> FORMULA Source #

negate a formula