/*
 * CSP Project
 * Authors:
 * 		Jay Bernardo
 * 		Matt Rancourt
 * 
 * File: TransitionManager.java
 * 
 * Contains the TransitionManager class. 
 * This class is responsible for applying transitions in the proper
 * order and maintining the M || F values and "doing the right thing"
 * at the right time
 *  
 */

import edu.neu.ccs.satsolver.*;

class TransitionManager{
	TransitionAssignment M;
	CSP F;
	
	/**
	 * Constructor
	 * @param c - CSP that is the "F" part of the transition
	 */
	public TransitionManager(CSP c)
	throws
		RelationNumberOutOfBoundsException,
		RankOutOfBoundsException,
		InvalidVariableNamesLengthException,
		InvalidVariableValueException{
		
		this.F = c.duplicate();
		M = new TransitionAssignment();
	}
	
	/**
	 * The run method simply applies transitions "forever" until
	 * either the SolveState or FailState occurs, determining which
	 * transitions to apply based on what previous transitions
	 * have accomplished or done.
	 * 
	 * NOTE: UnitPropagate is the only transition that actually
	 *       assigns variables in F, therefore it will be the 
	 *       main decider of the order in which transitions 
	 *       should be applied
	 * 
	 * @throws InvalidVariableValueException
	 * @throws RelationNumberOutOfBoundsException
	 * @throws RankOutOfBoundsException
	 * @throws InvalidVariableNamesLengthException
	 * @throws VariablePositionOutOfBoundsException
	 */
	public void run()
	throws
		InvalidVariableValueException,
		RelationNumberOutOfBoundsException,
		RankOutOfBoundsException,
		InvalidVariableNamesLengthException,
		VariablePositionOutOfBoundsException{
		
		// Create a restart so that we can capture F, unmodified
		Restart r = new Restart(M, F);
		
		boolean doInputInitial = true;
		PolynomialI oldPolynomial = null;
		
		// Loop "forever"
		while(true){
			
			// The first step is always to try and apply unit propagate
			print();
			System.out.println("\nUnitPropagate =>");
			UnitPropagate u = new UnitPropagate(M, F);
			int unitPropagateResult = u.doTransition();
			if(unitPropagateResult == -1){				
				// When Unit Propagate cannot do anything, then it is time for us
				// to decide upon a new variable
				System.out.println("Unit Propagate cannot perform any further.\n");
				
				print();
				Decide d = new Decide(M, F);
				
				if(doInputInitial != true){
					d.setPolynomial(oldPolynomial);
				}
				
				d.doingInitial(doInputInitial);
				d.doTransition();
				oldPolynomial = d.getPolynomial();
				
				doInputInitial = false;
				
				System.out.println("\nDecide =>");
				print();
				System.out.println("\n");
			}
			else if(unitPropagateResult == 1){
				// Semisuperresolution is required here. UnitPropagate has
				// determined that after assigning some variable, there is a relation
				// that is unsatisfied
				print();
				System.out.println("\n");
				
				print();
				System.out.println("\nSemiSuperResolution =>");
				SemiSuperResolution ssr = new SemiSuperResolution(M, F);
				ssr.doTransition();
				ssr.newRelation.print();
				
				// After running SemiSuperResolution we have to restart
				System.out.println("\n");
				print();
				System.out.println("\nRestart =>");
				r.doTransition();
				
				// This will not work in r.doTransition -- does not propagate upward. Must be done here
				F = r.originalF.duplicate();
				F.addRelation(ssr.newRelation);
				print();
				System.out.println("\n");
				
				// Make a new restart, keeping track of the new formula as
				// the "original"
				r = new Restart(M, F);
				
				// The update pairs has to be recreated
				//updatePairs = new HashMap<Integer, Integer>();
				doInputInitial = true;
				oldPolynomial = null;
			}
			else{
				print();
				System.out.println("\n");
			}
			
			
			// We will check for failstate
			FailState f = new FailState(M, F);
			if(f.doTransition() == 1){
				
				print();
				System.out.println("\nFailState =>");
				// We have failed
				System.out.println("Unsolvable");
				
				System.exit(1);
			}
			
			// At this point, we haven't failed, so lets check if we have 
			// a solution
			SolveState s = new SolveState(M, F);
			if(s.doTransition() == 1){
				print();
				System.out.println("\nSolveState =>");
				// We have failed
				System.out.println("Solved");
				
				System.exit(1);
			}
		}
	}
	
	/**
	 * Generic print method to display the manager in a pretty format
	 */
	void print(){
		System.out.print("{");
		int i = 0;
		for(; i < M.numberOfVariables(); i ++){
			M.getVariableAt(i).print();
			System.out.print(" ");
		}
		System.out.print("} || ");
		F.print(false);
	}
}