#!/usr/bin/env python
#coding: utf-8

OR_OP  = 1
AND_OP = 2
NOT_OP = 3

class NotAcceptableException(Exception): pass

class Operand:
    name = ""
    inverted = False

    def __eq__(self, other):
        return self._str_ == other._str_

    def __hash__(self):
        return self._hash_

    def __init__(self, name, inverted = False):
        assert(not name.startswith('!'))
        self.name = name
        self.inverted = inverted
        self.__gen_data__()

    def __gen_data__(self):
        self._str_  = self.__str__()
        self._hash_ = self._str_.__hash__()

    def invert(self):
        self.inverted = not self.inverted
        self.__gen_data__()

    def __str__(self):
        if self.inverted:
            return "!" + self.name
        else:
            return self.name

    def __repr__(self):
        return self._str_

# --------------------------------------------
# AND operation functions
# --------------------------------------------

# v is possible under cond ?
def is_acceptable(v, cond):
    if type(cond) == list:
        return all(map(lambda x: is_acceptable(v, x), cond))

    elif type(cond) == set:
        return all(map(lambda x: is_acceptable(v, x), cond))

    else:
        if v.name != cond.name or v.inverted == cond.inverted:
            return True
        else:
            raise NotAcceptableException()

# (ow = one way) are src conditions possible under dst ?
def is_ow_acceptable(src, dst):
    if type(src) == list:
        return all(map(lambda x: is_ow_acceptable(x, dst), src))

    elif type(src) == set:
        return all(map(lambda x: is_ow_acceptable(x, dst), src))

    else:
        return is_acceptable(src, dst)

# (tw = two way) are c1 and c2 possible simultaneously
def is_tw_acceptable(c1, c2):
    if c1 == None or c2 == None:
        return False

    ac2 = is_ow_acceptable(c1, c2)
    ac1 = is_ow_acceptable(c2, c1)
    return ac1 and ac2

# --------------------------------------------
# Common operation functions
# --------------------------------------------

# considers the different branches and may output a more compact one
# TODO: actually code the important part :P
def clean_branch_list(bl):
    l = []
    for i in xrange(len(bl)):
        bi = bl[i]

        already_contained = False
        to_delete = []

        le = len(l)
        for j in xrange(len(l)):
            bj = l[j]

            if bi.issubset(bj):
                if bj == bi:
                    to_delete.append(j)
                else:
                    already_contained = True

            elif bi.issuperset(bj):
                already_contained = True

        if not already_contained:
            l.append(bi)

        offset = 0
        for d in to_delete:
            l.pop(d - offset)
            offset += 1

    return l

# outputs the (con1 or con2) branch list
def rewrite_constraints_or(con1, con2):

    if type(con1) == set:
        con1 = [con1]

    if type(con2) == set:
        con2 = [con2]

    # Null operands?
    if con1 == None:
        if con2 == None:
            return None
        return con2

    elif con2 == None:
        return con1

    return clean_branch_list(con1 + con2)


# outputs the (con1 and con2) branch list
def rewrite_constraints_and(c1, c2):
    if type(c1) == set:
        c1 = [c1]
    elif c1 == None:
        c1 = []

    if type(c2) == set:
        c2 = [c2]
    elif c2 == None:
        c2 = []

    sets = []

    # Some optimization would be great here!! :P
    for x in c1:
        for y in c2:
            try:
                if is_tw_acceptable(x, y):
                    sets.append(x | y)

            except NotAcceptableException:
                pass

    if len(sets) == 0:
        return None
    else:
        return sets


# Obtains recursively the solution branches of a operation
def get_solutions(operand, inverted = False):
    if type(operand) == str:
        op = Operand(operand)
        if inverted:
            op.invert()
        return [set([op])]

    if not (type(operand) in (tuple, list)):
        raise Exception("Error: %s" % operand)

    if len(operand) == 2:
        op, op1 = operand
        sol = get_solutions(op1, not inverted)

        if op == NOT_OP:
            return sol
        raise Exception("%i operand doesn't apply to one operand (%s)" % (op,
                                                                       operand))

    else:
        try:
            op, op1, op2 = operand
        except:
            print "\x1b[0;91mOperation error"
            print len(operand)
            print operand, "\x1b[0m"
            raise Exception()

        sol1 = get_solutions(op1, inverted)
        sol2 = get_solutions(op2, inverted)

        if not inverted:
            if   op == OR_OP:
                return rewrite_constraints_or(sol1, sol2)

            elif op == AND_OP:
                return rewrite_constraints_and(sol1, sol2)

        else:
            if   op == OR_OP:
                return rewrite_constraints_and(sol1, sol2)

            elif op == AND_OP:
                return rewrite_constraints_or(sol1, sol2)


        raise Exception("%i operand doesn't apply to two operands" % op)

# TODO: Update this part
def get_solution_string(s):
    if type(s) == list:
        return ', '.join(map(get_solution_string, s))

    elif type(s) == set:
        return ', '.join(map(get_solution_string, s))

    else:
        return str(s)

# Pretty prints the solution branches
def print_solutions(sols):
    if sols == None:
        print "It's impossible!"
        return

    for s in sols:
        print get_solution_string(s)

    print '%i solution(s)' % len(sols)