1.1 --- a/sml.py	Mon May 30 13:19:03 2011 +0200
     1.2 +++ b/sml.py	Mon May 30 15:51:01 2011 +0200
     1.3 @@ -15,9 +15,10 @@
     1.4      formula3 = Not(Not(p))
     1.5      formula4 = Imp(Box(Imp(Diamond(p), p)), Box(Imp(p, Box(p))))
     1.6      formula5 = Imp(And(Or(p, q), r), Not(s))
     1.7 -    formula = formula4 # choose your formula here
     1.8 +    formula6 = And(Or(p, Or(q, Not(s))), And(Or(r, Not(s)), Or(Not(p), s)))
     1.9 +    formula = formula6 # choose your formula here
    1.10  
    1.11 -    args = parse_arguments()
    1.12 +    args = parse_arguments()   
    1.13      if (args.formula):
    1.14          scanner = Scanner(TOKENS)
    1.15          parser = Parser(SYNTAX, scanner)
    1.16 @@ -43,6 +44,43 @@
    1.17      cnf_formula = cnf(original)
    1.18      print "alpha cnf: \t\t\t%s [%i]" % (cnf_formula, cnf_formula.depth())
    1.19  
    1.20 +    if (args.dimacs):
    1.21 +        with open(args.dimacs, "w") as f:
    1.22 +            f.write(dimacs(formula))           
    1.23 +
    1.24 +def dimacs(formula):
    1.25 +    def clausify(f):        
    1.26 +        if f.id == AND:    
    1.27 +            c1 = clausify(f.values[0])   
    1.28 +            c2 = clausify(f.values[1])   
    1.29 +            if c1:
    1.30 +                clauses.append(clausify(f.values[0]))  
    1.31 +            if c2:
    1.32 +                clauses.append(clausify(f.values[1]))              
    1.33 +        if f.id == OR:
    1.34 +            clause = []         
    1.35 +            clause.extend(clausify(f.values[0]))
    1.36 +            clause.extend(clausify(f.values[1]))            
    1.37 +            return clause
    1.38 +        if f.id == NOT:
    1.39 +            return ["-" + clausify(f.values[0])]
    1.40 +        if f.id == VARIABLE:
    1.41 +            if f.values[0] in variables:
    1.42 +                n = variables[f.values[0]]
    1.43 +            else:
    1.44 +                n = len(variables) + 1
    1.45 +                variables[f.values[0]] = n
    1.46 +            return str(n)
    1.47 +      
    1.48 +    variables = {}
    1.49 +    clauses = []
    1.50 +    clausify(formula)
    1.51 +    out = "c DIMACS CNF input file generated by sml\n"
    1.52 +    out += "c Author: Eugen Sawin <sawine@informatik.uni-freiburg.de>\n"
    1.53 +    out += "p cnf %i %i\n" % (len(variables), len(clauses))    
    1.54 +    out += " 0\n".join([" ".join(c) for c in clauses]) + " 0\n"
    1.55 +    return out
    1.56 +
    1.57  def values(fun, f):  
    1.58      return [fun(v) for v in f.values] 
    1.59  
    1.60 @@ -105,7 +143,13 @@
    1.61          for v in f.values:
    1.62              if v.id != VARIABLE:
    1.63                  sub_formulae.append(v)
    1.64 -                part(v)
    1.65 +                part(v) 
    1.66 +
    1.67 +    def conjunct(f):
    1.68 +        if len(bicon):
    1.69 +            return And(f, conjunct(bicon.pop()))
    1.70 +        return f
    1.71 +
    1.72      sub_formulae = [formula]
    1.73      part(formula)
    1.74      sub_formulae.reverse() 
    1.75 @@ -116,11 +160,7 @@
    1.76              if v in known:
    1.77                  s.values[i] = known[v]
    1.78          bicon.append(Eq(Variable("x" + str(len(bicon))), s))
    1.79 -        known[s] = bicon[-1].values[0]    
    1.80 -    def conjunct(f):
    1.81 -        if len(bicon):
    1.82 -            return And(f, conjunct(bicon.pop()))
    1.83 -        return f
    1.84 +        known[s] = bicon[-1].values[0]     
    1.85      return mcnf(dist_mod(reduce_iter(de_morgan(expand_imp_eq(conjunct(known[formula]))))))
    1.86  
    1.87  """ The Parser - Do NOT look below this line! """ 
    1.88 @@ -365,6 +405,7 @@
    1.89  def parse_arguments():
    1.90      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.91      parser.add_argument("-f", "--formula", help="provide your own formula here, or better don't") 
    1.92 +    parser.add_argument("-d", "--dimacs", help="output file for the CNF DIMACS output")
    1.93      return parser.parse_args()
    1.94   
    1.95  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"""