1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25 package org.sat4j.minisat.constraints;
26
27 import java.math.BigInteger;
28
29 import org.sat4j.minisat.constraints.pb.IDataStructurePB;
30 import org.sat4j.minisat.constraints.pb.MinWatchCardPB;
31 import org.sat4j.minisat.constraints.pb.MinWatchPb;
32 import org.sat4j.minisat.constraints.pb.PBConstr;
33 import org.sat4j.minisat.constraints.pb.PuebloMinWatchPb;
34 import org.sat4j.minisat.constraints.pb.WLClausePB;
35 import org.sat4j.specs.ContradictionException;
36 import org.sat4j.specs.IVec;
37 import org.sat4j.specs.IVecInt;
38
39 public class PuebloPBMinClauseCardConstrDataStructure extends
40 AbstractPBClauseCardConstrDataStructure {
41
42
43
44
45 private static final long serialVersionUID = 1L;
46
47 @Override
48 protected PBConstr constructClause(IVecInt v) {
49 return WLClausePB.brandNewClause(solver, getVocabulary(), v);
50 }
51
52 @Override
53 protected PBConstr constructCard(IVecInt lits, int degree)
54 throws ContradictionException {
55 return MinWatchCardPB.normalizedMinWatchCardPBNew(solver,
56 getVocabulary(), lits, degree);
57 }
58
59 @Override
60 protected PBConstr constructPB(IDataStructurePB mpb)
61 throws ContradictionException {
62 return MinWatchPb.normalizedMinWatchPbNew(solver, getVocabulary(), mpb);
63 }
64
65 @Override
66 protected PBConstr constructPB(int[] lits, BigInteger[] coefs, BigInteger degree)
67 throws ContradictionException {
68 return MinWatchPb.normalizedMinWatchPbNew(solver, getVocabulary(), lits, coefs, degree);
69 }
70
71 @Override
72 protected PBConstr constructLearntClause(IVecInt literals) {
73 return new WLClausePB(literals, getVocabulary());
74 }
75
76 @Override
77 protected PBConstr constructLearntCard(IVecInt literals, int degree) {
78 return new MinWatchCardPB(getVocabulary(), literals, true, degree);
79 }
80
81 @Override
82 protected PBConstr constructLearntPB(IVecInt literals,
83 IVec<BigInteger> coefs, BigInteger degree) {
84 return PuebloMinWatchPb.watchPbNew(getVocabulary(), literals, coefs,
85 true, degree);
86 }
87
88 }