import java.applet.Applet;
import java.awt.*;
import java.awt.event.*;
import java.applet.*;
import java.awt.geom.*;
import java.math.*;


/*This file does calculation 3*/


public class ProofCalc3 {

    public static void main(Manager M) {
	for(int i=0;i<8;++i) M.C.MESSAGE[i]="";
	M.C.MESSAGE[0]="start calc 3";
	M.C.MESSAGE[1]="start first order-2 test";
	M.C.repaint();
	test1();
	M.C.MESSAGE[1]="first order-2 test done";

	M.C.MESSAGE[3]="start first order-2 test";
	M.C.repaint();
	M.C.MESSAGE[2]="start second order-2 test";
	M.C.repaint();
	test2();
	M.C.MESSAGE[2]="second order 2 test done";

	M.C.MESSAGE[3]="start main test";
	M.C.repaint();
	test3(M);
	M.C.MESSAGE[6]="main  test done";
	M.C.MESSAGE[7]="calc 3 done";
	M.C.repaint();

    }

    public static void fail() {
	throw new ProofException("calculation 3 fails");
    }


    /*Here is 6 times the 420-scaled volume of the trivial tile
      from 5/4 to 2. The unscaled tile has cross section
      (0,1), (-1,0), (0,1), (0,-1), which has area 2.
      The quantity we consider is 2 (2-5/4) 6 420 420 420*/

    public static long volumeTrivial() {
	return(666792000);
    }


    public static LongPolyhedron phi(LongPolyhedron P) {
	long x=0;
	for(int i=0;i<P.count;++i) x=x+P.V[i].x[0];
	int hand=0;
	if(x>0) hand=1;
	LongPolyhedron Q=new LongPolyhedron(P);
	for(int i=0;i<Q.count;++i) Q.V[i]=phi(hand,P.V[i]);
	Q.SCALE=P.SCALE;
	Q.FACE=P.FACE;
	return(Q);
    }

    public static LongVector phi(int hand,LongVector V) {
	LongVector W=new LongVector(V);
	W.x[2]=V.x[2]+420;
	if(hand==0) {
            W.x[0]=V.x[0]-420;
            W.x[1]=V.x[1]-420;
	}
	if(hand==1) {
	    W.x[0]=V.x[0]+420;
	    W.x[1]=V.x[1]+420;
	}
	return(W);
    }


    /*Checks the order 2 tile on the
      interval [5/4,2]*/
    public static void test1() {
	int[] I={0,19};
	for(int q=0;q<2;++q) {
          LongPolyhedron P1=DataPartition.imagePoly(I[q]);
	  LongPolyhedron Q1=phi(P1);
          LongPolyhedron Q2=ProofSupport.F2(Q1);
          boolean test1=isOutside(Q1);
          LongPolyhedron Q3=ProofSupport.F2(Q2);
          boolean test2=isOutside(Q2);
          boolean test3=LongPolyCombinatorics.isSubset(Q3,Q1);
	  if(test1==false) fail();
	  if(test2==false) fail();
	  if(test3==false) fail();
	}
    }

/*Checks the order 2 tile on the interval [1,3/2].
  We precompute the desired polyhedron separately in this case.*/
    public static void test2() {
        LongPolyhedron Q1=DataPartitionExtra.order2B();
        LongPolyhedron Q2=ProofSupport.F2(Q1);
        boolean test1=isOutside(Q1);
        LongPolyhedron Q3=ProofSupport.F2(Q2);
        boolean test2=isOutside(Q2);
        boolean test3=LongPolyCombinatorics.isSubset(Q3,Q1);
	if(test1==false) fail();
	if(test2==false) fail();
	if(test3==false) fail();
    }










    /*Target is the volume of the domain from 5/4 to 2.
      This is the main part of the calculation.*/

    public static void test3(Manager M) {
	long total=0;
	long target=2167074000L;
	for(int i=1;i<19;++i) {
	    LongPolyhedron P0=DataPartition.poly(i);
	    LongPolyhedron P1=DataPartition.imagePoly(i);
	    int test=checkReturn(P0,P1);
	    total=total+test*DataPartition.volume(i);
	}
	for(int i=20;i<32;++i) {
	    LongPolyhedron P0=DataPartition.poly(i);
	    LongPolyhedron P1=DataPartition.imagePoly(i);
	    int test=checkReturn(P0,P1);
	    total=total+test*DataPartition.volume(i);
	}
	total=total+2*DataPartition.volume(0)+2*DataPartition.volume(19);
	total=total+volumeTrivial();  //vol of trivial tile in [5/4,2]
	if(total!=target) fail();
	Long T1=new Long(total);
	Long T2=new Long(target);
	M.C.MESSAGE[3]="volume check";
	M.C.MESSAGE[4]= T1.toString();
	M.C.MESSAGE[5]= T2.toString();
    }


    public static int checkReturn(LongPolyhedron P0,LongPolyhedron P1) {
	boolean test=false;
	int count=0;
	LongPolyhedron Q0=phi(P0);
	LongPolyhedron Q1=phi(P1);
	while(test==false) {    
	    ++count;
	    Q1=ProofSupport.F2(Q1);
	    boolean test1=isOutside(Q1);
	    boolean test2=LongPolyCombinatorics.isSubset(Q1,Q0);
	    if((test1==false)&&(test2==false)) fail();
	    if(test2==true) return(count);
	}
	return(-1);
    }

    public static boolean isOutside(LongPolyhedron P) {
	for(int i=1;i<19;++i) {
	    LongPolyhedron Q=phi(DataPartition.poly(i));
	    if(LongPolyCombinatorics.separate(10,P,Q)==false) return(false);
	}
	for(int i=20;i<32;++i) {
	    LongPolyhedron Q=phi(DataPartition.poly(i));
	    if(LongPolyCombinatorics.separate(10,P,Q)==false) return(false);
	}
	return(true);
    }


}