"""

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()