import choco.Problem;
import choco.Constraint;
import choco.Solver;
import choco.integer.*;

public class HappyBirthdayboy {
    public static void main( String[] args ) {
	int planLen;
	final int integerRange = 20;
	if ( args.length == 1 )
	    planLen = Integer.parseInt(args[0]);
	else {
	    System.err.println("Usage:  java HappyBirthdayboy <plan length>");
	    return;
	}

	// Build the model
	Problem pb = new Problem();

	// Create variables

	//   Domain Predicates:
	IntDomainVar[] occupied             = new IntDomainVar[planLen+1];
	IntDomainVar[] matchFlame           = new IntDomainVar[planLen+1];
	IntDomainVar[] candleFire           = new IntDomainVar[planLen+1];
	IntDomainVar[] happy                = new IntDomainVar[planLen+1];

	//   Domain Functions:
	IntDomainVar[] numWishes            = new IntDomainVar[planLen+1];

	//   Domain Actions:
	IntDomainVar[] startBurnMatch       = new IntDomainVar[planLen];
	IntDomainVar[] endBurnMatch         = new IntDomainVar[planLen];
	IntDomainVar[] startBurnCandle      = new IntDomainVar[planLen];
	IntDomainVar[] endBurnCandle        = new IntDomainVar[planLen];
	IntDomainVar[] startMakeWish        = new IntDomainVar[planLen];
	IntDomainVar[] endMakeWish          = new IntDomainVar[planLen];
	IntDomainVar[] blowCandle           = new IntDomainVar[planLen];

	//   Performing Predicates:
	IntDomainVar[] performingBurnMatch  = new IntDomainVar[planLen+1];
	IntDomainVar[] performingBurnCandle = new IntDomainVar[planLen+1];
	IntDomainVar[] performingMakeWish   = new IntDomainVar[planLen+1];

	//   Since Functions
	IntDomainVar[] sinceBurnMatch       = new IntDomainVar[planLen+1];
	IntDomainVar[] sinceBurnCandle      = new IntDomainVar[planLen+1];
	IntDomainVar[] sinceMakeWish        = new IntDomainVar[planLen+1];

	//   Happening times
	IntDomainVar[] now                  = new IntDomainVar[planLen+1];


	// Create constraint variables for the "fact layers"
	for ( int i=0; i<=planLen; ++i ) {
	    occupied[i]             = pb.makeEnumIntVar("Occupied_"+i, 0, 1);
	    matchFlame[i]           = pb.makeEnumIntVar("MatchFlame_"+i, 0, 1);
	    candleFire[i]           = pb.makeEnumIntVar("CandleFire_"+i, 0, 1);
	    happy[i]                = pb.makeEnumIntVar("Happy_"+i, 0, 1);

	    numWishes[i]            = pb.makeEnumIntVar("NumberOfWishes_"+i, 0, integerRange);

	    performingBurnMatch[i]  = pb.makeEnumIntVar("PerformingBurnMatch_"+i, 0, 1);
	    performingBurnCandle[i] = pb.makeEnumIntVar("PerformingBurnCandle_"+i, 0, 1);
	    performingMakeWish[i]   = pb.makeEnumIntVar("PerformingMakeWish_"+i, 0, 1);

	    sinceBurnMatch[i]       = pb.makeEnumIntVar("SinceBurnMatch_"+i, 0, integerRange);
	    sinceBurnCandle[i]      = pb.makeEnumIntVar("SinceBurnCandle_"+i, 0, integerRange);
	    sinceMakeWish[i]        = pb.makeEnumIntVar("SinceMakeWish_"+i, 0, integerRange);

	    now[i]                  = pb.makeEnumIntVar("Now_"+i, 0, integerRange);
	}

	// Create constraint variables for the "action layers"
	for ( int i=0; i<planLen; ++i ) {
	    startBurnMatch[i]       = pb.makeEnumIntVar("StartBurnMatch_"+i, 0, 1);
	    endBurnMatch[i]         = pb.makeEnumIntVar("EndBurnMatch_"+i, 0, 1);

	    startBurnCandle[i]      = pb.makeEnumIntVar("StartBurnCandle_"+i, 0, 1);
	    endBurnCandle[i]        = pb.makeEnumIntVar("EndBurnCandle_"+i, 0, 1);

	    startMakeWish[i]        = pb.makeEnumIntVar("StartMakeWish_"+i, 0, 1);
	    endMakeWish[i]          = pb.makeEnumIntVar("EndMakeWish_"+i, 0, 1);

	    blowCandle[i]           = pb.makeEnumIntVar("BlowCandle_"+i, 0, 1);
	}

	// Post constraints
	// - Initial situation
	pb.post(pb.eq(occupied[0],0));
	pb.post(pb.eq(matchFlame[0],0));
	pb.post(pb.eq(candleFire[0],0));
	pb.post(pb.eq(happy[0],0));

	pb.post(pb.eq(numWishes[0],0));

	pb.post(pb.eq(performingBurnMatch[0],0));
	pb.post(pb.eq(performingBurnCandle[0],0));
	pb.post(pb.eq(performingMakeWish[0],0));

	pb.post(pb.eq(sinceBurnMatch[0],0));
	pb.post(pb.eq(sinceBurnCandle[0],0));
	pb.post(pb.eq(sinceMakeWish[0],0));

	pb.post(pb.eq(now[0],0));

	// - Goal
	//    Domain Goal:
	pb.post(pb.eq(happy[planLen],1));

	//    No running durative actions
	pb.post(pb.eq(performingBurnMatch[planLen],0));
	pb.post(pb.eq(performingBurnCandle[planLen],0));
	pb.post(pb.eq(performingMakeWish[planLen],0));

	// - Time non-decreasing
	for (int i=0; i<planLen; ++i) {
	    pb.post(pb.lt(now[i], now[i+1]));
	}

	// - Precondition constraints
	for (int i=0; i<planLen; ++i) {
	    //   Domain preconditions
	    pb.post(pb.implies
		    (pb.eq(startBurnMatch[i],1),
		     pb.eq(occupied[i],0)));
	    pb.post(pb.implies
		    (pb.eq(startBurnCandle[i],1),
		     pb.eq(matchFlame[i],1)));
	    pb.post(pb.implies
		    (pb.eq(startMakeWish[i],1),
		     pb.eq(occupied[i],0)));
	    pb.post(pb.implies
		    (pb.eq(blowCandle[i],1),
		     pb.and(pb.eq(occupied[i],0),
			    pb.eq(candleFire[i],1))));

	    //   Duration constraint preconditions
	    pb.post(pb.implies
		    (pb.eq(endBurnMatch[i],1),
		     pb.eq(pb.minus(now[i+1],sinceBurnMatch[i]),3)));
	    pb.post(pb.implies
		    (pb.eq(endBurnCandle[i],1),
		     pb.leq(pb.minus(now[i+1],sinceBurnCandle[i]),10)));

	    //   Start- End-constraints
	    //     Burn match
	    pb.post(pb.implies
		    (pb.eq(startBurnMatch[i],1),
		     pb.eq(performingBurnMatch[i],0)));
	    pb.post(pb.implies
		    (pb.eq(endBurnMatch[i],1),
		     pb.eq(performingBurnMatch[i],1)));

	    //     Burn candle
	    pb.post(pb.implies
		    (pb.eq(startBurnCandle[i],1),
		     pb.eq(performingBurnCandle[i],0)));
	    pb.post(pb.implies
		    (pb.eq(endBurnCandle[i],1),
		     pb.eq(performingBurnCandle[i],1)));

	    //     Make wish
	    pb.post(pb.implies
		    (pb.eq(startMakeWish[i],1),
		     pb.eq(performingMakeWish[i],0)));
	    pb.post(pb.implies
		    (pb.eq(endMakeWish[i],1),
		     pb.eq(performingMakeWish[i],1)));
	}

	// - Invariant (over all) constraint
	for (int i=1; i<planLen; ++i) {
	    pb.post(pb.implies
		    (pb.eq(performingBurnCandle[i],1),
		     pb.eq(candleFire[i],1)));
	    pb.post(pb.implies
		    (pb.eq(performingMakeWish[i],1),
		     pb.eq(candleFire[i],1)));
	}


	// - Successor state constraints
	for (int i=0; i<planLen; ++i) {
	    //    Number of Wishes
 	    pb.post(pb.implies(pb.eq(endMakeWish[i],1),
			       pb.eq(pb.minus(numWishes[i+1],numWishes[i]),
				     pb.minus(now[i+1],sinceMakeWish[i]))));

 	    pb.post(pb.implies(pb.eq(endMakeWish[i],0),
			       pb.eq(numWishes[i+1],numWishes[i])));

	    //    Occupied
	    pb.post(pb.implies
		    (pb.eq(occupied[i+1],1),
		     pb.or(pb.eq(startBurnMatch[i],1),
			   pb.eq(startMakeWish[i],1),
			   pb.and(pb.eq(occupied[i],1),
				  pb.eq(endBurnMatch[i],0),
				  pb.eq(endMakeWish[i],0)))));
	    pb.post(pb.implies
		    (pb.or(pb.eq(startBurnMatch[i],1),
			   pb.eq(startMakeWish[i],1),
			   pb.and(pb.eq(occupied[i],1),
				  pb.eq(endBurnMatch[i],0),
				  pb.eq(endMakeWish[i],0))),
		     pb.eq(occupied[i+1],1)));

	    //    Match flame
	    pb.post(pb.implies
		    (pb.eq(matchFlame[i+1],1),
		     pb.or(pb.eq(startBurnMatch[i],1),
			   pb.and(pb.eq(matchFlame[i],1),
				  pb.eq(endBurnMatch[i],0)))));
	    pb.post(pb.implies
		    (pb.or(pb.eq(startBurnMatch[i],1),
			   pb.and(pb.eq(matchFlame[i],1),
				  pb.eq(endBurnMatch[i],0))),
		     pb.eq(matchFlame[i+1],1)));

	    //    Candle fire
	    pb.post(pb.implies
		    (pb.eq(candleFire[i+1],1),
		     pb.or(pb.eq(startBurnCandle[i],1),
			   pb.and(pb.eq(candleFire[i],1),
				  pb.eq(endBurnCandle[i],0),
				  pb.eq(blowCandle[i],0)))));
	    pb.post(pb.implies
		    (pb.or(pb.eq(startBurnCandle[i],1),
			   pb.and(pb.eq(candleFire[i],1),
				  pb.eq(endBurnCandle[i],0),
				  pb.eq(blowCandle[i],0))),
		     pb.eq(candleFire[i+1],1)));

	    //    Happy
	    pb.post(pb.implies
		    (pb.eq(happy[i+1],1),
		     pb.or(pb.and(pb.eq(blowCandle[i],1),
				  pb.geq(numWishes[i],3)),
			   pb.eq(happy[i],1))));
	    pb.post(pb.implies
		    (pb.or(pb.and(pb.eq(blowCandle[i],1),
				  pb.geq(numWishes[i],3)),
			   pb.eq(happy[i],1)),
		     pb.eq(happy[i+1],1)));

	    //    Performing
	    //      Burn match
	    pb.post(pb.implies
		    (pb.eq(performingBurnMatch[i+1],1),
		     pb.or(pb.eq(startBurnMatch[i],1),
			   pb.and(pb.eq(performingBurnMatch[i],1),
				  pb.eq(endBurnMatch[i],0)))));
	    pb.post(pb.implies
		    (pb.or(pb.eq(startBurnMatch[i],1),
			   pb.and(pb.eq(performingBurnMatch[i],1),
				  pb.eq(endBurnMatch[i],0))),
		     pb.eq(performingBurnMatch[i+1],1)));

	    //      Burn candle
	    pb.post(pb.implies
		    (pb.eq(performingBurnCandle[i+1],1),
		     pb.or(pb.eq(startBurnCandle[i],1),
			   pb.and(pb.eq(performingBurnCandle[i],1),
				  pb.eq(endBurnCandle[i],0)))));
	    pb.post(pb.implies
		    (pb.or(pb.eq(startBurnCandle[i],1),
			   pb.and(pb.eq(performingBurnCandle[i],1),
				  pb.eq(endBurnCandle[i],0))),
		     pb.eq(performingBurnCandle[i+1],1)));

	    //      Make wish
	    pb.post(pb.implies
		    (pb.eq(performingMakeWish[i+1],1),
		     pb.or(pb.eq(startMakeWish[i],1),
			   pb.and(pb.eq(performingMakeWish[i],1),
				  pb.eq(endMakeWish[i],0)))));
	    pb.post(pb.implies
		    (pb.or(pb.eq(startMakeWish[i],1),
			   pb.and(pb.eq(performingMakeWish[i],1),
				  pb.eq(endMakeWish[i],0))),
		     pb.eq(performingMakeWish[i+1],1)));

	    //    Since
	    //      Burn match
	    pb.post(pb.or
		    (pb.and(pb.eq(startBurnMatch[i],1),
			    pb.eq(sinceBurnMatch[i+1],now[i+1])),
		     pb.and(pb.eq(startBurnMatch[i],0),
			    pb.eq(sinceBurnMatch[i+1],sinceBurnMatch[i]))));

	    //      Burn candle
	    pb.post(pb.or
		    (pb.and(pb.eq(startBurnCandle[i],1),
			    pb.eq(sinceBurnCandle[i+1],now[i+1])),
		     pb.and(pb.eq(startBurnCandle[i],0),
			    pb.eq(sinceBurnCandle[i+1],sinceBurnCandle[i]))));

	    //      Make wish
	    pb.post(pb.or
		    (pb.and(pb.eq(startMakeWish[i],1),
			    pb.eq(sinceMakeWish[i+1],now[i+1])),
		     pb.and(pb.eq(startMakeWish[i],0),
			    pb.eq(sinceMakeWish[i+1],sinceMakeWish[i]))));
	}

	// Action occurrance condition
	for (int i=0; i<planLen;++i) {
	    // Non-Null Step constraint
	    pb.post(pb.or(pb.or(pb.eq(startBurnMatch[i],1),
				pb.eq(endBurnMatch[i],1)),
			  pb.or(pb.eq(startBurnCandle[i],1),
				pb.eq(endBurnCandle[i],1)),
			  pb.or(pb.eq(startMakeWish[i],1),
				pb.eq(endMakeWish[i],1)),
			  pb.eq(blowCandle[i],1)));

	    // Mutex constraints
	    pb.post(pb.or(pb.eq(startBurnMatch[i],0),
			  pb.eq(startBurnCandle[i],0)));
	    pb.post(pb.or(pb.eq(endBurnMatch[i],0),
			  pb.eq(startBurnCandle[i],0)));
	    pb.post(pb.or(pb.eq(startBurnMatch[i],0),
			  pb.eq(endMakeWish[i],0)));
	    pb.post(pb.or(pb.eq(endBurnMatch[i],0),
			  pb.eq(startMakeWish[i],0)));
	    pb.post(pb.or(pb.eq(endBurnMatch[i],0),
			  pb.eq(blowCandle[i],0)));
	    pb.post(pb.or(pb.eq(startBurnCandle[i],0),
			  pb.eq(blowCandle[i],0)));
	    pb.post(pb.or(pb.eq(endMakeWish[i],0),
			  pb.eq(blowCandle[i],0)));	    
	}

	// Solve the problem
	if (pb.solve()) { //pb.minimize(now[planLen],false)) {
	    System.out.println("A solution exists.");
	    for (int i=0; i<pb.getNbIntVars(); ++i) {
		System.out.println(pb.getIntVar(i));
	    }
	}
	else {
	    System.out.println("No solution exists.");
	}
    }
}