"""

 Name: sml - Simple Modal Logic Lib.

 Description: sml provides classes for simple modal logic formulae construction and reduction. It also features a disfunctional parser for the SML syntax.

 Author: Eugen Sawin <sawine@informatik.uni-freiburg.de>

 """

 TMP_DIMACS = "dimacs~"

 TMP_SOLUTION = "solution~"

 def main():

     # edit your formulae here

     p = Variable("p")

     q = Variable("q")

     r = Variable("r") 

     s = Variable("s")

     formula1 = Imp(Eq(p, q), r)

     formula2 = Not(Or(p, q))

     formula3 = Not(Not(p))

     formula4 = Imp(Box(Imp(Diamond(p), p)), Box(Imp(p, Box(p))))

     formula5 = Imp(And(Or(p, q), r), Not(s))

     formula6 = And(Or(p, Or(q, Not(s))), And(Or(r, Not(s)), Or(Not(p), s)))

     formula = formula6 # choose your formula here

     args = parse_arguments()   

     if (args.formula):

         scanner = Scanner(TOKENS)

         parser = Parser(SYNTAX, scanner)

         (accepted, out, tree_nodes) = parser.parse(args.formula)

         if not accepted:

             print EXCUSE 

             return

         tree = SyntaxTree(out, tree_nodes) 

         formula = tree.root

     original = formula

     print "formula: \t\t\t%s [%i]" % (formula, formula.depth())

     formula = expand_imp_eq(formula)

     print "expanded -> and <->: \t\t%s [%i]" % (formula, formula.depth()) 

     formula = de_morgan(formula)

     print "reduced ~: \t\t\t%s [%i]" % (formula, formula.depth()) 

     formula = reduce_iter(formula)

     print "reduced iterated modalities: \t%s [%i]" % (formula, formula.depth()) 

     formula = reduce_iter(dist_mod((formula)))

     print "distributed modalities+: \t%s [%i]" % (formula, formula.depth()) 

     formula = mcnf(formula)

     print "alpha mcnf: \t\t\t%s [%i]" % (formula, formula.depth())

     #cnf_formula = cnf(original)

     #print "alpha cnf: \t\t\t%s [%i]" % (cnf_formula, cnf_formula.depth())

     if not args.dimacs:

         dimacs_file = TMP_DIMACS

     else:

         dimacs_file = args.dimacs

     solution = sat_test(original, dimacs_file)

     if solution:

         print "satisfiable: \t\t\t%s " % (", ".join([str(s) for s in solution]))

     else:

         print "not satisfiable"

 from subprocess import call, PIPE

 def sat_test(formula, dimacs_file):

     out, variables = dimacs(formula)

     with open(dimacs_file, "w") as f:

         f.write(out) 

     call(["minisat2", "-verb=0", dimacs_file, TMP_SOLUTION], stdout=PIPE)

     with open(TMP_SOLUTION) as f:

         solved, assignment = f.readlines()  

     solved = solved[0] == "S"      

     if solved:

         positive = set() 

         for a in assignment.split():           

             neg = a[0] == "-"

             if not neg:

                 positive.add(int(a))       

         solution = []

         for v, n in variables.iteritems():           

             if n in positive:              

                 solution.append(Variable(v))

             else:

                 solution.append(Not(Variable(v)))

         return solution

 def dimacs(formula):

     def clausify(f):        

         if f.id == AND:    

             c1 = clausify(f.values[0])   

             c2 = clausify(f.values[1])   

             if c1:

                 clauses.append(clausify(f.values[0]))  

             if c2:

                 clauses.append(clausify(f.values[1]))              

         if f.id == OR:

             clause = []         

             clause.extend(clausify(f.values[0]))

             clause.extend(clausify(f.values[1]))            

             return clause

         if f.id == NOT:

             return ["-" + clausify(f.values[0])]

         if f.id == VARIABLE:

             if f.values[0] in variables:

                 n = variables[f.values[0]]

             else:

                 n = len(variables) + 1

                 variables[f.values[0]] = n

             return str(n)

     variables = {}

     clauses = []

     clausify(formula)

     out = "c DIMACS CNF input file generated by sml\n"

     out += "c Author: Eugen Sawin <sawine@informatik.uni-freiburg.de>\n"

     out += "p cnf %i %i\n" % (len(variables), len(clauses))    

     out += " 0\n".join([" ".join(c) for c in clauses]) + " 0\n"

     return out, variables

 def values(fun, f):  

     return [fun(v) for v in f.values] 

 def expand_imp_eq(formula):  

     expmap = {IMP: lambda (a, b): Or(Not(a), b),

               EQ: lambda (a, b): And(Or(Not(a), b), Or(a, Not(b)))}   

     if not isinstance(formula, Operator):   

         return formula

     if formula.id in expmap:

         return expmap[formula.id](values(expand_imp_eq, formula))   

     return formula.__class__(*values(expand_imp_eq, formula))

 def de_morgan(formula):    

     negmap = {AND: lambda (a, b): Or(negate(a), negate(b)),

               OR: lambda (a, b): And(negate(a), negate(b)),

               BOX: lambda (a,): Diamond(negate(a)),

               DIAMOND: lambda (a,): Box(negate(a)),

               VARIABLE: lambda (a,): Not(Variable(a)),

               NOT: lambda (a,): a}    

     def negate(f):

         return negmap[f.id](f.values)

     if not isinstance(formula, Operator):

         return formula  

     if formula.id == NOT:

         return negate(formula.values[0])

     return formula.__class__(*values(de_morgan, formula))

 def reduce_iter(formula):  

     redset = set(((BOX, BOX), (DIAMOND, DIAMOND), (DIAMOND, BOX), (BOX, DIAMOND)))

     if not isinstance(formula, Operator) or not isinstance(formula.values[0], Operator):

         return formula

     ids = (formula.id, formula.values[0].id)

     if ids in redset:

         return reduce_iter(formula.values[0])

     return formula.__class__(*values(reduce_iter, formula))

 def dist_mod(formula):    

     distmap = {(BOX, AND): lambda (a, b): And(Box(a), Box(b)),

                (DIAMOND, OR): lambda (a, b): Or(Diamond(a), Diamond(b)),

                (BOX, OR): lambda (a, b): (isinstance(a, Box) or isinstance(b, Box))               

                and Or(Box(a), Box(b)) or Box(Or(a, b)),

                (DIAMOND, AND): lambda (a, b): (isinstance(a, Diamond) or isinstance(b, Diamond))

                and And(Diamond(a), Diamond(b)) or Diamond(And(a, b))}   

     if not isinstance(formula, Operator) or not isinstance(formula.values[0], Operator):

         return formula

     ids = (formula.id, formula.values[0].id)

     if ids in distmap:

         return distmap[ids](values(dist_mod, formula.values[0]))

     return formula.__class__(*values(dist_mod, formula))    

 def mcnf(formula):

     if formula.id == OR:

         conj_id = int(formula.values[1].id == AND) 

         return And(Or(formula.values[conj_id].values[0], formula.values[1 - conj_id]), 

                     Or(formula.values[conj_id].values[1], formula.values[1 - conj_id]));

     return formula

 def cnf(formula):      

     def part(f):

         for v in f.values:

             if v.id != VARIABLE:

                 sub_formulae.append(v)

                 part(v) 

     def conjunct(f):

         if len(bicon):

             return And(f, conjunct(bicon.pop()))

         return f

     sub_formulae = [formula]

     part(formula)

     sub_formulae.reverse() 

     known = {}

     bicon = []

     for s in sub_formulae:       

         for i, v in enumerate(s.values):

             if v in known:

                 s.values[i] = known[v]

         bicon.append(Eq(Variable("x" + str(len(bicon))), s))

         known[s] = bicon[-1].values[0]     

     return mcnf(dist_mod(reduce_iter(de_morgan(expand_imp_eq(conjunct(known[formula]))))))

 """ The Parser - Do NOT look below this line! """ 

 import re

 NOT = "~"

 AND = "&"

 OR = "|"

 IMP = "->"

 EQ = "<->"

 BOX = "[]"

 DIAMOND = "<>"

 VARIABLE = "VAR"

 LB = "("

 RB = ")"

 class Operator(object):

     def __init__(self, id, arity, *values):

         self.id = id         

         self.arity = arity

         self.values = list(values)

     def depth(self):       

         if self.arity == 0:

             return 0

         if self.id in (BOX, DIAMOND):

             return 1 + self.values[0].depth()

         if self.id == NOT:           

             return self.values[0].depth()       

         return max(self.values[0].depth(), self.values[1].depth())

     def __eq__(self, other):

         return self.id == other.id and self.values == other.values # commutative types not considered yet

     def __str__(self):

         out = self.id

         if self.arity == 0:

             out = str(self.values[0])           

         if self.arity == 1:

             out = self.id + str(self.values[0])

         elif self.arity  == 2:          

             out = "(" + str(self.values[0]) + " " + self.id + " " + str(self.values[1]) + ")"

         return out

 class Not(Operator):

     arity = 1

     def __init__(self, *values):

         Operator.__init__(self, NOT, Not.arity, *values)       

     def __call__(self):

         pass

 class And(Operator):

     arity = 2

     def __init__(self, *values):

         Operator.__init__(self, AND, And.arity, *values)

 class Or(Operator):

     arity = 2

     def __init__(self, *values):

         Operator.__init__(self, OR, Or.arity, *values)       

 class Imp(Operator):

     arity = 2

     def __init__(self, *values):

         Operator.__init__(self, IMP, Imp.arity, *values)

 class Eq(Operator):

     arity = 2

     def __init__(self, *values):

         Operator.__init__(self, EQ, Eq.arity, *values)

 class Box(Operator):

     arity = 1

     def __init__(self, *values):

         Operator.__init__(self, BOX, Box.arity, *values)

 class Diamond(Operator):

     arity = 1

     def __init__(self, *values):

         Operator.__init__(self, DIAMOND, Diamond.arity, *values)

 class Variable(Operator):

     arity = 0

     def __init__(self, *values):

         Operator.__init__(self, VARIABLE, Variable.arity, *values)   

 class Lb(Operator):

     arity = -1

     def __init__(self, *values):

         Operator.__init__(self, LB, Lb.arity, *values)

 class Rb(Operator):

     arity = -1

     def __init__(self, *values):

         Operator.__init__(self, RB, Rb.arity, *values)

 class Formula(object):

     def __init__(self):

         pass 

 TOKENS = {re.compile("\("): Lb,

           re.compile("\)"): Rb,

           re.compile("~"): Not,

           re.compile("&"): And,

           re.compile("\|"): Or,

           re.compile("->"): Imp,

           re.compile("<->"): Eq,

           re.compile("\[\]"): Box,

           re.compile("<>"): Diamond,

           re.compile("[a-z]+"): Variable}

 class Scanner(object):

     def __init__(self, tokens, source=None):

         self.tokens = tokens

         self.reset(source)

     def next(self):         

         while self.i < len(self.source):

             re.purge()

             for p, token in self.tokens.iteritems():

                 m = p.match(self.source[self.i:])               

                 if m:                  

                     self.i += m.end(0)

                     value = m.group(0)  

                     return (token, value)

             self.i += 1

         return (None, None)

     def reset(self, source):

         self.i = 0

         self.source = source

 S = Formula

 A = "A"

 #0 S: (Variable,),

 #1 S: (Not, S),

 #2 S: (Lb, A, Rb),

 #3 S: (Box, S),

 #4 S: (Diamond, S),

 #5 A: (S, And, S),

 #6 A: (S, Or, S),

 #7 A: (S, Imp, S),

 #8 A: (S, Eq, S)

 SYNTAX = ((Variable,),

           (Not, S),

           (Lb, A, Rb),

           (Box, S),

           (Diamond, S),

           (S, And, S),

           (S, Or, S),

           (S, Imp, S),

           (S, Eq, S))

 class Parser(object):

     def __init__(self, syntax, scanner):

         self.syntax = syntax

         self.scanner = scanner

     def parse(self, source):

         table = {(S, Variable): 0,

                  (S, Not): 1,

                  (S, Lb): 2,

                  (S, Box): 3,

                  (S, Diamond): 4,

                  (A, S, And): 5,

                  (A, S, Or): 6,

                  (A, S, Imp): 7,

                  (A, S, Eq): 8,

                  (A, Variable, And): 5,

                  (A, Variable, Or): 6,

                  (A, Variable, Imp): 7,

                  (A, Variable, Eq): 8,

                  (A, Not, Variable, And): 5,

                  (A, Not, Variable, Or): 6,

                  (A, Not, Variable, Imp): 7,

                  (A, Not, Variable, Eq): 8}

         stack = [S]

         tree_nodes = []

         tree = None

         out = []

         self.scanner.reset(source)

         (token, value) = self.scanner.next()

         (lookahead, la_value) = self.scanner.next()

         (lookahead2, la2_value) = self.scanner.next()

         accepted = True 

         while token and len(stack): 

             top = stack[-1]               

             if top == token:

                 tree_nodes.append((token, value))

                 stack.pop()

                 #tree_nodes.append((stack.pop(), value))

                 (token, value) = (lookahead, la_value)

                 (lookahead, la_value) = (lookahead2, la2_value)

                 #(lookahead, _) = self.scanner.next()

                 (lookahead2, la2_value) = self.scanner.next()

             else:

                 action = None

                 if (top, token) in table:

                     action = table[(top, token)]

                 elif (top, token, lookahead) in table:

                     action = table[(top, token, lookahead)]  

                 elif (top, token, lookahead, lookahead2) in table:

                     action = table[(top, token, lookahead, lookahead2)]    

                 if action is None:

                     accepted = False

                     break

                 out.append(action)

                 stack.pop()

                 stack.extend(reversed(self.syntax[action]))

         accepted = accepted and not len(stack)

         return (accepted, out, tree_nodes) 

 class SyntaxTree(object):

     def __init__(self, seq, tree_nodes):

         seq.reverse()

         tree_nodes.reverse()      

         self.root = self.compile(seq, tree_nodes)[0]       

     def compile(self, seq, tree_nodes):

         stack = []     

         while len(seq):           

             s = seq.pop()

             if s == 0:

                 c, v = tree_nodes.pop()

                 while c != Variable:

                     c, v = tree_nodes.pop()

                 stack.append(Variable(v))

             elif s == 1:

                 stack.append(Not(self.compile(seq, tree_nodes)))

             elif s == 2:

                 stack.extend(self.compile(seq, tree_nodes))

             elif s == 3:

                 stack.append(Box(self.compile(seq, tree_nodes)))

             elif s == 4:

                 stack.append(Diamond(self.compile(seq, tree_nodes)))

             elif s == 5:

                 stack.append(And(self.compile(seq, tree_nodes)))

             elif s == 6:

                 stack.append(Or(self.compile(seq, tree_nodes)))

             elif s == 7:

                 stack.append(Imp(self.compile(seq, tree_nodes)))

             elif s == 8:

                 stack.append(Eq(self.compile(seq, tree_nodes)))       

         return stack   

 from argparse import ArgumentParser

 def parse_arguments():

     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.")

     parser.add_argument("-f", "--formula", help="provide your own formula here, or better don't") 

     parser.add_argument("-d", "--dimacs", help="output file for the CNF DIMACS output")

     return parser.parse_args()

 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"""

 if __name__ == "__main__":

     main()