Commit 86c4b46d authored by Daniel Le Berre's avatar Daniel Le Berre
Browse files

fixed more sonarqube violatons (sat4j core done)

parent ddc8fdbc
Pipeline #20102 passed with stages
in 49 minutes and 26 seconds
......@@ -70,7 +70,6 @@ final class AgeLCDS implements LearnedConstraintsDeletionStrategy {
solver.out.log(solver.getLogPrefix() + "cleaning " //$NON-NLS-1$
+ (solver.learnts.size() - j) + " clauses out of " //$NON-NLS-1$
+ solver.learnts.size());
// out.flush();
}
solver.learnts.shrinkTo(j);
}
......
......@@ -29,6 +29,8 @@
*******************************************************************************/
package org.sat4j.minisat.core;
import java.io.Serializable;
/**
* Conflict based timer.
*
......@@ -37,7 +39,7 @@ package org.sat4j.minisat.core;
* @author daniel
*
*/
public interface ConflictTimer {
public interface ConflictTimer extends Serializable {
void reset();
......
......@@ -29,20 +29,17 @@
*******************************************************************************/
package org.sat4j.minisat.core;
import java.io.Serializable;
/**
* Perform a task when a given number of conflicts is reached.
*
* @author daniel
*
*/
public abstract class ConflictTimerAdapter implements Serializable,
ConflictTimer {
public abstract class ConflictTimerAdapter implements ConflictTimer {
/**
*
*/
*
*/
private static final long serialVersionUID = 1L;
private int counter;
......@@ -51,8 +48,9 @@ public abstract class ConflictTimerAdapter implements Serializable,
private final Solver<? extends DataStructureFactory> solver;
public ConflictTimerAdapter(
final Solver<? extends DataStructureFactory> solver, final int bound) {
protected ConflictTimerAdapter(
final Solver<? extends DataStructureFactory> solver,
final int bound) {
this.bound = bound;
this.counter = 0;
this.solver = solver;
......
......@@ -29,8 +29,6 @@
*******************************************************************************/
package org.sat4j.minisat.core;
import java.io.Serializable;
import org.sat4j.core.Vec;
import org.sat4j.specs.IVec;
......@@ -40,14 +38,14 @@ import org.sat4j.specs.IVec;
* @author daniel
*
*/
public class ConflictTimerContainer implements Serializable, ConflictTimer {
public class ConflictTimerContainer implements ConflictTimer {
/**
*
*/
*
*/
private static final long serialVersionUID = 1L;
private final IVec<ConflictTimer> timers = new Vec<ConflictTimer>();
private final IVec<ConflictTimer> timers = new Vec<>();
ConflictTimerContainer add(ConflictTimer timer) {
this.timers.push(timer);
......@@ -60,13 +58,13 @@ public class ConflictTimerContainer implements Serializable, ConflictTimer {
}
public void reset() {
for (int i = 0; i < this.timers.size(); i++) {
for (var i = 0; i < this.timers.size(); i++) {
this.timers.get(i).reset();
}
}
public void newConflict() {
for (int i = 0; i < this.timers.size(); i++) {
for (var i = 0; i < this.timers.size(); i++) {
this.timers.get(i).newConflict();
}
}
......
......@@ -145,7 +145,7 @@ public class QuadraticPrimeImplicantStrategy implements PrimeImplicantStrategy {
}
}
solver.cancelUntil(0);
int[] implicant = new int[prime.length - removed - 1];
var implicant = new int[prime.length - removed - 1];
int index = 0;
for (int i : prime) {
if (i != 0) {
......
......@@ -33,12 +33,12 @@ import static org.sat4j.core.LiteralsUtils.negLit;
import org.sat4j.minisat.core.IPhaseSelectionStrategy;
abstract class AbstractPhaserecordingSelectionStrategy implements
IPhaseSelectionStrategy {
abstract class AbstractPhaserecordingSelectionStrategy
implements IPhaseSelectionStrategy {
/**
*
*/
*
*/
private static final long serialVersionUID = 1L;
protected int[] phase;
......@@ -47,16 +47,16 @@ abstract class AbstractPhaserecordingSelectionStrategy implements
if (this.phase == null || this.phase.length < nlength) {
this.phase = new int[nlength];
}
for (int i = 1; i < nlength; i++) {
for (var i = 1; i < nlength; i++) {
this.phase[i] = negLit(i);
}
}
public void init(int var, int p) {
this.phase[var] = p;
public void init(int variable, int p) {
this.phase[variable] = p;
}
public int select(int var) {
return this.phase[var];
public int select(int variable) {
return this.phase[variable];
}
}
......@@ -55,7 +55,7 @@ public class LevelBasedVarOrderHeap extends VarOrderHeap {
private int[] level;
private final List<IVecInt> varsByLevel = new ArrayList<IVecInt>();
private final List<IVecInt> varsByLevel = new ArrayList<>();
public LevelBasedVarOrderHeap() {
}
......@@ -89,14 +89,14 @@ public class LevelBasedVarOrderHeap extends VarOrderHeap {
int nlength = this.lits.nVars() + 1;
if (level == null || level.length < nlength) {
this.level = new int[nlength];
for (int i = 0; i < nlength; i++) {
for (var i = 0; i < nlength; i++) {
level[i] = Integer.MAX_VALUE;
}
}
IVecInt currentLevel;
for (int i = 1; i <= varsByLevel.size(); i++) {
for (var i = 1; i <= varsByLevel.size(); i++) {
currentLevel = varsByLevel.get(i - 1);
for (int j = 0; j < currentLevel.size(); j++) {
for (var j = 0; j < currentLevel.size(); j++) {
level[currentLevel.get(j)] = i;
}
}
......
......@@ -49,11 +49,11 @@ public final class NegativeLiteralSelectionStrategy
public void init(int nlength) {
}
public void init(int var, int p) {
public void init(int variable, int p) {
}
public int select(int var) {
return negLit(var);
public int select(int variable) {
return negLit(variable);
}
public void updateVar(int p) {
......
......@@ -46,7 +46,7 @@ public class OrientedOrder implements IOrder {
@Override
public int select() {
int p;
for (int i = 0; i < orderedLits.size(); i++) {
for (var i = 0; i < orderedLits.size(); i++) {
p = orderedLits.get(i);
if (voc.isUnassigned(p)) {
return p;
......@@ -78,7 +78,7 @@ public class OrientedOrder implements IOrder {
public void init() {
order.init();
managed = new boolean[voc.nVars() + 1];
try (Scanner in = new Scanner(
try (var in = new Scanner(
new BufferedReader(new FileReader(fileName)))) {
while (in.hasNext()) {
append(in.nextInt());
......@@ -89,7 +89,7 @@ public class OrientedOrder implements IOrder {
}
private void append(int l) {
int p = LiteralsUtils.toInternal(l);
var p = LiteralsUtils.toInternal(l);
orderedLits.push(p);
managed[p >> 1] = true;
}
......
......@@ -50,7 +50,8 @@ public final class ArminRestarts implements RestartStrategy {
*/
private static final long serialVersionUID = 1L;
private double inner, outer;
private double inner;
private double outer;
private long conflicts;
private SearchParams params;
......
......@@ -53,7 +53,8 @@ public class EMARestarts implements RestartStrategy {
*/
private static final long serialVersionUID = 1L;
private long fast, slow;
private long fast;
private long slow;
private SolverStats stats;
......
......@@ -48,12 +48,12 @@ import org.sat4j.tools.SolverDecorator;
* @author daniel
*
*/
public abstract class AbstractSelectorVariablesDecorator extends
SolverDecorator<ISolver> implements IOptimizationProblem {
public abstract class AbstractSelectorVariablesDecorator
extends SolverDecorator<ISolver> implements IOptimizationProblem {
/**
*
*/
*
*/
private static final long serialVersionUID = 1L;
private int nbexpectedclauses;
......@@ -76,7 +76,7 @@ public abstract class AbstractSelectorVariablesDecorator extends
*/
private IVecInt prevBlockingClause;
public AbstractSelectorVariablesDecorator(ISolver solver) {
protected AbstractSelectorVariablesDecorator(ISolver solver) {
super(solver);
}
......@@ -102,13 +102,12 @@ public abstract class AbstractSelectorVariablesDecorator extends
boolean result = super.isSatisfiable(assumps, true);
if (result) {
this.prevboolmodel = new boolean[nVars()];
for (int i = 0; i < nVars(); i++) {
for (var i = 0; i < nVars(); i++) {
this.prevboolmodel[i] = decorated().model(i + 1);
}
this.prevfullmodel = super.modelWithInternalVariables();
this.prevmodel = super.model();
this.prevBlockingClause = super
.createBlockingClauseForCurrentModel();
this.prevBlockingClause = super.createBlockingClauseForCurrentModel();
calculateObjectiveValue();
} else {
this.isSolutionOptimal = true;
......@@ -124,8 +123,8 @@ public abstract class AbstractSelectorVariablesDecorator extends
}
@Override
public boolean model(int var) {
return this.prevboolmodel[var - 1];
public boolean model(int variable) {
return this.prevboolmodel[variable - 1];
}
@Override
......
......@@ -75,11 +75,11 @@ public final class MaxSatDecorator extends AbstractSelectorVariablesDecorator {
this.lits.push(newvar);
literals.push(newvar);
if (this.equivalence) {
ConstrGroup constrs = new ConstrGroup();
var constrs = new ConstrGroup();
constrs.add(super.addClause(literals));
IVecInt clause = new VecInt(2);
clause.push(-newvar);
for (int i = 0; i < literals.size() - 1; i++) {
for (var i = 0; i < literals.size() - 1; i++) {
clause.push(-literals.get(i));
constrs.add(super.addClause(clause));
}
......@@ -172,7 +172,6 @@ public final class MaxSatDecorator extends AbstractSelectorVariablesDecorator {
}
public void setTimeoutForFindingBetterSolution(int seconds) {
// TODO
throw new UnsupportedOperationException("No implemented yet");
}
}
......@@ -118,7 +118,7 @@ public final class MinOneDecorator extends SolverDecorator<ISolver>
*/
public void discardCurrentSolution() throws ContradictionException {
if (this.literals.isEmpty()) {
for (int i = 1; i <= nVars(); i++) {
for (var i = 1; i <= nVars(); i++) {
this.literals.push(i);
}
}
......@@ -176,7 +176,6 @@ public final class MinOneDecorator extends SolverDecorator<ISolver>
}
public void setTimeoutForFindingBetterSolution(int seconds) {
// TODO
throw new UnsupportedOperationException("No implemented yet");
}
}
......@@ -65,8 +65,8 @@ public class AAGReader extends Reader {
@Override
public String decode(int[] model) {
StringBuilder stb = new StringBuilder();
for (int i = 0; i < this.nbinputs; i++) {
var stb = new StringBuilder();
for (var i = 0; i < this.nbinputs; i++) {
stb.append(model[i] > 0 ? 1 : 0);
}
return stb.toString();
......@@ -74,7 +74,7 @@ public class AAGReader extends Reader {
@Override
public void decode(int[] model, PrintWriter out) {
for (int i = 0; i < this.nbinputs; i++) {
for (var i = 0; i < this.nbinputs; i++) {
out.print(model[i] > 0 ? 1 : 0);
}
}
......@@ -82,20 +82,20 @@ public class AAGReader extends Reader {
@Override
public IProblem parseInstance(java.io.InputStream in)
throws ParseFormatException, ContradictionException, IOException {
EfficientScanner scanner = new EfficientScanner(in);
var scanner = new EfficientScanner(in);
String prefix = scanner.next();
if (!"aag".equals(prefix)) {
throw new ParseFormatException("AAG format only!");
}
this.maxvarid = scanner.nextInt();
this.nbinputs = scanner.nextInt();
int nblatches = scanner.nextInt();
int nboutputs = scanner.nextInt();
var nblatches = scanner.nextInt();
var nboutputs = scanner.nextInt();
if (nboutputs > 1) {
throw new ParseFormatException(
"CNF conversion allowed for single output circuit only!");
}
int nbands = scanner.nextInt();
var nbands = scanner.nextInt();
this.solver.newVar(this.maxvarid + 1);
this.solver.setExpectedNumberOfClauses(3 * nbands + 2);
readInput(this.nbinputs, scanner);
......@@ -110,10 +110,10 @@ public class AAGReader extends Reader {
private void readAnd(int nbands, int output0, EfficientScanner scanner)
throws ContradictionException, IOException, ParseFormatException {
for (int i = 0; i < nbands; i++) {
int lhs = scanner.nextInt();
int rhs0 = scanner.nextInt();
int rhs1 = scanner.nextInt();
for (var i = 0; i < nbands; i++) {
var lhs = scanner.nextInt();
var rhs0 = scanner.nextInt();
var rhs1 = scanner.nextInt();
this.solver.and(toDimacs(lhs), toDimacs(rhs0), toDimacs(rhs1));
}
this.solver.gateTrue(this.maxvarid + 1);
......@@ -127,17 +127,17 @@ public class AAGReader extends Reader {
if (v == TRUE) {
return this.maxvarid + 1;
}
int var = v >> 1;
int variable = v >> 1;
if ((v & 1) == 0) {
return var;
return variable;
}
return -var;
return -variable;
}
private int readOutput(int nboutputs, EfficientScanner scanner)
throws IOException, ParseFormatException {
IVecInt outputs = new VecInt(nboutputs);
for (int i = 0; i < nboutputs; i++) {
for (var i = 0; i < nboutputs; i++) {
outputs.push(scanner.nextInt());
}
return outputs.get(0);
......@@ -146,7 +146,7 @@ public class AAGReader extends Reader {
private IVecInt readInput(int numberOfInputs, EfficientScanner scanner)
throws IOException, ParseFormatException {
IVecInt inputs = new VecInt(numberOfInputs);
for (int i = 0; i < numberOfInputs; i++) {
for (var i = 0; i < numberOfInputs; i++) {
inputs.push(scanner.nextInt());
}
return inputs;
......
......@@ -48,6 +48,11 @@ import org.sat4j.tools.GateTranslator;
@Feature(value = "reader", parent = "expert")
public class AIGReader extends Reader {
/**
*
*/
private static final long serialVersionUID = 1L;
private static final int FALSE = 0;
private static final int TRUE = 1;
......@@ -64,8 +69,8 @@ public class AIGReader extends Reader {
@Override
public String decode(int[] model) {
StringBuilder stb = new StringBuilder();
for (int i = 0; i < this.nbinputs; i++) {
var stb = new StringBuilder();
for (var i = 0; i < this.nbinputs; i++) {
stb.append(model[i] > 0 ? 1 : 0);
}
return stb.toString();
......@@ -73,7 +78,7 @@ public class AIGReader extends Reader {
@Override
public void decode(int[] model, PrintWriter out) {
for (int i = 0; i < this.nbinputs; i++) {
for (var i = 0; i < this.nbinputs; i++) {
out.print(model[i] > 0 ? 1 : 0);
}
}
......@@ -113,22 +118,22 @@ public class AIGReader extends Reader {
}
this.maxvarid = parseInt(in, ' ');
this.nbinputs = parseInt(in, ' ');
int nblatches = parseInt(in, ' ');
var nblatches = parseInt(in, ' ');
if (nblatches > 0) {
throw new ParseFormatException(
"CNF conversion cannot handle latches!");
}
int nboutputs = parseInt(in, ' ');
var nboutputs = parseInt(in, ' ');
if (nboutputs > 1) {
throw new ParseFormatException(
"CNF conversion allowed for single output circuit only!");
}
int nbands = parseInt(in, '\n');
var nbands = parseInt(in, '\n');
this.solver.newVar(this.maxvarid + 1);
this.solver.setExpectedNumberOfClauses(3 * nbands + 2);
if (nboutputs > 0) {
assert nboutputs == 1;
int output0 = parseInt(in, '\n');
var output0 = parseInt(in, '\n');
readAnd(nbands, output0, in, 2 * (this.nbinputs + 1));
}
return this.solver;
......@@ -157,7 +162,7 @@ public class AIGReader extends Reader {
private void readAnd(int nbands, int output0, InputStream in, int startid)
throws ContradictionException, IOException, ParseFormatException {
int lhs = startid;
for (int i = 0; i < nbands; i++) {
for (var i = 0; i < nbands; i++) {
int delta0 = decode(in);
int delta1 = decode(in);
int rhs0 = lhs - delta0;
......@@ -176,10 +181,10 @@ public class AIGReader extends Reader {
if (v == TRUE) {
return this.maxvarid + 1;
}
int var = v >> 1;
int variable = v >> 1;
if ((v & 1) == 0) {
return var;
return variable;
}
return -var;
return -variable;
}
}
......@@ -153,13 +153,13 @@ public class DimacsReader extends Reader implements Serializable {
*/
protected void readConstrs()
throws IOException, ParseFormatException, ContradictionException {
int realNbOfConstr = 0;
var realNbOfConstr = 0;
this.literals.clear();
boolean needToContinue = true;
var needToContinue = true;
while (needToContinue) {
boolean added = false;
var added = false;
if (this.scanner.eof()) {
// end of file
if (this.literals.size() > 0) {
......@@ -216,7 +216,7 @@ public class DimacsReader extends Reader implements Serializable {
protected boolean handleLine()
throws ContradictionException, IOException, ParseFormatException {
int lit;
boolean added = false;
var added = false;
while (!this.scanner.eof()) {
lit = this.scanner.nextInt();
if (lit == 0) {
......@@ -265,7 +265,7 @@ public class DimacsReader extends Reader implements Serializable {
@Override
public String decode(int[] model) {
StringBuilder stb = new StringBuilder();
var stb = new StringBuilder();
for (int element : model) {
stb.append(element);
stb.append(" ");
......
......@@ -98,9 +98,9 @@ public class EfficientScanner implements Serializable {
* @throws ParseFormatException
*/
public int nextInt() throws IOException, ParseFormatException {
int val = 0;
boolean neg = false;
char currentChar = skipSpaces();
var val = 0;
var neg = false;
var currentChar = skipSpaces();
if (currentChar == '-') {
neg = true;
currentChar = (char) this.in.read();
......@@ -123,17 +123,15 @@ public class EfficientScanner implements Serializable {
return neg ? -val : val;
}
public BigInteger nextBigInteger() throws IOException, ParseFormatException {
StringBuilder stb = new StringBuilder();
char currentChar = skipSpaces();
if (currentChar == '-') {
public BigInteger nextBigInteger()
throws IOException, ParseFormatException {
var stb = new StringBuilder();
var currentChar = skipSpaces();
if