# Exercise 2 Task 5
# Axel Hoffmann, Johannes Wendel, Jonas Zeunert

import sys
import collections
from itertools import izip, product

# Some magic to define new operators
class Infix:
    def __init__(self, function):
        self.function = function
    def __ror__(self, other):
        return Infix(lambda x, self=self, other=other: self.function(other, x))
    def __or__(self, other):
        return self.function(other)
    def __rlshift__(self, other):
        return Infix(lambda x, self=self, other=other: self.function(other, x))
    def __rshift__(self, other):
        return self.function(other)
    def __call__(self, value1, value2):
        return self.function(value1, value2)

# define 2 new operators |implies| and |equiv|
implies = Infix(lambda x,y: not x or y)
equiv = Infix(lambda x, y: (x |implies| y) and (y |implies| x))

# possible logic functions
logical_operators = ["not", "and", "or", "implies", "equiv"]

#convert given formula to DNF
def convert(formula):
    result = "("
    literals = extract_literals(formula)
    truthtable = create_truthtable(len(literals))

    # replace for usage with Infix
    formula = formula.replace("implies", "|implies|")
    formula = formula.replace("equiv", "|equiv|")

    # for right output
    firstrun = True
    # try all allocations in truthtable
    for allocation in truthtable:
        # Update global variables
        for literal, value in izip(literals, allocation):
            literals[literal] = value
        globals().update(literals)

        # Evaluate formula with given truthtable allocation and add DNF
        if(eval(formula)):
            if(not firstrun):
                result += " or ("

            print_and = False
            for key, value in literals.iteritems():
                if(print_and):
                    result += " and "

                if(not value):
                    result += "not "
                result += key

                print_and = True

            firstrun = False
            result += ")"
    return result

# Extracts all literals (every substring thats not a logical_operator) from given string
# Returns a dictionary with all literals in the string
def extract_literals(string):
    literals = {}
    # ignore brackets and split string
    literals_str = string.replace('(', ' ').replace(')', ' ').split()
    for l in literals_str:
        if(not(l in logical_operators)):
            literals[l] = False
    # sort literals
    sorted_literals = collections.OrderedDict(sorted(literals.items()))
    return sorted_literals

def create_truthtable(num):
    return list(product([True, False], repeat=num))

def utf8_convert(formula):
    formula = formula.replace("and", "\\u2227")
    formula = formula.replace("or", "\\u2228")
    formula = formula.replace("not ", "\\u00ac")
    formula = formula.replace("implies", "\\u2192")
    formula = formula.replace("equiv", "\\u2194")
    return formula.decode('unicode-escape')

if __name__ == "__main__":
    if(len(sys.argv) != 2):
        print("Usage: " +
              sys.argv[0] + " \"formula\" \n" +
              "Where usable logical operators are:")
        print(logical_operators)
        quit()

    input = sys.argv[1]

    print("Input:")
    print(utf8_convert(input))

    converted_formula = convert(input)

    print("\nConverted formula:")
    print(utf8_convert(converted_formula))