/*
 * CSP Project
 * Authors:
 * 		Jay Bernardo
 * 		Matt Rancourt
 * 
 * File: Relation.java
 * 
 * Contains the Relation class. 
 * A relation is essentially just a number representing
 * the truth table satisfaction given some number of variables
 * as input.
 * 
 * TODO: 
 * 
 * -Update description to include facilitation of variable 
 *  assignment and relation reduction once implemented
 * 
 * - Store relation number as binary upon instantiation? 
 */
import java.util.ArrayList;
import java.util.Iterator;

class Relation{
	int relationNumber;
	int rank;
	Variable variables[];
	
	/**
	 * Constructor for a relation
	 * 
	 * @param relationNumber - the number of the given relation
	 * @param rank - the rank of the relation (1, 2, or 3)
	 * @param variableNamesIn - names of the variables
	 */
	public Relation(int relationNumber, int rank, String variableNamesIn[]) 
	throws 
		RelationNumberOutOfBoundsException,
		RankOutOfBoundsException,
		InvalidVariableNamesLengthException,
		InvalidVariableValueException{
				
		// Set the relationNumber and make sure it's 
		// within reasonable boundaries
		this.relationNumber = relationNumber;
		if(this.relationNumber < 0 || this.relationNumber > 255)
		{
			throw new RelationNumberOutOfBoundsException();
		}
		
		// Set the rank. Since we know the relation number,
		// we can determine if we're asking for a rank
		// that is out of bounds in addition to constraining
		// our rank to between 1 and 3 (inclusive)
		this.rank = rank;
		if(this.rank < 1 || this.rank > 3 ||
		   (this.rank == 1 && rank > 3) ||
		   (this.rank == 2 && rank > 15))
		{
			throw new RankOutOfBoundsException();
		}
		
		// Make a clone of the strings that were passed in
		// so we don't modify their contents unintentionally
		String  variableNames[] = variableNamesIn.clone();
		
		// Make sure the length of the passed in
		// variableNames is the of the same size
		// as rank
		if(variableNames.length != this.rank)
		{
			throw new InvalidVariableNamesLengthException();
		}
		
		// If we've reached this point we know we can safely copy the 
		// variable names
		this.variables = new Variable[rank];
		
		int i = 0;
		for(i = 0; i < variableNames.length; i ++){
			boolean positive = true;
			if(variableNames[i].charAt(0) == '!'){
				variableNames[i] = new String(variableNames[i].substring(1));
				positive = false;
			}
			
			this.variables[i] = new Variable(variableNames[i], -1, positive);
		}
	}
	
	/**
	 * Sets the variable varName to the given value,
	 * if it exists in the relation
	 * @param varName - name of variable to set value for
	 * @param value - value to assign to the given variable
	 */
	public void setVariable(String varName, int value)
	throws
		InvalidVariableValueException{
		int i = 0;
		for(; i < rank; i ++){
			if(variables[i].getName().equals(varName)){
				variables[i].setValue(value);
			}
		}
	}
	
	/**
	 * Sets the relation number of this relation
	 * @param n - new relation number
	 */
	public void setRelationNumber(int n){
		relationNumber = n;
	}
	
	/**
	 * Returns the relationNumber of this relation
	 * @return relation number as an int
	 */
	public int getRelationNumber(){
		return relationNumber;
	}
	
	/**
	 * Returns the name of the first variable which is unassigned
	 * @return names of first unassigned variable or
	 * 		   null if all variables are assigned
	 */
	public String findUnassignedVariableName(){
		int i = 0;
		for(; i < variables.length; i ++){
			if(variables[i].getValue() == -1){
				return variables[i].getName();
			}
		}
		
		return null;
	}
	
