1.1 --- a/sml.py Tue May 17 19:11:34 2011 +0200
1.2 +++ b/sml.py Wed May 18 03:23:35 2011 +0200
1.3 @@ -13,7 +13,8 @@
1.4 formula1 = Imp([Eq([p, q]), r])
1.5 formula2 = Not([Or([p, q])])
1.6 formula3 = Not([Not([p])])
1.7 - formula = formula1 # choose your formula here
1.8 + formula4 = Imp([Box([Imp([Diamond([p]), p])]), Box([Imp([p, Box([p])])])])
1.9 + formula = formula4 # choose your formula here
1.10
1.11 args = parse_arguments()
1.12 if (args.formula):
1.13 @@ -26,31 +27,38 @@
1.14 tree = SyntaxTree(out, tree_nodes)
1.15 formula = tree.root
1.16
1.17 - print "formula: \t\t\t", formula
1.18 - print "expanded -> and <->: \t\t", expand_imp_eq(formula)
1.19 - print "reduced ~: \t\t\t", de_morgan(expand_imp_eq(formula))
1.20 - print "reduced iterated modalities: \t", reduce_iter(de_morgan(expand_imp_eq(formula)))
1.21 - print "distributed modalities+: \t", reduce_iter(dist(reduce_iter(de_morgan(expand_imp_eq(formula)))))
1.22 + print "formula: \t\t\t%s (%i)" % (formula, formula.depth())
1.23 + formula = expand_imp_eq(formula)
1.24 + print "expanded -> and <->: \t\t%s (%i)" % (formula, formula.depth())
1.25 + formula = de_morgan(formula)
1.26 + print "reduced ~: \t\t\t%s (%i)" % (formula, formula.depth())
1.27 + formula = reduce_iter(formula)
1.28 + print "reduced iterated modalities: \t%s (%i)" % (formula, formula.depth())
1.29 + formula = reduce_iter(dist_mod((formula)))
1.30 + print "distributed modalities+: \t%s (%i)" % (formula, formula.depth())
1.31 + formula = None
1.32
1.33 def values(fun, f):
1.34 return [fun(v) for v in f.values]
1.35
1.36 def expand_imp_eq(formula):
1.37 - map = {IMP: lambda (a, b): Or([Not([a]), b]),
1.38 - EQ: lambda (a, b): And([Or([Not([a]), b]), Or([a, Not([b])])])}
1.39 - if not isinstance(formula, Operator) or formula.id not in map:
1.40 + expmap = {IMP: lambda (a, b): Or([Not([a]), b]),
1.41 + EQ: lambda (a, b): And([Or([Not([a]), b]), Or([a, Not([b])])])}
1.42 + if not isinstance(formula, Operator):
1.43 return formula
1.44 - return map[formula.id](values(expand_imp_eq, formula))
1.45 + if formula.id in expmap:
1.46 + return expmap[formula.id](values(expand_imp_eq, formula))
1.47 + return formula.__class__(values(expand_imp_eq, formula))
1.48
1.49 -def de_morgan(formula):
1.50 +def de_morgan(formula):
1.51 negmap = {AND: lambda (a, b): Or([negate(a), negate(b)]),
1.52 OR: lambda (a, b): And([negate(a), negate(b)]),
1.53 BOX: lambda (a,): Diamond([negate(a)]),
1.54 DIAMOND: lambda (a,): Box([negate(a)]),
1.55 - VARIABLE: lambda (a,): Not([a]),
1.56 + VARIABLE: lambda (a,): Not([Variable([a])]),
1.57 NOT: lambda (a,): a}
1.58 def negate(f):
1.59 - return negmap[f.id](f.values)
1.60 + return negmap[f.id](f.values)
1.61 if not isinstance(formula, Operator):
1.62 return formula
1.63 if formula.id == NOT:
1.64 @@ -66,7 +74,7 @@
1.65 return reduce_iter(formula.values[0])
1.66 return formula.__class__(values(reduce_iter, formula))
1.67
1.68 -def dist(formula):
1.69 +def dist_mod(formula):
1.70 distmap = {(BOX, AND): lambda (a, b): And([Box([a]), Box([b])]),
1.71 (DIAMOND, OR): lambda (a, b): Or([Diamond([a]), Diamond([b])]),
1.72 (BOX, OR): lambda (a, b): (isinstance(a, Box) or isinstance(b, Box))
1.73 @@ -77,8 +85,8 @@
1.74 return formula
1.75 ids = (formula.id, formula.values[0].id)
1.76 if ids in distmap:
1.77 - return distmap[ids](formula.values[0].values)
1.78 - return formula.__class__(values(dist, formula))
1.79 + return distmap[ids](values(dist_mod, formula.values[0]))
1.80 + return formula.__class__(values(dist_mod, formula))
1.81
1.82 NOT = "~"
1.83 AND = "&"
1.84 @@ -96,10 +104,18 @@
1.85 self.id = id
1.86 self.arity = arity
1.87 self.values = values
1.88 + def depth(self):
1.89 + if self.arity == 0:
1.90 + return 0
1.91 + if self.id in (BOX, DIAMOND):
1.92 + return 1 + self.values[0].depth()
1.93 + if self.id == NOT:
1.94 + return self.values[0].depth()
1.95 + return max(self.values[0].depth(), self.values[1].depth())
1.96 def __str__(self):
1.97 out = self.id
1.98 if self.arity == 0:
1.99 - out = str(self.values[0])
1.100 + out = str(self.values[0])
1.101 if self.arity == 1:
1.102 out = self.id + str(self.values[0])
1.103 elif self.arity == 2:
1.104 @@ -319,7 +335,7 @@
1.105 parser.add_argument("-f", "--formula", help="your formula")
1.106 return parser.parse_args()
1.107
1.108 -EXCUSE = """The formula was not accepted by me, because I don't like you and the rest of the world. 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"""
1.109 +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"""
1.110
1.111 if __name__ == "__main__":
1.112 main()