1.1 --- a/downloads/sml.py Mon Jul 18 01:54:27 2011 +0200
1.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
1.3 @@ -1,447 +0,0 @@
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()