	/**
	 * Returns a duplicate of "this" Relation
	 * @return a copy of the relation "this"
	 * @throws RelationNumberOutOfBoundsException
	 * @throws RankOutOfBoundsException
	 * @throws InvalidVariableNamesLengthException
	 */
	public Relation duplicate()
	throws
		RelationNumberOutOfBoundsException,
		RankOutOfBoundsException,
		InvalidVariableNamesLengthException,
		InvalidVariableValueException
		{
		// Grab all the names from the variables
		// in this relation
		String names[] = new String[variables.length];
		int i = 0;
		for(; i < variables.length; i ++){
			names[i] = variables[i].getName();
			
			// If it's a Negative variable we want to make sure to
			// put the ! back in to the string, so that when we 
			// create the new relation with the list the assignments
			// will be set properly after parsing
			if(variables[i].getPositive() == false){
				names[i] = String.format("!%s", names[i]);
			}
		}
		
		// Create a new relation of the same rank, number, with the 
		// given variable names
		Relation newRelation = new Relation(relationNumber, rank, names);
		
		// Set the values to all the values within this
		// relation. Remember, getValue flips the value if
		// the variable is a neg -- but we don't want the value
		// flipped! We want to copy that value explicitly
		for(i = 0; i < variables.length; i ++){
			Variable v = newRelation.variables[i];
			int value = 0;
			if(v.getPositive() == false){
				int retValue = v.getValue();
				
				if(retValue == 0){
					value = 1;
				}
				else if(retValue == 1){
					value = 0;
				}
			}
			else{
				value = v.getValue();
			}
			
			newRelation.variables[i].setValue(value);
			
		}
		
		return newRelation;
	}
	
	/**
	 * Reduces this Relation according to which
	 * variables have set values.
	 * @return - reduced Relation
	 */
	public Relation reduce()
	throws
		RelationNumberOutOfBoundsException,
		RankOutOfBoundsException,
		InvalidVariableNamesLengthException,
		InvalidVariableValueException{
		
		// Depending on arity we have a set truth table to
		// look at and a given number of rows to query
		// from that table.
		int checkArity[][] = null;
		int rows = 0;
	
		switch(rank){
		case 1:
			checkArity = TruthTable.arity1;
			rows = 2;
			break;
		case 2:
			checkArity = TruthTable.arity2;
			rows = 4;
			break;
		case 3:
			checkArity = TruthTable.arity3;
			rows = 8;
			break;
		}
		
		ArrayList<Integer> setVariablePositions = new ArrayList<Integer>();
		ArrayList<Integer> unsetVariablePositions = new ArrayList<Integer>();
		int i = 0;
		
		// Determine which variables are set, so
		// we can reduce them out
		for(; i < rank; i ++){
			if(variables[i].getValue() != -1)
			{
				setVariablePositions.add(new Integer(i));
			}
			else{
				unsetVariablePositions.add(new Integer(i));
			}
		}
		
		// We know our new rank now, and we also need to know
		// how many rows are in our new relation
		int newRank = rank - setVariablePositions.size();
		int newRowSize = -1;
		switch(newRank){
		case 1:
			newRowSize = 2;
			break;
		case 2:
			newRowSize = 4;
			break;
		case 3:
			newRowSize = 8;
			break;
		default:
			return this;
		}
		
		// We will determine which rows we will use to construct
		// the new relation number in the new relation
		ArrayList<Integer>useRows = new ArrayList<Integer>();
		
		for(i = 0; i < rows; i ++){
			boolean allEqual = true;
			Iterator<Integer> it = setVariablePositions.iterator();
			while(it.hasNext()){
				int position = it.next().intValue();
				if(variables[position].getValue() != checkArity[i][position]){
					allEqual = false;
					break;
				}
			}
			
			if(allEqual == true){
				useRows.add(new Integer(i));
			}
		}
		
	
		// Given the rows that we care about, we need to
		// construct the bit string that will represent the
		// rank of our new relation
		int newBitString[] = new int[newRowSize];
		
		Iterator<Integer>it = useRows.iterator();
		int j = 0;
		int truth[] = Relation.convertRelationNumberToBinary(relationNumber, rank);
		while(it.hasNext()){
			int row = it.next().intValue();
			newBitString[j] = truth[row];
			j++;
		}
		
		// Calculate the integer value of the new bit string
		int newRelationNumber = Relation.convertRelationNumberFromBinary(newBitString);
		
		// Now we need to grab the variable names of the variables
		// that are left over and whether they are positive or negative
		String newVariableNames[] = new String[newRank];
		Iterator<Integer> it2 = unsetVariablePositions.iterator();
		int k = 0;
		while(it2.hasNext()){
			int value = it2.next().intValue();
			Variable variable = variables[value];
			newVariableNames[k] = new String(variable.getName());
			
			if(variable.getPositive() == false){
				newVariableNames[k] = String.format("!%s", newVariableNames[k]);
			}
			k ++;
		}
		
		// Now we can build the new relation with this information
		return new Relation(newRelationNumber, newRank, newVariableNames);
	}
	
