import parma_polyhedra_library.*;

public class PPLBug {

	public static void main(String[] args) {
		System.load("/usr/local/lib/ppl/libppl_java.so");
		Parma_Polyhedra_Library.initialize_library();
		Variable v0 = new Variable(0);
		Variable v1 = new Variable(1);
		
		// generate box1 with "A in 0, B in 1"
		Double_Box box1 = new Double_Box(2,Degenerate_Element.UNIVERSE);
		box1.affine_image(v0, new Linear_Expression_Coefficient(new Coefficient(0)), new Coefficient(1));
		box1.affine_image(v1, new Linear_Expression_Coefficient(new Coefficient(1)), new Coefficient(1));
		System.out.println (box1);  // correct: A in 0, B in 1
		
		// copy box1 into box2
		Double_Box box2 = new Double_Box(box1);
		System.out.println (box2);  // correct: A in 0, B in 1
		
		// assignment B = 4 applied to box1
		box1.affine_image(v1, new Linear_Expression_Coefficient(new Coefficient(4)), new Coefficient(1));		
		System.out.println (box1);  // correct: A in 0, B in 4
	
		// refining box2 with A > 1 should give false and it does
		Linear_Expression le = new Linear_Expression_Variable(v0);
		box2.refine_with_constraint(new Constraint(le, Relation_Symbol.GREATER_THAN, new Linear_Expression_Coefficient(new Coefficient(1))));		

		// ********************** NOTE 1 ********************
		// If I uncomment the line below, then everything works!! 
		// System.out.println(box2);   
		
		// ********************** NOTE 2 ********************
		// if I replace the call to refine_with_constraint with the following line, the result is correct.
		// Double_Box box2 = new Double_Box(2,Degenerate_Element.UNIVERSE);
				
		box1.upper_bound_assign(box2);
		System.out.println(box2);  // correct: false
		System.out.println(box1);  // wrong!! it should be "A in 0, B in 4", it is "A in 0, B in [1,4]"
		
		Parma_Polyhedra_Library.finalize_library();
	}
}