1.1 --- a/sml.py Mon May 30 13:19:03 2011 +0200
1.2 +++ b/sml.py Mon May 30 15:51:01 2011 +0200
1.3 @@ -15,9 +15,10 @@
1.4 formula3 = Not(Not(p))
1.5 formula4 = Imp(Box(Imp(Diamond(p), p)), Box(Imp(p, Box(p))))
1.6 formula5 = Imp(And(Or(p, q), r), Not(s))
1.7 - formula = formula4 # choose your formula here
1.8 + formula6 = And(Or(p, Or(q, Not(s))), And(Or(r, Not(s)), Or(Not(p), s)))
1.9 + formula = formula6 # choose your formula here
1.10
1.11 - args = parse_arguments()
1.12 + args = parse_arguments()
1.13 if (args.formula):
1.14 scanner = Scanner(TOKENS)
1.15 parser = Parser(SYNTAX, scanner)
1.16 @@ -43,6 +44,43 @@
1.17 cnf_formula = cnf(original)
1.18 print "alpha cnf: \t\t\t%s [%i]" % (cnf_formula, cnf_formula.depth())
1.19
1.20 + if (args.dimacs):
1.21 + with open(args.dimacs, "w") as f:
1.22 + f.write(dimacs(formula))
1.23 +
1.24 +def dimacs(formula):
1.25 + def clausify(f):
1.26 + if f.id == AND:
1.27 + c1 = clausify(f.values[0])
1.28 + c2 = clausify(f.values[1])
1.29 + if c1:
1.30 + clauses.append(clausify(f.values[0]))
1.31 + if c2:
1.32 + clauses.append(clausify(f.values[1]))
1.33 + if f.id == OR:
1.34 + clause = []
1.35 + clause.extend(clausify(f.values[0]))
1.36 + clause.extend(clausify(f.values[1]))
1.37 + return clause
1.38 + if f.id == NOT:
1.39 + return ["-" + clausify(f.values[0])]
1.40 + if f.id == VARIABLE:
1.41 + if f.values[0] in variables:
1.42 + n = variables[f.values[0]]
1.43 + else:
1.44 + n = len(variables) + 1
1.45 + variables[f.values[0]] = n
1.46 + return str(n)
1.47 +
1.48 + variables = {}
1.49 + clauses = []
1.50 + clausify(formula)
1.51 + out = "c DIMACS CNF input file generated by sml\n"
1.52 + out += "c Author: Eugen Sawin <sawine@informatik.uni-freiburg.de>\n"
1.53 + out += "p cnf %i %i\n" % (len(variables), len(clauses))
1.54 + out += " 0\n".join([" ".join(c) for c in clauses]) + " 0\n"
1.55 + return out
1.56 +
1.57 def values(fun, f):
1.58 return [fun(v) for v in f.values]
1.59
1.60 @@ -105,7 +143,13 @@
1.61 for v in f.values:
1.62 if v.id != VARIABLE:
1.63 sub_formulae.append(v)
1.64 - part(v)
1.65 + part(v)
1.66 +
1.67 + def conjunct(f):
1.68 + if len(bicon):
1.69 + return And(f, conjunct(bicon.pop()))
1.70 + return f
1.71 +
1.72 sub_formulae = [formula]
1.73 part(formula)
1.74 sub_formulae.reverse()
1.75 @@ -116,11 +160,7 @@
1.76 if v in known:
1.77 s.values[i] = known[v]
1.78 bicon.append(Eq(Variable("x" + str(len(bicon))), s))
1.79 - known[s] = bicon[-1].values[0]
1.80 - def conjunct(f):
1.81 - if len(bicon):
1.82 - return And(f, conjunct(bicon.pop()))
1.83 - return f
1.84 + known[s] = bicon[-1].values[0]
1.85 return mcnf(dist_mod(reduce_iter(de_morgan(expand_imp_eq(conjunct(known[formula]))))))
1.86
1.87 """ The Parser - Do NOT look below this line! """
1.88 @@ -365,6 +405,7 @@
1.89 def parse_arguments():
1.90 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.91 parser.add_argument("-f", "--formula", help="provide your own formula here, or better don't")
1.92 + parser.add_argument("-d", "--dimacs", help="output file for the CNF DIMACS output")
1.93 return parser.parse_args()
1.94
1.95 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"""