return this.constrs.values();
    }

    @Override
    public int[] findModel() throws TimeoutException {
        this.assump = VecInt.EMPTY;
        IVecInt extraVariables = new VecInt();
        for (Integer p : this.constrs.keySet()) {
            extraVariables.push(-p);
        }
        return super.findModel(extraVariables);
    }

    @Override
    public int[] findModel(IVecInt assumps) throws TimeoutException {
        this.assump = assumps;
        IVecInt extraVariables = new VecInt();
        assumps.copyTo(extraVariables);
        for (Integer p : this.constrs.keySet()) {
            extraVariables.push(-p);
        }
        return super.findModel(extraVariables);
    }

    @Override
    public boolean isSatisfiable() throws TimeoutException {
        this.assump = VecInt.EMPTY;
        IVecInt extraVariables = new VecInt();
        for (Integer p : this.constrs.keySet()) {
            extraVariables.push(-p);
        }
        return super.isSatisfiable(extraVariables);
    }

    @Override
    public boolean isSatisfiable(boolean global) throws TimeoutException {
        this.assump = VecInt.EMPTY;
        IVecInt extraVariables = new VecInt();
        for (Integer p : this.constrs.keySet()) {
            extraVariables.push(-p);
        }
        return super.isSatisfiable(extraVariables, global);
    }

    @Override
    public boolean isSatisfiable(IVecInt assumps) throws TimeoutException {
        this.assump = assumps;
        IVecInt extraVariables = new VecInt();
        assumps.copyTo(extraVariables);
        for (Integer p : this.constrs.keySet()) {
            extraVariables.push(-p);
        }
        return super.isSatisfiable(extraVariables);
    }

    @Override
    public boolean isSatisfiable(IVecInt assumps, boolean global)
            throws TimeoutException {
        this.assump = assumps;
        IVecInt extraVariables = new VecInt();
        assumps.copyTo(extraVariables);
        for (Integer p : this.constrs.keySet()) {
            extraVariables.push(-p);
        }
        return super.isSatisfiable(extraVariables, global);
    }

    @Override
    public int[] model() {
        int[] fullmodel = super.modelWithInternalVariables();

        final int n = literals.size();

        int y[] = new int[n - 1];

        for (int i = 0; i < n - 1; i++) {
            y[i] = solver.nextFreeVarId(true);
        }

        IVecInt clause = new VecInt();

        // Constraint \bigwedge_{i=1}{n-2} (\neg y_{i+1} \vee y_i)
        for (int i = 1; i <= n - 2; i++) {
            clause.push(-y[i]);
            clause.push(y[i - 1]);
            group.add(solver.addClause(clause));
            clause.clear();
        }

        // Constraint \bigwedge_{i=2}{n-1} (\neg y_{i-1} \vee y_i \vee x_i)
        for (int i = 2; i <= n - 1; i++) {
            clause.push(-y[i - 2]);
            clause.push(y[i - 1]);
            clause.push(literals.get(i - 1));
            group.add(solver.addClause(clause));
            clause.clear();
        }

        // Constraint \bigwedge_{i=2}{n-1} (\neg x_i \vee y_{i-1)})
        for (int i = 2; i <= n - 1; i++) {
            clause.push(-literals.get(i - 1));
            clause.push(y[i - 2]);
            group.add(solver.addClause(clause));
            clause.clear();
        }

        // Constraint \bigwedge_{i=2}{n-1} (\neg x_i \vee \neg y_i)
        for (int i = 2; i <= n - 1; i++) {
            clause.push(-literals.get(i - 1));
            clause.push(-y[i - 1]);
            group.add(solver.addClause(clause));
            clause.clear();
        }

        // Constraint y_1 \vee x_1
        clause.push(y[0]);
        clause.push(literals.get(0));
        group.add(solver.addClause(clause));
        clause.clear();

        // Constraint \neg y_1 \vee \neg x_1
        clause.push(-y[0]);
        clause.push(-literals.get(0));
        group.add(solver.addClause(clause));
        clause.clear();

        // Constraint \neg y_{n-1} \vee x_n
        clause.push(-y[n - 2]);
        clause.push(literals.get(n - 1));

            results.push(-firstExplanation.get(0));
            return results;
        }
        if (solver.isVerbose()) {
            System.out.print(solver.getLogPrefix() + "initial unsat core ");
            firstExplanation.sort();
            for (IteratorInt it = firstExplanation.iterator(); it.hasNext();) {
                System.out.print(constrs.get(-it.next()));
                System.out.print(" ");
            }
            System.out.println();
        }
        for (int i = 0; i < firstExplanation.size();) {
            if (assumps.contains(firstExplanation.get(i))) {
                firstExplanation.delete(i);
            } else {
                i++;
            }
        }
        Set<Integer> constraintsVariables = constrs.keySet();
        IVecInt remainingVariables = new VecInt(constraintsVariables.size());
        for (Integer v : constraintsVariables) {
            remainingVariables.push(v);
        }
        int p;
        for (IteratorInt it = firstExplanation.iterator(); it.hasNext();) {
            p = it.next();
            if (p < 0) {
                p = -p;
            }
            remainingVariables.remove(p);
            encodingAssumptions.push(p);
        }

