1.1 --- a/sml.py	Wed May 18 03:23:35 2011 +0200
     1.2 +++ b/sml.py	Wed May 18 03:51:08 2011 +0200
     1.3 @@ -36,7 +36,8 @@
     1.4      print "reduced iterated modalities: \t%s (%i)" % (formula, formula.depth()) 
     1.5      formula = reduce_iter(dist_mod((formula)))
     1.6      print "distributed modalities+: \t%s (%i)" % (formula, formula.depth()) 
     1.7 -    formula = None
     1.8 +    formula = mcnf(formula)
     1.9 +    print "alpha mcnf: \t\t\t%s (%i)" % (formula, formula.depth())
    1.10  
    1.11  def values(fun, f):  
    1.12      return [fun(v) for v in f.values] 
    1.13 @@ -86,7 +87,13 @@
    1.14      ids = (formula.id, formula.values[0].id)
    1.15      if ids in distmap:
    1.16          return distmap[ids](values(dist_mod, formula.values[0]))
    1.17 -    return formula.__class__(values(dist_mod, formula))        
    1.18 +    return formula.__class__(values(dist_mod, formula))    
    1.19 +
    1.20 +def mcnf(formula):
    1.21 +    if formula.id == OR:
    1.22 +        conj_id = int(formula.values[1].id == AND) 
    1.23 +        return And([Or([formula.values[conj_id].values[0], formula.values[1 - conj_id]]), 
    1.24 +                    Or([formula.values[conj_id].values[1], formula.values[1 - conj_id]])]);
    1.25   
    1.26  NOT = "~"
    1.27  AND = "&"