	/**
	 * Prints out the relation in a pretty format
	 */
	public void print(){
		System.out.printf("R%03d( ", relationNumber);
		
		// Print all the items, skipping spacing on the last one
		int i = 0;
		for(; i < rank; i ++){
			variables[i].print();
			
			if(i != rank-1){
				System.out.print(" ");
			}
		}
		
		System.out.print(" )");		
	}
	
	/**
	 * Returns the rank of the Relation
	 * @return rank of relation as integer
	 */
	public int getRank(){
		return rank;
	}
	
	/**
	 * Returns whether the relation is deemed unsatisfied or not--that is
	 * it is in the unsatisfiable state given the variable assignments
	 * 
	 * @return true if all variables are set, but the relation is unsatisfied with the given assignment
	 *         false otherwise
	 */
	public boolean isUnsatisfied(){
		int i = 0;
		for(; i < rank; i ++){
			if(variables[i].getValue() == -1){
				return false;
			}
		}
		
		return !isSatisfied();
	}
	
	/**
	 * Returns whether the relation is satisfied when all the 
	 * given variables are assigned.
	 * 
	 * NOTE: When this function returns false it does *NOT* mean
	 *       that the relation is in the "unsatisfied" state.
	 *       
	 *       See: isUnastisfied
	 *       
	 * @return true if satisfied
	 *         false otherwise
	 */
	public boolean isSatisfied(){
		int truth[] = convertRelationNumberToBinary(relationNumber, rank);
				
		// Depending on arity we have a set truth table to
		// look at and a given number of rows to query
		// from that table.
		int checkArity[][] = null;
		int rows = 0;
	
		switch(rank){
		case 1:
			checkArity = TruthTable.arity1;
			rows = 2;
			break;
		case 2:
			checkArity = TruthTable.arity2;
			rows = 4;
			break;
		case 3:
			checkArity = TruthTable.arity3;
			rows = 8;
			break;
		}
		
		// Do incremental checking to see if all of the variables
		// for the given arity are equivalent, then we can look
		// up the truth value from the binary representation
		// of the relation number. We tier the checking in this
		// way because we want to check for all arity types
		// without the use of three different functions (DRY principle)
		int row = 0;
		for(row = 0; row < rows; row ++){
			if(checkArity[row][0] == variables[0].getValue()){
				//System.out.println("Here1");
				if(rank == 1){
					if(truth[row] == 1)
						return true;
					else
						return false;
				}
				else if(checkArity[row][1] == variables[1].getValue()){
					//System.out.println("Here2");
					if(rank == 2){
						if(truth[row] == 1)
							return true;
						else
							return false;
					}
					else if(checkArity[row][2] == variables[2].getValue()){
						//System.out.println("Here3");
						if(truth[row] == 1)
							return true;
						else
							return false;
					}
				}
			}
		}
		
		return false;
	} 
	
	/**
	 * Translates this relation from rank 1, 2, or 3, into a rank three relation
	 * by simply copying the bistring representation into the "lower" portions
	 * of the higher order truth table
	 * 
	 * @return - Translated relation
	 */
	public Relation translateToRankThree()
	throws
		RelationNumberOutOfBoundsException,
		RankOutOfBoundsException,
		InvalidVariableNamesLengthException,
		InvalidVariableValueException
	{
		if(this.rank == 3){
			return this.duplicate();
		}
		
		// First we need to duplicate the rank number into
		// binary and of length rank 3
		int asBinary[] = Relation.convertRelationNumberToBinary(relationNumber, rank);
		
		// Default to 8, because we are rank 3
		int newBitString[] = new int[8];
		
		if(rank == 1){
			newBitString[0] = asBinary[0];
			newBitString[1] = asBinary[1];
			newBitString[2] = asBinary[0];
			newBitString[3] = asBinary[1];
		}
		else if(rank == 2){
			newBitString[0] = asBinary[0];
			newBitString[1] = asBinary[1];
			newBitString[2] = asBinary[2];
			newBitString[3] = asBinary[3];
		}
		
		// Copy this over once again from 0-3 to 4-7
		newBitString[4] = newBitString[0];
		newBitString[5] = newBitString[1];
		newBitString[6] = newBitString[2];
		newBitString[7] = newBitString[3];
		
		int newRelationNumber = Relation.convertRelationNumberFromBinary(newBitString);
		
		// Now we need to create the variable names
		String variableNames[] = new String[3];
		
		Variable useVariable = null;
		if(rank == 1){
			useVariable = variables[0];
		}
		else{
			useVariable = variables[1];
		}
		
		// We always copy the first variable into the last position
		// of the rank 3
		if(useVariable.getPositive() == false){
			variableNames[2] = String.format("!%s", useVariable.getName());
		}
		else{
			variableNames[2] = new String(useVariable.getName());
		}
		
		if(rank == 2){
			Variable useVariableTwo = variables[0];
			if(useVariableTwo.getPositive() == false){
				variableNames[1] = String.format("!%s", useVariableTwo.getName());
			}
			else{
				variableNames[1] = new String(useVariableTwo.getName());
			}
		}
		else{
			variableNames[1] = String.format("%s%s", useVariable.getName(), useVariable.getName());
		}
		
		String firstVariable = useVariable.getName();
		variableNames[0] = String.format("%s%s%s", firstVariable, firstVariable, firstVariable);
		
		return new Relation(newRelationNumber, 3, variableNames);
	}
	
