//Christian Tirella
//Brian Sweeney
//CSU670 Project

import java.util.*;

public class FClause {

	int relationName;				//integer representation of the relation, will later be build into a RelationTable
	ArrayList<FLiteral> literals;	//to be populated with FLiterals
	RelationTable relationTable;	//the relationship defined in terms of a set of possible truth values
	RelationTable candidateRows;	//RelationTable containing only those rows that remain satisfiable

	//Constructors
	public FClause (int relationName) {
		
		this.relationName = relationName;
		this.literals = new ArrayList<FLiteral>();

		if (literals.size() > 3) {
			//fix it
		}
		
		//Build and keep the relationTable for this clause
		this.relationTable = Main.tt.getRelationTable(relationName);
	}
	
	public FClause () {
		this.literals = new ArrayList<FLiteral>();
	}
	
	//get relation name
	public int getRelationName(){
		return relationName;
	}
	
	//is the clause empty?
	public boolean isEmpty(){
		if (this.size() == 0){ return true;}
		else{ return false;}
	}
	
	//print out literals of an FClause
	public void printLits(){
		
		int i;
		System.out.print("( ");
		for(i=0; i<=literals.size()-1; i++){
			
			System.out.print(literals.get(i).toString() + " ");
			
		}
		
		System.out.print(")");
	}

	//get size of clause
	public int size(){
		return literals.size();
	}
	
	//get literal at certain index
	public FLiteral get(int i){
		return this.get(i);
	}
	
	public FClause getLiteral(){
		return this;
	}
	
	//Add FLiterals to new ArrayList
	public void addToArrayList(ArrayList<FLiteral> list){
		int i;
		for(i=0; i<=literals.size()-1; i++){
			FLiteral f = literals.get(i);
			list.add(f);
		}
	}

	//Add FLiterals to the clause
	public void addFLit (FLiteral literal) {
		literals.add(literal);
	}
	
	//Add decision literals to a clause
	public void addDLit (DLiteral literal){
		FLiteral test = literal.toFLiteral();
		literals.add(test);
	}
	
	//Add MLiterals to a clause
	public void addMLit (MLiteral literal){
		FLiteral test = literal.toFLiteral();
		literals.add(test);
	}
	
	//Is the clause satisfied based on the current assignment?
	public boolean isSatisfied () {
		TruthRow currentRow;
		boolean result = false;	//assume false until found true

		relationTable.start();	//reset index in case it was previously traversed
		do {					//check first row for a match
			currentRow = relationTable.getCurrentRow();

			if (literals.size() == 3) {				

				//Get first literal from literals
				FLiteral current0 = this.literals.get(0);
				//Get first truth value from current row
				Integer currentRow0 = currentRow.bitAt(0);

				//Get second literal from literals
				FLiteral current1 = this.literals.get(1);
				//Get second truth value from current row
				Integer currentRow1 = currentRow.bitAt(1);

				//Get third literal from literals
				FLiteral current2 = this.literals.get(2);
				//Get third truth value from current row
				Integer currentRow2 = currentRow.bitAt(2);

				if (current0.matchRT(currentRow0) &&
					current1.matchRT(currentRow1) &&
					current2.matchRT(currentRow2)) {
					result = true;
				}	
			}
			if (literals.size() == 2) {

				//Get first literal from literals
				FLiteral current0 = this.literals.get(0);
				//Get first truth value from current row
				Integer currentRow1 = currentRow.bitAt(1);

				//Get second literal from literals
				FLiteral current1 = this.literals.get(1);
				//Get second truth value from current row
				Integer currentRow2 = currentRow.bitAt(2);				
				if (current0.matchRT(currentRow1) &&
						current1.matchRT(currentRow2)) {
						result = true;
					}
			}
			if (literals.size() == 1) {

				//Get first literal from literals
				FLiteral current0 = this.literals.get(0);

				//Get first truth value from current row
				Integer currentRow3 = currentRow.bitAt(3);
				if (current0.matchRT(currentRow3)) {
						result = true;
				}
			}
			//return whatever the result ended up getting set to
			return result;
		}						//check remaining rows if a match is not found
		while (relationTable.next());
	}
	
