1.1 --- a/sml.py	Wed May 18 03:51:08 2011 +0200
     1.2 +++ b/sml.py	Wed May 18 05:09:05 2011 +0200
     1.3 @@ -9,12 +9,14 @@
     1.4      # edit your formulae here
     1.5      p = Variable(["p"])
     1.6      q = Variable(["q"])
     1.7 -    r = Variable(["r"])
     1.8 +    r = Variable(["r"]) 
     1.9 +    s = Variable(["s"])
    1.10      formula1 = Imp([Eq([p, q]), r])
    1.11      formula2 = Not([Or([p, q])])
    1.12      formula3 = Not([Not([p])])
    1.13      formula4 = Imp([Box([Imp([Diamond([p]), p])]), Box([Imp([p, Box([p])])])])
    1.14 -    formula = formula4 # choose your formula here
    1.15 +    formula5 = Imp([And([Or([p, q]), r]), Not([s])])
    1.16 +    formula = formula5 # choose your formula here
    1.17  
    1.18      args = parse_arguments()
    1.19      if (args.formula):
    1.20 @@ -27,17 +29,20 @@
    1.21          tree = SyntaxTree(out, tree_nodes) 
    1.22          formula = tree.root
    1.23     
    1.24 -    print "formula: \t\t\t%s (%i)" % (formula, formula.depth())
    1.25 +    original = formula
    1.26 +    print "formula: \t\t\t%s [%i]" % (formula, formula.depth())
    1.27      formula = expand_imp_eq(formula)
    1.28 -    print "expanded -> and <->: \t\t%s (%i)" % (formula, formula.depth()) 
    1.29 +    print "expanded -> and <->: \t\t%s [%i]" % (formula, formula.depth()) 
    1.30      formula = de_morgan(formula)
    1.31 -    print "reduced ~: \t\t\t%s (%i)" % (formula, formula.depth()) 
    1.32 +    print "reduced ~: \t\t\t%s [%i]" % (formula, formula.depth()) 
    1.33      formula = reduce_iter(formula)
    1.34 -    print "reduced iterated modalities: \t%s (%i)" % (formula, formula.depth()) 
    1.35 +    print "reduced iterated modalities: \t%s [%i]" % (formula, formula.depth()) 
    1.36      formula = reduce_iter(dist_mod((formula)))
    1.37 -    print "distributed modalities+: \t%s (%i)" % (formula, formula.depth()) 
    1.38 +    print "distributed modalities+: \t%s [%i]" % (formula, formula.depth()) 
    1.39      formula = mcnf(formula)
    1.40 -    print "alpha mcnf: \t\t\t%s (%i)" % (formula, formula.depth())
    1.41 +    print "alpha mcnf: \t\t\t%s [%i]" % (formula, formula.depth())
    1.42 +    cnf_formula = cnf(original)
    1.43 +    print "alpha cnf: \t\t\t%s [%i]" % (cnf_formula, cnf_formula.depth())
    1.44  
    1.45  def values(fun, f):  
    1.46      return [fun(v) for v in f.values] 
    1.47 @@ -94,7 +99,33 @@
    1.48          conj_id = int(formula.values[1].id == AND) 
    1.49          return And([Or([formula.values[conj_id].values[0], formula.values[1 - conj_id]]), 
    1.50                      Or([formula.values[conj_id].values[1], formula.values[1 - conj_id]])]);
    1.51 - 
    1.52 +    return formula
    1.53 +
    1.54 +def cnf(formula):      
    1.55 +    def part(f):
    1.56 +        for v in f.values:
    1.57 +            if v.id != VARIABLE:
    1.58 +                sub_formulae.append(v)
    1.59 +                part(v)
    1.60 +    sub_formulae = [formula]
    1.61 +    part(formula)
    1.62 +    sub_formulae.reverse() 
    1.63 +    known = {}
    1.64 +    bicon = []
    1.65 +    for s in sub_formulae:       
    1.66 +        for i, v in enumerate(s.values):
    1.67 +            if v in known:
    1.68 +                s.values[i] = known[v]
    1.69 +        bicon.append(Eq([Variable(["x" + str(len(bicon))]), s]))
    1.70 +        known[s] = bicon[-1].values[0]    
    1.71 +    def conjunct(f):
    1.72 +        if len(bicon):
    1.73 +            return And([f, conjunct(bicon.pop())])
    1.74 +        return f
    1.75 +    return mcnf(dist_mod(reduce_iter(de_morgan(expand_imp_eq(conjunct(known[formula]))))))
    1.76 +
    1.77 +""" The Parser - Do NOT look below this line! """ 
    1.78 +
    1.79  NOT = "~"
    1.80  AND = "&"
    1.81  OR = "|"
    1.82 @@ -119,6 +150,8 @@
    1.83          if self.id == NOT:           
    1.84              return self.values[0].depth()
    1.85          return max(self.values[0].depth(), self.values[1].depth())
    1.86 +    def __eq__(self, other):
    1.87 +        return self.id == other.id and self.values == other.values # commutative types not considered yet
    1.88      def __str__(self):
    1.89          out = self.id
    1.90          if self.arity == 0:
    1.91 @@ -338,8 +371,8 @@
    1.92  from argparse import ArgumentParser
    1.93  
    1.94  def parse_arguments():
    1.95 -    parser = ArgumentParser(description="Parses simple modal logic syntax.")
    1.96 -    parser.add_argument("-f", "--formula", help="your formula") 
    1.97 +    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.")
    1.98 +    parser.add_argument("-f", "--formula", help="provide your own formula here, or better don't") 
    1.99      return parser.parse_args()
   1.100   
   1.101  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"""