{- |
Module : ./Propositional/Fold.hs
Description : folding function for propositional formulas
Copyright : (c) Christian Maeder, DFKI GmbH 2009
License : GPLv2 or higher, see LICENSE.txt
Maintainer : Christian.Maeder@dfki.de
Stability : provisional
Portability : portable
folding and simplification of propositional formulas
-}
module Propositional.Fold where
import Common.Id
import qualified Data.Set as Set
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
, foldTrue_atom :: Range -> a
, foldFalse_atom :: Range -> a
, foldPredication :: Token -> a }
foldFormula :: FoldRecord a -> FORMULA -> a
foldFormula r frm = case frm of
Negation f n -> foldNegation r (foldFormula r f) n
Conjunction xs n -> foldConjunction r (map (foldFormula r) xs) n
Disjunction xs n -> foldDisjunction r (map (foldFormula r) xs) n
Implication x y n -> foldImplication r (foldFormula r x) (foldFormula r y) n
Equivalence x y n -> foldEquivalence r (foldFormula r x) (foldFormula r y) n
True_atom n -> foldTrue_atom r n
False_atom n -> foldFalse_atom r n
Predication x -> foldPredication r x
mapRecord :: FoldRecord FORMULA
mapRecord = FoldRecord
{ foldNegation = Negation
, foldConjunction = Conjunction
, foldDisjunction = Disjunction
, foldImplication = Implication
, foldEquivalence = Equivalence
, foldTrue_atom = True_atom
, foldFalse_atom = False_atom
, foldPredication = Predication }
isNeg :: FORMULA -> Bool
isNeg f = case f of
Negation _ _ -> True
_ -> False
getLits = Set.fold (\ f -> case f of
Negation x _ -> Set.insert x
_ -> Set.insert f) Set.empty
bothLits :: Set.Set FORMULA -> Bool
bothLits fs = let
(ns, ps) = Set.partition isNeg fs
in not $ Set.null $ Set.intersection (getLits ns) (getLits ps)
getConj :: FORMULA -> [FORMULA]
getConj f = case f of
Conjunction xs _ -> xs
True_atom _ -> []
_ -> [f]
getDisj :: FORMULA -> [FORMULA]
getDisj f = case f of
Disjunction xs _ -> xs
False_atom _ -> []
_ -> [f]
flatConj :: [FORMULA] -> Set.Set FORMULA
flatConj = Set.fromList
. concatMap (\ f -> case f of
True_atom _ -> []
Conjunction fs _ -> fs
_ -> [f])
mkConj :: [FORMULA] -> Range -> FORMULA
mkConj fs n = let s = flatConj fs in
if Set.member (False_atom nullRange) s || bothLits s then False_atom n else
case Set.toList s of
[] -> True_atom n
[x] -> x
ls -> Conjunction (map (flip mkDisj n . Set.toList)
$ foldr ((\ l ll ->
if any (`Set.isSubsetOf` l) ll then ll else
l : filter (not . Set.isSubsetOf l) ll)
. Set.fromList . getDisj) [] ls) n
flatDisj :: [FORMULA] -> Set.Set FORMULA
flatDisj = Set.fromList
. concatMap (\ f -> case f of
False_atom _ -> []
Disjunction fs _ -> fs
_ -> [f])
mkDisj :: [FORMULA] -> Range -> FORMULA
mkDisj fs n = let s = flatDisj fs in
if Set.member (True_atom nullRange) s || bothLits s then True_atom n else
case Set.toList s of
[] -> False_atom n
[x] -> x
ls -> Disjunction (map (flip mkConj n . Set.toList)
$ foldr ((\ l ll ->
if any (`Set.isSubsetOf` l) ll then ll else
l : filter (not . Set.isSubsetOf l) ll)
. Set.fromList . getConj) [] ls) n
simplify :: FORMULA -> FORMULA
simplify = foldFormula mapRecord
{ foldNegation = \ f n -> case f of
True_atom p -> False_atom p
False_atom p -> True_atom p
Negation g _ -> g
s -> Negation s n
, foldConjunction = mkConj
, foldDisjunction = mkDisj
, foldImplication = \ x y n -> case x of
False_atom p -> True_atom p
_ -> if x == y then True_atom n else case x of
True_atom _ -> y
False_atom _ -> True_atom n
Negation z _ | z == y -> x
_ -> case y of
Negation z _ | z == x -> x
_ -> Implication x y n
, foldEquivalence = \ x y n -> case compare x y of
LT -> case y of
Negation z _ | x == z -> False_atom n
_ -> Equivalence x y n
EQ -> True_atom n
GT -> case x of
Negation z _ | z == y -> False_atom n
_ -> Equivalence y x n }
elimEquiv :: FORMULA -> FORMULA
elimEquiv = foldFormula mapRecord
{ foldEquivalence = \ x y n ->
Conjunction [Implication x y n, Implication y x n] n }
elimImpl :: FORMULA -> FORMULA
elimImpl = foldFormula mapRecord
{ foldImplication = \ x y n ->
Disjunction [Negation x n, y] n }
negForm :: Range -> FORMULA -> FORMULA
negForm r frm = case frm of
Negation f _ -> case f of
Negation nf _ -> negForm r nf
_ -> f
Conjunction xs n -> Disjunction (map (negForm r) xs) n
Disjunction xs n -> Conjunction (map (negForm r) xs) n
True_atom n -> False_atom n
False_atom n -> True_atom n
_ -> Negation frm r
moveNegIn :: FORMULA -> FORMULA
moveNegIn frm = case frm of
Negation f n -> negForm n f
Conjunction xs n -> Conjunction (map moveNegIn xs) n
Disjunction xs n -> Disjunction (map moveNegIn xs) n
_ -> frm
distributeAndOverOr :: FORMULA -> FORMULA
distributeAndOverOr f = case f of
Conjunction xs n -> mkConj (map distributeAndOverOr xs) n
Disjunction xs n -> if all isPrimForm xs then mkDisj xs n else
distributeAndOverOr
$ mkConj (map (`mkDisj` n) . combine $ map getConj xs) n
_ -> f
cnf :: FORMULA -> FORMULA
cnf = flipLiterals . distributeAndOverOr . moveNegIn . elimImpl . elimEquiv
flipLiterals :: FORMULA -> FORMULA
flipLiterals f = case f of
Negation p@(Predication _) _ -> p
Predication t -> Negation f $ tokPos t
Conjunction xs n -> Conjunction (map flipLiterals xs) n
Disjunction xs n -> Disjunction (map flipLiterals xs) n
_ -> f
distributeOrOverAnd :: FORMULA -> FORMULA
distributeOrOverAnd f = case f of
Disjunction xs n -> mkDisj (map distributeOrOverAnd xs) n
Conjunction xs n -> if all isPrimForm xs then mkConj xs n else
distributeOrOverAnd
$ mkDisj (map (`mkConj` n) . combine $ map getDisj xs) n
_ -> f
dnf :: FORMULA -> FORMULA
dnf = distributeOrOverAnd . moveNegIn . elimImpl . elimEquiv
combine :: [[a]] -> [[a]]
combine l = case l of
[] -> [[]]
h : t -> concatMap (flip map h . flip (:)) (combine t)