	//return an ArrayList of whatever literals could be forced
	public ArrayList forced() {

		this.setCandidateRows();
		ArrayList <ALiteral> result = new ArrayList <ALiteral> (2);

		if (literals.size() == 3) {
			int rTColumnIndex;
			ArrayList rowsToCheck = candidateRows.forcableColumnIndex();
			rTColumnIndex = 0;
			if (literals.get(rTColumnIndex).getValue() == -1 && rowsToCheck.contains(rTColumnIndex)) {
				result.add((FLiteral)literals.get(rTColumnIndex));
			}
			rTColumnIndex = 1;
			if (literals.get(rTColumnIndex).getValue() == -1 && rowsToCheck.contains(rTColumnIndex)) {
				result.add((FLiteral)literals.get(rTColumnIndex));
			}
			rTColumnIndex = 2;
			if (literals.get(rTColumnIndex).getValue() == -1 && rowsToCheck.contains(rTColumnIndex)) {
				result.add((FLiteral)literals.get(rTColumnIndex));
			}		
		}
		if (literals.size() == 2) {
			int rTColumnIndex;
			ArrayList rowsToCheck = candidateRows.forcableColumnIndex();
			rTColumnIndex = 1;
			if (literals.get(rTColumnIndex).getValue() == -1 && rowsToCheck.contains(rTColumnIndex)) {
				result.add((FLiteral)literals.get(rTColumnIndex));
			}
			rTColumnIndex = 2;
			if (literals.get(rTColumnIndex).getValue() == -1 && rowsToCheck.contains(rTColumnIndex)) {
				result.add((FLiteral)literals.get(rTColumnIndex));
			}
		}
		if (literals.size() == 1) {
			int rTColumnIndex;
			ArrayList rowsToCheck = candidateRows.forcableColumnIndex();
			rTColumnIndex = 2;
			if (literals.get(rTColumnIndex).getValue() == -1 && rowsToCheck.contains(rTColumnIndex)) {
				result.add((FLiteral)literals.get(rTColumnIndex));
			}
		}
		return result;
	}

	private void setCandidateRows () {

		TruthRow currentRow;
		Boolean result = false;

		relationTable.start();	//reset index in case it was previously traversed
		do {					//check first row for a match
			currentRow = relationTable.getCurrentRow();

			if (literals.size() == 3) {

				//Get first literal from literals
				FLiteral current0 = this.literals.get(0);
				//Get first truth value from current row
				Integer currentRow0 = currentRow.bitAt(0);
				//Get second literal from literals
				FLiteral current1 = this.literals.get(1);
				//Get second truth value from current row
				Integer currentRow1 = currentRow.bitAt(1);
				//Get third literal from literals
				FLiteral current2 = this.literals.get(2);
				//Get third truth value from current row
				Integer currentRow2 = currentRow.bitAt(2);
								
				if (current0.matchRT(currentRow0) &&
					current1.matchRT(currentRow1) &&
					current2.matchRT(currentRow2)) {
					result = true;
				}	
			}
			if (literals.size() == 2) {
				
				//Get first literal from literals
				FLiteral current0 = this.literals.get(0);
				//Get first truth value from current row
				Integer currentRow1 = currentRow.bitAt(1);
				//Get second literal from literals
				FLiteral current1 = this.literals.get(1);
				//Get second truth value from current row
				Integer currentRow2 = currentRow.bitAt(2);
				
				if (current0.matchRT(currentRow1) &&
						current1.matchRT(currentRow2)) {
						result = true;
					}
			}
			if (literals.size() == 1) {
				
				//Get first literal from literals
				FLiteral current0 = this.literals.get(0);
				//Get first truth value from current row
				Integer currentRow3 = currentRow.bitAt(3);
							
				if (current0.matchRT(currentRow3)) {
						result = true;
				}
			}
			
			//add rows to table
			if (result == true) {candidateRows.add(currentRow);}
			
		}						//check all rows
		while (relationTable.next());
	}
	
	//is this clause contradictory to a give clause
	public boolean contradict(FClause clause) {
		
		int i = 0;
		int j;
		boolean result = false;
			
		for(j=0; j<=clause.size()-1;){
			
			//note:  we do not need to check the rank of the clauses; we will be
			//doing that in the method failState(), so these clauses are going to
			//be of the same rank already; thus, we only need to check the rank of 
			//one of the clauses and not both
			
			FLiteral f1 = this.get(i);
			FLiteral f2 = clause.get(j);
				
			if(f1.equals(f2)){
					
				if(i == this.size()-1){
					//all literals match up; we've reached a contradiction
					result = true;
					System.out.println("Contradiction");
				}
					
				else{
					//check next literals of 1st and 2nd clauses
					i++;
					j++;
				}

			}
				
			else{
					
				if(i == this.size()-1){
					//all literals don't match up, we haven't reached a contradiction
					result = false;
					System.out.println("No Contradiction");
				}
				
				else{
					//check next literal of 2nd clause
					j++;
				}
					
			}
				
		}
		
		return result;
			
	}

}