Cacher is the code snippet organizer for pro developers

"""
A program to verify whether the proposition
entered is a tautology or not.

Run and Tested in Python 2.7

"""

import string
import itertools


class _Constants(object):
    """
    Constants for Tautology Verifier

    """
    BOOL_OPERATORS = ('!', '&', '|')
    PRECEDENCE = {'!': 3, '&': 2, '|': 1, '(': 0}
    TRUTH_DICT = {'True': True, 'False': False}
    BOOL_VALS = ('True', 'False')
    GRAMMAR = ('!', '&', '|', '(', ')')


def _clean_up(text):
    """
    Performs basic grammar check of the proposition after
    removing whitespaces.

    Throws error if variables are not part of the grammar defined.

    :param text: proposition
    :return : <List> of elements in cleaned up proposition
    """
    temp = []
    text = text.replace(' ', '')
    for t in text:
        if t in string.ascii_letters or t in _Constants.GRAMMAR:
            temp.append(t)
        else:
            raise ValueError("{0} in  proposition: {1} is invalid".format(t, text))
    return temp


def _get_postfix_expr(proposition, variables):
    """
    Generate postfix expression from the proposition
    list and variable list.

    Throws error if the infix expression is not correctly
    balanced.

    :param proposition: <List> infix expression
    :param variables : <Set> variables
    :return: the expression in postfix notation
    """

    temp = []
    postfix = []
    try:
        for i in proposition:
            if i == "(":
                temp.append(i)
            elif i == ")":
                elem = temp.pop()
                while elem is not "(":
                    postfix.append(elem)
                    elem = temp.pop()
            elif i in variables:
                postfix.append(i)
            elif i in _Constants.BOOL_OPERATORS:
                pre = _Constants.PRECEDENCE[i]
                while len(temp) != 0 and pre <= _Constants.PRECEDENCE.get(temp[-1], 4):
                    postfix.append(temp.pop())
                temp.append(i)

        while len(temp) > 0:
            postfix.append(temp.pop())
        postfix_expr = "".join(postfix)

    except IndexError:
        raise ValueError('Expression: {0} is not valid and unable to convert to postfix'.format("".join(proposition)))

    return postfix_expr


def _get_possibilities(variables):
    """
    Generate all the boolean possibilities for a set of variables

    2^n possibilities exist for n variables

    :param variables: Set of variables in the proposition
    :return: List of all boolean possibilities for the variables
    """
    possibilities = map(lambda x: zip(variables, x), list(itertools.product(['True', 'False'], repeat=len(variables))))
    return possibilities


def _evaluate_postfix_expr(t):
    """
    Evaluate the postfix expression.

    :param t: postfix expression
    :return: truth value of the post fix expression
    """
    pf = t.split(' ')
    eval_stack = []
    for i in pf:
        if i in _Constants.BOOL_VALS:
            eval_stack.append(i)
        elif i == '!':
            operand = eval_stack.pop()
            res = _logic_op(first_operand=operand, operator=i)
            eval_stack.append(res)
        else:
            first_operand = eval_stack.pop()
            second_operand = eval_stack.pop()
            res = _logic_op(first_operand=first_operand, operator=i, second_operand=second_operand)
            eval_stack.append(res)

    fin = eval_stack.pop()
    return fin


def _logic_op(first_operand, operator, second_operand=None):
    """
    For given operands , perform the boolean logic specified
    by the operator.

    :param first_operand: First operand  (True or False)
    :param operator: Boolean operator
    :param second_operand: Second operand which can be also None
    :return: Truth value of the expression
    """

    if operator == "!":
        return not _Constants.TRUTH_DICT[str(first_operand)]

    elif operator == '&':
        return _Constants.TRUTH_DICT[str(first_operand)] and _Constants.TRUTH_DICT[str(second_operand)]

    elif operator == '|':
        return _Constants.TRUTH_DICT[str(first_operand)] or _Constants.TRUTH_DICT[str(second_operand)]
    else:
        raise ValueError('Operator not defined')


def _eval_boolean(pf, p):
    """
    Method which evaluates the truth value for
    a given possibility combination of variables.

    :param pf: Proposition list
    :param p: Boolean possibilites for the variables
    :return: the boolean value obtained after postfix evaluation
    """
    t = " ".join(pf)
    for var, truth in p:
        t = t.replace(str(var), str(truth))
    res = _evaluate_postfix_expr(t)
    return res


def _calculate_tautology(proposition, possibilities):
    """

    Check whether the proposition is a tautology by
    checking the result for all the  boolean possible
    combinations.


    :param proposition: Proposition statement
    :param possibilities: Possibile boolean values
    :return: True if proposition is a tautology
    """
    truth = True
    for p in possibilities:

        bool_val = _eval_boolean(proposition, p)
        if bool_val == False:
            truth = False
            break
    return truth


def verify_tautology(proposition):
    """
    Verify whether a given propostion is tautology or not.

    :param proposition: Proposition statement
    :return: True if proposition is tautology, False if not
    """

    proposition = _clean_up(proposition)
    variables = set([proposition[i] for i in range(0, len(proposition)) if proposition[i] in string.ascii_letters])
    postfix_proposition = _get_postfix_expr(proposition, variables)
    possibilities = _get_possibilities(variables)
    res = _calculate_tautology(postfix_proposition, possibilities)
    print res


# Unit Test cases

verify_tautology('(!a | (a & a))')
verify_tautology('(!a | (b & !a)) ')
verify_tautology('(!a | a) ')
verify_tautology('((a & (!b | b)) | (!a & (!b | b))) ')

# Few extra test cases

# verify_tautology('a&b&c')
# verify_tautology('((a & (!b | b)) | (      !a & (!b | b))) ')
# verify_tautology('((a & (!b | b)) | (      !a & (!b | b)))) ')
# verify_tautology('#%^$^$#')