1.1 --- a/smm.py	Tue May 17 13:52:38 2011 +0200
     1.2 +++ b/smm.py	Tue May 17 14:05:25 2011 +0200
     1.3 @@ -19,24 +19,24 @@
     1.4      q = Variable(["q"])
     1.5      r = Variable(["r"])
     1.6      formula = Imp([Eq([p, q]), r])
     1.7 -    formula = Not([Or([p, q])])
     1.8 -    formula = Not([Not([p])])
     1.9 +    #formula = Not([Or([p, q])])
    1.10 +    #formula = Not([Not([p])])
    1.11      print formula
    1.12      print "reduced"
    1.13      print reduce(formula)
    1.14  
    1.15 -
    1.16 -def reduce(formula):
    1.17 +def reduce(formula):  
    1.18      map = {IMP: lambda (a, b): Or([Not([a]), b]),
    1.19             EQ: lambda (a, b): And([Or([Not([a]), b]), Or([a, Not([b])])]),
    1.20 -           NOT: lambda (a,): not isinstance(a, Not) and a.__class__([Not([v]) for v in a.values]) or Not(a.values),
    1.21 +           NOT: lambda (a,): not isinstance(a, Not) 
    1.22 +           and not isinstance(a.values[0], Not) 
    1.23 +           and a.__class__([Not([v]) for v in a.values]) or a.values[0],
    1.24             AND: lambda (a, b): And([a, b]), 
    1.25             OR: lambda (a, b): Or([a, b])}
    1.26 -    def values():
    1.27 +    def values():       
    1.28          return [reduce(v) for v in formula.values] 
    1.29  
    1.30 -    if not isinstance(formula, Operator) or formula.id not in map:
    1.31 -        print "skipped"
    1.32 +    if not isinstance(formula, Operator) or formula.id not in map:       
    1.33          return formula
    1.34      return map[formula.id](values())    
    1.35