#!/usr/bin/env python
# coding: utf-8

import itertools as it
import sys 
from pysat.formula import CNF

def my_mod(k,n):
    # modulo function but uses 1...n instead of 0...n-1. We need this because Sat solvers number the variables starting with 1.  
    if k%n==0:
        return n
    else:
        return k%n

def perm_from(perm,start,n):
    #Calculates k-gon in an n-gon based on a starting position and the permutation of the sides.
    return list(it.accumulate(perm[:-1],lambda x,y: my_mod(x+y,n),initial=start))
   

def make_formula(k,file_name):
    # Generate formula for 2**k-1 gon, with distances 1,2,...,2**(k-1) then writes to file
 
    n=2**k-1
    
    formula=CNF()
    #Calulate side lengths
    nums=[2**i for i in range(k)]
    print(nums)
    
    #for all starting position take all permutations starting with 1.
    for k in range(1,n+1):
        for permutation in it.permutations(nums[1:]):
            
            perm=list(permutation)
            perm.insert(0,1)
           
            pos=perm_from(perm,k,n)
            neg=[-x for x in perm_from(perm,k,n)]
                    
            formula.append(neg)
            formula.append(pos)
            
    formula.to_file(file_name)  # writing to a file


    
if __name__ == "__main__":
    # expects two arguments, k and output file name
    make_formula(int(sys.argv[1]),sys.argv[2])