# HG changeset patch
# User Eugen Sawin <sawine@me73.com>
# Date 1305688145 -7200
# Node ID 53f84d13199869d8ee45502d2978bcc34e9458f5
# Parent  b7480b2e8fd2c891537bf3e89319b1735a2eb980
Basic CNF.

diff -r b7480b2e8fd2 -r 53f84d131998 sml.py
--- a/sml.py	Wed May 18 03:51:08 2011 +0200
+++ b/sml.py	Wed May 18 05:09:05 2011 +0200
@@ -9,12 +9,14 @@
     # edit your formulae here
     p = Variable(["p"])
     q = Variable(["q"])
-    r = Variable(["r"])
+    r = Variable(["r"]) 
+    s = Variable(["s"])
     formula1 = Imp([Eq([p, q]), r])
     formula2 = Not([Or([p, q])])
     formula3 = Not([Not([p])])
     formula4 = Imp([Box([Imp([Diamond([p]), p])]), Box([Imp([p, Box([p])])])])
-    formula = formula4 # choose your formula here
+    formula5 = Imp([And([Or([p, q]), r]), Not([s])])
+    formula = formula5 # choose your formula here
 
     args = parse_arguments()
     if (args.formula):
@@ -27,17 +29,20 @@
         tree = SyntaxTree(out, tree_nodes) 
         formula = tree.root
    
-    print "formula: \t\t\t%s (%i)" % (formula, formula.depth())
+    original = formula
+    print "formula: \t\t\t%s [%i]" % (formula, formula.depth())
     formula = expand_imp_eq(formula)
-    print "expanded -> and <->: \t\t%s (%i)" % (formula, formula.depth()) 
+    print "expanded -> and <->: \t\t%s [%i]" % (formula, formula.depth()) 
     formula = de_morgan(formula)
-    print "reduced ~: \t\t\t%s (%i)" % (formula, formula.depth()) 
+    print "reduced ~: \t\t\t%s [%i]" % (formula, formula.depth()) 
     formula = reduce_iter(formula)
-    print "reduced iterated modalities: \t%s (%i)" % (formula, formula.depth()) 
+    print "reduced iterated modalities: \t%s [%i]" % (formula, formula.depth()) 
     formula = reduce_iter(dist_mod((formula)))
-    print "distributed modalities+: \t%s (%i)" % (formula, formula.depth()) 
+    print "distributed modalities+: \t%s [%i]" % (formula, formula.depth()) 
     formula = mcnf(formula)
-    print "alpha mcnf: \t\t\t%s (%i)" % (formula, formula.depth())
+    print "alpha mcnf: \t\t\t%s [%i]" % (formula, formula.depth())
+    cnf_formula = cnf(original)
+    print "alpha cnf: \t\t\t%s [%i]" % (cnf_formula, cnf_formula.depth())
 
 def values(fun, f):  
     return [fun(v) for v in f.values] 
@@ -94,7 +99,33 @@
         conj_id = int(formula.values[1].id == AND) 
         return And([Or([formula.values[conj_id].values[0], formula.values[1 - conj_id]]), 
                     Or([formula.values[conj_id].values[1], formula.values[1 - conj_id]])]);
- 
+    return formula
+
+def cnf(formula):      
+    def part(f):
+        for v in f.values:
+            if v.id != VARIABLE:
+                sub_formulae.append(v)
+                part(v)
+    sub_formulae = [formula]
+    part(formula)
+    sub_formulae.reverse() 
+    known = {}
+    bicon = []
+    for s in sub_formulae:       
+        for i, v in enumerate(s.values):
+            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
+    return mcnf(dist_mod(reduce_iter(de_morgan(expand_imp_eq(conjunct(known[formula]))))))
+
+""" The Parser - Do NOT look below this line! """ 
+
 NOT = "~"
 AND = "&"
 OR = "|"
@@ -119,6 +150,8 @@
         if self.id == NOT:           
             return self.values[0].depth()
         return max(self.values[0].depth(), self.values[1].depth())
+    def __eq__(self, other):
+        return self.id == other.id and self.values == other.values # commutative types not considered yet
     def __str__(self):
         out = self.id
         if self.arity == 0:
@@ -338,8 +371,8 @@
 from argparse import ArgumentParser
 
 def parse_arguments():
-    parser = ArgumentParser(description="Parses simple modal logic syntax.")
-    parser.add_argument("-f", "--formula", help="your formula") 
+    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") 
     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"""