View Javadoc

1   package org.sat4j.pb.constraints;
2   
3   import java.math.BigInteger;
4   
5   import org.sat4j.core.Vec;
6   import org.sat4j.core.VecInt;
7   import org.sat4j.minisat.constraints.card.MinWatchCard;
8   import org.sat4j.minisat.constraints.cnf.LearntBinaryClause;
9   import org.sat4j.minisat.constraints.cnf.LearntHTClause;
10  import org.sat4j.minisat.constraints.cnf.OriginalBinaryClause;
11  import org.sat4j.minisat.constraints.cnf.OriginalHTClause;
12  import org.sat4j.minisat.constraints.cnf.UnitClause;
13  import org.sat4j.minisat.core.Constr;
14  import org.sat4j.pb.constraints.pb.IDataStructurePB;
15  import org.sat4j.specs.ContradictionException;
16  import org.sat4j.specs.IVec;
17  import org.sat4j.specs.IVecInt;
18  
19  public class CompetMinHTmixedClauseCardConstrDataStructureFactory extends
20  		PBMinClauseCardConstrDataStructure {
21  
22  	/**
23  	 * 
24  	 */
25  	private static final long serialVersionUID = 1L;
26  
27  	public CompetMinHTmixedClauseCardConstrDataStructureFactory() {
28  		// TODO Auto-generated constructor stub
29  	}
30  
31  	@Override
32  	protected Constr constructClause(IVecInt v) {
33  		if (v == null)
34  			return null;
35  		if (v.size() == 2) {
36  			return OriginalBinaryClause.brandNewClause(solver, getVocabulary(),
37  					v);
38  		}
39  		return OriginalHTClause.brandNewClause(solver, getVocabulary(), v);
40  	}
41  
42  	@Override
43  	protected Constr constructLearntClause(IVecInt resLits) {
44  		if (resLits.size() == 1) {
45  			return new UnitClause(resLits.last());
46  		}
47  		if (resLits.size() == 2) {
48  			return new LearntBinaryClause(resLits, getVocabulary());
49  		}
50  		return new LearntHTClause(resLits, getVocabulary());
51  	}
52  
53  	@Override
54  	protected Constr constructCard(IVecInt theLits, int degree)
55  			throws ContradictionException {
56  		return MinWatchCard.minWatchCardNew(solver, getVocabulary(), theLits,
57  				MinWatchCard.ATLEAST, degree);
58  	}
59  
60  	@Override
61  	protected Constr constructLearntCard(IDataStructurePB dspb) {
62  		IVecInt resLits = new VecInt();
63  		IVec<BigInteger> resCoefs = new Vec<BigInteger>();
64  		dspb.buildConstraintFromConflict(resLits, resCoefs);
65  		return new MinWatchCard(getVocabulary(), resLits, true, dspb
66  				.getDegree().intValue());
67  	}
68  
69  }