//
// Doing our own backtracking, using
//
// - getEnvironment
// - world push
// - instantiateTo
// - worldPop
//

import org.chocosolver.solver.Solver;
import org.chocosolver.solver.variables.*;
import org.chocosolver.solver.constraints.*;
import org.chocosolver.solver.search.strategy.*;
import org.chocosolver.solver.trace.Chatterbox;
import org.chocosolver.solver.exception.ContradictionException;


public class XYZ11 {

    public static void main(String args[]) throws ContradictionException {
	Solver solver = new Solver("x+y+z=11");
	IntVar x = VF.enumerated("x",0,11,solver); // NOTE: enumerated!
	IntVar y = VF.enumerated("y",0,11,solver);
	IntVar z = VF.enumerated("z",0,11,solver);
	solver.post(ICF.sum(new IntVar[]{x,y,z},VF.fixed(11,solver)));
	solver.set(ISF.lexico_LB(new IntVar[]{x,y,z}));
	
	//
	// Start a new world where x=3
	// propagate to see effect then
	// undo this with worlPop
	//
	solver.getEnvironment().worldPush();
	x.instantiateTo(3,null);
	solver.propagate();
	System.out.println(solver);
	solver.getEnvironment().worldPop();

	//
	// now find a 1st solution, and we see x=0 in solution
	//
	System.out.println("there is a solution: "+ solver.findSolution());

	System.out.println(x +" "+ y +" "+ z);
    }
}
//
//
// might also use the times constraint ICF.times(X,Y,C)
// where C can be an IntVar or an int
//