def binrange(bits):
    for num in range(2**bits):
        l = []
        while len(l) < bits:
            l.insert(0, bool(num & 1))
            num >>= 1
        yield l

def getvars(prop):
    if isinstance(prop, Variable):
        return set([prop])
    else:
        return reduce(set.union, map(getvars, prop.children))


class Proposition(object):
    def __init__(self, *children):
        assert type(self) != Proposition, "Proposition must be subclassed"
        self.children = children
    
    def substitute(self, var, prop):
        if self == var:
            return prop
        else:
            args = []
            for child in self.children:
                if isinstance(child, Proposition):
                    args.append(child.substitute(var, prop))
                elif child == var:
                    args.append(prop)
                else:
                    args.append(child)
            return self.__class__(*args).evaluate()
    
    def evaluate(self):
        raise NotImplementedError
    
    def __or__(self, other):
        return Or(self, other).evaluate()
    
    def __and__(self, other):
        return And(self, other).evaluate()
    
    def __invert__(self):
        return Not(self).evaluate()
    
    def __repr__(self):
        return str(self)


class Variable(Proposition):
    def __init__(self, name="some condition"):
        self.name = name
        super(Variable, self).__init__(self)
    
    def __eq__(self, other):
        if isinstance(other, Variable):
            return self is other
    
    def __str__(self):
        if self.name.isalpha():
            return self.name
        else:
            return "(%s)" % self.name
    
    def substitute(self, var, prop):
        if var is self:
            return prop
        else:
            return self
    
    def evaluate(self):
        return self


class Function(Proposition):
    associative = False
    operatorstr = None
    
    def __init__(self, *args):
        self.children = []
        for arg in args:
            if self.associative and type(arg) == type(self):
                self.children += arg.children
            else:
                self.children.append(arg)
    
    def __str__(self):
        if self.operatorstr:
            if len(self.children) == 1:
                return str(self.children[0])
            else:
                return "(%s)" % self.operatorstr.join([str(child) for child in self.children])
        else:
            return "%s(%s)" % (self.__class__.__name__, ', '.join([str(child) for child in children]))
    
    def evaluate(self):
        raise NotImplementedError


class And(Function):
    associative = True
    operatorstr = " & "
    
    def evaluate(self):
        if len(self.children) == 1:
            return self.children[0]
        
        conditions = []
        for child in self.children:
            if isinstance(child, Proposition):
                result = child.evaluate()
            else:
                result = child
            if result is False:
                return False
            elif result is not True:
                conditions.append(result)
        if conditions:
            return And(*conditions)
        else:
            return True

class Or(Function):
    associative = True
    operatorstr = " | "
    
    def evaluate(self):
        if len(self.children) == 1:
            return self.children[0]
        
        conditions = []
        for child in self.children:
            if isinstance(child, Proposition):
                result = child.evaluate()
            else:
                result = child
            if result is True:
                return True
            elif result is not False:
                conditions.append(result)
        if conditions:
            return Or(*conditions)
        else:
            return False


#XXX todo de morgans law
class Not(Function):
    def evaluate(self):
        # handle not-not
        if isinstance(self.children[0], Not):
            result = self.children[0].children[0]
            if isinstance(result, Proposition):
                return result.evaluate()
            return result
        
        if isinstance(self.children[0], Proposition):
            result = self.children[0].evaluate()
        else:
            result = self.children[0]
        
        if isinstance(result, bool):
            return not result
        else:
            return Not(result)
    
    def __str__(self):
        return "~%s" % self.children[0]


class TruthTable(object):
    def __init__(self, *props):
        assert len(props), "a truth table must have at least one column"
        
        self.vars = [prop for prop in props if isinstance(prop, Variable)]
        self.props = props
        self.filterprop = True
    
    def __str__(self):
        cols = []
        cols.append([str(props) for props in self.props])
        for values in binrange(len(self.vars)):
            col = []
            for prop in self.props + (self.filterprop,):
                for i in range(len(self.vars)):
                    if not isinstance(prop, Proposition):
                        break
                    prop = prop.substitute(self.vars[i], values[i])
                col.append(prop)
            filterresult = col.pop()
            if isinstance(filterresult, bool) and filterresult:
                cols.append(map(str, col))
        
        rowlengths = [[len(row) for row in col] for col in cols]
        maxlengths = tuple(reduce(lambda a,b: map(max, a, b), rowlengths))
        
        lines = []
        doneheader = False
        for col in cols:
            lines.append((' | '.join(['%%-%ds'] * len(col)) % maxlengths) % tuple(col))
            if not doneheader:
                doneheader = True
                lines.append('-' * (sum(maxlengths) + 3 * (len(maxlengths) - 1)))
        return '\n'.join(lines)
    
    def filter(self, prop):
        self.filterprop = And(self.filterprop, prop).evaluate()
        return self
    
    __repr__ = __str__

for char in "abcdefghijklmnopqrstuvwxyz":
    locals()[char] = Variable(char)