import junit.framework.Assert;
import junit.framework.TestCase;

public class Test extends TestCase{
	
	/**
	 * This SIMPLE test should return satisfiable
	 * @param filename
	 */

/*
 * In the testSat() Function, I construct an addition constraint 
 * -x-z>=-3
 * z-y>=-8
 * w+y>=2
 * w-x>=-4
 * 
 * First translate every variable into two variables, for example: x-->x+ and x-
 * Then put them in the matrix. Assume that every row denotes the negative represenation of the variable
 * and each column denotes the possitive representation of variable
 *   x y z w x- y- z- w-
 * -x
 * -y
 * -z
 * -w
 * -x-
 * -y-
 * -z-
 * -w-
 * It is an 8*8 matrix. Then the addition constraints can be translated into difference constraints:
 * -x-z>=-3 ==> (x-)-z>=-3
 * z-y>=-8  ==>  z-y>=-8  
 * w+y>=2   ==>  w-(-y)>=2
 * w-x>=-4  ==>  w-x>=-4
 *    x y z w x- y- z- w-
 * -x * * * -4 *  *  *  *
 * -y * * -8 * *  *  *  *
 * -z * * * * -3  *  *  *
 * -w * * * * *  *  *  *
 * -x-* * * * *  *  *  *
 * -y-* * * 2 *  *  *  *
 * -z-* * * * *  *  *  *
 * -w-* * * * *  *  *  *
 * 
 * After this coversion, we can use the SAT function for difference constraint to test the satisfication of the addition constraint
 */	
	
	
	public void testSimpleSat()
	{
		ABMatrix m = new ABMatrix();
		m.matrix = new double[5][5];
		for (int i=0; i<5; i++)
			for (int j=0; j<5; j++)
			{
				m.matrix[i][j] = Double.NEGATIVE_INFINITY;
			}
		m.matrix[1][0] = 5; // x-y >= 5
		m.matrix[0][1] = -10; // -x+y >= -10
		m.M = 5;
		
		CdbTuple t = new CdbTuple(m, new String[] {"x", "y", "z", "x1", "z1"});
		boolean flag = t.satisfiable();
		Assert.assertTrue(flag);
	}
	
	public void testSimpleUnsat()
	{
		ABMatrix m = new ABMatrix();
		m.matrix = new double[5][5];
		for (int i=0; i<5; i++)
			for (int j=0; j<5; j++)
			{
				m.matrix[i][j] = Double.NEGATIVE_INFINITY;
			}
		m.matrix[1][0] = 12; // x-y >= 12
		m.matrix[0][1] = -10; // -x+y >= -10
		m.M = 5;
		
		CdbTuple t = new CdbTuple(m, new String[] {"x", "y", "z", "x1", "z1"});
		boolean flag = t.satisfiable();
		Assert.assertTrue(!flag);
	}
	
	public void testSat()
	{
		ABMatrix m = new  ABMatrix();
		m.matrix = new   double[8][8];
		
		for (int i=0;i<8;i++)
			for(int j=0;j<8;j++)
			{
			  m.matrix[i][j] =   Double.NEGATIVE_INFINITY;	
			}
		m.matrix[0][3]=  -4;
		m.matrix[1][2]=  -8;
		m.matrix[2][4]=  -3;
		m.matrix[5][3]=  2;
		m.M=8;
		
		CdbTuple  t = new   CdbTuple(m, new String[] {"x", "y", "z", "w", "x-","y-","z-","w-"});
		boolean  flag  =   t.satisfiable();
		Assert.assertTrue(flag);
		
	}
	
}
