}

	@Override
	protected Constr constructClause(IVecInt v) {
		if (v == null)
			return null;
		if (v.size() == 2) {
			return OriginalBinaryClause.brandNewClause(solver, getVocabulary(),
					v);
		}
		return OriginalHTClause.brandNewClause(solver, getVocabulary(), v);
	}

	@Override
	protected Constr constructLearntClause(IVecInt resLits) {
		if (resLits.size() == 1) {
			return new UnitClause(resLits.last());
		}
		if (resLits.size() == 2) {
			return new LearntBinaryClause(resLits, getVocabulary());
		}
		return new LearntHTClause(resLits, getVocabulary());
	}

	@Override
	protected Constr constructCard(IVecInt theLits, int degree)
			throws ContradictionException {
		return MinWatchCard.minWatchCardNew(solver, getVocabulary(), theLits,
				MinWatchCard.ATLEAST, degree);
	}

	@Override
	protected Constr constructLearntCard(IDataStructurePB dspb) {
		IVecInt resLits = new VecInt();
		IVec<BigInteger> resCoefs = new Vec<BigInteger>();
		dspb.buildConstraintFromConflict(resLits, resCoefs);
		return new MinWatchCard(getVocabulary(), resLits, true, dspb
				.getDegree().intValue());
	}

}

		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")) {

		return new LearntWLClause(resLits, getVocabulary());
	}

	@Override
	protected Constr constructCard(IVecInt theLits, int degree)
			throws ContradictionException {
		return MinWatchCard.minWatchCardNew(solver, getVocabulary(), theLits,
				MinWatchCard.ATLEAST, degree);
	}

	@Override
	protected Constr constructLearntCard(IDataStructurePB dspb) {
		IVecInt resLits = new VecInt();
		IVec<BigInteger> resCoefs = new Vec<BigInteger>();
		dspb.buildConstraintFromConflict(resLits, resCoefs);
		return new MinWatchCard(getVocabulary(), resLits, true, dspb
				.getDegree().intValue());
	}

}

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

		PuebloPBMinClauseCardConstrDataStructure {

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

	@Override
	protected PBConstr constructCard(IVecInt theLits, int degree)
			throws ContradictionException {
		return AtLeastPB.atLeastNew(solver, getVocabulary(), theLits, degree);
	}

	@Override
	protected Constr constructLearntCard(IDataStructurePB dspb) {
		IVecInt resLits = new VecInt();
		IVec<BigInteger> resCoefs = new Vec<BigInteger>();
		dspb.buildConstraintFromConflict(resLits, resCoefs);
		return AtLeastPB.atLeastNew(getVocabulary(), resLits, dspb.getDegree()
				.intValue());
	}

}