7 segment decoder with minimal nor gates

segsat.py

from z3 import *

def build_gate(nodes, edges):
    assert len(nodes) == len(edges)
    subs = [And(node, edge) for node, edge in zip(nodes, edges)]
    return Not(Or(subs))

def build_circuit(inputs, edgemap, sels):
    nodes = list(inputs)
    for edges in edgemap:
        new_node = build_gate(nodes, edges)
        nodes.append(new_node)

    outs = list()
    for sel in sels:
        out = nodes[len(inputs)]
        for i in range(1, len(sel)):
            out = If(sel[i], nodes[len(inputs)+i], out)
        outs.append(out)

    return outs

def print_dot(num_in, num_out, num_gates, model):
    print('digraph D {')
    for i in model:
        #print(i, type(i), model[i], type(model[i]), bool(model[i]))
        if not model[i]:
            continue
        estr = str(i).split('_')
        if estr[0] == 'e':
            print('{}{} -> g{}'.format('i' if int(estr[2]) < num_in else 'g',
                estr[2] if int(estr[2]) < num_in else int(estr[2]) - num_in, estr[1]))
        elif estr[0] == 's':
            print('g{} -> o{}'.format(estr[2], estr[1]))
        else:
            assert False
    print('}')

def main():
    num_gates = 13
    num_in = 4
    num_out = 7
    expected = {'0000':'1111110', '0001':'0110000',
                '0010':'1101101', '0011':'1111001',
                '0100':'0110011', '0101':'1011011',
                '0110':'1011111', '0111':'1110000',
                '1000':'1111111', '1001':'1110111'}

    opt = Solver()
    #opt = Optimize()

    edgemap = list()
    for i in range(num_gates):
        edges = [Bool('e_{}_{}'.format(i, j)) for j in range(num_in + i)]
        # edge constrain
        edgemap.append(edges)
    sels = list()
    assert num_gates >= 2
    for i in range(num_out):
        sel = [Bool('s_{}_{}'.format(i, j)) for j in range(num_gates)]
        sels.append(sel)
        opt.add(PbEq([(x,1) for x in sel], 1))

    for istr, ostr in expected.items():
        assert len(istr) == num_in and len(ostr) == num_out
        inputs = [x != '0' for x in istr]
        outs = build_circuit(inputs, edgemap, sels)
        for x, y in zip(outs, ostr):
            assert y in '01x'
            if y != 'x':
                opt.add(x == (y == '1'))
    #opt.minimize(Sum([If(edge, 1, 0) for sublist in edgemap for edge in sublist]))

    if opt.check() == sat:
        print(opt.model())
        print_dot(num_in, num_out, num_gates, opt.model())
    else:
        print('unsat')

if __name__ == '__main__':
    main()