public class QuickXplainStrategy implements MinimizationStrategy {

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

    private boolean computationCanceled;

    public void cancelExplanationComputation() {
        this.computationCanceled = true;
    }

    public IVecInt explain(ISolver solver, Map<Integer, ?> constrs,
            IVecInt assumps) throws TimeoutException {
        this.computationCanceled = false;
        IVecInt encodingAssumptions = new VecInt(constrs.size()
                + assumps.size());
        assumps.copyTo(encodingAssumptions);
        IVecInt firstExplanation = solver.unsatExplanation();
        IVecInt results = new VecInt(firstExplanation.size());
        if (firstExplanation.size() == 1) {
            results.push(-firstExplanation.get(0));
            return results;
        }
        if (solver.isVerbose()) {
            System.out.print(solver.getLogPrefix() + "initial unsat core ");
            firstExplanation.sort();
            for (IteratorInt it = firstExplanation.iterator(); it.hasNext();) {
                System.out.print(constrs.get(-it.next()));
                System.out.print(" ");
            }
            System.out.println();

    }

    @Override
    public IConstr addAtLeast(ISolver solver, IVecInt literals, int k)
            throws ContradictionException {

        IVecInt newLits = new VecInt();
        for (int i = 0; i < literals.size(); i++) {
            newLits.push(-literals.get(i));
        }

        return addAtMost(solver, newLits, literals.size() - k);
    }

    @Override
    public IConstr addExactlyOne(ISolver solver, IVecInt literals)
            throws ContradictionException {
        ConstrGroup group = new ConstrGroup();

        group.add(addAtLeastOne(solver, literals));
        group.add(addAtMostOne(solver, literals));

        return group;
    }

    @Override
    public IConstr addExactly(ISolver solver, IVecInt literals, int degree)
            throws ContradictionException {
        ConstrGroup group = new ConstrGroup();

        group.add(addAtLeast(solver, literals, degree));
        group.add(addAtMost(solver, literals, degree));

        return group;
    }

}

public class MixedDataStructureSingleWL extends AbstractDataStructureFactory {

    private static final long serialVersionUID = 1L;

    /*
     * (non-Javadoc)
     * 
     * @see
     * org.sat4j.minisat.DataStructureFactory#createCardinalityConstraint(org
     * .sat4j.datatype.VecInt, int)
     */
    @Override
    public Constr createCardinalityConstraint(IVecInt literals, int degree)
            throws ContradictionException {
        return AtLeast.atLeastNew(this.solver, getVocabulary(), literals,
                degree);
    }

