public interface Condition {

	/**
	 * Returns an object instance of a class implementing {@code Condition}, built from the specified arguments.
	 * 
	 * @param operator
	 *            a relational operator {@code TypeConditionOperatorRel}, a set operator
	 *            {@code TypeConditionOperatorSet} or a more general object {@code TypeConditionOperator}
	 * @param limit
	 *            an integer (object {@code Number}), a variable (object {@code IVar}), a range (object {@code Range})
	 *            or a 1-dimensional array of {@code int}
	 * @return an object instance of a class implementing {@code Condition}, built from the specified arguments
	 */
	public static Condition buildFrom(Object operator, Object limit) {
		if (limit instanceof XParameter)
			return new ConditionPar(operator, (XParameter) limit);
		if (operator instanceof TypeConditionOperatorRel) {
			TypeConditionOperatorRel op = (TypeConditionOperatorRel) operator;
			return limit instanceof Number ? new ConditionVal(op, ((Number) limit).longValue()) : new ConditionVar(op, (IVar) limit);
		} else if (operator instanceof TypeConditionOperatorSet) {
			TypeConditionOperatorSet op = (TypeConditionOperatorSet) operator;
			return limit instanceof Range ? new ConditionIntvl(op, ((Range) limit)) : new ConditionIntset(op, ((int[]) limit));
		} else {
			control(operator instanceof TypeConditionOperator, " Bad Argument");
			TypeConditionOperator op = (TypeConditionOperator) operator;
			if (limit instanceof Long)
				return new ConditionVal(op.toRel(), (Long) limit);
			if (limit instanceof IVar)
				return new ConditionVar(op.toRel(), (IVar) limit);
			if (limit instanceof XNodeLeaf && ((XNodeLeaf<?>) limit).type == TypeExpr.VAR)
				return new ConditionVar(op.toRel(), (IVar) ((XNodeLeaf<?>) limit).value);
			if (limit instanceof IntegerInterval)
				return new ConditionIntvl(op.toSet(), ((IntegerInterval) limit).inf, ((IntegerInterval) limit).sup);
			assert limit instanceof long[];
			return new ConditionIntset(op.toSet(), LongStream.of((long[]) limit).mapToInt(l -> Utilities.safeInt(l)).toArray());
		}
	}

	/**
	 * Returns the variable involved in the condition, if one is present, {@code null} otherwise.
	 * 
	 * @return the variable involved in the condition, if one is present, {@code null} otherwise
	 */
	default IVar involvedVar() {
		return null;
	}

	TypeExpr operatorTypeExpr();

	Object rightTerm();

	default int[] filtering(int[] values) {
		throw new AssertionError("should not be called for this kind of objects");
	}

	public class ConditionPar implements Condition {
		public Object operator;
		public XParameter par;

		public ConditionPar(Object operator, XParameter par) {
			this.operator = operator;
			this.par = par;
		}

		public Condition concretizeWith(Object limit) {
			return Condition.buildFrom(operator, limit);
		}

		@Override
		public TypeExpr operatorTypeExpr() {
			return operator instanceof TypeConditionOperatorRel ? ((TypeConditionOperatorRel) operator).toExpr()
					: ((TypeConditionOperatorSet) operator).toExpr();
		}

		@Override
		public Object rightTerm() {
			return par;
		}

	}

	/**
	 * Represents a condition based on a relational operator.
	 */
	public abstract class ConditionRel implements Condition {
		/**
		 * The relational operator on which the condition is based.
		 */
		public TypeConditionOperatorRel operator;

		/**
		 * Constructs a condition based on a relational operator.
		 * 
		 * @param operator
		 *            a relational operator
		 */
		public ConditionRel(TypeConditionOperatorRel operator) {
			this.operator = operator;
		}

		@Override
		public TypeExpr operatorTypeExpr() {
			return operator.toExpr();
		}
	}

	/**
	 * Represents a condition composed of a relational operator and a variable as operand.
	 */
	public static class ConditionVar extends ConditionRel {
		/**
		 * The variable that represents the operand of the condition.
		 */
		public IVar x;

		/**
		 * Constructs a condition composed of the specified relational operator and the specified variable as (right)
		 * operand
		 * 
		 * @param operator
		 *            a relational operator
		 * @param x
		 *            a variable
		 */
		public ConditionVar(TypeConditionOperatorRel operator, IVar x) {
			super(operator);
			this.x = x;
		}

		@Override
		public IVar involvedVar() {
			return x;
		}

		@Override
		public Object rightTerm() {
			return x;
		}

		@Override
		public String toString() {
			return "(" + operator.name().toLowerCase() + "," + x + ")";
		}
	}

	/**
	 * Represents a condition composed of a relational operator and a value (long integer) as (right) operand.
	 */
	public static class ConditionVal extends ConditionRel {
		/**
		 * The value that represents the operand of the condition.
		 */
		public long k;

		/**
		 * Constructs a condition composed of the specified relational operator and the specified value as (right)
		 * operand
		 * 
		 * @param operator
		 *            a relational operator
		 * @param k
		 *            an integer
		 */
		public ConditionVal(TypeConditionOperatorRel operator, long k) {
			super(operator);
			this.k = k;
		}

		@Override
		public Object rightTerm() {
			return k;
		}

		@Override
		public int[] filtering(int[] values) {
			return IntStream.of(values).filter(v -> {
				switch (operator) {
				case LT:
					return v < k;
				case LE:
					return v <= k;
				case GE:
					return v >= k;
				case GT:
					return v > k;
				case EQ:
					return v == k;
				case NE:
					return v != k;
				}
				throw new AssertionError();
			}).toArray();
		}

		@Override
		public String toString() {
			return "(" + operator.name().toLowerCase() + "," + k + ")";
		}
	}

	/**
	 * Represents a condition based on a set operator.
	 */
	public abstract class ConditionSet implements Condition {
		/**
		 * The set operator on which the condition is based.
		 */
		public TypeConditionOperatorSet operator;

		/**
		 * Constructs a condition based on a set operator.
		 * 
		 * @param operator
		 *            a set operator
		 */
		public ConditionSet(TypeConditionOperatorSet operator) {
			this.operator = operator;
		}

		@Override
		public TypeExpr operatorTypeExpr() {
			return operator.toExpr();
		}
	}

	/** The class denoting a condition where the operand is an interval. */

	/**
	 * Represents a condition composed of a set operator and an interval (defined by its two inclusive bounds) as
	 * (right) operand.
	 */
	public static class ConditionIntvl extends ConditionSet {
		/**
		 * The lower bound (inclusive) of the interval.
		 */
		public long min;

		/**
		 * The upper bound (inclusive) of the interval.
		 */
		public long max;

		/**
		 * Constructs a condition composed of a set operator and an interval (defined by its two inclusive bounds) as
		 * (right) operand
		 * 
		 * @param operator
		 *            a set operator
		 * @param min
		 *            the lower bound (inclusive) of the interval
		 * @param max
		 *            the upper bound (inclusive) of the interval
		 */
		public ConditionIntvl(TypeConditionOperatorSet operator, long min, long max) {
			super(operator);
			control(min <= max, "The specified bouds are not valid.");
			this.min = min;
			this.max = max;
		}

		/**
		 * Constructs a condition composed of a set operator and an interval defined by a range.
		 * 
		 * @param operator
		 *            a set operator
		 * @param range
		 *            a range denoting an interval
		 */
		public ConditionIntvl(TypeConditionOperatorSet operator, Range range) {
			this(operator, range.start, range.stop - 1);
			control(range.step == 1, "Specified ranges must have a step equal to 1");
		}

		public Range range() {
			return new Range(safeInt(min), safeInt(max) + 1);
		}

		@Override
		public Object rightTerm() {
			return range();
		}

		@Override
		public int[] filtering(int[] values) {
			return IntStream.of(values).filter(v -> {
				switch (operator) {
				case IN:
					return min <= v && v <= max;
				case NOTIN:
					return v < min || v > max;
				}
				throw new AssertionError();
			}).toArray();
		}

		@Override
		public String toString() {
			return "(" + operator.name().toLowerCase() + "," + min + ".." + max + ")";
		}

	}

	/**
	 * Represents a condition composed of a set operator and an array of values (int) as (right) operand.
	 */
	public static class ConditionIntset extends ConditionSet {
		/**
		 * The array of values, used as (right) operand.
		 */
		public int[] t;

		/**
		 * Constructs a condition composed of a set operator and an array of values (int) as (right) operand.
		 * 
		 * @param operator
		 *            a set operator
		 * @param t
		 *            the array of values, used as (right) operand
		 */
		public ConditionIntset(TypeConditionOperatorSet operator, int[] t) {
			super(operator);
			t = IntStream.of(t).sorted().distinct().toArray();
			control(t.length > 0, "The specified array is empty (and so, not valid).");
			this.t = t;
		}

		@Override
		public Object rightTerm() {
			return t;
		}

		@Override
		public int[] filtering(int[] values) {
			return IntStream.of(values).filter(v -> {
				switch (operator) {
				case IN:
					return Arrays.binarySearch(t, v) >= 0;
				case NOTIN:
					return Arrays.binarySearch(t, v) < 0;
				}
				throw new AssertionError();
			}).toArray();
		}

