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

public class Test extends TestCase{
	
	/**
	 * This SIMPLE test should return satisfiable
	 * @param filename
	 */
	
	/* --------------------------------------------
	 *  Because the framework given here cannot
	 *  accept an expression as its input, I have
	 *  to convert the addition constraint here to
	 *  difference constraint.
	 *  
	 *  I use x- and x+ to convert x from the 
	 *  difference constraint.
	 * ----------------------------------------- */
	
	public void testAddConSat()
	{
		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]=-3;
		m.matrix[1][2]=-5;
		m.matrix[2][4]=0;
		m.matrix[5][3]=1;
		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);
		
	}
	
	/* -------------------------------------
	 *  x + y >= 3
	 *  -x - y >= -2
	 *  
	 *  After converting this case,  the test
	 *  case still fail, which should be 
	 *  unsatisfy.
	 */
	
	/* ------------------------------------
	
	public void testAddConUnSat()
	{
		ABMatrix m = new ABMatrix();
		m.matrix = new double[4][4];
		for (int i=0;i<4;i++)
			for(int j=0;j<4;j++)
			{
			  m.matrix[i][j] = Double.NEGATIVE_INFINITY;	
			}
		m.matrix[1][2] = -2;
		m.matrix[3][0] = 3;
		m.M=4;
		
		CdbTuple t = new CdbTuple(m, new String[] {"x", "y", "x-","y-",});
		boolean flag = t.satisfiable();
		Assert.assertTrue(!flag);
	}	
	
	------------------------------------- */

	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);
	}
}