    /*
     * (non-Javadoc)
     * 
     * @see
     * org.sat4j.minisat.DataStructureFactory#createClause(org.sat4j.datatype
     * .VecInt)
     */
    public Constr createClause(IVecInt literals) throws ContradictionException {
        IVecInt v = Clauses.sanityCheck(literals, getVocabulary(), this.solver);
        if (v == null) {
            // tautological clause
            return null;
        }
        if (v.size() == 1) {
            return new UnitClause(v.last());
        }
        if (v.size() == 2) {
            return OriginalBinaryClause.brandNewClause(this.solver,
                    getVocabulary(), v);
        }
        return OriginalWLClause.brandNewClause(this.solver, getVocabulary(), v);
    }

    public Constr createUnregisteredClause(IVecInt literals) {

    public Constr createClause(IVecInt literals) throws ContradictionException {
        IVecInt v = Clauses.sanityCheck(literals, getVocabulary(), this.solver);
        if (v == null) {
            // tautological clause
            return null;
        }
        if (v.size() == 1) {
            return new UnitClause(v.last());
        }
        if (v.size() == 2) {
            return OriginalBinaryClause.brandNewClause(this.solver,
                    getVocabulary(), v);
        }
        return OriginalWLClause.brandNewClause(this.solver, getVocabulary(), v);
    }

    public Constr createUnregisteredClause(IVecInt literals) {
        return new LearntWLClause(literals, getVocabulary());
    }

    @Override
    protected ILits createLits() {
        return new Lits();
    }
}

public class MixedDataStructureDanielWL extends AbstractDataStructureFactory {

    private static final long serialVersionUID = 1L;

    /*
     * (non-Javadoc)
     * 
     * @see
     * org.sat4j.minisat.DataStructureFactory#createCardinalityConstraint(org
     * .sat4j.datatype.VecInt, int)
     */
    @Override
    public Constr createCardinalityConstraint(IVecInt literals, int degree)
            throws ContradictionException {
        return AtLeast.atLeastNew(this.solver, getVocabulary(), literals,
                degree);
    }

    /*
     * (non-Javadoc)
     * 
     * @see
     * org.sat4j.minisat.DataStructureFactory#createClause(org.sat4j.datatype
     * .VecInt)
     */
    public Constr createClause(IVecInt literals) throws ContradictionException {
        IVecInt v = Clauses.sanityCheck(literals, getVocabulary(), this.solver);
        if (v == null) {
            // tautological clause
            return null;
        }
        if (v.size() == 1) {
            return new UnitClause(v.last());
        }
        if (v.size() == 2) {
            return OriginalBinaryClause.brandNewClause(this.solver,
                    getVocabulary(), v);
        }
        return OriginalWLClause.brandNewClause(this.solver, getVocabulary(), v);

            System.out.println();
        }
        for (int i = 0; i < firstExplanation.size();) {
            if (assumps.contains(firstExplanation.get(i))) {
                firstExplanation.delete(i);
            } else {
                i++;
            }
        }
        Set<Integer> constraintsVariables = constrs.keySet();
        IVecInt remainingVariables = new VecInt(constraintsVariables.size());
        for (Integer v : constraintsVariables) {
            remainingVariables.push(v);
        }
        int p;
        for (IteratorInt it = firstExplanation.iterator(); it.hasNext();) {
            p = it.next();
            if (p < 0) {
                p = -p;
            }
            remainingVariables.remove(p);

            for (int i = nVars() + 1; i <= realNumberOfVariables(); i++) {
                if (this.voc.belongsToPool(i)) {
                    int p = this.voc.getFromPool(i);
                    if (!this.voc.isUnassigned(p)) {
                        tempmodel.push(this.voc.isSatisfied(p) ? i : -i);
                        this.userbooleanmodel[i - 1] = this.voc.isSatisfied(p);
                        if (this.voc.getReason(p) == null) {
                            this.decisions.push(tempmodel.last());
                        } else {
                            this.implied.push(tempmodel.last());
                        }
                    }
                }
            }
            this.fullmodel = new int[tempmodel.size()];

    AIGReader(ISolver s) {
        this.solver = new GateTranslator(s);
    }

    @Override
    public String decode(int[] model) {
        StringBuffer stb = new StringBuffer();
        for (int i = 0; i < this.nbinputs; i++) {
            stb.append(model[i] > 0 ? 1 : 0);
        }
        return stb.toString();
    }

    @Override
    public void decode(int[] model, PrintWriter out) {
        for (int i = 0; i < this.nbinputs; i++) {
            out.print(model[i] > 0 ? 1 : 0);
        }
    }

    public Constr createClause(IVecInt literals) throws ContradictionException {
        IVecInt v = Clauses.sanityCheck(literals, getVocabulary(), this.solver);
        if (v == null) {
            // tautological clause
            return null;
        }
        if (v.size() == 1) {
            return new UnitClause(v.last());
        }
        if (v.size() == 2) {
            return OriginalBinaryClause.brandNewClause(this.solver,
                    getVocabulary(), v);
        }
        return OriginalWLClause.brandNewClause(this.solver, getVocabulary(), v);
    }

    public Constr createUnregisteredClause(IVecInt literals) {

        }
        if (this.voc.isFalsified(this.tail)) {
            outReason.push(neg(this.tail));
        }
    }

