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

import java.util.ArrayList;

public class Formula {
	
	private ArrayList<ALiteral> M;  //literals
	private FCSP F;  //CSP
	
	public Formula(){
		this.M = new ArrayList<ALiteral>();
		this.F = new FCSP();
	}
	
	//are there any decision literals in M? (need this for FailState rule)
	public boolean dLitsInM(){
		
		int i;
		boolean result = false;
		
		for(i=0; i<=M.size()-1; i++){
			
			if(M.get(i).getClass().toString().equals("class DLiteral")){
				result = true;
				i = M.size();
			}
			
			else{/*do nothing, check the next literal of M until none are left*/}
			
		}
		
		return result;
		
	}
	
	//get M
	public ArrayList<ALiteral> getM(){
		
		int i;
		ArrayList<ALiteral> mlist = new ArrayList<ALiteral>();
		
		for(i=0; i<=M.size()-1; i++){
			ALiteral m = M.get(i);
			mlist.add(m);
		}

		mlist.trimToSize();
		this.printM();
		return mlist;
	}
	
	//get F
	public FCSP getF(){
		
		int i;
		FCSP flist = new FCSP();
		
		for(i=0; i<=F.size()-1; i++){
			FClause f = F.get(i);
			flist.addClause(f);
		}

		this.printF();
		return flist;

	}
	
	//print out M literals
	public void printM(){
		
		int i;
		
		//if M is empty, print out "{ }"
		if(this.M.isEmpty()){
			System.out.print("{ }");
		}
		
		else{
			for(i=0; i<=M.size()-1; i++){
			String mLit = M.get(i).toString();
			System.out.print(mLit + " ");
			}
		}
	}
	
	//print out formula clauses
	public void printF(){
		
		int i;
		
		for(i=0; i<=F.size()-1; i++){
			System.out.print(F.get(i).getRelationName());
			F.get(i).printLits();
			System.out.print(" ");
		}
		System.out.println();
		System.out.println();
	}
	
	//print out formula
	public void printFormula(){
		this.printM();
		System.out.print("|| ");
		this.printF();
	}
	
	//add literal to M
	public void addToM(ALiteral literal){
		if(M.isEmpty()){
			System.out.println();
			this.M.add(literal);
			}
		
		else{
			
			int i;
			
			for(i=0; i<=M.size()-1; ){
				if(M.get(i).name == literal.name){
					
					System.out.println("Error:  Literal " + M.get(i).name + " has been previously added to M.");
					i = M.size();
					System.out.println();
				
				}
				
				else{
					/*if at end of list and no matches*/
					if(i == M.size()-1){
						//add literal
						this.M.add(literal);
						i = M.size();
					}
					else{i++;}
					
				}
				
			}
			
		}
		
	}
	
	//add an FCSP to F
	public void addToF(FCSP fcsp){
		this.F = fcsp;
	}
	
	//add a clause to F
	public void addClause(FClause clause){
		this.F.addClause(clause);
	}

	
	//UnitPropagate
	public boolean unitPropagate() {
		boolean success;
		//apply forced
		F.cspForced();
		//apply isSatisified
		success = F.cspSatisfied();
		//return result
		return success;
	}
	
	//Decide
	/*
	 * make up simple decide method to be switched out later on by coin-flipping
	 */
	public void decide(){

		//go through the CSP and decide on a literal; make it into a decision literal
		//1. add a DLiteral to M
		//2. set the values in the FClause after deciding (check to see if negated)
		int i;
		ArrayList<FLiteral> templist = new ArrayList<FLiteral>();
		
		//gather all FLiterals from every FClause into temporary lists containing only
		//that literal; we will decide on the literal that occurs least frequently
		
		FCSP fcsp = this.getF();
		System.out.println(fcsp);
		
		for(i=0; i<=fcsp.size()-1; i++){
			
			FClause clause = fcsp.get(i);
			System.out.println(clause);
			clause.addToArrayList(templist);
			
		}
		
		System.out.println(templist);
		
		System.out.println(templist.get(0));
		
		//at this point, all the FLiterals in F have been combined to one ArrayList
		//now we need to put them into separate lists
		/*for(int tli=0; tli<=templist.size()-1; tli++){
			
			if(tli == 0 || templist.get(tli).equals(templist.get(tli-1))){
				
				FLiteral literal = templist.get(tli);
				ArrayList<FLiteral> list = new ArrayList<FLiteral>();
				list.add(literal);
				
			}
			
			else{
				
				FLiteral literal2 = templist.get(tli);
				
			}
			
			tli = -1;
		}*/
		
		//for now, just take the first literal of templist and make it your decision literal
		//we will fix this later on
		
		DLiteral decision = templist.get(0).fromAtoDLiteral();
		decision.addDToM(this);
		System.out.println("Decision Literal: " + decision);
		this.printFormula();
		
		
	}
	
