#!/usr/bin/python
# -*- coding: utf-8 -*
"""Derive optimal functions to compute elementary Boolean functions from abj.

This program represents the truth tables of two-input Boolean
functions of inputs called X and Y as binary numbers in big-endian
form, using the encoding demonstrated in the table below.

    |                        | X | Y | F | X abj Y | X OR Y | X NAND Y |  T |
    |                        | 0 | 0 | 0 |       0 |      0 |        1 |  1 |
    |                        | 0 | 1 | 0 |       0 |      1 |        1 |  1 |
    |                        | 1 | 0 | 0 |       1 |      1 |        1 |  1 |
    |                        | 1 | 1 | 0 |       0 |      1 |        0 |  1 |
    |------------------------+---+---+---+---------+--------+----------+----|
    | binary value of column | 3 | 5 | 0 |       2 |      7 |       14 | 15 |

Because abj is falsehood-preserving, the program doesn’t succeed in
generating all possible Boolean truth tables using abj when it’s not
given a “source of truth”, an input that is always true.  More
surprising, it doesn’t even succeed in generating OR or XOR.  Unless
it’s buggy, that means that it’s impossible to compute OR or XOR in
abjunction logic without using an external source of power.  Given the
OR of the inputs, it can compute XOR using abjunction, but not vice
versa.

"""

def main():
    for base in [{3: 'X', 5: 'Y'},
                 {3: 'X', 5: 'Y', 7: 'X OR Y'},
                 {3: 'X', 5: 'Y', 6: 'X XOR Y'},
                 {3: 'X', 5: 'Y', 15: 'T'},
                 {0: 'F', 3: 'X', 5: 'Y', 15: 'T'}]:
        print "from basis", base
        for gate, weight in [(abj, weight_by_gates),
                             (abj, weight_by_depth),
                             (nand, weight_by_gates)]:
            print gate.func_name, weight.func_name, derive(gate, weight, base)

def derive(gate, weight, base):
    circuits = base.copy()
    updating = True
    while updating:
        updating = False
        inputs = list(circuits.keys())
        for a in inputs:
            for b in inputs:
                c = gate(a, b)
                circuit = circuits[a], circuits[b]
                if c not in circuits or weight(circuit) < weight(circuits[c]):
                    circuits[c] = circuit
                    updating = True
    return circuits

def abj(a, b):
    return (a & ~b) & 15

def nand(a, b):
    return ~(a & b) & 15

def weight_by_gates(circuit):
    def inner(circuit, already_counted):
        if circuit in already_counted:
            return 0, already_counted
        elif type(circuit) is tuple:
            a, b = circuit
            wa, already_counted = inner(a, already_counted)
            wb, already_counted = inner(b, already_counted)
            return 1 + wa + wb, already_counted
        else:
            return 0, already_counted

    return inner(circuit, set())

def weight_by_depth(circuit):
    if type(circuit) is tuple:
        a, b = circuit
        return 1 + max(weight_by_depth(a), weight_by_depth(b))
    else:
        return 0

if __name__ == '__main__':
    main()