import Zql.*;
import java.util.*;


/**
*  Determines whether a particular query can be satisfied from the data present in the local cache
*
*/
public class Solver
{

private ZQuery user_ ;
private ZQuery modified_ ;
private ZQuery answerby_ ;
private ZQuery remainder_ ;

public ZQuery getUQuery() { return user_; }
public ZQuery getModified() { return modified_; }
public ZQuery getAnswerby() { return answerby_; }
public ZQuery getRemainder() { return remainder_; }



/** check whether the user query can be satisfied from local data
 *  if satisfied, find the modified, answerby & remainder queries and return TRUE
 *  else return FALSE
 */
public boolean isQuerySatisfiable(QueryObject ob)
{

user_ = ob.getZQuery();
// qgidVector contains ID's of all queries in cache whose signatures match with new query "ob"
Vector qgidVector = Cache.signatureMatch(ob);

	if(qgidVector==null)  // implies hashSet or hashTable empty
		{
			System.out.println("New Query: " + user_.toString());
			System.out.println("No previous queries in cache: New query cannot be satisfied locally ");
			remainder_ = user_;
			return false;
		}
	else
	if(qgidVector.size()==0)  // implies no match found
		{
			System.out.println("New Query: " + user_.toString());
			System.out.println("No signature match found in cache: New query cannot be satisfied locally ");
			remainder_ = user_;
			return false;
		}
	else
		{

		Vector iterateVector = new Vector();
		Vector principalVector = new Vector();  // a vector of vectors (vector T)
		// each Ti is a vector of negated atoms

		for(int i=0;i<qgidVector.size();i++)
			{
				int x = Cache.getIndex( ( (Integer)qgidVector.get(i)).intValue() );
				iterateVector = (Vector) ((Vector)Cache.negatedQueryPredicates).get(x);
				principalVector.add(iterateVector);
			}
				// we are trying to show that -(q-->t) is true
				// -(-q v t) == (q ^ -t)
				// ==  q ^ -t1 ^ -t2 ^ ....
				// but for each atoms in t1 ... disjunction has to be handled
		if(isSat(ob.getPredicates(),principalVector))
			{
			 // currently we are only working with queries that are completely answerable from cache
			 //modified_ = userQuery.getZQuery();
			 //answerby_ = cachedQuery.getZQuery();
			 remainder_ = null;
			 System.out.println("New Query: " + user_.toString());
			 System.out.println("Query can be satisfied locally: ");
			 return true;

			}

		System.out.println("New Query: " + user_.toString());
		System.out.println("Signature match found: But new query cannot be completely satisfied locally ");
		remainder_ = user_;
		return false;


		}

}

// Q in conjunctive form only.
// that will lead to negated T in disjunctive form
public boolean isSat(Vector object1, Vector T)
{

//System.out.println("Object predicates" + object1.toString());
//System.out.println("Cache  predicates" + T.toString());
//System.out.println();
	Satisfy stf;
	Vector parcel;

	int tSize = T.size();

	parcel = new Vector(tSize);
	for(int i=0;i<tSize;i++)
		parcel.add(   ((Vector)T.get(i)).get(0) );

	int arr[][] = new int[tSize][2];
	int pr = 1;
	for(int i=(tSize-1);i>=0;i--)
	{
		arr[i][1] = ((Vector)T.get(i)).size();
		arr[i][0] = pr;
		pr *= arr[i][1];
	}


	for(int j=0;j<pr;j++)
	{

		for(int i=0;i<tSize;i++)
		{

		if( (j%arr[i][0]) == 0  ) // remainder of multiple
			{
			  int index = (j/arr[i][0])%arr[i][1]; // remainder of quotient
   			  parcel.set(i,((Vector)T.get(i)).get(index));
			}

		}

		// execution step
		Vector pack = new Vector(parcel);
		pack.addAll(0,object1);
		stf = new Satisfy(pack);
		if(stf.isQuerySatisfiable())
			{
				Vector _temp1 = new Vector(Atom.getComplement(parcel));
				_temp1.addAll(0,object1);
				System.out.println("Unsolvable boolean predicates " + _temp1.toString());
				return false;

			}

	}

	return true;

}





}