ad772a9e1c0a951a5fa508a3a3ec35e3fda2aec2Christian MaederDescription : folding function for propositional formulas
ad772a9e1c0a951a5fa508a3a3ec35e3fda2aec2Christian MaederCopyright : (c) Christian Maeder, DFKI GmbH 2009
98890889ffb2e8f6f722b00e265a211f13b5a861Corneliu-Claudiu ProdescuLicense : GPLv2 or higher, see LICENSE.txt
ad772a9e1c0a951a5fa508a3a3ec35e3fda2aec2Christian MaederMaintainer : Christian.Maeder@dfki.de
ad772a9e1c0a951a5fa508a3a3ec35e3fda2aec2Christian MaederStability : provisional
ad772a9e1c0a951a5fa508a3a3ec35e3fda2aec2Christian MaederPortability : portable
ad772a9e1c0a951a5fa508a3a3ec35e3fda2aec2Christian Maederfolding and simplification of propositional formulas
ae4309002e3121468cc3f3f77b821d4620ca24ccChristian Maederimport qualified Data.Set as Set
ad772a9e1c0a951a5fa508a3a3ec35e3fda2aec2Christian Maederdata FoldRecord a = FoldRecord
ad772a9e1c0a951a5fa508a3a3ec35e3fda2aec2Christian Maeder { foldNegation :: a -> Range -> a
ad772a9e1c0a951a5fa508a3a3ec35e3fda2aec2Christian Maeder , foldConjunction :: [a] -> Range -> a
ad772a9e1c0a951a5fa508a3a3ec35e3fda2aec2Christian Maeder , foldDisjunction :: [a] -> Range -> a
ad772a9e1c0a951a5fa508a3a3ec35e3fda2aec2Christian Maeder , foldImplication :: a -> a -> Range -> a
ad772a9e1c0a951a5fa508a3a3ec35e3fda2aec2Christian Maeder , foldEquivalence :: a -> a -> Range -> a
ad772a9e1c0a951a5fa508a3a3ec35e3fda2aec2Christian Maeder , foldTrue_atom :: Range -> a
ad772a9e1c0a951a5fa508a3a3ec35e3fda2aec2Christian Maeder , foldFalse_atom :: Range -> a
ad772a9e1c0a951a5fa508a3a3ec35e3fda2aec2Christian Maeder , foldPredication :: Token -> a }
ad772a9e1c0a951a5fa508a3a3ec35e3fda2aec2Christian MaederfoldFormula :: FoldRecord a -> FORMULA -> a
ad772a9e1c0a951a5fa508a3a3ec35e3fda2aec2Christian MaederfoldFormula r frm = case frm of
ad772a9e1c0a951a5fa508a3a3ec35e3fda2aec2Christian Maeder Negation f n -> foldNegation r (foldFormula r f) n
ad772a9e1c0a951a5fa508a3a3ec35e3fda2aec2Christian Maeder Conjunction xs n -> foldConjunction r (map (foldFormula r) xs) n
ad772a9e1c0a951a5fa508a3a3ec35e3fda2aec2Christian Maeder Disjunction xs n -> foldDisjunction r (map (foldFormula r) xs) n
ad772a9e1c0a951a5fa508a3a3ec35e3fda2aec2Christian Maeder Implication x y n -> foldImplication r (foldFormula r x) (foldFormula r y) n
ad772a9e1c0a951a5fa508a3a3ec35e3fda2aec2Christian Maeder Equivalence x y n -> foldEquivalence r (foldFormula r x) (foldFormula r y) n
ad772a9e1c0a951a5fa508a3a3ec35e3fda2aec2Christian Maeder True_atom n -> foldTrue_atom r n
ad772a9e1c0a951a5fa508a3a3ec35e3fda2aec2Christian Maeder False_atom n -> foldFalse_atom r n
ad772a9e1c0a951a5fa508a3a3ec35e3fda2aec2Christian Maeder Predication x -> foldPredication r x
ad772a9e1c0a951a5fa508a3a3ec35e3fda2aec2Christian MaedermapRecord :: FoldRecord FORMULA
ad772a9e1c0a951a5fa508a3a3ec35e3fda2aec2Christian MaedermapRecord = FoldRecord
ad772a9e1c0a951a5fa508a3a3ec35e3fda2aec2Christian Maeder { foldNegation = Negation
ad772a9e1c0a951a5fa508a3a3ec35e3fda2aec2Christian Maeder , foldConjunction = Conjunction
ad772a9e1c0a951a5fa508a3a3ec35e3fda2aec2Christian Maeder , foldDisjunction = Disjunction
ad772a9e1c0a951a5fa508a3a3ec35e3fda2aec2Christian Maeder , foldImplication = Implication
ad772a9e1c0a951a5fa508a3a3ec35e3fda2aec2Christian Maeder , foldEquivalence = Equivalence
ad772a9e1c0a951a5fa508a3a3ec35e3fda2aec2Christian Maeder , foldTrue_atom = True_atom
ad772a9e1c0a951a5fa508a3a3ec35e3fda2aec2Christian Maeder , foldFalse_atom = False_atom
ad772a9e1c0a951a5fa508a3a3ec35e3fda2aec2Christian Maeder , foldPredication = Predication }
c7af9fa9874262288327ea398b2466e1f4c20fe2Christian MaederisNeg :: FORMULA -> Bool
c7af9fa9874262288327ea398b2466e1f4c20fe2Christian MaederisNeg f = case f of
c7af9fa9874262288327ea398b2466e1f4c20fe2Christian Maeder Negation _ _ -> True
c7af9fa9874262288327ea398b2466e1f4c20fe2Christian MaedergetLits :: Set.Set FORMULA -> Set.Set FORMULA
c7af9fa9874262288327ea398b2466e1f4c20fe2Christian MaedergetLits = Set.fold (\ f -> case f of
c7af9fa9874262288327ea398b2466e1f4c20fe2Christian Maeder Negation x _ -> Set.insert x
c7af9fa9874262288327ea398b2466e1f4c20fe2Christian MaederbothLits :: Set.Set FORMULA -> Bool
c7af9fa9874262288327ea398b2466e1f4c20fe2Christian MaederbothLits fs = let
c7af9fa9874262288327ea398b2466e1f4c20fe2Christian Maeder (ns, ps) = Set.partition isNeg fs
c7af9fa9874262288327ea398b2466e1f4c20fe2Christian Maeder in not $ Set.null $ Set.intersection (getLits ns) (getLits ps)
97c9d39efee30883aa578294c46506ff8a9478c8Christian MaedergetConj :: FORMULA -> [FORMULA]
97c9d39efee30883aa578294c46506ff8a9478c8Christian MaedergetConj f = case f of
97c9d39efee30883aa578294c46506ff8a9478c8Christian Maeder Conjunction xs _ -> xs
b06c4591505328304ede152a5d517f832c08950aChristian Maeder True_atom _ -> []
97c9d39efee30883aa578294c46506ff8a9478c8Christian MaedergetDisj :: FORMULA -> [FORMULA]
97c9d39efee30883aa578294c46506ff8a9478c8Christian MaedergetDisj f = case f of
97c9d39efee30883aa578294c46506ff8a9478c8Christian Maeder Disjunction xs _ -> xs
b06c4591505328304ede152a5d517f832c08950aChristian Maeder False_atom _ -> []
c7af9fa9874262288327ea398b2466e1f4c20fe2Christian MaederflatConj :: [FORMULA] -> Set.Set FORMULA
ae4309002e3121468cc3f3f77b821d4620ca24ccChristian Maeder . concatMap (\ f -> case f of
ae4309002e3121468cc3f3f77b821d4620ca24ccChristian Maeder True_atom _ -> []
ae4309002e3121468cc3f3f77b821d4620ca24ccChristian Maeder Conjunction fs _ -> fs
c7af9fa9874262288327ea398b2466e1f4c20fe2Christian MaedermkConj :: [FORMULA] -> Range -> FORMULA
c7af9fa9874262288327ea398b2466e1f4c20fe2Christian MaedermkConj fs n = let s = flatConj fs in
c7af9fa9874262288327ea398b2466e1f4c20fe2Christian Maeder if Set.member (False_atom nullRange) s || bothLits s then False_atom n else
c7af9fa9874262288327ea398b2466e1f4c20fe2Christian Maeder [] -> True_atom n
97c9d39efee30883aa578294c46506ff8a9478c8Christian Maeder ls -> Conjunction (map (flip mkDisj n . Set.toList)
a5d871d31482698effb061956781bf21517e469bChristian Maeder $ foldr ((\ l ll ->
a5d871d31482698effb061956781bf21517e469bChristian Maeder if any (`Set.isSubsetOf` l) ll then ll else
a5d871d31482698effb061956781bf21517e469bChristian Maeder l : filter (not . Set.isSubsetOf l) ll)
a5d871d31482698effb061956781bf21517e469bChristian Maeder . Set.fromList . getDisj) [] ls) n
c7af9fa9874262288327ea398b2466e1f4c20fe2Christian MaederflatDisj :: [FORMULA] -> Set.Set FORMULA
ae4309002e3121468cc3f3f77b821d4620ca24ccChristian Maeder . concatMap (\ f -> case f of
ae4309002e3121468cc3f3f77b821d4620ca24ccChristian Maeder False_atom _ -> []
ae4309002e3121468cc3f3f77b821d4620ca24ccChristian Maeder Disjunction fs _ -> fs
c7af9fa9874262288327ea398b2466e1f4c20fe2Christian MaedermkDisj :: [FORMULA] -> Range -> FORMULA
c7af9fa9874262288327ea398b2466e1f4c20fe2Christian MaedermkDisj fs n = let s = flatDisj fs in
c7af9fa9874262288327ea398b2466e1f4c20fe2Christian Maeder if Set.member (True_atom nullRange) s || bothLits s then True_atom n else
c7af9fa9874262288327ea398b2466e1f4c20fe2Christian Maeder [] -> False_atom n
97c9d39efee30883aa578294c46506ff8a9478c8Christian Maeder ls -> Disjunction (map (flip mkConj n . Set.toList)
a5d871d31482698effb061956781bf21517e469bChristian Maeder $ foldr ((\ l ll ->
a5d871d31482698effb061956781bf21517e469bChristian Maeder if any (`Set.isSubsetOf` l) ll then ll else
a5d871d31482698effb061956781bf21517e469bChristian Maeder l : filter (not . Set.isSubsetOf l) ll)
a5d871d31482698effb061956781bf21517e469bChristian Maeder . Set.fromList . getConj) [] ls) n
ad772a9e1c0a951a5fa508a3a3ec35e3fda2aec2Christian Maedersimplify :: FORMULA -> FORMULA
ad772a9e1c0a951a5fa508a3a3ec35e3fda2aec2Christian Maedersimplify = foldFormula mapRecord
ad772a9e1c0a951a5fa508a3a3ec35e3fda2aec2Christian Maeder { foldNegation = \ f n -> case f of
ad772a9e1c0a951a5fa508a3a3ec35e3fda2aec2Christian Maeder True_atom p -> False_atom p
ad772a9e1c0a951a5fa508a3a3ec35e3fda2aec2Christian Maeder False_atom p -> True_atom p
ad772a9e1c0a951a5fa508a3a3ec35e3fda2aec2Christian Maeder Negation g _ -> g
ad772a9e1c0a951a5fa508a3a3ec35e3fda2aec2Christian Maeder s -> Negation s n
c7af9fa9874262288327ea398b2466e1f4c20fe2Christian Maeder , foldConjunction = mkConj
c7af9fa9874262288327ea398b2466e1f4c20fe2Christian Maeder , foldDisjunction = mkDisj
ad772a9e1c0a951a5fa508a3a3ec35e3fda2aec2Christian Maeder , foldImplication = \ x y n -> case x of
ad772a9e1c0a951a5fa508a3a3ec35e3fda2aec2Christian Maeder False_atom p -> True_atom p
ffb6099205b26594acf25e64efd338cee362a659Christian Maeder _ -> if x == y then True_atom n else case x of
ffb6099205b26594acf25e64efd338cee362a659Christian Maeder True_atom _ -> y
ffb6099205b26594acf25e64efd338cee362a659Christian Maeder False_atom _ -> True_atom n
ffb6099205b26594acf25e64efd338cee362a659Christian Maeder Negation z _ | z == y -> x
ffb6099205b26594acf25e64efd338cee362a659Christian Maeder _ -> case y of
ffb6099205b26594acf25e64efd338cee362a659Christian Maeder Negation z _ | z == x -> x
ffb6099205b26594acf25e64efd338cee362a659Christian Maeder _ -> Implication x y n
ae4309002e3121468cc3f3f77b821d4620ca24ccChristian Maeder , foldEquivalence = \ x y n -> case compare x y of
ffb6099205b26594acf25e64efd338cee362a659Christian Maeder LT -> case y of
ffb6099205b26594acf25e64efd338cee362a659Christian Maeder Negation z _ | x == z -> False_atom n
ffb6099205b26594acf25e64efd338cee362a659Christian Maeder _ -> Equivalence x y n
ae4309002e3121468cc3f3f77b821d4620ca24ccChristian Maeder EQ -> True_atom n
ffb6099205b26594acf25e64efd338cee362a659Christian Maeder GT -> case x of
ffb6099205b26594acf25e64efd338cee362a659Christian Maeder Negation z _ | z == y -> False_atom n
ffb6099205b26594acf25e64efd338cee362a659Christian Maeder _ -> Equivalence y x n }
ffb6099205b26594acf25e64efd338cee362a659Christian MaederelimEquiv :: FORMULA -> FORMULA
ffb6099205b26594acf25e64efd338cee362a659Christian MaederelimEquiv = foldFormula mapRecord
ffb6099205b26594acf25e64efd338cee362a659Christian Maeder { foldEquivalence = \ x y n ->
ffb6099205b26594acf25e64efd338cee362a659Christian Maeder Conjunction [Implication x y n, Implication y x n] n }
ffb6099205b26594acf25e64efd338cee362a659Christian MaederelimImpl :: FORMULA -> FORMULA
ffb6099205b26594acf25e64efd338cee362a659Christian MaederelimImpl = foldFormula mapRecord
ffb6099205b26594acf25e64efd338cee362a659Christian Maeder { foldImplication = \ x y n ->
ffb6099205b26594acf25e64efd338cee362a659Christian Maeder Disjunction [Negation x n, y] n }
97c9d39efee30883aa578294c46506ff8a9478c8Christian MaedernegForm :: Range -> FORMULA -> FORMULA
97c9d39efee30883aa578294c46506ff8a9478c8Christian MaedernegForm r frm = case frm of
a487f12bb3f43a648466f3ebf98561444472c5a6Christian Maeder Negation f _ -> case f of
a487f12bb3f43a648466f3ebf98561444472c5a6Christian Maeder Negation nf _ -> negForm r nf
97c9d39efee30883aa578294c46506ff8a9478c8Christian Maeder Conjunction xs n -> Disjunction (map (negForm r) xs) n
97c9d39efee30883aa578294c46506ff8a9478c8Christian Maeder Disjunction xs n -> Conjunction (map (negForm r) xs) n
97c9d39efee30883aa578294c46506ff8a9478c8Christian Maeder True_atom n -> False_atom n
97c9d39efee30883aa578294c46506ff8a9478c8Christian Maeder False_atom n -> True_atom n
97c9d39efee30883aa578294c46506ff8a9478c8Christian Maeder _ -> Negation frm r
97c9d39efee30883aa578294c46506ff8a9478c8Christian MaedermoveNegIn :: FORMULA -> FORMULA
97c9d39efee30883aa578294c46506ff8a9478c8Christian MaedermoveNegIn frm = case frm of
97c9d39efee30883aa578294c46506ff8a9478c8Christian Maeder Negation f n -> negForm n f
97c9d39efee30883aa578294c46506ff8a9478c8Christian Maeder Conjunction xs n -> Conjunction (map moveNegIn xs) n
97c9d39efee30883aa578294c46506ff8a9478c8Christian Maeder Disjunction xs n -> Disjunction (map moveNegIn xs) n
97c9d39efee30883aa578294c46506ff8a9478c8Christian MaederdistributeAndOverOr :: FORMULA -> FORMULA
97c9d39efee30883aa578294c46506ff8a9478c8Christian MaederdistributeAndOverOr f = case f of
97c9d39efee30883aa578294c46506ff8a9478c8Christian Maeder Conjunction xs n -> mkConj (map distributeAndOverOr xs) n
97c9d39efee30883aa578294c46506ff8a9478c8Christian Maeder Disjunction xs n -> if all isPrimForm xs then mkDisj xs n else
97c9d39efee30883aa578294c46506ff8a9478c8Christian Maeder distributeAndOverOr
a5d871d31482698effb061956781bf21517e469bChristian Maeder $ mkConj (map (`mkDisj` n) . combine $ map getConj xs) n
97c9d39efee30883aa578294c46506ff8a9478c8Christian Maedercnf :: FORMULA -> FORMULA
a5d871d31482698effb061956781bf21517e469bChristian Maedercnf = flipLiterals . distributeAndOverOr . moveNegIn . elimImpl . elimEquiv
a5d871d31482698effb061956781bf21517e469bChristian MaederflipLiterals :: FORMULA -> FORMULA
a5d871d31482698effb061956781bf21517e469bChristian MaederflipLiterals f = case f of
a5d871d31482698effb061956781bf21517e469bChristian Maeder Negation p@(Predication _) _ -> p
a5d871d31482698effb061956781bf21517e469bChristian Maeder Predication t -> Negation f $ tokPos t
a5d871d31482698effb061956781bf21517e469bChristian Maeder Conjunction xs n -> Conjunction (map flipLiterals xs) n
a5d871d31482698effb061956781bf21517e469bChristian Maeder Disjunction xs n -> Disjunction (map flipLiterals xs) n
722a05deb703fa670175a34467bdb1fe5873bd2fChristian MaederdistributeOrOverAnd :: FORMULA -> FORMULA
722a05deb703fa670175a34467bdb1fe5873bd2fChristian MaederdistributeOrOverAnd f = case f of
722a05deb703fa670175a34467bdb1fe5873bd2fChristian Maeder Disjunction xs n -> mkDisj (map distributeOrOverAnd xs) n
722a05deb703fa670175a34467bdb1fe5873bd2fChristian Maeder Conjunction xs n -> if all isPrimForm xs then mkConj xs n else
722a05deb703fa670175a34467bdb1fe5873bd2fChristian Maeder distributeOrOverAnd
a5d871d31482698effb061956781bf21517e469bChristian Maeder $ mkDisj (map (`mkConj` n) . combine $ map getDisj xs) n
722a05deb703fa670175a34467bdb1fe5873bd2fChristian Maederdnf :: FORMULA -> FORMULA
722a05deb703fa670175a34467bdb1fe5873bd2fChristian Maederdnf = distributeOrOverAnd . moveNegIn . elimImpl . elimEquiv
638ef5e65fd5713e2ef668ec48188867544f72a3Christian Maedercombine :: [[a]] -> [[a]]
638ef5e65fd5713e2ef668ec48188867544f72a3Christian Maedercombine l = case l of
638ef5e65fd5713e2ef668ec48188867544f72a3Christian Maeder h : t -> concatMap (flip map h . flip (:)) (combine t)