diff options
| -rw-r--r-- | src/Lib.hs | 332 |
1 files changed, 218 insertions, 114 deletions
@@ -1,60 +1,73 @@ -{-# LANGUAGE GADTs #-} -{-# LANGUAGE LambdaCase #-} -{-# LANGUAGE RankNTypes #-} {-# LANGUAGE TupleSections #-} +{-# LANGUAGE BangPatterns #-} module Lib where -import Data.Char (chr, ord) -import qualified Data.List as L -import qualified Data.Map as M -import Data.Maybe (fromJust) -import qualified Data.Set as S -import Debug.Trace () -import Parser -import qualified Text.Parsec as Parsec +import Data.Char ( chr + , ord + ) +import qualified Data.List as L +import qualified Data.Map as M +import Data.Maybe ( fromJust ) +import qualified Data.Set as S +import Debug.Trace ( traceShowId + , traceShow + ) +import Parser +import qualified Text.Parsec as Parsec mget :: (Ord a) => a -> M.Map a b -> b mget a m = fromJust $ M.lookup a m automatizem :: M.Map Addend Int -> Matrix -> DFA [Int] Int -automatizem dir (MEq as bs) = eq (fromIntegral $ length dir) (map (`mget` dir) as) (map (`mget` dir) bs) -automatizem dir (MLe a b) = le (mget a dir) (mget b dir) -automatizem dir (MLt a b) = lt (mget a dir) (mget b dir) +automatizem dir (MEq as bs) = + eq (fromIntegral $ length dir) (map (`mget` dir) as) (map (`mget` dir) bs) +automatizem dir (MLe a b) = le (mget a dir) (mget b dir) +automatizem dir (MLt a b) = lt (mget a dir) (mget b dir) automatizem dir (MAnd x y) = conj (automatizem dir x) (automatizem dir y) -automatizem dir (MOr x y) = disj (automatizem dir x) (automatizem dir y) -automatizem dir (MNot x) = compl (automatizem dir x) +automatizem dir (MOr x y) = disj (automatizem dir x) (automatizem dir y) +automatizem dir (MNot x ) = compl (automatizem dir x) automatize :: M.Map Addend Int -> QNMFormula -> NFA [Int] Int -automatize dir (QNMFormula [] m) = minimize (fromIntegral $ length dir) $ nondeterminize $ automatizem dir m +automatize dir (QNMFormula [] m) = + let dfa@( DFA s _ _ _) = automatizem dir m + mdfa@(DFA s' _ _ _) = rmdist dfa (fromIntegral (length dir)) + !t = (traceShowId $ (length s, length s')) + in minimize (fromIntegral $ length dir) $ nondeterminize $ mdfa automatize dir (QNMFormula (Neg : quas) m) = let nfa = automatize dir (QNMFormula quas m) - in minimize (fromIntegral (length dir)) (ncompl nfa) + in minimize (fromIntegral (length dir)) (ncompl nfa) + where + rmmin d = rmdist d (fromIntegral (length dir)) + ncompl = nondeterminize . compl . rmmin . determinize automatize dir (QNMFormula (Qua (Exists, v) : quas) m) = let nfa = automatize dir (QNMFormula quas m) - in case M.lookup (Var v) dir of - Nothing -> nfa + in case M.lookup (Var v) dir of + Nothing -> nfa (Just i) -> minimize (fromIntegral $ length dir) $ existentialize i nfa assign :: S.Set Addend -> M.Map Addend Int assign xs = M.fromList (zip (S.toList xs) [0 ..]) collect :: Matrix -> S.Set Addend -collect (MEq as bs) = S.fromList (as ++ bs) -collect (MLe a b) = S.fromList [a, b] -collect (MLt a b) = S.fromList [a, b] -collect (MAnd x y) = S.union (collect x) (collect y) -collect (MOr x y) = S.union (collect x) (collect y) -collect (MNot x) = collect x +collect (MEq as bs) = S.fromList (as ++ bs) +collect (MLe a b ) = S.fromList [a, b] +collect (MLt a b ) = S.fromList [a, b] +collect (MAnd x y ) = S.union (collect x) (collect y) +collect (MOr x y ) = S.union (collect x) (collect y) +collect (MNot x ) = collect x literals :: M.Map Addend Int -> [[Int]] literals m = - let addends = L.sortOn snd (M.toList m) - reversedLiterals = map (\(a, i) -> addendReverseBinary a) addends - max = L.maximum (map length reversedLiterals) - paddedReversed = map (\x -> x ++ replicate (max - length x) 0) reversedLiterals - padded = map reverse paddedReversed - in L.transpose padded + let + addends = L.sortOn snd (M.toList m) + reversedLiterals = map (\(a, i) -> addendReverseBinary a) addends + max = L.maximum (map length reversedLiterals) + paddedReversed = + map (\x -> x ++ replicate (max - length x) 0) reversedLiterals + padded = map reverse paddedReversed + in + L.transpose padded addendReverseBinary :: Addend -> [Int] addendReverseBinary (Var x) = [] @@ -66,12 +79,12 @@ reverseBinary n = fromIntegral (mod n 2) : reverseBinary (div n 2) eval :: QNMFormula -> Bool eval f@(QNMFormula q m) = - let dir = (assign $ collect m) - nfa = automatize dir f + let dir = (assign $ collect m) + nfa = automatize dir f input = literals (assign $ collect m) - in runNFA nfa input + in runNFA nfa input -data State a = Single a | Double (State a, State a) | Multi [State a] deriving (Eq, Ord, Show) +data State a = S a | Double (State a, State a) | Multi [State a] deriving (Eq, Ord, Show) data DFA c a = DFA [State a] (State a) [State a] (State a -> c -> State a) @@ -80,35 +93,137 @@ data NFA c a = NFA [State a] [State a] [State a] (State a -> c -> [State a]) runDFA :: (Ord a) => DFA c a -> [c] -> Bool runDFA (DFA _ start accepts f) cs = foldl f start cs `elem` accepts +minimize :: (Ord a) => Integer -> NFA [Int] a -> NFA [Int] a +minimize n nfa@(NFA _ starts accepts f) = NFA states' starts' accepts' f + where + states' = closure nfa (chars n) starts + starts' = starts `L.intersect` states' + accepts' = accepts `L.intersect` states' + + +rmdist :: (Ord a, Show a) => DFA [Int] a -> Integer -> DFA [Int] a +rmdist dfa@(DFA states start accepts f) n = + let + statecandidates = minimize2 dfa n + states' = map head statecandidates + start' = head $ head $ filter (\c -> L.elem start c) statecandidates + accepts' = L.intersect accepts states' + f' s c = + let s' = f s c + in head $ head $ filter (\c -> L.elem s' c) statecandidates + in + DFA states' start' accepts' f' + + +minimize2 :: (Ord a, Show a) => DFA [Int] a -> Integer -> [[State a]] +minimize2 dfa@(DFA states start accepts f) n = + let p0 = [states L.\\ accepts, accepts] in minrec dfa n p0 + +minrec + :: (Ord a, Show a) => DFA [Int] a -> Integer -> [[State a]] -> [[State a]] +minrec dfa n pklast = + let next = concatMap (\part -> minimize3 dfa n pklast [] part) pklast + in if normpartition next == normpartition pklast + then next + else minrec dfa n next + +normpartition :: Ord a => [[a]] -> S.Set (S.Set a) +normpartition xs = S.fromList (map S.fromList xs) + + +minimize3 + :: (Ord a, Show a) + => DFA [Int] a + -> Integer + -> [[State a]] + -> [[State a]] + -> [State a] + -> [[State a]] +minimize3 dfa@(DFA states starts accepts f) n pklast pk [] = pk +minimize3 dfa@(DFA states starts accepts f) n pklast [] (x : xs) = + minimize3 dfa n pklast [[x]] xs +minimize3 dfa@(DFA states starts accepts f) n pklast pk (x : xs) = + let ys = filter (\s -> equivall dfa pklast (chars n) (head s) x) pk + in if ys == [] + then minimize3 dfa n pklast ([x] : pk) xs + else + let coll = (head ys) + trunc = L.delete coll pk + new = x : coll + pk' = new : trunc + in minimize3 dfa n pklast pk' xs + +equivall + :: (Eq a) + => DFA [Int] a + -> [[State a]] + -> [[Int]] + -> (State a) + -> (State a) + -> Bool +equivall dfa partition cs x y = all (\c -> not $ dist dfa partition c x y) cs + +states = S <$> [0, 1, 2, 3, 4] +start = S 0 +accepts = [S 4] +f (S 0) [0] = S 1 +f (S 0) [1] = S 2 +f (S 1) [0] = S 1 +f (S 1) [1] = S 3 +f (S 2) [0] = S 1 +f (S 2) [1] = S 2 +f (S 3) [0] = S 1 +f (S 3) [1] = S 4 +f (S 4) [0] = S 1 +f (S 4) [1] = S 2 +dfa = DFA states start accepts f +p0 = [states L.\\ accepts, accepts] +p1 = concatMap (minimize3 dfa 1 p0 []) p0 +p2 = concatMap (minimize3 dfa 1 p1 []) p1 +minp = minimize2 dfa 1 + + +dist + :: (Eq a) + => DFA [Int] a + -> [[State a]] + -> [Int] + -> (State a) + -> (State a) + -> Bool +dist (DFA states starts accepts f) partition c x y = + (findset partition (f x c)) /= (findset partition (f y c)) + +findset :: (Eq a) => [[State a]] -> State a -> [State a] +findset xs x = head (filter (\s -> L.elem x s) xs) + runNFA :: (Ord a) => NFA c a -> [c] -> Bool runNFA (NFA _ starts accepts f) cs = - foldl (\xs c -> L.nub $ concatMap (`f` c) xs) starts cs `L.intersect` accepts /= [] + foldl (\xs c -> L.nub $ concatMap (`f` c) xs) starts cs + `L.intersect` accepts + /= [] reversal :: (Ord a) => NFA c a -> NFA c a reversal (NFA states starts accepts f) = NFA states accepts starts f' - where - f' s c = filter (\state -> s `elem` f state c) states + where f' s c = filter (\state -> s `elem` f state c) states eq :: Integer -> [Int] -> [Int] -> DFA [Int] Int eq n is js = determinize $ minimize n $ reversal $ nondeterminize dfa - where - states = Single <$> [- (length js - 1) .. length is - 1 + 1] - start = Single 0 - accepts = [Single 0] - rejector = last states - f :: State Int -> [Int] -> State Int - f carrystate@(Single carry) c = - if carrystate == rejector - then rejector - else - let si = sum (map (c !!) is) - sj = sum (map (c !!) js) - parityok = mod (carry + si) 2 == mod sj 2 - newcarry = div (carry + si - sj) 2 - in if parityok - then Single newcarry - else rejector - dfa = DFA states start accepts f + where + states = S <$> [-(length js - 1) .. length is - 1 + 1] + start = S 0 + accepts = [S 0] + rejector = last states + f :: State Int -> [Int] -> State Int + f carrystate@(S carry) c = if carrystate == rejector + then rejector + else + let si = sum (map ((c) !!) (is)) + sj = sum (map (c !!) (js)) + parityok = mod (carry + si) 2 == mod sj 2 + newcarry = div (carry + si - sj) 2 + in if parityok then S newcarry else rejector + dfa = DFA states start accepts f le :: Int -> Int -> DFA [Int] Int le = less LessEqual @@ -119,36 +234,37 @@ lt = less LessThan data LessType = LessEqual | LessThan deriving (Eq, Ord, Show) less :: LessType -> Int -> Int -> DFA [Int] Int -less lt i j = DFA [Single 0, Single 1, Single 2] (Single 0) accepts f - where - accepts = if lt == LessEqual then [Single 0, Single 2] else [Single 2] - f s c = case (s, (c !! i, c !! j)) of - (Single 0, (1, 1)) -> Single 0 - (Single 0, (0, 0)) -> Single 0 - (Single 0, (1, 0)) -> Single 1 - (Single 0, _) -> Single 2 - (Single 1, _) -> Single 1 - (_, _) -> Single 2 +less lt i j = DFA [S 0, S 1, S 2] (S 0) accepts f + where + accepts = if lt == LessEqual then [S 0, S 2] else [S 2] + f s c = case (s, (c !! i, c !! j)) of + (S 0, (1, 1)) -> S 0 + (S 0, (0, 0)) -> S 0 + (S 0, (1, 0)) -> S 1 + (S 0, _ ) -> S 2 + (S 1, _ ) -> S 1 + (_ , _ ) -> S 2 prod :: [a] -> [b] -> [(a, b)] -prod xs [] = [] -prod [] ys = [] -prod (x : xs) ys = fmap (x,) ys ++ prod xs ys +prod xs [] = [] +prod [] ys = [] +prod (x : xs) ys = fmap (x, ) ys ++ prod xs ys data JunctionType = Conj | Disj deriving (Eq, Ord, Show) junction :: (Ord a) => JunctionType -> DFA c a -> DFA c a -> DFA c a junction jt (DFA states1 start1 accepts1 f1) (DFA states2 start2 accepts2 f2) = DFA states' start' accepts' f' - where - newStates = prod states1 states2 - states' = Double <$> newStates - start' = Double (start1, start2) - accepts' = - if jt == Conj - then Double <$> prod accepts1 accepts2 - else Double <$> filter (\(s, t) -> s `elem` accepts1 || t `elem` accepts2) newStates - f' (Double (s, t)) c = Double (f1 s c, f2 t c) + where + newStates = prod states1 states2 + states' = Double <$> newStates + start' = Double (start1, start2) + accepts' = if jt == Conj + then Double <$> prod accepts1 accepts2 + else + Double + <$> filter (\(s, t) -> s `elem` accepts1 || t `elem` accepts2) newStates + f' (Double (s, t)) c = Double (f1 s c, f2 t c) conj :: (Ord a) => DFA c a -> DFA c a -> DFA c a conj = junction Conj @@ -157,14 +273,11 @@ disj :: (Ord a) => DFA c a -> DFA c a -> DFA c a disj = junction Disj compl :: (Ord a) => DFA c a -> DFA c a -compl (DFA states start accepts f) = - DFA states start (states L.\\ accepts) f +compl (DFA states start accepts f) = DFA states start (states L.\\ accepts) f nondeterminize :: (Ord a) => DFA c a -> NFA c a -nondeterminize (DFA states start accepts f) = - NFA states [start] accepts f' - where - f' s c = [f s c] +nondeterminize (DFA states start accepts f) = NFA states [start] accepts f' + where f' s c = [f s c] change :: [a] -> Int -> a -> [a] change xs idx b = take idx xs ++ [b] ++ drop (idx + 1) xs @@ -172,45 +285,36 @@ change xs idx b = take idx xs ++ [b] ++ drop (idx + 1) xs closure :: (Ord a) => NFA c a -> [c] -> [State a] -> [State a] closure nfa@(NFA states starts accepts f) cs initstates = let new = concatMap (\state -> concatMap (f state) cs) initstates - in if L.nub new L.\\ L.nub initstates /= [] + in if L.nub new L.\\ L.nub initstates /= [] then closure nfa cs (L.nub $ new ++ initstates) else L.nub initstates existentialize :: (Ord a) => Int -> NFA [Int] a -> NFA [Int] a -existentialize idx nfa@(NFA states starts accepts f) = - NFA states starts' accepts f' - where - zeroer = replicate 50 0 - oneer = change zeroer idx 1 - starts' = closure nfa [zeroer, oneer] starts - f' s c = f s (change c idx 0) ++ f s (change c idx 1) +existentialize idx nfa@(NFA states starts accepts f) = NFA states + starts' + accepts + f' + where + zeroer = replicate 50 0 + oneer = change zeroer idx 1 + starts' = closure nfa [zeroer, oneer] starts + f' s c = f s (change c idx 0) ++ f s (change c idx 1) powerset :: [a] -> [[a]] -powerset [] = [[]] +powerset [] = [[]] powerset (x : xs) = let rest = powerset xs in map (x :) rest ++ rest determinize :: (Ord a) => NFA c a -> DFA c a -determinize (NFA states start accepts f) = - DFA states' start' accepts' f' - where - newStates = map L.sort $ powerset states - states' = Multi <$> newStates - start' = Multi $ L.sort start - accepts' = Multi <$> filter (\state' -> state' `L.intersect` accepts /= []) newStates - f' (Multi s) c = Multi $ L.nub $ L.sort $ concatMap (`f` c) s +determinize (NFA states start accepts f) = DFA states' start' accepts' f' + where + newStates = map L.sort $ powerset states + states' = Multi <$> newStates + start' = Multi $ L.sort start + accepts' = + Multi <$> filter (\state' -> state' `L.intersect` accepts /= []) newStates + f' (Multi s) c = Multi $ L.nub $ L.sort $ concatMap (`f` c) s -ncompl :: (Ord a) => NFA c a -> NFA c a -ncompl = nondeterminize . compl . determinize chars :: Integer -> [[Int]] chars 0 = [[]] -chars n = - let r = chars (n -1) - in map (1 :) r ++ map (0 :) r - -minimize :: (Ord a) => Integer -> NFA [Int] a -> NFA [Int] a -minimize n nfa@(NFA _ starts accepts f) = NFA states' starts' accepts' f - where - states' = closure nfa (chars n) starts - starts' = starts `L.intersect` states' - accepts' = accepts `L.intersect` states' +chars n = let r = chars (n - 1) in map (1 :) r ++ map (0 :) r |