#!/usr/bin/env python3

import operator, functools, math, sys
import SAT_lib, my_utils

"""
rows with dots are partial products:

     aaaa
b ___....
b __...._
b _....__
b ....___

width = OUTPUT_SIZE (INPUT_SIZE*2-1)
height = INPUT_SIZE

"""

def factor(poly):
    #print ("factor 0x%x" % poly)
    s=SAT_lib.SAT_lib(verbose=0)
    INPUT_SIZE=size=my_utils.ceil_binlog(poly)
    OUTPUT_SIZE=INPUT_SIZE*2-1

    a=s.alloc_BV(INPUT_SIZE)
    b=s.alloc_BV(INPUT_SIZE)
    partial_products=[s.alloc_BV(OUTPUT_SIZE) for _ in range(INPUT_SIZE)]
    product=s.alloc_BV(OUTPUT_SIZE)

    s.fix_BV(product, SAT_lib.n_to_BV(poly, OUTPUT_SIZE))

    for i in range(INPUT_SIZE):
        t=s.shift_left(s.BV_zero_extend(a, OUTPUT_SIZE), i)

        # we index b[] array other way round here:
        b_idx=INPUT_SIZE-i-1
        mask = [b[b_idx]] * OUTPUT_SIZE
        s.fix_BV_EQ(partial_products[b_idx], s.BV_AND(t, mask))

    # FIXME: this is slow! due to BV_XOR
    s.fix_BV_EQ(functools.reduce (s.BV_XOR, partial_products), product)

    # but this is WAY SLOWER:
    """
    for col in range(OUTPUT_SIZE):
        tmp=[partial_products[row][col] for row in range(INPUT_SIZE)]
        s.fix_EQ(s.XOR_list(tmp), product[col])
    """

    # outputs must not be 1
    s.fix_BV_NEQ(a, s.n_to_BV(1, INPUT_SIZE))
    s.fix_BV_NEQ(b, s.n_to_BV(1, INPUT_SIZE))

    #print ("going to run s.solve()")
    if s.solve():
        a_n=s.get_val_from_solution(a)
        b_n=s.get_val_from_solution(b)
        #print ("a_n, b_n = 0x%x, 0x%x" % (a_n, b_n))
        # factor results recursively:
        factor(a_n)
        factor(b_n)
    else:
        print ("prime factor: 0x%x or %s" % (poly, my_utils.poly_to_str(poly)))

poly=int(sys.argv[1], 16)
    
print ("starting. poly=0x%x or %s" % (poly, my_utils.poly_to_str(poly)))
factor(poly)