	/**
	 * Class method to determine if a variable in a given position
	 * of a relation of relationNumber of rank is forced to
	 * some value or not
	 * @param relationNumber
	 * @param rank
	 * @param position
	 * @return -1 if not forced
	 *         0 if forced to 0
	 *         1 if forced to 1
	 * @throws RankOutOfBoundsException
	 * @throws VariablePositionOutOfBoundsException
	 */
	public static int forced(int relationNumber, int rank, int position)
	throws
		RankOutOfBoundsException,
		VariablePositionOutOfBoundsException{
		
		// Do some generic bounds checking
		if(rank < 0 || rank > 3){
			throw new RankOutOfBoundsException();
		}
		
		// Decrement position because the user is using start index 1,
		// but with arrays we use start index 0
		position --;
		
		// TODO: This still allows for a relation to be
		// specified and a position within that relation to
		// be asked for which does not exist
		if(position > 0 && rank == 1 ||
		   position > 1 && rank == 2 ||
		   position < 0 ||
		   position > 2){
					throw new VariablePositionOutOfBoundsException();
		}
		
		int rows = 0;
		int arity[][] = null;
		switch(rank){
		case 1:
			rows = 2;
			arity = TruthTable.arity1;
			break;
		case 2:
			rows = 4;
			arity = TruthTable.arity2;
			break;
		case 3:
			rows = 8;
			arity = TruthTable.arity3;
			break;
		}
		
		int relationInBinary[] = Relation.convertRelationNumberToBinary(relationNumber, rank);
		
		// Determine which rows we care about
		ArrayList<Integer> rowsToCheck = new ArrayList<Integer>();
		int i = 0;
		for(; i < rows; i ++){
			if(relationInBinary[i] == 1){
				rowsToCheck.add(new Integer(i));
			}
		}
		
		// If there are no rows that are 1, then
		// we must be relation 0. Nothing is forced. Wooha!
		if(rowsToCheck.size() == 0){
			return -1;
		}
		
		// Do all of the variables in position "position" equal the same value
		// wherever the relation is satisfied? If so, then the variable is forced
		boolean allMatch = true;
		Iterator<Integer> iter = rowsToCheck.iterator();
		
		int first = 0;
		int toMatch = 0;
		
		if(iter.hasNext()){
			first = iter.next().intValue();
			toMatch = arity[first][position];
		}
		
		while(iter.hasNext()){
			int thisOne = iter.next().intValue();
			int matcher = arity[thisOne][position];
			if(toMatch != matcher){
				allMatch = false;
			}
		}
		
		if(allMatch)
			return toMatch;
		
		return -1;
	}
	
