package rccDiagram.util;

import java.lang.reflect.InvocationTargetException;
import java.lang.reflect.Method;
import java.util.Arrays;
import java.util.Collection;
import java.util.HashSet;
import java.util.Iterator;
import java.util.LinkedList;
import java.util.List;
import java.util.Set;
import java.util.Stack;
import java.util.concurrent.RejectedExecutionException;

import rccDiagram.lang.Constraint;
import rccDiagram.lang.ContradictionException;
import rccDiagram.lang.ConstraintVariable;
import rccDiagram.lang.RCCPoint;
import rccDiagram.lang.RCCSet;
import rccDiagram.lang.Region;

/**
 * Execute the RCC Procedure.  This class is Runnable, therefore
 * can be threaded if proper caution is taken in setting up the
 * RCCState.
 * @author Patrick
 *
 */
public class RCCProcedure implements Runnable {

	private RCCState state;
	private int maxdepth;
	private int	depth;
	private RCCSet<Constraint> set;
	private RCCSet<Constraint> old;
	private int deepest_prop;
	private String last_prop;
	
	/** Maintains a stack for the recursion to assoicate assertions 
with parents */
	private Stack<Constraint> workingStack;
	private Stack<List<Constraint>> assertionStack;
	/** Supplementary Constraints involved with assertion */
	private List<Constraint> workingSupplement;
	
