module Exercise_9 where {-WETT-} import Data.List import Data.Maybe type Name = String type Valuation = [(Name,Bool)] data Atom = T | Var Name deriving (Eq, Show) data Literal = Pos Atom | Neg Atom deriving (Eq, Show) data Form = L Literal | Form :&: Form | Form :|: Form deriving (Eq, Show) type Clause = [Literal] type ConjForm = [Clause] {-T9.3.2-} top :: Literal top = Pos T bottom :: Literal bottom = Neg T {-T9.3.3-} clauseToForm :: Clause -> Form clauseToForm [] = L bottom clauseToForm ls = foldr ((:|:) . L) (L $ last ls) (init ls) conjToForm :: ConjForm -> Form conjToForm [] = L top conjToForm ds = foldr ((:&:) . clauseToForm) (clauseToForm $ last ds) (init ds) {-T9.3.4-} substLiteral :: Valuation -> Literal -> Literal substLiteral v l@(Pos (Var n)) = case lookup n v of Just b -> if b then top else bottom Nothing -> l substLiteral v l@(Neg (Var n)) = case lookup n v of Just b -> if b then bottom else top Nothing -> l substLiteral v l = l substClause :: Valuation -> Clause -> Clause substClause = map . substLiteral substConj :: Valuation -> ConjForm -> ConjForm substConj = map . substClause {-H9.2.1-} simpConj :: ConjForm -> ConjForm simpConj cnf = aux cnf [] where aux [] rs = rs aux (c:cs) rs | any (== top) c = aux cs rs | otherwise = if nc == [] then [[]] else aux cs (nc:rs) where nc = filter (/= bottom) c {-H9.2.2-} cnf :: Form -> ConjForm cnf (L l) = [[l]] cnf (p :&: q) = (cnf p) ++ (cnf q) cnf (p :|: q) = multiplyOut (cnf p) (cnf q) where multiplyOut [] qs = [] multiplyOut (p:ps) qs = (map (\x -> p ++ x) qs) ++ multiplyOut ps qs {-H9.2.3-} selectV :: ConjForm -> Maybe (Name, Bool) selectV [] = Nothing selectV cnf | null $ concatMap (filter (\l -> l /= top && l /= bottom)) cnf = Nothing | otherwise = maybe (Just (head $ vars cnf, True)) (\l -> Just (name l, sign l)) (findOLR cnf) where sign (Pos(Var _)) = True sign (Neg(Var _)) = False findOLR cnf = if cs == [] then Nothing else Just (head . sortOn name . concat $ cs) --One Literal Rule where cs = filter (\c -> length c == 1 && head c /= top && head c /= bottom) cnf name :: Literal -> Name name (Pos T) = "True" name (Neg T) = "False" name (Pos(Var n)) = n name (Neg(Var n)) = n vars :: ConjForm -> [Name] vars = sort . filter (\n -> n /= "True" && n /= "False") . concatMap (map name) {-H9.2.5-} satConj :: ConjForm -> Maybe Valuation satConj cnf = aux [] (simpConj cnf) where aux :: Valuation -> ConjForm -> Maybe Valuation aux v cnf | cnf == [] = Just v | cnf == [[]] = Nothing | otherwise = case aux (nv:v) (simpConj $ substConj (nv:v) cnf ) of Just vv -> Just vv Nothing -> aux ((negate nv):v) (simpConj $ substConj ((negate nv):v) cnf) where nv = fromJust $ selectV cnf negate (n, True) = (n, False) negate (n, False) = (n, True) {-H9.2.6-} sat :: Form -> Maybe Valuation sat = satConj . cnf {-TTEW-}