}

	public void printStat(PrintStream output, String prefix) {
		// TODO Auto-generated method stub
	}

	public void printStat(PrintWriter output, String prefix) {
		// TODO Auto-generated method stub

	}

	public Map<String, Number> getStat() {
		// TODO Auto-generated method stub
		return null;
	}

	public String toString(String prefix) {
		return "Dimacs output solver";
	}

	public void clearLearntClauses() {
		// TODO Auto-generated method stub

	}

	public int[] model() {
		throw new UnsupportedOperationException();
	}

	public boolean model(int var) {
		throw new UnsupportedOperationException();
	}

	public boolean isSatisfiable() throws TimeoutException {
		throw new TimeoutException("There is no real solver behind!");
	}

	public boolean isSatisfiable(IVecInt assumps) throws TimeoutException {
		throw new TimeoutException("There is no real solver behind!");
	}

	public int[] findModel() throws TimeoutException {
		throw new UnsupportedOperationException();
	}

	public int[] findModel(IVecInt assumps) throws TimeoutException {
		throw new UnsupportedOperationException();
	}

	public int nConstraints() {
		return nbclauses;
	}

	public int nVars() {
		return maxvarid;

public class ReplayXplainStrategy implements XplainStrategy {

	private boolean computationCanceled;

	/**
	 * @since 2.1
	 */
	public void cancelExplanationComputation() {
		computationCanceled = true;
	}

	/**
	 * @since 2.1
	 */
	public IVecInt explain(ISolver solver, Map<Integer, IConstr> constrs,
			IVecInt assumps) throws TimeoutException {
		computationCanceled = false;
		IVecInt encodingAssumptions = new VecInt(constrs.size()
				+ assumps.size());
		List<Pair> pairs = new ArrayList<Pair>(constrs.size());
		IConstr constr;
		for (Map.Entry<Integer, IConstr> entry : constrs.entrySet()) {
			constr = entry.getValue();
			pairs.add(new Pair(entry.getKey(), constr));
		}
		Collections.sort(pairs);

		assumps.copyTo(encodingAssumptions);
		// for (Integer p : constrsIds) {
		// encodingAssumptions.push(p);
		// }
		for (Pair p : pairs) {
			encodingAssumptions.push(p.key);
		}

    }

    @Override
    public String decode(int[] model) {
        StringBuffer stb = new StringBuffer();
        for (int i = 0; i < model.length; i++) {
            stb.append(model[i]);
            stb.append(" ");
        }
        stb.append("0");
        return stb.toString();
    }

    @Override
    public void decode(int[] model, PrintWriter out) {
        for (int i = 0; i < model.length; i++) {
            out.print(model[i]);
            out.print(" ");
        }
        out.print("0");
    }

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

    @Override
    public String decode(int[] model) {
        StringBuffer stb = new StringBuffer();
        for (int i = 0; i < 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 < nbinputs; i++) {
            out.print(model[i]>0?1:0);
        }
    }

	}

	public void expireTimeout() {
		// TODO Auto-generated method stub

	}

	public boolean isSatisfiable(IVecInt assumps, boolean global)
			throws TimeoutException {
		throw new TimeoutException("There is no real solver behind!");
	}

	public boolean isSatisfiable(boolean global) throws TimeoutException {
		throw new TimeoutException("There is no real solver behind!");
	}

	public void printInfos(PrintWriter output, String prefix) {
	}

	public void setTimeoutOnConflicts(int count) {

	}

	public boolean isDBSimplificationAllowed() {
		return false;
	}

	public void setDBSimplificationAllowed(boolean status) {

	}

	/**
	 * @since 2.1
	 */
	public void setSearchListener(SearchListener sl) {
	}

	/**
	 * @since 2.1
	 */
	public int nextFreeVarId(boolean reserve) {

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(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(), solver);
		if (v == null)
			return null;
		if (v.size() == 2) {
			return OriginalBinaryClause.brandNewClause(solver, getVocabulary(),
					v);
		}
		return OriginalWLClause.brandNewClause(solver, getVocabulary(), v);