# HG changeset patch
# User Eugen Sawin <sawine@me73.com>
# Date 1306763461 -7200
# Node ID 3418ff66b9ed3eb9260308438327f5ce9ba5abaa
# Parent  502d9d333417019466314d2cd1d236d3187097ac
Added DIMACS CNF input file generation.

diff -r 502d9d333417 -r 3418ff66b9ed sml.py
--- a/sml.py	Mon May 30 13:19:03 2011 +0200
+++ b/sml.py	Mon May 30 15:51:01 2011 +0200
@@ -15,9 +15,10 @@
     formula3 = Not(Not(p))
     formula4 = Imp(Box(Imp(Diamond(p), p)), Box(Imp(p, Box(p))))
     formula5 = Imp(And(Or(p, q), r), Not(s))
-    formula = formula4 # choose your formula here
+    formula6 = And(Or(p, Or(q, Not(s))), And(Or(r, Not(s)), Or(Not(p), s)))
+    formula = formula6 # choose your formula here
 
-    args = parse_arguments()
+    args = parse_arguments()   
     if (args.formula):
         scanner = Scanner(TOKENS)
         parser = Parser(SYNTAX, scanner)
@@ -43,6 +44,43 @@
     cnf_formula = cnf(original)
     print "alpha cnf: \t\t\t%s [%i]" % (cnf_formula, cnf_formula.depth())
 
+    if (args.dimacs):
+        with open(args.dimacs, "w") as f:
+            f.write(dimacs(formula))           
+
+def dimacs(formula):
+    def clausify(f):        
+        if f.id == AND:    
+            c1 = clausify(f.values[0])   
+            c2 = clausify(f.values[1])   
+            if c1:
+                clauses.append(clausify(f.values[0]))  
+            if c2:
+                clauses.append(clausify(f.values[1]))              
+        if f.id == OR:
+            clause = []         
+            clause.extend(clausify(f.values[0]))
+            clause.extend(clausify(f.values[1]))            
+            return clause
+        if f.id == NOT:
+            return ["-" + clausify(f.values[0])]
+        if f.id == VARIABLE:
+            if f.values[0] in variables:
+                n = variables[f.values[0]]
+            else:
+                n = len(variables) + 1
+                variables[f.values[0]] = n
+            return str(n)
+      
+    variables = {}
+    clauses = []
+    clausify(formula)
+    out = "c DIMACS CNF input file generated by sml\n"
+    out += "c Author: Eugen Sawin <sawine@informatik.uni-freiburg.de>\n"
+    out += "p cnf %i %i\n" % (len(variables), len(clauses))    
+    out += " 0\n".join([" ".join(c) for c in clauses]) + " 0\n"
+    return out
+
 def values(fun, f):  
     return [fun(v) for v in f.values] 
 
@@ -105,7 +143,13 @@
         for v in f.values:
             if v.id != VARIABLE:
                 sub_formulae.append(v)
-                part(v)
+                part(v) 
+
+    def conjunct(f):
+        if len(bicon):
+            return And(f, conjunct(bicon.pop()))
+        return f
+
     sub_formulae = [formula]
     part(formula)
     sub_formulae.reverse() 
@@ -116,11 +160,7 @@
             if v in known:
                 s.values[i] = known[v]
         bicon.append(Eq(Variable("x" + str(len(bicon))), s))
-        known[s] = bicon[-1].values[0]    
-    def conjunct(f):
-        if len(bicon):
-            return And(f, conjunct(bicon.pop()))
-        return f
+        known[s] = bicon[-1].values[0]     
     return mcnf(dist_mod(reduce_iter(de_morgan(expand_imp_eq(conjunct(known[formula]))))))
 
 """ The Parser - Do NOT look below this line! """ 
@@ -365,6 +405,7 @@
 def parse_arguments():
     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.")
     parser.add_argument("-f", "--formula", help="provide your own formula here, or better don't") 
+    parser.add_argument("-d", "--dimacs", help="output file for the CNF DIMACS output")
     return parser.parse_args()
  
 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"""