	/**
	 * Converts the given integer relationNumber into an array
	 * containing the bits of the relationNumber as represented
	 * in binary format
	 * @param relationNumber - number of the relation to convert
	 * @param rank - rank of the relation
	 * @return - binary representation of the truth values given by relationNumber
	 */
	public static int[] convertRelationNumberToBinary(int relationNumber, int rank){
		int size = 0;
		switch(rank){
		case 1:
			size = 2;
			break;
		case 2:
			size = 4;
			break;
		case 3:
			size = 8;
			break;
		}
		
		int retVal[] = new int[size];
		int i = 0;
		for(; i < retVal.length; i ++){
			retVal[i] = 0;
		}
		
		String asBinaryString = String.format("%s", Integer.toBinaryString(relationNumber));
		
		int j = asBinaryString.length()-1;
		for(i = 0; i < asBinaryString.length(); i ++){
			retVal[i] = Integer.valueOf(String.format("%c", asBinaryString.charAt(j)));
			j --;
		}
		
		return retVal;
	}
	
	/**
	 * Utility method of Relation that converts a relation number from a binary []
	 * representation to its decimal integer representation
	 * @param binary - array of bits
	 * @return integer representation of the bitstring "binary"
	 */
	public static int convertRelationNumberFromBinary(int [] binary){
		//Now calculate the integer value of the bitstring
		// This is the new relationNumber
		int i = 0;
		int newRelationNumber = 0;
		for(; i < binary.length; i ++){
			int test = binary[i];
			if(test == 1)
			{
				newRelationNumber += Math.pow(2, i);
			}
		}		
		return newRelationNumber;
	}
	
	/**
	 * Preprocesses the relation to contain no negative
	 * variables
	 * 
	 * NOTE: ASSUMES RANK IS 3
	 * 
	 * @return - the preprocessed relation
	 * @throws RelationNumberOutOfBoundsException
	 * @throws RankOutOfBoundsException
	 * @throws InvalidVariableNamesLengthException
	 * @throws InvalidVariableValueException
	 */
	public Relation preprocess()
	throws
	RelationNumberOutOfBoundsException,
	RankOutOfBoundsException,
	InvalidVariableNamesLengthException,
	InvalidVariableValueException{
		
		// Grab this relation
		Relation r = this;
		
		// We need to know how many variables we're going to set
		// to positive from negative when we're done
		int numVarsToSet = 0;
		if(r.rank < 3){
			numVarsToSet = 3 - r.rank;
			r = r.translateToRankThree();
		}
		
		// We will ALWAYS have three variables
		int j = 0;
		for(; j < 3; j ++){
			if(r.variables[j].getPositive() == false){		
				int bitString[] = Relation.convertRelationNumberToBinary(r.relationNumber, 3);
					
				// Depending on our position, we change the bitstring accordingly
				// With first variable set, we need to swap the top four bits
				// with the bottom four bits
				if(j == 0){
					int tmp[] = new int[4];
					tmp[0] = bitString[4];
					tmp[1] = bitString[5];
					tmp[2] = bitString[6];
					tmp[3] = bitString[7];
					bitString[4] = bitString[0];
					bitString[5] = bitString[1];
					bitString[6] = bitString[2];
					bitString[7] = bitString[3];
					bitString[0] = tmp[0];
					bitString[1] = tmp[1];
					bitString[2] = tmp[2];
					bitString[3] = tmp[3];
				}
				// If we're looking at position 1, then we swap in steps
				// of two, for the top half and the bottom half
				else if(j == 1){
					int tmp[] = new int[8];
					tmp[0] = bitString[2];
					tmp[1] = bitString[3];
					tmp[2] = bitString[0];
					tmp[3] = bitString[1];
					tmp[4] = bitString[6];
					tmp[5] = bitString[7];
					tmp[6] = bitString[4];
					tmp[7] = bitString[5];
					bitString = tmp;
					
				}
				// Swap every bit with its neighbor in groups of 2
				else if(j == 2){
					int z = 0;
					for(; z< bitString.length-1; z += 2){
						int tmp = bitString[z+1];
						bitString[z+1] = bitString[z];
						bitString[z] = tmp;
					}
				}
					
				// Create the new relation
				int newRelationNumber = Relation.convertRelationNumberFromBinary(bitString);
				r.setRelationNumber(newRelationNumber);
				
				// Set the variable to positive from negative
				r.variables[j].setPositive(true);
			}
		}
		
		// Now we need to set the variables that "don't matter"
		// from upreducing so that we can reduce and get back the
		// new, reduced form of the preprocessed relation
		for(j = 0; j < numVarsToSet; j ++){
			r.setVariable(r.variables[j].getName(), 1);
		}
		
		return r.reduce();
	}
}