	/**
	 * Avoid race conditions by offering a fresh state.
	 * The maximum depth of the Procedure is Integer.MAX_VALUE;
	 * @param state
	 * @param maxdepth Determines the maximum depth the procedure 
should
	 *			recurse to.  
	 */
	public RCCProcedure(RCCState state){
		this.state = state;
		int maxdepth = (Integer) 
this.state.runtime.getValue("depth");
		
		this.depth = 0;
		this.deepest_prop = 0;
		this.last_prop = new String();
		if(maxdepth < -1)
			throw new IllegalArgumentException("Invalid 
maximum depth: "+depth);
		else if(maxdepth == -1)
			this.maxdepth = Integer.MAX_VALUE;
		else 
			this.maxdepth = maxdepth;
		
		this.set = this.state.getSet();
		this.old = new RCCSet<Constraint>();
		this.workingStack = new Stack<Constraint>();
		this.assertionStack = new Stack<List<Constraint>>();
		this.assertionStack.push(new LinkedList<Constraint>());
	}
	
	public void run() {
		if(!state.silent()){
			state.progress().pln("Beginning RCC 
Algorithm.").incr().flush();
			if(this.set.size() < 1){
				state.progress().pln("No Constraints - 
Invalid Set").flush();
				throw new 
RejectedExecutionException("Set is empty");
			}
		}
		try {
			main();
		} catch (ContradictionException e) {
			if(!state.silent()){
				
this.state.progress().reset().pln("Failure on Contradiction").
					
indentMore().pln(e.toString()).flush();
			}
			this.state.runtime.error(e);
		} catch (Exception e) {
			if(!state.silent()){
				
this.state.progress().reset().pln("Failure on unknown exception").
					
indentMore().pln(e.toString()).flush();
			}
			this.state.runtime.error(e);
		}
	}
	
	/**
	 * Executes the RCCProcedure on the given set.
	 * @throws ContradictionException
	 */
	public void main() throws ContradictionException{
		if(!state.silent()){
			this.state.progress().pln("Eliminating 
EQ's").flush();
		}
		eliminateEQs();
		if(state.intermediary()){
			state.printSet();
		}
		if(!state.silent()){
			this.state.progress().pln("Propogating 
Constraints").flush();
		}
		//Create an iterable copy to allow concurrent 
modification.
		for(Constraint c : this.set.cloneSet()){
			propagate(c);		
		}
		if(!state.silent()){
			
this.state.progress().decr().pln().pln("Generating 
Supplementaries").flush();
		}
		genSupplementaries();
	}
	
	/**
	 * propagates over a constraint built from the given Name and 
ConstraintVariable
	 * @param Cname
	 * @param geometry
	 * @throws ContradictionException
	 */
	public void propagate(String Cname, ConstraintVariable ... 
geometry)
	 throws ContradictionException{
		Constraint c = new Constraint(Cname, geometry);
		propagate(c);
	}
	
	/**
	 * propagates over the given Constraint
	 * @param c
	 * @throws ContradictionException
	 */
	public void propagate(Constraint c) throws 
ContradictionException{
		//Return if the maximum depth is passed.
		
		this.depth++;
		if(this.state.test()){
			StringBuilder builder = new StringBuilder();
			builder.append("propagate").append(c.name());
			for(Iterator<ConstraintVariable> iter = 
c.iterator(); iter.hasNext(); ){
				builder.append(' 
').append(iter.next().toString());
			}
			this.last_prop = builder.toString();
			if(this.depth > this.deepest_prop) 
this.deepest_prop = this.depth;
		}
		if(this.depth > this.maxdepth){ depth--; pop(); return; 
}
		
		ConstraintVariable A = c.get(0);
		ConstraintVariable B = c.get(1);
		if(A.equals(B)){
			throw new ContradictionException(c,A+"=="+B);
		}
		String name = "propagate"+c.name();
		try {
			this.push(c);
			Method m = this.getClass().getMethod(name, 
c.getClass());
			printSource();
			Boolean success = (Boolean) m.invoke(this, c);
			printAssertions();
			this.pop();
		} catch (SecurityException e) {
			this.state.runtime.error(e);
		} catch (NoSuchMethodException e) {
			this.state.runtime.error(e);
		} catch (IllegalArgumentException e) {
			this.state.runtime.error(e);
		} catch (IllegalAccessException e) {
			this.state.runtime.error(e);
		} catch (InvocationTargetException e) {
			Exception exc = (Exception) e.getCause();
			if(exc instanceof ContradictionException)
				throw (ContradictionException)exc;
			else
				this.state.runtime.error(exc);
		}
		this.depth--;
	}


	/**
	 * procedure propagateNTPP(A,B)
	 * {
	 * 	if (NTPP(A,B) in OLD) return;
   	 *	if ((A==B) or (TPP(A,B) in S)) fail;
   	 *	assert(NTPP(A,B));
   	 *	propagatePP(A,B);
     *  for (every region C)
     *  { if (DC(B,C) or EC(B,C) or DS(B,C) in S) propagateDC(A,C);
     *    if (EC(A,C) in S) propagateO(B,C);
     *    if (PP(B,C) in S) propagateNTPP(A,C));
     *  }
	 * }
	 * @param c
	 * @throws ContradictionException 
	 */
	public void propagateNTPP(Constraint c) throws 
ContradictionException{
		if(this.old.contains(c)) return;
		List<ConstraintVariable> geo = c.getVariables();
		ConstraintVariable A = geo.get(0);
		ConstraintVariable B = geo.get(1);
		if(this.set.contains("TPP", A,B)) contradict(c, "TPP", 
A,B);
		
		assertConstraint(c);
		propagate("PP",A,B);

		for(Region C : 
this.set.cloneSet().getRegionsIgnoring(A,B)){
			if(this.set.contains("DC", B, C) || 
this.set.contains("EC", B, C) ||
					this.set.contains("DS", B, C) ){
				propagate("DC", A, C);
			}
			if(this.set.contains("EC", A, C)){
				propagate("O", B, C);
			}
			if(this.set.contains("PP", B, C)){
				propagate("NTPP", A, C);
			}
		}
	}

	/**
	 * procedure propagateTPP(A,B)
	 *	{	if (TPP(A,B) in OLD) return;
  	 *		if ((A==B) or (NTPP(A,B) in S)) fail;
  	 *		assert(TPP(A,B));
  	 *		propagatePP(A,B);
	 *	}
	 * @param c
	 * @throws ContradictionException 
	 */
	public void propagateTPP(Constraint c) throws 
ContradictionException {
		if(this.old.contains(c)) return;
		List<ConstraintVariable> geo = c.getVariables();
		ConstraintVariable A = geo.get(0);
		ConstraintVariable B = geo.get(1);
		if(this.set.contains("NTPP", A,B)) 
			contradict(c,"NTPP",A,B);
		assertConstraint(c);
		propagate("PP",A,B);
		
	}

	/**
	 * procedure propagatePP(A,B)
	 *	{ if (PP(A,B) in OLD) return;
  	 *	assert(PP(A,B));
  	 *	if ((A==B) or (PP(B,A) or OV(A,B) or in S) fail;
  	 *	propagateO(A,B);
  	 *  propagateC(A,B);
  	 *	for (every region C)
   	 *	{ if (NTPP(B,C) in S) propagateNTPP(A,C);
     * 		if (TPP(B,C) or PP(B,C) in S) propagatePP(A,C);
     *		if (DC(B,C) in S) propagateDC(A,C);
     * 		if (EC(B,C) or DS(B,C) in S) propagateDS(A,C);
     *		if (PP(A,C) in S) propagateO(B,C);
   	 *	}
	 * }
	 */
	public void propagatePP(Constraint c) throws 
ContradictionException {
		List<ConstraintVariable> geo = c.getVariables();
		ConstraintVariable A = geo.get(0);
		ConstraintVariable B = geo.get(1);
		if(this.old.contains(c)) return;
		assertConstraint(c);
		if(this.set.contains("PP", B, A))	
			contradict(c, "PP",B,A);
		if(this.set.contains("OV",A,B))
			contradict(c, "OV",A,B);
		propagate("O",A,B);
		propagate("C",A,B);
		for(Region C : 
this.set.cloneSet().getRegionsIgnoring(A,B)){
			if(this.set.contains("NTPP",B,C))
				propagate("NTPP",A,C);
			if(this.set.contains("TPP",B,C) || 
					this.set.contains("PP",B,C)){
				propagate("PP",A,C);
			}
			if(this.set.contains("DC",B,C))
				propagate("DC",A,C);
			if(this.set.contains("EC",B,C) || 
this.set.contains("DS",B,C))
				propagate("DS",A,C);
			if(this.set.contains("PP",A,C))
				propagate("O",B,C);
		}			
	}
	
	/**
	 * procedure propagateOV(A,B)
	 *	{ if (OV(A,B)  in OLD) return;
  	 *		assert(OV(A,B));
  	 *		assert(OV(B,A));
  	 *		if ((A==B) or (PP(A,B) or PP(B,A) in S) fail;
  	 *		propagateO(A,B);
	 *	}
	 */
	public void propagateOV(Constraint c) throws 
ContradictionException{
		if(this.old.contains(c)) return;
		List<ConstraintVariable> geo = c.getVariables();
		ConstraintVariable A = geo.get(0);
		ConstraintVariable B = geo.get(1);
		assertConstraint("OV",A,B);
		assertConstraint("OV",B,A);
		if(this.set.contains("PP",A,B))
			contradict(c,"PP",A,B);
		if(this.set.contains("PP",B,A))
			contradict(c,"PP",B,A);
		propagate("O",A,B);
	}

	/**
	 * procedure propagateO(A,B)
	 *	{ if (O(A,B) in OLD) return;
  	 *		assert(O(A,B));
  	 *		assert(O(B,A));
  	 *		if ((A==B) or DS(A,B) in S) fail;
  	 *		for (each region C)
     *			if (PP(B,C) in S) propagateO(A,C);
     *			if (PP(A,C) in S) propagateO(B,C);
     *    propagateC(A,B)
	 *	}
	 * @param c
	 * @throws ContradictionException
	 */
	public void propagateO(Constraint c) throws 
ContradictionException{
		if(this.old.contains(c)) return;
		List<ConstraintVariable> geo = c.getVariables();
		ConstraintVariable A = geo.get(0);
		ConstraintVariable B = geo.get(1);
		assertConstraint("O",A,B);
		assertConstraint("O",B,A);
		if(this.set.contains("DS",A,B))
			contradict(c,"DS",A,B);
		for(Region C : this.set.getRegionsIgnoring(A,B)){
			if(this.set.contains("PP",B,C))
				propagate("O",A,C);
			if(this.set.contains("PP",A,C))
				propagate("O",B,C);
		}
		propagate("C",A,B);
	}
	
	/**
	 * propagateEC(A,B)
	 *	{ if (EC(A,B) in OLD) return;
  	 *		assert(EC(A,B));
  	 *		assert(EC(B,A));
  	 *		if (A==B or DC(A,B) in S) fail;
  	 *		propagateDS(A,B);
  	 *      propagateC(A,B);
	 *	}
	 */
	public void propagateEC(Constraint c) throws 
ContradictionException{
		if(this.old.contains(c)) return;
		List<ConstraintVariable> geo = c.getVariables();
		ConstraintVariable A = geo.get(0);
		ConstraintVariable B = geo.get(1);
		assertConstraint("EC",A,B);
		assertConstraint("EC",B,A);
		if(this.set.contains("DC",A,B))
			contradict(c,"DC",A,B);
		propagate("DS",A,B);
		propagate("C",A,B);
	}
	
	/**
	 *  propagateDC(A,B)
	 *	{   if (DC(A,B) in OLD) return;
  	 *		assert(DC(A,B));
  	 *		assert(DC(B,A));
  	 *		if (A==B or C(A,B) in S) fail;
  	 *		propagateDS(A,B);
  	 *  for (each region C)
  	 *  { if (PP(C,A) in S) {assert DC(C,B); assert(DC(B,C);}
  	 *  { if (PP(C,B) in S) {assert DC(C,A); assert(DC(A,C);}
	 *	}  
	 * 
	 * @param c
	 * @throws ContradictionException
	 */
	public void propagateDC(Constraint c) throws 
ContradictionException{
		if(this.old.contains(c)) return;
		List<ConstraintVariable> geo = c.getVariables();
		ConstraintVariable A = geo.get(0);
		ConstraintVariable B = geo.get(1);
		assertConstraint("DC",A,B);
		assertConstraint("DC",B,A);
		if(this.set.contains("C",A,B))
			contradict(c,"C",A,B);
		propagate("DS",A,B);
		
		for(Region C : 
this.set.cloneSet().getRegionsIgnoring(A,B)){
			if(this.set.contains("PP",C,A)){
				assertConstraint("DC",C,B);
				assertConstraint("DC",B,C);
			}
			if(this.set.contains("PP",C,B)){
				assertConstraint("DC",C,A);
				assertConstraint("DC",A,C);
			}
		}
		
	}
	
	

	/**
	 * propagateDS(A,B)
	 * { if (DS(A,B) in OLD) return;
  	 *	if (A==B or O(A,B) in S) fail;
  	 *  assert(DS(A,B));
  	 *	assert(DS(B,A));
  	 *  if (C(A,B) in S) { assert EC(A,B); assert EC(B,A); }
  	 *  for (each region C)
  	 *  { if (PP(C,A) in S) {assert DS(C,B); assert(DS(B,C);}
  	 *  { if (PP(C,B) in S) {assert DS(C,A); assert(DS(A,C);}
  	 *	
  	 * }
	 * @param c
	 * @throws ContradictionException
	 */
	public void propagateDS(Constraint c) throws 
ContradictionException{
		if(this.old.contains(c)) return;
		List<ConstraintVariable> geo = c.getVariables();
		ConstraintVariable A = geo.get(0);
		ConstraintVariable B = geo.get(1);
		if(this.set.contains("O",A,B))
			contradict(c,"O",A,B);			
		assertConstraint("DS",A,B);
		assertConstraint("DS",B,A);
		
		for(Region C : 
this.set.cloneSet().getRegionsIgnoring(A,B)){
			if(this.set.contains("PP",C,A)){
				assertConstraint("DS",C,B);
				assertConstraint("DS",B,C);
			}
			if(this.set.contains("PP",C,B)){
				assertConstraint("DS",C,A);
				assertConstraint("DS",A,C);
			}
		}
	}
	
	/**
		propagateC(A,B)
		{ if (C(A,B) in OLD) return;
		  if (DC(A,B) in S) fail;
		  assert C(A,B);
		  assert C(B,A);
		  if (DS(A,B) in S) { assert EC(A,B); assertEC(B,A) }
		  for (each region C) 
		    { if (NTPP(A,C) in S) propagateO(B,C);
		       else if (PP(A,C) in S) propagateC(B,C);
		      if (NTPP(B,C) in S) propagateO(A,C);
		       else if (PP(B,C) in S) propagateC(A,C);
		    }  
		}
	*/
	public void propagateC(Constraint c){
		if(this.old.contains(c)) return;
		List<ConstraintVariable> geo = c.getVariables();
		ConstraintVariable A = geo.get(0);
		ConstraintVariable B = geo.get(1);
		if(this.set.contains("DC",A,B))
			contradict(c,"DC",A,B);
		
		assertConstraint("C",A,B);
		assertConstraint("C",B,A);
		if(this.set.contains("DS",A,B)){
			assertConstraint("EC",A,B);
			assertConstraint("EC",B,A);
		}
		for(Region C : 
this.set.cloneSet().getRegionsIgnoring(A,B)){
			if(this.set.contains("NTPP",A,C))
				propagate("O",B,C);
			else if(this.set.contains("PP",A,C))
				propagate("C",B,C);
			if(this.set.contains("NTPP",B,C))
				propagate("O",A,C);
			else if(this.set.contains("PP",B,C))
				propagate("C",A,C);
			
		}
	}
	
	
	public void genSupplementaries() throws ContradictionException{
		if(state.intermediary()){
			state.printSet();
		}
		if(!state.silent()){
			
this.state.progress().pln("GenerateO").flush().incr();
		}
		generateO();
		
		if(state.intermediary()){
			state.printSet();
		}
		if(!state.silent()){
			
this.state.progress().pln().pln("GeneratePP").flush();
		}
		generatePP();
		
		if(state.intermediary()){
			state.printSet();
		}
		if(!state.silent()){
			
this.state.progress().pln().pln("GenerateContacts").flush();
		}
		generateContacts();
	}
	
	
	
	/**
	 *	procedure generateO()
	 *	{ for (all regions A,B such that O(A,B))
	 *	   { 
	 *		 if ((PP(A,B) is not in S) and (PP (B,A) is not 
in S)
	 *		   and there is no region R such that PP(R,A) 
and PP(R,B))
	 *	        then { create a new region R;
	 *	               propagatePP(R,A);
	 *	               propagatePP(R,B);
	 *	             }
	 *	     if (OV(A,B)) {
	 *	       if (there is no region R such that PP(R,A) and 
DS(R,B))
	 *	          then { create a new region R;
	 *	                 propagatePP(R,A);
	 *	                 propagateDS(R,B);
	 *	               }
	 *	       if (there is no region R such that PP(R,B) and 
DS(R,A))
	 *	          then { create a new region R;
	 *	                 propagatePP(R,B);
	 *	                 propagateDS(R,A);
	 *	               }
	 *	      }//end if OV A B
	 *	   }//end for
	 *	}
	 * @throws ContradictionException 
	 */
	public void generateO() throws ContradictionException{
		//for all regions OV(A,B)
		for(Constraint c : this.set.getConstraints("O")){
			if(state.verbose()){
				
state.progress().pln("*"+c.toString()).flush();
			}
			
			push(c);
			
			//Flags the existence of such
			boolean ppabba = false;
			boolean pprab = false;
			boolean ppdsrab = false;
			boolean ppdsrba = false;
			
			ConstraintVariable A = c.get(0);
			ConstraintVariable B = c.get(1);
			
			//(if no ppab and no ppba)
			if(this.set.contains("PP",A,B) || 
this.set.contains("PP",B,A))
				ppabba = true;
				
			//grab all PP( R , A)
			Set<Constraint> ppra = this.set.getComplex("PP", 
null, A);
			for(Constraint ppc : ppra){
				ConstraintVariable R = ppc.get(0);
				if(R.equals(A) || R.equals(B)) continue;
				//If size 0, this relationship doesn't 
exist
				
if(this.set.getComplex("PP",R,B).size()>0) pprab = true;
			}
			if(!pprab && !ppabba){
				Region newRegion = makeRegion();
				propagate("PP",newRegion,A);
				propagate("PP",newRegion,B);
			}
			
			if(this.set.getComplex("OV", A,B).size()>0){
				ppra = this.set.getComplex("PP", null, 
A);
				for(Constraint ppc : ppra){
					ConstraintVariable R = 
ppc.get(0);
					if(R.equals(A) || R.equals(B)) 
continue;
					//If null, this relationship 
doesn't exist
					
if(this.set.getComplex("DS",R,B).size()>0) ppdsrab = true;
				}
				if(!ppdsrab){
					Region newRegion = makeRegion();
					propagate("PP",newRegion,A);
					propagate("DS",newRegion,B);					
				}

				Set<Constraint> pprb = 
this.set.getComplex("PP", null, B);
				for(Constraint ppc : pprb){
					ConstraintVariable R = 
ppc.get(0);
					if(R.equals(A) || R.equals(B)) 
continue;
					//If null, this relationship 
doesn't exist
					
if(this.set.getComplex("DS",R,A).size()>0) ppdsrba = true;
				}
				if(!ppdsrba){
					Region newRegion = makeRegion();
					propagate("PP",newRegion,B);
					propagate("DS",newRegion,A);
				}
			}//end if OV A B
			pop();
		}
	}
	
	
	
	/**
	 * Note: if NTPP(A,B) then the existence of B-A is taken care of
	 *	in diagram generation
	 *
	 * procedure generatePP() 
	 *	{ for (all regions A,B such that PP(A,B) and not 
NTPP(A,B))
     *	if (there is no region R such that PP(R,B) and DS(R,A))
     *	then { create a new region R;
     *       propagatePP(R,B);
     *       propagateDS(R,A);
     *		}
	 *	}
	 * @throws ContradictionException 
	 * 
	 */
	public void generatePP() throws ContradictionException{
		Set<Constraint> subSet = this.set.getConstraints("PP");
		for(Constraint c : subSet){
			push(c);
			if(state.verbose()){
				
state.progress().pln("*"+c.toString()).flush();
			}
			
			ConstraintVariable A = c.get(0);
			ConstraintVariable B = c.get(1);
			//If no NTPP
			if(this.set.getComplex("NTPP",A,B).size()>0) 
continue;
			
			boolean pprb_dsra = false;
			
			Set<Constraint> cpprb = 
this.set.getComplex("PP", null, B);
			for(Constraint ppc : cpprb){
				ConstraintVariable R = ppc.get(0);
				if(R.equals(A) || R.equals(B)) continue;
				if(this.set.getComplex("DS", 
R,A).size()>0)
					pprb_dsra = true;
			}
			if(!pprb_dsra){
				ConstraintVariable newRegion = 
makeRegion();
				propagate("PP", newRegion,B);
				propagate("DS", newRegion,A);
			}
			
			pop();
		}
	}
	
	/**
	 * procedure generateContacts ()
	 *	{ mark all constraints EC(A,B) or TPP(A,B) as 
"unsatisfied";
  	 *		repeat (until all constraints are satisfied)
     *		{ let R(A,B) be an unsatisfied constraint;
     * 			mark R(A,B) as satisfied;
     * 			Q := { A,B } /* Q is a set of regions
     * 			for (every unsatisfied constraint R1(C,D))
   	 *			{ if (C is in Q and D is not in Q and
   	 *				(there is no (E in Q) for which 
DC(E,D) or NTPP(E,D) in S)
   	 *				then { add D to Q;
     *             	mark R1(C,D) as satisfied;
     *           	} 
     *   		}
     *  		generate a new point P;
     *  		for (C in Q) add BdPt(P,C)
     *		}
	 *	}  
	 */
	public void generateContacts(){
		LinkedList<Constraint> unsatisfied = new 
LinkedList<Constraint>();
		unsatisfied.addAll(this.set.getConstraints("EC","TPP"));
		//let c be a constraint
		while(unsatisfied.size()>0){
			//mark as satisfied
			Constraint z = unsatisfied.remove();
			ConstraintVariable A = z.get(0);
			ConstraintVariable B = z.get(1);
			
			push(z);
			
			if(state.verbose()){
				state.progress().indent().p("Unsatisfied 
").pln(z.toString()).flush();
			}
			
			
			//Build Q
			Set<ConstraintVariable> Q = new 
HashSet<ConstraintVariable>();
			Q.add(A);
			Q.add(B);
			//Create a modifiable iterator to avoid 
concurrent modification x.
			for(Constraint R1 : 
(List<Constraint>)unsatisfied.clone()){
				ConstraintVariable C = R1.get(0);
				ConstraintVariable D = R1.get(1);
				//There exists no DC(E,D) and no 
NTPP(E,D)
				if(Q.contains(C) && !Q.contains(D)){
					if(this.set.getComplex("DC", 
null,D).size()<1
						|| 
this.set.getComplex("NTPP",null,D).size()<1){
					
						//Add D to Q, mark c as 
satisfied
						Q.add(D);
						unsatisfied.remove(R1);
					}
				}
			}
			//generate point
			RCCPoint p = makePoint();
			//for c in q, add BdPt(p, c)
			for(ConstraintVariable c : Q){
				assertConstraint("BdPt", p,c);
			}
			printAssertions();
			pop();
		}
	}
	
	/** 
	 * For every relation EQ(A,B) in S, replace B by A throughout S.
     *   (Be sure, however, that in the eventual diagram the region is 
labelled 
     *   both A and B.) 
	 * @throws ContradictionException 
	 */
	public void eliminateEQs() throws ContradictionException{
		Collection<Constraint> removable = new 
LinkedList<Constraint>();
		for(Constraint c : this.set){
		//We are looking for EQ only
		if(!c.name().equals("EQ")) continue;
			List<ConstraintVariable> list = 
c.getVariables();
			ConstraintVariable newG = list.get(0);
			for(ConstraintVariable oldG : list){
				//Rename all subsequent 
ConstraintVariable to the first name
				if(! oldG.equals(newG)){
					if(state.verbose()){
						
this.state.progress().indentMore().
							pln("Renamed 
"+oldG.name()+" to "+newG.name()).flush();
					}
					//Gather old Constraints
					Set<Constraint> oldSet = 
this.set.getConstraints(oldG);
					//Check for contradictions, 
remove this EQ
					oldSet.remove(c);
					for(Constraint old : oldSet){
						if(old.involves(newG)) 
throw new ContradictionException(old);
					}
					//RENAME
					this.set.renameGeometry(newG, 
oldG);
				}
			}
			removable.add(c);
		}
		this.set.removeAll(removable);
	}
	
	public int getDeepestProp(){
		return this.deepest_prop;
	}
	
	public String getLastProp(){
		return this.last_prop;
	}
	
	/**
	 * Throws a ContradictionException based on the offending 
Constraint.
	 * @param c
	 * @throws ContradictionException
	 */
	private void contradict(Constraint c) throws 
ContradictionException{
		throw new ContradictionException(c);
	}
	
	/**
	 * Throws a ContradictionException with an associated Constraint 
built from
	 * Cname and the variable number of ConstraintVariable.
	 * @param c
	 * @param Cname
	 * @param gs
	 * @throws ContradictionException
	 */
	private void contradict(Constraint c, String Cname, 
ConstraintVariable ... gs)
	 throws ContradictionException{
		StringBuilder msg = new StringBuilder();
		msg.append(Cname);
		msg.append("(");
		for(int i=0; i<gs.length; i++){
			msg.append(gs[i]);
			if(i != gs.length-1)
				msg.append(", ");
		}
		msg.append(")");
		throw new ContradictionException(c,msg.toString());
	}
	
	
	private void assertConstraint(Constraint c){
		if(!this.set.contains(c)){
			this.set.add(c);
			if(assertionStack != null)
				this.assertionStack.peek().add(c);
		}
		this.old.add(c);
		if(workingStack != null && !workingStack.isEmpty())
			c.source(workingStack.peek());
	}
	
	private Constraint assertConstraint(String name, 
List<ConstraintVariable> constraintVariable){
		Constraint c = new Constraint(name, constraintVariable);
		assertConstraint(c);
		return c;
	}
	
	private Constraint assertConstraint(String name, 
ConstraintVariable ... geometry){
		return assertConstraint(name, Arrays.asList(geometry));
	}
	
	/**
	 * Make a new RCCPoint, give it a numerical name based on the
	 * size of the current set of Points, and add it to the Set.
	 * @return The RCCPoint added.
	 */
	private RCCPoint makePoint(){
		int size = this.set.sizePoints();
		RCCPoint p = new RCCPoint("P"+size);
		while(this.set.containsPoint(p)){ 
			size++; p = new RCCPoint("P"+size);
		}
		this.set.addPoint(p);
		if(state.verbose()){
			state.progress().indentMore().p("New RCCPoint   
").pln(p.name()).flush();
		}
		return p;
	}
	
	private Region makeRegion(){
		int size = this.set.sizeRegions();
		Region r = new Region("R"+size);
		while(this.set.containsRegion(r)){ 
			size++; r = new Region("R"+size);
		}
		this.set.addRegion(r);
		if(state.verbose()){
			state.progress().indentMore().p("New Region 
").pln(r.name()).flush();
		}
		return r;
	}
	
	private void push(Constraint c){
		workingStack.push(c);
		assertionStack.push(new LinkedList<Constraint>());
	}
	
	private List<Constraint> pop(){
		if(!workingStack.isEmpty())
			workingStack.pop();
		if(!assertionStack.isEmpty())
			return this.assertionStack.pop();
		return null;
	}
	
	private void printSource() {
		if(!state.verbose()) return;
		Constraint c = workingStack.peek();
		state.progress().indent().p("Propagating ");
		if(c.source() != null && 
c.source().toString().equals("Input"))
			state.progress().p("Top Level Constraint - ");
		state.progress().p(c.toString()).p(" - 
").pln(depth).flush();
	}
	
	private void printAssertions() {
		if(!state.verbose()) return;
		if(assertionStack.isEmpty()) return;
		List<Constraint> assertionList = assertionStack.peek();			
		//Print a list of Assertions
		for(Constraint assertion : assertionList){
			String source = "null";
			if(assertion.source() != null) source = 
assertion.source().toString();
			state.progress().indentMore().p("asserting   ").
				p(assertion.toString()).
				p(" - ").pln(depth);
		}
		state.progress().flush();
		
	}
}