# HG changeset patch
# User Eugen Sawin <sawine@me73.com>
# Date 1305633925 -7200
# Node ID c7ca4a177c908772a1c9dd542821ce954cebefa2
# Parent  7e81bfff05217f17e7f827ba87f3c52d354c4058
Fixed double not reduction.

diff -r 7e81bfff0521 -r c7ca4a177c90 smm.py
--- a/smm.py	Tue May 17 13:52:38 2011 +0200
+++ b/smm.py	Tue May 17 14:05:25 2011 +0200
@@ -19,24 +19,24 @@
     q = Variable(["q"])
     r = Variable(["r"])
     formula = Imp([Eq([p, q]), r])
-    formula = Not([Or([p, q])])
-    formula = Not([Not([p])])
+    #formula = Not([Or([p, q])])
+    #formula = Not([Not([p])])
     print formula
     print "reduced"
     print reduce(formula)
 
-
-def reduce(formula):
+def reduce(formula):  
     map = {IMP: lambda (a, b): Or([Not([a]), b]),
            EQ: lambda (a, b): And([Or([Not([a]), b]), Or([a, Not([b])])]),
-           NOT: lambda (a,): not isinstance(a, Not) and a.__class__([Not([v]) for v in a.values]) or Not(a.values),
+           NOT: lambda (a,): not isinstance(a, Not) 
+           and not isinstance(a.values[0], Not) 
+           and a.__class__([Not([v]) for v in a.values]) or a.values[0],
            AND: lambda (a, b): And([a, b]), 
            OR: lambda (a, b): Or([a, b])}
-    def values():
+    def values():       
         return [reduce(v) for v in formula.values] 
 
-    if not isinstance(formula, Operator) or formula.id not in map:
-        print "skipped"
+    if not isinstance(formula, Operator) or formula.id not in map:       
         return formula
     return map[formula.id](values())