1.1 --- a/sml.py	Tue May 17 16:11:11 2011 +0200
     1.2 +++ b/sml.py	Tue May 17 18:00:34 2011 +0200
     1.3 @@ -15,7 +15,7 @@
     1.4      formula1 = Imp([Eq([p, q]), r])
     1.5      formula2 = Not([Or([p, q])])
     1.6      formula3 = Not([Not([p])])
     1.7 -    use = formula1
     1.8 +    formula =  formula1
     1.9  
    1.10      args = parse_arguments()
    1.11      if (args.formula):
    1.12 @@ -28,25 +28,54 @@
    1.13          tree = SyntaxTree(out, tree_nodes) 
    1.14          formula = tree.root
    1.15     
    1.16 -    print formula
    1.17 -    print "reduced"
    1.18 -    print reduce(formula)
    1.19 -    print reduce(formula)
    1.20 +    print "formula: \t\t", formula
    1.21 +    print "expanded -> and <->: \t", expand_imp_eq(formula)
    1.22 +    print "reduced ~: \t\t", reduce_not(expand_imp_eq(formula))
    1.23  
    1.24 -def reduce(formula):  
    1.25 +def expand_imp_eq(formula):  
    1.26      map = {IMP: lambda (a, b): Or([Not([a]), b]),
    1.27 -           EQ: lambda (a, b): And([Or([Not([a]), b]), Or([a, Not([b])])]),
    1.28 -           NOT: lambda (a,): not isinstance(a, Not) 
    1.29 -           and not isinstance(a.values[0], Not) 
    1.30 -           and a.__class__([Not([v]) for v in a.values]) or a.values[0],
    1.31 -           AND: lambda (a, b): And([a, b]), 
    1.32 -           OR: lambda (a, b): Or([a, b])}
    1.33 +           EQ: lambda (a, b): And([Or([Not([a]), b]), Or([a, Not([b])])])}
    1.34 +
    1.35      def values():       
    1.36 -        return [reduce(v) for v in formula.values] 
    1.37 +        return [expand_imp_eq(v) for v in formula.values] 
    1.38  
    1.39      if not isinstance(formula, Operator) or formula.id not in map:       
    1.40          return formula
    1.41 -    return map[formula.id](values())    
    1.42 +    return map[formula.id](values())   
    1.43 +
    1.44 +def reduce_not(formula):  
    1.45 +    negmap = {AND: lambda (a, b): Or([negate(a), negate(b)]),
    1.46 +              OR: lambda (a, b): And([negate(a), negate(b)]),
    1.47 +              VARIABLE: lambda (a,): Not([a]),
    1.48 +              NOT: lambda (a,): a}
    1.49 +
    1.50 +    def values():
    1.51 +        return [reduce_not(v) for v in formula.values]
    1.52 +
    1.53 +    def negate(f):
    1.54 +         return negmap[f.id](f.values)
    1.55 +
    1.56 +    if not isinstance(formula, Operator):
    1.57 +        return formula   
    1.58 +    if formula.id == NOT:
    1.59 +        return negate(formula.values[0])
    1.60 +    return formula.__class__(values())
    1.61 +
    1.62 +
    1.63 +
    1.64 +
    1.65 +    map = {NOT: lambda (a,): not isinstance(a, Not) 
    1.66 +           and not isinstance(a.values[0], Not) 
    1.67 +           and a.__class__([Not([reduce2(v)]) for v in a.values]) or a.values[0]}
    1.68 +
    1.69 +    def values(): 
    1.70 +        return [reduce2(v) for v in formula.values] 
    1.71 +
    1.72 +    if not isinstance(formula, Operator) or not isinstance(formula.values[0], Operator):
    1.73 +        return formula 
    1.74 +    elif formula.id not in map: 
    1.75 +        return formula.__class__(values())
    1.76 +    return map[formula.id](values())   
    1.77   
    1.78  NOT = "~"
    1.79  AND = "&"
    1.80 @@ -55,7 +84,7 @@
    1.81  EQ = "<->"
    1.82  BOX = "[]"
    1.83  DIAMOND = "<>"
    1.84 -VARIABLE = "p"
    1.85 +VARIABLE = "VAR"
    1.86  LB = "("
    1.87  RB = ")"
    1.88