import java.util.*;


/**
 *  This class decides whether a Boolean Expression of the form (A1^A2^...^An) is satisfiable
 *  Atoms A1,A2... are of the form (x op c) or (x op y)
 *  The algorithm is adopted from Rosenkrantz and Hunt's algo. given in "Processing conjunctive predicates and queries"
 *
 *  Brief steps:
 *  It adjusts the lower and upper bounds of all variable involved in the expression
 *  Creates a hierarchal graph of variables based on the operators "<", ">" present between two variables in an Atom A1
 *
 */
public class Satisfy
{

private Vector type1;
private Vector type2;

public Satisfy() {}

public Satisfy(Vector type1, Vector type2) {this.type1 = type1; this.type2 = type2;}

public Satisfy(Vector type0)
{

	// we need to seggregate type1 and type2 vectors
	type1 = new Vector();
	type2 = new Vector();
	for(int i=0;i<type0.size();i++)
	{
		Atom at = (Atom) type0.get(i);
		if(at.getOperand2() == null)
			type1.add(at);
		else
			type2.add(at);
	}

}





private int[] mark ;
private int dim;
private int[][] arr;
private Hashtable  intAtom;



/*
 *  this is the main method that calls all other methods
 */
public boolean isQuerySatisfiable()
{
	Vector temp = adjustRange(type1);
	//PRINT(temp);
	//System.out.println("-------------");
	boolean flag = checkRange(temp);
	if (!flag)
		return false;
	else
		{
			// we need to adjust ranges from type1 to type2
			type1 = temp;
			type2 = eliminateEqualto(type2); // it modifies both type1 and type2 vectors
			//PRINT(type2);
			//System.out.println("-------------");
			//PRINT(type1);
			//System.out.println("-------------");

			temp = createMatrix(type2);
			flag = checkRange(temp);
			//PRINT(temp);
			if (!flag)
				return false;
			else
				return true;
		}
}






/*
 * Input a Vector of Atoms (x op c) or (x op y) defined over variables (x_1,x_2...x_m)
 * Number of input atoms = n,  where n >= m
 * Output a Vector of Atoms with range defined (lower and upper bound)
 * Number of output atoms = m (one entry per variable)
 */
public Vector adjustRange(Vector inputVector )
{

/* get a list of unique variables present in the inputVector and put them in a Hashtable
 * to do this, iterate over the inputVector. if variable already present in Hashtable, adjust range
 * else add the new variable to the hashtable
 */

Hashtable lookupTable = new Hashtable();

Atom tempAtom,listAtom ;
for(int i=0;i<inputVector.size();i++)
{
	listAtom = (Atom)inputVector.get(i);
	if(lookupTable.containsKey(listAtom.getOperand1()))
		{
			// adjustrange
			/*
				61		int e = (new String("=")).hashCode();
				60		int l = (new String("<")).hashCode();
				1921	int le = (new String("<=")).hashCode();
				62		int g = (new String(">")).hashCode();
				1983	int ge = (new String(">=")).hashCode();
				1922	int ne = (new String("<>")).hashCode();  // this may create problem.. just added here
				1444	int n = (new String("-1")).hashCode();
			*/
			tempAtom = (Atom)lookupTable.remove(listAtom.getOperand1());
			switch(listAtom.getOperator().hashCode())
				{
					case 61:
					//System.out.println("matches = ");
					tempAtom.setRange(listAtom.getConstant(),listAtom.getConstant());
					break;

					case 60	:
					//System.out.println("matches < ");
					tempAtom.setRange(tempAtom.getLeft(),min(tempAtom.getRight(),listAtom.getConstant()-1));
					break;

					case 1921:
					//System.out.println("matches <= ");
					tempAtom.setRange(tempAtom.getLeft(),min(tempAtom.getRight(),listAtom.getConstant()));
					break;

					case 62	:
					//System.out.println("matches > ");
					tempAtom.setRange(max(tempAtom.getLeft(),listAtom.getConstant()+1),tempAtom.getRight());
					break;

					case 1983:
					//System.out.println("matches >= ");
					tempAtom.setRange(max(tempAtom.getLeft(),listAtom.getConstant()),tempAtom.getRight());
					break;

					default:
					System.out.println("Invalid operator: AdjustRange method : in class Satisfy. Will use default range defined in class Atom");
					break;

				}


			lookupTable.put(tempAtom.getOperand1(),tempAtom);
		}

	else
		{
		lookupTable.put(listAtom.getOperand1(),listAtom);
		i--;  // this is the biggest gamble
		// essentially we process the list element again.
		// first time we enter the Atom in the Hashtable and second time we adjust its range

		}
}

Vector outputVector = new Vector();
outputVector.addAll((Collection) lookupTable.values());
return outputVector;

}


public int min(int a, int b)
{
	if(a<=b)
		return a;
	else
		return b;
}


public int max(int a, int b)
{
	if(a>=b)
		return a;
	else
		return b;
}

// check if the range is valid ... meaning (Left <= Right)
public boolean checkRange(Vector in)
{
	Atom at;
	for(int i=0;i<in.size();i++)
	{
		at = (Atom)in.get(i);
		if(at.getLeft() > at.getRight())
			return false;
	}
	return true;
}

public void PRINT(Vector printout)
{
	for(int i=0;i<printout.size();i++)
		{
			Atom x1 = (Atom) printout.get(i);
			System.out.println(x1.getOperand1() + " " + x1.getLeft() + " " + x1.getRight() + " " + x1.getOperator() + " " + x1.getOperand2() + " ");
		}
}




/* this method will eliminate the Atoms of the form "x = y"
 * Ranges of x and y are reconciled and Atom y is deleted from type1 vector
 * All occurances of y in type2 vector is replaced by x
 */
public Vector eliminateEqualto(Vector t2)
{
	String e = (new String("="));
	for(int i=0;i<t2.size();i++)
	{
		Atom b = (Atom)t2.get(i);
		if( (b.getOperator()).equals(e) )
		 {
				String f1 = b.getOperand1();
				String f2 = b.getOperand2();
				t2.remove(i); // remove that vector from t2 and adjust its size
				i--; // vector adjustment

				// replace all occurances of f2 by f1 in type2
				for(int l=0;l<t2.size();l++)
				{
					Atom f = (Atom)t2.get(l);
					if( (f.getOperand1()).equals(f2) )
						{
							f.setOperand1(f1);
							t2.set(l,f);
						}
					else if( (f.getOperand2()).equals(f2) )
						{
							f.setOperand2(f1);
							t2.set(l,f);
						}
				}

				// adjust type1 now. eliminate the occurance of f2, and adjust ranges.
				Atom c = new Atom();
				Atom d = new Atom();

				for(int j=0;j<type1.size();j++)
					{

						c = (Atom)type1.get(j);
						if( (c.getOperand1()).equals(f2) ) 	//  reconcile the range of f1 annd f2
						{
							c = (Atom) type1.remove(j);  // delete f2
							for(int k=0;k<type1.size();k++)
							{
								d = (Atom)type1.get(k);
								if( (d.getOperand1()).equals(f1) )
										{
												Atom ee = new Atom(d);
												ee.setRange(max(c.getLeft(),d.getLeft()),min(c.getRight(),d.getRight()));
												type1.set(k,ee);
												//System.out.println("entered elimination equalto step");
												break;
										}
							}
						break; // this may give some problem
						}
					}

		}
	}

	return t2;

}



public Vector createMatrix(Vector inputVector)
{

	Hashtable lookupTable = new Hashtable();  // key=operand value=Atom
	Hashtable operandInt = new Hashtable();   // key=operand value=Integer
	intAtom = new Hashtable(); // key=Integer value=Atom

	Atom listAtom ;
	dim=0;

	// this for loop is just for creating unique variables ...(there could be some in type2 but not in type1)
	// inputVector is of type2
	// we populate the hashtable lookupTable with empty atoms
	for(int i=0;i<inputVector.size();i++)
	{
		listAtom = (Atom)inputVector.get(i);
		if(lookupTable.containsKey(listAtom.getOperand1()))
			{
				// check for duplicate like (x < y) (x >= y)
				Atom dupl = (Atom) lookupTable.get(listAtom.getOperand1());
				if(listAtom.getOperand2() == dupl.getOperand2())
					{
						// here we have 2 predicates having the same operands
						selectOne(listAtom,dupl);

					}
			}
		else
			{
				lookupTable.put(listAtom.getOperand1(),listAtom);
				//operandInt.put(listAtom.getOperand1(),new Integer(dim));
				//dim++;
			}

		if(lookupTable.containsKey(listAtom.getOperand2()))
			{

			}
		else
			{
				lookupTable.put(listAtom.getOperand2(),listAtom);
				//operandInt.put(listAtom.getOperand2(),new Integer(dim));
				//dim++;

			}

	}

	// iterate over the type1 vector and copy its range to the Atoms present in lookupTable
	// NOTE: there could be variables in type1 not in type2...... we accomodate this condition
	for(int i=0;i<type1.size();i++)
	{
		// if x11 is already presnt in lookupTable, replace it, else add it to the lookupTable
		Atom x11 = (Atom)type1.get(i);
		lookupTable.remove(x11.getOperand1()); // this might yield null object. in that case do nothing
		lookupTable.put(x11.getOperand1(),x11); //
	}


	dim=0;
	operandInt = new Hashtable();

	// populate intAtom and operandInt hashtables
	// we need this hashtable for further access
	// NOTE :  operandInt contains only variable in type2 .. what abt type1 ?
	Enumeration itr = ((Enumeration) lookupTable.keys());
	while(itr.hasMoreElements())
	{
			Object tempObject = itr.nextElement(); // the object is an operand
			operandInt.put(tempObject,new Integer(dim));
			intAtom.put(new Integer(dim),lookupTable.get(tempObject));
			dim++;
	}


	Enumeration itr2 = ((Enumeration) operandInt.keys());
	while(itr2.hasMoreElements())
	{
		Object tempObject = itr2.nextElement();
		System.out.println(tempObject.toString() + " " +  ((Integer)operandInt.get(tempObject)).intValue() );

	}


	/*
	Enumeration itr = ((Enumeration) operandInt.keys());
	while(itr.hasMoreElements())
	{
		Object tempObject = itr.nextElement();
		intAtom.put(operandInt.get(tempObject),lookupTable.get(tempObject));
	}
	*/


// dim is the number of variables
// define and initialize array
	arr = new int[dim][dim];
	for(int i=0;i<dim;i++)
	for(int j=0;j<dim;j++)
		arr[i][j] = 0;

// set the mark to 0 (false)
	mark = new int[dim];
 	for(int i=0;i<dim;i++)
      mark[i] = 0;


	String e = (new String("="));
	String l = (new String("<"));
	String g = (new String(">"));
	String le = (new String("<="));
	String ge = (new String(">="));
	String op1,op2,oper;


	for(int i=0;i<inputVector.size();i++) // populate matrix
	{
		listAtom = (Atom)inputVector.get(i);
		op1 = listAtom.getOperand1();
		op2 = listAtom.getOperand2();
		oper = listAtom.getOperator();

		if( oper.equals(g) || oper.equals(ge) )
		{
			arr[((Integer)operandInt.get(op1)).intValue()][((Integer)operandInt.get(op2)).intValue()] = 1;
		}
		else if ( oper.equals(l) || oper.equals(le) )
		{
			arr[((Integer)operandInt.get(op2)).intValue()][((Integer)operandInt.get(op1)).intValue()] = 1;
		}
		else
		{
			System.out.println("Creating matrix: operator = this case should have been handled earlier");
		}
	}

/*
	for(int i=0;i<dim;i++)
	{
	for(int j=0;j<dim;j++)
		System.out.print(arr[i][j]);
	System.out.println();
	}
*/


// real procedure
	for(int i=0;i<dim;i++)
	{
		callPred(i);
	}



Vector printout = new Vector();
printout.addAll((Collection) intAtom.values());
return printout;



}

// recursive function
public void callPred(int i)
{
	while(mark[i]==0)
	{
		for(int j=0;j<dim;j++)
			{
				//System.out.println("did i enter col" + i + " " + j);
				if(arr[i][j] == 1)
				{
					if(mark[j] == 0)
							callPred(j);

					Atom predecessor = (Atom)intAtom.get(new Integer(j));
					Atom current = (Atom)intAtom.remove(new Integer(i));
					int lower = max(current.getLeft(), (predecessor.getLeft() + 1));
					// only lower bound is considered, since we form the matrix with only one operator ">"
					current.setRange(lower, current.getRight());
					intAtom.put(new Integer(i),current);
							//set bound
							// continue

				}
			}

		mark[i] = 1; // set mark
	}

}




}