The following document contains the results of PMD's CPD 3.9.
| File | Line |
|---|---|
| org/sat4j/minisat/constraints/card/MaxWatchCard.java | 76 |
| org/sat4j/minisat/constraints/card/MinWatchCard.java | 84 |
public MinWatchCard(ILits voc, IVecInt ps, boolean moreThan, int degree) {
// On met en place les valeurs
this.voc = voc;
this.degree = degree;
this.moreThan = moreThan;
// On simplifie ps
int[] index = new int[voc.nVars() * 2 + 2];
for (int i = 0; i < index.length; i++)
index[i] = 0;
// On repertorie les litt?raux utiles
for (int i = 0; i < ps.size(); i++) {
if (index[ps.get(i) ^ 1] == 0) {
index[ps.get(i)]++;
} else {
index[ps.get(i) ^ 1]--;
}
}
// On supprime les litt?raux inutiles
int ind = 0;
while (ind < ps.size()) {
if (index[ps.get(ind)] > 0) {
index[ps.get(ind)]--;
ind++;
} else {
// ??
if ((ps.get(ind) & 1) != 0)
this.degree--;
ps.set(ind, ps.last());
ps.pop();
}
}
// On copie les litt?raux de la contrainte
lits = new int[ps.size()];
ps.moveTo(lits);
// On normalise la contrainte au sens de Barth
normalize(); | |
| File | Line |
|---|---|
| org/sat4j/tools/ExtendedDimacsArrayToDimacsConverter.java | 272 |
| org/sat4j/tools/GateTranslator.java | 264 |
private void iff2Clause(int[] f, int prefix, boolean negation)
throws ContradictionException {
if (prefix == f.length - 1) {
IVecInt clause = new VecInt(f.length);
for (int i = 0; i < f.length - 1; ++i) {
clause.push(f[i]);
}
clause.push(f[f.length - 1] * (negation ? -1 : 1));
processClause(clause);
return;
}
if (negation) {
iff2Clause(f, prefix + 1, false);
f[prefix] = -f[prefix];
iff2Clause(f, prefix + 1, true);
f[prefix] = -f[prefix];
} else {
f[prefix] = -f[prefix];
iff2Clause(f, prefix + 1, false);
f[prefix] = -f[prefix];
iff2Clause(f, prefix + 1, true);
}
}
} | |
| File | Line |
|---|---|
| org/sat4j/tools/ExtendedDimacsArrayToDimacsConverter.java | 245 |
| org/sat4j/tools/GateTranslator.java | 237 |
private void xor2Clause(int[] f, int prefix, boolean negation)
throws ContradictionException {
if (prefix == f.length - 1) {
IVecInt clause = new VecInt(f.length);
for (int i = 0; i < f.length - 1; ++i) {
clause.push(f[i]);
}
clause.push(f[f.length - 1] * (negation ? -1 : 1));
processClause(clause);
return;
}
if (negation) {
f[prefix] = -f[prefix];
xor2Clause(f, prefix + 1, false);
f[prefix] = -f[prefix];
xor2Clause(f, prefix + 1, true);
} else {
xor2Clause(f, prefix + 1, false);
f[prefix] = -f[prefix];
xor2Clause(f, prefix + 1, true);
f[prefix] = -f[prefix];
}
} | |
| File | Line |
|---|---|
| org/sat4j/minisat/orders/VarOrder.java | 197 |
| org/sat4j/minisat/orders/VarOrderHeap.java | 143 |
}
protected void updateActivity(final int var) {
if ((activity[var] += varInc) > VAR_RESCALE_BOUND) {
varRescaleActivity();
}
}
/**
*
*/
public void varDecayActivity() {
varInc *= varDecay;
}
/**
*
*/
private void varRescaleActivity() {
for (int i = 1; i < activity.length; i++) {
activity[i] *= VAR_RESCALE_FACTOR;
}
varInc *= VAR_RESCALE_FACTOR;
}
public double varActivity(int p) {
return activity[p >> 1];
}
/**
*
*/
public int numberOfInterestingVariables() {
int cpt = 0;
for (int i = 1; i < activity.length; i++) {
if (activity[i] > 1.0) {
cpt++;
}
}
return cpt;
}
/**
* that method has the responsability to initialize all arrays in the
* heuristics. PLEASE CALL super.init() IF YOU OVERRIDE THAT METHOD.
*/
public void init() {
int nlength = lits.nVars() + 1; | |
| File | Line |
|---|---|
| org/sat4j/minisat/constraints/pb/ConflictMapClause.java | 35 |
| org/sat4j/minisat/constraints/pb/ConflictMapMerging.java | 11 |
public ConflictMapMerging(Map<Integer, BigInteger> m, BigInteger d, ILits voc,
int level) {
super(m, d, voc, level);
}
public static IConflict createConflict(PBConstr cpb, int level) {
Map<Integer, BigInteger> m = new HashMap<Integer, BigInteger>();
int lit;
BigInteger coefLit;
for (int i = 0; i < cpb.size(); i++) {
lit = cpb.get(i);
coefLit = cpb.getCoef(i);
assert cpb.get(i) != 0;
assert cpb.getCoef(i).signum() > 0;
m.put(lit, coefLit);
}
return new ConflictMapMerging(m, cpb.getDegree(), cpb.getVocabulary(), | |
| File | Line |
|---|---|
| org/sat4j/tools/ExtendedDimacsArrayToDimacsConverter.java | 171 |
| org/sat4j/tools/GateTranslator.java | 121 |
public void and(int y, IVecInt literals) throws ContradictionException {
// y <=> AND x1 ... xn
// y <= x1 .. xn
IVecInt clause = new VecInt(literals.size() + 1);
clause.push(y);
for (int i = 0; i < literals.size(); i++) {
clause.push(-literals.get(i));
}
processClause(clause);
clause.clear();
for (int i = 0; i < literals.size(); i++) {
// y => xi
clause.clear();
clause.push(-y);
clause.push(literals.get(i));
processClause(clause);
}
} | |
| File | Line |
|---|---|
| org/sat4j/reader/DimacsReader.java | 263 |
| org/sat4j/reader/LecteurDimacs.java | 211 |
}
@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");
} | |
| File | Line |
|---|---|
| org/sat4j/reader/ExtendedDimacsReader.java | 44 |
| org/sat4j/tools/ExtendedDimacsArrayToDimacsConverter.java | 42 |
DimacsArrayToDimacsConverter {
public static final int FALSE = 1;
public static final int TRUE = 2;
public static final int NOT = 3;
public static final int AND = 4;
public static final int NAND = 5;
public static final int OR = 6;
public static final int NOR = 7;
public static final int XOR = 8;
public static final int XNOR = 9;
public static final int IMPLIES = 10;
public static final int IFF = 11;
public static final int IFTHENELSE = 12;
public static final int ATLEAST = 13;
public static final int ATMOST = 14;
public static final int COUNT = 15;
private static final long serialVersionUID = 1L;
public ExtendedDimacsArrayToDimacsConverter(int bufSize) { | |
| File | Line |
|---|---|
| org/sat4j/reader/ExtendedDimacsReader.java | 44 |
| org/sat4j/tools/ExtendedDimacsArrayReader.java | 41 |
public class ExtendedDimacsArrayReader extends DimacsArrayReader {
public static final int FALSE = 1;
public static final int TRUE = 2;
public static final int NOT = 3;
public static final int AND = 4;
public static final int NAND = 5;
public static final int OR = 6;
public static final int NOR = 7;
public static final int XOR = 8;
public static final int XNOR = 9;
public static final int IMPLIES = 10;
public static final int IFF = 11;
public static final int IFTHENELSE = 12;
public static final int ATLEAST = 13;
public static final int ATMOST = 14;
public static final int COUNT = 15;
private static final long serialVersionUID = 1L; | |
| File | Line |
|---|---|
| org/sat4j/reader/AAGReader.java | 50 |
| org/sat4j/reader/AIGReader.java | 48 |
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);
}
} | |
| File | Line |
|---|---|
| org/sat4j/tools/ExtendedDimacsArrayToDimacsConverter.java | 191 |
| org/sat4j/tools/GateTranslator.java | 171 |
public void or(int y, IVecInt literals) throws ContradictionException {
// y <=> OR x1 x2 ...xn
// y => x1 x2 ... xn
IVecInt clause = new VecInt(literals.size() + 1);
literals.copyTo(clause);
clause.push(-y);
processClause(clause);
clause.clear();
for (int i = 0; i < literals.size(); i++) {
// xi => y
clause.clear();
clause.push(y);
clause.push(-literals.get(i));
processClause(clause);
}
}
private void processClause(IVecInt clause) throws ContradictionException { | |
