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

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

        this.watching = new int[this.coefs.length];
        this.watched = new boolean[this.coefs.length];
        this.activity = 0;
        this.watchCumul = 0;
        this.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 this.watchCumul == 0;
        assert this.watchingCount == 0;
        for (int i = 0; i < this.lits.length
                && this.watchCumul - this.coefs[0] < this.degree; i++) {
            if (!this.voc.isFalsified(this.lits[i])) {
                this.voc.watch(this.lits[i] ^ 1, this);
                this.watching[this.watchingCount++] = i;
                this.watched[i] = true;
                // update the initial value for watchCumul (poss)
                this.watchCumul = this.watchCumul + this.coefs[i];
            }
        }

        if (this.learnt) {
            watchMoreForLearntConstraint();
        }

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

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

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

            if (free > 0) {
                assert maxi >= 0;
                this.voc.watch(this.lits[maxi] ^ 1, this);
                this.watching[this.watchingCount++] = maxi;
                this.watched[maxi] = true;
                // update of the watchCumul value
                this.watchCumul = this.watchCumul + this.coefs[maxi];
                free--;
                assert free >= 0;
            }
        }
        assert this.lits.length == 1 || this.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 < this.lits.length
                && this.watchCumul - this.coefs[this.watching[ind]] < this.degree) {
            if (this.voc.isUnassigned(this.lits[ind])
                    && !s.enqueue(this.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(

            }

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

    }

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

        if (this.lits.length > 0) {
            for (int i = 0; i < this.lits.length; i++) {
                stb.append(" + ");
                stb.append(this.coefs[i]);
                stb.append(".");
                stb.append(Lits.toString(this.lits[i]));
                stb.append("[");
                stb.append(this.voc.valueToString(this.lits[i]));
                stb.append("@");
                stb.append(this.voc.getLevel(this.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 < this.lits.length; i++) {
            if (this.voc.isUnassigned(this.lits[i]) && tmp < this.coefs[i]) {
                boolean ret = s.enqueue(this.lits[i], this);
                assert ret;
            }
        }
    }

    public void register() {
        assert this.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[this.lits.length];
        System.arraycopy(this.lits, 0, litsBis, 0, this.lits.length);
        return litsBis;
    }

    public ILits getVocabulary() {
        return this.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 = this.coefs.length;
        while (cptCoefs > this.degree && index > 0) {
            cptCoefs = cptCoefs + this.coefs[--index];
        }
        if (index > 0 && index < size() / 2) {
            IVecInt literals = new VecInt(index);
            for (int j = 0; j <= index; j++) {
                literals.push(this.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 {

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

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

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

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

        assert this.watchCumul >= computeLeftSide();
        if (!this.learnt && this.watchCumul < this.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 < this.coefs.length
                && this.watchCumul - this.coefs[ind] < this.degree) {
            if (this.voc.isUnassigned(this.lits[ind])
                    && !s.enqueue(this.lits[ind], this)) {
                // because this happens during the building of a constraint.
                throw new ContradictionException("non satisfiable constraint");
            }
            ind++;
        }
        assert this.watchCumul >= computeLeftSide();
    }

    public boolean propagate(UnitPropagationListener s, int p) {
        assert nbOfWatched() == this.watchingCount;
        assert this.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 < this.watchingCount
                && (this.lits[this.watching[pIndiceWatching]] ^ 1) != p) {
            pIndiceWatching++;
        }
        int pIndice = this.watching[pIndiceWatching];

        assert p == (this.lits[pIndice] ^ 1);
        assert this.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 = this.watchCumul - this.coefs[pIndice];
        assert nbOfWatched() == this.watchingCount;

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

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

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

        return true;
    }

        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 < this.watchingCount; i++) {
            if (this.coefs[this.watching[i]] > maxCoef
                    && this.watching[i] != pIndice) {
                maxCoef = this.coefs[this.watching[i]];
            }
        }

        assert this.learnt || 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 (this.watchingCount < size()) {
            // the watchCumul sum will have to be updated
            long upWatchCumul = this.watchCumul - this.coefs[pIndice];

            // we must obtain upWatchCumul such that
            // upWatchCumul = degree + maxCoef
            long degreePlusMaxCoef = this.degree + maxCoef;
            for (int ind = 0; ind < this.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 (!this.voc.isFalsified(this.lits[ind]) && !this.watched[ind]) {
                    // watch one more
                    upWatchCumul = upWatchCumul + this.coefs[ind];
                    // update arrays watched and watching
                    this.watched[ind] = true;
                    assert this.watchingCount < size();
                    this.watching[this.watchingCount++] = ind;
                    this.voc.watch(this.lits[ind] ^ 1, this);
                    // this new watched literal could change the maximal
                    // coefficient
                    if (this.coefs[ind] > maxCoef) {
                        maxCoef = this.coefs[ind];
                        degreePlusMaxCoef = this.degree + maxCoef;
                    }
                }
            }
            // update watchCumul
            this.watchCumul = upWatchCumul + this.coefs[pIndice];
        }
        return maxCoef;
    }

}

                        && this.lits[j] < litPivot);

                if (i >= j) {
                    break;
                }

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

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

    }

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

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

    public void assertConstraint(UnitPropagationListener s) {

                        && i != pIndiceWatching
                        && !this.voc.isSatisfied(this.lits[this.watching[i]])
                        && !s.enqueue(this.lits[this.watching[i]], this)) {
                    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.
            this.voc.undos(p).push(this);
        }

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

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

        return true;
    }

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

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

        assert pIndice < this.lits.length;

        this.watchCumul = this.watchCumul + this.coefs[pIndice];

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

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

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

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

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

        // if no conflict, not(p) can be propagated
        // allow a later un-assignation
        this.voc.undos(p).push(this);
        // really update watchCumul
        this.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 = this.watchCumul - this.degree;
        // for each coefficient greater than limit
        while (ind < this.coefs.length && limit < this.coefs[ind]) {
            // its corresponding literal is implied
            if (this.voc.isUnassigned(this.lits[ind])
                    && !s.enqueue(this.lits[ind], this)) {
                // if it is not possible then there is a conflict
                assert !isSatisfiable();
                return false;
            }
            ind++;
        }

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

            WatchPbLongCP wpb = (WatchPbLongCP) pb;
            if (this.degree != wpb.degree
                    || this.coefs.length != wpb.coefs.length
                    || this.lits.length != wpb.lits.length) {
                return false;
            }
            int lit;
            boolean ok;
            for (int ilit = 0; ilit < this.coefs.length; ilit++) {
                lit = this.lits[ilit];
                ok = false;
                for (int ilit2 = 0; ilit2 < this.coefs.length; ilit2++) {
                    if (wpb.lits[ilit2] == lit) {
                        if (wpb.coefs[ilit2] != this.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 : this.lits) {
            sum += p;
        }
        return (int) sum / this.lits.length;
    }

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

    public long[] getLongCoefs() {

                }
            }
        }
    }

    protected abstract void computeWatches() throws ContradictionException;

    protected abstract 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 this.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 this.activity;
    }

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

    public void setActivity(double d) {
        if (this.learnt) {
            this.activity = d;
        }
    }

    /**
     * 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 < this.lits.length; i++) {
            if (!this.voc.isFalsified(this.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) {

        }
        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 < this.lits.length; i++) {
            if (this.coefs[i] > 0
                    && (!this.voc.isFalsified(this.lits[i]) || this.voc
                            .getLevel(this.lits[i]) >= dl)) {
                slack = slack + this.coefs[i];
            }
        }
        slack = slack - this.degree;
        if (slack < 0) {
            return false;
        }
        for (int i = 0; i < this.lits.length; i++) {
            if (this.coefs[i] > 0
                    && (this.voc.isUnassigned(this.lits[i]) || this.voc
                            .getLevel(this.lits[i]) >= dl)
                    && slack < this.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) {
        long sumfalsified = 0;

        return this.objs.size();
    }

    public IConstr addAtMost(IVecInt literals, IVecInt coeffs, int degree)
            throws ContradictionException {
        return decorated().addAtMost(literals, coeffs, degree);
    }

    public IConstr addAtMost(IVecInt literals, IVec<BigInteger> coeffs,
            BigInteger degree) throws ContradictionException {
        return decorated().addAtMost(literals, coeffs, degree);
    }

    public IConstr addAtLeast(IVecInt literals, IVecInt coeffs, int degree)
            throws ContradictionException {
        return decorated().addAtLeast(literals, coeffs, degree);
    }

    public IConstr addAtLeast(IVecInt literals, IVec<BigInteger> coeffs,
            BigInteger degree) throws ContradictionException {
        return decorated().addAtLeast(literals, coeffs, degree);
    }

    public IConstr addExactly(IVecInt literals, IVecInt coeffs, int weight)
            throws ContradictionException {
        return decorated().addExactly(literals, coeffs, weight);
    }

    public IConstr addExactly(IVecInt literals, IVec<BigInteger> coeffs,
            BigInteger weight) throws ContradictionException {
        return decorated().addExactly(literals, coeffs, weight);
    }

}

            }

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

    }

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

        if (this.lits.length > 0) {
            for (int i = 0; i < this.lits.length; i++) {
                stb.append(" + ");
                stb.append(this.coefs[i]);
                stb.append(".");
                stb.append(Lits.toString(this.lits[i]));
                stb.append("[");
                stb.append(this.voc.valueToString(this.lits[i]));
                stb.append("@");
                stb.append(this.voc.getLevel(this.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 < this.watchingCount; i++) {
                if (this.watching[i] == ind) {
                    assert this.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() == this.watchingCount;
        assert this.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 < this.watchingCount
                && (this.lits[this.watching[pIndiceWatching]] ^ 1) != p) {
            pIndiceWatching++;
        }
        int pIndice = this.watching[pIndiceWatching];

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

            BigInteger weight) throws ContradictionException {
        StringBuffer out = getOut();
        assert literals.size() == coeffs.size();
        this.nbOfConstraints++;
        int n = literals.size();
        if (n > 0) {
            out.append(coeffs.get(0));
            out.append("x");
            out.append(literals.get(0));
            out.append(" ");
        }
        BigInteger coeff;
        for (int i = 1; i < n; i++) {
            coeff = coeffs.get(i);
            if (coeff.signum() > 0) {
                out.append("+ " + coeff);
            } else {
                out.append("- " + coeff.negate());
            }
            out.append("x");
            out.append(literals.get(i));
            out.append(" ");
        }
        out.append("= ");

    public IConstr addExactly(IVecInt literals, IVecInt coeffs, int weight)
            throws ContradictionException {
        StringBuffer out = getOut();
        assert literals.size() == coeffs.size();
        this.nbOfConstraints++;
        int n = literals.size();
        if (n > 0) {
            out.append(coeffs.get(0));
            out.append("x");
            out.append(literals.get(0));
            out.append(" ");
        }
        int coeff;
        for (int i = 1; i < n; i++) {
            coeff = coeffs.get(i);
            if (coeff > 0) {
                out.append("+ " + coeff);
            } else {
                out.append("- " + coeff * -1);
            }
            out.append("x");
            out.append(literals.get(i));
            out.append(" ");
        }
        out.append("= ");

        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");
        }

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

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

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

            if (rest != null && rest.contains("#soft")) {

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

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

        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();
    }

            }
        }
        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() >= this.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 this.learnt;
    }

    /**
     * The constraint is the reason of a unit propagation.
     * 
     * @return true
     */
    public boolean locked() {
        for (int p : this.lits) {
            if (this.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) {
        this.activity *= d;
    }

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

    }

    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();
    }

        }
    }

    /**
     * the constraint is learnt
     */
    public void setLearnt() {
        this.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 < this.lits.length && cumul < this.degree) {
            if (this.voc.isSatisfied(this.lits[i])) {
                // strong measure
                cumul = cumul + this.coefs[i];
            }
            i++;
        }

        return cumul >= this.degree;
    }

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

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

                getOut().append("-1 x" + -p + " >= 0 ;\n");
            }
            this.nbOfConstraints++;
        }
        throw new TimeoutException();
    }

    @Override
    public boolean isSatisfiable(IVecInt assumps, boolean global)
            throws TimeoutException {
        return super.isSatisfiable(assumps, global);
    }

    public IConstr addPseudoBoolean(IVecInt lits, IVec<BigInteger> coeffs,
            boolean moreThan, BigInteger d) throws ContradictionException {
        if (moreThan) {
            return addAtLeast(lits, coeffs, d);
        }
        return addAtMost(lits, coeffs, d);
    }

    public void setObjectiveFunction(ObjectiveFunction obj) {
        this.obj = obj;
    }

    @Override
    public IConstr addAtLeast(IVecInt literals, int degree)
            throws ContradictionException {
        StringBuffer out = getOut();
        this.nbOfConstraints++;
        int negationweight = 0;
        int p;

                        && i != pIndiceWatching
                        && !this.voc.isSatisfied(this.lits[this.watching[i]])
                        && !s.enqueue(this.lits[this.watching[i]], this)) {
                    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.
            this.voc.undos(p).push(this);
        }

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

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

        return true;
    }

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

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

                if (i >= j) {
                    break;
                }

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

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

        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 < this.watchingCount; i++) {
                if (this.watching[i] == ind) {
                    assert this.watched[ind];
                }
            }
            retour += this.watched[ind] ? 1 : 0;
        }
        return retour;
    }

