Hets - the Heterogeneous Tool Set

Copyright(c) Jonathan von Schroeder, DFKI GmbH 2010
LicenseGPLv2 or higher, see LICENSE.txt
Maintainer<jonathan.von_schroeder@dfki.de>
Stabilityprovisional
Portabilityportable
Safe HaskellSafe-Inferred

QBF.Tools

Description

folding and simplification of propositional formulas

Synopsis

Documentation

data FoldRecord a

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
 

combine :: [[a]] -> [[a]]

data QuantifiedVars

Constructors

QuantifiedVars 

Fields

universallyQ :: [Token]
 
existentiallyQ :: [Token]
 
notQ :: [Token]
 

Instances

flatten :: FORMULA -> [FORMULA]

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]

"flattening" for disjunctions

negateFormula :: FORMULA -> FORMULA

negate a formula