Fixed variable bug with de morgan.
2 Name: sml - Simple Modal Logic Lib.
3 Description: sml provides classes for simple modal logic formulae construction and reduction. It also features a disfunctional parser for the SML syntax.
4 Author: Eugen Sawin <sawine@informatik.uni-freiburg.de>
9 # edit your formulae here
13 formula1 = Imp([Eq([p, q]), r])
14 formula2 = Not([Or([p, q])])
15 formula3 = Not([Not([p])])
16 formula4 = Imp([Box([Imp([Diamond([p]), p])]), Box([Imp([p, Box([p])])])])
17 formula = formula4 # choose your formula here
19 args = parse_arguments()
21 scanner = Scanner(TOKENS)
22 parser = Parser(SYNTAX, scanner)
23 (accepted, out, tree_nodes) = parser.parse(args.formula)
27 tree = SyntaxTree(out, tree_nodes)
30 print "formula: \t\t\t%s (%i)" % (formula, formula.depth())
31 formula = expand_imp_eq(formula)
32 print "expanded -> and <->: \t\t%s (%i)" % (formula, formula.depth())
33 formula = de_morgan(formula)
34 print "reduced ~: \t\t\t%s (%i)" % (formula, formula.depth())
35 formula = reduce_iter(formula)
36 print "reduced iterated modalities: \t%s (%i)" % (formula, formula.depth())
37 formula = reduce_iter(dist_mod((formula)))
38 print "distributed modalities+: \t%s (%i)" % (formula, formula.depth())
42 return [fun(v) for v in f.values]
44 def expand_imp_eq(formula):
45 expmap = {IMP: lambda (a, b): Or([Not([a]), b]),
46 EQ: lambda (a, b): And([Or([Not([a]), b]), Or([a, Not([b])])])}
47 if not isinstance(formula, Operator):
49 if formula.id in expmap:
50 return expmap[formula.id](values(expand_imp_eq, formula))
51 return formula.__class__(values(expand_imp_eq, formula))
53 def de_morgan(formula):
54 negmap = {AND: lambda (a, b): Or([negate(a), negate(b)]),
55 OR: lambda (a, b): And([negate(a), negate(b)]),
56 BOX: lambda (a,): Diamond([negate(a)]),
57 DIAMOND: lambda (a,): Box([negate(a)]),
58 VARIABLE: lambda (a,): Not([Variable([a])]),
61 return negmap[f.id](f.values)
62 if not isinstance(formula, Operator):
65 return negate(formula.values[0])
66 return formula.__class__(values(de_morgan, formula))
68 def reduce_iter(formula):
69 redset = set(((BOX, BOX), (DIAMOND, DIAMOND), (DIAMOND, BOX), (BOX, DIAMOND)))
70 if not isinstance(formula, Operator) or not isinstance(formula.values[0], Operator):
72 ids = (formula.id, formula.values[0].id)
74 return reduce_iter(formula.values[0])
75 return formula.__class__(values(reduce_iter, formula))
77 def dist_mod(formula):
78 distmap = {(BOX, AND): lambda (a, b): And([Box([a]), Box([b])]),
79 (DIAMOND, OR): lambda (a, b): Or([Diamond([a]), Diamond([b])]),
80 (BOX, OR): lambda (a, b): (isinstance(a, Box) or isinstance(b, Box))
81 and Or([Box([a]), Box([b])]) or Box([Or([a, b])]),
82 (DIAMOND, AND): lambda (a, b): (isinstance(a, Diamond) or isinstance(b, Diamond))
83 and And([Diamond([a]), Diamond([b])]) or Diamond([And([a, b])])}
84 if not isinstance(formula, Operator) or not isinstance(formula.values[0], Operator):
86 ids = (formula.id, formula.values[0].id)
88 return distmap[ids](values(dist_mod, formula.values[0]))
89 return formula.__class__(values(dist_mod, formula))
102 class Operator(object):
103 def __init__(self, id, arity, values):
110 if self.id in (BOX, DIAMOND):
111 return 1 + self.values[0].depth()
113 return self.values[0].depth()
114 return max(self.values[0].depth(), self.values[1].depth())
118 out = str(self.values[0])
120 out = self.id + str(self.values[0])
121 elif self.arity == 2:
122 out = "(" + str(self.values[0]) + " " + self.id + " " + str(self.values[1]) + ")"
127 def __init__(self, values):
128 Operator.__init__(self, NOT, Not.arity, values)
134 def __init__(self, values):
135 Operator.__init__(self, AND, And.arity, values)
139 def __init__(self, values):
140 Operator.__init__(self, OR, Or.arity, values)
144 def __init__(self, values):
145 Operator.__init__(self, IMP, Imp.arity, values)
149 def __init__(self, values):
150 Operator.__init__(self, EQ, Eq.arity, values)
154 def __init__(self, values):
155 Operator.__init__(self, BOX, Box.arity, values)
157 class Diamond(Operator):
159 def __init__(self, values):
160 Operator.__init__(self, DIAMOND, Diamond.arity, values)
162 class Variable(Operator):
164 def __init__(self, values):
165 Operator.__init__(self, VARIABLE, Variable.arity, values)
169 def __init__(self, values):
170 Operator.__init__(self, LB, Lb.arity, values)
174 def __init__(self, values):
175 Operator.__init__(self, RB, Rb.arity, values)
177 class Formula(object):
181 TOKENS = {re.compile("\("): Lb,
182 re.compile("\)"): Rb,
183 re.compile("~"): Not,
184 re.compile("&"): And,
185 re.compile("\|"): Or,
186 re.compile("->"): Imp,
187 re.compile("<->"): Eq,
188 re.compile("\[\]"): Box,
189 re.compile("<>"): Diamond,
190 re.compile("[a-z]+"): Variable}
192 class Scanner(object):
193 def __init__(self, tokens, source=None):
197 while self.i < len(self.source):
199 for p, token in self.tokens.iteritems():
200 m = p.match(self.source[self.i:])
204 return (token, value)
207 def reset(self, source):
222 SYNTAX = ((Variable,),
233 def __init__(self, parent, value):
237 def addChild(self, value):
238 self.children.append(self, node)
240 class Parser(object):
241 def __init__(self, syntax, scanner):
243 self.scanner = scanner
244 def parse(self, source):
245 table = {(S, Variable): 0,
254 (A, Variable, And): 5,
255 (A, Variable, Or): 6,
256 (A, Variable, Imp): 7,
257 (A, Variable, Eq): 8,
258 (A, Not, Variable, And): 5,
259 (A, Not, Variable, Or): 6,
260 (A, Not, Variable, Imp): 7,
261 (A, Not, Variable, Eq): 8}
266 self.scanner.reset(source)
267 (token, value) = self.scanner.next()
268 (lookahead, la_value) = self.scanner.next()
269 (lookahead2, la2_value) = self.scanner.next()
271 while token and len(stack):
274 tree_nodes.append((token, value))
276 #tree_nodes.append((stack.pop(), value))
277 (token, value) = (lookahead, la_value)
278 (lookahead, la_value) = (lookahead2, la2_value)
279 #(lookahead, _) = self.scanner.next()
280 (lookahead2, la2_value) = self.scanner.next()
283 if (top, token) in table:
284 action = table[(top, token)]
285 elif (top, token, lookahead) in table:
286 action = table[(top, token, lookahead)]
287 elif (top, token, lookahead, lookahead2) in table:
288 action = table[(top, token, lookahead, lookahead2)]
295 stack.extend(reversed(self.syntax[action]))
296 accepted = accepted and not len(stack)
297 return (accepted, out, tree_nodes)
299 class SyntaxTree(object):
300 def __init__(self, seq, tree_nodes):
303 self.root = self.compile(seq, tree_nodes)[0]
304 def compile(self, seq, tree_nodes):
309 c, v = tree_nodes.pop()
311 c, v = tree_nodes.pop()
312 stack.append(Variable(v))
314 stack.append(Not(self.compile(seq, tree_nodes)))
316 stack.extend(self.compile(seq, tree_nodes))
318 stack.append(Box(self.compile(seq, tree_nodes)))
320 stack.append(Diamond(self.compile(seq, tree_nodes)))
322 stack.append(And(self.compile(seq, tree_nodes)))
324 stack.append(Or(self.compile(seq, tree_nodes)))
326 stack.append(Imp(self.compile(seq, tree_nodes)))
328 stack.append(Eq(self.compile(seq, tree_nodes)))
331 from argparse import ArgumentParser
333 def parse_arguments():
334 parser = ArgumentParser(description="Parses simple modal logic syntax.")
335 parser.add_argument("-f", "--formula", help="your formula")
336 return parser.parse_args()
338 EXCUSE = """The formula was not accepted by me, because I do not like you. It is not personal. I seem to have some issues with formulae with inner nesting and I generally suffer from my hasty implementation. I would like to thank you for your coorporation by providing the formula within the code file itself. Thank you. ~The Parser"""
340 if __name__ == "__main__":