getsolution.py

#!/usr/bin/env python3

import argparse  # requires Python >= 3.2
import re
import sys
import textwrap

if __name__ == "__main__":
    # parsing command line input
    parser = argparse.ArgumentParser(formatter_class=argparse.RawTextHelpFormatter)
    parser.add_argument('file', help='Name of the anf file as generated by getanf.py')
    parser.add_argument('-m', dest='mode', metavar='mode', choices=['mc', 'bgc', 'gc', 'depth'], help="Mode to operate in. One of:\nmc     for multiplicative complexity\nbgc    for bitslice gate complexity\ngc     for gate complexity\ndepth  for depth complexity\nIf omitted, the mode will be based on the filename")
    parser.add_argument('-c', dest='claim', metavar='claim', help=textwrap.fill('Name of the claim file as generated by cnfclaimtoclaim.py. If omitted, <file>.claim.txt will be used', 68))
    args = parser.parse_args()

    if args.mode is None:
        if('_mc' in args.file):
            args.mode = 'mc'
        # currently, gc, bgc and depth mode are all the same
        # distinguish anyway for future flexibility
        elif('_gc' in args.file):
            args.mode = 'gc'
        elif('_bgc' in args.file):
            args.mode = 'bgc'
        elif('_d' in args.file):
            args.mode = 'depth'
        else:
            parser.print_usage(sys.stderr)
            print(sys.argv[0] + ': error: cannot determine mode', file=sys.stderr)
            exit()
    if args.claim is None:
        args.claim = args.file + '.claim.txt'

    # read anf file for equations
    content = []
    with open(args.file, 'rt') as eqs_file:
        for line in eqs_file:
            if line == 'x_0\n':
                break
            if not line.startswith('a_') and not line.startswith('b_'):
                content.append(line)

    # read claim file for value mapping of a's and b's
    valmapab = {}
    with open(args.claim, 'rt') as claim_file:
        for line in claim_file:
            if line.startswith('q_0'):
                break
            val = line.rstrip().split('=')
            valmapab[val[0]] = val[1]

    # substitute variables in equations according to solution found by SAT solver
    valmapq = {}
    output = []
    for line in content:
        # substitute a's and b's
        for val in valmapab:
            if valmapab.get(val) == '1':
                # because otherwise single a's at the start get removed
                line = re.sub(val + r' \+', '1 +', line)  # e.g.: q_0 = a_0 + a_1 * x_0 + ...
                # because otherwise single b's at the end get removed
                line = re.sub(val + r'$', '1', line)  # e.g.: t_0 = b_0 * q_0 * q_1 + b_1 * q_0 + b_1 * q_1 + b_2
                # e.g.: a_0 * x_0 -> x_0
                line = re.sub(val + r'\W+', '', line)
            else:
                # remove e.g.: a_0 * x_0 +
                line = re.sub(val + r'[^0-9][^+]*(\+ |$)', '', line)

        if args.mode == 'mc':
            output.append(line.rstrip(' \n+'))
        # if q's are equal to a single variable, we can substitute them completely
        elif line.startswith('q_'):
            val = line.rstrip(' \n+').split(' = ')
            if len(val) != 2:
                continue
            valmapq[val[0]] = val[1]
        elif line.startswith('t_'):
            # rewrite OR gate
            line = re.sub(r'(q_\d+) \* (q_\d+) \+ q_\d+ \+ q_\d+', r'\1 | \2', line)
            # add parenthesis for clarity on operator precedence for NAND/NOR gate
            line = re.sub(r'(q_\d+ [*|] q_\d+) \+ 1$', r'(\1) + 1', line)
            # substitute q's
            for val in valmapq:
                line = re.sub(val + r'\b', valmapq.get(val), line)
            output.append(line.rstrip(' \n+'))
        elif line.startswith('y_'):
            val = line.rstrip(' \n+').split(' = ')
            # substitute t's that correspond to a y
            for i in range(len(output)):
                output[i] = re.sub(val[1], val[0], output[i])

    print('\n'.join(output))