Updated with goodies.
2 Name: sml - Simple Modal Logic Lib.
3 Description: sml provides classes for simple modal logic formulae construction and reduction. It also features a disfunctional parser for the SML syntax.
4 Author: Eugen Sawin <sawine@informatik.uni-freiburg.de>
8 TMP_SOLUTION = "solution~"
11 # edit your formulae here
16 formula1 = Imp(Eq(p, q), r)
17 formula2 = Not(Or(p, q))
18 formula3 = Not(Not(p))
19 formula4 = Imp(Box(Imp(Diamond(p), p)), Box(Imp(p, Box(p))))
20 formula5 = Imp(And(Or(p, q), r), Not(s))
21 formula6 = And(Or(p, Or(q, Not(s))), And(Or(r, Not(s)), Or(Not(p), s)))
22 formula = formula6 # choose your formula here
24 args = parse_arguments()
26 scanner = Scanner(TOKENS)
27 parser = Parser(SYNTAX, scanner)
28 (accepted, out, tree_nodes) = parser.parse(args.formula)
32 tree = SyntaxTree(out, tree_nodes)
36 print "formula: \t\t\t%s [%i]" % (formula, formula.depth())
37 formula = expand_imp_eq(formula)
38 print "expanded -> and <->: \t\t%s [%i]" % (formula, formula.depth())
39 formula = de_morgan(formula)
40 print "reduced ~: \t\t\t%s [%i]" % (formula, formula.depth())
41 formula = reduce_iter(formula)
42 print "reduced iterated modalities: \t%s [%i]" % (formula, formula.depth())
43 formula = reduce_iter(dist_mod((formula)))
44 print "distributed modalities+: \t%s [%i]" % (formula, formula.depth())
45 formula = mcnf(formula)
46 print "alpha mcnf: \t\t\t%s [%i]" % (formula, formula.depth())
47 #cnf_formula = cnf(original)
48 #print "alpha cnf: \t\t\t%s [%i]" % (cnf_formula, cnf_formula.depth())
51 dimacs_file = TMP_DIMACS
53 dimacs_file = args.dimacs
54 solution = sat_test(original, dimacs_file)
56 print "satisfiable: \t\t\t%s " % (", ".join([str(s) for s in solution]))
58 print "not satisfiable"
60 from subprocess import call, PIPE
62 def sat_test(formula, dimacs_file):
63 out, variables = dimacs(formula)
64 with open(dimacs_file, "w") as f:
66 call(["minisat2", "-verb=0", dimacs_file, TMP_SOLUTION], stdout=PIPE)
67 with open(TMP_SOLUTION) as f:
68 solved, assignment = f.readlines()
69 solved = solved[0] == "S"
72 for a in assignment.split():
77 for v, n in variables.iteritems():
79 solution.append(Variable(v))
81 solution.append(Not(Variable(v)))
87 c1 = clausify(f.values[0])
88 c2 = clausify(f.values[1])
90 clauses.append(clausify(f.values[0]))
92 clauses.append(clausify(f.values[1]))
95 clause.extend(clausify(f.values[0]))
96 clause.extend(clausify(f.values[1]))
99 return ["-" + clausify(f.values[0])]
101 if f.values[0] in variables:
102 n = variables[f.values[0]]
104 n = len(variables) + 1
105 variables[f.values[0]] = n
111 out = "c DIMACS CNF input file generated by sml\n"
112 out += "c Author: Eugen Sawin <sawine@informatik.uni-freiburg.de>\n"
113 out += "p cnf %i %i\n" % (len(variables), len(clauses))
114 out += " 0\n".join([" ".join(c) for c in clauses]) + " 0\n"
115 return out, variables
118 return [fun(v) for v in f.values]
120 def expand_imp_eq(formula):
121 expmap = {IMP: lambda (a, b): Or(Not(a), b),
122 EQ: lambda (a, b): And(Or(Not(a), b), Or(a, Not(b)))}
123 if not isinstance(formula, Operator):
125 if formula.id in expmap:
126 return expmap[formula.id](values(expand_imp_eq, formula))
127 return formula.__class__(*values(expand_imp_eq, formula))
129 def de_morgan(formula):
130 negmap = {AND: lambda (a, b): Or(negate(a), negate(b)),
131 OR: lambda (a, b): And(negate(a), negate(b)),
132 BOX: lambda (a,): Diamond(negate(a)),
133 DIAMOND: lambda (a,): Box(negate(a)),
134 VARIABLE: lambda (a,): Not(Variable(a)),
137 return negmap[f.id](f.values)
138 if not isinstance(formula, Operator):
140 if formula.id == NOT:
141 return negate(formula.values[0])
142 return formula.__class__(*values(de_morgan, formula))
144 def reduce_iter(formula):
145 redset = set(((BOX, BOX), (DIAMOND, DIAMOND), (DIAMOND, BOX), (BOX, DIAMOND)))
146 if not isinstance(formula, Operator) or not isinstance(formula.values[0], Operator):
148 ids = (formula.id, formula.values[0].id)
150 return reduce_iter(formula.values[0])
151 return formula.__class__(*values(reduce_iter, formula))
153 def dist_mod(formula):
154 distmap = {(BOX, AND): lambda (a, b): And(Box(a), Box(b)),
155 (DIAMOND, OR): lambda (a, b): Or(Diamond(a), Diamond(b)),
156 (BOX, OR): lambda (a, b): (isinstance(a, Box) or isinstance(b, Box))
157 and Or(Box(a), Box(b)) or Box(Or(a, b)),
158 (DIAMOND, AND): lambda (a, b): (isinstance(a, Diamond) or isinstance(b, Diamond))
159 and And(Diamond(a), Diamond(b)) or Diamond(And(a, b))}
160 if not isinstance(formula, Operator) or not isinstance(formula.values[0], Operator):
162 ids = (formula.id, formula.values[0].id)
164 return distmap[ids](values(dist_mod, formula.values[0]))
165 return formula.__class__(*values(dist_mod, formula))
169 conj_id = int(formula.values[1].id == AND)
170 return And(Or(formula.values[conj_id].values[0], formula.values[1 - conj_id]),
171 Or(formula.values[conj_id].values[1], formula.values[1 - conj_id]));
178 sub_formulae.append(v)
183 return And(f, conjunct(bicon.pop()))
186 sub_formulae = [formula]
188 sub_formulae.reverse()
191 for s in sub_formulae:
192 for i, v in enumerate(s.values):
194 s.values[i] = known[v]
195 bicon.append(Eq(Variable("x" + str(len(bicon))), s))
196 known[s] = bicon[-1].values[0]
197 return mcnf(dist_mod(reduce_iter(de_morgan(expand_imp_eq(conjunct(known[formula]))))))
199 """ The Parser - Do NOT look below this line! """
213 class Operator(object):
214 def __init__(self, id, arity, *values):
217 self.values = list(values)
221 if self.id in (BOX, DIAMOND):
222 return 1 + self.values[0].depth()
224 return self.values[0].depth()
225 return max(self.values[0].depth(), self.values[1].depth())
226 def __eq__(self, other):
227 return self.id == other.id and self.values == other.values # commutative types not considered yet
231 out = str(self.values[0])
233 out = self.id + str(self.values[0])
234 elif self.arity == 2:
235 out = "(" + str(self.values[0]) + " " + self.id + " " + str(self.values[1]) + ")"
240 def __init__(self, *values):
241 Operator.__init__(self, NOT, Not.arity, *values)
247 def __init__(self, *values):
248 Operator.__init__(self, AND, And.arity, *values)
252 def __init__(self, *values):
253 Operator.__init__(self, OR, Or.arity, *values)
257 def __init__(self, *values):
258 Operator.__init__(self, IMP, Imp.arity, *values)
262 def __init__(self, *values):
263 Operator.__init__(self, EQ, Eq.arity, *values)
267 def __init__(self, *values):
268 Operator.__init__(self, BOX, Box.arity, *values)
270 class Diamond(Operator):
272 def __init__(self, *values):
273 Operator.__init__(self, DIAMOND, Diamond.arity, *values)
275 class Variable(Operator):
277 def __init__(self, *values):
278 Operator.__init__(self, VARIABLE, Variable.arity, *values)
282 def __init__(self, *values):
283 Operator.__init__(self, LB, Lb.arity, *values)
287 def __init__(self, *values):
288 Operator.__init__(self, RB, Rb.arity, *values)
290 class Formula(object):
294 TOKENS = {re.compile("\("): Lb,
295 re.compile("\)"): Rb,
296 re.compile("~"): Not,
297 re.compile("&"): And,
298 re.compile("\|"): Or,
299 re.compile("->"): Imp,
300 re.compile("<->"): Eq,
301 re.compile("\[\]"): Box,
302 re.compile("<>"): Diamond,
303 re.compile("[a-z]+"): Variable}
305 class Scanner(object):
306 def __init__(self, tokens, source=None):
310 while self.i < len(self.source):
312 for p, token in self.tokens.iteritems():
313 m = p.match(self.source[self.i:])
317 return (token, value)
320 def reset(self, source):
335 SYNTAX = ((Variable,),
345 class Parser(object):
346 def __init__(self, syntax, scanner):
348 self.scanner = scanner
349 def parse(self, source):
350 table = {(S, Variable): 0,
359 (A, Variable, And): 5,
360 (A, Variable, Or): 6,
361 (A, Variable, Imp): 7,
362 (A, Variable, Eq): 8,
363 (A, Not, Variable, And): 5,
364 (A, Not, Variable, Or): 6,
365 (A, Not, Variable, Imp): 7,
366 (A, Not, Variable, Eq): 8}
371 self.scanner.reset(source)
372 (token, value) = self.scanner.next()
373 (lookahead, la_value) = self.scanner.next()
374 (lookahead2, la2_value) = self.scanner.next()
376 while token and len(stack):
379 tree_nodes.append((token, value))
381 #tree_nodes.append((stack.pop(), value))
382 (token, value) = (lookahead, la_value)
383 (lookahead, la_value) = (lookahead2, la2_value)
384 #(lookahead, _) = self.scanner.next()
385 (lookahead2, la2_value) = self.scanner.next()
388 if (top, token) in table:
389 action = table[(top, token)]
390 elif (top, token, lookahead) in table:
391 action = table[(top, token, lookahead)]
392 elif (top, token, lookahead, lookahead2) in table:
393 action = table[(top, token, lookahead, lookahead2)]
400 stack.extend(reversed(self.syntax[action]))
401 accepted = accepted and not len(stack)
402 return (accepted, out, tree_nodes)
404 class SyntaxTree(object):
405 def __init__(self, seq, tree_nodes):
408 self.root = self.compile(seq, tree_nodes)[0]
409 def compile(self, seq, tree_nodes):
414 c, v = tree_nodes.pop()
416 c, v = tree_nodes.pop()
417 stack.append(Variable(v))
419 stack.append(Not(self.compile(seq, tree_nodes)))
421 stack.extend(self.compile(seq, tree_nodes))
423 stack.append(Box(self.compile(seq, tree_nodes)))
425 stack.append(Diamond(self.compile(seq, tree_nodes)))
427 stack.append(And(self.compile(seq, tree_nodes)))
429 stack.append(Or(self.compile(seq, tree_nodes)))
431 stack.append(Imp(self.compile(seq, tree_nodes)))
433 stack.append(Eq(self.compile(seq, tree_nodes)))
436 from argparse import ArgumentParser
438 def parse_arguments():
439 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.")
440 parser.add_argument("-f", "--formula", help="provide your own formula here, or better don't")
441 parser.add_argument("-d", "--dimacs", help="output file for the CNF DIMACS output")
442 return parser.parse_args()
444 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"""
446 if __name__ == "__main__":