## NOTE: This will not run without the permpy library installed. See http://permpy.com.

from permpy import *
import itertools
import sympy
import math

donesofar = 0

# Check if two functions are equal by subtracting, simplifying, and comparing to 0
def check_form(thing_to_check, form):
	return sympy.simplify(thing_to_check - form) == 0

# The aim of this function is to verify that for any class C whose SI sequence starts
# 1, 1, 2, 3, there can be no entry in the SI sequence greater than 5 unless there is
# a 5 preceding it. This function verifies it for the maximal classes whose SI sequence
# starts 1, 1, 2, 3.

# For a non-verbose output that only prints the end result, run the command 
#       check_class(Av([]))
# The command will complete in a few minutes with no output indicating that
# no counterexample has been found.
# 
# To run in verbose mode where all maximal classes are displayed along with their
# generating functions, run the command
#       check_class(Av([]), verbose=True)

def check_class(C, start_seq=[0,1,1,2,3], verbose=False):
	global donesofar
	
	# We first calculate the SI sequence of the class	
	si_spec = [len([P for P in C[i] if not P.sum_decomposable()]) for i in range(len(C))]
	
	if verbose:
		print '\nExamining the class Av(',C.basis,').\n\tThe SI sequence is: ',si_spec[1:]
	
	# If the SI sequence appears to have no entries greater than 5 then we probably
	# don't need to keep looking at this class. To verify, we enumerate the class with
	# the insertion encoding and check against known forms.
	if max(si_spec) <= 5:
		donesofar += 1
		
		if verbose:
			print '\tThe SI sequence starts',start_seq[1:],' and appears to have nothing > 5, so we attempt to enumerate.'
	
		I = InsertionScheme(C.basis)
		f = I.gf()
		g = 1-1/f
		g_copy = sympy.simplify(g)
		h = g.series(n=12)
		x = sympy.Symbol('x')

		i = 0
		while True:
			if h.coeff(x,i) < 4 and i < 8:
				g -= h.coeff(x,i)*x**i
				i += 1
			else:
				break
				
		g = sympy.simplify(g)
		
		if verbose:
			print '\t~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~'
			print '\t Completed Class #: ',donesofar
			print '\t\tEnumerated Successfully'
			print '\n\t\tGF: ',g_copy
			print '\n\t\tInitial terms: ',h
			if sympy.denom(g) == 1 or check_form(g, 4*x**5/(1-x)) or check_form(g, x**5*(x**2 - 4)/(x - 1)) or check_form(g, -x**5*(x**2 + 4*x + 4)/(x**2 - 1)) or check_form(g, -2*x**8/(x - 1)):
				print '\n\t\tForm recognized, no 5s present.'
			else:
				print '\n\t\tForm not recognized, should be checked by hand for 5s.'
				print '\t\t\t',g
			print '\t~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~'
		else:
			if not (sympy.denom(g) == 1 or check_form(g, 4*x**5/(1-x)) or check_form(g, x**5*(x**2 - 4)/(x - 1)) or check_form(g, -x**5*(x**2 + 4*x + 4)/(x**2 - 1)) or check_form(g, -2*x**8/(x - 1))):
				print '\t~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~'
				print '\t Class to be checked by hand.'
				print '\t\tAv(',C.basis,')'
				print '\t\tEnumerated Successfully'
				print '\n\t\tGF: ',g_copy
				print '\t\t\t',g
				print '\n\t\tInitial terms: ',h
				print '\t~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~'

	# If there are entries greater than 5 and they don't have a 5 before them, we output
	# as a counterexample. If there are entries greater than 5 and they do have a 5
	# before then, we try to kill the 5 and see if any entries greater than 5 are left.
	else:
		
		# First, if the SI sequence doesn't start 1, 1, 2, 3 then we add basis
		# elements to work toward that.
		for (pos, val) in enumerate(start_seq):
			if pos == len(C) - 1:
				print '\tlength not long enough to complete the computation'
			if si_spec[pos] > val:
				diff = si_spec[pos] - val
				new_class_basis_additions = list(itertools.combinations([P for P in C[pos] if not P.sum_decomposable()], diff))
				
				if verbose:
					print '\tWe need to add',diff,'SI permutations of length',pos,'to the basis.'
				new_classes = []
				for B in new_class_basis_additions:
					new_classes.append(Av(C.basis+list(B), 10))

				for D in new_classes:
					check_class(D, start_seq, verbose)
				return

		# If there is no 5, we're in trouble.
		if 5 not in si_spec:
			print '[!!] A counterexample has been found: Av(',C.basis,') [!!]'

		# If there is a 5, try to turn it into a 4 and see if the elements greater
		# than 5 are still there.
		if 5 in si_spec:
			first_5_pos = min([i for (i,v) in enumerate(si_spec) if v == 5])
			if verbose:
				print '\tThere is a 5 at length',first_5_pos,'that we will try to kill.'
			new_class_basis_additions = [P for P in C[first_5_pos] if not P.sum_decomposable()]
			new_classes = [Av(C.basis+[P]) for P in new_class_basis_additions]
			for D in new_classes:
				check_class(D, start_seq, verbose)