public class OPBStringSolver 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);
        }
    };

    /**
	 * 
	 */
    public OPBStringSolver() {

        int tmp2;

        for (i = from; i < to - 1; i++) {
            bestIndex = i;
            for (j = i + 1; j < to; j++) {
                if (this.coefs[j] > this.coefs[bestIndex]
                        || this.coefs[j] == this.coefs[bestIndex]
                        && this.lits[j] > this.lits[bestIndex]) {
                    bestIndex = j;
                }
            }
            tmp = this.coefs[i];
            this.coefs[i] = this.coefs[bestIndex];
            this.coefs[bestIndex] = 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);
        }
    };

    }

    @Override
    public int newVar(int howmany) {
        StringBuffer out = getOut();
        setNbVars(howmany);
        // to add later the number of constraints
        this.indxConstrObj = out.length();
        out.append("\n");
        return howmany;
    }

    @Override
    public void setExpectedNumberOfClauses(int nb) {
    }

    public ObjectiveFunction getObjectiveFunction() {
        return this.obj;
    }

    @Override
    public int nConstraints() {
        return this.nbOfConstraints;
    }

    public IConstr addAtMost(IVecInt literals, IVecInt coeffs, int degree)
            throws ContradictionException {
        StringBuffer out = getOut();
        assert literals.size() == coeffs.size();
        this.nbOfConstraints++;

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);
        }
    };

    }

    /**
     * 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 this.learnt;
    }

    /**
     * The constraint is the reason of a unit propagation.
     * 
     * @return true
     */
    public boolean locked() {
        for (int p : this.lits) {
            if (this.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) {
        this.activity *= d;
    }

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

    private MaxWatchPbLongCP(ILits voc, IDataStructurePB mpb) {

        super(mpb);
        this.voc = voc;

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

    /**
     * Builds a PB constraint for a0.x0 + a1.x1 + ... + an.xn >= k
     * 
     * @param voc
     *            all the possible variables (vocabulary)
     * @param lits
     *            literals of the constraint (x0,x1, ... xn)
     * @param coefs
     *            coefficients of the left side of the constraint (a0, a1, ...
     *            an)
     * @param degree
     *            degree of the constraint (k)
     */
    private MaxWatchPbLongCP(ILits voc, int[] lits, BigInteger[] coefs,

        for (int i = 0; i < this.lits.length; i++) {
            if (this.voc.isFalsified(this.lits[i])) {
                if (this.learnt) {
                    this.voc.undos(this.lits[i] ^ 1).push(this);
                    this.voc.watch(this.lits[i] ^ 1, this);
                }
            } else {
                // updating of the initial value for the counter
                this.voc.watch(this.lits[i] ^ 1, this);
                this.watchCumul = this.watchCumul + this.coefs[i];

    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,

    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;
    }

    public void undo(int p) {
        this.voc.watch(p, this);
        int pIndice = 0;
        while ((this.lits[pIndice] ^ 1) != p) {
            pIndice++;
        }

        assert pIndice < this.lits.length;

        this.watchCumul = this.watchCumul + this.coefs[pIndice];

        assert this.watchingCount == nbOfWatched();

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

        assert this.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 WatchPbLongCP normalizedWatchPbNew(ILits voc,

        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 < this.watchingCount; i++) {
                if (this.watching[i] == ind) {
                    assert this.watched[ind];
                }
            }
            retour += this.watched[ind] ? 1 : 0;
        }
        return retour;
    }

            BigInteger weight) throws ContradictionException {
        StringBuffer out = getOut();
        assert literals.size() == coeffs.size();
        this.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(weight);
        out.append(" ;\n");
        return FAKE_CONSTR;
    }

            BigInteger degree) throws ContradictionException {
        StringBuffer out = getOut();
        assert literals.size() == coeffs.size();
        this.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;

    }