    /*
     * (non-Javadoc)
     * 
     * @see Constr#remove(Solver)
     */
    public void remove(UnitPropagationListener upl) {
        this.voc.watches(neg(this.head)).remove(this);
        this.voc.watches(neg(this.tail)).remove(this);
    }

    /*
     * (non-Javadoc)
     * 
     * @see Constr#simplify(Solver)
     */
    public boolean simplify() {
        if (this.voc.isSatisfied(this.head) || this.voc.isSatisfied(this.tail)) {
            return true;
        }

    }

    /*
     * For learnt clauses only @author leberre
     */
    public boolean locked() {
        return this.voc.getReason(this.head) == this
                || this.voc.getReason(this.tail) == this;
    }

    /**
     * @return the activity of the clause
     */
    public double getActivity() {
        return this.activity;
    }

    @Override
    public String toString() {
        StringBuffer stb = new StringBuffer();
        stb.append(Lits.toString(this.head));
        stb.append("["); //$NON-NLS-1$
        stb.append(this.voc.valueToString(this.head));
        stb.append("]"); //$NON-NLS-1$
        stb.append(" "); //$NON-NLS-1$

                    }
                }
                for (; i < Solver.this.learnts.size(); i++) {
                    Solver.this.learnts.set(j++, Solver.this.learnts.get(i));
                }
                if (Solver.this.verbose) {
                    Solver.this.out.log(getLogPrefix()
                            + "cleaning " + (Solver.this.learnts.size() - j) //$NON-NLS-1$
                            + " clauses out of " + Solver.this.learnts.size()); //$NON-NLS-1$ 
                    // out.flush();
                }
                Solver.this.learnts.shrinkTo(j);
            }

            public ConflictTimer getTimer() {

            }
            stb.append(">= "); //$NON-NLS-1$
            stb.append(this.degree);
        }
        return stb.toString();
    }

    /**
     * Updates information on the constraint in case of a backtrack
     * 
     * @param p
     *            unassigned literal
     */
    public void undo(int p) {
        // Le litt?ral observ? et falsifi? devient non assign?
        this.watchCumul++;
    }

    public void setLearnt() {
        throw new UnsupportedOperationException();
    }

    public void register() {
        throw new UnsupportedOperationException();
    }

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

    public int get(int i) {
        return this.lits[i];
    }

    public void assertConstraint(UnitPropagationListener s) {
        throw new UnsupportedOperationException();
    }

    }

    @Override
    public IConstr addExactlyOne(ISolver solver, IVecInt literals)
            throws ContradictionException {
        ConstrGroup group = new ConstrGroup();

        group.add(addAtLeastOne(solver, literals));
        group.add(addAtMostOne(solver, literals));

        return group;
    }

    @Override
    public IConstr addExactly(ISolver solver, IVecInt literals, int degree)
            throws ContradictionException {
        ConstrGroup group = new ConstrGroup();

        group.add(addAtLeast(solver, literals, degree));
        group.add(addAtMost(solver, literals, degree));

        return group;
    }