Commit 324ec34e authored by Daniel Le Berre's avatar Daniel Le Berre
Browse files

fixed more sonarqube violatons in sat4j core

parent 86c4b46d
Pipeline #20103 passed with stages
in 54 minutes and 22 seconds
......@@ -31,7 +31,6 @@
package org.sat4j.tools.counting;
import java.math.BigInteger;
import java.util.Comparator;
import org.sat4j.core.Vec;
import org.sat4j.specs.ISolver;
......@@ -165,8 +164,8 @@ public abstract class AbstractApproxMC implements IModelCounter {
// Computing the number of models for t random formulas.
int iterCount = computeIterCount();
IVec<BigInteger> counts = new Vec<BigInteger>(iterCount);
for (int i = 0; i < iterCount; i++) {
IVec<BigInteger> counts = new Vec<>(iterCount);
for (var i = 0; i < iterCount; i++) {
BigInteger count = internalCountModels(threshold);
if (count != null) {
counts.push(count);
......@@ -253,12 +252,7 @@ public abstract class AbstractApproxMC implements IModelCounter {
}
// The values need to be sorted to find the median...
values.sort(new Comparator<BigInteger>() {
@Override
public int compare(BigInteger o1, BigInteger o2) {
return o1.compareTo(o2);
}
});
values.sort(BigInteger::compareTo);
// ... which is at the middle-th position of the vector.
return values.get(values.size() >> 1);
......
......@@ -153,7 +153,7 @@ public class ApproxMC2 extends AbstractApproxMC {
// Computing the number of models with the optimal set of constraints.
int nConstr = logSatSearch(thresh, nConstrPrev);
BigInteger nSols = BigInteger.valueOf(boundedSAT(nConstr, thresh));
var nSols = BigInteger.valueOf(boundedSAT(nConstr, thresh));
// Forgetting all parity constraints used in this run.
generator.clear();
......@@ -174,10 +174,10 @@ public class ApproxMC2 extends AbstractApproxMC {
* @return The best number of parity constraints to add.
*/
private int logSatSearch(int thresh, int nConstrPrev) {
int loIndex = 0;
var loIndex = 0;
int hiIndex = samplingSet.nVars() - 1;
int nConstr = nConstrPrev;
int[] cells = new int[samplingSet.nVars()];
var cells = new int[samplingSet.nVars()];
Arrays.fill(cells, -1);
cells[0] = 1;
cells[samplingSet.nVars() - 1] = 0;
......
......@@ -88,7 +88,7 @@ public final class ModelCounterAdapter implements IModelCounter {
* @return The created model counter.
*/
public static ModelCounterAdapter newInstance(ISolver solver, long bound) {
ModelCounterAdapter counter = new ModelCounterAdapter(solver);
var counter = new ModelCounterAdapter(solver);
counter.setBound(bound);
return counter;
}
......
......@@ -108,13 +108,13 @@ public class ParityConstraintGenerator {
* The number of constraints to generate.
*/
public void generate(int nb) {
for (int i = 0; i < nb; i++) {
for (var i = 0; i < nb; i++) {
// Looking for the variables to put in the constraint.
IVecInt lits = new VecInt();
for (IteratorInt it = samplingSet.variables(); it.hasNext();) {
int var = it.next();
var variable = it.next();
if (RANDOM.nextBoolean()) {
lits.push(var);
lits.push(variable);
}
}
......@@ -158,7 +158,7 @@ public class ParityConstraintGenerator {
*/
public void deactivate(int nb) {
// Deactivating the constraints.
for (int i = 0; i < nb; i++) {
for (var i = 0; i < nb; i++) {
getConstraint(i).deactivate();
}
activated = false;
......@@ -181,7 +181,7 @@ public class ParityConstraintGenerator {
* The number of constraints to activate
*/
public void activate(int nb) {
for (int i = 0; i < nb; i++) {
for (var i = 0; i < nb; i++) {
getConstraint(i).activate();
}
activated = true;
......
......@@ -69,31 +69,31 @@ public class Binary extends EncodingStrategyAdapter {
@Override
public IConstr addAtMostOne(ISolver solver, IVecInt literals)
throws ContradictionException {
ConstrGroup group = new ConstrGroup(false);
var group = new ConstrGroup(false);
final int n = literals.size();
final int p = (int) Math.ceil(Math.log(n) / Math.log(2));
final int k = (int) Math.pow(2, p) - n;
IVecInt clause = new VecInt();
String binary = "";
var binary = "";
if (p == 0) {
return group;
}
int y[] = new int[p];
for (int i = 0; i < p; i++) {
var y = new int[p];
for (var i = 0; i < p; i++) {
y[i] = solver.nextFreeVarId(true);
}
for (int i = 0; i < k; i++) {
for (var i = 0; i < k; i++) {
binary = Integer.toBinaryString(i);
while (binary.length() != p - 1) {
binary = "0" + binary;
}
for (int j = 0; j < p - 1; j++) {
for (var j = 0; j < p - 1; j++) {
clause.push(-literals.get(i));
if (binary.charAt(j) == '0') {
clause.push(-y[j]);
......@@ -106,12 +106,12 @@ public class Binary extends EncodingStrategyAdapter {
}
}
for (int i = k; i < n; i++) {
for (var i = k; i < n; i++) {
binary = Integer.toBinaryString(2 * k + i - k);
while (binary.length() != p) {
binary = "0" + binary;
}
for (int j = 0; j < p; j++) {
for (var j = 0; j < p; j++) {
clause.push(-literals.get(i));
if (binary.charAt(j) == '0') {
clause.push(-y[j]);
......@@ -134,20 +134,20 @@ public class Binary extends EncodingStrategyAdapter {
final int n = literals.size();
final int p = (int) Math.ceil(Math.log(n) / Math.log(2));
ConstrGroup group = new ConstrGroup(false);
var group = new ConstrGroup(false);
int[][] b = new int[k][p];
var b = new int[k][p];
for (int i = 0; i < k; i++) {
for (int j = 0; j < p; j++) {
for (var i = 0; i < k; i++) {
for (var j = 0; j < p; j++) {
b[i][j] = solver.nextFreeVarId(true);
}
}
int[][] t = new int[k][n];
var t = new int[k][n];
for (int i = 0; i < k; i++) {
for (int j = 0; j < n; j++) {
for (var i = 0; i < k; i++) {
for (var j = 0; j < n; j++) {
t[i][j] = solver.nextFreeVarId(true);
}
}
......@@ -155,8 +155,8 @@ public class Binary extends EncodingStrategyAdapter {
int max, min;
IVecInt clause1 = new VecInt();
IVecInt clause2 = new VecInt();
String binary = "";
for (int i = 0; i < n; i++) {
var binary = "";
for (var i = 0; i < n; i++) {
max = Math.max(1, k - n + i + 1);
min = Math.min(i + 1, k);
clause1.push(-literals.get(i));
......@@ -168,7 +168,7 @@ public class Binary extends EncodingStrategyAdapter {
for (int g = max - 1; g < min; g++) {
clause1.push(t[g][i]);
for (int j = 0; j < p; j++) {
for (var j = 0; j < p; j++) {
clause2.push(-t[g][i]);
if (binary.charAt(j) == '0') {
clause2.push(-b[g][j]);
......@@ -189,7 +189,7 @@ public class Binary extends EncodingStrategyAdapter {
@Override
public IConstr addExactlyOne(ISolver solver, IVecInt literals)
throws ContradictionException {
ConstrGroup group = new ConstrGroup(false);
var group = new ConstrGroup(false);
group.add(addAtLeastOne(solver, literals));
group.add(addAtMostOne(solver, literals));
......@@ -200,7 +200,7 @@ public class Binary extends EncodingStrategyAdapter {
@Override
public IConstr addExactly(ISolver solver, IVecInt literals, int degree)
throws ContradictionException {
ConstrGroup group = new ConstrGroup(false);
var group = new ConstrGroup(false);
group.add(addAtLeast(solver, literals, degree));
group.add(addAtMost(solver, literals, degree));
......
......@@ -60,7 +60,7 @@ public class Binomial extends EncodingStrategyAdapter {
@Override
public IConstr addAtMost(ISolver solver, IVecInt literals, int degree)
throws ContradictionException {
ConstrGroup group = new ConstrGroup(false);
var group = new ConstrGroup(false);
IVecInt clause = new VecInt();
......@@ -69,7 +69,7 @@ public class Binomial extends EncodingStrategyAdapter {
}
for (IVecInt vec : literals.subset(degree + 1)) {
for (int i = 0; i < vec.size(); i++) {
for (var i = 0; i < vec.size(); i++) {
clause.push(-vec.get(i));
}
group.add(solver.addClause(clause));
......@@ -82,11 +82,11 @@ public class Binomial extends EncodingStrategyAdapter {
@Override
public IConstr addAtMostOne(ISolver solver, IVecInt literals)
throws ContradictionException {
ConstrGroup group = new ConstrGroup(false);
var group = new ConstrGroup(false);
IVecInt clause = new VecInt();
for (int i = 0; i < literals.size() - 1; i++) {
for (var i = 0; i < literals.size() - 1; i++) {
for (int j = i + 1; j < literals.size(); j++) {
clause.push(-literals.get(i));
clause.push(-literals.get(j));
......@@ -100,7 +100,7 @@ public class Binomial extends EncodingStrategyAdapter {
@Override
public IConstr addExactlyOne(ISolver solver, IVecInt literals)
throws ContradictionException {
ConstrGroup group = new ConstrGroup(false);
var group = new ConstrGroup(false);
group.add(addAtLeastOne(solver, literals));
group.add(addAtMostOne(solver, literals));
......@@ -111,7 +111,7 @@ public class Binomial extends EncodingStrategyAdapter {
@Override
public IConstr addExactly(ISolver solver, IVecInt literals, int degree)
throws ContradictionException {
ConstrGroup group = new ConstrGroup(false);
var group = new ConstrGroup(false);
group.add(addAtLeast(solver, literals, degree));
group.add(addAtMost(solver, literals, degree));
......
......@@ -40,9 +40,9 @@ import org.sat4j.specs.IVecInt;
/**
* Commander encoding for "at most one" and "at most k" cases.
*
* The case "at most one" is introduced in W. Klieber and G. Kwon
* "Efficient CNF encoding for selecting 1 from N objects" in Fourth Workshop on
* Constraints in Formal Verification, 2007.
* The case "at most one" is introduced in W. Klieber and G. Kwon "Efficient CNF
* encoding for selecting 1 from N objects" in Fourth Workshop on Constraints in
* Formal Verification, 2007.
*
* The generalization to the "at most k" case is described in A. M. Frisch and P
* . A. Giannaros, "SAT Encodings of the At-Most-k Constraint", in International
......@@ -71,21 +71,21 @@ public class Commander extends EncodingStrategyAdapter {
return addAtMostOne(solver, literals, 3);
}
private IConstr addAtMostOne(ISolver solver, IVecInt literals, int groupSize)
throws ContradictionException {
private IConstr addAtMostOne(ISolver solver, IVecInt literals,
int groupSize) throws ContradictionException {
ConstrGroup constrGroup = new ConstrGroup(false);
var constrGroup = new ConstrGroup(false);
IVecInt clause = new VecInt();
IVecInt clause1 = new VecInt();
final int n = literals.size();
int nbGroup = (int) Math.ceil((double) literals.size()
/ (double) groupSize);
int nbGroup = (int) Math
.ceil((double) literals.size() / (double) groupSize);
if (nbGroup == 1) {
for (int i = 0; i < literals.size() - 1; i++) {
for (var i = 0; i < literals.size() - 1; i++) {
for (int j = i + 1; j < literals.size(); j++) {
clause.push(-literals.get(i));
clause.push(-literals.get(j));
......@@ -96,24 +96,24 @@ public class Commander extends EncodingStrategyAdapter {
return constrGroup;
}
int[] c = new int[nbGroup];
var c = new int[nbGroup];
for (int i = 0; i < nbGroup; i++) {
for (var i = 0; i < nbGroup; i++) {
c[i] = solver.nextFreeVarId(true);
}
int nbVarLastGroup = n - (nbGroup - 1) * groupSize;
// Encoding <=1 for each group of groupLitterals
for (int i = 0; i < nbGroup; i++) {
int size = 0;
for (var i = 0; i < nbGroup; i++) {
var size = 0;
if (i == nbGroup - 1) {
size = nbVarLastGroup;
} else {
size = groupSize;
}
// Encoding <=1 for each group of groupLitterals
for (int j = 0; j < size - 1; j++) {
for (var j = 0; j < size - 1; j++) {
for (int k = j + 1; k < size; k++) {
clause.push(-literals.get(i * groupSize + j));
clause.push(-literals.get(i * groupSize + k));
......@@ -127,7 +127,7 @@ public class Commander extends EncodingStrategyAdapter {
// If a commander variable is false then no variable in its group
// can be true (clause)
clause1.push(-c[i]);
for (int j = 0; j < size; j++) {
for (var j = 0; j < size; j++) {
clause1.push(literals.get(i * groupSize + j));
clause.push(c[i]);
clause.push(-literals.get(i * groupSize + j));
......@@ -147,7 +147,7 @@ public class Commander extends EncodingStrategyAdapter {
@Override
public IConstr addExactlyOne(ISolver solver, IVecInt literals)
throws ContradictionException {
ConstrGroup group = new ConstrGroup(false);
var group = new ConstrGroup(false);
group.add(addAtLeastOne(solver, literals));
group.add(addAtMostOne(solver, literals));
......@@ -158,7 +158,7 @@ public class Commander extends EncodingStrategyAdapter {
@Override
public IConstr addExactly(ISolver solver, IVecInt literals, int degree)
throws ContradictionException {
ConstrGroup group = new ConstrGroup(false);
var group = new ConstrGroup(false);
group.add(addAtLeast(solver, literals, degree));
group.add(addAtMost(solver, literals, degree));
......
......@@ -56,7 +56,7 @@ public abstract class EncodingStrategyAdapter implements Serializable {
throws ContradictionException {
final int n = literals.size();
IVecInt newLiterals = new VecInt(n);
for (int i = 0; i < n; i++) {
for (var i = 0; i < n; i++) {
newLiterals.push(-literals.get(i));
}
return this.addAtMost(solver, newLiterals, n - degree);
......
......@@ -41,9 +41,9 @@ import org.sat4j.specs.IVecInt;
*
* Ladder encoding for the "at most one" and "exactly one" cases.
*
* The ladder encoding described in: I. P. Gent and P. Nightingale,
* "A new encoding for AllDifferent into SAT", in International Workshop on
* Modeling and Reformulating Constraint Satisfaction Problems, 2004
* The ladder encoding described in: I. P. Gent and P. Nightingale, "A new
* encoding for AllDifferent into SAT", in International Workshop on Modeling
* and Reformulating Constraint Satisfaction Problems, 2004
*
* @author sroussel
* @since 2.3.1
......@@ -57,26 +57,25 @@ public class Ladder extends EncodingStrategyAdapter {
@Override
/**
* If n is the number of variables in the constraint,
* this encoding adds n variables and 4n clauses
* (3n+1 size 2 clauses and n-1 size 3 clauses)
* If n is the number of variables in the constraint, this encoding adds n
* variables and 4n clauses (3n+1 size 2 clauses and n-1 size 3 clauses)
*/
public IConstr addAtMostOne(ISolver solver, IVecInt literals)
throws ContradictionException {
ConstrGroup group = new ConstrGroup(false);
var group = new ConstrGroup(false);
final int n = literals.size() + 1;
int xN = solver.nextFreeVarId(true);
int y[] = new int[n - 1];
var y = new int[n - 1];
for (int i = 0; i < n - 1; i++) {
for (var i = 0; i < n - 1; i++) {
y[i] = solver.nextFreeVarId(true);
}
IVecInt clause = new VecInt();
// Constraint \bigwedge_{i=1}{n-2} (\neg y_{i+1} \vee y_i)
for (int i = 1; i <= n - 2; i++) {
for (var i = 1; i <= n - 2; i++) {
clause.push(-y[i]);
clause.push(y[i - 1]);
group.add(solver.addClause(clause));
......@@ -84,7 +83,7 @@ public class Ladder extends EncodingStrategyAdapter {
}
// Constraint \bigwedge_{i=2}{n-1} (\neg y_{i-1} \vee y_i \vee x_i)
for (int i = 2; i <= n - 1; i++) {
for (var i = 2; i <= n - 1; i++) {
clause.push(-y[i - 2]);
clause.push(y[i - 1]);
clause.push(literals.get(i - 1));
......@@ -93,7 +92,7 @@ public class Ladder extends EncodingStrategyAdapter {
}
// Constraint \bigwedge_{i=2}{n-1} (\neg x_i \vee y_{i-1)})
for (int i = 2; i <= n - 1; i++) {
for (var i = 2; i <= n - 1; i++) {
clause.push(-literals.get(i - 1));
clause.push(y[i - 2]);
group.add(solver.addClause(clause));
......@@ -101,7 +100,7 @@ public class Ladder extends EncodingStrategyAdapter {
}
// Constraint \bigwedge_{i=2}{n-1} (\neg x_i \vee \neg y_i)
for (int i = 2; i <= n - 1; i++) {
for (var i = 2; i <= n - 1; i++) {
clause.push(-literals.get(i - 1));
clause.push(-y[i - 1]);
group.add(solver.addClause(clause));
......@@ -137,13 +136,12 @@ public class Ladder extends EncodingStrategyAdapter {
@Override
/**
* If n is the number of variables in the constraint,
* this encoding adds n-1 variables and 4(n-1) clauses
* (3n-2 size 2 clauses and n-2 size 3 clauses)
* If n is the number of variables in the constraint, this encoding adds n-1
* variables and 4(n-1) clauses (3n-2 size 2 clauses and n-2 size 3 clauses)
*/
public IConstr addExactlyOne(ISolver solver, IVecInt literals)
throws ContradictionException {
ConstrGroup group = new ConstrGroup(false);
var group = new ConstrGroup(false);
final int n = literals.size();
IVecInt clause = new VecInt();
......@@ -154,14 +152,14 @@ public class Ladder extends EncodingStrategyAdapter {
return group;
}
int y[] = new int[n - 1];
var y = new int[n - 1];
for (int i = 0; i < n - 1; i++) {
for (var i = 0; i < n - 1; i++) {
y[i] = solver.nextFreeVarId(true);
}
// Constraint \bigwedge_{i=1}{n-2} (\neg y_{i+1} \vee y_i)
for (int i = 1; i <= n - 2; i++) {
for (var i = 1; i <= n - 2; i++) {
clause.push(-y[i]);
clause.push(y[i - 1]);
group.add(solver.addClause(clause));
......@@ -169,7 +167,7 @@ public class Ladder extends EncodingStrategyAdapter {
}
// Constraint \bigwedge_{i=2}{n-1} (\neg y_{i-1} \vee y_i \vee x_i)
for (int i = 2; i <= n - 1; i++) {
for (var i = 2; i <= n - 1; i++) {
clause.push(-y[i - 2]);
clause.push(y[i - 1]);
clause.push(literals.get(i - 1));
......@@ -178,7 +176,7 @@ public class Ladder extends EncodingStrategyAdapter {
}
// Constraint \bigwedge_{i=2}{n-1} (\neg x_i \vee y_{i-1)})
for (int i = 2; i <= n - 1; i++) {
for (var i = 2; i <= n - 1; i++) {
clause.push(-literals.get(i - 1));
clause.push(y[i - 2]);
group.add(solver.addClause(clause));
......@@ -186,7 +184,7 @@ public class Ladder extends EncodingStrategyAdapter {
}
// Constraint \bigwedge_{i=2}{n-1} (\neg x_i \vee \neg y_i)
for (int i = 2; i <= n - 1; i++) {
for (var i = 2; i <= n - 1; i++) {
clause.push(-literals.get(i - 1));
clause.push(-y[i - 1]);
group.add(solver.addClause(clause));
......
......@@ -108,7 +108,8 @@ public class Policy extends EncodingStrategyAdapter {
return this.atMostOneEncoding;
}
public void setAtMostOneEncoding(EncodingStrategyAdapter atMostOneEncoding) {
public void setAtMostOneEncoding(
EncodingStrategyAdapter atMostOneEncoding) {
this.atMostOneEncoding = atMostOneEncoding;
}
......@@ -132,12 +133,14 @@ public class Policy extends EncodingStrategyAdapter {
return this.exactlyOneEncoding;
}
public void setExactlyOneEncoding(EncodingStrategyAdapter exactlyOneEncoding) {
public void setExactlyOneEncoding(
EncodingStrategyAdapter exactlyOneEncoding) {
this.exactlyOneEncoding = exactlyOneEncoding;
}
public void setExactlyOneEncoding(EncodingStrategy exactlyOneEncoding) {
this.exactlyOneEncoding = getAdapterFromEncodingName(exactlyOneEncoding);
this.exactlyOneEncoding = getAdapterFromEncodingName(
exactlyOneEncoding);
}
public EncodingStrategyAdapter getExactlyKEncoding() {
......@@ -156,12 +159,14 @@ public class Policy extends EncodingStrategyAdapter {
return this.atLeastOneEncoding;
}
public void setAtLeastOneEncoding(EncodingStrategyAdapter atLeastOneEncoding) {
public void setAtLeastOneEncoding(
EncodingStrategyAdapter atLeastOneEncoding) {
this.atLeastOneEncoding = atLeastOneEncoding;
}
public void setAtLeastOneEncoding(EncodingStrategy atLeastOneEncoding) {
this.atLeastOneEncoding = getAdapterFromEncodingName(atLeastOneEncoding);
this.atLeastOneEncoding = getAdapterFromEncodingName(
atLeastOneEncoding);
}
public EncodingStrategyAdapter getAtLeastKEncoding() {
......@@ -234,17 +239,19 @@ public class Policy extends EncodingStrategyAdapter {
@Override
public String toString() {
String s = "";
s += "Policy = [At most K: "
+ getEncodingTypeFromAdapter(getAtMostKEncoding())
+ ", at most 1: "
+ getEncodingTypeFromAdapter(getAtMostOneEncoding())
+ ", exactly K: "
+ getEncodingTypeFromAdapter(getExactlyKEncoding())
+ ", exactly 1: "
+ getEncodingTypeFromAdapter(getExactlyOneEncoding()) + "]";
return s;
var stb = new StringBuilder();
stb.append("Policy = [At most K: ");
stb.append(getEncodingTypeFromAdapter(getAtMostKEncoding()));
stb.append(", at most 1: ");
stb.append(getEncodingTypeFromAdapter(getAtMostOneEncoding()));