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

QBF.Tools

Description

folding and simplification of propositional formulas

Synopsis

Documentation

data FoldRecord a Source #

Constructors

FoldRecord 

Fields

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 #

data QuantifiedVars Source #

Constructors

QuantifiedVars 

Fields

Instances

Show QuantifiedVars Source # 

Methods

showsPrec :: Int -> QuantifiedVars -> ShowS

show :: QuantifiedVars -> String

showList :: [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

flattenDis :: FORMULA -> [FORMULA] Source #

"flattening" for disjunctions

negateFormula :: FORMULA -> FORMULA Source #

negate a formula