import re
from sets import Set

max_len = 171
usable_str = 'plaidctf'
begin_str = '^(.*[^plaidctf].*|.{,170}|.{172,}|'
pass_str = ''
end_str = ')$'

solv_dict = {'p':0, 'l':1,'a':2,'i':3,'d':4,'c':5,'t':6,'f':7}

#Setup plaidctf array
pos_strs = []
for i in range(max_len):
   const_dict = {'p':set(), 'l':set(),'a':set(),'i':set(),'d':set(),'c':set(),'t':set(),'f':set()}
   pos_strs.append(const_dict)


#Open the file
f = open( 'regex_bak.txt' , 'r' )
data = f.read()
split_reg = data.split("|");

o = open( 'out2.txt' , 'w')

#Set the str to 171 chars of a
pass_str = 'a' * 171
curr_reg = begin_str
print "Total regexs: " + str(len(split_reg))
for i in range(3, len(split_reg)):
	cur_pos = 0
	period_count = 0
	char_idx = 0
   #Get the current reg to add
	next_reg = split_reg[i]
	#print "Next reg to pass" + next_reg
	obj_list = []
	out_str = "solver.add( Or( "
	while cur_pos < len(next_reg):
		next_char = next_reg[cur_pos]
		if next_char == ".":
			period_count += 1
			cur_pos += 1
			continue
		elif next_char == "{":
			end_pos = next_reg.find("}", cur_pos ) 
			skip = int(next_reg[cur_pos+1:end_pos])  
			cur_pos = end_pos + 1
		elif next_char == "[":
			end_pos = next_reg.find("]", cur_pos )   
			chars = next_reg[cur_pos+1:end_pos] 
			cur_pos = end_pos + 1

			#print "Chars: " + chars
			#Set the skip count
			if skip == None:
				skip = period_count

			#print "Skip: " + str(skip)
			char_idx += skip
			out_str += "And( " 
			for i in range(len(chars)):
				the_char = chars[i]
				out_str += "c" + str(char_idx) + " != " + str(solv_dict[the_char]) + ", "		
			                   
			#Add or
			out_str = out_str[:-2]
			out_str += "), ";
									
			#print "String at " + str(char_idx) + ": " + pos_strs[char_idx]
			#Set skip to None
			char_idx += 1
			skip = None
			period_count = 0

		elif next_char == ")":
			break

	#Remove the last or
	out_str = out_str[:-2]
	out_str += "))"  
	print out_str   
	o.write( out_str + "\n")

	#Reset None
	if skip != None:
		char_idx += skip
		skip = None

	#print "End index: " + str(char_idx) + "\n"
 
o.close()
f.close()