1.1 --- a/sml.py Wed May 18 05:09:05 2011 +0200
1.2 +++ b/sml.py Mon May 30 13:16:21 2011 +0200
1.3 @@ -3,19 +3,18 @@
1.4 Description: sml provides classes for simple modal logic formulae construction and reduction. It also features a disfunctional parser for the SML syntax.
1.5 Author: Eugen Sawin <sawine@informatik.uni-freiburg.de>
1.6 """
1.7 -import re
1.8
1.9 def main():
1.10 # edit your formulae here
1.11 - p = Variable(["p"])
1.12 - q = Variable(["q"])
1.13 - r = Variable(["r"])
1.14 - s = Variable(["s"])
1.15 - formula1 = Imp([Eq([p, q]), r])
1.16 - formula2 = Not([Or([p, q])])
1.17 - formula3 = Not([Not([p])])
1.18 - formula4 = Imp([Box([Imp([Diamond([p]), p])]), Box([Imp([p, Box([p])])])])
1.19 - formula5 = Imp([And([Or([p, q]), r]), Not([s])])
1.20 + p = Variable("p")
1.21 + q = Variable("q")
1.22 + r = Variable("r")
1.23 + s = Variable("s")
1.24 + formula1 = Imp(Eq(p, q), r)
1.25 + formula2 = Not(Or(p, q))
1.26 + formula3 = Not(Not(p))
1.27 + formula4 = Imp(Box(Imp(Diamond(p), p)), Box(Imp(p, Box(p))))
1.28 + formula5 = Imp(And(Or(p, q), r), Not(s))
1.29 formula = formula5 # choose your formula here
1.30
1.31 args = parse_arguments()
1.32 @@ -48,20 +47,20 @@
1.33 return [fun(v) for v in f.values]
1.34
1.35 def expand_imp_eq(formula):
1.36 - expmap = {IMP: lambda (a, b): Or([Not([a]), b]),
1.37 - EQ: lambda (a, b): And([Or([Not([a]), b]), Or([a, Not([b])])])}
1.38 + expmap = {IMP: lambda (a, b): Or(Not(a), b),
1.39 + EQ: lambda (a, b): And(Or(Not(a), b), Or(a, Not(b)))}
1.40 if not isinstance(formula, Operator):
1.41 return formula
1.42 if formula.id in expmap:
1.43 return expmap[formula.id](values(expand_imp_eq, formula))
1.44 - return formula.__class__(values(expand_imp_eq, formula))
1.45 + return formula.__class__(*values(expand_imp_eq, formula))
1.46
1.47 def de_morgan(formula):
1.48 - negmap = {AND: lambda (a, b): Or([negate(a), negate(b)]),
1.49 - OR: lambda (a, b): And([negate(a), negate(b)]),
1.50 - BOX: lambda (a,): Diamond([negate(a)]),
1.51 - DIAMOND: lambda (a,): Box([negate(a)]),
1.52 - VARIABLE: lambda (a,): Not([Variable([a])]),
1.53 + negmap = {AND: lambda (a, b): Or(negate(a), negate(b)),
1.54 + OR: lambda (a, b): And(negate(a), negate(b)),
1.55 + BOX: lambda (a,): Diamond(negate(a)),
1.56 + DIAMOND: lambda (a,): Box(negate(a)),
1.57 + VARIABLE: lambda (a,): Not(Variable(a)),
1.58 NOT: lambda (a,): a}
1.59 def negate(f):
1.60 return negmap[f.id](f.values)
1.61 @@ -69,7 +68,7 @@
1.62 return formula
1.63 if formula.id == NOT:
1.64 return negate(formula.values[0])
1.65 - return formula.__class__(values(de_morgan, formula))
1.66 + return formula.__class__(*values(de_morgan, formula))
1.67
1.68 def reduce_iter(formula):
1.69 redset = set(((BOX, BOX), (DIAMOND, DIAMOND), (DIAMOND, BOX), (BOX, DIAMOND)))
1.70 @@ -78,27 +77,27 @@
1.71 ids = (formula.id, formula.values[0].id)
1.72 if ids in redset:
1.73 return reduce_iter(formula.values[0])
1.74 - return formula.__class__(values(reduce_iter, formula))
1.75 + return formula.__class__(*values(reduce_iter, formula))
1.76
1.77 def dist_mod(formula):
1.78 - distmap = {(BOX, AND): lambda (a, b): And([Box([a]), Box([b])]),
1.79 - (DIAMOND, OR): lambda (a, b): Or([Diamond([a]), Diamond([b])]),
1.80 + distmap = {(BOX, AND): lambda (a, b): And(Box(a), Box(b)),
1.81 + (DIAMOND, OR): lambda (a, b): Or(Diamond(a), Diamond(b)),
1.82 (BOX, OR): lambda (a, b): (isinstance(a, Box) or isinstance(b, Box))
1.83 - and Or([Box([a]), Box([b])]) or Box([Or([a, b])]),
1.84 + and Or(Box(a), Box(b)) or Box(Or(a, b)),
1.85 (DIAMOND, AND): lambda (a, b): (isinstance(a, Diamond) or isinstance(b, Diamond))
1.86 - and And([Diamond([a]), Diamond([b])]) or Diamond([And([a, b])])}
1.87 + and And(Diamond(a), Diamond(b)) or Diamond(And(a, b))}
1.88 if not isinstance(formula, Operator) or not isinstance(formula.values[0], Operator):
1.89 return formula
1.90 ids = (formula.id, formula.values[0].id)
1.91 if ids in distmap:
1.92 - return distmap[ids](values(dist_mod, formula.values[0]))
1.93 - return formula.__class__(values(dist_mod, formula))
1.94 + return distmap[ids](*values(dist_mod, formula.values[0]))
1.95 + return formula.__class__(*values(dist_mod, formula))
1.96
1.97 def mcnf(formula):
1.98 if formula.id == OR:
1.99 conj_id = int(formula.values[1].id == AND)
1.100 - return And([Or([formula.values[conj_id].values[0], formula.values[1 - conj_id]]),
1.101 - Or([formula.values[conj_id].values[1], formula.values[1 - conj_id]])]);
1.102 + return And(Or(formula.values[conj_id].values[0], formula.values[1 - conj_id]),
1.103 + Or(formula.values[conj_id].values[1], formula.values[1 - conj_id]));
1.104 return formula
1.105
1.106 def cnf(formula):
1.107 @@ -116,15 +115,16 @@
1.108 for i, v in enumerate(s.values):
1.109 if v in known:
1.110 s.values[i] = known[v]
1.111 - bicon.append(Eq([Variable(["x" + str(len(bicon))]), s]))
1.112 + bicon.append(Eq(Variable("x" + str(len(bicon))), s))
1.113 known[s] = bicon[-1].values[0]
1.114 def conjunct(f):
1.115 if len(bicon):
1.116 - return And([f, conjunct(bicon.pop())])
1.117 + return And(f, conjunct(bicon.pop()))
1.118 return f
1.119 return mcnf(dist_mod(reduce_iter(de_morgan(expand_imp_eq(conjunct(known[formula]))))))
1.120
1.121 """ The Parser - Do NOT look below this line! """
1.122 +import re
1.123
1.124 NOT = "~"
1.125 AND = "&"
1.126 @@ -138,17 +138,17 @@
1.127 RB = ")"
1.128
1.129 class Operator(object):
1.130 - def __init__(self, id, arity, values):
1.131 + def __init__(self, id, arity, *values):
1.132 self.id = id
1.133 self.arity = arity
1.134 - self.values = values
1.135 + self.values = list(values)
1.136 def depth(self):
1.137 if self.arity == 0:
1.138 return 0
1.139 if self.id in (BOX, DIAMOND):
1.140 return 1 + self.values[0].depth()
1.141 if self.id == NOT:
1.142 - return self.values[0].depth()
1.143 + return self.values[0].depth()
1.144 return max(self.values[0].depth(), self.values[1].depth())
1.145 def __eq__(self, other):
1.146 return self.id == other.id and self.values == other.values # commutative types not considered yet
1.147 @@ -164,55 +164,55 @@
1.148
1.149 class Not(Operator):
1.150 arity = 1
1.151 - def __init__(self, values):
1.152 - Operator.__init__(self, NOT, Not.arity, values)
1.153 + def __init__(self, *values):
1.154 + Operator.__init__(self, NOT, Not.arity, *values)
1.155 def __call__(self):
1.156 pass
1.157
1.158 class And(Operator):
1.159 arity = 2
1.160 - def __init__(self, values):
1.161 - Operator.__init__(self, AND, And.arity, values)
1.162 + def __init__(self, *values):
1.163 + Operator.__init__(self, AND, And.arity, *values)
1.164
1.165 class Or(Operator):
1.166 arity = 2
1.167 - def __init__(self, values):
1.168 - Operator.__init__(self, OR, Or.arity, values)
1.169 + def __init__(self, *values):
1.170 + Operator.__init__(self, OR, Or.arity, *values)
1.171
1.172 class Imp(Operator):
1.173 arity = 2
1.174 - def __init__(self, values):
1.175 - Operator.__init__(self, IMP, Imp.arity, values)
1.176 + def __init__(self, *values):
1.177 + Operator.__init__(self, IMP, Imp.arity, *values)
1.178
1.179 class Eq(Operator):
1.180 arity = 2
1.181 - def __init__(self, values):
1.182 - Operator.__init__(self, EQ, Eq.arity, values)
1.183 + def __init__(self, *values):
1.184 + Operator.__init__(self, EQ, Eq.arity, *values)
1.185
1.186 class Box(Operator):
1.187 arity = 1
1.188 - def __init__(self, values):
1.189 - Operator.__init__(self, BOX, Box.arity, values)
1.190 + def __init__(self, *values):
1.191 + Operator.__init__(self, BOX, Box.arity, *values)
1.192
1.193 class Diamond(Operator):
1.194 arity = 1
1.195 - def __init__(self, values):
1.196 - Operator.__init__(self, DIAMOND, Diamond.arity, values)
1.197 + def __init__(self, *values):
1.198 + Operator.__init__(self, DIAMOND, Diamond.arity, *values)
1.199
1.200 class Variable(Operator):
1.201 arity = 0
1.202 - def __init__(self, values):
1.203 - Operator.__init__(self, VARIABLE, Variable.arity, values)
1.204 + def __init__(self, *values):
1.205 + Operator.__init__(self, VARIABLE, Variable.arity, *values)
1.206
1.207 class Lb(Operator):
1.208 arity = -1
1.209 - def __init__(self, values):
1.210 - Operator.__init__(self, LB, Lb.arity, values)
1.211 + def __init__(self, *values):
1.212 + Operator.__init__(self, LB, Lb.arity, *values)
1.213
1.214 class Rb(Operator):
1.215 arity = -1
1.216 - def __init__(self, values):
1.217 - Operator.__init__(self, RB, Rb.arity, values)
1.218 + def __init__(self, *values):
1.219 + Operator.__init__(self, RB, Rb.arity, *values)
1.220
1.221 class Formula(object):
1.222 def __init__(self):
1.223 @@ -269,14 +269,6 @@
1.224 (S, Imp, S),
1.225 (S, Eq, S))
1.226
1.227 -class Node(object):
1.228 - def __init__(self, parent, value):
1.229 - self.parent = parent
1.230 - self.value = value
1.231 - self.children = []
1.232 - def addChild(self, value):
1.233 - self.children.append(self, node)
1.234 -
1.235 class Parser(object):
1.236 def __init__(self, syntax, scanner):
1.237 self.syntax = syntax