# HG changeset patch # User Eugen Sawin # Date 1306754181 -7200 # Node ID 649753d09da6657d21e1eb5e36c21bd846a879b3 # Parent 53f84d13199869d8ee45502d2978bcc34e9458f5 Introduced varargs for values. diff -r 53f84d131998 -r 649753d09da6 sml.py --- a/sml.py Wed May 18 05:09:05 2011 +0200 +++ b/sml.py Mon May 30 13:16:21 2011 +0200 @@ -3,19 +3,18 @@ Description: sml provides classes for simple modal logic formulae construction and reduction. It also features a disfunctional parser for the SML syntax. Author: Eugen Sawin """ -import re def main(): # edit your formulae here - p = Variable(["p"]) - q = Variable(["q"]) - r = Variable(["r"]) - s = Variable(["s"]) - formula1 = Imp([Eq([p, q]), r]) - formula2 = Not([Or([p, q])]) - formula3 = Not([Not([p])]) - formula4 = Imp([Box([Imp([Diamond([p]), p])]), Box([Imp([p, Box([p])])])]) - formula5 = Imp([And([Or([p, q]), r]), Not([s])]) + p = Variable("p") + q = Variable("q") + r = Variable("r") + s = Variable("s") + formula1 = Imp(Eq(p, q), r) + formula2 = Not(Or(p, q)) + formula3 = Not(Not(p)) + formula4 = Imp(Box(Imp(Diamond(p), p)), Box(Imp(p, Box(p)))) + formula5 = Imp(And(Or(p, q), r), Not(s)) formula = formula5 # choose your formula here args = parse_arguments() @@ -48,20 +47,20 @@ return [fun(v) for v in f.values] def expand_imp_eq(formula): - expmap = {IMP: lambda (a, b): Or([Not([a]), b]), - EQ: lambda (a, b): And([Or([Not([a]), b]), Or([a, Not([b])])])} + expmap = {IMP: lambda (a, b): Or(Not(a), b), + EQ: lambda (a, b): And(Or(Not(a), b), Or(a, Not(b)))} if not isinstance(formula, Operator): return formula if formula.id in expmap: return expmap[formula.id](values(expand_imp_eq, formula)) - return formula.__class__(values(expand_imp_eq, formula)) + return formula.__class__(*values(expand_imp_eq, formula)) def de_morgan(formula): - negmap = {AND: lambda (a, b): Or([negate(a), negate(b)]), - OR: lambda (a, b): And([negate(a), negate(b)]), - BOX: lambda (a,): Diamond([negate(a)]), - DIAMOND: lambda (a,): Box([negate(a)]), - VARIABLE: lambda (a,): Not([Variable([a])]), + negmap = {AND: lambda (a, b): Or(negate(a), negate(b)), + OR: lambda (a, b): And(negate(a), negate(b)), + BOX: lambda (a,): Diamond(negate(a)), + DIAMOND: lambda (a,): Box(negate(a)), + VARIABLE: lambda (a,): Not(Variable(a)), NOT: lambda (a,): a} def negate(f): return negmap[f.id](f.values) @@ -69,7 +68,7 @@ return formula if formula.id == NOT: return negate(formula.values[0]) - return formula.__class__(values(de_morgan, formula)) + return formula.__class__(*values(de_morgan, formula)) def reduce_iter(formula): redset = set(((BOX, BOX), (DIAMOND, DIAMOND), (DIAMOND, BOX), (BOX, DIAMOND))) @@ -78,27 +77,27 @@ ids = (formula.id, formula.values[0].id) if ids in redset: return reduce_iter(formula.values[0]) - return formula.__class__(values(reduce_iter, formula)) + return formula.__class__(*values(reduce_iter, formula)) def dist_mod(formula): - distmap = {(BOX, AND): lambda (a, b): And([Box([a]), Box([b])]), - (DIAMOND, OR): lambda (a, b): Or([Diamond([a]), Diamond([b])]), + distmap = {(BOX, AND): lambda (a, b): And(Box(a), Box(b)), + (DIAMOND, OR): lambda (a, b): Or(Diamond(a), Diamond(b)), (BOX, OR): lambda (a, b): (isinstance(a, Box) or isinstance(b, Box)) - and Or([Box([a]), Box([b])]) or Box([Or([a, b])]), + and Or(Box(a), Box(b)) or Box(Or(a, b)), (DIAMOND, AND): lambda (a, b): (isinstance(a, Diamond) or isinstance(b, Diamond)) - and And([Diamond([a]), Diamond([b])]) or Diamond([And([a, b])])} + and And(Diamond(a), Diamond(b)) or Diamond(And(a, b))} if not isinstance(formula, Operator) or not isinstance(formula.values[0], Operator): return formula ids = (formula.id, formula.values[0].id) if ids in distmap: - return distmap[ids](values(dist_mod, formula.values[0])) - return formula.__class__(values(dist_mod, formula)) + return distmap[ids](*values(dist_mod, formula.values[0])) + return formula.__class__(*values(dist_mod, formula)) def mcnf(formula): if formula.id == OR: conj_id = int(formula.values[1].id == AND) - return And([Or([formula.values[conj_id].values[0], formula.values[1 - conj_id]]), - Or([formula.values[conj_id].values[1], formula.values[1 - conj_id]])]); + return And(Or(formula.values[conj_id].values[0], formula.values[1 - conj_id]), + Or(formula.values[conj_id].values[1], formula.values[1 - conj_id])); return formula def cnf(formula): @@ -116,15 +115,16 @@ for i, v in enumerate(s.values): if v in known: s.values[i] = known[v] - bicon.append(Eq([Variable(["x" + str(len(bicon))]), s])) + bicon.append(Eq(Variable("x" + str(len(bicon))), s)) known[s] = bicon[-1].values[0] def conjunct(f): if len(bicon): - return And([f, conjunct(bicon.pop())]) + return And(f, conjunct(bicon.pop())) return f return mcnf(dist_mod(reduce_iter(de_morgan(expand_imp_eq(conjunct(known[formula])))))) """ The Parser - Do NOT look below this line! """ +import re NOT = "~" AND = "&" @@ -138,17 +138,17 @@ RB = ")" class Operator(object): - def __init__(self, id, arity, values): + def __init__(self, id, arity, *values): self.id = id self.arity = arity - self.values = values + self.values = list(values) def depth(self): if self.arity == 0: return 0 if self.id in (BOX, DIAMOND): return 1 + self.values[0].depth() if self.id == NOT: - return self.values[0].depth() + return self.values[0].depth() return max(self.values[0].depth(), self.values[1].depth()) def __eq__(self, other): return self.id == other.id and self.values == other.values # commutative types not considered yet @@ -164,55 +164,55 @@ class Not(Operator): arity = 1 - def __init__(self, values): - Operator.__init__(self, NOT, Not.arity, values) + def __init__(self, *values): + Operator.__init__(self, NOT, Not.arity, *values) def __call__(self): pass class And(Operator): arity = 2 - def __init__(self, values): - Operator.__init__(self, AND, And.arity, values) + def __init__(self, *values): + Operator.__init__(self, AND, And.arity, *values) class Or(Operator): arity = 2 - def __init__(self, values): - Operator.__init__(self, OR, Or.arity, values) + def __init__(self, *values): + Operator.__init__(self, OR, Or.arity, *values) class Imp(Operator): arity = 2 - def __init__(self, values): - Operator.__init__(self, IMP, Imp.arity, values) + def __init__(self, *values): + Operator.__init__(self, IMP, Imp.arity, *values) class Eq(Operator): arity = 2 - def __init__(self, values): - Operator.__init__(self, EQ, Eq.arity, values) + def __init__(self, *values): + Operator.__init__(self, EQ, Eq.arity, *values) class Box(Operator): arity = 1 - def __init__(self, values): - Operator.__init__(self, BOX, Box.arity, values) + def __init__(self, *values): + Operator.__init__(self, BOX, Box.arity, *values) class Diamond(Operator): arity = 1 - def __init__(self, values): - Operator.__init__(self, DIAMOND, Diamond.arity, values) + def __init__(self, *values): + Operator.__init__(self, DIAMOND, Diamond.arity, *values) class Variable(Operator): arity = 0 - def __init__(self, values): - Operator.__init__(self, VARIABLE, Variable.arity, values) + def __init__(self, *values): + Operator.__init__(self, VARIABLE, Variable.arity, *values) class Lb(Operator): arity = -1 - def __init__(self, values): - Operator.__init__(self, LB, Lb.arity, values) + def __init__(self, *values): + Operator.__init__(self, LB, Lb.arity, *values) class Rb(Operator): arity = -1 - def __init__(self, values): - Operator.__init__(self, RB, Rb.arity, values) + def __init__(self, *values): + Operator.__init__(self, RB, Rb.arity, *values) class Formula(object): def __init__(self): @@ -269,14 +269,6 @@ (S, Imp, S), (S, Eq, S)) -class Node(object): - def __init__(self, parent, value): - self.parent = parent - self.value = value - self.children = [] - def addChild(self, value): - self.children.append(self, node) - class Parser(object): def __init__(self, syntax, scanner): self.syntax = syntax