		@Override
		public String toString() {
			return "(" + operator.name().toLowerCase() + ",{" + join(t, ",") + "})";
		}
	}
} public abstract class ConditionRel implements Condition {
	/**
	 * The relational operator on which the condition is based.
	 */
	public TypeConditionOperatorRel operator;

	/**
	 * Constructs a condition based on a relational operator.
	 * 
	 * @param operator
	 *            a relational operator
	 */
	public ConditionRel(TypeConditionOperatorRel operator) {
		this.operator = operator;
	}

	@Override
	public TypeExpr operatorTypeExpr() {
		return operator.toExpr();
	}
} public interface Constants {
	String EMPTY_STRING = "";

	String REG_WS = "\\s+";
	String WHITE_SPACE = " \t\n\r\f";

	// For each primitive type, we can safely use all values except the extreme ones (as defined by SAFETY_MARGIN)
	// so as to be able to use special values (for example, for representing +infinity and -infinity)
	int SAFETY_MARGIN = 10;
	long MIN_SAFE_BYTE = Byte.MIN_VALUE + SAFETY_MARGIN, MAX_SAFE_BYTE = Byte.MAX_VALUE - SAFETY_MARGIN;
	long MIN_SAFE_SHORT = Short.MIN_VALUE + SAFETY_MARGIN, MAX_SAFE_SHORT = Short.MAX_VALUE - SAFETY_MARGIN;
	long MIN_SAFE_INT = Integer.MIN_VALUE + SAFETY_MARGIN, MAX_SAFE_INT = Integer.MAX_VALUE - SAFETY_MARGIN;
	long MIN_SAFE_LONG = Long.MIN_VALUE + SAFETY_MARGIN, MAX_SAFE_LONG = Long.MAX_VALUE - SAFETY_MARGIN;
	BigInteger BIG_MIN_SAFE_LONG = BigInteger.valueOf(MIN_SAFE_LONG), BIG_MAX_SAFE_LONG = BigInteger.valueOf(MAX_SAFE_LONG);

	long MINUS_INFINITY = Long.MIN_VALUE;
	long PLUS_INFINITY = Long.MAX_VALUE;
	int MINUS_INFINITY_INT = Integer.MIN_VALUE;
	int PLUS_INFINITY_INT = Integer.MAX_VALUE;
	String MINUS_INFINITY_STRING = "-infinity";
	String PLUS_INFINITY_STRING = "+infinity";

	int ALL = Integer.MAX_VALUE;

	// We use the maximum value of each primitive type, minus 1, to denote STAR (related to the concept of short tuples)
	String STAR_SYMBOL = "*";

	byte STAR_BYTE = Byte.MAX_VALUE - 1;
	short STAR_SHORT = Short.MAX_VALUE - 1;
	int STAR_INT = Integer.MAX_VALUE - 1;
	long STAR_LONG = Long.MAX_VALUE - 1;
	int STAR = STAR_INT;

	public final String TIMES = "x";

	/** We use the minimum long value, plus 1, to denote that a value is outside bounds (e.g., of a domain) */
	long OUTSIDE_BOUNDS = Long.MIN_VALUE + 1;

	// Constants used for some first-level elements of the instances
	String INSTANCE = "instance";
	String VARIABLES = "variables";
	String VAR = "var";
	String ARRAY = "array";
	String DOMAIN = "domain";
	String REQUIRED = "required";
	String POSSIBLE = "possible";
	String CONSTRAINTS = "constraints";
	String BLOCK = "block";
	String GROUP = "group";
	String ARGS = "args";
	String OBJECTIVES = "objectives";
	String OBJECTIVE = "objective";
	String MINIMIZE = "minimize";
	String MAXIMIZE = "maximize";
	String SOFT = "soft";
	String ANNOTATIONS = "annotations";
	String DECISION = "decision";

	/** A regex for denoting delimiters used in lists (elements separated by commas and surrounded by parentheses) */
	String DELIMITER_LISTS = "\\s*\\)\\s*\\(\\s*|\\s*\\(\\s*|\\s*\\)\\s*";

	/** A regex for denoting delimiters used in sets (elements separated by a comma and surrounded by brace brackets) */
	String DELIMITER_SETS = "\\s*\\}\\s*\\{\\s*|\\s*\\{\\s*|\\s*\\}\\s*";

	/** A regex for denoting delimiters used in msets (elements separated by a comma and surrounded by double brace brackets) */
	String DELIMITER_MSETS = "\\s*\\}\\}\\s*\\{\\{\\s*|\\s*\\{\\{\\s*|\\s*\\}\\}\\s*";

	String[] KEYWORDS = { "neg", "abs", "add", "sub", "mul", "div", "mod", "sqr", "pow", "min", "max", "dist", "lt", "le", "ge", "gt", "ne", "eq", "set", "in",
			"not", "and", "or", "xor", "iff", "imp", "if", "card", "union", "inter", "diff", "sdiff", "hull", "djoint", "subset", "subseq", "supseq", "supset",
			"convex", "PI", "E", "fdiv", "fmod", "sqrt", "nroot", "exp", "ln", "log", "sin", "cos", "tan", "asin", "acos", "atan", "sinh", "cosh", "tanh",
			"others" };
} public static enum TypeAtt {
	format,
	type,
	id,
	CLASS, // upper-cased because a keyword
	note,
	as,
	size,
	violationMeasure,
	violationParameters,
	defaultCost,
	violationCost,
	cost,
	reifiedBy,
	hreifiedFrom,
	hreifiedTo,
	closed,
	FOR, // upper-cased because a keyword
	restriction,
	rank,
	startIndex,
	startRowIndex,
	startColIndex,
	zeroIgnored,
	CASE, // upper-cased because a keyword
	order,
	circular,
	offset,
	collect,
	covered,
	violable,
	lb,
	ub,
	combination;
	// unclean, // used for tuples of table constraints
	// starred; // used for tuples of table constraints

	/**
	 * Returns true iff the element has a (full or half) reification nature.
	 */
	public boolean isReifying() {
		return this == reifiedBy || this == hreifiedFrom || this == hreifiedTo;
	}

	/**
	 * Returns the constant that corresponds to the specified string (we need this method to manage the special
	 * constants FOR and CASE).
	 */
	public static TypeAtt valOf(String s) {
		return s.equals("class") ? CLASS : s.equals("for") ? FOR : s.equals("case") ? TypeAtt.CASE : valueOf(s);
	}
} public static enum TypeChild {
	list,
	set,
	mset,
	matrix,
	function,
	supports,
	conflicts,
	except,
	value,
	values,
	total,
	coeffs,
	condition,
	cost,
	operator,
	number,
	transitions,
	start,
	FINAL, // upper-cased because a keyword
	terminal,
	rules,
	index,
	mapping,
	occurs,
	rowOccurs,
	colOccurs,
	widths,
	patterns,
	origins,
	lengths,
	ends,
	heights,
	machines,
	conditions,
	sizes,
	weights,
	profits,
	limit,
	size,
	root,
	image,
	graph,
	row;
} public static enum TypeConditionOperatorRel {
	LT, LE, GE, GT, NE, EQ;

	/**
	 * Returns the operator that is the reverse operator of this operator (no change for NE and EQ).
	 */
	public TypeConditionOperatorRel arithmeticInversion() {
		return this == LT ? GT : this == LE ? GE : this == GE ? LE : this == GT ? LT : this; // no change for NE and
																								// EQ
	}

	/**
	 * Returns true iff this operator evaluates to true when given the two specified operands.
	 */
	public boolean isValidFor(long v1, long v2) {
		return this == LT ? v1 < v2 : this == LE ? v1 <= v2 : this == GE ? v1 >= v2 : this == GT ? v1 > v2 : this == NE ? v1 != v2 : v1 == v2;
	}

	public static TypeConditionOperatorRel valueFor(String s) {
		Utilities.control(s.equals("<") || s.equals("<=") || s.equals(">") || s.equals(">=") || s.equals("=") || s.equals("!="), "bad argument");
		return s.equals("<") ? LT : s.equals("<=") ? LE : s.equals(">") ? GT : s.equals(">=") ? GE : s.equals("=") ? EQ : NE;
	}

	public boolean oneOf(TypeConditionOperatorRel... types) {
		return Stream.of(types).anyMatch(t -> t == this);
	}

	/**
	 * The type from {@code TypeExpr} with the same name as this type, if it exists, {@code null} otherwise.
	 * 
	 * @return The type from {@code TypeExpr} with the same name as this type, if it exists, {@code null} otherwise
	 */
	public TypeExpr toExpr() {
		return this == LT ? TypeExpr.LT
				: this == LE ? TypeExpr.LE
						: this == GE ? TypeExpr.GE : this == GT ? TypeExpr.GT : this == EQ ? TypeExpr.EQ : this == NE ? TypeExpr.NE : null;
	}

} public static enum TypeCtr {
	extension,
	intension,
	regular,
	grammar,
	mdd,
	allDifferent,
	allEqual,
	allDistant,
	ordered,
	lex,
	allIncomparable,
	sum,
	count,
	nValues,
	cardinality,
	balance,
	spread,
	deviation,
	sumCosts,
	stretch,
	noOverlap,
	cumulative,
	binPacking,
	knapsack,
	networkFlow,
	circuit,
	nCircuits,
	path,
	nPaths,
	tree,
	nTrees,
	arbo,
	nArbos,
	nCliques,
	clause,
	instantiation,
	allIntersecting,
	range,
	roots,
	partition,
	minimum,
	maximum,
	element,
	channel,
	permutation,
	precedence,
	and,
	or,
	not,
	iff, // future meta-constraint to be taken into account
	ifThen,
	ifThenElse,
	slide,
	seqbin,
	smart;

	/** Returns true if the element has a sliding nature. */
	public boolean isSliding() {
		return this == slide || this == seqbin;
	}

	/** Returns true if the element has a "direct" logical nature. */
	public boolean isLogical() {
		return this == and || this == or || this == not || this == iff;
	}

	/** Returns true if the element has a logical nature corresponding to an if-based control structure. */
	public boolean isControl() {
		return this == ifThen || this == ifThenElse;
	}

	/** Returns true if the element corresponds to a meta-constraint. */
	public boolean isMeta() {
		return isSliding() || isLogical() || isControl();
	}

	/**
	 * Returns {@code true} iff this type is one of the specified types.
	 * 
	 * @param types
	 *            a sequence of types
	 * @return {@code true} iff this type is one of the specified types
	 */
	public boolean oneOf(TypeCtr... types) {
		return Stream.of(types).anyMatch(t -> t == this);
	}
} public static enum TypeExpr {
	NEG(1),
	ABS(1),
	SQR(1),
	ADD(2, Integer.MAX_VALUE),
	SUB(2),
	MUL(2, Integer.MAX_VALUE),
	DIV(2),
	MOD(2),
	POW(2),
	DIST(2),
	MIN(2, Integer.MAX_VALUE),
	MAX(2, Integer.MAX_VALUE),
	LT(2),
	LE(2),
	GE(2),
	GT(2),
	NE(2, Integer.MAX_VALUE),
	EQ(2, Integer.MAX_VALUE),
	SET(0, Integer.MAX_VALUE),
	IN(2),
	NOTIN(2),
	NOT(1),
	AND(2, Integer.MAX_VALUE),
	OR(2, Integer.MAX_VALUE),
	XOR(2, Integer.MAX_VALUE),
	IFF(2, Integer.MAX_VALUE),
	IMP(2),
	IF(3),
	CARD(1),
	UNION(2, Integer.MAX_VALUE),
	INTER(2, Integer.MAX_VALUE),
	DIFF(2),
	SDIFF(2, Integer.MAX_VALUE),
	HULL(1),
	DJOINT(2),
	SUBSET(2),
	SUBSEQ(2),
	SUPSEQ(2),
	SUPSET(2),
	CONVEX(1),
	FDIV(2),
	FMOD(2),
	SQRT(1),
	NROOT(2),
	EXP(1),
	LN(1),
	LOG(2),
	SIN(1),
	COS(1),
	TAN(1),
	ASIN(1),
	ACOS(1),
	ATAN(1),
	SINH(1),
	COSH(1),
	TANH(1),
	VAR(0),
	PAR(0),
	LONG(0),
	RATIONAL(0),
	DECIMAL(0),
	SYMBOL(0),
	SPECIAL(0, Integer.MAX_VALUE); // SPECIAL is a virtual type, useful when managing abstract trees

	/**
	 * The name of this type in lower-case.
	 */
	public final String lcname;

	/**
	 * The minimum arity (number of sons) for a node of this type.
	 */
	public final int arityMin;

	/**
	 * The maximum arity (number of sons) for a node of this type.
	 */
	public final int arityMax;

	/** Builds a constant, while specifying its minimum and maximum arity (number of sons). */
	private TypeExpr(int arityMin, int arityMax) {
		this.arityMin = arityMin;
		this.arityMax = arityMax;
		this.lcname = name().toLowerCase();
	}

	/** Builds a constant, while specifying its arity (number of sons). */
	private TypeExpr(int arity) {
		this(arity, arity);
	}

	/**
	 * Returns {@code true} iff this type is one of the specified types.
	 * 
	 * @param types
	 *            a sequence of types
	 * @return {@code true} iff this type is one of the specified types
	 */
	public boolean oneOf(TypeExpr... types) {
		return Stream.of(types).anyMatch(t -> t == this);
	}

	/**
	 * Returns {@code true} iff this type is not one of the specified types.
	 * 
	 * @param types
	 *            a sequence of types
	 * @return {@code true} iff this type is not one of the specified types
	 */
	public boolean notOneOf(TypeExpr... types) {
		return Stream.of(types).noneMatch(t -> t == this);
	}

	/**
	 * Returns {@code true} iff this type denotes an operator that is commutative (and also associative when it is a
	 * non-binary operator).
	 * 
	 * @return {@code true} iff this type denotes an operator that is symmetric
	 */
	public boolean isSymmetricOperator() {
		return oneOf(ADD, MUL, MIN, MAX, DIST, NE, EQ, SET, AND, OR, XOR, IFF, UNION, INTER, DJOINT);
	}

	/**
	 * Returns {@code true} iff this type denotes a binary non-symmetric relational operator (i.e.,
	 * {@code LT, LE, GE and GT}).
	 * 
	 * @return {@code true} iff this type denotes a binary non-symmetric relational
	 */
	public boolean isUnsymmetricRelationalOperator() {
		return oneOf(LT, LE, GE, GT);
	}

	/**
	 * Returns {@code true} iff this type denotes a relational operator (i.e., {@code LT, LE, GE, GT, EQ and NE}).
	 * 
	 * @return {@code true} iff this type denotes a relational operator
	 */
	public boolean isRelationalOperator() {
		return isUnsymmetricRelationalOperator() || oneOf(NE, EQ);
	}

	/**
	 * Returns {@code true} iff this type denotes a unary arithmetic or logic operator (i.e.,
	 * {@code ABS, NEG, SQR, and NOT}).
	 * 
	 * @return {@code true} iff this type denotes a unary arithmetic or logic operator
	 */
	public boolean isUnaryArithmeticOrLogicOperator() {
		return oneOf(ABS, NEG, SQR, NOT);
	}

	/**
	 * Returns {@code true} iff this type denotes a (non-unary) arithmetic operator (i.e.,
	 * {@code ADD, SUB, MUL, DIV, MOD, POW and DIST}).
	 * 
	 * @return {@code true} iff this type denotes a (non-unary) arithmetic operator
	 */
	public boolean isArithmeticOperator() {
		return oneOf(ADD, SUB, MUL, DIV, MOD, POW, DIST);
	}

	/**
	 * Returns {@code true} iff this type denotes a (non-unary) logical operator (i.e.,
	 * {@code AND, OR, XOR, IFF, and IMP}).
	 * 
	 * @return {@code true} iff this type denotes a (non-unary) logical operator
	 */
	public boolean isLogicalOperator() {
		return oneOf(AND, OR, XOR, IFF, IMP);
	}

	/**
	 * Returns {@code true} iff this type denotes an operator that evaluates to 0/1 (false/true).
	 * 
	 * @return {@code true} iff this type denotes an operator that evaluates to 0/1 (false/true)
	 */
	public boolean isPredicateOperator() {
		return isRelationalOperator() || isLogicalOperator() || oneOf(NOT, IN, NOTIN);
	}

	/**
	 * Returns {@code true} iff this type denotes an operator that behaves like identity if only one operand was
	 * given.
	 * 
	 * @return @code true} iff this type denotes an operator that behaves like identity for only one operand
	 */
	public boolean isIdentityWhenOneOperand() {
		return oneOf(ADD, MUL, MIN, MAX, EQ, AND, OR, XOR, IFF);
	}

	/**
	 * Returns the type denoting the arithmetic inversion of this type, if this type denotes a relational operator,
	 * {@code null} otherwise. The arithmetic inversion is not obtained by applying a logical negation but a
	 * multiplication by -1. For example, the arithmetic inversion of {@code LT} is {@code GT} (and not {@code GE}).
	 * Also, the arithmetic inversion of {@code EQ} is {@code EQ}.
	 * 
	 * @return the type denoting the arithmetic inversion of this type, if this type denotes a relational operator,
	 *         {@code null} otherwise
	 */
	public TypeExpr arithmeticInversion() {
		return this == LT ? GT : this == LE ? GE : this == GE ? LE : this == GT ? LT : this == NE ? NE : this == EQ ? EQ : null;
	}

	/**
	 * Returns the type denoting the logical inversion of this type, if this type denotes a a Boolean operator (that
	 * can be inverted when considering the current pool of constants), {@code null} otherwise. The logical
	 * inversion is different from the arithmetic inversion. For example, the logical inversion of {@code LT} is
	 * {@code GE} (and not {@code GT}). Also, the logical inversion of {@code EQ} is {@code NE}.
	 * 
	 * @return the type denoting the logical inversion of this type, if this type denotes a a Boolean operator that
	 *         can be inverted, {@code null} otherwise
	 */
	public TypeExpr logicalInversion() {
		return this == LT ? GE
				: this == LE ? GT
						: this == GE ? LT
								: this == GT ? LE
										: this == NE ? EQ
												: this == EQ ? NE
														: this == IN ? NOTIN
																: this == NOTIN ? IN
																		: this == SUBSET ? SUPSEQ
																				: this == SUBSEQ ? SUPSET
																						: this == SUPSEQ ? SUBSET : this == SUPSET ? SUBSEQ : null;
	}

	/**
	 * Returns {@code true} iff this type denotes an operator that can be logically inverted, {@code null}
	 * otherwise.
	 * 
	 * @return {@code true} iff this type denotes an operator that can be logically inverted, {@code null} otherwise
	 */
	public boolean isLogicallyInvertible() {
		return logicalInversion() != null;
	}

	/**
	 * The type from {@code TypeConditionOperatorRel} with the same name as this type, if it exists, {@code null}
	 * otherwise.
	 * 
	 * @return The type from {@code TypeConditionOperatorRel} with the same name as this type, if it exists,
	 *         {@code null} otherwise
	 */
	public TypeConditionOperatorRel toRelop() {
		return this == LT ? TypeConditionOperatorRel.LT
				: this == LE ? TypeConditionOperatorRel.LE
						: this == GE ? TypeConditionOperatorRel.GE
								: this == GT ? TypeConditionOperatorRel.GT
										: this == EQ ? TypeConditionOperatorRel.EQ : this == NE ? TypeConditionOperatorRel.NE : null;
	}

	/**
	 * The type from {@code TypeConditionOperatorSet} with the same name as this type, if it exists, {@code null}
	 * otherwise.
	 * 
	 * @return The type from {@code TypeConditionOperatorSet} with the same name as this type, if it exists,
	 *         {@code null} otherwise
	 */
	public TypeConditionOperatorSet toSetop() {
		return this == IN ? TypeConditionOperatorSet.IN : this == NOTIN ? TypeConditionOperatorSet.NOTIN : null;
	}

	/**
	 * The type from {@code TypeArithmeticOperator} with the same name as this type, if it exists, {@code null}
	 * otherwise.
	 * 
	 * @return The type from {@code TypeArithmeticOperator} with the same name as this type, if it exists,
	 *         {@code null} otherwise
	 */
	public TypeArithmeticOperator toAriop() {
		return this == ADD ? TypeArithmeticOperator.ADD
				: this == SUB ? TypeArithmeticOperator.SUB
						: this == MUL ? TypeArithmeticOperator.MUL
								: this == DIV ? TypeArithmeticOperator.DIV
										: this == MOD ? TypeArithmeticOperator.MOD
												: this == POW ? TypeArithmeticOperator.POW : this == DIST ? TypeArithmeticOperator.DIST : null;
	}

	/**
	 * The type from {@code TypeUnaryArithmeticOperator} with the same name as this type, if it exists, {@code null}
	 * otherwise.
	 * 
	 * @return The type from {@code TypeUnaryArithmeticOperator} with the same name as this type, if it exists,
	 *         {@code null} otherwise
	 */
	public TypeUnaryArithmeticOperator toUnalop() {
		return this == ABS ? TypeUnaryArithmeticOperator.ABS
				: this == NEG ? TypeUnaryArithmeticOperator.NEG
						: this == SQR ? TypeUnaryArithmeticOperator.SQR : this == NOT ? TypeUnaryArithmeticOperator.NOT : null;
	}

	/**
	 * The type from {@code TypeLogicalOperator} with the same name as this type, if it exists, {@code null}
	 * otherwise.
	 * 
	 * @return The type from {@code TypeLogicalOperator} with the same name as this type, if it exists, {@code null}
	 *         otherwise
	 */
	public TypeLogicalOperator toLogop() {
		return this == AND ? TypeLogicalOperator.AND
				: this == OR ? TypeLogicalOperator.OR
						: this == XOR ? TypeLogicalOperator.XOR : this == IFF ? TypeLogicalOperator.IFF : this == IMP ? TypeLogicalOperator.IMP : null;
	}

} public static enum TypeOperator {
	LT, LE, GE, GT, SUBSET, SUBSEQ, SUPSEQ, SUPSET;

	public static TypeOperator valOf(String s) {
		return TypeOperator.valueOf(s.trim().toUpperCase());
	}

	/**
	 * Returns the corresponding specialized TypeOperatorRel for this constant, or null if this constant is a set
	 * operator,.
	 */
	public TypeOperatorRel toRel() {
		return isSet() ? null : this == LT ? TypeOperatorRel.LT : this == LE ? TypeOperatorRel.LE : this == GE ? TypeOperatorRel.GE : TypeOperatorRel.GT;
	}

	/** Returns true iff the constant corresponds to a set operator. */
	public boolean isSet() {
		return this == SUBSET || this == SUBSEQ || this == SUPSEQ || this == SUPSET;
	}

} public static enum TypeOperatorRel {
	LT, LE, GE, GT;

	/**
	 * Returns the operator that is the reverse operator of this operator (no change for NE and EQ).
	 */
	public TypeOperatorRel arithmeticInversion() {
		return this == LT ? GT : this == LE ? GE : this == GE ? LE : LT;
	}

	/**
	 * Returns true iff this operator evaluates to true when given the two specified operands.
	 */
	public boolean isValidFor(long v1, long v2) {
		return this == LT ? v1 < v2 : this == LE ? v1 <= v2 : this == GE ? v1 >= v2 : v1 > v2;
	}

	/**
	 * The type from {@code TypeExpr} with the same name as this type.
	 * 
	 * @return The type from {@code TypeExpr} with the same name as this type
	 */
	public TypeExpr toExpr() {
		return this == LT ? TypeExpr.LT : this == LE ? TypeExpr.LE : this == GE ? TypeExpr.GE : TypeExpr.GT;
	}

	public TypeConditionOperatorRel toConditionOperator() {
		return this == LT ? TypeConditionOperatorRel.LT
				: this == LE ? TypeConditionOperatorRel.LE : this == GE ? TypeConditionOperatorRel.GE : TypeConditionOperatorRel.GT;
	}
} public static enum TypeRank {
	FIRST, LAST, ANY;
} public class Utilities {

	public static final Comparator<int[]> lexComparatorInt = (t1, t2) -> {
		for (int i = 0; i < t1.length; i++)
			if (t1[i] < t2[i])
				return -1;
			else if (t1[i] > t2[i])
				return +1;
		return 0;
	};

	public static final Comparator<String[]> lexComparatorString = (t1, t2) -> {
		for (int i = 0; i < t1.length; i++) {
			int res = t1[i].compareTo(t2[i]);
			if (res != 0)
				return res;
		}
		return 0;
	};

	public static <T> T[] buildArray(Class<?> cl, int length) {
		return (T[]) Array.newInstance(cl, length);
	}

	public static <T> T[][] buildArray(Class<?> cl, int length1, int length2) {
		return (T[][]) Array.newInstance(cl, length1, length2);
	}

	public static Object firstNonNull(Object array) {
		if (array != null && array.getClass().isArray())
			return IntStream.range(0, Array.getLength(array)).mapToObj(i -> firstNonNull(Array.get(array, i))).filter(o -> o != null).findFirst().orElse(null);
		return array;
	}

	/**
	 * Builds a one-dimensional array of T with the objects of the specified list. If the list does not contain any
	 * object other than null, null is returned.
	 */
	public static <T> T[] convert(Collection<T> list) {
		Object firstObject = list.stream().filter(o -> o != null).findFirst().orElse(null);
		if (firstObject == null)
			return null;
		T[] ts = buildArray(firstObject.getClass(), list.size());
		int i = 0;
		for (T x : list)
			ts[i++] = x;
		return ts;
	}

	/**
	 * Builds a one-dimensional array of T with the objects of the specified stream. If the stream does not contain any
	 * object other than null, null is returned.
	 */
	public static <T> T[] convert(Stream<T> stream) {
		return convert(stream.collect(Collectors.toList()));
	}

	public static <T> T[] convert(Object[] t) {
		Object firstObject = Stream.of(t).filter(o -> o != null).findFirst().orElse(null);
		Class<?> clazz = firstObject == null ? null
				: Stream.of(t).noneMatch(o -> o != null && o.getClass() != firstObject.getClass()) ? firstObject.getClass() : null;
		if (clazz == null)
			return null; // null is returned if the array has only null or elements of several types
		T[] ts = buildArray(firstObject.getClass(), t.length);
		int i = 0;
		for (Object x : t)
			ts[i++] = (T) x;
		return ts;
	}

	public static <T> T[][] convert(Object[][] t) {
		control(isRegular(t), " pb");
		// other controls to add
		T[][] m = buildArray(t[0][0].getClass(), t.length, t[0].length);
		for (int i = 0; i < t.length; i++)
			for (int j = 0; j < t[i].length; j++)
				m[i][j] = (T) t[i][j];
		return m;
	}

	public static Object[] specificArrayFrom(List<Object> list) {
		Object firstObject = list.stream().filter(o -> o != null).findFirst().orElse(null);
		Class<?> clazz = firstObject == null ? null
				: list.stream().noneMatch(o -> o != null && o.getClass() != firstObject.getClass()) ? firstObject.getClass() : null;
		return clazz == null ? list.toArray() : list.toArray((Object[]) Array.newInstance(clazz, list.size()));
	}

	public static Object[][] specificArray2DFrom(List<Object[]> list) {
		Class<?> clazz = list.stream().noneMatch(o -> o.getClass() != list.get(0).getClass()) ? list.get(0).getClass() : null;
		return clazz == null ? list.toArray(new Object[0][]) : list.toArray((Object[][]) Array.newInstance(clazz, list.size()));
	}

	private static <T> List<T> collectRec(Class<T> clazz, List<T> list, Object src) {
		if (src != null) {
			if (src instanceof Collection)
				collectRec(clazz, list, ((Collection<?>) src).stream());
			else if (src instanceof Stream)
				((Stream<?>) src).forEach(o -> collectRec(clazz, list, o));
			else if (src.getClass().isArray())
				IntStream.range(0, Array.getLength(src)).forEach(i -> collectRec(clazz, list, Array.get(src, i)));
			else if (clazz.isAssignableFrom(src.getClass()))
				list.add(clazz.cast(src));
			else if (src instanceof IntStream)
				((IntStream) src).forEach(o -> collectRec(clazz, list, o));
			else if (src.getClass() == Range.class)
				collectRec(clazz, list, ((Range) src).toArray()); // in order to deal with clazz being Integer.class
		}
		return list;
	}

	/**
	 * Returns a 1-dimensional array of objects of the specified type after collecting any object of this type being
	 * present in the specified objects. The specified objects can be stream (and IntStream), collections and arrays.
	 * The collecting process is made recursively.
	 * 
	 * @param clazz
	 *            the class of the objects to be collected
	 * @param src
	 *            the objects where to collect the objects
	 * @return a 1-dimensional array of objects of the specified type after collecting any object of this type being
	 *         present in the specified objects
	 */
	public static <T> T[] collect(Class<T> clazz, Object... src) {
		List<T> list = new ArrayList<>();
		Stream.of(src).forEach(o -> collectRec(clazz, list, o));
		return convert(list.stream().collect(Collectors.toList()));
	}

	/**
	 * Builds a 1-dimensional array of integers (int) from the specified sequence of parameters. Each parameter can be
	 * an integer, a Range, an array, a stream, a collection, etc. All integers are collected and concatenated to form a
	 * 1-dimensional array.
	 *
	 * @param src
	 *            the objects where to collect the integers
	 * @return a 1-dimensional array of integers after collecting any encountered integer in the specified objects
	 */
	public static int[] collectInt(Object... src) {
		Integer[] t = collect(Integer.class, src);
		return t == null ? new int[0] : Stream.of(t).filter(i -> i != null).mapToInt(i -> i).toArray();
	}

	public static boolean isNumeric(String token) {
		return token.matches("-?\\d+(\\.\\d+)?"); // match a number with optional '-' and decimal.
	}

	public static boolean isNumericInterval(String token) {
		return token.matches("-?\\d+\\.\\.-?\\d+");
	}

	public static int[] splitToInts(String s, String regex) {
		return Arrays.stream(s.trim().split(regex)).filter(tok -> tok.length() > 0).mapToInt(tok -> Integer.parseInt(tok)).toArray();
	}

	public static int[] splitToInts(String s) {
		return splitToInts(s, Constants.REG_WS);
	}

	public static int splitToInt(String s, String regex) {
		int[] t = splitToInts(s, regex);
		control(t.length > 0, "Not possible to extract an int from this call");
		return t[0];
	}

	public static int[] wordAsIntArray(String s) {
		assert s.chars().allMatch(c -> ('a' <= c && c <= 'z') || ('A' <= c && c <= 'Z'));
		int[] t = new int[s.length()]; // We don't use streams here for efficiency reasons (when dealing with large sets
										// of words)
		for (int i = 0; i < s.length(); i++)
			t[i] = s.charAt(i) - (Character.isUpperCase(s.charAt(i)) ? 'A' : 'a');
		return t;
	}

	public static Boolean toBoolean(String s) {
		s = s.toLowerCase();
		if (s.equals("yes") || s.equals("y") || s.equals("true") || s.equals("t") || s.equals("1"))
			return Boolean.TRUE;
		if (s.equals("no") || s.equals("n") || s.equals("false") || s.equals("f") || s.equals("0"))
			return Boolean.FALSE;
		return null;
	}

	public static boolean isInteger(String token) {
		try {
			Integer.parseInt(token);
			return true;
		} catch (NumberFormatException e) {
			return false;
		}
	}

	public static boolean isLong(String token) {
		try {
			Long.parseLong(token);
			return true;
		} catch (NumberFormatException e) {
			return false;
		}
	}

	public static Integer toInteger(String token, Predicate<Integer> p) {
		try {
			Integer i = Integer.parseInt(token);
			Utilities.control(p == null || p.test(i), "Value " + i + " not accepted by " + p);
			return i;
		} catch (RuntimeException e) {
			return null;
		}
	}

	public static Integer toInteger(String token) {
		return toInteger(token, null);
	}

	public static int[] toIntegers(String[] tokens) {
		if (tokens == null || tokens.length == 0)
			return null;
		return Stream.of(tokens).map(tok -> toInteger(tok)).mapToInt(i -> i).toArray();
	}

	public static Double toDouble(String token, Predicate<Double> p) {
		try {
			Double d = Double.parseDouble(token);
			Utilities.control(p == null || p.test(d), "Value " + d + " not accepted by " + p);
			return d;
		} catch (RuntimeException e) {
			return null;
		}
	}

	public static double toDouble(String token) {
		return toDouble(token, null);
	}

	public static BigInteger powerBig(long a, int b) {
		return BigInteger.valueOf(a).pow(b);
	}

	public static int power(long a, int b) {
		return powerBig(a, b).intValueExact();
	}

	private static BigInteger recursiveFactorial(long start, long n) {
		long i;
		if (n <= 16) {
			BigInteger r = BigInteger.valueOf(start);
			for (i = start + 1; i < start + n; i++)
				r = r.multiply(BigInteger.valueOf(i));
			return r;
		}
		i = n / 2;
		return recursiveFactorial(start, i).multiply(recursiveFactorial(start + i, n - i));
	}

	public static BigInteger factorialBig(int n) {
		return recursiveFactorial(1, n);
	}

	public static int factorial(int n) {
		return factorialBig(n).intValueExact();
	}

	public static BigInteger binomialBig(int n, int k) {
		if (k < 0 || n < k)
			return BigInteger.ZERO;
		if (k > n - k)
			k = n - k;
		BigInteger i = BigInteger.ONE;
		for (int v = 0; v < k; v++)
			i = i.multiply(BigInteger.valueOf(n - v)).divide(BigInteger.valueOf(v + 1));
		return i;
	}

	public static int binomial(int n, int k) {
		return binomialBig(n, k).intValueExact();
	}

	public static BigInteger nArrangementsFor(int[] nValues) {
		return IntStream.of(nValues).mapToObj(v -> BigInteger.valueOf(v)).reduce(BigInteger.ONE, (acc, v) -> acc.multiply(v));
	}

	public static boolean contains(int[] tab, int v, int from, int to) {
		return IntStream.rangeClosed(from, to).anyMatch(i -> tab[i] == v);
	}

	public static boolean contains(int[] tab, int v) {
		return contains(tab, v, 0, tab.length - 1);
	}

	public static int indexOf(String s, String... t) {
		return IntStream.range(0, t.length).filter(i -> t[i].equals(s)).findFirst().orElse(-1);
	}

	public static int indexOf(String s, List<Object> list) {
		return IntStream.range(0, list.size()).filter(i -> list.get(i).equals(s)).findFirst().orElse(-1);
	}

	public static int indexOf(int value, int[] t) {
		for (int i = 0; i < t.length; i++)
			if (value == t[i])
				return i;
		return -1;
		// return IntStream.range(0, t.length).filter(i -> t[i] == value).findFirst().orElse(-1);
	}

	public static int indexOf(Object value, Object[] t) {
		return IntStream.range(0, t.length).filter(i -> t[i] == value).findFirst().orElse(-1);
	}

	/**
	 * Returns true is the array is regular and matches exactly the specified size. For example, if size is [5,4] then
	 * the specified array must be a 2-dimensional array of 5 x 4 squares.
	 */
	public static boolean hasSize(Object array, int... size) {
		boolean b1 = array != null && array.getClass().isArray(), b2 = size.length > 0;
		if (!b1 && !b2)
			return true;
		if (b1 && !b2 || !b1 && b2 || Array.getLength(array) != size[0])
			return false;
		return IntStream.range(0, size[0]).noneMatch(i -> !hasSize(Array.get(array, i), Arrays.stream(size).skip(1).toArray()));
	}

	/**
	 * Returns true is the array is regular, that is to say has the form of a rectangle for a 2-dimensional array, a
	 * cube for a 3-dimensional array... For example, if the specified array is a 2-dimensional array of 5 x 4 squares,
	 * then it is regular. But it has 3 squares for the first row, and 4 squares for the second row, then it is not
	 * regular.
	 */
	public static boolean isRegular(Object array) {
		List<Integer> list = new ArrayList<>();
		for (Object a = array; a != null && a.getClass().isArray(); a = Array.getLength(a) == 0 ? null : Array.get(a, 0))
			list.add(Array.getLength(a));
		return hasSize(array, list.stream().mapToInt(i -> i).toArray());
	}

	/**
	 * Method that controls that the specified condition is verified. If it is not the case, a message is displayed and
	 * the program is stopped.
	 */
	public static Object control(boolean condition, String message) {
		if (!condition) {
			System.out.println("\n\nFatal Error: " + message);
			throw new RuntimeException();
			// System.exit(1);
		}
		return null;
	}

	public static Object exit(String message) {
		return control(false, message);
	}

	/**
	 * Checks if the specified {@code Runnable} object raises an {@code ArithmeticException} object, when run. The value
	 * {@code true} is returned iff no such exception is raised.
	 * 
	 * @param r
	 *            a {@code Runnable} object to be run
	 * @return {@code true} iff no {@code ArithmeticException} is raised when running the specified code
	 */
	public static boolean checkSafeArithmeticOperation(Runnable r) {
		try {
			r.run();
			return true;
		} catch (ArithmeticException e) {
			return false;
		}
	}

	/**
	 * Method that parses the specified string as a long integer. If the value is too small or too big, an exception is
	 * raised. The specified boolean allows us to indicate if some special values (such as +infinity) must be checked.
	 */
	public static Long safeLong(String s, boolean checkSpecialValues) {
		if (checkSpecialValues) {
			if (s.equals(PLUS_INFINITY_STRING))
				return PLUS_INFINITY;
			if (s.equals(MINUS_INFINITY_STRING))
				return MINUS_INFINITY;
		}
		if (s.length() > 18) { // 18 because MAX_LONG and MIN_LONG are composed of at most 19 characters
			BigInteger big = new BigInteger(s);
			control(big.compareTo(BIG_MIN_SAFE_LONG) >= 0 && big.compareTo(BIG_MAX_SAFE_LONG) <= 0, "Too small or big value for this parser : " + s);
			return big.longValue();
		} else
			return Long.parseLong(s);
	}

	/**
	 * Method that parses the specified string as a long integer. If the value is too small or too big, an exception is
	 * raised.
	 */
	public static Long safeLong(String s) {
		return safeLong(s, false);
	}

	public static boolean isSafeInt(long l, boolean useMargin) {
		return (useMargin ? Constants.MIN_SAFE_INT : Integer.MIN_VALUE) <= l && l <= (useMargin ? Constants.MAX_SAFE_INT : Integer.MAX_VALUE);
	}

	public static boolean isSafeInt(long l) {
		return isSafeInt(l, true);
	}

	/**
	 * Converts the specified long number to int if it is safe to do it. When the specified boolean is set to true, we
	 * control that it is safe according to the constants MIN_SAFE_INT and MAX_SAFE_INT.
	 */
	public static int safeInt(Long l, boolean useMargin) {
		control(isSafeInt(l, useMargin), "Too big integer value " + l);
		return l.intValue();
		// return safeLong2Int(number.longValue(), useMargin);
	}

	/**
	 * Converts the specified long to int if it is safe to do it. We control that it is safe according to the constants
	 * MIN_SAFE_INT and MAX_SAFE_INT.
	 */
	public static int safeInt(Long l) {
		return safeInt(l, true);
	}

	/**
	 * Converts the specified long to int if it is safe to do it. Note that VAL_MINUS_INFINITY will be translated to
	 * VAL_MINUS_INFINITY_INT and that VAL_PLUS_INFINITY will be translated to VAL_PLUS_INFINITY_INT . We control that
	 * it is safe according to the constants MIN_SAFE_INT and MAX_SAFE_INT.
	 */
	public static int safeIntWhileHandlingInfinity(long l) {
		if (l == Constants.MINUS_INFINITY)
			return Constants.MINUS_INFINITY_INT;
		if (l == Constants.PLUS_INFINITY)
			return Constants.PLUS_INFINITY_INT;
		return safeInt(l);
	}

	public static <T> T[] swap(T[] t, int i, int j) {
		T tmp = t[i];
		t[i] = t[j];
		t[j] = tmp;
		return t;
	}

	/** Method that joins the elements of the specified array, using the specified delimiter to separate them. */
	public static String join(Object array, String delimiter) {
		StringBuilder sb = new StringBuilder();
		for (int i = 0, length = Array.getLength(array); i < length; i++) {
			Object item = Array.get(array, i);
			if (item != null && item.getClass().isArray())
				sb.append("[").append(join(item, delimiter)).append("]");
			else
				sb.append(item != null ? item.toString() : "null").append(i < length - 1 ? delimiter : "");
		}
		return sb.toString();
	}

	/** Method that joins the elements of the specified array, using a white-space as delimiter. */
	public static String join(Object array) {
		return join(array, " ");
	}

	public static String join(Collection<? extends Object> c) {
		return join(c.toArray());
	}

	/** Method that joins the elements of the specified map, using the specified separator and delimiter. */
	public static <K, V> String join(Map<K, V> m, String separator, String delimiter) {
		return m.entrySet().stream().map(e -> e.getKey() + separator + e.getValue()).reduce("", (n, p) -> n + (n.length() == 0 ? "" : delimiter) + p);
	}

	/**
	 * Method that joins the elements of the specified two-dimensional array, using the specified separator and
	 * delimiter.
	 */
	public static String join(Object[][] m, String separator, String delimiter) {
		return Arrays.stream(m).map(t -> join(t, delimiter)).reduce("", (n, p) -> n + (n.length() == 0 ? "" : separator) + p);
	}

	public static String join(int[][] m, String separator, String delimiter) {
		return Arrays.stream(m).map(t -> join(t, delimiter)).reduce("", (n, p) -> n + (n.length() == 0 ? "" : separator) + p);
	}

	/**
	 * Returns the specified string in camel case form (with the first letter of the first word in lower case).
	 */
	public static String toCamelCase(String s) {
		String[] words = s.split("_");
		return IntStream.range(0, words.length)
				.mapToObj(i -> i == 0 ? words[i].toLowerCase() : words[i].substring(0, 1).toUpperCase() + words[i].substring(1).toLowerCase())
				.collect(Collectors.joining());
	}

	/**
	 * Returns the specified string in kebab case form.
	 */
	public static String toKebabCase(String s) {
		String[] words = s.split("_");
		return Stream.of(words).map(w -> w.toLowerCase()).collect(Collectors.joining("-"));
	}

	/** Method for converting an array into a string. */
	public static String arrayToString(Object array, final char LEFT, final char RIGHT, final String SEP) {
		assert array.getClass().isArray();

		if (array instanceof boolean[])
			return Arrays.toString((boolean[]) array);
		if (array instanceof byte[])
			return Arrays.toString((byte[]) array);
		if (array instanceof short[])
			return Arrays.toString((short[]) array);
		if (array instanceof int[])
			return Arrays.toString((int[]) array);
		if (array instanceof long[])
			return Arrays.toString((long[]) array);
		if (array instanceof String[])
			return LEFT + String.join(SEP, (String[]) array) + RIGHT;
		if (array instanceof IVar[])
			return LEFT + String.join(SEP, Stream.of((IVar[]) array).map(x -> x.toString()).toArray(String[]::new)) + RIGHT;

		if (array instanceof boolean[][])
			return LEFT + String.join(SEP, Stream.of((boolean[][]) array).map(t -> arrayToString(t, LEFT, RIGHT, SEP)).toArray(String[]::new)) + RIGHT;
		if (array instanceof byte[][])
			return LEFT + String.join(SEP, Stream.of((byte[][]) array).map(t -> arrayToString(t, LEFT, RIGHT, SEP)).toArray(String[]::new)) + RIGHT;
		if (array instanceof short[][])
			return LEFT + String.join(SEP, Stream.of((short[][]) array).map(t -> arrayToString(t, LEFT, RIGHT, SEP)).toArray(String[]::new)) + RIGHT;
		if (array instanceof int[][])
			return LEFT + String.join(SEP, Stream.of((int[][]) array).map(t -> arrayToString(t, LEFT, RIGHT, SEP)).toArray(String[]::new)) + RIGHT;
		if (array instanceof long[][])
			return LEFT + String.join(SEP, Stream.of((long[][]) array).map(t -> arrayToString(t, LEFT, RIGHT, SEP)).toArray(String[]::new)) + RIGHT;
		if (array instanceof String[][])
			return LEFT + String.join(SEP, Stream.of((String[][]) array).map(t -> arrayToString(t, LEFT, RIGHT, SEP)).toArray(String[]::new)) + RIGHT;

		if (array instanceof boolean[][][])
			return LEFT + String.join(SEP, Stream.of((boolean[][][]) array).map(t -> arrayToString(t, LEFT, RIGHT, SEP)).toArray(String[]::new)) + RIGHT;
		if (array instanceof byte[][][])
			return LEFT + String.join(SEP, Stream.of((byte[][][]) array).map(t -> arrayToString(t, LEFT, RIGHT, SEP)).toArray(String[]::new)) + RIGHT;
		if (array instanceof short[][][])
			return LEFT + String.join(SEP, Stream.of((short[][][]) array).map(t -> arrayToString(t, LEFT, RIGHT, SEP)).toArray(String[]::new)) + RIGHT;
		if (array instanceof int[][][])
			return LEFT + String.join(SEP, Stream.of((int[][][]) array).map(t -> arrayToString(t, LEFT, RIGHT, SEP)).toArray(String[]::new)) + RIGHT;
		if (array instanceof long[][][])
			return LEFT + String.join(SEP, Stream.of((long[][][]) array).map(t -> arrayToString(t, LEFT, RIGHT, SEP)).toArray(String[]::new)) + RIGHT;
		if (array instanceof String[][][])
			return LEFT + String.join(SEP, Stream.of((String[][][]) array).map(t -> arrayToString(t, LEFT, RIGHT, SEP)).toArray(String[]::new)) + RIGHT;

		if (array instanceof Long[][])
			return LEFT + String.join(SEP, Stream.of((Long[][]) array).map(t -> arrayToString(t, LEFT, RIGHT, SEP)).toArray(String[]::new)) + RIGHT;

		if (array instanceof IVar[][])
			return LEFT + String.join(SEP, Stream.of((IVar[][]) array).map(t -> arrayToString(t, LEFT, RIGHT, SEP)).toArray(String[]::new)) + RIGHT;

		if (array instanceof Object[][])
			return LEFT + String.join(SEP, Stream.of((Object[][]) array).map(t -> arrayToString(t)).toArray(String[]::new)) + RIGHT;
		// return "(" + String.join(")(", Stream.of((Object[][]) array).map(t ->
		// simplify(Arrays.toString(t))).toArray(String[]::new)) +
		// ")";
		if (array instanceof Object[])
			return String.join(SEP,
					Stream.of((Object[]) array).map(t -> t.getClass().isArray() ? LEFT + arrayToString(t) + RIGHT : t.toString()).toArray(String[]::new));
		return null;
	}

	/** Method for converting an array into a string. */
	public static String arrayToString(Object array) {
		return arrayToString(array, '[', ']', ", ");
	}

	/**
	 * Returns true if inside the specified object, there is an element that checks the predicate. If syntactic trees
	 * are encountered, we check the leaves only.
	 */
	public static boolean check(Object obj, Predicate<Object> p) {
		if (obj instanceof Object[])
			return IntStream.range(0, Array.getLength(obj)).anyMatch(i -> check(Array.get(obj, i), p));
		if (obj instanceof XNode)
			return ((XNode<?>) obj).firstNodeSuchThat(n -> n instanceof XNodeLeaf && p.test(((XNodeLeaf<?>) n).value)) != null;
		// if (obj instanceof XNode)
		// return ((XNode<?>) obj).containsLeafSuchThat(leaf -> p.test(leaf.value));
		return p.test(obj);
	}

	public static class ModifiableBoolean {
		public Boolean value;

		public ModifiableBoolean(Boolean value) {
			this.value = value;
		}
	}

	// ************************************************************************
	// ***** Methods for XML
	// ************************************************************************

	/** Method that loads an XML document, using the specified file name. */
	public static Document loadDocument(String fileName) throws Exception {
		Utilities.control(new File(fileName).exists(), "Filename " + fileName + " not found\n");
		if (fileName.endsWith("xml.bz2") || fileName.endsWith("xml.lzma")) {
			Process p = Runtime.getRuntime().exec((fileName.endsWith("xml.bz2") ? "bunzip2 -c " : "lzma -c -d ") + fileName);
			Document document = DocumentBuilderFactory.newInstance().newDocumentBuilder().parse(p.getInputStream());
			p.waitFor();
			return document;
		} else
			return DocumentBuilderFactory.newInstance().newDocumentBuilder().parse(new FileInputStream(new File(fileName)));
	}

	public static void save(Document document, PrintWriter out) {
		try {
			Transformer transformer = TransformerFactory.newInstance().newTransformer();
			transformer.setOutputProperty(OutputKeys.INDENT, "yes");
			transformer.setOutputProperty(OutputKeys.OMIT_XML_DECLARATION, "yes");
			transformer.transform(new DOMSource(document), new StreamResult(out));
		} catch (Exception e) {
			e.printStackTrace();
		}
	}

	public static String save(Document document, String fileName) {
		try (PrintWriter out = new PrintWriter(new BufferedWriter(new FileWriter(fileName)))) {
			save(document, out);
		} catch (Exception e) {
			e.printStackTrace();
		}
		return fileName;
	}

	/** Method that returns an array with the child elements of the specified element. */
	public static Element[] childElementsOf(Element element) {
		NodeList childs = element.getChildNodes();
		return IntStream.range(0, childs.getLength()).mapToObj(i -> childs.item(i)).filter(e -> e.getNodeType() == Node.ELEMENT_NODE).toArray(Element[]::new);
	}

	/** Determines whether the specified element has the specified type as tag name. */
	public static boolean isTag(Element elt, TypeChild type) {
		return elt.getTagName().equals(type.name());
	}

	public static Element element(Document doc, String tag, List<Element> sons) {
		Element elt = doc.createElement(tag);
		sons.stream().forEach(c -> elt.appendChild(c));
		return elt;
	}

	public static Element element(Document doc, String tag, Element son) {
		return element(doc, tag, Arrays.asList(son));
	}

	public static Element element(Document doc, String tag, Element son, Element... otherSons) {
		return element(doc, tag, IntStream.range(0, 1 + otherSons.length).mapToObj(i -> i == 0 ? son : otherSons[i - 1]).collect(Collectors.toList()));
	}

	public static Element element(Document doc, String tag, Element son, Stream<Element> otherSons) {
		return element(doc, tag, Stream.concat(Stream.of(son), otherSons).collect(Collectors.toList()));
	}

	public static Element element(Document doc, String tag, Object textContent) {
		Element elt = doc.createElement(tag);
		elt.setTextContent(" " + textContent + " ");
		return elt;
	}

	public static Element element(Document doc, String tag, String attName, String attValue, Object textContent) {
		Element elt = element(doc, tag, textContent);
		elt.setAttribute(attName, attValue);
		return elt;
	}

	public static Element element(Document doc, String tag, String attName, String attValue) {
		Element elt = doc.createElement(tag);
		elt.setAttribute(attName, attValue);
		return elt;
	}

	public static Element element(Document doc, String tag, String attName1, String attValue1, String attName2, String attValue2) {
		Element elt = doc.createElement(tag);
		elt.setAttribute(attName1, attValue1);
		elt.setAttribute(attName2, attValue2);
		return elt;
	}

	public static Element element(Document doc, String tag, Stream<Entry<String, Object>> attributes) {
		Element elt = doc.createElement(tag);
		if (attributes != null)
			attributes.forEach(e -> elt.setAttribute(e.getKey(), e.getValue().toString()));
		return elt;
	}

	public static Element element(Document doc, String tag, Collection<Entry<String, Object>> attributes) {
		return element(doc, tag, attributes != null ? attributes.stream() : null);
	}

} public static class ModifiableBoolean {
	public Boolean value;

	public ModifiableBoolean(Boolean value) {
		this.value = value;
	}
} public static final class Dom extends DomBasic {

	public static String compactFormOf(int[] values) {
		StringBuilder sb = new StringBuilder();
		if (values.length == 2)
			return values[0] + " " + values[1];
		int prevVal = values[0], startInterval = prevVal;
		for (int i = 1; i < values.length; i++) {
			int currVal = values[i];
			if (currVal != prevVal + 1) {
				sb.append(prevVal == startInterval ? prevVal : startInterval + (prevVal == startInterval + 1 ? " " : "..") + prevVal).append(" ");
				// when only two values, no need for an interval
				startInterval = currVal;
			}
			prevVal = currVal;
		}
		return sb.append(prevVal == startInterval ? prevVal : startInterval + (prevVal == startInterval + 1 ? " " : "..") + prevVal).toString();
	}

	/**
	 * Builds an integer domain, with the integer values (entities that are either integers or integer intervals) obtained by parsing the
	 * specified string.
	 */
	protected Dom(String seq) {
		super(IntegerEntity.parseSeq(seq)); // must be already sorted.
	}

	/** Builds an integer domain, with the specified integer values. */
	public Dom(int[] values) {
		super(IntStream.of(values).mapToObj(v -> new IntegerValue(v)).toArray(IntegerEntity[]::new));
	}

	/** Builds an integer domain, with the specified integer interval. */
	public Dom(int min, int max) {
		super(new IntegerEntity[] { new IntegerInterval(min, max) });
	}

	/** Returns the first (smallest) value of the domain. It may be VAL_M_INFINITY for -infinity. */
	public long firstValue() {
		return ((IntegerEntity) values[0]).smallest();
	}

	/** Returns the last (greatest) value of the domain. It may be VAL_P_INFINITY for +infinity. */
	public long lastValue() {
		return ((IntegerEntity) values[values.length - 1]).greatest();
	}

	/** Returns true iff the domain contains the specified value. */
	public boolean contains(long v) {
		for (int left = 0, right = values.length - 1; left <= right;) {
			int center = (left + right) / 2;
			int res = ((IntegerEntity) values[center]).compareContains(v);
			if (res == 0)
				return true;
			if (res == -1)
				left = center + 1;
			else
				right = center - 1;
		}
		return false;
	}

	private Object cacheAllValues; // cache for lazy initialization

	/** Returns the number of values in the domain, if the domain is finite. Returns -1 otherwise. */
	public long nValues() {
		if (cacheAllValues == null)
			cacheAllValues = allValues();
		return cacheAllValues == null ? -1 : cacheAllValues instanceof Range ? ((Range) cacheAllValues).length() : ((int[]) cacheAllValues).length;
	}

	/**
	 * Returns the values of the integer domain, either as an object Range or as an array of integers. Returns null if the domain is infinite (or
	 * too large).
	 **/
	public Object allValues() {
		if (cacheAllValues == null) {
			IntegerEntity[] vs = (IntegerEntity[]) values;
			if (values.length == 1 && values[0] instanceof IntegerInterval) {
				IntegerInterval ii = (IntegerInterval) values[0];
				cacheAllValues = ii.width() == -1 ? null : new Range(ii);
			} else
				cacheAllValues = IntegerEntity.toIntArray(vs, Integer.MAX_VALUE);
		}
		assert !(cacheAllValues instanceof int[])
				|| IntStream.range(0, ((int[]) cacheAllValues).length - 1).allMatch(i -> ((int[]) cacheAllValues)[i] < ((int[]) cacheAllValues)[i + 1]);
		return cacheAllValues;
	}

	/**
	 * Returns this object if the condition is evaluated to {@code true}, {@code null} otherwise.
	 * 
	 * @param condition
	 *            a Boolean expression
	 * @return this object if the condition is evaluated to {@code true}, {@code null} otherwise
	 */
	public Dom when(boolean condition) {
		return condition ? this : null;
	}
} public static interface IntegerEntity extends Comparable<IntegerEntity> {
	/** Returns an integer entity (integer value or integer interval) obtained by parsing the specified string. */
	public static IntegerEntity parse(String s) {
		String[] t = s.split("\\.\\.");
		return t.length == 1 ? new IntegerValue(safeLong(t[0])) : new IntegerInterval(safeLong(t[0], true), safeLong(t[1], true));
	}

	/** Returns an array of integer entities (integer values or integer intervals) obtained by parsing the specified string. */
	public static IntegerEntity[] parseSeq(String seq) {
		return Stream.of(seq.split("\\s+")).map(tok -> IntegerEntity.parse(tok)).toArray(IntegerEntity[]::new);
	}

	/**
	 * Returns the number of values in the specified array of integer entities. Importantly, note that -1 is returned if this number is infinite, or simply
	 * greater than {@code Long.MAX_VALUE}.
	 */
	public static long nValues(IntegerEntity[] pieces) {
		assert IntStream.range(0, pieces.length - 1).noneMatch(i -> pieces[i].greatest() >= pieces[i + 1].smallest());
		if (Stream.of(pieces).anyMatch(p -> p.width() == -1))
			return -1L; // the number of values does not fit within a long
		long cnt = 0;
		try {
			for (IntegerEntity piece : pieces)
				cnt = Math.addExact(cnt, piece.width());
		} catch (ArithmeticException e) {
			return -1L;
		}
		return cnt;
	}

	/**
	 * Returns an array of integers with all values represented by the specified integer entities. Note that null is returned if the number of values is
	 * infinite or greater than the specified limit value.
	 */
	public static int[] toIntArray(IntegerEntity[] pieces, int limit) {
		long l = nValues(pieces);
		if (l == -1L || l > limit)
			return null;
		int[] values = new int[(int) l];
		int i = 0;
		for (IntegerEntity piece : pieces)
			if (piece instanceof IntegerValue)
				values[i++] = Utilities.safeInt(((IntegerValue) piece).v);
			else {
				int min = Utilities.safeInt(((IntegerInterval) piece).inf), max = Utilities.safeInt(((IntegerInterval) piece).sup);
				for (int v = min; v <= max; v++)
					values[i++] = v;
			}
		return values;
	}

	/**
	 * Returns an array of integers with all values represented by the specified integer entities. Note that null is returned if the number of values is
	 * infinite or greater than Integer.MAX_VALUE
	 */
	public static int[] toIntArray(IntegerEntity[] pieces) {
		return toIntArray(pieces, Integer.MAX_VALUE);
	}

	@Override
	public default int compareTo(IntegerEntity p) {
		long l1 = this instanceof IntegerValue ? ((IntegerValue) this).v : ((IntegerInterval) this).inf;
		long l2 = p instanceof IntegerValue ? ((IntegerValue) p).v : ((IntegerInterval) p).inf;
		return l1 < l2 ? -1 : l1 > l2 ? 1 : 0; // correct because pieces do not overlap
	}

	/** Returns true iff the entity is an integer value or an integer interval containing only one value */
	public boolean isSingleton();

	/** Returns the smallest value of the entity (the value itself or the lower bound of the interval). */
	public long smallest();

	/** Returns the greatest value of the entity (the value itself or the upper bound of the interval). */
	public long greatest();

	/** Returns the number of values represented by the entity, or -1 if this number does not fit within a {@code long}. */
	public long width();

	/**
	 * Returns 0 if the entity contains the specified value, -1 if the values of the entity are strictly smaller than the specified value, and +1 if the
	 * values of the entity are strictly greater than the specified value.
	 */
	public int compareContains(long l);

} public static final class IntegerInterval implements IntegerEntity {
	/** The bounds of the interval. */
	public final long inf, sup;

	private final long width;

	/** Builds an IntegerInterval object with the specified bounds. */
	public IntegerInterval(long inf, long sup) {
		this.inf = inf;
		this.sup = sup;
		Utilities.control(inf <= sup, "Interval problem " + this);
		width = inf == MINUS_INFINITY || sup == PLUS_INFINITY || !Utilities.checkSafeArithmeticOperation(() -> Math.subtractExact(sup + 1, inf)) ? -1
				: sup + 1 - inf;
	}

	public IntegerInterval(long singleton) {
		this(singleton, singleton);
	}

	@Override
	public boolean isSingleton() {
		return inf == sup;
	}

	@Override
	public long smallest() {
		return inf;
	}

	@Override
	public long greatest() {
		return sup;
	}

	@Override
	public long width() {
		return width;
	}

	@Override
	public int compareContains(long l) {
		return sup < l ? -1 : inf > l ? 1 : 0;
	}

	@Override
	public String toString() {
		return inf == sup - 1 ? inf + " " + sup : inf + ".." + sup;
	}
} public static final class Occurrences {

	public final Object value;
	public final long nOccurrences;

	public Occurrences(Object value, int nOccurrences) {
		this.value = value;
		this.nOccurrences = nOccurrences;
		Utilities.control(value instanceof String || value instanceof Long, "bad argument");
	}

	@Override
	public String toString() {
		return value + Constants.TIMES + nOccurrences;
	}
} public class TreeEvaluator {

	/**********************************************************************************************
	 * Static
	 *********************************************************************************************/

	private static final Map<String, Class<?>> classMap = new HashMap<>();

	private static final Map<String, Integer> arityMap = new HashMap<>();

	private static final Set<String> symmetricEvaluators = new HashSet<>(), associativeEvaluators = new HashSet<>();

	static {
		for (Class<?> cl : Stream.of(TreeEvaluator.class.getDeclaredClasses())
				.filter(c -> Evaluator.class.isAssignableFrom(c) && !Modifier.isAbstract(c.getModifiers())).toArray(Class<?>[]::new)) {
			String evaluatorToken = cl.getSimpleName().substring(0, 1).toLowerCase()
					+ cl.getSimpleName().substring(1, cl.getSimpleName().lastIndexOf(Evaluator.class.getSimpleName()));
			classMap.put(evaluatorToken, cl);
			// System.out.println(evaluatorToken + " " + clazz);
			int arity = -1;
			try {
				if (TagArity0.class.isAssignableFrom(cl))
					arity = 0;
				if (TagArity1.class.isAssignableFrom(cl))
					arity = 1;
				if (TagArity2.class.isAssignableFrom(cl))
					arity = 2;
				if (TagArity3.class.isAssignableFrom(cl))
					arity = 3;
				if (TagArityX.class.isAssignableFrom(cl))
					arity = Integer.MAX_VALUE;
				if (TagSymmetric.class.isAssignableFrom(cl))
					symmetricEvaluators.add(evaluatorToken);
				if (TagAssociative.class.isAssignableFrom(cl))
					associativeEvaluators.add(evaluatorToken);
			} catch (Exception e) {
				e.printStackTrace();
				System.exit(1);
			}
			Utilities.control(arity != -1, "Pb with arity");
			arityMap.put(evaluatorToken, arity);
		}
	}

	public static Class<?> classOf(String tok) {
		return classMap.get(tok);
	}

	public static int arityOf(String tok) {
		Integer a = arityMap.get(tok);
		if (a != null)
			return a; // arity of a basic operator
		int pos = IntStream.range(0, tok.length()).filter(i -> !Character.isDigit(tok.charAt(i))).findFirst().orElse(tok.length()) - 1;
		// either a token that is not an operator (return -1) or an eXtended operator (necessarily starts with an integer)
		return pos == -1 || pos == tok.length() - 1 ? -1 : Integer.parseInt(tok.substring(0, pos + 1));
	}

	public static boolean isSymmetric(String tok) {
		return symmetricEvaluators.contains(tok);
	}

	public static boolean isAssociative(String tok) {
		return associativeEvaluators.contains(tok);
	}

	public static final int SAMPLING_LIMIT = 1000;

	/**********************************************************************************************
	 * Tags
	 *********************************************************************************************/

	public interface TagBoolean {
	}

	public interface TagInteger {
	}

	public interface TagArithmetic extends TagInteger {
	}

	public interface TagLogical extends TagBoolean {
	}

	public interface TagRelational extends TagBoolean {
	}

	public interface TagSet {
	}

	public interface TagTerminal {
	}

	public interface TagSymmetric {
	}

	public interface TagAssociative {
	}

	public interface TagArity0 {
	}

	public interface TagArity1 {
	}

	public interface TagArity2 {
	}

	public interface TagArity3 {
	}

	public interface TagArityX {
	}

	/**********************************************************************************************
	 * Root class for evaluators
	 *********************************************************************************************/

	public abstract class Evaluator {

		public int arity = -1;

		public void fixArity() {
			Utilities.control(arity == -1 || this instanceof TagArityX, "Pb with arity");
			if (arity == -1)
				arity = this instanceof TagArity0 ? 0 : this instanceof TagArity1 ? 1 : this instanceof TagArity2 ? 2 : this instanceof TagArity3 ? 3 : -1;
		}

		public abstract void evaluate();

		@Override
		public String toString() {
			return getClass().getSimpleName();
		}
	}

	/**********************************************************************************************
	 * Arithmetic Evaluators
	 *********************************************************************************************/

	public class NegEvaluator extends Evaluator implements TagArity1, TagArithmetic {
		@Override
		public void evaluate() {
			stack[top] = -stack[top];
		}
	}

	public class AbsEvaluator extends Evaluator implements TagArity1, TagArithmetic {
		@Override
		public void evaluate() {
			stack[top] = Math.abs(stack[top]);
		}
	}

	public class AddEvaluator extends Evaluator implements TagArity2, TagArithmetic, TagSymmetric, TagAssociative {
		@Override
		public void evaluate() {
			top--;
			stack[top] = stack[top] + stack[top + 1];
		}
	}

	public class AddxEvaluator extends Evaluator implements TagArityX, TagArithmetic, TagSymmetric, TagAssociative {
		@Override
		public void evaluate() {
			top -= arity - 1;
			long sum = stack[top];
			for (int i = 1; i < arity; i++)
				sum += stack[top + i];
			stack[top] = sum;
		}
	}

	public class SubEvaluator extends Evaluator implements TagArity2, TagArithmetic {
		@Override
		public void evaluate() {
			top--;
			stack[top] = stack[top] - stack[top + 1];
		}
	}

	public class MulEvaluator extends Evaluator implements TagArity2, TagArithmetic, TagSymmetric, TagAssociative {
		@Override
		public void evaluate() {
			top--;
			stack[top] = stack[top] * stack[top + 1];
		}
	}

	public class MulxEvaluator extends Evaluator implements TagArityX, TagArithmetic, TagSymmetric, TagAssociative {
		@Override
		public void evaluate() {
			top -= arity - 1;
			long product = stack[top];
			for (int i = 1; i < arity; i++)
				product *= stack[top + i];
			stack[top] = product;
		}
	}

	public class DivEvaluator extends Evaluator implements TagArity2, TagArithmetic {
		@Override
		public void evaluate() {
			top--;
			stack[top] = stack[top] / stack[top + 1];
		}
	}

	public class ModEvaluator extends Evaluator implements TagArity2, TagArithmetic {
		@Override
		public void evaluate() {
			top--;
			stack[top] = stack[top] % stack[top + 1];
		}
	}

	public class SqrEvaluator extends Evaluator implements TagArity1, TagArithmetic {
		@Override
		public void evaluate() {
			stack[top] = stack[top] * stack[top];
		}
	}

	public class PowEvaluator extends Evaluator implements TagArity2, TagArithmetic {
		@Override
		public void evaluate() {
			top--;
			stack[top] = (long) Math.pow(stack[top], stack[top + 1]);
		}
	}

	public class MinEvaluator extends Evaluator implements TagArity2, TagArithmetic, TagSymmetric, TagAssociative {
		@Override
		public void evaluate() {
			top--;
			stack[top] = Math.min(stack[top], stack[top + 1]);
		}
	}

	public class MinxEvaluator extends Evaluator implements TagArityX, TagArithmetic, TagSymmetric, TagAssociative {
		@Override
		public void evaluate() {
			top -= arity - 1;
			long min = stack[top];
			for (int i = 1; i < arity; i++)
				min = Math.min(min, stack[top + i]);
			stack[top] = min;
		}
	}

	public class MaxEvaluator extends Evaluator implements TagArity2, TagArithmetic, TagSymmetric, TagAssociative {
		@Override
		public void evaluate() {
			top--;
			stack[top] = Math.max(stack[top], stack[top + 1]);
		}
	}

	public class MaxxEvaluator extends Evaluator implements TagArityX, TagArithmetic, TagSymmetric, TagAssociative {
		@Override
		public void evaluate() {
			top -= arity - 1;
			long max = stack[top];
			for (int i = 1; i < arity; i++)
				max = Math.max(max, stack[top + i]);
			stack[top] = max;
		}
	}

	public class DistEvaluator extends Evaluator implements TagArity2, TagArithmetic, TagSymmetric {
		@Override
		public void evaluate() {
			top--;
			stack[top] = Math.abs(stack[top] - stack[top + 1]);
		}
	}

	public interface ExternFunctionArity1 {
		public long evaluate(long l);
	}

	public interface ExternFunctionArity2 {
		public long evaluate(long l1, long l2);
	}

	public class F1Evaluator extends Evaluator implements TagArity1, TagArithmetic {
		public ExternFunctionArity1 function;

		@Override
		public void evaluate() {
			stack[top] = function.evaluate(stack[top]);
		}
	}

	public class F2Evaluator extends Evaluator implements TagArity2, TagArithmetic {
		public ExternFunctionArity2 function;

		@Override
		public void evaluate() {
			top--;
			stack[top] = function.evaluate(stack[top], stack[top + 1]);
		}
	}

	/**********************************************************************************************
	 * Relational Evaluators
	 *********************************************************************************************/

	public class LtEvaluator extends Evaluator implements TagArity2, TagRelational {
		@Override
		public void evaluate() {
			top--;
			stack[top] = (stack[top] < stack[top + 1] ? 1 : 0);
		}
	}

	public class LtxEvaluator extends Evaluator implements TagArityX, TagRelational, TagSymmetric, TagAssociative {
		@Override
		public void evaluate() {
			top -= arity - 1;
			for (int i = 1; i < arity; i++)
				if (stack[top + i - 1] >= stack[top + i]) {
					stack[top] = 0;
					return;
				}
			stack[top] = 1;
		}
	}

	public class LeEvaluator extends Evaluator implements TagArity2, TagRelational {
		@Override
		public void evaluate() {
			top--;
			stack[top] = (stack[top] <= stack[top + 1] ? 1 : 0);
		}
	}

	public class LexEvaluator extends Evaluator implements TagArityX, TagRelational, TagSymmetric, TagAssociative {
		@Override
		public void evaluate() {
			top -= arity - 1;
			for (int i = 1; i < arity; i++)
				if (stack[top + i - 1] > stack[top + i]) {
					stack[top] = 0;
					return;
				}
			stack[top] = 1;
		}
	}

	public class GeEvaluator extends Evaluator implements TagArity2, TagRelational {
		@Override
		public void evaluate() {
			top--;
			stack[top] = (stack[top] >= stack[top + 1] ? 1 : 0);
		}
	}

	public class GexEvaluator extends Evaluator implements TagArityX, TagRelational, TagSymmetric, TagAssociative {
		@Override
		public void evaluate() {
			top -= arity - 1;
			for (int i = 1; i < arity; i++)
				if (stack[top + i - 1] < stack[top + i]) {
					stack[top] = 0;
					return;
				}
			stack[top] = 1;
		}
	}

	public class GtEvaluator extends Evaluator implements TagArity2, TagRelational {
		@Override
		public void evaluate() {
			top--;
			stack[top] = (stack[top] > stack[top + 1] ? 1 : 0);
		}
	}

	public class GtxEvaluator extends Evaluator implements TagArityX, TagRelational, TagSymmetric, TagAssociative {
		@Override
		public void evaluate() {
			top -= arity - 1;
			for (int i = 1; i < arity; i++)
				if (stack[top + i - 1] <= stack[top + i]) {
					stack[top] = 0;
					return;
				}
			stack[top] = 1;
		}
	}

	public class NeEvaluator extends Evaluator implements TagArity2, TagRelational, TagSymmetric, TagAssociative {
		@Override
		public void evaluate() {
			top--;
			stack[top] = (stack[top] != stack[top + 1] ? 1 : 0);
		}
	}

	public class NexEvaluator extends Evaluator implements TagArityX, TagRelational, TagSymmetric, TagAssociative {
		@Override
		public void evaluate() {
			top -= arity - 1;
			for (int i = arity - 1; i > 0; i--)
				for (int j = i - 1; j >= 0; j--)
					if (stack[top + i] == stack[top + j]) {
						stack[top] = 0;
						return;
					}
			stack[top] = 1;
		}
	}

	public class EqEvaluator extends Evaluator implements TagArity2, TagRelational, TagSymmetric, TagAssociative {
		@Override
		public void evaluate() {
			top--;
			stack[top] = (stack[top] == stack[top + 1] ? 1 : 0);
		}
	}

	public class EqxEvaluator extends Evaluator implements TagArityX, TagRelational, TagSymmetric, TagAssociative {
		@Override
		public void evaluate() {
			top -= arity - 1;
			long value = stack[top];
			for (int i = 1; i < arity; i++)
				if (stack[top + i] != value) {
					stack[top] = 0;
					return;
				}
			stack[top] = 1;
		}
	}

	/**********************************************************************************************
	 * Set Evaluators
	 *********************************************************************************************/

	public class SetxEvaluator extends Evaluator implements TagArityX, TagSet {
		@Override
		public void evaluate() {
			// System.out.println("arity=" + arity + " " + this);
			stack[++top] = arity; // to be used by next operator which is necessarily in or notin
		}
	}

	public class InEvaluator extends Evaluator implements TagArity2, TagSet, TagBoolean {
		@Override
		public void evaluate() {
			int arity = (int) stack[top--]; // comes from operator set
			top -= arity;
			long value = stack[top];
			for (int i = 1; i < arity + 1; i++)
				if (stack[top + i] == value) {
					stack[top] = 1;
					return;
				}

			stack[top] = 0;
		}
	}

	public class NotinEvaluator extends Evaluator implements TagArity2, TagSet, TagBoolean {
		@Override
		public void evaluate() {
			int arity = (int) stack[top--]; // comes from operator set
			top -= arity;
			long value = stack[top];
			for (int i = 1; i < arity + 1; i++)
				if (stack[top + i] == value) {
					stack[top] = 0;
					return;
				}

			stack[top] = 1;
		}
	}

	/**********************************************************************************************
	 * Logical Evaluators
	 *********************************************************************************************/

	public class NotEvaluator extends Evaluator implements TagArity1 {
		@Override
		public void evaluate() {
			stack[top] = 1 - stack[top]; // (stack[nbStackElements - 1] == 1 ? 0 : 1);
		}
	}

	public class AndEvaluator extends Evaluator implements TagArity2, TagLogical, TagSymmetric, TagAssociative {
		@Override
		public void evaluate() {
			top--;
			stack[top] = Math.min(stack[top], stack[top + 1]);
		}
	}

	public class AndxEvaluator extends Evaluator implements TagArityX, TagLogical, TagSymmetric, TagAssociative {
		@Override
		public void evaluate() {
			top -= arity - 1;
			for (int i = 0; i < arity; i++)
				if (stack[top + i] == 0) {
					stack[top] = 0;
					return;
				}
			stack[top] = 1;
		}
	}

	public class OrEvaluator extends Evaluator implements TagArity2, TagLogical, TagSymmetric, TagAssociative {
		@Override
		public void evaluate() {
			top--;
			stack[top] = Math.max(stack[top], stack[top + 1]);
		}
	}

	public class OrxEvaluator extends Evaluator implements TagArityX, TagLogical, TagSymmetric, TagAssociative {
		@Override
		public void evaluate() {
			top -= arity - 1;
			for (int i = 0; i < arity; i++)
				if (stack[top + i] == 1) {
					stack[top] = 1;
					return;
				}
			stack[top] = 0;
		}
	}

	public class XorEvaluator extends Evaluator implements TagArity2, TagLogical, TagSymmetric, TagAssociative {
		@Override
		public void evaluate() {
			top--;
			stack[top] = (stack[top] + stack[top + 1] == 1 ? 1 : 0);
		}
	}

	public class XorxEvaluator extends Evaluator implements TagArityX, TagLogical, TagSymmetric, TagAssociative {
		@Override
		public void evaluate() {
			top -= arity - 1;
			int cnt = 0;
			for (int i = 0; i < arity; i++)
				if (stack[top + i] == 1)
					cnt++;
			stack[top] = cnt % 2;
		}
	}

	public class IffEvaluator extends Evaluator implements TagArity2, TagLogical, TagSymmetric, TagAssociative {
		@Override
		public void evaluate() {
			top--;
			stack[top] = (stack[top] == stack[top + 1] ? 1 : 0);
		}
	}

	public class IffxEvaluator extends Evaluator implements TagArityX, TagLogical, TagSymmetric, TagAssociative {
		@Override
		public void evaluate() {
			top -= arity - 1;
			long value = stack[top];
			for (int i = 1; i < arity; i++)
				if (stack[top + i] != value) {
					stack[top] = 0;
					return;
				}
			stack[top] = 1;
		}
	}

	public class ImpEvaluator extends Evaluator implements TagArity2, TagLogical {
		@Override
		public void evaluate() {
			top--;
			stack[top] = (stack[top] == 0 || stack[top + 1] == 1 ? 1 : 0);
		}
	}

	public class IfEvaluator extends Evaluator implements TagArity3, TagArithmetic {
		@Override
		public void evaluate() {
			top -= 2;
			stack[top] = stack[top] == 1 ? stack[top + 1] : stack[top + 2];
			// if (stack[top+2] == 1)
			// stack[top]=stack[top+1];
		}
	}

	/**********************************************************************************************
	 * Terminal Evaluators
	 *********************************************************************************************/

	public class FalseEvaluator extends Evaluator implements TagArity0, TagTerminal, TagBoolean {
		@Override
		public void evaluate() {
			stack[++top] = 0;
		}
	}

	public class TrueEvaluator extends Evaluator implements TagArity0, TagTerminal, TagBoolean {
		@Override
		public void evaluate() {
			stack[++top] = 1;
		}
	}

	public class LongEvaluator extends Evaluator implements TagArity0, TagTerminal, TagInteger {

		public final long value;

		public LongEvaluator(long value) {
			this.value = value;
		}

		@Override
		public void evaluate() {
			stack[++top] = value;
		}

		@Override
		public String toString() {
			return super.toString() + "(" + value + ")";
		}

	}

	public class VariableEvaluator extends Evaluator implements TagArity0, TagTerminal, TagInteger {

		public final int position;

		public VariableEvaluator(int position) {
			this.position = position;
		}

		@Override
		public void evaluate() {
			stack[++top] = values[position];
		}
	}

	/**********************************************************************************************
	 * The body of the class
	 *********************************************************************************************/

	/** The syntactic tree representing the predicate. */
	private XNode<? extends IVar> tree;

	/**
	 * The sequence of evaluators (built from a post-fixed expression) that can be called for evaluating a tuple of values (instantiation).
	 */
	public Evaluator[] evaluators;

	/** The current top value for the stack. Initially, at -1 */
	private int top = -1;

	/** The stack used for evaluating a tuple of values (instantiation). */
	private long[] stack;

	/**
	 * 1D = index of evaluator; <br>
	 * value = 1 means that if the result of the evaluator is 1 it can be returned immediately, <br>
	 * value = 0 means that if the result of the evaluator is 0 it can be returned immediately, <br>
	 * value = -1 means that we have to keep evaluating
	 */
	private int[] shortCircuits;

	/**
	 * This field is inserted in order to avoid having systematically a tuple of values as parameter of methods evaluate() in Evaluator classes.
	 */
	private int[] values;

	private int[] tmp = new int[1];

	Integer arity;

	public boolean isBoolean() {
		return evaluators[evaluators.length - 1] instanceof TagBoolean;
	}

	public boolean isInteger() {
		return evaluators[evaluators.length - 1] instanceof TagInteger;
	}

	private Evaluator buildEvaluator(String tok, List<String> varNames) {
		try {
			if (tok.matches("^(-?)\\d+$"))
				return new LongEvaluator(Long.parseLong(tok));
			if (tok.startsWith("%"))
				return new VariableEvaluator(Integer.parseInt(tok.substring(1)));
			if (classOf(tok) != null)
				return (Evaluator) classOf(tok).getDeclaredConstructor(TreeEvaluator.class).newInstance(TreeEvaluator.this);
			int pos = IntStream.range(0, tok.length()).filter(i -> !Character.isDigit(tok.charAt(i))).findFirst().orElse(tok.length()) - 1;
			if (pos == -1) {
				int varPos = varNames.indexOf(tok);
				if (varPos == -1) {
					varPos = varNames.size();
					varNames.add(tok);
				}
				return new VariableEvaluator(varPos);
			}
			Evaluator evaluator = (Evaluator) classOf(tok.substring(pos + 1) + "x").getDeclaredConstructor(TreeEvaluator.class).newInstance(TreeEvaluator.this);
			evaluator.arity = Integer.parseInt(tok.substring(0, pos + 1));
			return evaluator;
		} catch (Exception e) {
			(e.getCause() == null ? e : e.getCause()).printStackTrace();
			return null;
		}
	}

	// Reste a faire pour IF
	private void dealWithShortCircuits() {
		boolean useShortCircuits = true; // TODO
		if (!useShortCircuits)
			return;
		shortCircuits = new int[evaluators.length];
		useShortCircuits = false;
		for (int i = 0; i < evaluators.length - 1; i++) {
			if (evaluators[i] instanceof TagInteger)
				continue;
			// from a Boolean evaluator, we may find a short circuit
			int j = i + 1;
			int nbStackedElements = 1;
			while (j < evaluators.length) {
				nbStackedElements += 1 - evaluators[j].arity;
				if (nbStackedElements <= 1)
					break;
				j++;
			}
			if (j == i + 1)
				continue;
			if (evaluators[j] instanceof OrEvaluator) {
				shortCircuits[i] = j + 1;
				useShortCircuits = true;
			} else if (evaluators[j] instanceof AndEvaluator) {
				shortCircuits[i] = -j - 1;
				useShortCircuits = true;
			}
		}
		if (!useShortCircuits)
			shortCircuits = null;
	}

	private void buildEvaluators() {
		List<String> varNames = new ArrayList<>(); // necessary to collect variable names when building the evaluators
		evaluators = Stream.of(tree.toPostfixExpression(tree.vars()).split(Constants.REG_WS)).map(s -> buildEvaluator(s, varNames)).peek(e -> e.fixArity())
				.toArray(Evaluator[]::new);
		dealWithShortCircuits();
		stack = new long[evaluators.length];
		assert evaluators.length > 0;
		int[] allPositions = Stream.of(evaluators).filter(e -> e instanceof VariableEvaluator).mapToInt(e -> ((VariableEvaluator) e).position).distinct()
				.sorted().toArray();
		Utilities.control(IntStream.range(0, allPositions.length).allMatch(i -> i == allPositions[i]), "");
		arity = allPositions.length;
	}

	public TreeEvaluator(XNode<? extends IVar> tree) {
		this.tree = tree;
		buildEvaluators();
	}

	public TreeEvaluator(XNode<? extends IVar> tree, Map<String, Integer> mapOfSymbols) {
		this(mapOfSymbols == null ? tree : (XNode<? extends IVar>) tree.replaceSymbols(mapOfSymbols));
	}

	/** Evaluates the specified tuple of values, by using the recorded so-called evaluators. */
	public final long evaluate(int[] values) {
		this.values = values;
		top = -1;
		if (shortCircuits == null)
			for (Evaluator evaluator : evaluators)
				evaluator.evaluate();
		else
			for (int i = 0; i < evaluators.length;) { // i = shortCircuits[i] == 0 ? i + 1 : nextEvaluator(i)) {
				evaluators[i].evaluate();
				if (shortCircuits[i] == 0)
					i++;
				else if (shortCircuits[i] > 0)
					i = stack[top] == 1 ? shortCircuits[i] : i + 1;
				else
					i = stack[top] == 0 ? -shortCircuits[i] : i + 1;
			}
		assert top == 0 : "" + top;
		return stack[top]; // 1 means true while 0 means false
	}

	// public final int[][] generateTuples(int[] sizes, Function<int[], int[]> f, ModifiableBoolean positive, int limit) {
	// List<int[]> supports = new ArrayList<>(), conflicts = new ArrayList<>();
	// int[] tupleIdx = new int[sizes.length];
	// int cnt = 0;
	// for (boolean hasNext = true; hasNext;) {
	// int[] tupleVal = f.apply(tupleIdx);
	// boolean consistent = evaluate(tupleVal) == 1;
	// if (consistent && positive.value != Boolean.FALSE)
	// supports.add(tupleVal.clone());
	// if (!consistent && positive.value != Boolean.TRUE)
	// conflicts.add(tupleVal.clone());
	// if (positive.value == null && ++cnt > limit)
	// positive.value = supports.size() <= conflicts.size() ? Boolean.TRUE : Boolean.FALSE;
	// hasNext = false;
	// for (int i = 0; !hasNext && i < tupleIdx.length; i++)
	// if (tupleIdx[i] + 1 < sizes[i].length) {
	// tupleIdx[i]++;
	// hasNext = true;
	// } else
	// tupleIdx[i] = 0;
	// }
	// if (positive.value == null)
	// positive.value = supports.size() <= conflicts.size() ? Boolean.TRUE : Boolean.FALSE;
	// return positive.value ? supports.toArray(new int[0][]) : conflicts.toArray(new int[0][]);
	// }

	public final int[] generatePossibleValues(int[][] domValues) {
		if (isBoolean())
			return new int[] { 0, 1 };
		Set<Long> set = new HashSet<>();
		new EnumerationCartesian(domValues).execute(tuple -> set.add(evaluate(tuple)));
		// for (int[] tuple : new EnumerationCartesian(domValues).toArray())
		// set.add(evaluate(tuple));
		return set.stream().peek(i -> Utilities.isSafeInt(i)).mapToInt(i -> i.intValue()).sorted().toArray();
	}

	public final int[][] generateTuples(int[][] domValues, ModifiableBoolean positive, int limit) {
		// control Boolean evaluator
		List<int[]> supports = new ArrayList<>(), conflicts = new ArrayList<>();
		int[] tupleIdx = new int[domValues.length], tupleVal = new int[domValues.length];
		int cnt = 0;
		for (boolean hasNext = true; hasNext;) {
			for (int i = 0; i < tupleVal.length; i++)
				tupleVal[i] = domValues[i][tupleIdx[i]];
			boolean consistent = evaluate(tupleVal) == 1;
			if (consistent && positive.value != Boolean.FALSE)
				supports.add(tupleVal.clone());
			if (!consistent && positive.value != Boolean.TRUE)
				conflicts.add(tupleVal.clone());
			if (positive.value == null && ++cnt > limit)
				positive.value = supports.size() <= conflicts.size() ? Boolean.TRUE : Boolean.FALSE;
			hasNext = false;
			for (int i = 0; !hasNext && i < tupleIdx.length; i++)
				if (tupleIdx[i] + 1 < domValues[i].length) {
					tupleIdx[i]++;
					hasNext = true;
				} else
					tupleIdx[i] = 0;
		}
		if (positive.value == null)
			positive.value = supports.size() <= conflicts.size() ? Boolean.TRUE : Boolean.FALSE;
		return positive.value ? supports.toArray(new int[0][]) : conflicts.toArray(new int[0][]);
	}

	public final int[][] generateTuples(int[][] domValues, ModifiableBoolean positive) {
		return generateTuples(domValues, positive, SAMPLING_LIMIT);
	}

	public final int[][] generateSupports(int[][] domValues) {
		return generateTuples(domValues, new ModifiableBoolean(true));
	}

	public final int[][] generateConflicts(int[][] domValues) {
		return generateTuples(domValues, new ModifiableBoolean(false));
	}

	public final int[][] computeTuples(int[][] domValues) {
		int arity = domValues.length;
		List<int[]> tuples = new ArrayList<>();
		int[] tupleIdx = new int[arity], tupleVal = new int[arity + 1];
		for (boolean hasNext = true; hasNext;) {
			for (int i = 0; i < arity; i++)
				tupleVal[i] = domValues[i][tupleIdx[i]];
			tupleVal[arity] = (int) evaluate(tupleVal); // TODO control long to int ?
			tuples.add(tupleVal.clone());
			hasNext = false;
			for (int i = 0; !hasNext && i < tupleIdx.length; i++)
				if (tupleIdx[i] + 1 < domValues[i].length) {
					tupleIdx[i]++;
					hasNext = true;
				} else
					tupleIdx[i] = 0;
		}
		return tuples.toArray(new int[0][]);
	}

	/** Evaluates the value, by using the recorded so-called evaluators. */
	public final long evaluate(int value) {
		tmp[0] = value;
		return evaluate(tmp);
	}

	public boolean controlArityOfEvaluators() {
		return Stream.of(evaluators).mapToInt(e -> 1 - e.arity).sum() == 1;
	}

	public boolean controlTypeOfEvaluators(boolean booleanType) {
		if (booleanType && !isBoolean())
			return false;
		if (!booleanType && !isInteger())
			return false;
		boolean[] booleanTypes = new boolean[evaluators.length];
		int top = -1;
		for (Evaluator evaluator : evaluators) {
			if (evaluator instanceof TagArithmetic) {
				if (evaluator instanceof IfEvaluator) {
					if (!booleanTypes[top] || booleanTypes[top - 1] || booleanTypes[top - 2])
						return false;
					top -= 3;
				} else {
					for (int j = 0; j < evaluator.arity; j++) {
						if (booleanTypes[top])
							return false;
						top--;
					}
				}
			} else if (evaluator instanceof TagLogical) {
				for (int j = 0; j < evaluator.arity; j++) {
					if (!booleanTypes[top])
						return false;
					top--;
				}
			} else if (evaluator instanceof TagRelational) {
				for (int j = 0; j < evaluator.arity; j++) {
					if (booleanTypes[top])
						return false;
					top--;
				}
			}
			booleanTypes[++top] = (evaluator instanceof TagBoolean);
		}
		return true;
	}
} public class XNodeParent<V extends IVar> extends XNode<V> {

	public static XNodeParent<IVar> build(TypeExpr type, Object... os) {
		os = Stream.of(os).flatMap(o -> o instanceof Stream ? (Stream<?>) o : Stream.of(o)).toArray();
		Utilities.control(type.arityMin <= os.length && os.length <= type.arityMax, "The arity (number of sons) is not valid");
		List<XNode<IVar>> sons = Stream.of(os).map(o -> {
			if (o instanceof XNode)
				return (XNode<IVar>) o;
			if (o instanceof IVar)
				return new XNodeLeaf<IVar>(TypeExpr.VAR, o);
			if (o instanceof Byte || o instanceof Short || o instanceof Integer || o instanceof Long)
				return new XNodeLeaf<IVar>(TypeExpr.LONG, ((Number) o).longValue());
			if (o instanceof String)
				return new XNodeLeaf<IVar>(TypeExpr.SYMBOL, o);
			return (XNode<IVar>) Utilities.control(false,
					"Bad form: have you used equal, different , lessThan,... instead of eq, ne, lt,... ?\n" + "The class causing problem is " + o.getClass());
		}).collect(Collectors.toList()); // toArray(XNode[]::new);
		return new XNodeParent<IVar>(type, sons);
	}

	public static XNodeParent<IVar> abs(Object operand) {
		return build(TypeExpr.ABS, operand);
	}

	public static XNodeParent<IVar> neg(Object operand) {
		return build(TypeExpr.NEG, operand);
	}

	public static XNodeParent<IVar> sqr(Object operand) {
		return build(TypeExpr.SQR, operand);
	}

	public static XNodeParent<IVar> add(Object... operands) {
		return build(TypeExpr.ADD, operands);
	}

	public static XNodeParent<IVar> sub(Object operand1, Object operand2) {
		return build(TypeExpr.SUB, operand1, operand2);
	}

	public static XNodeParent<IVar> mul(Object... operands) {
		return build(TypeExpr.MUL, operands);
	}

	public static XNodeParent<IVar> div(Object operand1, Object operand2) {
		return build(TypeExpr.DIV, operand1, operand2);
	}

	public static XNodeParent<IVar> mod(Object operand1, Object operand2) {
		return build(TypeExpr.MOD, operand1, operand2);
	}

	public static XNodeParent<IVar> pow(Object operand1, Object operand2) {
		return build(TypeExpr.POW, operand1, operand2);
	}

	public static XNodeParent<IVar> min(Object... operands) {
		return build(TypeExpr.MIN, operands);
	}

	public static XNodeParent<IVar> max(Object... operands) {
		return build(TypeExpr.MAX, operands);
	}

	public static XNodeParent<IVar> dist(Object operand1, Object operand2) {
		return build(TypeExpr.DIST, operand1, operand2);
	}

	public static XNodeParent<IVar> lt(Object operand1, Object operand2) {
		return build(TypeExpr.LT, operand1, operand2);
	}

	public static XNodeParent<IVar> le(Object operand1, Object operand2) {
		return build(TypeExpr.LE, operand1, operand2);
	}

	public static XNodeParent<IVar> ge(Object operand1, Object operand2) {
		return build(TypeExpr.GE, operand1, operand2);
	}

	public static XNodeParent<IVar> gt(Object operand1, Object operand2) {
		return build(TypeExpr.GT, operand1, operand2);
	}

	public static XNodeParent<IVar> ne(Object... operands) {
		return build(TypeExpr.NE, operands);
	}

	public static XNodeParent<IVar> eq(Object... operands) {
		return build(TypeExpr.EQ, operands);
	}

	public static XNode<IVar> set(Object... operands) {
		if (operands.length == 0)
			return new XNodeLeaf<IVar>(TypeExpr.SET, null);
		if (operands.length == 1 && operands[0] instanceof Range)
			return set(((Range) operands[0]).toArray());
		if (operands.length == 1 && operands[0] instanceof Collection) {
			Collection<?> coll = (Collection<?>) operands[0];
			if (coll.size() == 0)
				return new XNodeLeaf<IVar>(TypeExpr.SET, null);
			Object first = coll.iterator().next();
			if (first instanceof Byte || first instanceof Short || first instanceof Integer || first instanceof Long)
				return new XNodeParent<IVar>(TypeExpr.SET,
						coll.stream().map(s -> new XNodeLeaf<IVar>(TypeExpr.LONG, ((Number) s).longValue())).collect(toList()));
			if (first instanceof String)
				return new XNodeParent<IVar>(TypeExpr.SET, coll.stream().map(s -> new XNodeLeaf<IVar>(TypeExpr.SYMBOL, s)).collect(toList()));
			throw new RuntimeException();
		}
		return build(TypeExpr.SET, operands);
	}

	public static XNode<IVar> set(int[] operands) {
		if (operands.length == 0)
			return new XNodeLeaf<IVar>(TypeExpr.SET, null);
		return new XNodeParent<IVar>(TypeExpr.SET, IntStream.of(operands).mapToObj(v -> new XNodeLeaf<IVar>(TypeExpr.LONG, (long) v)).collect(toList()));
	}

	public static XNodeParent<IVar> in(Object var, Object set) {
		return build(TypeExpr.IN, var, set);
	}

	public static XNodeParent<IVar> notin(Object var, Object set) {
		return build(TypeExpr.NOTIN, var, set);
	}

	public static XNodeParent<IVar> not(Object operand) {
		return build(TypeExpr.NOT, operand);
	}

	public static XNodeParent<IVar> and(Object... operands) {
		return operands.length == 1 ? (XNodeParent<IVar>) operands[0] : build(TypeExpr.AND, operands); // modeling facility
	}

	public static XNodeParent<IVar> or(Object... operands) {
		return operands.length == 1 ? (XNodeParent<IVar>) operands[0] : build(TypeExpr.OR, operands); // modeling facility
	}

	public static XNodeParent<IVar> xor(Object... operands) {
		return build(TypeExpr.XOR, operands);
	}

	public static XNodeParent<IVar> iff(Object... operands) {
		return build(TypeExpr.IFF, operands);
	}

	public static XNodeParent<IVar> imp(Object operand1, Object operand2) {
		return build(TypeExpr.IMP, operand1, operand2);
	}

	public static XNodeParent<IVar> ifThenElse(Object operand1, Object operand2, Object operand3) {
		return build(TypeExpr.IF, operand1, operand2, operand3);
	}

	public static XNodeParent<IVar> scalar(int[] t1, Object[] t2) {
		Utilities.control(t1.length == t2.length, "Not the same number of elements in the two arrays");
		return new XNodeParent<IVar>(TypeExpr.ADD, IntStream.range(0, t1.length).mapToObj(i -> mul(t1[i], t2[i])).collect(toList()));
	}

	@Override
	public boolean equals(Object obj) {
		if (!(obj instanceof XNodeParent))
			return false;
		XNodeParent<?> node = (XNodeParent<?>) obj;
		return type == node.type && sons.length == node.sons.length && IntStream.range(0, sons.length).allMatch(i -> sons[i].equals(node.sons[i]));
	}

	@Override
	public int compareTo(XNode<V> obj) {
		if (type != obj.type)
			return Integer.compare(type.ordinal(), obj.type.ordinal());
		XNodeParent<V> node = (XNodeParent<V>) obj;
		if (sons.length < node.sons.length)
			return -1;
		if (sons.length > node.sons.length)
			return 1;
		return IntStream.range(0, sons.length).map(i -> sons[i].compareTo(node.sons[i])).filter(v -> v != 0).findFirst().orElse(0);
	}

	/** Builds a parent node for a syntactic tree, with the specified type and the specified sons. */
	public XNodeParent(TypeExpr type, XNode<V>[] sons) {
		super(type, sons);
		Utilities.control(sons.length > 0, "Pb with this node that should be a parent");
	}

	/** Builds a parent node for a syntactic tree, with the specified type and the specified sons. */
	public XNodeParent(TypeExpr type, List<XNode<V>> sons) {
		this(type, sons.toArray(new XNode[sons.size()]));
	}

	/** Builds a parent node for a syntactic tree, with the specified type and the specified son. */
	public XNodeParent(TypeExpr type, XNode<V> son) {
		this(type, Arrays.asList(son));
	}

	/** Builds a parent node for a syntactic tree, with the specified type and the two specified sons. */
	public XNodeParent(TypeExpr type, XNode<V> son1, XNode<V> son2) {
		this(type, Arrays.asList(son1, son2));
	}

	@Override
	public int size() {
		return 1 + Stream.of(sons).mapToInt(c -> c.size()).sum();
	}

	@Override
	public int maxParameterNumber() {
		return Stream.of(sons).mapToInt(c -> c.maxParameterNumber()).max().orElse(-1);
	}

	// private Matcher matcher() {
	// return new Matcher((XNodeParent<IVar>) this);
	// }

	private static class Canonizer<W extends IVar> {
		private Matcher abs_sub = new Matcher(node(ABS, node(SUB, any, any)));
		private Matcher not_not = new Matcher(node(NOT, node(NOT, any)));
		private Matcher neg_neg = new Matcher(node(NEG, node(NEG, any)));
		private Matcher any_lt_k = new Matcher(node(LT, any, val));
		private Matcher k_lt_any = new Matcher(node(LT, val, any));
		private Matcher not_logop = new Matcher(node(NOT, anyc), (node, level) -> level == 1 && node.type.isLogicallyInvertible());
		private Matcher not_symrel_any = new Matcher(node(symop, not, any)); // , (node, level) -> level == 0 && node.type.oneOf(EQ, NE));
		private Matcher any_symrel_not = new Matcher(node(symop, any, not)); // , (node, level) -> level == 0 && node.type.oneOf(EQ, NE));
		private Matcher x_mul_k__eq_l = new Matcher(node(EQ, node(MUL, var, val), val));
		private Matcher flattenable = new Matcher(anyc,
				(node, level) -> level == 0 && node.type.oneOf(ADD, MUL, MIN, MAX, AND, OR) && Stream.of(node.sons).anyMatch(s -> s.type == node.type));
		private Matcher mergeable = new Matcher(anyc, (node, level) -> level == 0 && node.type.oneOf(ADD, MUL, MIN, MAX, AND, OR) && node.sons.length >= 2
				&& node.sons[node.sons.length - 1].type == LONG && node.sons[node.sons.length - 2].type == LONG);
		private Matcher sub_relop_sub = new Matcher(node(relop, sub, sub));
		private Matcher any_relop_sub = new Matcher(node(relop, any, sub));
		private Matcher sub_relop_any = new Matcher(node(relop, sub, any));
		private Matcher any_add_val__relop__any_add_val = new Matcher(node(relop, any_add_val, any_add_val));
		private Matcher var_add_val__relop__val = new Matcher(node(relop, var_add_val, val));
		private Matcher val__relop__var_add_val = new Matcher(node(relop, val, var_add_val));

		private Map<Matcher, Function<XNodeParent<W>, XNode<W>>> rules = new LinkedHashMap<>();

		private Canonizer() {
			rules.put(abs_sub, r -> node(DIST, r.sons[0].sons)); // abs(sub(a,b)) => dist(a,b)
			rules.put(not_not, r -> r.sons[0].sons[0]); // not(not(a)) => a
			rules.put(neg_neg, r -> r.sons[0].sons[0]); // neg(neg(a)) => a
			rules.put(any_lt_k, r -> node(LE, r.sons[0], augment(r.sons[1], -1))); // e.g., lt(x,5) => le(x,4)
			rules.put(k_lt_any, r -> node(LE, augment(r.sons[0], 1), r.sons[1])); // e.g., lt(5,x) => le(6,x)
			rules.put(not_logop, r -> node(r.sons[0].type.logicalInversion(), r.sons[0].sons)); // e.g., not(lt(x)) => ge(x)
			rules.put(not_symrel_any, r -> node(r.type.logicalInversion(), r.sons[0].sons[0], r.sons[1])); // e.g., ne(not(x),y) => eq(x,y)
			rules.put(any_symrel_not, r -> node(r.type.logicalInversion(), r.sons[0], r.sons[1].sons[0])); // e.g., ne(x,not(y)) => eq(x,y)
			rules.put(x_mul_k__eq_l, r -> r.val(1) % r.val(0) == 0 ? node(EQ, r.sons[0].sons[0], longLeaf(r.val(1) / r.val(0))) : longLeaf(0));
			// below, e.g., eq(mul(x,4),8) => eq(x,2) and eq(mul(x,4),6) => 0 (false)
			rules.put(flattenable, r -> { // we flatten operators when possible; for example add(add(x,y),z) becomes add(x,y,z)
				int l1 = r.sons.length, pos = IntStream.range(0, l1).filter(i -> r.sons[i].type == r.type).findFirst().getAsInt(), l2 = r.sons[pos].sons.length;
				Stream<XNode<W>> list = IntStream.range(0, l1 - 1 + l2)
						.mapToObj(j -> j < pos ? r.sons[j] : j < pos + l2 ? r.sons[pos].sons[j - pos] : r.sons[j - l2 + 1]);
				return node(r.type, list);
			});
			rules.put(mergeable, r -> { // we merge long when possible. e.g., add(a,3,2) => add(a,5) and max(a,2,1) => max(a,2)
				XNode<W>[] t = Arrays.copyOf(r.sons, r.arity() - 1);
				long v1 = r.sons[r.arity() - 1].val(0), v2 = r.sons[r.arity() - 2].val(0);
				t[r.arity() - 2] = longLeaf(r.type == ADD ? v1 + v2 : r.type == MUL ? v1 * v2 : r.type.oneOf(MIN, AND) ? Math.min(v1, v2) : Math.max(v1, v2));
				return node(r.type, t);
			});
			// We replace sub by add when possible
			rules.put(sub_relop_sub, r -> node(r.type, node(ADD, r.sons[0].sons[0], r.sons[1].sons[1]), node(ADD, r.sons[1].sons[0], r.sons[0].sons[1])));
			rules.put(any_relop_sub, r -> node(r.type, node(ADD, r.sons[0], r.sons[1].sons[1]), r.sons[1].sons[0]));
			rules.put(sub_relop_any, r -> node(r.type, r.sons[0].sons[0], node(ADD, r.sons[1], r.sons[0].sons[1])));
			// We remove add when possible
			rules.put(any_add_val__relop__any_add_val,
					r -> node(r.type, node(ADD, r.sons[0].sons[0], longLeaf(r.sons[0].sons[1].val(0) - r.sons[1].sons[1].val(0))), r.sons[1].sons[0]));
			rules.put(var_add_val__relop__val, r -> node(r.type, r.sons[0].sons[0], longLeaf(r.sons[1].val(0) - r.sons[0].sons[1].val(0))));
			rules.put(val__relop__var_add_val, r -> node(r.type, longLeaf(r.sons[0].val(0) - r.sons[1].sons[1].val(0)), r.sons[1].sons[0]));
			// mul(x,1) = > x, and add(x,0) => x // TODO
		}

		private XNode<W> augment(XNode<W> n, int offset) {
			((XNodeLeaf<?>) n).value = (long) n.val(0) + offset;
			return n;
		}
	}

	private static Canonizer<?> canonizer;

	private Canonizer<V> canonizer() {
		if (XNodeParent.canonizer != null)
			return (Canonizer<V>) XNodeParent.canonizer;
		Canonizer<V> can = new Canonizer<>();
		canonizer = can;
		return can;
	}

	@Override
	public XNode<V> canonization() {
		// We will build the canonized form of the node, with the local variables type and sons
		TypeExpr type = this.type; // possibly, this initial value of type will be modified during canonization
		XNode<V>[] sons = this.sons.clone();
		IntStream.range(0, sons.length).forEach(i -> sons[i] = sons[i].canonization()); // sons are made canonical
		if (type.isSymmetricOperator())
			Arrays.sort(sons); // Sons are sorted if the type of the node is symmetric
		// Now, sons are potentially sorted if the type corresponds to a non-symmetric binary relational operator (in that case, we swap sons and
		// arithmetically inverse the operator provided that the ordinal value of the reverse operator is smaller)
		if (sons.length == 2 && type.isUnsymmetricRelationalOperator() && (type.arithmeticInversion().ordinal() < type.ordinal()
				|| (type.arithmeticInversion().ordinal() == type.ordinal() && sons[0].compareTo(sons[1]) > 0))) {
			type = type.arithmeticInversion();
			Utilities.swap(sons, 0, 1);
		}
		if (sons.length == 1 && type.isIdentityWhenOneOperand()) // add(x) becomes x, min(x) becomes x, ...
			return sons[0]; // certainly can happen during the canonization process
		XNodeParent<V> node = node(type, sons);
		Entry<Matcher, Function<XNodeParent<V>, XNode<V>>> rule = canonizer().rules.entrySet().stream().filter(e -> e.getKey().matches(node)).findFirst()
				.orElse(null);
		return rule != null ? rule.getValue().apply(node).canonization() : node;
	}

	private XNode<V> buildNewTreeUsing(Function<XNode<V>, XNode<V>> f) {
		return new XNodeParent<V>(type, Stream.of(sons).map(f).collect(Collectors.toList()));
	}

	@Override
	public XNode<V> abstraction(List<Object> args, boolean abstractIntegers, boolean multiOccurrences) {
		return buildNewTreeUsing(s -> s.abstraction(args, abstractIntegers, multiOccurrences));
	}

	@Override
	public XNode<V> concretization(Object[] args) {
		return buildNewTreeUsing(s -> s.concretization(args));
	}

	@Override
	public XNode<V> replaceSymbols(Map<String, Integer> mapOfSymbols) {
		return buildNewTreeUsing(s -> s.replaceSymbols(mapOfSymbols));
	}

	@Override
	public XNode<V> replaceLeafValues(Function<Object, Object> f) {
		return new XNodeParent<V>(type, Stream.of(sons).map(s -> s.replaceLeafValues(f)).collect(Collectors.toList()));
	}

	@Override
	public XNode<V> replacePartiallyParameters(Object[] valueParameters) {
		return new XNodeParent<V>(type, Stream.of(sons).map(s -> s.replacePartiallyParameters(valueParameters)).collect(Collectors.toList()));
	}

	@Override
	public XNode<V> firstNodeSuchThat(Predicate<XNode<V>> p) {
		return p.test(this) ? this : Stream.of(sons).map(son -> son.firstNodeSuchThat(p)).filter(o -> o != null).findFirst().orElse(null);
	}

	@Override
	public LinkedList<XNode<V>> allNodesSuchThat(Predicate<XNode<V>> p, LinkedList<XNode<V>> list) {
		if (p.test(this))
			list.add(this);
		Stream.of(sons).forEach(s -> s.allNodesSuchThat(p, list));
		return list;
	}

	@Override
	public String toPostfixExpression(IVar[] scopeForAbstraction) {
		String s = Stream.of(sons).map(c -> c.toPostfixExpression(scopeForAbstraction)).collect(Collectors.joining(" "));
		return s + " " + ((type == TypeExpr.SET || sons.length > 2 && type != TypeExpr.IF ? sons.length : "") + type.toString().toLowerCase());
	}

	@Override
	public String toFunctionalExpression(Object[] argsForConcretization) {
		String s = this instanceof XNodeParentSpecial ? ((XNodeParentSpecial<?>) this).specialName : type.toString().toLowerCase();
		return s + "(" + Stream.of(sons).map(c -> c.toFunctionalExpression(argsForConcretization)).collect(Collectors.joining(",")) + ")";
	}

} public interface AbstractTuple {

	boolean match(int[] tuple);

	public static class OrdinaryTuple implements AbstractTuple {
		public int[] values;

		public OrdinaryTuple(int[] values) {
			this.values = values;
		}

		@Override
		public boolean match(int[] t) {
			assert t.length == values.length;
			return IntStream.range(0, t.length).allMatch(i -> values[i] == Constants.STAR || t[i] == Constants.STAR || values[i] == t[i]);
		}

	}

	public static class SmartTuple implements AbstractTuple {
		public Object[] values; // either Integer or Condition objects inside the array

		public SmartTuple(Object[] values) {
			this.values = values;
			Utilities.control(Stream.of(values).allMatch(v -> v instanceof Integer || v instanceof ConditionVal || v instanceof ConditionSet),
					"Bad form for smart tuple");
		}

		@Override
		public boolean match(int[] t) {
			assert t.length == values.length;
			for (int i = 0; i < t.length; i++) {
				if (values[i] instanceof Integer) {
					int v = ((Integer) values[i]).intValue();
					if (v != Constants.STAR && t[i] != Constants.STAR && v != t[i])
						return false;
				} else {
					Condition condition = (Condition) values[i];
					if (condition instanceof ConditionVal) {
						if (((ConditionVal) condition).operator.isValidFor(t[i], ((ConditionVal) condition).k) == false)
							return false;
					} else if (condition instanceof ConditionIntvl) {
						if (((ConditionIntvl) condition).operator.isValidFor(t[i], ((ConditionIntvl) condition).min, ((ConditionIntvl) condition).max) == false)
							return false;
					} else if (condition instanceof ConditionIntset) {
						if (((ConditionIntset) condition).operator.isValidFor(t[i], ((ConditionIntset) condition).t) == false)
							return false;
					}
				}
			}
			return true;
		}
	}
} public class Transition {

	/**
	 * The source state, where the transition begins.
	 */
	public String start;

	/**
	 * The value (object) labeling the transition.
	 */
	public Object value;

	/**
	 * The target state, where the transition ends.
	 */
	public String end;

	/**
	 * Constructs a transition from the specified arguments.
	 * 
	 * @param firstState
	 *            the first state, where the transition begins
	 * @param symbol
	 *            the symbol labeling the transition
	 * @param secondState
	 *            the second state, where the transition ends
	 */
	public Transition(String firstState, Object symbol, String secondState) {
		this.start = firstState;
		this.value = symbol;
		this.end = secondState;
	}

	@Override
	public String toString() {
		return "(" + start + "," + value.toString() + "," + end + ")";
	}
} public interface XCallbacks {

	/**********************************************************************************************
	 * Managing Data required for implementation
	 *********************************************************************************************/

	/**
	 * The constants that can be used to pilot the parser.
	 */
	enum XCallbacksParameters {
		RECOGNIZE_UNARY_PRIMITIVES,
		RECOGNIZE_BINARY_PRIMITIVES,
		RECOGNIZE_TERNARY_PRIMITIVES,
		RECOGNIZE_LOGIC_CASES,
		RECOGNIZE_EXTREMUM_CASES, // minimum and maximum
		RECOGNIZE_SUM_CASES,
		RECOGNIZE_COUNT_CASES,
		RECOGNIZE_NVALUES_CASES,
		CONVERT_INTENSION_TO_EXTENSION_ARITY_LIMIT, // set it to 0 for deactivating "intension to extension" conversion
		CONVERT_INTENSION_TO_EXTENSION_SPACE_LIMIT,
		RECOGNIZING_BEFORE_CONVERTING;
	}

	/**
	 * The class that contains all data structures (objects) that are used during the process of loading the XCSP3
	 * instance.
	 * 
	 * @author lecoutre
	 *
	 */
	static class Implem {
		/** The object used to load integer constraints. */
		public final CtrLoaderInteger ctrLoaderInteger;

		/** The object used to load symbolic constraints. */
		public final CtrLoaderSymbolic ctrLoaderSymbolic;

		/** The cache used to avoid creating several times similar domains. */
		public Map<IDom, Object> cache4DomObject;

		/** The cache used to avoid creating several times similar tables (arrays of tuples). */
		public Map<Object, int[][]> cache4Tuples;

		/** The map containing the current parameters that are used to pilot the parser. */
		public final Map<XCallbacksParameters, Object> currParameters;

		public Set<String> allIds;

		/** The set that is used to determine if a "recognized" constraint has really be posted or not. */
		public Set<String> postedRecognizedCtrs;

		/**
		 * The limit on the size of the Cartesian product of the domains of the variables, for trying a conversion
		 * (intension to extension).
		 */
		public static final Long CONVERSION_SPACE_LIMIT = 1000000L;

		/**
		 * Makes current parameters in raw form, meaning that constraints will be given in their very original forms.
		 */
		public void rawParameters() {
			currParameters.clear(); // we don't try to recognize anything
			currParameters.put(XCallbacksParameters.CONVERT_INTENSION_TO_EXTENSION_ARITY_LIMIT, 0); // we don't make any
																									// conversion (since
																									// arity 0)
			currParameters.put(XCallbacksParameters.CONVERT_INTENSION_TO_EXTENSION_SPACE_LIMIT, CONVERSION_SPACE_LIMIT);
			currParameters.put(XCallbacksParameters.RECOGNIZING_BEFORE_CONVERTING, Boolean.TRUE);
		}

		/**
		 * Returns a map with the default parameters that can be used to pilot the parser. When parsing, by default the
		 * parser will try for example to recognize primitives and special cases of constraints count and nValues.
		 * 
		 * @return a map with the default values that can be used to pilot the parser.
		 */
		private Map<XCallbacksParameters, Object> defaultParameters() {
			Object dummy = new Object();
			Map<XCallbacksParameters, Object> map = new HashMap<>();
			// we need a dummy object to put (deactivate) all these properties.
			map.put(XCallbacksParameters.RECOGNIZE_UNARY_PRIMITIVES, dummy);
			map.put(XCallbacksParameters.RECOGNIZE_BINARY_PRIMITIVES, dummy);
			map.put(XCallbacksParameters.RECOGNIZE_TERNARY_PRIMITIVES, dummy);
			map.put(XCallbacksParameters.RECOGNIZE_LOGIC_CASES, dummy);
			map.put(XCallbacksParameters.RECOGNIZE_SUM_CASES, dummy);
			map.put(XCallbacksParameters.RECOGNIZE_EXTREMUM_CASES, dummy);
			map.put(XCallbacksParameters.RECOGNIZE_COUNT_CASES, dummy);
			map.put(XCallbacksParameters.RECOGNIZE_NVALUES_CASES, dummy);
			map.put(XCallbacksParameters.CONVERT_INTENSION_TO_EXTENSION_ARITY_LIMIT, 0); // no conversion by default
																							// (since arity 0)
			map.put(XCallbacksParameters.CONVERT_INTENSION_TO_EXTENSION_SPACE_LIMIT, CONVERSION_SPACE_LIMIT);
			map.put(XCallbacksParameters.RECOGNIZING_BEFORE_CONVERTING, Boolean.TRUE);
			return map;
		}

		/**
		 * Resets the structures used when parsing a specific instance (e.g., caches for ids and tables).
		 */
		public void resetStructures() {
			cache4DomObject = new HashMap<>();
			cache4Tuples = new HashMap<>();
			allIds = new HashSet<>();
			postedRecognizedCtrs = new HashSet<>();
		}

		/**
		 * Builds the object that will be used during the process of loading an XCSP3 instance.
		 * 
		 * @param xc
		 *            the object XCallbacks for which this object is attached to
		 */
		public Implem(XCallbacks xc) {
			ctrLoaderInteger = new CtrLoaderInteger(xc);
			ctrLoaderSymbolic = new CtrLoaderSymbolic(xc);
			currParameters = defaultParameters();
			resetStructures();
		}

		private int nextCtrId, nextLogId;

		public String manageIdFor(ParsingEntry ae) {
			if (ae.id != null) {
				Utilities.control(!allIds.contains(ae.id), "Duplicate id " + ae.id);
				Utilities.control(Stream.of(Constants.KEYWORDS).allMatch(k -> !k.equals(ae.id)), "The id " + ae.id + " is a keyword, and so cannot be used.");
			}
			if (ae.id != null)
				allIds.add(ae.id);
			else {
				// we want an id for each constraint (note that each variable has necessary already an id)
				if (ae instanceof XCtr) {
					while (allIds.contains("c_" + nextCtrId))
						nextCtrId++;
					ae.id = "c_" + nextCtrId;
					allIds.add(ae.id);
					nextCtrId++;
				}
				if (ae instanceof XLogic) {
					while (allIds.contains("m_" + nextLogId))
						nextLogId++;
					ae.id = "m_" + nextLogId;
					allIds.add(ae.id);
					nextLogId++;
				}
			}
			return ae.id;
		}
	}

	/**
	 * Returns the object that implements necessary data structures during the loading process. In your class
	 * implementing XCallbacks, you should simply write something like:
	 * 
	 * <pre>
	 * {@code
	 * 	 Implem implem = new Implem(this);
	 *   
	 *   &#64;Override
	 *   public Implem implem() {
	 *   	return implem;
	 *   }
	 * }
	 * </pre>
	 * 
	 * @return the object that implements some data structures used during the loading process
	 */
	abstract Implem implem();

	/**
	 * Method that must be called when an intercepted ("recognized") constraint cannot be dealt with, and so the
	 * constraint must be resent to the parser so as to be treated classically.
	 * 
	 * @param constraintId
	 *            the id of a constraint
	 */
	default void repost(String constraintId) {
		if (XParser.VERBOSE)
			System.out.println("\t=> Reposting constraint with id " + constraintId);
		implem().postedRecognizedCtrs.remove(constraintId);
	}

	/**
	 * Throws a runtime exception because a piece of code is not implemented. The specified objects are simply displayed
	 * to give information about the problem to fix.
	 * 
	 * @param objects
	 *            objects to be displayed (with toString())
	 * @return a fake object because the exception will quit first.
	 */
	default Object unimplementedCase(Object... objects) {
		throw new RuntimeException("Unimplemented case " + Stream.of(objects).map(o -> o.toString()).collect(Collectors.joining("\n")));
	}

	/**********************************************************************************************
	 * Main Methods for loading variables, constraints and objectives
	 *********************************************************************************************/

	/**
	 * Loads the XML document corresponding to the XCSP3 instance whose filename is given. This method has to be
	 * overridden when special tools are required to load the file.
	 * 
	 * @param fileName
	 *            the name of an XCSP3 file
	 * @return the document corresponding to the XCSP3 file whose filename is given
	 */
	default Document loadDocument(String fileName) throws Exception {
		return Utilities.loadDocument(fileName);
	}

	/**
	 * Loads and parses the XCSP3 instance represented by the specified document. The optional specified classes
	 * indicate which elements (variables, constraints) must be discarded when parsing; for example, one may wish to
	 * ignore all constraints related to "symmetryBreaking". Normally, this method should not be overridden.
	 * 
	 * @param document
	 *            the document representing the XCSP3 instance
	 * @param discardedClasses
	 *            the name of the classes (tags) of elements (variables, constraints) that must be discarded when
	 *            parsing
	 * @throws Exception
	 */
	default void loadInstance(Document document, String... discardedClasses) throws Exception {
		implem().resetStructures();
		XParser parser = new XParser(document, discardedClasses);
		beginInstance(parser.typeFramework);
		beginVariables(parser.vEntries);
		loadVariables(parser);
		endVariables();
		beginConstraints(parser.cEntries);
		loadConstraints(parser);
		endConstraints();
		beginObjectives(parser.oEntries, parser.typeCombination);
		loadObjectives(parser);
		endObjectives();
		beginAnnotations(parser.aEntries);
		loadAnnotations(parser);
		endAnnotations();
		endInstance();
	}

	/**
	 * Loads and parses the XCSP3 instance whose filename is given. The optional specified classes indicate which
	 * elements (variables, constraints) must be discarded when parsing; for example, one may wish to ignore all
	 * constraints related to "symmetryBreaking". Normally, this method should not be overridden.
	 * 
	 * @param fileName
	 *            the name of an XCSP3 file
	 * @param discardedClasses
	 *            the name of the classes (tags) of elements (variables, constraints) that must be discarded when
	 *            parsing
	 * @throws Exception
	 */
	default void loadInstance(String fileName, String... discardedClasses) throws Exception {
		loadInstance(loadDocument(fileName), discardedClasses);
	}

	/**
	 * Loads all elements that are contained in the element &lt;variables&gt; of the XCSP3 instance, which have been
	 * parsed by the specified parser object. Except for some advanced uses, this method should not be overridden.
	 * 
	 * @param parser
	 *            the object used to parse the element <variables>
	 */
	default void loadVariables(XParser parser) {
		for (VEntry entry : parser.vEntries) {
			try {
				if (entry instanceof XVar)
					loadVar((XVar) entry);
				else {
					beginArray((XArray) entry);
					loadArray((XArray) entry);
					endArray((XArray) entry);
				}
			} catch (ClassCastException e) {
				throw new WrongTypeException("in declaration of variable with id \"" + entry.id + "\": does domain correspond to the declared type ?");
			}
		}
		// for (VEntry entry : parser.vEntries) {
		// if (entry instanceof XArray) {
		// int n = (int) Stream.of(((XArray) entry).vars).filter(x -> x == null).count();
		// System.out.println("N=" + n);
		// }
		// }

	}

	/**
	 * Loads the specified variable. One callback function 'buildVarInteger' or 'buildVarSymbolic' is called when this
	 * method is executed. Except for some advanced uses, this method should not be overridden.
	 * 
	 * @param v
	 *            the variable to be loaded
	 */
	default void loadVar(XVar v) {
		implem().manageIdFor(v);
		if (v.degree == 0)
			return;
		Object domObject = implem().cache4DomObject.get(v.dom);
		if (domObject == null) {
			if (v.dom instanceof Dom) {
				IntegerEntity[] pieces = (IntegerEntity[]) ((Dom) v.dom).values;
				if (pieces.length == 1 && pieces[0] instanceof IntegerInterval)
					domObject = pieces[0];
				else {
					int[] values = IntegerEntity.toIntArray(pieces, CtrLoaderInteger.N_MAX_VALUES);
					Utilities.control(values != null, "Too many values. You have to extend the parser.");
					domObject = values;
				}
			} else if (v.dom instanceof DomSymbolic)
				domObject = ((DomSymbolic) v.dom).values;
			else
				unimplementedCase(v.dom);
			implem().cache4DomObject.put(v.dom, domObject); // = trDom(v.dom));
		}
		if (domObject instanceof IntegerInterval) {
			IntegerInterval ii = (IntegerInterval) domObject;
			int min = Utilities.safeIntWhileHandlingInfinity(ii.inf);
			int max = Utilities.safeIntWhileHandlingInfinity(ii.sup);
			buildVarInteger((XVarInteger) v, min, max);
		} else if (domObject instanceof int[])
			buildVarInteger((XVarInteger) v, (int[]) domObject);
		else if (domObject instanceof String[])
			buildVarSymbolic((XVarSymbolic) v, (String[]) domObject);
		else
			unimplementedCase(v);
	}

	/**
	 * Loads the specified array of variables. All non-null variables of the array are iterated over and loaded. Except
	 * for some advanced uses, this method should not be overridden.
	 * 
	 * @param va
	 *            the array of variables to be loaded
	 */
	default void loadArray(XArray va) {
		implem().manageIdFor(va);
		Stream.of(va.vars).filter(v -> v != null).forEach(v -> loadVar(v));
	}

	/**
	 * Loads all elements that are contained in the element &lt;constraints&gt; of the XCSP3 instance, which have been
	 * parsed by the specified parser object. Except for some advanced uses, this method should not be overridden.
	 * 
	 * @param parser
	 *            the object used to parse the element <constraints>
	 */
	default void loadConstraints(XParser parser) {
		loadConstraints(parser.cEntries); // recursive loading process (through potential blocks)
	}

	/**
	 * Loads all constraints that can be found in the specified list. This method is recursive, allowing us to deal with
	 * blocks and groups. Normally, this method should not be overridden.
	 * 
	 * @param list
	 *            a list of elements from <constraints> that must be parsed.
	 */
	default void loadConstraints(List<CEntry> list) {
		for (CEntry entry : list) {
			if (entry instanceof XBlock)
				loadBlock((XBlock) entry);
			else if (entry instanceof XGroup)
				loadGroup((XGroup) entry);
			else if (entry instanceof XSlide)
				loadSlide((XSlide) entry);
			else if (entry instanceof XLogic) {
				loadLogic((XLogic) entry);
			} else if (entry instanceof XCtr) {
				try {
					loadCtr((XCtr) entry);
				} catch (ClassCastException e) {
					e.printStackTrace();
					throw new WrongTypeException("Wrong parameter type in constraint:\n" + entry + "\n" + e);
				}
			} else
				unimplementedCase(entry);
		}
	}

	/**
	 * Loads a block from <constraints>. Normally, this method should not be overridden.
	 * 
	 * @param b
	 *            the block to be loaded.
	 */
	default void loadBlock(XBlock b) {
		implem().manageIdFor(b);
		beginBlock(b);
		loadConstraints(b.subentries); // recursive call
		endBlock(b);
	}

	/**
	 * Loads a group from <constraints>. Normally, this method should not be overridden.
	 * 
	 * @param g
	 *            the group to be loaded.
	 */
	default void loadGroup(XGroup g) {
		implem().manageIdFor(g);
		beginGroup(g);
		if (g.template instanceof XCtr)
			loadCtrs((XCtr) g.template, g.argss, g);
		else
			unimplementedCase(g);
		endGroup(g);
	}

	/**
	 * Loads a meta-constraint slide. Normally, this method should not be overridden.
	 * 
	 * @param s
	 *            the meta-constraint slide to be loaded.
	 */
	default void loadSlide(XSlide s) {
		implem().manageIdFor(s);
		beginSlide(s);
		loadCtrs((XCtr) s.template, s.scopes, s);
		endSlide(s);
	}

	/**
	 * Loads a meta-constraint based on a logical form (including control ones). This corresponds to meta-constraints
	 * {@code <and>, <or>, <iff>, <not>, <ifThen> or <ifThenElse>}. Normally, this method should not be overridden.
	 * 
	 * @param l
	 *            the logic-based meta-constraint to be loaded.
	 */
	default void loadLogic(XLogic l) {
		implem().manageIdFor(l);
		beginLogic(l);
		loadConstraints(Arrays.asList(l.components)); // recursive call
		endLogic(l);
	}

	/**
	 * Loads all constraints that can be built from the specified template and the specified array of arguments. For
	 * each value between 0 and argss.length, a constraint is built. Normally, this method should not be overridden.
	 * 
	 * @param template
	 *            a constraint template
	 * @param argss
	 *            an array of arguments
	 * @param entry
	 *            the object at the origin of the abstraction
	 */
	default void loadCtrs(XCtr template, Object[][] argss, CEntry entry) {
		Stream.of(argss).forEach(args -> {
			template.id = null; // because the template object is shared
			template.abstraction.concretize(args);
			loadCtr(template);
		}); // TODO : be careful, the object template is simply modified; for parallel stuff, it should be rebuilt
			// entirely
	}

	/**
	 * Loads the specified constraint. One callback function (for example, builCtrIntension or buildCtrAllDifferent) is
	 * called when this method is executed. Except for some advanced uses, this method should not be overridden.
	 * 
	 * @param c
	 *            the constraint to be loaded
	 */
	default void loadCtr(XCtr c) {
		implem().manageIdFor(c);
		CChild[] childs = c.childs;
		Utilities.control(Stream.of(TypeChild.cost, TypeChild.set, TypeChild.mset).noneMatch(t -> t == childs[childs.length - 1].type),
				"soft, set and mset currently not implemented");
		if (Stream.of(c.vars()).allMatch(x -> x instanceof XVarInteger)) {
			implem().ctrLoaderInteger.load(c);
		} else if (Stream.of(c.vars()).allMatch(x -> x instanceof XVarSymbolic)) {
			implem().ctrLoaderSymbolic.load(c);
		} else
			unimplementedCase(c);
	}

	/**
	 * Loads all elements that are contained in the element <objectives> of the XCSP3 instance, which have been parsed
	 * by the specified parser object. Except for some advanced uses, this method should not be overridden.
	 * 
	 * @param parser
	 *            the object used to parse the element <objectives>
	 */
	default void loadObjectives(XParser parser) {
		parser.oEntries.stream().forEach(entry -> loadObj((XObj) entry));
	}

	/**
	 * Loads the specified objective. One callback function (for example, builObjToMinimize or buildObjToMaximize) is
	 * called when this method is executed. Except for some advanced uses, this method should not be overridden.
	 * 
	 * @param o
	 *            the objective to be loaded
	 */
	default void loadObj(XObj o) {
		implem().manageIdFor(o);
		if (o.type == TypeObjective.EXPRESSION) {
			XNode<?> node = ((OObjectiveExpr) o).rootNode;
			if (node.getType() == TypeExpr.VAR) {
				if (o.minimize)
					buildObjToMinimize(o.id, (XVarInteger) ((XNodeLeaf<?>) node).value);
				else
					buildObjToMaximize(o.id, (XVarInteger) ((XNodeLeaf<?>) node).value);
			} else {
				if (o.minimize)
					buildObjToMinimize(o.id, (XNodeParent<XVarInteger>) node);
				else
					buildObjToMaximize(o.id, (XNodeParent<XVarInteger>) node);
			}
		} else {
			Object[] terms = ((OObjectiveSpecial) o).terms;
			SimpleValue[] vals = ((OObjectiveSpecial) o).coeffs;
			int[] coeffs = vals == null ? null : Stream.of(vals).mapToInt(val -> Utilities.safeInt(((IntegerValue) val).v)).toArray();
			if (coeffs == null) {
				if (o.minimize) {
					if (terms[0] instanceof XVarInteger)
						buildObjToMinimize(o.id, o.type, (XVarInteger[]) terms);
					else
						buildObjToMinimize(o.id, o.type, (XNode<XVarInteger>[]) terms);
				} else {
					if (terms[0] instanceof XVarInteger)
						buildObjToMaximize(o.id, o.type, (XVarInteger[]) terms);
					else
						buildObjToMaximize(o.id, o.type, (XNode<XVarInteger>[]) terms);
				}
			} else {
				if (o.minimize) {
					if (terms[0] instanceof XVarInteger)
						buildObjToMinimize(o.id, o.type, (XVarInteger[]) terms, coeffs);
					else
						buildObjToMinimize(o.id, o.type, (XNode<XVarInteger>[]) terms, coeffs);
				} else if (terms[0] instanceof XVarInteger)
					buildObjToMaximize(o.id, o.type, (XVarInteger[]) terms, coeffs);
				else
					buildObjToMaximize(o.id, o.type, (XNode<XVarInteger>[]) terms, coeffs);
			}
		}
	}

	default void loadAnnotations(XParser parser) {
		Object obj = parser.aEntries.get(Constants.DECISION);
		if (obj != null)
			buildAnnotationDecision((XVarInteger[]) obj);
	}

	/**********************************************************************************************
	 * Methods called at Specific Moments
	 *********************************************************************************************/

	/**
	 * Method called at the very beginning of the process of loading the XCSP3 instance. Implement (or redefine) this
	 * method (if you implement XCallbacks2) in case you want some special operation to be executed (for example, for
	 * debugging).
	 * 
	 * @param type
	 *            the framework of the XCSP3 instance
	 */
	void beginInstance(TypeFramework type);

	/**
	 * Method called at the end of the process of loading the XCSP3 instance. Implement (or redefine) this method (if
	 * you implement XCallbacks2) in case you want some special operation to be executed (for example, for debugging).
	 */
	void endInstance();

	/**
	 * Method called at the beginning of the process of loading the variables of the XCSP3 instance. Implement (or
	 * redefine) this method (if you implement XCallbacks2) in case you want some special operation to be executed (for
	 * example, for debugging).
	 * 
	 * @param vEntries
	 *            the list of objects found in <variables>
	 */
	void beginVariables(List<VEntry> vEntries);

	/**
	 * Method called at the end of the process of loading the variables of the XCSP3 instance. Implement (or redefine)
	 * this method (if you implement XCallbacks2) in case you want some special operation to be executed (for example,
	 * for debugging).
	 */
	void endVariables();

	/**
	 * Method called at the beginning of the process of loading the specified array of variables. Implement (or
	 * redefine) this method (if you implement XCallbacks2) in case you want some special operation to be executed (for
	 * example, for debugging).
	 * 
	 * @param a
	 *            an object representing an array of variables
	 */
	void beginArray(XArray a);

	/**
	 * Method called at the end of the process of loading the specified array of variables. Implement (or redefine) this
	 * method (if you implement XCallbacks2) in case you want some special operation to be executed (for example, for
	 * debugging).
	 * 
	 * @param a
	 *            an object representing an array of variables
	 */
	void endArray(XArray a);

	/**
	 * Method called at the beginning of the process of loading the constraints of the XCSP3 instance. Implement (or
	 * redefine) this method (if you implement XCallbacks2) in case you want some special operation to be executed (for
	 * example, for debugging).
	 * 
	 * @param cEntries
	 *            the list of objects found in <constraints>
	 */
	void beginConstraints(List<CEntry> cEntries);

	/**
	 * Method called at the end of the process of loading the constraints of the XCSP3 instance. Implement (or redefine)
	 * this method (if you implement XCallbacks2) in case you want some special operation to be executed (for example,
	 * for debugging).
	 */
	void endConstraints();

	/**
	 * Method called at the beginning of the process of loading the specified block. Implement (or redefine) this method
	 * (if you implement XCallbacks2) in case you want some special operation to be executed (for example, for
	 * debugging).
	 * 
	 * @param b
	 *            a block to be loaded
	 */
	void beginBlock(XBlock b);

	/**
	 * Method called at the end of the process of loading the specified block. Implement (or redefine) this method (if
	 * you implement XCallbacks2) in case you want some special operation to be executed (for example, for debugging).
	 * 
	 * @param b
	 *            a block
	 */
	void endBlock(XBlock b);

	/**
	 * Method called at the beginning of the process of loading the specified group of constraints. Implement (or
	 * redefine) this method (if you implement XCallbacks2) in case you want some special operation to be executed (for
	 * example, for debugging).
	 * 
	 * @param g
	 *            a group to be loaded
	 */
	void beginGroup(XGroup g);

	/**
	 * Method called at the end of the process of loading the specified group of constraints. Implement (or redefine)
	 * this method (if you implement XCallbacks2) in case you want some special operation to be executed (for example,
	 * for debugging).
	 * 
	 * @param g
	 *            a group
	 */
	void endGroup(XGroup g);

	/**
	 * Method called at the beginning of the process of loading the specified meta-constraint slide. Implement (or
	 * redefine) this method (if you implement XCallbacks2) in case you want some special operation to be executed (for
	 * example, for debugging).
	 * 
	 * @param s
	 *            a meta-constraint slide to be loaded
	 */
	void beginSlide(XSlide s);

	/**
	 * Method called at the end of the process of loading the specified meta-constraint slide. Implement (or redefine)
	 * this method (if you implement XCallbacks2) in case you want some special operation to be executed (for example,
	 * for debugging).
	 * 
	 * @param s
	 *            a meta-constraint slide
	 */
	void endSlide(XSlide s);

	/**
	 * Method called at the beginning of the process of loading the specified logic-based meta-constraint
	 * {@code <and>, <or>, <iff>, <not>, <ifThen> or <ifThenElse>}. Implement (or redefine) this method (if you
	 * implement XCallbacks2).
	 * 
	 * @param l
	 *            a logic-based meta-constraint to be loaded
	 */
	void beginLogic(XLogic l);

	/**
	 * Method called at the end of the process of loading the specified logic-based meta-constraint
	 * {@code <and>, <or>, <iff>, <not>, <ifThen> or <ifThenElse>}. Implement (or redefine) this method (if you
	 * implement XCallbacks2) in case you want some special operation to be executed (for example, for debugging).
	 * 
	 * @param l
	 *            a logic-based meta-constraint
	 */
	void endLogic(XLogic l);

	/**
	 * Method called at the beginning of the process of loading the objectives (if any) of the XCSP3 instance. Implement
	 * (or redefine) this method (if you implement XCallbacks2) in case you want some special operation to be executed
	 * (for example, for debugging).
	 * 
	 * @param oEntries
	 *            the list of objects found in <objectives>
	 * @param type
	 *            the type indicating how to manage multi-optimization; this parameter is irrelevant in case of
	 *            mono-optimization
	 */
	void beginObjectives(List<OEntry> oEntries, TypeCombination type);

	/**
	 * Method called at the end of the process of loading the objectives (if any) of the XCSP3 instance. Implement (or
	 * redefine) this method (if you implement XCallbacks2) in case you want some special operation to be executed (for
	 * example, for debugging).
	 */
	void endObjectives();

	void beginAnnotations(Map<String, Object> aEntries);

	void endAnnotations();

	/**********************************************************************************************
	 * Methods to be implemented on integer variables/constraints
	 *********************************************************************************************/

	/**
	 * Callback method for building in the solver an integer variable whose domain contains all integer values between
	 * the two specified bounds.
	 * 
	 * @param x
	 *            an integer variable built by the parser
	 * @param minValue
	 *            the minimum value of the domain of x
	 * @param maxValue
	 *            the maximum value of the domain of x
	 */
	void buildVarInteger(XVarInteger x, int minValue, int maxValue);

	/**
	 * Callback method for building in the solver an integer variable whose domain is given by the specified array.
	 * 
	 * @param x
	 *            an integer variable built by the parser
	 * @param values
	 *            the values in the domain of x
	 */
	void buildVarInteger(XVarInteger x, int[] values);

	/**
	 * Callback method for building in the solver an initially entailed (i.e., universally satisfied) constraint. By
	 * default, this method does nothing. You should redefine it if you need to preserve all constraints (e.g, for
	 * MaxCSP).
	 * 
	 * @param id
	 *            the id of the constraint
	 * @param list
	 *            the list of variables of the constraint
	 */
	default void buildCtrTrue(String id, XVar[] list) {
	}

	/**
	 * Callback method for building in the solver an initially disentailed (i.e., universally unsatisfied) constraint.
	 * By default, this method throws an exception. You should redefine it if you can deal with such very special
	 * constraints.
	 * 
	 * @param id
	 *            the id of the constraint
	 * @param list
	 *            the list of variables of the constraint
	 */
	default void buildCtrFalse(String id, XVar[] list) {
		throw new RuntimeException("Constraint with only conflicts");
	}

	/**
	 * Callback method for building a constraint <code>intension</code> from the specified syntactic tree. Variables of
	 * the specified array of variables are exactly those that are present in the tree.
	 * 
	 * @param id
	 *            the id of the constraint
	 * @param scope
	 *            the list of integer variables of the constraint
	 * @param tree
	 *            the root of a syntactic tree representing the predicate associated with the constraint
	 */
	void buildCtrIntension(String id, XVarInteger[] scope, XNodeParent<XVarInteger> tree);

	/**
	 * Callback method for building an unary primitive constraint with one of the following forms:
	 * <ul>
	 * <li>x < k</li>
	 * <li>x &le; k</li>
	 * <li>x &ge; k</li>
	 * <li>x > k</li>
	 * <li>x = k</li>
	 * <li>x &ne; k</li>
	 * </ul>
	 * with x being an integer variable and k a constant (integer).
	 * 
	 * @param id
	 *            the id of the constraint
	 * @param x
	 *            an integer variable
	 * @param op
	 *            a relational operator
	 * @param k
	 *            a constant (integer)
	 */
	void buildCtrPrimitive(String id, XVarInteger x, TypeConditionOperatorRel op, int k);

	/**
	 * Callback method for building an unary primitive constraint with one of the following forms:
	 * <ul>
	 * <li>x &isin; t</li>
	 * <li>x &notin; t</li>
	 * </ul>
	 * with x being an integer variable and t a set of constants (integers) represented by an array.
	 * 
	 * @param id
	 *            the id of the constraint
	 * @param x
	 *            an integer variable
	 * @param op
	 *            a set operator
	 * @param t
	 *            a set (array) of constants (integers)
	 */
	void buildCtrPrimitive(String id, XVarInteger x, TypeConditionOperatorSet op, int[] t);

	/**
	 * Callback method for building an unary primitive constraint with one of the following forms:
	 * <ul>
	 * <li>x &isin; min..max</li>
	 * <li>x &notin; min..max</li>
	 * </ul>
	 * with x being an integer variable and min and max two constants (integers) denoting the bounds of an integer
	 * interval.
	 * 
	 * @param id
	 *            the id of the constraint
	 * @param x
	 *            an integer variable
	 * @param op
	 *            a set operator
	 * @param min
	 *            the minimum value of the interval
	 * @param max
	 *            the maximum value of the interval
	 */
	void buildCtrPrimitive(String id, XVarInteger x, TypeConditionOperatorSet op, int min, int max);

	/**
	 * Callback method for building an unary primitive constraint with one of the following forms:
	 * <ul>
	 * <li>(x + p) &odot; k</li>
	 * <li>(x - p) &odot; k</li>
	 * <li>(x * p) &odot; k</li>
	 * <li>(x / p) &odot; k</li>
	 * <li>(x % p) &odot; k</li>
	 * <li>(x ^ p) &odot; k</li>
	 * <li>|x - p| &odot; k</li>
	 * </ul>
	 * with x being an integer variable, p and k constants (integers) and &odot; a relational operator in
	 * {<,&le;,&ge;,>,=,&ne;}
	 * 
	 * @param id
	 *            the id of the constraint
	 * @param x
	 *            an integer variable
	 * @param aop
	 *            an arithmetic operator
	 * @param p
	 *            a constant (integer)
	 * @param op
	 *            a relational operator
	 * @param k
	 *            a constant (integer)
	 */
	void buildCtrPrimitive(String id, XVarInteger x, TypeArithmeticOperator aop, int p, TypeConditionOperatorRel op, int k);

	// /**
	// * Callback method for building an unary primitive constraint with one of the following forms:
	// * <ul>
	// * <li>(x + p) &odot; t</li>
	// * <li>(x - p) &odot; t</li>
	// * <li>(x * p) &odot; t</li>
	// * <li>(x / p) &odot; t</li>
	// * <li>(x % p) &odot; t</li>
	// * <li>|x - p| &odot; t</li>
	// * </ul>
	// * with x being an integer variable, p a constant (integer), &odot; a set operator in {&isin;&notin;} and t a set
	// of constants
	// (integers) represented by
	// an
	// * array.
	// *
	// * @param id
	// * the id of the constraint
	// * @param x
	// * an integer variable
	// * @param aop
	// * an arithmetic operator
	// * @param p
	// * a constant (integer)
	// * @param op
	// * a relational operator
	// * @param t
	// * a set (array) of constants (integers)
	// */
	// void buildCtrPrimitive(String id, XVarInteger x, TypeArithmeticOperator aop, int p, TypeConditionOperatorSet op,
	// int[] t);

	/**
	 * Callback method for building a binary primitive constraint with one of the following forms:
	 * <ul>
	 * <li>x = |y|</li>
	 * <li>x = -y</li>
	 * <li>x = y*y</li>
	 * </ul>
	 * with x, and y being two integer variables.
	 * 
	 * @param id
	 *            the id of the constraint
	 * @param x
	 *            an integer variable
	 * @param aop
	 *            a unary arithmetic operator
	 * @param y
	 *            an integer variable
	 */
	void buildCtrPrimitive(String id, XVarInteger x, TypeUnaryArithmeticOperator aop, XVarInteger y);

	/**
	 * Callback method for building a binary primitive constraint with one of the following forms:
	 * <ul>
	 * <li>(x + y) &odot; k</li>
	 * <li>(x - y) &odot; k</li>
	 * <li>(x * y) &odot; k</li>
	 * <li>(x / y) &odot; k</li>
	 * <li>(x % y) &odot; k</li>
	 * <li>(x ^ y) &odot; k</li>
	 * <li>|x - y| &odot; k</li>
	 * </ul>
	 * with x and y being two integer variables, k a constant (integer) and &odot; a relational operator in
	 * {<,&le;,&ge;,>,=,&ne;}
	 * 
	 * @param id
	 *            the id of the constraint
	 * @param x
	 *            an integer variable
	 * @param aop
	 *            an arithmetic operator
	 * @param y
	 *            an integer variable
	 * @param op
	 *            a relational operator
	 * @param k
	 *            a constant (integer)
	 */
	void buildCtrPrimitive(String id, XVarInteger x, TypeArithmeticOperator aop, XVarInteger y, TypeConditionOperatorRel op, int k);

	/**
	 * Callback method for building a binary primitive constraint with one of the following forms:
	 * <ul>
	 * <li>(x + p) &odot; y</li>
	 * <li>(x - p) &odot; y</li>
	 * <li>(x * p) &odot; y</li>
	 * <li>(x / p) &odot; y</li>
	 * <li>(x % p) &odot; y</li>
	 * <li>(x ^ p) &odot; y</li>
	 * <li>|x - p| &odot; y</li>
	 * </ul>
	 * with x and y being two integer variables, p a constant (integer) and &odot; a relational operator in
	 * {<,&le;,&ge;,>,=,&ne;}
	 * 
	 * @param id
	 *            the id of the constraint
	 * @param x
	 *            an integer variable
	 * @param aop
	 *            an arithmetic operator
	 * @param p
	 *            a constant (integer)
	 * @param op
	 *            a relational operator
	 * @param y
	 *            an integer variable
	 */
	void buildCtrPrimitive(String id, XVarInteger x, TypeArithmeticOperator aop, int p, TypeConditionOperatorRel op, XVarInteger y);

	/**
	 * Callback method for building a ternary primitive constraint with one of the following forms:
	 * <ul>
	 * <li>(x + y) &odot; z</li>
	 * <li>(x - y) &odot; z</li>
	 * <li>(x * y) &odot; z</li>
	 * <li>(x / y) &odot; z</li>
	 * <li>(x % y) &odot; z</li>
	 * <li>(x ^ y) &odot; z</li>
	 * <li>|x - y| &odot; z</li>
	 * </ul>
	 * with x, y and z being three integer variables, and &odot; a relational operator in {<,&le;,&ge;,>,=,&ne;}
	 * 
	 * @param id
	 *            the id of the constraint
	 * @param x
	 *            an integer variable
	 * @param aop
	 *            an arithmetic operator
	 * @param y
	 *            an integer variable
	 * @param op
	 *            a relational operator
	 * @param z
	 *            an integer variable
	 */
	void buildCtrPrimitive(String id, XVarInteger x, TypeArithmeticOperator aop, XVarInteger y, TypeConditionOperatorRel op, XVarInteger z);

	/**
	 * Callback method for building a logic constraint with one of the following forms: *
	 * <ul>
	 * <li>and(x1,x2,...,xr)</li>
	 * <li>or(x1,x2,...,xr)</li>
	 * <li>xor(x1,x2,...,xr)</li>
	 * <li>iff(x1,x2,...,xr)</li>
	 * <li>imp(x1,x2)</li>
	 * </ul>
	 * with x1,x2,..., xr being 0/1 variables
	 * 
	 * @param id
	 *            the id of the constraint
	 * @param lop
	 *            a logical operator
	 * @param vars
	 *            a set (array) of 0/1 variables
	 */
	void buildCtrLogic(String id, TypeLogicalOperator lop, XVarInteger[] vars);

	/**
	 * Callback method for building a logic constraint with one of the following forms: *
	 * <ul>
	 * <li>x = and(x1,x2,...,xr)</li>
	 * <li>x = or(x1,x2,...,xr)</li>
	 * <li>x = xor(x1,x2,...,xr)</li>
	 * <li>x = iff(x1,x2,...,xr)</li>
	 * <li>x = imp(x1,x2)</li>
	 * <li>x &ne; and(x1,x2,...,xr)</li>
	 * <li>x &ne; or(x1,x2,...,xr)</li>
	 * <li>x &ne; xor(x1,x2,...,xr)</li>
	 * <li>x &ne; iff(x1,x2,...,xr)</li>
	 * <li>x &ne; imp(x1,x2)</li>
	 * </ul>
	 * with x1,x2,..., xr being 0/1 variables
	 * 
	 * @param id
	 *            the id of the constraint
	 * @param x
	 *            a 0/1 variable
	 * @param op
	 *            either the operator EQ or the operator NE
	 * @param lop
	 *            a logical operator
	 * @param vars
	 *            a set (array) of 0/1 variables
	 */
	void buildCtrLogic(String id, XVarInteger x, TypeEqNeOperator op, TypeLogicalOperator lop, XVarInteger[] vars);

	/**
	 * Callback method for building a "logic" constraint with the following form:
	 * <ul>
	 * <li>x = (y &odot; k)</li>
	 * </ul>
	 * with x a 0/1 variable, y an integer variable, k a constant (integer) and &odot; a relational operator in
	 * {<,&le;,&ge;,>,=,&ne;}
	 * 
	 * @param id
	 *            the id of the constraint
	 * @param x
	 *            a 0/1 variable
	 * @param y
	 *            an integer variable
	 * @param op
	 *            a relational operator
	 * @param k
	 *            a constant (integer)
	 */
	void buildCtrLogic(String id, XVarInteger x, XVarInteger y, TypeConditionOperatorRel op, int k);

	/**
	 * Callback method for building a "logic" constraint with the following form:
	 * <ul>
	 * <li>x = (y &odot; z)</li>
	 * </ul>
	 * with x a 0/1 variable, y and z two integer variables, and &odot; a relational operator in {<,&le;,&ge;,>,=,&ne;}
	 * 
	 * @param id
	 *            the id of the constraint
	 * @param x
	 *            a 0/1 variable
	 * @param y
	 *            an integer variable
	 * @param op
	 *            a relational operator
	 * @param z
	 *            an integer variable
	 */
	void buildCtrLogic(String id, XVarInteger x, XVarInteger y, TypeConditionOperatorRel op, XVarInteger z);

	/**
	 * Callback method for building a unary extensional constraint. Values are supports (accepted by the constraint) iff
	 * the specified Boolean is true, otherwise they are conflicts (not accepted by the constraint). The flag
	 * STARRED_TUPLES cannot appear in the specified set (because this is a unary constraint). The flag UNCLEAN_TUPLES,
	 * if present, indicates that all specified values do not necessarily belong to the (initial) domain of the
	 * specified variable. More information in <a href="http://xcsp.org/format3.pdf"> the specifications (Chapter
	 * 4)</a>. Quick information available at <a href="http://xcsp.org/specifications"> XCSP3 website (Tab
	 * Specifications).
	 * 
	 * @param id
	 *            the id of the constraint
	 * @param x
	 *            an integer variable
	 * @param values
	 *            supports or conflicts
	 * @param positive
	 *            values are supports iff this value is true
	 * @param flags
	 *            set of flags giving information about the values
	 */
	void buildCtrExtension(String id, XVarInteger x, int[] values, boolean positive, Set<TypeFlag> flags);

	/**
	 * Callback method for building a (non-unary) extensional constraint. Tuples are supports (accepted by the
	 * constraint) iff the specified Boolean is true, otherwise they are conflicts (not accepted by the constraint). The
	 * flag STARRED_TUPLES indicates if the symbol * (denoted by Constants.STAR_INT, whose value is Integer.MAX_VALUE -
	 * 1) is present in some tuple(s). The flag UNCLEAN_TUPLES, if present, indicates that all specified tuples do not
	 * necessarily belong to the (initial) domains of the specified variables. More information in
	 * <a href="http://xcsp.org/format3.pdf"> the specifications (Chapter 4)</a>. Quick information available at
	 * <a href="http://xcsp.org/specifications"> XCSP3 website (Tab Specifications).
	 * 
	 * @param id
	 *            the id of the constraint
	 * @param list
	 *            the scope of the constraint
	 * @param tuples
	 *            supports or conflicts
	 * @param positive
	 *            tuples are supports iff this value is true
	 * @param flags
	 *            set of flags giving information about the tuples
	 */
	void buildCtrExtension(String id, XVarInteger[] list, int[][] tuples, boolean positive, Set<TypeFlag> flags);

	void buildCtrExtension(String id, XVarInteger[] list, AbstractTuple[] tuples, boolean positive, Set<TypeFlag> flags);

	/**
	 * Full information about the constraint (this form) in <a href="http://xcsp.org/format3.pdf"> the specifications
	 * (Chapter 4)</a>. <br>
	 * Quick information available on the <a href="http://xcsp.org/specifications"> XCSP3 website (Tab Specifications)
	 * </a>. <br>
	 * Select the constraint after opening the left navigation bar below heading XCSP3-core.
	 * 
	 */
	void buildCtrRegular(String id, XVarInteger[] list, Transition[] transitions, String startState, String[] finalStates);

	/**
	 * Full information about the constraint (this form) in <a href="http://xcsp.org/format3.pdf"> the specifications
	 * (Chapter 4)</a>. <br>
	 * Quick information available on the <a href="http://xcsp.org/specifications"> XCSP3 website (Tab Specifications)
	 * </a>. <br>
	 * Select the constraint after opening the left navigation bar below heading XCSP3-core.
	 * 
	 */
	void buildCtrMDD(String id, XVarInteger[] list, Transition[] transitions);

	/**
	 * Full information about the constraint (this form) in <a href="http://xcsp.org/format3.pdf"> the specifications
	 * (Chapter 4)</a>. <br>
	 * Quick information available on the <a href="http://xcsp.org/specifications"> XCSP3 website (Tab Specifications)
	 * </a>. <br>
	 * Select the constraint after opening the left navigation bar below heading XCSP3-core.
	 * 
	 */
	void buildCtrAllDifferent(String id, XVarInteger[] list);

	/**
	 * Full information about the constraint (this form) in <a href="http://xcsp.org/format3.pdf"> the specifications
	 * (Chapter 4)</a>. <br>
	 * Quick information available on the <a href="http://xcsp.org/specifications"> XCSP3 website (Tab Specifications)
	 * </a>. <br>
	 * Select the constraint after opening the left navigation bar below heading XCSP3-core.
	 * 
	 */
	void buildCtrAllDifferentExcept(String id, XVarInteger[] list, int[] except);

	/**
	 * Full information about the constraint (this form) in <a href="http://xcsp.org/format3.pdf"> the specifications
	 * (Chapter 4)</a>. <br>
	 * Quick information available on the <a href="http://xcsp.org/specifications"> XCSP3 website (Tab Specifications)
	 * </a>. <br>
	 * Select the constraint after opening the left navigation bar below heading XCSP3-core.
	 * 
	 */
	void buildCtrAllDifferentList(String id, XVarInteger[][] lists);

	/**
	 * Full information about the constraint (this form) in <a href="http://xcsp.org/format3.pdf"> the specifications
	 * (Chapter 4)</a>. <br>
	 * Quick information available on the <a href="http://xcsp.org/specifications"> XCSP3 website (Tab Specifications)
	 * </a>. <br>
	 * Select the constraint after opening the left navigation bar below heading XCSP3-core.
	 * 
	 */
	void buildCtrAllDifferentMatrix(String id, XVarInteger[][] matrix);

	void buildCtrAllDifferentMatrix(String id, XVarInteger[][] matrix, int[] except);

	void buildCtrAllDifferent(String id, XNode<XVarInteger>[] trees);

	/**
	 * Callback method for building a constraint <code>allEqual</code>.
	 * 
	 * @param id
	 *            the id of the constraint
	 * @param list
	 *            the list of variables of the constraint
	 */
	void buildCtrAllEqual(String id, XVarInteger[] list);

	void buildCtrAllEqual(String id, XNode<XVarInteger>[] trees);

	/**
	 * Full information about the constraint (this form) in <a href="http://xcsp.org/format3.pdf"> the specifications
	 * (Chapter 4)</a>. <br>
	 * Quick information available on the <a href="http://xcsp.org/specifications"> XCSP3 website (Tab Specifications)
	 * </a>. <br>
	 * Select the constraint after opening the left navigation bar below heading XCSP3-core.
	 * 
	 */
	void buildCtrOrdered(String id, XVarInteger[] list, TypeOperatorRel operator);

	/**
	 * Full information about the constraint (this form) in <a href="http://xcsp.org/format3.pdf"> the specifications
	 * (Chapter 4)</a>. <br>
	 * Quick information available on the <a href="http://xcsp.org/specifications"> XCSP3 website (Tab Specifications)
	 * </a>. <br>
	 * Select the constraint after opening the left navigation bar below heading XCSP3-core.
	 * 
	 */
	void buildCtrOrdered(String id, XVarInteger[] list, int[] lengths, TypeOperatorRel operator);

	/**
	 * Full information about the constraint (this form) in <a href="http://xcsp.org/format3.pdf"> the specifications
	 * (Chapter 4)</a>. <br>
	 * Quick information available on the <a href="http://xcsp.org/specifications"> XCSP3 website (Tab Specifications)
	 * </a>. <br>
	 * Select the constraint after opening the left navigation bar below heading XCSP3-core.
	 * 
	 */
	void buildCtrOrdered(String id, XVarInteger[] list, XVarInteger[] lengths, TypeOperatorRel operator);

	/**
	 * Full information about the constraint (this form) in <a href="http://xcsp.org/format3.pdf"> the specifications
	 * (Chapter 4)</a>. <br>
	 * Quick information available on the <a href="http://xcsp.org/specifications"> XCSP3 website (Tab Specifications)
	 * </a>. <br>
	 * Select the constraint after opening the left navigation bar below heading XCSP3-core.
	 * 
	 */
	void buildCtrLex(String id, XVarInteger[][] lists, TypeOperatorRel operator);

	/**
	 * Full information about the constraint (this form) in <a href="http://xcsp.org/format3.pdf"> the specifications
	 * (Chapter 4)</a>. <br>
	 * Quick information available on the <a href="http://xcsp.org/specifications"> XCSP3 website (Tab Specifications)
	 * </a>. <br>
	 * Select the constraint after opening the left navigation bar below heading XCSP3-core.
	 * 
	 */
	void buildCtrLexMatrix(String id, XVarInteger[][] matrix, TypeOperatorRel operator);

	void buildCtrPrecedence(String id, XVarInteger[] list, int[] values, boolean covered);

	/**
	 * Full information about the constraint (this form) in <a href="http://xcsp.org/format3.pdf"> the specifications
	 * (Chapter 4)</a>. <br>
	 * Quick information available on the <a href="http://xcsp.org/specifications"> XCSP3 website (Tab Specifications)
	 * </a>. <br>
	 * Select the constraint after opening the left navigation bar below heading XCSP3-core.
	 * 
	 */
	void buildCtrSum(String id, XVarInteger[] list, Condition condition);

	/**
	 * Full information about the constraint (this form) in <a href="http://xcsp.org/format3.pdf"> the specifications
	 * (Chapter 4)</a>. <br>
	 * Quick information available on the <a href="http://xcsp.org/specifications"> XCSP3 website (Tab Specifications)
	 * </a>. <br>
	 * Select the constraint after opening the left navigation bar below heading XCSP3-core.
	 * 
	 */
	void buildCtrSum(String id, XVarInteger[] list, int[] coeffs, Condition condition);

	/**
	 * Full information about the constraint (this form) in <a href="http://xcsp.org/format3.pdf"> the specifications
	 * (Chapter 4)</a>. <br>
	 * Quick information available on the <a href="http://xcsp.org/specifications"> XCSP3 website (Tab Specifications)
	 * </a>. <br>
	 * Select the constraint after opening the left navigation bar below heading XCSP3-core.
	 * 
	 */
	void buildCtrSum(String id, XVarInteger[] list, XVarInteger[] coeffs, Condition condition);

	void buildCtrSum(String id, XNode<XVarInteger>[] trees, Condition condition);

	void buildCtrSum(String id, XNode<XVarInteger>[] trees, int[] coeffs, Condition condition);

	void buildCtrSum(String id, XNode<XVarInteger>[] trees, XVarInteger[] coeffs, Condition condition);

	/**
	 * Full information about the constraint (this form) in <a href="http://xcsp.org/format3.pdf"> the specifications
	 * (Chapter 4)</a>. <br>
	 * Quick information available on the <a href="http://xcsp.org/specifications"> XCSP3 website (Tab Specifications)
	 * </a>. <br>
	 * Select the constraint after opening the left navigation bar below heading XCSP3-core.
	 * 
	 */
	void buildCtrCount(String id, XVarInteger[] list, int[] values, Condition condition);

	void buildCtrCount(String id, XNode<XVarInteger>[] trees, int[] values, Condition condition);

	/**
	 * Full information about the constraint (this form) in <a href="http://xcsp.org/format3.pdf"> the specifications
	 * (Chapter 4)</a>. <br>
	 * Quick information available on the <a href="http://xcsp.org/specifications"> XCSP3 website (Tab Specifications)
	 * </a>. <br>
	 * Select the constraint after opening the left navigation bar below heading XCSP3-core.
	 * 
	 */
	void buildCtrCount(String id, XVarInteger[] list, XVarInteger[] values, Condition condition);

	/**
	 * Full information about the constraint (this form) in <a href="http://xcsp.org/format3.pdf"> the specifications
	 * (Chapter 4)</a>. <br>
	 * Quick information available on the <a href="http://xcsp.org/specifications"> XCSP3 website (Tab Specifications)
	 * </a>. <br>
	 * Select the constraint after opening the left navigation bar below heading XCSP3-core.
	 * 
	 */
	void buildCtrAtLeast(String id, XVarInteger[] list, int value, int k);

	/**
	 * Full information about the constraint (this form) in <a href="http://xcsp.org/format3.pdf"> the specifications
	 * (Chapter 4)</a>. <br>
	 * Quick information available on the <a href="http://xcsp.org/specifications"> XCSP3 website (Tab Specifications)
	 * </a>. <br>
	 * Select the constraint after opening the left navigation bar below heading XCSP3-core.
	 * 
	 */
	void buildCtrAtMost(String id, XVarInteger[] list, int value, int k);

	/**
	 * Full information about the constraint (this form) in <a href="http://xcsp.org/format3.pdf"> the specifications
	 * (Chapter 4)</a>. <br>
	 * Quick information available on the <a href="http://xcsp.org/specifications"> XCSP3 website (Tab Specifications)
	 * </a>. <br>
	 * Select the constraint after opening the left navigation bar below heading XCSP3-core.
	 * 
	 */
	void buildCtrExactly(String id, XVarInteger[] list, int value, int k);

	/**
	 * Full information about the constraint (this form) in <a href="http://xcsp.org/format3.pdf"> the specifications
	 * (Chapter 4)</a>. <br>
	 * Quick information available on the <a href="http://xcsp.org/specifications"> XCSP3 website (Tab Specifications)
	 * </a>. <br>
	 * Select the constraint after opening the left navigation bar below heading XCSP3-core.
	 * 
	 */
	void buildCtrExactly(String id, XVarInteger[] list, int value, XVarInteger k);

	/**
	 * Full information about the constraint (this form) in <a href="http://xcsp.org/format3.pdf"> the specifications
	 * (Chapter 4)</a>. <br>
	 * Quick information available on the <a href="http://xcsp.org/specifications"> XCSP3 website (Tab Specifications)
	 * </a>. <br>
	 * Select the constraint after opening the left navigation bar below heading XCSP3-core.
	 * 
	 */
	void buildCtrAmong(String id, XVarInteger[] list, int[] values, int k);

	/**
	 * Full information about the constraint (this form) in <a href="http://xcsp.org/format3.pdf"> the specifications
	 * (Chapter 4)</a>. <br>
	 * Quick information available on the <a href="http://xcsp.org/specifications"> XCSP3 website (Tab Specifications)
	 * </a>. <br>
	 * Select the constraint after opening the left navigation bar below heading XCSP3-core.
	 * 
	 */
	void buildCtrAmong(String id, XVarInteger[] list, int[] values, XVarInteger k);

	/**
	 * Full information about the constraint (this form) in <a href="http://xcsp.org/format3.pdf"> the specifications
	 * (Chapter 4)</a>. <br>
	 * Quick information available on the <a href="http://xcsp.org/specifications"> XCSP3 website (Tab Specifications)
	 * </a>. <br>
	 * Select the constraint after opening the left navigation bar below heading XCSP3-core.
	 * 
	 */
	void buildCtrNValues(String id, XVarInteger[] list, Condition condition);

	/**
	 * Full information about the constraint (this form) in <a href="http://xcsp.org/format3.pdf"> the specifications
	 * (Chapter 4)</a>. <br>
	 * Quick information available on the <a href="http://xcsp.org/specifications"> XCSP3 website (Tab Specifications)
	 * </a>. <br>
	 * Select the constraint after opening the left navigation bar below heading XCSP3-core.
	 * 
	 */
	void buildCtrNValuesExcept(String id, XVarInteger[] list, int[] except, Condition condition);

	void buildCtrNValues(String id, XNode<XVarInteger>[] trees, Condition condition);

	/**
	 * Full information about the constraint (this form) in <a href="http://xcsp.org/format3.pdf"> the specifications
	 * (Chapter 4)</a>. <br>
	 * Quick information available on the <a href="http://xcsp.org/specifications"> XCSP3 website (Tab Specifications)
	 * </a>. <br>
	 * Select the constraint after opening the left navigation bar below heading XCSP3-core.
	 * 
	 */
	void buildCtrNotAllEqual(String id, XVarInteger[] list);

	/**
	 * Full information about the constraint (this form) in <a href="http://xcsp.org/format3.pdf"> the specifications
	 * (Chapter 4)</a>. <br>
	 * Quick information available on the <a href="http://xcsp.org/specifications"> XCSP3 website (Tab Specifications)
	 * </a>. <br>
	 * Select the constraint after opening the left navigation bar below heading XCSP3-core.
	 * 
	 */
	void buildCtrCardinality(String id, XVarInteger[] list, boolean closed, int[] values, XVarInteger[] occurs);

	/**
	 * Full information about the constraint (this form) in <a href="http://xcsp.org/format3.pdf"> the specifications
	 * (Chapter 4)</a>. <br>
	 * Quick information available on the <a href="http://xcsp.org/specifications"> XCSP3 website (Tab Specifications)
	 * </a>. <br>
	 * Select the constraint after opening the left navigation bar below heading XCSP3-core.
	 * 
	 */
	void buildCtrCardinality(String id, XVarInteger[] list, boolean closed, int[] values, int[] occurs);

	/**
	 * Full information about the constraint (this form) in <a href="http://xcsp.org/format3.pdf"> the specifications
	 * (Chapter 4)</a>. <br>
	 * Quick information available on the <a href="http://xcsp.org/specifications"> XCSP3 website (Tab Specifications)
	 * </a>. <br>
	 * Select the constraint after opening the left navigation bar below heading XCSP3-core.
	 * 
	 */
	void buildCtrCardinality(String id, XVarInteger[] list, boolean closed, int[] values, int[] occursMin, int[] occursMax);

	/**
	 * Full information about the constraint (this form) in <a href="http://xcsp.org/format3.pdf"> the specifications
	 * (Chapter 4)</a>. <br>
	 * Quick information available on the <a href="http://xcsp.org/specifications"> XCSP3 website (Tab Specifications)
	 * </a>. <br>
	 * Select the constraint after opening the left navigation bar below heading XCSP3-core.
	 * 
	 */
	void buildCtrCardinality(String id, XVarInteger[] list, boolean closed, XVarInteger[] values, XVarInteger[] occurs);

	/**
	 * Full information about the constraint (this form) in <a href="http://xcsp.org/format3.pdf"> the specifications
	 * (Chapter 4)</a>. <br>
	 * Quick information available on the <a href="http://xcsp.org/specifications"> XCSP3 website (Tab Specifications)
	 * </a>. <br>
	 * Select the constraint after opening the left navigation bar below heading XCSP3-core.
	 * 
	 */
	void buildCtrCardinality(String id, XVarInteger[] list, boolean closed, XVarInteger[] values, int[] occurs);

	/**
	 * Full information about the constraint (this form) in <a href="http://xcsp.org/format3.pdf"> the specifications
	 * (Chapter 4)</a>. <br>
	 * Quick information available on the <a href="http://xcsp.org/specifications"> XCSP3 website (Tab Specifications)
	 * </a>. <br>
	 * Select the constraint after opening the left navigation bar below heading XCSP3-core.
	 * 
	 */
	void buildCtrCardinality(String id, XVarInteger[] list, boolean closed, XVarInteger[] values, int[] occursMin, int[] occursMax);

	/**
	 * Full information about the constraint (this form) in <a href="http://xcsp.org/format3.pdf"> the specifications
	 * (Chapter 4)</a>. <br>
	 * Quick information available on the <a href="http://xcsp.org/specifications"> XCSP3 website (Tab Specifications)
	 * </a>. <br>
	 * Select the constraint after opening the left navigation bar below heading XCSP3-core.
	 * 
	 */
	void buildCtrMaximum(String id, XVarInteger[] list, Condition condition);

	/**
	 * Full information about the constraint (this form) in <a href="http://xcsp.org/format3.pdf"> the specifications
	 * (Chapter 4)</a>. <br>
	 * Quick information available on the <a href="http://xcsp.org/specifications"> XCSP3 website (Tab Specifications)
	 * </a>. <br>
	 * Select the constraint after opening the left navigation bar below heading XCSP3-core.
	 * 
	 */
	void buildCtrMaximum(String id, XVarInteger[] list, int startIndex, XVarInteger index, TypeRank rank, Condition condition);

	void buildCtrMaximum(String id, XNode<XVarInteger>[] trees, Condition condition);

	/**
	 * Full information about the constraint (this form) in <a href="http://xcsp.org/format3.pdf"> the specifications
	 * (Chapter 4)</a>. <br>
	 * Quick information available on the <a href="http://xcsp.org/specifications"> XCSP3 website (Tab Specifications)
	 * </a>. <br>
	 * Select the constraint after opening the left navigation bar below heading XCSP3-core.
	 * 
	 */
	void buildCtrMinimum(String id, XVarInteger[] list, Condition condition);

	/**
	 * Full information about the constraint (this form) in <a href="http://xcsp.org/format3.pdf"> the specifications
	 * (Chapter 4)</a>. <br>
	 * Quick information available on the <a href="http://xcsp.org/specifications"> XCSP3 website (Tab Specifications)
	 * </a>. <br>
	 * Select the constraint after opening the left navigation bar below heading XCSP3-core.
	 * 
	 */
	void buildCtrMinimum(String id, XVarInteger[] list, int startIndex, XVarInteger index, TypeRank rank, Condition condition);

	void buildCtrMinimum(String id, XNode<XVarInteger>[] trees, Condition condition);

	void buildCtrElement(String id, XVarInteger[] list, Condition condition);

	void buildCtrElement(String id, XVarInteger[] list, int startIndex, XVarInteger index, TypeRank rank, Condition condition);

	void buildCtrElement(String id, int[] list, int startIndex, XVarInteger index, TypeRank rank, Condition condition);

	void buildCtrElement(String id, int[][] matrix, int startRowIndex, XVarInteger rowIndex, int startColIndex, XVarInteger colIndex, Condition condition);

	void buildCtrElement(String id, XVarInteger[][] matrix, int startRowIndex, XVarInteger rowIndex, int startColIndex, XVarInteger colIndex,
			Condition condition);

	/**
	 * Full information about the constraint (this form) in <a href="http://xcsp.org/format3.pdf"> the specifications
	 * (Chapter 4)</a>. <br>
	 * Quick information available on the <a href="http://xcsp.org/specifications"> XCSP3 website (Tab Specifications)
	 * </a>. <br>
	 * Select the constraint after opening the left navigation bar below heading XCSP3-core.
	 * 
	 */
	void buildCtrChannel(String id, XVarInteger[] list, int startIndex);

	/**
	 * Full information about the constraint (this form) in <a href="http://xcsp.org/format3.pdf"> the specifications
	 * (Chapter 4)</a>. <br>
	 * Quick information available on the <a href="http://xcsp.org/specifications"> XCSP3 website (Tab Specifications)
	 * </a>. <br>
	 * Select the constraint after opening the left navigation bar below heading XCSP3-core.
	 * 
	 */
	void buildCtrChannel(String id, XVarInteger[] list1, int startIndex1, XVarInteger[] list2, int startIndex2);

	/**
	 * Full information about the constraint (this form) in <a href="http://xcsp.org/format3.pdf"> the specifications
	 * (Chapter 4)</a>. <br>
	 * Quick information available on the <a href="http://xcsp.org/specifications"> XCSP3 website (Tab Specifications)
	 * </a>. <br>
	 * Select the constraint after opening the left navigation bar below heading XCSP3-core.
	 * 
	 */
	void buildCtrChannel(String id, XVarInteger[] list, int startIndex, XVarInteger value);

	/**
	 * Full information about the constraint (this form) in <a href="http://xcsp.org/format3.pdf"> the specifications
	 * (Chapter 4)</a>. <br>
	 * Quick information available on the <a href="http://xcsp.org/specifications"> XCSP3 website (Tab Specifications)
	 * </a>. <br>
	 * Select the constraint after opening the left navigation bar below heading XCSP3-core.
	 * 
	 */
	void buildCtrStretch(String id, XVarInteger[] list, int[] values, int[] widthsMin, int[] widthsMax);

	/**
	 * Full information about the constraint (this form) in <a href="http://xcsp.org/format3.pdf"> the specifications
	 * (Chapter 4)</a>. <br>
	 * Quick information available on the <a href="http://xcsp.org/specifications"> XCSP3 website (Tab Specifications)
	 * </a>. <br>
	 * Select the constraint after opening the left navigation bar below heading XCSP3-core.
	 * 
	 */
	void buildCtrStretch(String id, XVarInteger[] list, int[] values, int[] widthsMin, int[] widthsMax, int[][] patterns);

	/**
	 * Full information about the constraint (this form) in <a href="http://xcsp.org/format3.pdf"> the specifications
	 * (Chapter 4)</a>. <br>
	 * Quick information available on the <a href="http://xcsp.org/specifications"> XCSP3 website (Tab Specifications)
	 * </a>. <br>
	 * Select the constraint after opening the left navigation bar below heading XCSP3-core.
	 * 
	 */
	void buildCtrNoOverlap(String id, XVarInteger[] origins, int[] lengths, boolean zeroIgnored);

	/**
	 * Full information about the constraint (this form) in <a href="http://xcsp.org/format3.pdf"> the specifications
	 * (Chapter 4)</a>. <br>
	 * Quick information available on the <a href="http://xcsp.org/specifications"> XCSP3 website (Tab Specifications)
	 * </a>. <br>
	 * Select the constraint after opening the left navigation bar below heading XCSP3-core.
	 * 
	 */
	void buildCtrNoOverlap(String id, XVarInteger[] origins, XVarInteger[] lengths, boolean zeroIgnored);

	/**
	 * Full information about the constraint (this form) in <a href="http://xcsp.org/format3.pdf"> the specifications
	 * (Chapter 4)</a>. <br>
	 * Quick information available on the <a href="http://xcsp.org/specifications"> XCSP3 website (Tab Specifications)
	 * </a>. <br>
	 * Select the constraint after opening the left navigation bar below heading XCSP3-core.
	 * 
	 */
	void buildCtrNoOverlap(String id, XVarInteger[][] origins, int[][] lengths, boolean zeroIgnored);

	/**
	 * Full information about the constraint (this form) in <a href="http://xcsp.org/format3.pdf"> the specifications
	 * (Chapter 4)</a>. <br>
	 * Quick information available on the <a href="http://xcsp.org/specifications"> XCSP3 website (Tab Specifications)
	 * </a>. <br>
	 * Select the constraint after opening the left navigation bar below heading XCSP3-core.
	 * 
	 */
	void buildCtrNoOverlap(String id, XVarInteger[][] origins, XVarInteger[][] lengths, boolean zeroIgnored);

	/**
	 * Full information about the constraint (this form) in <a href="http://xcsp.org/format3.pdf"> the specifications
	 * (Chapter 4)</a>. <br>
	 * Quick information available on the <a href="http://xcsp.org/specifications"> XCSP3 website (Tab Specifications)
	 * </a>. <br>
	 * Select the constraint after opening the left navigation bar below heading XCSP3-core.
	 * 
	 */
	void buildCtrCumulative(String id, XVarInteger[] origins, int[] lengths, int[] heights, Condition condition);

	/**
	 * Full information about the constraint (this form) in <a href="http://xcsp.org/format3.pdf"> the specifications
	 * (Chapter 4)</a>. <br>
	 * Quick information available on the <a href="http://xcsp.org/specifications"> XCSP3 website (Tab Specifications)
	 * </a>. <br>
	 * Select the constraint after opening the left navigation bar below heading XCSP3-core.
	 * 
	 */
	void buildCtrCumulative(String id, XVarInteger[] origins, int[] lengths, XVarInteger[] heights, Condition condition);

	/**
	 * Full information about the constraint (this form) in <a href="http://xcsp.org/format3.pdf"> the specifications
	 * (Chapter 4)</a>. <br>
	 * Quick information available on the <a href="http://xcsp.org/specifications"> XCSP3 website (Tab Specifications)
	 * </a>. <br>
	 * Select the constraint after opening the left navigation bar below heading XCSP3-core.
	 * 
	 */
	void buildCtrCumulative(String id, XVarInteger[] origins, XVarInteger[] lengths, int[] heights, Condition condition);

	/**
	 * Full information about the constraint (this form) in <a href="http://xcsp.org/format3.pdf"> the specifications
	 * (Chapter 4)</a>. <br>
	 * Quick information available on the <a href="http://xcsp.org/specifications"> XCSP3 website (Tab Specifications)
	 * </a>. <br>
	 * Select the constraint after opening the left navigation bar below heading XCSP3-core.
	 * 
	 */
	void buildCtrCumulative(String id, XVarInteger[] origins, XVarInteger[] lengths, XVarInteger[] heights, Condition condition);

	/**
	 * Full information about the constraint (this form) in <a href="http://xcsp.org/format3.pdf"> the specifications
	 * (Chapter 4)</a>. <br>
	 * Quick information available on the <a href="http://xcsp.org/specifications"> XCSP3 website (Tab Specifications)
	 * </a>. <br>
	 * Select the constraint after opening the left navigation bar below heading XCSP3-core.
	 * 
	 */
	void buildCtrCumulative(String id, XVarInteger[] origins, int[] lengths, XVarInteger[] ends, int[] heights, Condition condition);

	/**
	 * Full information about the constraint (this form) in <a href="http://xcsp.org/format3.pdf"> the specifications
	 * (Chapter 4)</a>. <br>
	 * Quick information available on the <a href="http://xcsp.org/specifications"> XCSP3 website (Tab Specifications)
	 * </a>. <br>
	 * Select the constraint after opening the left navigation bar below heading XCSP3-core.
	 * 
	 */
	void buildCtrCumulative(String id, XVarInteger[] origins, int[] lengths, XVarInteger[] ends, XVarInteger[] heights, Condition condition);

	/**
	 * Full information about the constraint (this form) in <a href="http://xcsp.org/format3.pdf"> the specifications
	 * (Chapter 4)</a>. <br>
	 * Quick information available on the <a href="http://xcsp.org/specifications"> XCSP3 website (Tab Specifications)
	 * </a>. <br>
	 * Select the constraint after opening the left navigation bar below heading XCSP3-core.
	 * 
	 */
	void buildCtrCumulative(String id, XVarInteger[] origins, XVarInteger[] lengths, XVarInteger[] ends, int[] heights, Condition condition);

	/**
	 * Full information about the constraint (this form) in <a href="http://xcsp.org/format3.pdf"> the specifications
	 * (Chapter 4)</a>. <br>
	 * Quick information available on the <a href="http://xcsp.org/specifications"> XCSP3 website (Tab Specifications)
	 * </a>. <br>
	 * Select the constraint after opening the left navigation bar below heading XCSP3-core.
	 * 
	 */
	void buildCtrCumulative(String id, XVarInteger[] origins, XVarInteger[] lengths, XVarInteger[] ends, XVarInteger[] heights, Condition condition);

	void buildCtrBinPacking(String id, XVarInteger[] list, int[] sizes, Condition condition);

	void buildCtrBinPacking(String id, XVarInteger[] list, int[] sizes, Condition[] conditions, int startIndex);

	/**
	 * Full information about the constraint (this form) in <a href="http://xcsp.org/format3.pdf"> the specifications
	 * (Chapter 4)</a>. <br>
	 * Quick information available on the <a href="http://xcsp.org/specifications"> XCSP3 website (Tab Specifications)
	 * </a>. <br>
	 * Select the constraint after opening the left navigation bar below heading XCSP3-core.
	 * 
	 */
	void buildCtrInstantiation(String id, XVarInteger[] list, int[] values);

	/**
	 * Full information about the constraint (this form) in <a href="http://xcsp.org/format3.pdf"> the specifications
	 * (Chapter 4)</a>. <br>
	 * Quick information available on the <a href="http://xcsp.org/specifications"> XCSP3 website (Tab Specifications)
	 * </a>. <br>
	 * Select the constraint after opening the left navigation bar below heading XCSP3-core.
	 * 
	 */
	void buildCtrClause(String id, XVarInteger[] pos, XVarInteger[] neg);

	/**
	 * Full information about the constraint (this form) in <a href="http://xcsp.org/format3.pdf"> the specifications
	 * (Chapter 4)</a>. <br>
	 * Quick information available on the <a href="http://xcsp.org/specifications"> XCSP3 website (Tab Specifications)
	 * </a>. <br>
	 * Select the constraint after opening the left navigation bar below heading XCSP3-core.
	 * 
	 */
	void buildCtrCircuit(String id, XVarInteger[] list, int startIndex);

	/**
	 * Full information about the constraint (this form) in <a href="http://xcsp.org/format3.pdf"> the specifications
	 * (Chapter 4)</a>. <br>
	 * Quick information available on the <a href="http://xcsp.org/specifications"> XCSP3 website (Tab Specifications)
	 * </a>. <br>
	 * Select the constraint after opening the left navigation bar below heading XCSP3-core.
	 * 
	 */
	void buildCtrCircuit(String id, XVarInteger[] list, int startIndex, int size);

	/**
	 * Full information about the constraint (this form) in <a href="http://xcsp.org/format3.pdf"> the specifications
	 * (Chapter 4)</a>. <br>
	 * Quick information available on the <a href="http://xcsp.org/specifications"> XCSP3 website (Tab Specifications)
	 * </a>. <br>
	 * Select the constraint after opening the left navigation bar below heading XCSP3-core.
	 * 
	 */
	void buildCtrCircuit(String id, XVarInteger[] list, int startIndex, XVarInteger size);

	/**********************************************************************************************
	 * Methods to be implemented for managing objectives
	 *********************************************************************************************/

	void buildObjToMinimize(String id, XVarInteger x);

	void buildObjToMaximize(String id, XVarInteger x);

	void buildObjToMinimize(String id, XNodeParent<XVarInteger> tree);

	void buildObjToMaximize(String id, XNodeParent<XVarInteger> tree);

	void buildObjToMinimize(String id, TypeObjective type, XVarInteger[] list);

	void buildObjToMaximize(String id, TypeObjective type, XVarInteger[] list);

	void buildObjToMinimize(String id, TypeObjective type, XVarInteger[] list, int[] coeffs);

	void buildObjToMaximize(String id, TypeObjective type, XVarInteger[] list, int[] coeffs);

	void buildObjToMinimize(String id, TypeObjective type, XNode<XVarInteger>[] trees);

	void buildObjToMaximize(String id, TypeObjective type, XNode<XVarInteger>[] trees);

	void buildObjToMinimize(String id, TypeObjective type, XNode<XVarInteger>[] trees, int[] coeffs);

	void buildObjToMaximize(String id, TypeObjective type, XNode<XVarInteger>[] trees, int[] coeffs);

	/**********************************************************************************************
	 * Methods to be implemented on symbolic variables/constraints
	 *********************************************************************************************/

	void buildVarSymbolic(XVarSymbolic x, String[] values);

	void buildCtrIntension(String id, XVarSymbolic[] scope, XNodeParent<XVarSymbolic> syntaxTreeRoot);

	void buildCtrExtension(String id, XVarSymbolic x, String[] values, boolean positive, Set<TypeFlag> flags);

	void buildCtrExtension(String id, XVarSymbolic[] list, String[][] tuples, boolean positive, Set<TypeFlag> flags);

	void buildCtrAllDifferent(String id, XVarSymbolic[] list);

	/**********************************************************************************************
	 * Methods to be implemented on Annotations
	 *********************************************************************************************/

	void buildAnnotationDecision(XVarInteger[] list);
} public static final class CChild extends CEntry {

	/** The type of the child. For example list, supports, or transitions. */
	public final TypeChild type;

	/** Returns the type of the child. For example list, supports, or transitions. We need an accessor for Scala. **/
	public final TypeChild getType() {
		return type;
	}

	/**
	 * The value of the child. It is actually the parsed textual content of the child. After parsing, it may be a variable, an integer, an array of
	 * variables, a condition, an array of parameters ...
	 */
	public Object value;

	/**
	 * Build an object representing a child element of a constraint (template). The specified type corresponds to the tag name of the child, and the value
	 * corresponds to the parsed textual content of the child.
	 */
	public CChild(TypeChild type, Object value) {
		this.type = type;
		this.value = value;
	}

	/** Returns true iff a set variable is involved in the (value field of the) element. */
	public boolean setVariableInvolved() {
		return Utilities.check(value, obj -> (obj instanceof XVar && ((XVar) obj).type.isSet()));
	}

	@Override
	public LinkedHashSet<XVar> collectVars(LinkedHashSet<XVar> set) {
		return type == TypeChild.supports || type == TypeChild.conflicts ? set : collectVarsIn(value, set);
	}

	@Override
	public boolean subjectToAbstraction() {
		if (type == TypeChild.function && ((XNode<?>) value).firstNodeSuchThat(n -> n.type == TypeExpr.PAR) != null) // containsLeafSuchThat(n ->
																														// n.getType() ==
																														// TypeExpr.PAR))
			return true;
		if (type == TypeChild.condition && value instanceof ConditionPar)
			return true;
		return Utilities.check(value, obj -> obj instanceof XParameter); // check if a parameter somewhere inside the value
	}

	/** Returns true iff the value of the child only contains parameters (tokens of the form %i or %...). */
	public boolean isTotallyAbstract() {
		if (!value.getClass().isArray())
			return value instanceof XParameter;
		int size = Array.getLength(value);
		return size > 0 && IntStream.range(0, size).allMatch(i -> ((XParameter) Array.get(value, i)) instanceof XParameter);
	}

	@Override
	public String toString() {
		return type + super.toString() + " : " + (value == null ? "" : value.getClass().isArray() ? Utilities.arrayToString(value) : value);
	}
} public static class XCtr extends CEntryReifiable {
	/** The type of the constraint. For example, it may be intension, extension, or regular. */
	public final TypeCtr type;

	/** Returns the type of the constraint. For example, it may be intension, extension, or regular. We need an accessor for Scala. **/
	public final TypeCtr getType() {
		return type;
	}

	/**
	 * The child elements of the constraint. For example, we have a first child for <list> and a second child for <transitions> if the constraint is <mdd>.
	 */
	public final CChild[] childs;

	/**
	 * The object for handling abstraction. Of course, it is null if the constraint is not abstract, i.e., is not a constraint template.
	 */
	public XAbstraction abstraction;

	/** Build an object representing a stand-alone constraint (template). */
	public XCtr(TypeCtr type, CChild... childs) {
		this.type = type;
		this.childs = childs;
		int[] abstractChildsPositions = IntStream.range(0, childs.length).filter(i -> childs[i].subjectToAbstraction()).toArray();
		if (abstractChildsPositions.length > 0) {
			Utilities.control(
					IntStream.of(abstractChildsPositions).mapToObj(i -> childs[i])
							.allMatch(child -> child.type == TypeChild.function || child.isTotallyAbstract() || child.value instanceof ConditionPar),
					"Abstraction Form not handled");
			abstraction = new XAbstraction(IntStream.of(abstractChildsPositions).mapToObj(i -> childs[i]).toArray(CChild[]::new));
		}
	}

	@Override
	public LinkedHashSet<XVar> collectVars(LinkedHashSet<XVar> set) {
		Stream.of(childs).filter(child -> child.type != TypeChild.supports && child.type != TypeChild.conflicts).forEach(child -> child.collectVars(set));
		return super.collectVars(set);
	}

	@Override
	public boolean subjectToAbstraction() {
		return abstraction != null;
	}

	@Override
	public String toString() {
		return type + super.toString() + "\n\t" + Utilities.join(childs, "\n\t");
	}
} public static abstract class XVar extends VEntry implements IVar {

	/** Builds a variable with the specified id, type and domain. */
	public static final XVar build(String id, TypeVar type, IDom dom) {
		switch (type) {
		case integer:
			return new XVarInteger(id, type, dom);
		case symbolic:
			return new XVarSymbolic(id, type, dom);
		case stochastic:
			return new XVarStochastic(id, type, dom);
		case real:
			return new XVarReal(id, type, dom);
		case set:
			return new XVarSet(id, type, dom);
		default:
			throw new RuntimeException("Unimplemented case ");
		}
	}

	/** Builds a variable from an array with the specified id (combined with the specified indexes), type and domain. */
	public static final XVar build(String idArray, TypeVar type, IDom dom, int[] indexes) {
		return build(idArray + "[" + Utilities.join(indexes, "][") + "]", type, dom);
	}

	/** The domain of the variable. It is null if the variable is qualitative. */
	public final IDom dom;

	/** The degree of the variable. This is automatically computed after all constraints have been parsed. */
	public int degree;

	/** Builds a variable with the specified id, type and domain. */
	protected XVar(String id, TypeVar type, IDom dom) {
		super(id, type);
		this.dom = dom;
	}

	// /** Builds a variable from an array with the specified id (combined with the specified indexes), type and domain. */
	// protected VVar(String idArray, TypeVar type, DDom dom, int[] indexes) {
	// this(idArray + "[" + XUtility.join(indexes, "][") + "]", type, dom);
	// }

	@Override
	public String id() {
		return id;
	}

	@Override
	public String toString() {
		return id; // + " :" + type + " of " + dom;
	}
} public static final class XVarInteger extends XVar implements Var {

	/**
	 * Returns the size of the Cartesian product for the domains of the specified variables. Importantly, if this value does not fit within a
	 * {@code long}, -1 is returned.
	 */
	public static long domainCartesianProductSize(XVarInteger[] scp) {
		long[] domSizes = Stream.of(scp).mapToLong(x -> IntegerEntity.nValues((IntegerEntity[]) ((Dom) x.dom).values)).toArray();
		if (LongStream.of(domSizes).anyMatch(l -> l == -1L))
			return -1L;
		long cnt = 1;
		try {
			for (long size : domSizes)
				cnt = Math.multiplyExact(cnt, size);
		} catch (ArithmeticException e) {
			return -1L;
		}
		return cnt;
	}

	public TypePrimitive whichPrimitive() {
		return TypePrimitive.whichPrimitiveFor(firstValue(), lastValue());
	}

	/** Builds an integer variable with the specified id, type and domain. */
	protected XVarInteger(String id, TypeVar type, IDom dom) {
		super(id, type, dom);
	}

	public long firstValue() {
		return ((Dom) dom).firstValue();
	}

	public long lastValue() {
		return ((Dom) dom).lastValue();
	}

	@Override
	public Object allValues() {
		return ((Dom) dom).allValues();
	}

	public boolean isZeroOne() {
		return firstValue() == 0 && lastValue() == 1;
	}
}
import static org.xcsp.common.Types.TypeConditionOperatorRel.EQ;
import static org.xcsp.parser.callbacks.XCallbacks.XCallbacksParameters.CONVERT_INTENSION_TO_EXTENSION_ARITY_LIMIT;
import static org.xcsp.parser.callbacks.XCallbacks.XCallbacksParameters.CONVERT_INTENSION_TO_EXTENSION_SPACE_LIMIT;
import static org.xcsp.parser.callbacks.XCallbacks.XCallbacksParameters.RECOGNIZING_BEFORE_CONVERTING;
import java.lang.reflect.Array;
import java.util.ArrayList;
import java.util.Arrays;
import java.util.HashSet;
import java.util.List;
import java.util.function.BiFunction;
import java.util.stream.IntStream;
import java.util.stream.Stream;
import org.xcsp.common.Condition;
import org.xcsp.common.Condition.ConditionRel;
import org.xcsp.common.Constants;
import org.xcsp.common.Types.TypeAtt;
import org.xcsp.common.Types.TypeChild;
import org.xcsp.common.Types.TypeConditionOperatorRel;
import org.xcsp.common.Types.TypeCtr;
import org.xcsp.common.Types.TypeExpr;
import org.xcsp.common.Types.TypeOperator;
import org.xcsp.common.Types.TypeOperatorRel;
import org.xcsp.common.Types.TypeRank;
import org.xcsp.common.Utilities;
import org.xcsp.common.Utilities.ModifiableBoolean;
import org.xcsp.common.domains.Domains.Dom;
import org.xcsp.common.domains.Values.IntegerEntity;
import org.xcsp.common.domains.Values.IntegerInterval;
import org.xcsp.common.domains.Values.Occurrences;
import org.xcsp.common.predicates.TreeEvaluator;
import org.xcsp.common.predicates.XNode;
import org.xcsp.common.predicates.XNodeLeaf;
import org.xcsp.common.predicates.XNodeParent;
import org.xcsp.common.structures.AbstractTuple;
import org.xcsp.common.structures.Transition;
import org.xcsp.parser.callbacks.XCallbacks;
import org.xcsp.parser.entries.XConstraints.CChild;
import org.xcsp.parser.entries.XConstraints.XCtr;
import org.xcsp.parser.entries.XVariables.XVar;
import org.xcsp.parser.entries.XVariables.XVarInteger;
		XNodeParent<XVarInteger> root = (XNodeParent<XVarInteger>) r;
		XVarInteger[] scope = root.vars();
		if (xc.implem().currParameters.get(RECOGNIZING_BEFORE_CONVERTING) == Boolean.FALSE) // we try first converting
																							// into extension
			if (intensionToExtension(c.id, scope, root))
				return;
		if (recognizer.specificIntensionCases(c.id, root, scope.length)) // we try to recognize special forms of
																			// intension constraints
			return;
		if (xc.implem().currParameters.get(RECOGNIZING_BEFORE_CONVERTING) == Boolean.TRUE) // we now try converting into
																							// extension
			if (intensionToExtension(c.id, scope, root))
				return;
		xc.buildCtrIntension(c.id, scope, root);
	}

	private void extension(XCtr c) {
		CChild c1 = c.childs[1];
		boolean positive = c1.type == TypeChild.supports;
		if (c1.value == null || Array.getLength(c1.value) == 0) { // special case because 0 tuple
			if (positive)
				xc.buildCtrFalse(c.id, c.vars());
			else
				xc.buildCtrTrue(c.id, c.vars());
		} else {
			XVarInteger[] list = (XVarInteger[]) c.childs[0].value;
			if (list.length == 1) // unary constraint
				xc.buildCtrExtension(c.id, list[0], trIntegers(c1.value), positive, c1.flags);
			else {
				if (c1.value instanceof AbstractTuple[]) {
					xc.buildCtrExtension(c.id, list, (AbstractTuple[]) c1.value, positive, c1.flags);
					System.out.println("jjj");
				} else {
					int[][] tuples = xc.implem().cache4Tuples.computeIfAbsent(c1.value, k -> trIntegers2D(c1.value));
					// if (tuples == null)
					// xc.implem().cache4Tuples.put(c1.value, tuples = trIntegers2D(c1.value));
					// control to insert later below ?
					// for (int i = 0; i < tuples.length - 1; i++) if (Utilities.lexComparatorInt.compare(tuples[i],
					// tuples[i + 1]) >= 0) {
					// System.out.println("\nSAME " + c + " " + Utilities.join(tuples[i]) + " " +
					// Utilities.join(tuples[i + 1]) + " (" + i + ")");
					// System.exit(1); }
					xc.buildCtrExtension(c.id, list, tuples, positive, c1.flags);
				}
			}
		}
	}

	private void regular(XCtr c) {
		xc.buildCtrRegular(c.id, (XVarInteger[]) c.childs[0].value, (Transition[]) c.childs[1].value, (String) c.childs[2].value, (String[]) c.childs[3].value);
	}

	private void mdd(XCtr c) {
		xc.buildCtrMDD(c.id, (XVarInteger[]) c.childs[0].value, (Transition[]) c.childs[1].value);
	}

	private void allDifferent(XCtr c) {
		CChild[] childs = c.childs;
		if (childs[0].value instanceof XNode[]) {
			Utilities.control(childs.length == 1 && childs[0].type == TypeChild.list, "Other forms not implemented");
			XNode<XVarInteger>[] trees = ((XNode<XVarInteger>[]) childs[0].value);
			xc.buildCtrAllDifferent(c.id, trees);
		} else if (childs[0].type == TypeChild.matrix) {
			if (childs.length == 1)
				xc.buildCtrAllDifferentMatrix(c.id, (XVarInteger[][]) (childs[0].value));
			else
				xc.buildCtrAllDifferentMatrix(c.id, (XVarInteger[][]) (childs[0].value), trIntegers(childs[1].value));
		} else if (childs[0].type == TypeChild.list) {
			if (childs.length == 1)
				xc.buildCtrAllDifferent(c.id, (XVarInteger[]) childs[0].value);
			else if (childs[1].type == TypeChild.except)
				xc.buildCtrAllDifferentExcept(c.id, (XVarInteger[]) childs[0].value, trIntegers(childs[1].value));
			else if (childs[childs.length - 1].type == TypeChild.list)
				xc.buildCtrAllDifferentList(c.id, Stream.of(childs).map(p -> p.value).toArray(XVarInteger[][]::new));
			else
				xc.unimplementedCase(c);
		} else
			xc.unimplementedCase(c);
	}

	private void allEqual(XCtr c) {
		if (c.childs[0].type == TypeChild.list)
			if (c.childs.length == 1) {
				if (c.childs[0].value instanceof XNode[]) {
					xc.buildCtrAllEqual(c.id, ((XNode<XVarInteger>[]) c.childs[0].value));
				} else
					xc.buildCtrAllEqual(c.id, (XVarInteger[]) c.childs[0].value);
			} else
				xc.unimplementedCase(c);
		else
			xc.unimplementedCase(c);
	}

	private void ordered(XCtr c) {
		if (c.childs[0].type == TypeChild.list)
			if (c.childs.length == 2)
				xc.buildCtrOrdered(c.id, (XVarInteger[]) c.childs[0].value, ((TypeOperator) c.childs[1].value).toRel());
			else if (c.childs.length == 3 && c.childs[1].type == TypeChild.lengths) {
				if (c.childs[1].value instanceof XVarInteger[])
					xc.buildCtrOrdered(c.id, (XVarInteger[]) c.childs[0].value, (XVarInteger[]) c.childs[1].value, ((TypeOperator) c.childs[2].value).toRel());
				else
					xc.buildCtrOrdered(c.id, (XVarInteger[]) c.childs[0].value, trIntegers(c.childs[1].value), ((TypeOperator) c.childs[2].value).toRel());
			} else
				xc.unimplementedCase(c);
		else
			xc.unimplementedCase(c);
	}

	private void lex(XCtr c) {
		TypeOperatorRel op = ((TypeOperator) c.childs[c.childs.length - 1].value).toRel();
		if (c.childs[0].type == TypeChild.matrix)
			xc.buildCtrLexMatrix(c.id, (XVarInteger[][]) c.childs[0].value, op);
		else {
			xc.buildCtrLex(c.id, IntStream.range(0, c.childs.length - 1).mapToObj(i -> c.childs[i].value).toArray(XVarInteger[][]::new), op);
		}
	}

	private void precedence(XCtr c) {
		if (c.childs[0].type == TypeChild.list) {
			Utilities.control(c.childs.length == 2, "bad form");
			boolean covered = c.childs[1].getAttributeValue(TypeAtt.covered, false);