Hets - the Heterogeneous Tool Set
Copyright (c) Jonathan von Schroeder DFKI GmbH 2010 GPLv2 or higher, see LICENSE.txt provisional portable Safe

QBF.Tools

Description

folding and simplification of propositional formulas

Synopsis

# Documentation

data FoldRecord a Source #

Constructors

 FoldRecord FieldsfoldNegation :: 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

isNeg :: FORMULA -> Bool Source #

bothLits :: Set FORMULA -> Bool Source #

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

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

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

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

Constructors

 QuantifiedVars FieldsuniversallyQ :: [Token] existentiallyQ :: [Token] notQ :: [Token]

#### Instances

Instances details
 Show QuantifiedVars Source # Instance detailsDefined in QBF.Tools MethodsshowsPrec :: Int -> QuantifiedVars -> ShowSshow :: QuantifiedVars -> StringshowList :: [QuantifiedVars] -> ShowS

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

"flattening" for disjunctions

negate a formula