1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/downloads/sml.py Mon Jul 18 01:51:06 2011 +0200
1.3 @@ -0,0 +1,447 @@
1.4 +"""
1.5 +Name: sml - Simple Modal Logic Lib.
1.6 +Description: sml provides classes for simple modal logic formulae construction and reduction. It also features a disfunctional parser for the SML syntax.
1.7 +Author: Eugen Sawin <sawine@informatik.uni-freiburg.de>
1.8 +"""
1.9 +
1.10 +TMP_DIMACS = "dimacs~"
1.11 +TMP_SOLUTION = "solution~"
1.12 +
1.13 +def main():
1.14 + # edit your formulae here
1.15 + p = Variable("p")
1.16 + q = Variable("q")
1.17 + r = Variable("r")
1.18 + s = Variable("s")
1.19 + formula1 = Imp(Eq(p, q), r)
1.20 + formula2 = Not(Or(p, q))
1.21 + formula3 = Not(Not(p))
1.22 + formula4 = Imp(Box(Imp(Diamond(p), p)), Box(Imp(p, Box(p))))
1.23 + formula5 = Imp(And(Or(p, q), r), Not(s))
1.24 + formula6 = And(Or(p, Or(q, Not(s))), And(Or(r, Not(s)), Or(Not(p), s)))
1.25 + formula = formula6 # choose your formula here
1.26 +
1.27 + args = parse_arguments()
1.28 + if (args.formula):
1.29 + scanner = Scanner(TOKENS)
1.30 + parser = Parser(SYNTAX, scanner)
1.31 + (accepted, out, tree_nodes) = parser.parse(args.formula)
1.32 + if not accepted:
1.33 + print EXCUSE
1.34 + return
1.35 + tree = SyntaxTree(out, tree_nodes)
1.36 + formula = tree.root
1.37 +
1.38 + original = formula
1.39 + print "formula: \t\t\t%s [%i]" % (formula, formula.depth())
1.40 + formula = expand_imp_eq(formula)
1.41 + print "expanded -> and <->: \t\t%s [%i]" % (formula, formula.depth())
1.42 + formula = de_morgan(formula)
1.43 + print "reduced ~: \t\t\t%s [%i]" % (formula, formula.depth())
1.44 + formula = reduce_iter(formula)
1.45 + print "reduced iterated modalities: \t%s [%i]" % (formula, formula.depth())
1.46 + formula = reduce_iter(dist_mod((formula)))
1.47 + print "distributed modalities+: \t%s [%i]" % (formula, formula.depth())
1.48 + formula = mcnf(formula)
1.49 + print "alpha mcnf: \t\t\t%s [%i]" % (formula, formula.depth())
1.50 + #cnf_formula = cnf(original)
1.51 + #print "alpha cnf: \t\t\t%s [%i]" % (cnf_formula, cnf_formula.depth())
1.52 +
1.53 + if not args.dimacs:
1.54 + dimacs_file = TMP_DIMACS
1.55 + else:
1.56 + dimacs_file = args.dimacs
1.57 + solution = sat_test(original, dimacs_file)
1.58 + if solution:
1.59 + print "satisfiable: \t\t\t%s " % (", ".join([str(s) for s in solution]))
1.60 + else:
1.61 + print "not satisfiable"
1.62 +
1.63 +from subprocess import call, PIPE
1.64 +
1.65 +def sat_test(formula, dimacs_file):
1.66 + out, variables = dimacs(formula)
1.67 + with open(dimacs_file, "w") as f:
1.68 + f.write(out)
1.69 + call(["minisat2", "-verb=0", dimacs_file, TMP_SOLUTION], stdout=PIPE)
1.70 + with open(TMP_SOLUTION) as f:
1.71 + solved, assignment = f.readlines()
1.72 + solved = solved[0] == "S"
1.73 + if solved:
1.74 + positive = set()
1.75 + for a in assignment.split():
1.76 + neg = a[0] == "-"
1.77 + if not neg:
1.78 + positive.add(int(a))
1.79 + solution = []
1.80 + for v, n in variables.iteritems():
1.81 + if n in positive:
1.82 + solution.append(Variable(v))
1.83 + else:
1.84 + solution.append(Not(Variable(v)))
1.85 + return solution
1.86 +
1.87 +def dimacs(formula):
1.88 + def clausify(f):
1.89 + if f.id == AND:
1.90 + c1 = clausify(f.values[0])
1.91 + c2 = clausify(f.values[1])
1.92 + if c1:
1.93 + clauses.append(clausify(f.values[0]))
1.94 + if c2:
1.95 + clauses.append(clausify(f.values[1]))
1.96 + if f.id == OR:
1.97 + clause = []
1.98 + clause.extend(clausify(f.values[0]))
1.99 + clause.extend(clausify(f.values[1]))
1.100 + return clause
1.101 + if f.id == NOT:
1.102 + return ["-" + clausify(f.values[0])]
1.103 + if f.id == VARIABLE:
1.104 + if f.values[0] in variables:
1.105 + n = variables[f.values[0]]
1.106 + else:
1.107 + n = len(variables) + 1
1.108 + variables[f.values[0]] = n
1.109 + return str(n)
1.110 +
1.111 + variables = {}
1.112 + clauses = []
1.113 + clausify(formula)
1.114 + out = "c DIMACS CNF input file generated by sml\n"
1.115 + out += "c Author: Eugen Sawin <sawine@informatik.uni-freiburg.de>\n"
1.116 + out += "p cnf %i %i\n" % (len(variables), len(clauses))
1.117 + out += " 0\n".join([" ".join(c) for c in clauses]) + " 0\n"
1.118 + return out, variables
1.119 +
1.120 +def values(fun, f):
1.121 + return [fun(v) for v in f.values]
1.122 +
1.123 +def expand_imp_eq(formula):
1.124 + expmap = {IMP: lambda (a, b): Or(Not(a), b),
1.125 + EQ: lambda (a, b): And(Or(Not(a), b), Or(a, Not(b)))}
1.126 + if not isinstance(formula, Operator):
1.127 + return formula
1.128 + if formula.id in expmap:
1.129 + return expmap[formula.id](values(expand_imp_eq, formula))
1.130 + return formula.__class__(*values(expand_imp_eq, formula))
1.131 +
1.132 +def de_morgan(formula):
1.133 + negmap = {AND: lambda (a, b): Or(negate(a), negate(b)),
1.134 + OR: lambda (a, b): And(negate(a), negate(b)),
1.135 + BOX: lambda (a,): Diamond(negate(a)),
1.136 + DIAMOND: lambda (a,): Box(negate(a)),
1.137 + VARIABLE: lambda (a,): Not(Variable(a)),
1.138 + NOT: lambda (a,): a}
1.139 + def negate(f):
1.140 + return negmap[f.id](f.values)
1.141 + if not isinstance(formula, Operator):
1.142 + return formula
1.143 + if formula.id == NOT:
1.144 + return negate(formula.values[0])
1.145 + return formula.__class__(*values(de_morgan, formula))
1.146 +
1.147 +def reduce_iter(formula):
1.148 + redset = set(((BOX, BOX), (DIAMOND, DIAMOND), (DIAMOND, BOX), (BOX, DIAMOND)))
1.149 + if not isinstance(formula, Operator) or not isinstance(formula.values[0], Operator):
1.150 + return formula
1.151 + ids = (formula.id, formula.values[0].id)
1.152 + if ids in redset:
1.153 + return reduce_iter(formula.values[0])
1.154 + return formula.__class__(*values(reduce_iter, formula))
1.155 +
1.156 +def dist_mod(formula):
1.157 + distmap = {(BOX, AND): lambda (a, b): And(Box(a), Box(b)),
1.158 + (DIAMOND, OR): lambda (a, b): Or(Diamond(a), Diamond(b)),
1.159 + (BOX, OR): lambda (a, b): (isinstance(a, Box) or isinstance(b, Box))
1.160 + and Or(Box(a), Box(b)) or Box(Or(a, b)),
1.161 + (DIAMOND, AND): lambda (a, b): (isinstance(a, Diamond) or isinstance(b, Diamond))
1.162 + and And(Diamond(a), Diamond(b)) or Diamond(And(a, b))}
1.163 + if not isinstance(formula, Operator) or not isinstance(formula.values[0], Operator):
1.164 + return formula
1.165 + ids = (formula.id, formula.values[0].id)
1.166 + if ids in distmap:
1.167 + return distmap[ids](values(dist_mod, formula.values[0]))
1.168 + return formula.__class__(*values(dist_mod, formula))
1.169 +
1.170 +def mcnf(formula):
1.171 + if formula.id == OR:
1.172 + conj_id = int(formula.values[1].id == AND)
1.173 + return And(Or(formula.values[conj_id].values[0], formula.values[1 - conj_id]),
1.174 + Or(formula.values[conj_id].values[1], formula.values[1 - conj_id]));
1.175 + return formula
1.176 +
1.177 +def cnf(formula):
1.178 + def part(f):
1.179 + for v in f.values:
1.180 + if v.id != VARIABLE:
1.181 + sub_formulae.append(v)
1.182 + part(v)
1.183 +
1.184 + def conjunct(f):
1.185 + if len(bicon):
1.186 + return And(f, conjunct(bicon.pop()))
1.187 + return f
1.188 +
1.189 + sub_formulae = [formula]
1.190 + part(formula)
1.191 + sub_formulae.reverse()
1.192 + known = {}
1.193 + bicon = []
1.194 + for s in sub_formulae:
1.195 + for i, v in enumerate(s.values):
1.196 + if v in known:
1.197 + s.values[i] = known[v]
1.198 + bicon.append(Eq(Variable("x" + str(len(bicon))), s))
1.199 + known[s] = bicon[-1].values[0]
1.200 + return mcnf(dist_mod(reduce_iter(de_morgan(expand_imp_eq(conjunct(known[formula]))))))
1.201 +
1.202 +""" The Parser - Do NOT look below this line! """
1.203 +import re
1.204 +
1.205 +NOT = "~"
1.206 +AND = "&"
1.207 +OR = "|"
1.208 +IMP = "->"
1.209 +EQ = "<->"
1.210 +BOX = "[]"
1.211 +DIAMOND = "<>"
1.212 +VARIABLE = "VAR"
1.213 +LB = "("
1.214 +RB = ")"
1.215 +
1.216 +class Operator(object):
1.217 + def __init__(self, id, arity, *values):
1.218 + self.id = id
1.219 + self.arity = arity
1.220 + self.values = list(values)
1.221 + def depth(self):
1.222 + if self.arity == 0:
1.223 + return 0
1.224 + if self.id in (BOX, DIAMOND):
1.225 + return 1 + self.values[0].depth()
1.226 + if self.id == NOT:
1.227 + return self.values[0].depth()
1.228 + return max(self.values[0].depth(), self.values[1].depth())
1.229 + def __eq__(self, other):
1.230 + return self.id == other.id and self.values == other.values # commutative types not considered yet
1.231 + def __str__(self):
1.232 + out = self.id
1.233 + if self.arity == 0:
1.234 + out = str(self.values[0])
1.235 + if self.arity == 1:
1.236 + out = self.id + str(self.values[0])
1.237 + elif self.arity == 2:
1.238 + out = "(" + str(self.values[0]) + " " + self.id + " " + str(self.values[1]) + ")"
1.239 + return out
1.240 +
1.241 +class Not(Operator):
1.242 + arity = 1
1.243 + def __init__(self, *values):
1.244 + Operator.__init__(self, NOT, Not.arity, *values)
1.245 + def __call__(self):
1.246 + pass
1.247 +
1.248 +class And(Operator):
1.249 + arity = 2
1.250 + def __init__(self, *values):
1.251 + Operator.__init__(self, AND, And.arity, *values)
1.252 +
1.253 +class Or(Operator):
1.254 + arity = 2
1.255 + def __init__(self, *values):
1.256 + Operator.__init__(self, OR, Or.arity, *values)
1.257 +
1.258 +class Imp(Operator):
1.259 + arity = 2
1.260 + def __init__(self, *values):
1.261 + Operator.__init__(self, IMP, Imp.arity, *values)
1.262 +
1.263 +class Eq(Operator):
1.264 + arity = 2
1.265 + def __init__(self, *values):
1.266 + Operator.__init__(self, EQ, Eq.arity, *values)
1.267 +
1.268 +class Box(Operator):
1.269 + arity = 1
1.270 + def __init__(self, *values):
1.271 + Operator.__init__(self, BOX, Box.arity, *values)
1.272 +
1.273 +class Diamond(Operator):
1.274 + arity = 1
1.275 + def __init__(self, *values):
1.276 + Operator.__init__(self, DIAMOND, Diamond.arity, *values)
1.277 +
1.278 +class Variable(Operator):
1.279 + arity = 0
1.280 + def __init__(self, *values):
1.281 + Operator.__init__(self, VARIABLE, Variable.arity, *values)
1.282 +
1.283 +class Lb(Operator):
1.284 + arity = -1
1.285 + def __init__(self, *values):
1.286 + Operator.__init__(self, LB, Lb.arity, *values)
1.287 +
1.288 +class Rb(Operator):
1.289 + arity = -1
1.290 + def __init__(self, *values):
1.291 + Operator.__init__(self, RB, Rb.arity, *values)
1.292 +
1.293 +class Formula(object):
1.294 + def __init__(self):
1.295 + pass
1.296 +
1.297 +TOKENS = {re.compile("\("): Lb,
1.298 + re.compile("\)"): Rb,
1.299 + re.compile("~"): Not,
1.300 + re.compile("&"): And,
1.301 + re.compile("\|"): Or,
1.302 + re.compile("->"): Imp,
1.303 + re.compile("<->"): Eq,
1.304 + re.compile("\[\]"): Box,
1.305 + re.compile("<>"): Diamond,
1.306 + re.compile("[a-z]+"): Variable}
1.307 +
1.308 +class Scanner(object):
1.309 + def __init__(self, tokens, source=None):
1.310 + self.tokens = tokens
1.311 + self.reset(source)
1.312 + def next(self):
1.313 + while self.i < len(self.source):
1.314 + re.purge()
1.315 + for p, token in self.tokens.iteritems():
1.316 + m = p.match(self.source[self.i:])
1.317 + if m:
1.318 + self.i += m.end(0)
1.319 + value = m.group(0)
1.320 + return (token, value)
1.321 + self.i += 1
1.322 + return (None, None)
1.323 + def reset(self, source):
1.324 + self.i = 0
1.325 + self.source = source
1.326 +
1.327 +S = Formula
1.328 +A = "A"
1.329 +#0 S: (Variable,),
1.330 +#1 S: (Not, S),
1.331 +#2 S: (Lb, A, Rb),
1.332 +#3 S: (Box, S),
1.333 +#4 S: (Diamond, S),
1.334 +#5 A: (S, And, S),
1.335 +#6 A: (S, Or, S),
1.336 +#7 A: (S, Imp, S),
1.337 +#8 A: (S, Eq, S)
1.338 +SYNTAX = ((Variable,),
1.339 + (Not, S),
1.340 + (Lb, A, Rb),
1.341 + (Box, S),
1.342 + (Diamond, S),
1.343 + (S, And, S),
1.344 + (S, Or, S),
1.345 + (S, Imp, S),
1.346 + (S, Eq, S))
1.347 +
1.348 +class Parser(object):
1.349 + def __init__(self, syntax, scanner):
1.350 + self.syntax = syntax
1.351 + self.scanner = scanner
1.352 + def parse(self, source):
1.353 + table = {(S, Variable): 0,
1.354 + (S, Not): 1,
1.355 + (S, Lb): 2,
1.356 + (S, Box): 3,
1.357 + (S, Diamond): 4,
1.358 + (A, S, And): 5,
1.359 + (A, S, Or): 6,
1.360 + (A, S, Imp): 7,
1.361 + (A, S, Eq): 8,
1.362 + (A, Variable, And): 5,
1.363 + (A, Variable, Or): 6,
1.364 + (A, Variable, Imp): 7,
1.365 + (A, Variable, Eq): 8,
1.366 + (A, Not, Variable, And): 5,
1.367 + (A, Not, Variable, Or): 6,
1.368 + (A, Not, Variable, Imp): 7,
1.369 + (A, Not, Variable, Eq): 8}
1.370 + stack = [S]
1.371 + tree_nodes = []
1.372 + tree = None
1.373 + out = []
1.374 + self.scanner.reset(source)
1.375 + (token, value) = self.scanner.next()
1.376 + (lookahead, la_value) = self.scanner.next()
1.377 + (lookahead2, la2_value) = self.scanner.next()
1.378 + accepted = True
1.379 + while token and len(stack):
1.380 + top = stack[-1]
1.381 + if top == token:
1.382 + tree_nodes.append((token, value))
1.383 + stack.pop()
1.384 + #tree_nodes.append((stack.pop(), value))
1.385 + (token, value) = (lookahead, la_value)
1.386 + (lookahead, la_value) = (lookahead2, la2_value)
1.387 + #(lookahead, _) = self.scanner.next()
1.388 + (lookahead2, la2_value) = self.scanner.next()
1.389 + else:
1.390 + action = None
1.391 + if (top, token) in table:
1.392 + action = table[(top, token)]
1.393 + elif (top, token, lookahead) in table:
1.394 + action = table[(top, token, lookahead)]
1.395 + elif (top, token, lookahead, lookahead2) in table:
1.396 + action = table[(top, token, lookahead, lookahead2)]
1.397 + if action is None:
1.398 + accepted = False
1.399 + break
1.400 +
1.401 + out.append(action)
1.402 + stack.pop()
1.403 + stack.extend(reversed(self.syntax[action]))
1.404 + accepted = accepted and not len(stack)
1.405 + return (accepted, out, tree_nodes)
1.406 +
1.407 +class SyntaxTree(object):
1.408 + def __init__(self, seq, tree_nodes):
1.409 + seq.reverse()
1.410 + tree_nodes.reverse()
1.411 + self.root = self.compile(seq, tree_nodes)[0]
1.412 + def compile(self, seq, tree_nodes):
1.413 + stack = []
1.414 + while len(seq):
1.415 + s = seq.pop()
1.416 + if s == 0:
1.417 + c, v = tree_nodes.pop()
1.418 + while c != Variable:
1.419 + c, v = tree_nodes.pop()
1.420 + stack.append(Variable(v))
1.421 + elif s == 1:
1.422 + stack.append(Not(self.compile(seq, tree_nodes)))
1.423 + elif s == 2:
1.424 + stack.extend(self.compile(seq, tree_nodes))
1.425 + elif s == 3:
1.426 + stack.append(Box(self.compile(seq, tree_nodes)))
1.427 + elif s == 4:
1.428 + stack.append(Diamond(self.compile(seq, tree_nodes)))
1.429 + elif s == 5:
1.430 + stack.append(And(self.compile(seq, tree_nodes)))
1.431 + elif s == 6:
1.432 + stack.append(Or(self.compile(seq, tree_nodes)))
1.433 + elif s == 7:
1.434 + stack.append(Imp(self.compile(seq, tree_nodes)))
1.435 + elif s == 8:
1.436 + stack.append(Eq(self.compile(seq, tree_nodes)))
1.437 + return stack
1.438 +
1.439 +from argparse import ArgumentParser
1.440 +
1.441 +def parse_arguments():
1.442 + parser = ArgumentParser(description="Tries to parse simple modal logic syntax and reduces the formula. Edit your formula directly in the code file for best results.")
1.443 + parser.add_argument("-f", "--formula", help="provide your own formula here, or better don't")
1.444 + parser.add_argument("-d", "--dimacs", help="output file for the CNF DIMACS output")
1.445 + return parser.parse_args()
1.446 +
1.447 +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.448 +
1.449 +if __name__ == "__main__":
1.450 + main()