1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
|
{-# LANGUAGE GADTs #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TupleSections #-}
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
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 (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)
automatize :: M.Map Addend Int -> QNMFormula -> NFA [Int] Int
automatize dir (QNMFormula [] m) = minimize (fromIntegral $ length dir) $ nondeterminize $ automatizem dir m
automatize dir (QNMFormula (Neg : quas) m) =
let nfa = automatize dir (QNMFormula quas m)
in minimize (fromIntegral (length dir)) (ncompl nfa)
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
(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
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
addendReverseBinary :: Addend -> [Int]
addendReverseBinary (Var x) = []
addendReverseBinary (Con n) = reverseBinary n
reverseBinary :: Integer -> [Int]
reverseBinary 0 = []
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
input = literals (assign $ collect m)
in runNFA nfa input
data State a = Single 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)
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
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 /= []
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
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
le :: Int -> Int -> DFA [Int] Int
le = less LessEqual
lt :: Int -> Int -> DFA [Int] Int
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
prod :: [a] -> [b] -> [(a, b)]
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)
conj :: (Ord a) => DFA c a -> DFA c a -> DFA c a
conj = junction Conj
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
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]
change :: [a] -> Int -> a -> [a]
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 /= []
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)
powerset :: [a] -> [[a]]
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
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'
|
