}

			sort(from, i);
			sort(i, to);
		}

	}

	@Override
	public String toString() {
		StringBuffer stb = new StringBuffer();

		if (lits.length > 0) {
			for (int i = 0; i < lits.length; i++) {
				// if (voc.isUnassigned(lits[i])) {
				stb.append(" + ");
				stb.append(this.coefs[i]);
				stb.append(".");
				stb.append(Lits.toString(this.lits[i]));
				stb.append("[");
				stb.append(voc.valueToString(lits[i]));
				stb.append("@");
				stb.append(voc.getLevel(lits[i]));
				stb.append("]");
				stb.append(" ");
				// }
			}
			stb.append(">= ");
			stb.append(this.degree);
		}
		return stb.toString();
	}

	public void assertConstraint(UnitPropagationListener s) {
		long tmp = slackConstraint();
		for (int i = 0; i < lits.length; i++) {
			if (voc.isUnassigned(lits[i]) && tmp < coefs[i]) {
				boolean ret = s.enqueue(lits[i], this);
				assert ret;
			}
		}
	}

	public void register() {
		assert learnt;
		try {
			computeWatches();
		} catch (ContradictionException e) {
			System.out.println(this);
			assert false;
		}
	}

	/**
	 * to obtain the literals of the constraint.
	 * 
	 * @return a copy of the array of the literals
	 */
	public int[] getLits() {
		int[] litsBis = new int[lits.length];
		System.arraycopy(lits, 0, litsBis, 0, lits.length);
		return litsBis;
	}

	public ILits getVocabulary() {
		return voc;
	}

	/**
	 * compute an implied clause on the literals with the greater coefficients.
	 * 
	 * @return a vector containing the literals for this clause.
	 */
	public IVecInt computeAnImpliedClause() {
		long cptCoefs = 0;
		int index = coefs.length;
		while ((cptCoefs > degree) && (index > 0)) {
			cptCoefs = cptCoefs + coefs[--index];
		}
		if (index > 0 && index < size() / 2) {
			IVecInt literals = new VecInt(index);
			for (int j = 0; j <= index; j++)
				literals.push(lits[j]);
			return literals;
		}
		return null;
	}

	public boolean coefficientsEqualToOne() {
		return false;
	}

	@Override
	public boolean equals(Object pb) {
		if (pb == null) {
			return false;
		}
		// this method should be simplified since now two constraints should
		// have
		// always
		// their literals in the same order
		try {

	protected MinWatchPbLongCP(ILits voc, int[] lits, BigInteger[] coefs, // NOPMD
			BigInteger degree) {

		super(lits, coefs, degree);
		this.voc = voc;

		watching = new int[this.coefs.length];
		watched = new boolean[this.coefs.length];
		activity = 0;
		watchCumul = 0;
		watchingCount = 0;

	}

	/*
	 * This method initialize the watched literals.
	 * 
	 * This method is only called in the factory methods.
	 * 
	 * @see org.sat4j.minisat.constraints.WatchPb#computeWatches()
	 */
	@Override
	protected void computeWatches() throws ContradictionException {
		assert watchCumul == 0;
		assert watchingCount == 0;
		for (int i = 0; i < lits.length && (watchCumul - coefs[0]) < degree; i++) {
			if (!voc.isFalsified(lits[i])) {
				voc.watch(lits[i] ^ 1, this);
				watching[watchingCount++] = i;
				watched[i] = true;
				// update the initial value for watchCumul (poss)
				watchCumul = watchCumul + coefs[i];
			}
		}

		if (learnt)
			watchMoreForLearntConstraint();

		if (watchCumul < degree) {
			throw new ContradictionException("non satisfiable constraint");
		}
		assert nbOfWatched() == watchingCount;
	}

	private void watchMoreForLearntConstraint() {
		// looking for literals to be watched,
		// ordered by decreasing level
		int free = 1;
		int maxlevel, maxi, level;

		while ((watchCumul - coefs[0]) < degree && (free > 0)) {
			free = 0;
			// looking for the literal falsified
			// at the least (lowest ?) level
			maxlevel = -1;
			maxi = -1;
			for (int i = 0; i < lits.length; i++) {
				if (voc.isFalsified(lits[i]) && !watched[i]) {
					free++;
					level = voc.getLevel(lits[i]);
					if (level > maxlevel) {
						maxi = i;
						maxlevel = level;
					}
				}
			}

			if (free > 0) {
				assert maxi >= 0;
				voc.watch(lits[maxi] ^ 1, this);
				watching[watchingCount++] = maxi;
				watched[maxi] = true;
				// update of the watchCumul value
				watchCumul = watchCumul + coefs[maxi];
				free--;
				assert free >= 0;
			}
		}
		assert lits.length == 1 || watchingCount > 1;
	}

	/*
	 * This method propagates any possible value.
	 * 
	 * This method is only called in the factory methods.
	 * 
	 * @see
	 * org.sat4j.minisat.constraints.WatchPb#computePropagation(org.sat4j.minisat
	 * .UnitPropagationListener)
	 */
	@Override
	protected void computePropagation(UnitPropagationListener s)
			throws ContradictionException {
		// propagate any possible value
		int ind = 0;
		while (ind < lits.length
				&& (watchCumul - coefs[watching[ind]]) < degree) {
			if (voc.isUnassigned(lits[ind]) && !s.enqueue(lits[ind], this)) {
				throw new ContradictionException("non satisfiable constraint");
			}
			ind++;
		}
	}

	/**
	 * build a pseudo boolean constraint. Coefficients are positive integers
	 * less than or equal to the degree (this is called a normalized
	 * constraint).
	 * 
	 * @param s
	 *            a unit propagation listener
	 * @param voc
	 *            the vocabulary
	 * @param lits
	 *            the literals
	 * @param coefs
	 *            the coefficients
	 * @param degree
	 *            the degree of the constraint to normalize.
	 * @return a new PB constraint or null if a trivial inconsistency is
	 *         detected.
	 */
	public static MinWatchPbLongCP normalizedMinWatchPbNew(

		}
		return res;
	}

	/**
	 * This predicate tests wether the constraint is assertive at decision level
	 * dl
	 * 
	 * @param dl
	 * @return true iff the constraint is assertive at decision level dl.
	 */
	public boolean isAssertive(int dl) {
		long slack = 0;
		for (int i = 0; i < lits.length; i++) {
			if ((coefs[i] > 0)
					&& ((!voc.isFalsified(lits[i]) || voc.getLevel(lits[i]) >= dl)))
				slack = slack + coefs[i];
		}
		slack = slack - degree;
		if (slack < 0)
			return false;
		for (int i = 0; i < lits.length; i++) {
			if ((coefs[i] > 0)
					&& (voc.isUnassigned(lits[i]) || voc.getLevel(lits[i]) >= dl)
					&& (slack < coefs[i])) {
				return true;
			}
		}
		return false;
	}

	/**
	 * compute the reason for the assignment of a literal
	 * 
	 * @param p
	 *            a falsified literal (or Lit.UNDEFINED)
	 * @param outReason
	 *            list of falsified literals for which the negation is the
	 *            reason of the assignment
	 * @see org.sat4j.minisat.core.Constr#calcReason(int, IVecInt)
	 */
	public void calcReason(int p, IVecInt outReason) {
		final int[] mlits = lits;
		for (int q : mlits) {
			if (voc.isFalsified(q)) {
				outReason.push(q ^ 1);
			}
		}
	}

	abstract protected void computeWatches() throws ContradictionException;

	abstract protected void computePropagation(UnitPropagationListener s)
			throws ContradictionException;

	/**
	 * to obtain the i-th literal of the constraint
	 * 
	 * @param i
	 *            index of the literal
	 * @return the literal
	 */
	public int get(int i) {
		return lits[i];
	}

	/**
	 * to obtain the activity value of the constraint
	 * 
	 * @return activity value of the constraint
	 * @see org.sat4j.minisat.core.Constr#getActivity()
	 */
	public double getActivity() {
		return activity;
	}

	/**
	 * increase activity value of the constraint
	 * 
	 * @see org.sat4j.minisat.core.Constr#incActivity(double)
	 */
	public void incActivity(double claInc) {
		if (learnt) {
			activity += claInc;
		}
	}

	/**
	 * compute the slack of the current constraint slack = poss - degree of the
	 * constraint
	 * 
	 * @return la marge
	 */
	public long slackConstraint() {
		return computeLeftSide() - this.degree;
	}

	/**
	 * compute the slack of a described constraint slack = poss - degree of the
	 * constraint
	 * 
	 * @param theCoefs
	 *            coefficients of the constraint
	 * @param theDegree
	 *            degree of the constraint
	 * @return slack of the constraint
	 */
	public long slackConstraint(long[] theCoefs, long theDegree) {
		return computeLeftSide(theCoefs) - theDegree;
	}

	/**
	 * compute the sum of the coefficients of the satisfied or non-assigned
	 * literals of a described constraint (usually called poss)
	 * 
	 * @param coefs
	 *            coefficients of the constraint
	 * @return poss
	 */
	public long computeLeftSide(long[] theCoefs) {
		long poss = 0;
		// for each literal
		for (int i = 0; i < lits.length; i++)
			if (!voc.isFalsified(lits[i])) {
				assert theCoefs[i] >= 0;
				poss = poss + theCoefs[i];
			}
		return poss;
	}

	/**
	 * compute the sum of the coefficients of the satisfied or non-assigned
	 * literals of a described constraint (usually called poss)
	 * 
	 * @param coefs
	 *            coefficients of the constraint
	 * @return poss
	 */
	public BigInteger computeLeftSide(BigInteger[] theCoefs) {

	private MaxWatchPbLongCP(ILits voc, int[] lits, BigInteger[] coefs,
			BigInteger degree) {

		super(lits, coefs, degree);
		this.voc = voc;

		activity = 0;
		watchCumul = 0;
		if (coefs.length > MaxWatchPb.LIMIT_FOR_MAP) {
			litToCoeffs = new HashMap<Integer, Long>(coefs.length);
			for (int i = 0; i < coefs.length; i++) {
				litToCoeffs.put(lits[i], this.coefs[i]);
			}
		} else
			litToCoeffs = null;
	}

	/**
	 * All the literals are watched.
	 * 
	 * @see org.sat4j.pb.constraints.pb.WatchPbLong#computeWatches()
	 */
	@Override
	protected void computeWatches() throws ContradictionException {
		assert watchCumul == 0;
		for (int i = 0; i < lits.length; i++) {
			if (voc.isFalsified(lits[i])) {
				if (learnt) {
					voc.undos(lits[i] ^ 1).push(this);
					voc.watch(lits[i] ^ 1, this);
				}
			} else {
				// updating of the initial value for the counter
				voc.watch(lits[i] ^ 1, this);
				watchCumul = watchCumul + coefs[i];
			}
		}

		assert watchCumul >= computeLeftSide();
		if (!learnt && watchCumul < degree) {
			throw new ContradictionException("non satisfiable constraint");
		}
	}

	/*
	 * This method propagates any possible value.
	 * 
	 * This method is only called in the factory methods.
	 * 
	 * @see org.sat4j.minisat.constraints.WatchPb#computePropagation()
	 */
	@Override
	protected void computePropagation(UnitPropagationListener s)
			throws ContradictionException {
		// propagate any possible value
		int ind = 0;
		while (ind < coefs.length && (watchCumul - coefs[ind]) < degree) {
			if (voc.isUnassigned(lits[ind]) && !s.enqueue(lits[ind], this))
				// because this happens during the building of a constraint.
				throw new ContradictionException("non satisfiable constraint");
			ind++;
		}
		assert watchCumul >= computeLeftSide();
	}

	public boolean propagate(UnitPropagationListener s, int p) {
		assert nbOfWatched() == watchingCount;
		assert watchingCount > 1;

		// finding the index for p in the array of literals (pIndice)
		// and in the array of watching (pIndiceWatching)
		int pIndiceWatching = 0;
		while (pIndiceWatching < watchingCount
				&& (lits[watching[pIndiceWatching]] ^ 1) != p)
			pIndiceWatching++;
		int pIndice = watching[pIndiceWatching];

		assert p == (lits[pIndice] ^ 1);
		assert watched[pIndice];

		// the greatest coefficient of the watched literals is necessary
		// (pIndice excluded)
		long maxCoef = maximalCoefficient(pIndice);

		// update watching and watched w.r.t. to the propagation of p
		// new literals will be watched, maxCoef could be changed
		maxCoef = updateWatched(maxCoef, pIndice);

		long upWatchCumul = watchCumul - coefs[pIndice];
		assert nbOfWatched() == watchingCount;

		// if a conflict has been detected, return false
		if (upWatchCumul < degree) {
			// conflit
			voc.watch(p, this);
			assert watched[pIndice];
			assert !isSatisfiable();
			return false;
		} else if (upWatchCumul < (degree + maxCoef)) {
			// some literals must be assigned to true and then propagated
			assert watchingCount != 0;
			long limit = upWatchCumul - degree;
			for (int i = 0; i < watchingCount; i++) {
				if (limit < coefs[watching[i]] && i != pIndiceWatching
						&& !voc.isSatisfied(lits[watching[i]])
						&& !s.enqueue(lits[watching[i]], this)) {
					voc.watch(p, this);
					assert !isSatisfiable();
					return false;
				}
			}
			// if the constraint is added to the undos of p (by propagation),
			// then p should be preserved.
			voc.undos(p).push(this);
		}

		// else p is no more watched
		watched[pIndice] = false;
		watchCumul = upWatchCumul;
		watching[pIndiceWatching] = watching[--watchingCount];

		assert watchingCount != 0;
		assert nbOfWatched() == watchingCount;

		return true;
	}

						|| ((coefs[j] == pivot) && (lits[j] < litPivot)));

				if (i >= j)
					break;

				tmp = coefs[i];
				coefs[i] = coefs[j];
				coefs[j] = tmp;
				tmp2 = lits[i];
				lits[i] = lits[j];
				lits[j] = tmp2;
			}

			sort(from, i);
			sort(i, to);
		}

	}

	@Override
	public String toString() {
		StringBuffer stb = new StringBuffer();

		if (lits.length > 0) {
			for (int i = 0; i < lits.length; i++) {
				// if (voc.isUnassigned(lits[i])) {
				stb.append(" + ");
				stb.append(this.coefs[i]);
				stb.append(".");
				stb.append(Lits.toString(this.lits[i]));
				stb.append("[");
				stb.append(voc.valueToString(lits[i]));
				stb.append("@");
				stb.append(voc.getLevel(lits[i]));
				stb.append("]");
				stb.append(" ");
				// }
			}
			stb.append(">= ");
			stb.append(this.degree);
		}
		return stb.toString();
	}

	public void assertConstraint(UnitPropagationListener s) {

		return new MinWatchPbLongCP(voc, mpb);
	}

	/**
	 * the maximal coefficient for the watched literals
	 * 
	 * @param pIndice
	 *            propagated literal : its coefficient is excluded from the
	 *            search of the maximal coefficient
	 * @return the maximal coefficient for the watched literals
	 */
	protected long maximalCoefficient(int pIndice) {
		long maxCoef = 0;
		for (int i = 0; i < watchingCount; i++)
			if (coefs[watching[i]] > maxCoef && watching[i] != pIndice) {
				maxCoef = coefs[watching[i]];
			}

		assert learnt || maxCoef != 0;
		// DLB assert maxCoef!=0;
		return maxCoef;
	}

	/**
	 * update arrays watched and watching w.r.t. the propagation of a literal.
	 * 
	 * return the maximal coefficient of the watched literals (could have been
	 * changed).
	 * 
	 * @param mc
	 *            the current maximal coefficient of the watched literals
	 * @param pIndice
	 *            the literal propagated (falsified)
	 * @return the new maximal coefficient of the watched literals
	 */
	protected long updateWatched(long mc, int pIndice) {
		long maxCoef = mc;
		// if not all the literals are watched
		if (watchingCount < size()) {
			// the watchCumul sum will have to be updated
			long upWatchCumul = watchCumul - coefs[pIndice];

			// we must obtain upWatchCumul such that
			// upWatchCumul = degree + maxCoef
			long degreePlusMaxCoef = degree + maxCoef; // dvh
			for (int ind = 0; ind < lits.length; ind++) {
				if (upWatchCumul >= degreePlusMaxCoef) {
					// nothing more to watch
					// note: logic negated to old version // dvh
					break;
				}
				// while upWatchCumul does not contain enough
				if (!voc.isFalsified(lits[ind]) && !watched[ind]) {
					// watch one more
					upWatchCumul = upWatchCumul + coefs[ind];
					// update arrays watched and watching
					watched[ind] = true;
					assert watchingCount < size();
					watching[watchingCount++] = ind;
					voc.watch(lits[ind] ^ 1, this);
					// this new watched literal could change the maximal
					// coefficient
					if (coefs[ind] > maxCoef) {
						maxCoef = coefs[ind];
						degreePlusMaxCoef = degree + maxCoef; // update
						// that one
						// too
					}
				}
			}
			// update watchCumul
			watchCumul = upWatchCumul + coefs[pIndice];
		}
		return maxCoef;
	}

}

				if (limit < coefs[watching[i]] && i != pIndiceWatching
						&& !voc.isSatisfied(lits[watching[i]])
						&& !s.enqueue(lits[watching[i]], this)) {
					voc.watch(p, this);
					assert !isSatisfiable();
					return false;
				}
			}
			// if the constraint is added to the undos of p (by propagation),
			// then p should be preserved.
			voc.undos(p).push(this);
		}

		// else p is no more watched
		watched[pIndice] = false;
		watchCumul = upWatchCumul;
		watching[pIndiceWatching] = watching[--watchingCount];

		assert watchingCount != 0;
		assert nbOfWatched() == watchingCount;

		return true;
	}

	/**
	 * Remove the constraint from the solver
	 */
	public void remove(UnitPropagationListener upl) {
		for (int i = 0; i < watchingCount; i++) {
			voc.watches(lits[watching[i]] ^ 1).remove(this);
			this.watched[this.watching[i]] = false;
		}
		watchingCount = 0;
		assert nbOfWatched() == watchingCount;
	}

	/**
	 * this method is called during backtrack
	 * 
	 * @param p
	 *            un unassigned literal
	 */
	public void undo(int p) {
		voc.watch(p, this);
		int pIndice = 0;
		while ((lits[pIndice] ^ 1) != p)
			pIndice++;

		assert pIndice < lits.length;

		watchCumul = watchCumul + coefs[pIndice];

	public boolean propagate(UnitPropagationListener s, int p) {
		voc.watch(p, this);

		assert watchCumul >= computeLeftSide() : "" + watchCumul + "/"
				+ computeLeftSide() + ":" + learnt;

		// compute the new value for watchCumul
		long coefP;
		if (litToCoeffs == null) {
			// finding the index for p in the array of literals
			int indiceP = 0;
			while ((lits[indiceP] ^ 1) != p)
				indiceP++;

			// compute the new value for watchCumul
			coefP = coefs[indiceP];
		} else {
			coefP = litToCoeffs.get(p ^ 1);
		}
		long newcumul = watchCumul - coefP;

		if (newcumul < degree) {
			// there is a conflict
			assert !isSatisfiable();
			return false;
		}

		// if no conflict, not(p) can be propagated
		// allow a later un-assignation
		voc.undos(p).push(this);
		// really update watchCumul
		watchCumul = newcumul;

		// propagation
		int ind = 0;
		// limit is the margin between the sum of the coefficients of the
		// satisfied+unassigned literals
		// and the degree of the constraint
		long limit = watchCumul - degree;
		// for each coefficient greater than limit
		while (ind < coefs.length && limit < coefs[ind]) {
			// its corresponding literal is implied
			if (voc.isUnassigned(lits[ind]) && (!s.enqueue(lits[ind], this))) {
				// if it is not possible then there is a conflict
				assert !isSatisfiable();
				return false;
			}
			ind++;
		}

		assert learnt || watchCumul >= computeLeftSide();
		assert watchCumul >= computeLeftSide();
		return true;
	}

		MinWatchPbLongLimit outclause = new MinWatchPbLongLimit(voc, lits,
				coefs, degree);

		if (outclause.degree <= 0) {
			return null;
		}

		outclause.computeWatches();

		outclause.computePropagation(s);

		return outclause;

	}

	/**
	 * Number of really watched literals. It should return the same value as
	 * watchingCount.
	 * 
	 * This method must only be called for assertions.
	 * 
	 * @return number of watched literals.
	 */
	protected int nbOfWatched() {
		int retour = 0;
		for (int ind = 0; ind < this.watched.length; ind++) {
			for (int i = 0; i < watchingCount; i++)
				if (watching[i] == ind)
					assert watched[ind];
			retour += (this.watched[ind]) ? 1 : 0;
		}
		return retour;
	}

	/**
	 * Propagation of a falsified literal
	 * 
	 * @param s
	 *            the solver
	 * @param p
	 *            the propagated literal (it must be falsified)
	 * @return false iff there is a conflict
	 */
	public boolean propagate(UnitPropagationListener s, int p) {
		assert nbOfWatched() == watchingCount;
		assert watchingCount > 1;

		// finding the index for p in the array of literals (pIndice)
		// and in the array of watching (pIndiceWatching)
		int pIndiceWatching = 0;
		while (pIndiceWatching < watchingCount
				&& (lits[watching[pIndiceWatching]] ^ 1) != p)
			pIndiceWatching++;
		int pIndice = watching[pIndiceWatching];

		assert p == (lits[pIndice] ^ 1);
		assert watched[pIndice];

		// the greatest coefficient of the watched literals is necessary
		// (pIndice excluded)
		long maxCoef = maximalCoefficient(pIndice);

		// update watching and watched w.r.t. to the propagation of p
		// new literals will be watched, maxCoef could be changed
		maxCoef = updateWatched(maxCoef, pIndice);

			WatchPbLongCP wpb = (WatchPbLongCP) pb;
			if (degree != wpb.degree || coefs.length != wpb.coefs.length
					|| lits.length != wpb.lits.length) {
				return false;
			}
			int lit;
			boolean ok;
			for (int ilit = 0; ilit < coefs.length; ilit++) {
				lit = lits[ilit];
				ok = false;
				for (int ilit2 = 0; ilit2 < coefs.length; ilit2++)
					if (wpb.lits[ilit2] == lit) {
						if (wpb.coefs[ilit2] != coefs[ilit]) {
							return false;
						}

						ok = true;
						break;

					}
				if (!ok) {
					return false;
				}
			}
			return true;
		} catch (ClassCastException e) {
			return false;
		}
	}

	@Override
	public int hashCode() {
		long sum = 0;
		for (int p : lits) {
			sum += p;
		}
		return (int) sum / lits.length;
	}

	public void forwardActivity(double claInc) {
		if (!learnt) {
			activity += claInc;
		}
	}

	public long[] getLongCoefs() {

			}

			sort(from, i);
			sort(i, to);
		}

	}

	@Override
	public String toString() {
		StringBuffer stb = new StringBuffer();

		if (lits.length > 0) {
			for (int i = 0; i < lits.length; i++) {
				// if (voc.isUnassigned(lits[i])) {
				stb.append(" + ");
				stb.append(this.coefs[i]);
				stb.append(".");
				stb.append(Lits.toString(this.lits[i]));
				stb.append("[");
				stb.append(voc.valueToString(lits[i]));
				stb.append("@");
				stb.append(voc.getLevel(lits[i]));
				stb.append("]");
				stb.append(" ");
				// }
			}
			stb.append(">= ");
			stb.append(this.degree);
		}
		return stb.toString();
	}

	public void assertConstraint(UnitPropagationListener s) {

		if (outclause.degree <= 0) {
			return null;
		}

		outclause.computeWatches();

		outclause.computePropagation(s);

		return outclause;

	}

	/**
	 * Number of really watched literals. It should return the same value as
	 * watchingCount.
	 * 
	 * This method must only be called for assertions.
	 * 
	 * @return number of watched literals.
	 */
	protected int nbOfWatched() {
		int retour = 0;
		for (int ind = 0; ind < this.watched.length; ind++) {
			for (int i = 0; i < watchingCount; i++)
				if (watching[i] == ind)
					assert watched[ind];
			retour += (this.watched[ind]) ? 1 : 0;
		}
		return retour;
	}

	/**
	 * Propagation of a falsified literal
	 * 
	 * @param s
	 *            the solver
	 * @param p
	 *            the propagated literal (it must be falsified)
	 * @return false iff there is a conflict
	 */
	public boolean propagate(UnitPropagationListener s, int p) {
		assert nbOfWatched() == watchingCount;
		assert watchingCount > 1;

		// finding the index for p in the array of literals (pIndice)
		// and in the array of watching (pIndiceWatching)
		int pIndiceWatching = 0;
		while (pIndiceWatching < watchingCount
				&& (lits[watching[pIndiceWatching]] ^ 1) != p)
			pIndiceWatching++;
		int pIndice = watching[pIndiceWatching];

		assert p == (lits[pIndice] ^ 1);
		assert watched[pIndice];

		return decorated().getObjectiveFunction();
	}

	public IConstr addAtMost(IVecInt literals, IVecInt coeffs, int degree)
			throws ContradictionException {
		throw new UnsupportedOperationException();
	}

	public IConstr addAtMost(IVecInt literals, IVec<BigInteger> coeffs,
			BigInteger degree) throws ContradictionException {
		throw new UnsupportedOperationException();
	}

	public IConstr addAtLeast(IVecInt literals, IVecInt coeffs, int degree)
			throws ContradictionException {
		throw new UnsupportedOperationException();
	}

	public IConstr addAtLeast(IVecInt literals, IVec<BigInteger> coeffs,
			BigInteger degree) throws ContradictionException {
		throw new UnsupportedOperationException();
	}

	public IConstr addExactly(IVecInt literals, IVecInt coeffs, int weight)
			throws ContradictionException {
		throw new UnsupportedOperationException();
	}

	public IConstr addExactly(IVecInt literals, IVec<BigInteger> coeffs,
			BigInteger weight) throws ContradictionException {
		throw new UnsupportedOperationException();
	}
}

	}

	public IConstr addAtMost(IVecInt literals, IVecInt coeffs, int degree)
			throws ContradictionException {
		throw new UnsupportedOperationException();
	}

	public IConstr addAtMost(IVecInt literals, IVec<BigInteger> coeffs,
			BigInteger degree) throws ContradictionException {
		throw new UnsupportedOperationException();
	}

	public IConstr addAtLeast(IVecInt literals, IVecInt coeffs, int degree)
			throws ContradictionException {
		throw new UnsupportedOperationException();
	}

	public IConstr addAtLeast(IVecInt literals, IVec<BigInteger> coeffs,
			BigInteger degree) throws ContradictionException {
		throw new UnsupportedOperationException();
	}

	public IConstr addExactly(IVecInt literals, IVecInt coeffs, int weight)
			throws ContradictionException {
		throw new UnsupportedOperationException();
	}

	public IConstr addExactly(IVecInt literals, IVec<BigInteger> coeffs,
			BigInteger weight) throws ContradictionException {
		throw new UnsupportedOperationException();
	}

}

		assert watchingCount == nbOfWatched();

		watched[pIndice] = true;
		watching[watchingCount++] = pIndice;

		assert watchingCount == nbOfWatched();
	}

	/**
	 * build a pseudo boolean constraint from a specific data structure. For
	 * learnt constraints.
	 * 
	 * @param s
	 *            a unit propagation listener (usually the solver)
	 * @param mpb
	 *            data structure which contains literals of the constraint,
	 *            coefficients (a0, a1, ... an), and the degree of the
	 *            constraint (k). The constraint is a "more than" constraint.
	 * @return a new PB constraint or null if a trivial inconsistency is
	 *         detected.
	 */
	public static WatchPbLong normalizedWatchPbNew(ILits voc,
			IDataStructurePB mpb) {
		return new MinWatchPbLong(voc, mpb);
	}

	/**
	 * the maximal coefficient for the watched literals
	 * 
	 * @param pIndice
	 *            propagated literal : its coefficient is excluded from the
	 *            search of the maximal coefficient
	 * @return the maximal coefficient for the watched literals
	 */
	protected long maximalCoefficient(int pIndice) {
		long maxCoef = 0;
		for (int i = 0; i < watchingCount; i++)
			if (coefs[watching[i]] > maxCoef && watching[i] != pIndice) {
				maxCoef = coefs[watching[i]];
			}

		assert learnt || maxCoef != 0;
		// DLB assert maxCoef!=0;
		return maxCoef;
	}

	/**
	 * update arrays watched and watching w.r.t. the propagation of a literal.
	 * 
	 * return the maximal coefficient of the watched literals (could have been
	 * changed).
	 * 
	 * @param mc
	 *            the current maximal coefficient of the watched literals
	 * @param pIndice
	 *            the literal propagated (falsified)
	 * @return the new maximal coefficient of the watched literals
	 */
	protected long updateWatched(long mc, int pIndice) {
		long maxCoef = mc;
		// if not all the literals are watched
		if (watchingCount < size()) {
			// the watchCumul sum will have to be updated
			// long upWatchCumul = watchCumul - coefs[pIndice];
			long upWatchCumul = 0;

			}
		return poss;
	}

	/**
	 * compute the sum of the coefficients of the satisfied or non-assigned
	 * literals of the current constraint (usually called poss)
	 * 
	 * @return poss
	 */
	public long computeLeftSide() {
		return computeLeftSide(this.coefs);
	}

	/**
	 * tests if the constraint is still satisfiable.
	 * 
	 * this method is only called in assertions.
	 * 
	 * @return the constraint is satisfiable
	 */
	protected boolean isSatisfiable() {
		return computeLeftSide() >= degree;
	}

	/**
	 * is the constraint a learnt constraint ?
	 * 
	 * @return true if the constraint is learnt, else false
	 * @see org.sat4j.specs.IConstr#learnt()
	 */
	public boolean learnt() {
		return learnt;
	}

	/**
	 * The constraint is the reason of a unit propagation.
	 * 
	 * @return true
	 */
	public boolean locked() {
		for (int p : lits) {
			if (voc.getReason(p) == this) {
				return true;
			}
		}
		return false;
	}

	/**
	 * ppcm : least common multiple for two integers (plus petit commun
	 * multiple)
	 * 
	 * @param a
	 *            one integer
	 * @param b
	 *            the other integer
	 * @return the least common multiple of a and b
	 */
	protected static BigInteger ppcm(BigInteger a, BigInteger b) {
		return a.divide(a.gcd(b)).multiply(b);
	}

	/**
	 * to re-scale the activity of the constraint
	 * 
	 * @param d
	 *            adjusting factor
	 */
	public void rescaleBy(double d) {
		activity *= d;
	}

	void selectionSort(int from, int to) {
		int i, j, best_i;
		long tmp;

		super(solver);
	}

	/**
	 * read the first comment line to get the number of variables and the number
	 * of constraints in the file calls metaData with the data that was read
	 * 
	 * @throws IOException
	 * @throws ParseFormatException
	 */
	@Override
	protected void readMetaData() throws IOException, ParseFormatException {
		char c;
		String s;

		// get the number of variables and constraints
		c = get();
		if (c != '*')
			throw new ParseFormatException(
					"First line of input file should be a comment");
		s = readWord();
		if (eof() || !"#variable=".equals(s))
			throw new ParseFormatException(
					"First line should contain #variable= as first keyword");

		nbVars = Integer.parseInt(readWord());
		nbNewSymbols = nbVars + 1;

		s = readWord();
		if (eof() || !"#constraint=".equals(s))
			throw new ParseFormatException(
					"First line should contain #constraint= as second keyword");

		nbConstr = Integer.parseInt(readWord());
		charAvailable = false;
		if (!eol()) {
			String rest = in.readLine();

			if (rest.contains("#soft")) {

		while ((watchCumul - coefs[0]) < degree && (free > 0)) {
			free = 0;
			// looking for the literal falsified
			// at the least (lowest ?) level
			maxlevel = -1;
			maxi = -1;
			for (int i = 0; i < lits.length; i++) {
				if (voc.isFalsified(lits[i]) && !watched[i]) {
					free++;
					level = voc.getLevel(lits[i]);
					if (level > maxlevel) {
						maxi = i;
						maxlevel = level;
					}
				}
			}

			if (free > 0) {
				assert maxi >= 0;
				voc.watch(lits[maxi] ^ 1, this);
				watching[watchingCount++] = maxi;
				watched[maxi] = true;
				// update of the watchCumul value
				watchCumul = watchCumul + coefs[maxi];

		while (watchCumulMinusValueIsLessThanDegree(coefs[0]) && (free > 0)) {
			free = 0;
			// looking for the literal falsified
			// at the least (lowest ?) level
			maxlevel = -1;
			maxi = -1;
			for (int i = 0; i < lits.length; i++) {
				if (voc.isFalsified(lits[i]) && !watched[i]) {
					free++;
					level = voc.getLevel(lits[i]);
					if (level > maxlevel) {
						maxi = i;
						maxlevel = level;
					}
				}
			}

			if (free > 0) {
				assert maxi >= 0;
				voc.watch(lits[maxi] ^ 1, this);
				watching[watchingCount++] = maxi;
				watched[maxi] = true;

		while (watchCumulMinusValueIsLessThanDegree(coefs[0]) && (free > 0)) {
			free = 0;
			// looking for the literal falsified
			// at the least (lowest ?) level
			maxlevel = -1;
			maxi = -1;
			for (int i = 0; i < lits.length; i++) {
				if (voc.isFalsified(lits[i]) && !watched[i]) {
					free++;
					level = voc.getLevel(lits[i]);
					if (level > maxlevel) {
						maxi = i;
						maxlevel = level;
					}
				}
			}

			if (free > 0) {
				assert maxi >= 0;
				voc.watch(lits[maxi] ^ 1, this);
				watching[watchingCount++] = maxi;
				watched[maxi] = true;

		}
	}

	/**
	 * the constraint is learnt
	 */
	public void setLearnt() {
		learnt = true;
	}

	/**
	 * simplify the constraint (if it is satisfied)
	 * 
	 * @return true if the constraint is satisfied, else false
	 */
	public boolean simplify() {
		long cumul = 0;

		int i = 0;
		while (i < lits.length && cumul < degree) {
			if (voc.isSatisfied(lits[i])) {
				// strong measure
				cumul = cumul + coefs[i];
			}
			i++;
		}

		return (cumul >= degree);
	}

	public final int size() {
		return lits.length;
	}

	/**
	 * sort coefficient and literal arrays
	 */
	final protected void sort() {
		assert this.lits != null;
		if (coefs.length > 0) {
			this.sort(0, size());

			int i = from - 1;
			int j = to;
			int tmp2;

			for (;;) {
				do
					i++;
				while ((coefs[i] > pivot)
						|| ((coefs[i] == pivot) && (lits[i] > litPivot)));
				do
					j--;
				while ((pivot > coefs[j])
						|| ((coefs[j] == pivot) && (lits[j] < litPivot)));

				if (i >= j)
					break;

				tmp = coefs[i];
				coefs[i] = coefs[j];
				coefs[j] = tmp;

public class UserFriendlyPBStringSolver<T> extends DimacsStringSolver implements
		IPBSolver {

	private static final String FAKE_I_CONSTR_MSG = "Fake IConstr";

	/**
	 * 
	 */
	private static final long serialVersionUID = 1L;

	private int indxConstrObj;

	private int nbOfConstraints;

	private ObjectiveFunction obj;

	private boolean inserted = false;

	private static final IConstr FAKE_CONSTR = new IConstr() {

		public int size() {
			throw new UnsupportedOperationException(FAKE_I_CONSTR_MSG);
		}

		public boolean learnt() {
			throw new UnsupportedOperationException(FAKE_I_CONSTR_MSG);
		}

		public double getActivity() {
			throw new UnsupportedOperationException(FAKE_I_CONSTR_MSG);
		}

		public int get(int i) {
			throw new UnsupportedOperationException(FAKE_I_CONSTR_MSG);
		}

		public boolean canBePropagatedMultipleTimes() {
			throw new UnsupportedOperationException(FAKE_I_CONSTR_MSG);
		}
	};

		MinWatchPbLongCP outclause = new MinWatchPbLongCP(voc, lits, coefs,
				degree);

		if (outclause.degree <= 0) {
			return null;
		}

		outclause.computeWatches();

		outclause.computePropagation(s);

		return outclause;

	}

	/**
	 * Number of really watched literals. It should return the same value as
	 * watchingCount.
	 * 
	 * This method must only be called for assertions.
	 * 
	 * @return number of watched literals.
	 */
	protected int nbOfWatched() {
		int retour = 0;
		for (int ind = 0; ind < this.watched.length; ind++) {
			for (int i = 0; i < watchingCount; i++)
				if (watching[i] == ind)
					assert watched[ind];
			retour += (this.watched[ind]) ? 1 : 0;
		}
		return retour;
	}

	public OriginalHTClausePB(IVecInt ps, ILits voc) {
		super(ps, voc);
	}

	/**
     * 
     */
	private static final long serialVersionUID = 1L;

	public IVecInt computeAnImpliedClause() {
		return null;
	}

	public BigInteger getCoef(int literal) {
		return BigInteger.ONE;
	}

	public BigInteger[] getCoefs() {
		BigInteger[] tmp = new BigInteger[size()];
		for (int i = 0; i < tmp.length; i++)
			tmp[i] = BigInteger.ONE;
		return tmp;
	}

	public BigInteger getDegree() {
		return BigInteger.ONE;
	}

	/**
	 * Creates a brand new clause, presumably from external data. Performs all
	 * sanity checks.
	 * 
	 * @param s
	 *            the object responsible for unit propagation
	 * @param voc
	 *            the vocabulary
	 * @param literals
	 *            the literals to store in the clause
	 * @return the created clause or null if the clause should be ignored
	 *         (tautology for example)
	 */
	public static OriginalHTClausePB brandNewClause(UnitPropagationListener s,

	}

	/**
	 * is the constraint a learnt constraint ?
	 * 
	 * @return true if the constraint is learnt, else false
	 * @see org.sat4j.specs.IConstr#learnt()
	 */
	public boolean learnt() {
		return learnt;
	}

	/**
	 * The constraint is the reason of a unit propagation.
	 * 
	 * @return true
	 */
	public boolean locked() {
		for (int p : lits) {
			if (voc.getReason(p) == this) {
				return true;
			}
		}
		return false;
	}

	/**
	 * ppcm : least common multiple for two integers (plus petit commun
	 * multiple)
	 * 
	 * @param a
	 *            one integer
	 * @param b
	 *            the other integer
	 * @return the least common multiple of a and b
	 */
	protected static BigInteger ppcm(BigInteger a, BigInteger b) {
		return a.divide(a.gcd(b)).multiply(b);
	}

	/**
	 * to re-scale the activity of the constraint
	 * 
	 * @param d
	 *            adjusting factor
	 */
	public void rescaleBy(double d) {
		activity *= d;
	}

	void selectionSort(int from, int to) {
		int i, j, best_i;

	public OriginalBinaryClausePB(IVecInt ps, ILits voc) {
		super(ps, voc);
		// TODO Auto-generated constructor stub
	}

	/**
     * 
     */
	private static final long serialVersionUID = 1L;

	public IVecInt computeAnImpliedClause() {
		return null;
	}

	public BigInteger getCoef(int literal) {
		return BigInteger.ONE;
	}

	public BigInteger[] getCoefs() {
		BigInteger[] tmp = new BigInteger[size()];
		for (int i = 0; i < tmp.length; i++)
			tmp[i] = BigInteger.ONE;
		return tmp;
	}

	public BigInteger getDegree() {
		return BigInteger.ONE;
	}

			BigInteger degree) throws ContradictionException {
		StringBuffer out = getOut();
		assert literals.size() == coeffs.size();
		nbOfConstraints++;
		for (int i = 0; i < literals.size(); i++) {
			out.append(coeffs.get(i));
			out.append(" x");
			out.append(literals.get(i));
			out.append(" ");
		}
		out.append(">= ");
		out.append(degree);
		out.append(" ;\n");
		return FAKE_CONSTR;

	}

	public IConstr addExactly(IVecInt literals, IVecInt coeffs, int weight)