}

	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());
		assumps.copyTo(encodingAssumptions);
		IVecInt firstExplanation = solver.unsatExplanation();
		Set<Integer> constraintsVariables = constrs.keySet();
		int p;
		for (int i = 0; i < firstExplanation.size(); i++) {
			if (constraintsVariables.contains(p = -firstExplanation.get(i))) {
				encodingAssumptions.push(p);
			}
		}

	}

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

	}

	public void backtracking(int p) {
		// TODO Auto-generated method stub

	}

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

	}

	public void conflictFound(IConstr confl, int dlevel, int trailLevel) {
		// TODO Auto-generated method stub

	}

	public void conflictFound(int p) {
		// TODO Auto-generated method stub

	}

	public void delete(int[] clause) {
		// TODO Auto-generated method stub

	}

	public void end(Lbool result) {
		out.close();

	}

	public void learn(IConstr c) {
		// TODO Auto-generated method stub

	}

	public void propagating(int p, IConstr reason) {
		// TODO Auto-generated method stub

	}

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

	}

	public void start() {

	}

	public void restarting() {
		// out.close();
		// restartNumber++;
		// updateWriter();
	}

	public void backjump(int backjumpLevel) {

    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 LearnedClauseSizeTracing(String filename) {
		this.filename = filename;
		updateWriter();
	}

	private void updateWriter() {
		try {
			out = new PrintStream(new FileOutputStream(filename + ".dat"));
		} catch (FileNotFoundException e) {
			out = System.out;
		}
	}

	public void adding(int p) {
		// TODO Auto-generated method stub

	}

	public void assuming(int p) {

	}

	public void backtracking(int p) {
		// TODO Auto-generated method stub

	}

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

	}

	public void conflictFound(IConstr confl, int dlevel, int trailLevel) {
		out.println(confl.size());

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