module Exercise09 where import Types import Data.List (sort, sortOn, intersect, intersectBy, nub, nubBy, delete, deleteBy, minimumBy, map, partition) import Data.Ord (Down(Down), compare) import qualified Data.HashMap.Lazy as HM import qualified Data.IntMap.Lazy as IM -- things from the tutorial instance Show Polarity where show Pos = "" show Neg = "~" instance Show ELiteral where show (Literal p a) = show p ++ a lName :: Literal -> Name lName (Literal _ n) = n lPor :: Literal -> Polarity lPor (Literal por _) = por lPos :: Name -> Literal lPos = Literal Pos lNeg :: Name -> Literal lNeg = Literal Neg lIsPos :: Literal -> Bool lIsPos (Literal p _) = p == Pos lIsNeg :: Literal -> Bool lIsNeg = not . lIsPos lNegate :: Literal -> Literal lNegate (Literal Pos n) = Literal Neg n lNegate (Literal Neg n) = Literal Pos n complements :: Literal -> Literal -> Bool complements (Literal p n) (Literal p' n') = p /= p' && n == n' evalLiteral :: Valuation -> Literal -> Bool evalLiteral val l@(Literal _ n) | lIsPos l = n `elem` val | otherwise = n `notElem` val evalClause :: Valuation -> Clause -> Bool evalClause = any . evalLiteral eval :: Valuation -> ConjForm -> Bool eval = all . evalClause clauseIsTauto :: Clause -> Bool clauseIsTauto [] = False clauseIsTauto (l:ls) = lNegate l `elem` ls || clauseIsTauto ls -- homework starts here -- feel free to change behaviour and type resolve :: Name -> Clause -> Clause -> Clause resolve n cp cn = (filter (\l -> lIsNeg l || (lName l /= n)) cp) ++ (filter (\l -> lIsPos l || (lName l /= n)) cn) -- feel free to change behaviour and type resolvants :: KeyClause -> KeyClause -> [(Resolve, Clause)] --Key = Int -- EKeyClause = (Key, EClause) --EResolve = Resolve EName Key Key resolvants kc1 kc2 = [if lIsPos var then aux (lName var) 1 else aux (lName var) 2 | var <- commonVars] where [key1, key2] = map fst [kc1, kc2] [c1, c2] = map snd [kc1, kc2] commonVars = intersectBy (\l1 l2 -> lName l1 == lName l2 && lIsPos l1 == lIsNeg l2) c1 c2 aux :: Name -> Int -> (Resolve, Clause) aux n posK | posK == 1 = (Resolve n key1 key2, resolve n c1 c2) | posK == 2 = (Resolve n key2 key1, resolve n c2 c1) -- proof checking -- don't change the type nor expected behaviour proofCheck :: ConjForm -> Proof -> Bool -- EProof = Refutation [EResolve] | Model EValuation -- EValuation = [EName] proofCheck cjF (Model vs) = all (any (\l -> (lName l `elem` vs ) == lIsPos l)) cjF proofCheck cjF (Refutation steps) = null $last $foldl aux cjF steps where aux :: ConjForm -> Resolve -> ConjForm aux oldF (Resolve n key1 key2) = oldF ++ [resolve n (oldF !! key1) (oldF !! key2)] arrange :: (Int, Int) -> [(Int, Int)] -> [(Int, Int)] arrange (nv,ni) [] = [(nv,ni)] arrange (nv,ni) ((v',i'):xs) = if nv <= v' then (nv,ni) : ((v',i'):xs) else (v',i') : (arrange (nv,ni) xs) addNew :: ScoreTab -> ScoreTab -> EKeyConjForm -> (ScoreTab, ScoreTab) addNew p n [] = (p,n) addNew p n ((k,c):kcs) = addNew np nn kcs where (np,nn) = aux' k c (p,n) aux' :: Int -> Clause -> (ScoreTab, ScoreTab) -> (ScoreTab, ScoreTab) aux' idx cl (oldP, oldN) = foldl (\(oP, oN) l -> if lPor l == Pos then (HM.insertWith f (lName l) [(v, idx)] oP, oN) else (oP, HM.insertWith f (lName l) [(v, idx)] oN) ) (oldP, oldN) cl' where cl' = nub cl v = length cl' f [new] old = arrange new old convert :: EKeyConjForm -> (ScoreTab, ScoreTab) convert = addNew tPos tNeg where tPos = HM.empty :: ScoreTab tNeg = HM.empty :: ScoreTab deleteProcessed :: ScoreTab -> ScoreTab -> KeyClause-> (ScoreTab, ScoreTab) deleteProcessed p n (k,c) = ( foldl (\map key -> HM.adjust f key map) p posN, foldl (\map key -> HM.adjust f key map) n negN ) where (posL, negL) = partition lIsPos c posN = map lName posL negN = map lName negL f = deleteBy (\(_,a) (_,b) -> a == b) (0,k) complementAll :: Clause -> [Literal] -> Bool complementAll [] _ = True complementAll _ [] = False complementAll xs ls = and [ or [x `complements` l | l <- ls] | x <- xs] -- feel free to change behaviour and type selClause :: SelClauseStrategy -- KeyConjForm -> ScoreTab -> ScoreTab -> EKeyConjForm -> (Name, Int, Int) selClause u p n [] = if not (null s1) then head s1 else s2 where commonKeys = [let (Just x, Just y) = (HM.lookup k p, HM.lookup k n) in if snd (head y) /= snd (head x) then (k, head x, head y) else if (length x >= 2 && length y >= 2) then if fst (x!!1) <= fst (y!!1) then (k, x!!1, head y) else (k, head x, y!!1) else if length x >= 2 then (k, x!!1, head y) else (k, head x, y!!1) | k <- intersect (HM.keys p) (HM.keys n), let (Just x, Just y) = (HM.lookup k p, HM.lookup k n) in (not (null x)) && (not (null y)) && (take 2 x /= take 2 y) ] s1 = [(k, snd pc, snd nc) | (k, pc, nc) <- commonKeys, fst pc == 1, fst nc == 1] s2 = if not (null commonKeys) then let (nameL, idxP, idxN) = minimumBy (\(_, (a,_), (b,_)) (_, (c,_),(d,_)) -> compare (a+b) (c+d)) commonKeys in (nameL, snd idxP, snd idxN) else ("", -1, -1) selClause u p n pSingle = if not (null s1') then head s1 else if not (null s4) then head s4 else if ((fst s2 - 1) <= (fst s3 - 2)) && (fst s2 /= 0) then snd s2 else if (fst s2 /= 0) && (fst s3 == 0) then snd s2 else snd s3 where pLits = concat (map snd pSingle) s1' = sortOn (\x -> length (snd x)) [ (k, u IM.! k) | k <- IM.keys u, complementAll (nub (u IM.! k)) pLits] s1 = if not (null s1') then let (idx,c) = head s1' in [if lIsPos l then (lName l, idx, idx') else (lName l, idx', idx) | l <- nub c, (idx',[l']) <- pSingle, l `complements` l'] else [] s2' = [if lIsPos l then let Just x = HM.lookup (lName l) n in (fst (head x), (lName l, i, snd (head x) )) else let Just x = HM.lookup (lName l) p in (fst (head x), (lName l, snd (head x), i)) | (i,[l]) <- pSingle, if lIsPos l then HM.member (lName l) n && HM.lookup (lName l) n /= Just [] else HM.member (lName l) p && HM.lookup (lName l) p /= Just [] ] s2 = if not (null s2') then minimumBy (\(a,_) (b,_) -> compare a b) s2' else (0,("", -1, -1)) -- commonKeys = intersect (HM.keys p) (HM.keys n) -- minPs = [let Just x = HM.lookup k p in head x | k <- commonKeys, HM.lookup k p /= Just []] -- minNs = [let Just x = HM.lookup k n in head x | k <- commonKeys, HM.lookup k n /= Just []] commonKeys = [let (Just x, Just y) = (HM.lookup k p, HM.lookup k n) in if snd (head y) /= snd (head x) then (k, head x, head y) else if (length x >= 2 && length y >= 2) then if fst (x!!1) <= fst (y!!1) then (k, x!!1, head y) else (k, head x, y!!1) else if length x >= 2 then (k, x!!1, head y) else (k, head x, y!!1) | k <- intersect (HM.keys p) (HM.keys n), let (Just x, Just y) = (HM.lookup k p, HM.lookup k n) in (not (null x)) && (not (null y)) && (take 2 x /= take 2 y) ] s4 = [(k, snd pc, snd nc) | (k, pc, nc) <- commonKeys, fst pc == 1, fst nc == 1] s3 = if not (null commonKeys) then let (nameL, idxP, idxN) = minimumBy (\(_,(a,_),(b,_)) (_,(c,_),(d,_)) -> compare (a+b) (c+d)) commonKeys in (fst idxP + fst idxN, (nameL, snd idxP, snd idxN)) else (0,("", -1, -1)) -- feel free to change behaviour and type resolutionParam :: SelClauseStrategy -> ConjForm -> (Proof, KeyConjForm) -- SelClauseStrategy -- KeyConjForm -> ScoreTab -> ScoreTab -> EKeyConjForm -> (Name, Int, Int) -- EProof = Refutation [EResolve] | Model EValuation -- EValuation = [EName] -- EResolve = Resolve EName Key Key -- if Model return processed, if refu return unprocessed ++ processed resolutionParam strat cj = aux kCj (IM.empty) kCj tP tN [] [] where kCj = toKeyConjForm (zip [0..length cj - 1] cj) (tP, tN) = convert (zip [0..length cj - 1] cj) aux :: KeyConjForm -> KeyConjForm -> KeyConjForm -> ScoreTab -> ScoreTab -> EKeyConjForm -> [EResolve] -> (Proof, KeyConjForm) aux oldKCj p u tPos tNeg pSingle rs | u == IM.empty = (Model (extractModel (snd (unzip (toEKeyConjForm p)))), p) | uc == ("", -1, -1) = (Model (extractModel (snd (unzip (toEKeyConjForm oldKCj)))), p) | null nu = (Refutation rs', oldKCj) | otherwise = aux newKCj p' u' tPos' tNeg' pSingle' rs' where uc'@(nameL', idxP', idxN') = strat u tPos tNeg pSingle -- resolve found-able nu' = nub (resolve nameL' (oldKCj IM.! idxP') (oldKCj IM.! idxN')) uc@(nameL, idxP, idxN) = if uc' /= ("", -1, -1) && (notElem nu' (IM.elems p)) then uc' else aux' u p nr = Resolve nameL idxP idxN nu = nub (resolve nameL (oldKCj IM.! idxP) (oldKCj IM.! idxN)) newKCj = IM.insert (IM.size oldKCj) nu oldKCj p' = foldl (\map i -> IM.insert i (nub (newKCj IM.! i)) map) p [idxP, idxN] --p ++ map (\i -> oldKCj IM.! i) [idxP, idxN] u' = let u'' = foldl (\map i -> IM.delete i map) u [idxP, idxN] in IM.insert (IM.size oldKCj) nu u'' rs' = rs ++ [nr] (tPos',tNeg') = let (tPos'',tNeg'') = foldl (\(x,y) i -> deleteProcessed x y (i, oldKCj IM.! i)) (tPos, tNeg) [idxP, idxN] in addNew tPos'' tNeg'' [(IM.size oldKCj, nu)] pSingle' = foldl (\lst i -> if length (oldKCj IM.! i) == 1 then ((i, oldKCj IM.! i):lst) else lst) pSingle [idxP, idxN] aux' :: KeyConjForm -> KeyConjForm -> (Name, Int, Int) aux' un pr = aux'' un' pr where elemsP = IM.elems pr kss = IM.keys un un' = foldl (\map i -> if subSummed (map IM.! i) elemsP then IM.delete i map else map) un kss aux'' :: KeyConjForm -> KeyConjForm -> (Name, Int, Int) aux'' un'' pr'' | un'' == IM.empty = ("", -1, -1) | not (null valid) = let (Resolve nm i1 i2, _) = head valid in (nm, i1, i2) | otherwise = aux' (IM.delete ky un'') pr'' where elemsPr = IM.elems pr'' (ky:ks) = IM.keys un'' x = un'' IM.! ky valid = filter (\(_,b) -> subSummed (nub b) elemsPr) (concatMap (resolvants (ky, x)) (toEKeyConjForm pr'')) -- KeyClause -> KeyClause -> [(Resolve, Clause)] subSummed :: Clause -> ConjForm -> Bool subSummed c cj = or [and [l `elem` cl | l <- c] | cl <- cj] -- {-WETT-} -- don't change the type; instantiate your best resolution prover here -- Please leave some comments for the MC Jr to understand your ideas and code :') resolution :: ConjForm -> (Proof, KeyConjForm) resolution cj = resolutionParam selClause (map nub cj) -- {-TTEW-} -- extract a model as described on https://lara.epfl.ch/w/_media/sav08/gbtalk.pdf instance Ord Polarity where Neg <= Pos = False _ <= _ = True instance Ord ELiteral where (Literal p a) <= (Literal p' a') = a < a' || a == a' && p <= p' extractModel :: ConjForm -> Valuation extractModel = run [] . sort . map (sortOn Down) where run val [] = val run val (c:cs) | evalClause val c = run val cs | otherwise = run (lName (head c):val) cs testXS :: ConjForm testXS = [[ Literal Neg "5", Literal Pos "6", Literal Pos "6", Literal Neg "6", Literal Neg "9", Literal Pos "8", Literal Pos "2"],[ Literal Neg "10"],[ Literal Pos "8", Literal Pos "3", Literal Neg "8", Literal Neg "5", Literal Pos "3", Literal Neg "9", Literal Neg "1"],[ Literal Pos "10", Literal Neg "5", Literal Pos "4"],[ Literal Pos "9", Literal Pos "3", Literal Pos "9", Literal Pos "10", Literal Neg "7"],[ Literal Pos "5", Literal Neg "8", Literal Pos "10", Literal Neg "7", Literal Neg "1"],[ Literal Pos "10", Literal Pos "8", Literal Neg "9", Literal Pos "2"],[ Literal Pos "5", Literal Neg "1", Literal Neg "4", Literal Neg "5", Literal Pos "5", Literal Pos "4", Literal Neg "1"]]