handler bool
{
	class java.lang.Integer;
	class nl;
	class IntUtil;
	class NlIntUtil;

	constraint boEquiv(java.lang.Integer,java.lang.Integer,java.lang.Integer);
	constraint boAnd(java.lang.Integer,java.lang.Integer,java.lang.Integer);
	constraint boOr(java.lang.Integer,java.lang.Integer,java.lang.Integer);
	constraint boXor(java.lang.Integer,java.lang.Integer,java.lang.Integer);
	constraint boNeg(java.lang.Integer,java.lang.Integer);
	constraint boImp(java.lang.Integer,java.lang.Integer);
	constraint boCard(java.lang.Integer,java.lang.Integer,nl,java.lang.Integer);

	rules { 
		
		variable java.lang.Integer X,Y,Z,N,A,B,A1,B1,N1,Len,F,A2,H;
		variable nl L,L1;

		// and
		{ boAnd(0,Y,Z) } <=> { Z = 0 } and1;
		{ boAnd(X,0,Z) } <=> { Z = 0 } and2;
		{ boAnd(1,Y,Z) } <=> { Y = Z } and3;
		{ boAnd(X,1,Z) } <=> { X = Z } and4;
		{ boAnd(X,Y,1) } <=> { X = 1 && Y=1 } and5;
		{ boAnd(X,X,Z) } <=> { X = Z } and6;
		{ boAnd(X,Y,A) &\& boAnd(X,Y,B) } <=> { A = B } and7;
		{ boAnd(X,Y,A) &\& boAnd(Y,X,B) } <=> { A = B } and8;

		// or
		{ boOr(0,Y,Z) } <=> { Z = Y } or1;
		{ boOr(X,0,Z) } <=> { Z = X } or2;
		{ boOr(X,Y,0) } <=> { X=0 && Y=0 } or3;
		{ boOr(1,Y,Z) } <=> { Z = 1 } or4;
		{ boOr(X,1,Z) } <=> { Z = 1 } or5;
		{ boOr(X,X,Z) } <=> { Z = X } or6;
		{ boOr(X,Y,A) &\& boOr(X,Y,B) } <=> { A = B } or7;
		{ boOr(X,Y,A) &\& boOr(Y,X,B) } <=> { A = B } or8;

		// xor
		{ boXor(0,Y,Z) } <=> { Y=Z } xor1;
		{ boXor(X,0,Z) } <=> { X=Z } xor2;
		{ boXor(X,Y,0) } <=> { X=Y } xor3;
		{ boXor(1,Y,Z) } <=> { boNeg(Y,Z) } xor4;
		{ boXor(X,1,Z) } <=> { boNeg(X,Z) } xor5;
		{ boXor(X,Y,1) } <=> { boNeg(X,Y) } xor6;
		{ boXor(X,X,Z) } <=> { Z=0 } xor7;
		{ boXor(X,Y,X) } <=> { Y=0 } xor8;
		{ boXor(Y,X,X) } <=> { Y=0 } xor9;
		{ boXor(X,Y,A) &\& boXor(X,Y,B) } <=> { A = B } xor10;
		{ boXor(X,Y,A) &\& boXor(Y,X,B) } <=> { A = B } xor11;

		// neg
		{ boNeg(0,Y) } <=> { Y = 1 } not1;
		{ boNeg(1,Y) } <=> { Y = 0 } not2;
		{ boNeg(X,0) } <=> { X = 1 } not3;
		{ boNeg(X,1) } <=> { X = 0 } not4;
		{ boNeg(X,X) } <=> { false } neg1;
		{ boNeg(X,Y) &\& boNeg(Y,Z) } <=> { X=Z } neg2;
		{ boNeg(X,Y) &\& boNeg(Z,Y) } <=> { X=Z } neg3;
		{ boNeg(Y,X) &\& boNeg(Y,Z) } <=> { X=Z } neg4;
		
		// Interaction with other boolean constraints
		{ boNeg(X,Y) &\& boAnd(X,Y,Z) } <=> { Z=0 } neg5;
		{ boNeg(Y,X) &\& boAnd(X,Y,Z) } <=> { Z=0 } neg6;
		{ boNeg(X,Z) && boAnd(X,Y,Z) } <=> { X=1 && Y=0 && Z=0 } neg7;
		{ boNeg(Z,X) && boAnd(X,Y,Z) } <=> { X=1 && Y=0 && Z=0 } neg8;
		{ boNeg(Y,Z) && boAnd(X,Y,Z) } <=> { X=0 && Y=1 && Z=0 } neg9;
		{ boNeg(Z,Y) && boAnd(X,Y,Z) } <=> { X=0 && Y=1 && Z=0 } neg10;
		{ boNeg(X,Y) &\& boOr(X,Y,Z) } <=> { Z=1 } neg11;
		{ boNeg(Y,X) &\& boOr(X,Y,Z) } <=> { Z=1 } neg12;
		{ boNeg(X,Z) && boOr(X,Y,Z) } <=> { X=0 && Y=1 && Z=1 } neg13;
		{ boNeg(Z,X) && boOr(X,Y,Z) } <=> { X=0 && Y=1 && Z=1 } neg14;
		{ boNeg(Y,Z) && boOr(X,Y,Z) } <=> { X=1 && Y=0 && Z=1 } neg15;
		{ boNeg(Z,Y) && boOr(X,Y,Z) } <=> { X=1 && Y=0 && Z=1 } neg16;
		{ boNeg(X,Y) &\& boXor(X,Y,Z) } <=> { Z=1 } neg17;
		{ boNeg(Y,X) &\& boXor(X,Y,Z) } <=> { Z=1 } neg18;
		{ boNeg(X,Z) &\& boXor(X,Y,Z) } <=> { Y=1 } neg19;
		{ boNeg(Z,X) &\& boXor(X,Y,Z) } <=> { Y=1 } neg20;
		{ boNeg(Y,Z) &\& boXor(X,Y,Z) } <=> { X=1 } neg21;
		{ boNeg(Z,Y) &\& boXor(X,Y,Z) } <=> { X=1 } neg22;
		{ boNeg(X,Y) && boImp(X,Y) } <=> { X=0 && Y=1 } neg23;
		{ boNeg(Y,X) && boImp(X,Y) } <=> { X=0 && Y=1 } neg24;

		// imp
		{ boImp(0,Y) } <=> { true } imp1;
		{ boImp(X,0) } <=> { X = 0 } imp2;
		{ boImp(1,Y) } <=> { Y = 1 } imp3;
		{ boImp(X,X) } <=> { true } imp4;
		{ boImp(X,Y) && boImp(Y,X) } <=> { X = Y } imp5;

		// equiv 
		//{ boEquiv(X,Y,Z) } <=> { boXor(X,Y,A) && boNeg(Z,A) } equiv;
		{ boEquiv(1,Y,Z) } <=> { Z = Y } equiv1;
		{ boEquiv(X,1,Z) } <=> { X = Z } equiv2;
		{ boEquiv(X,Y,1) } <=> { X = Y } equiv3;
		{ boEquiv(0,Y,Z) } <=> { boNeg(Y,Z) } equiv4;
		{ boEquiv(X,0,Z) } <=> { boNeg(X,Z) } equiv5;
		{ boEquiv(X,Y,0) } <=> { boNeg(X,Y) } equiv6;
		{ boEquiv(X,X,Z) } <=> { Z = 1 } equiv7;
		{ boNeg(X,Y) &\& boEquiv(X,Y,Z) } <=> { Z = 0 } equiv8;

		// card
		if (IntUtil.le(A,0) && IntUtil.le(N,B))
		   { boCard(A,B,L,N) } <=> { true } triv_sat;

		if ( IntUtil.gt(B,0) && nl.ground(L)) 
		   { boCard(N,B,L,N) } <=> {

 		        nl.head(L) = 1 &&
			L1 = nl.rest(L) &&
			B1 = IntUtil.dec(B) &&
			N1 = IntUtil.dec(N) &&
			boCard(N1,B1,L1,N1)

		   } pos_sat;

		if ( nl.ground(L)) 
		   { boCard(A,0,L,N) } <=> {

			nl.head(L) = 0 && 
			L1 = nl.rest(L) &&
			N1 = IntUtil.dec(N) &&
			boCard(A,0,L1,N1)

		   } neg_sat;		

		// special cases with two variables
		if ( 2=nl.size(L) ) 
		   { boCard(0,1,L,2) } <=> {
 
			X = nl.head(L) &&
			L1 = nl.rest(L) &&
			Y = nl.head(L1) &&
			boAnd(X,Y,0) 

		   } boCard2nand;

		if ( 2=nl.size(L) ) 
		   { boCard(1,1,L,2) } <=>  {
 
			X = nl.head(L) &&
			L1 = nl.rest(L) &&
			Y = nl.head(L1) &&
			boNeg(X,Y)

		   } boCard2neg;

		if ( 2=nl.size(L) ) 
		   { boCard(1,2,L,2) } <=> { 

			X = nl.head(L) &&
			L1 = nl.rest(L) &&
			Y = nl.head(L1) &&
			boOr(X,Y,1)

		   } boCard2or;


		if ( N=nl.size(L) && IntUtil.ground(A) && IntUtil.ground(B) &&
		     F=nl.head(L) && F=1 ) 
		   { boCard(A,B,L,N) } <=> {

			L1 = nl.rest(L) &&
			A1 = IntUtil.dec(A) &&
			B1 = IntUtil.dec(B) &&
			N1 = IntUtil.dec(N) &&
			boCard(A1,B1,L1,N1)

		   } pos_red;


		if ( N=nl.size(L) && F=nl.head(L) && F=0 ) 
		   { boCard(A,B,L,N) } <=> {

			L1 = nl.rest(L) &&
			N1 = IntUtil.dec(N) &&
			boCard(A,B,L1,N1)

		   } neg_red;		

	}

    goal and_0_X_Y {
	    variable java.lang.Integer X, Y, Z;
		boAnd(X, Y, Z) && X = 0
	}//end of and_0_X_Y


    goal and_X_Y_Z_xor_1_Z_Y {
	    variable java.lang.Integer X, Y, Z;
		boAnd(X, Y, Z) && boXor(1, Z, Y)
	}//end of and_X_Y_Z_xor_1_Z_Y


    goal equiv_X_1_1 {
	    variable java.lang.Integer X, Y, Z;
		boEquiv(X, Y, Z) && Y = 1 && Z = 1
	}//end of equiv_X_1_1

}//end of handler bool