	//FailState
	public boolean failState(){
		/*
		 * Fail: M||F,C => FailState if M satisfies !C and M contains no decision literals
		 */
		//check to see if there are any decision literals in M before you see if you've reached FailState
		//if we learn the empty clause, then we reach FailState
		
		boolean result = false;
		
		if(this.dLitsInM() == true){
			/*you have not reached FailState yet, All MLiterals must be forced*/
			System.out.println("Error: DLiterals still exist in M.  FailState has not been reached.");
			System.out.println("FailState = "+ result + ".");
			System.out.println();
		}
		
		else{
			
			//put all MLiterals into a clause
			FClause x = new FClause();
			int i,j;
			
			for(i=0; i<=M.size()-1; i++){
				
				FLiteral f = M.get(i).fromAtoFLiteral();
				
				//now add the opposites of each MLiteral; this new clause is what we're checking for in F
				if(f.isNegated() == true){
					f.negated = false;
					x.addFLit(f);
				}
				
				else{
					f.negated = true;
					x.addFLit(f);
				}
				
			}
			
			for(j=0; j<=F.size()-1; j++){
				
				//does each clause in F have the same rank as the temporary clause of MLiterals?
				if(x.size() == F.size()){
					
					//now since the clauses are of the same rank, see if the literals match up
					if(F.get(j).contradict(x) == true){
						//FailState
						System.out.println("FailState");
						result = true;
					}
					
					else{
						//go to next clause
					}
					
				}
				
				else{
					if(j == F.size()-1){
						//No FailState
						System.out.println("No FailState");
						result = false;
					}
					
					else{
						//do nothing, go to next clause
					}
				}
				
			}
			
		}
		
		System.out.println(result);
		return result;
		
	}
	
	//Restart
	/*
	 * M || F => {} || F
	 */
	public void restart(){
		//print out last step before restarting and wiping out all M
		this.printM();
		System.out.print("|| ");
		this.printF();
		System.out.println("Restart in progress...");
		
		//clear M
		M.clear();
		System.out.println("Restart complete");
	}
	
	//Semi-Superresolution
	public void semiSuperResolution(){
		
		/*
		 * after deciding literals, if you come across forced variables that
		 * contradict each other or contradict a decision literal, learn the 
		 * opposite of the last decision literal (put into F) and Restart
		 */
		if(M.isEmpty()){
			System.out.println("There are no decision literals in M, so { } is the semi-superresolvant");
		}
		
		else{
			//make sure M.size()-1 is a decision literal, NOT just any old M literal
			//add decision literals to a separate ArrayList
			int i;
			ArrayList<DLiteral> list = new ArrayList<DLiteral>();
			
			for(i=M.size()-1; i>=0; i--){
				
				ALiteral test = M.get(i);
				
				if(test.getClass().toString().equals("class DLiteral")){
					
					System.out.println("Adding DLiteral " + test + " to temporary D list...");
					list.add((DLiteral)test);
					System.out.println("DLiteral has been added to temporary list.");
					System.out.println();
					
				}
				else {
					//Do nothing
				}
				
			}
			
			/*
			 *now what we want to do is everything that is in the temporary DLiteral
			 *ArrayList put into a new clause, then add that clause to F.  Get the 
			 *DLiterals from the temporary list, starting from the end of the list
			 */
			
			//if temporary DLiteral list is of rank 1....
			if(list.size() == 1){
				
				FClause ftemp = new FClause(2);
				
				for(i=list.size()-1; i>=0; i--){
					
					//right now all this does is take the last literal of M (which is
					//assumed to be a decision literal) and add its negation to F

					DLiteral temp = list.get(i);
					
					if(temp.isNegated()){
						temp.negated = false;
						ftemp.addDLit(temp);
					}
					else{
						temp.negated = true;
						ftemp.addDLit(temp);
					}
					

					
				}	
				
				F.addClause(ftemp);
				this.printF();
				
			}
			
			//if temporary DLiteral list is of rank 2....
			if(list.size() == 2){
				
				FClause ftemp = new FClause(14);
				
				for(i=list.size()-1; i>=0; i--){
					
					//right now all this does is take the last literal of M (which is
					//assumed to be a decision literal) and add its negation to F

					DLiteral temp = list.get(i);
					
					if(temp.isNegated()){
						temp.negated = false;
						ftemp.addDLit(temp);
					}
					else{
						temp.negated = true;
						ftemp.addDLit(temp);
					}
					
				}				
				
				F.addClause(ftemp);
				this.printF();

			}
			
			//if temporary DLiteral list is of rank 3....
			if(list.size() == 3){
				
				FClause ftemp = new FClause(254);
				
				for(i=list.size()-1; i>=0; i--){
					
					//right now all this does is take the last literal of M (which is
					//assumed to be a decision literal) and add its negation to F

					DLiteral temp = list.get(i);
					
					if(temp.isNegated()){
						temp.negated = false;
						ftemp.addDLit(temp);
					}
					else{
						temp.negated = true;
						ftemp.addDLit(temp);
					}
					
				}
				
				F.addClause(ftemp);
				this.printF();
			}
			
			//if temporary DLiteral list is of rank 4 or more....
			//???????????
		}
	}
		//you would then follow this with Restart
}