Commit b7b13afe authored by Daniel Le Berre's avatar Daniel Le Berre
Browse files

Fixed a few more sonarqube violations

parent f6815808
Pipeline #20209 passed with stages
in 52 minutes and 10 seconds
......@@ -46,6 +46,8 @@ import org.sat4j.specs.UnitClauseProvider;
public abstract class AbstractOutputSolver implements ISolver {
private static final String THERE_IS_NO_REAL_SOLVER_BEHIND = "There is no real solver behind!";
protected int nbvars;
protected int nbclauses;
......@@ -94,11 +96,11 @@ public abstract class AbstractOutputSolver implements ISolver {
public boolean isSatisfiable(IVecInt assumps, boolean global)
throws TimeoutException {
throw new TimeoutException("There is no real solver behind!");
throw new TimeoutException(THERE_IS_NO_REAL_SOLVER_BEHIND);
}
public boolean isSatisfiable(boolean global) throws TimeoutException {
throw new TimeoutException("There is no real solver behind!");
throw new TimeoutException(THERE_IS_NO_REAL_SOLVER_BEHIND);
}
public void printInfos(PrintWriter output, String prefix) {
......@@ -140,11 +142,11 @@ public abstract class AbstractOutputSolver implements ISolver {
}
public boolean isSatisfiable() throws TimeoutException {
throw new TimeoutException("There is no real solver behind!");
throw new TimeoutException(THERE_IS_NO_REAL_SOLVER_BEHIND);
}
public boolean isSatisfiable(IVecInt assumps) throws TimeoutException {
throw new TimeoutException("There is no real solver behind!");
throw new TimeoutException(THERE_IS_NO_REAL_SOLVER_BEHIND);
}
public int[] findModel() throws TimeoutException {
......
......@@ -51,6 +51,8 @@ import org.sat4j.specs.TimeoutException;
*/
public class AllMUSes implements Serializable {
private static final String ORG_SAT4J_CORE = "org.sat4j.core";
/**
*
*/
......@@ -197,7 +199,7 @@ public class AllMUSes implements Serializable {
}
}
} catch (TimeoutException e) {
Logger.getLogger("org.sat4j.core").log(Level.INFO,
Logger.getLogger(ORG_SAT4J_CORE).log(Level.INFO,
"Timeout when computing all muses", e);
}
if (css.isVerbose()) {
......@@ -290,14 +292,14 @@ public class AllMUSes implements Serializable {
try {
css.addBlockingClause(blockingClause);
} catch (ContradictionException e) {
Logger.getLogger("org.sat4j.core").log(Level.INFO,
Logger.getLogger(ORG_SAT4J_CORE).log(Level.INFO,
"Trivial inconsistency", e);
break;
}
}
} catch (TimeoutException e) {
Logger.getLogger("org.sat4j.core").log(Level.INFO,
Logger.getLogger(ORG_SAT4J_CORE).log(Level.INFO,
"Timeout during the first stage", e);
}
if (css.isVerbose()) {
......
......@@ -46,6 +46,8 @@ import org.sat4j.specs.TimeoutException;
@Feature("solutionlistener")
public class CheckMUSSolutionListener implements SolutionFoundListener {
private static final String ORG_SAT4J_CORE = "org.sat4j.core";
/**
*
*/
......@@ -96,11 +98,11 @@ public class CheckMUSSolutionListener implements SolutionFoundListener {
}
} catch (ContradictionException e) {
Logger.getLogger("org.sat4j.core").log(Level.INFO,
Logger.getLogger(ORG_SAT4J_CORE).log(Level.INFO,
"Trivial inconsistency", e);
result = true;
} catch (TimeoutException e) {
Logger.getLogger("org.sat4j.core").log(Level.INFO,
Logger.getLogger(ORG_SAT4J_CORE).log(Level.INFO,
"Timeout when checking unsatisfiability", e);
}
......@@ -121,11 +123,11 @@ public class CheckMUSSolutionListener implements SolutionFoundListener {
}
}
} catch (ContradictionException e) {
Logger.getLogger("org.sat4j.core").log(Level.INFO,
Logger.getLogger(ORG_SAT4J_CORE).log(Level.INFO,
"Trivial inconsistency", e);
result = false;
} catch (TimeoutException e) {
Logger.getLogger("org.sat4j.core").log(Level.INFO,
Logger.getLogger(ORG_SAT4J_CORE).log(Level.INFO,
"Timeout when checking satisfiability", e);
}
......
......@@ -56,6 +56,8 @@ import org.sat4j.specs.UnitClauseConsumer;
public class DimacsOutputSolver extends AbstractOutputSolver
implements IGroupSolver {
private static final String NOT_A_CLAUSAL_PROBLEM_DEGREE = "Not a clausal problem! degree ";
/**
*
*/
......@@ -110,7 +112,7 @@ public class DimacsOutputSolver extends AbstractOutputSolver
throws ContradictionException {
if (degree > 1) {
throw new UnsupportedOperationException(
"Not a clausal problem! degree " + degree);
NOT_A_CLAUSAL_PROBLEM_DEGREE + degree);
}
assert degree == 1;
if (this.firstConstr) {
......@@ -132,7 +134,7 @@ public class DimacsOutputSolver extends AbstractOutputSolver
throws ContradictionException {
if (degree > 1) {
throw new UnsupportedOperationException(
"Not a clausal problem! degree " + degree);
NOT_A_CLAUSAL_PROBLEM_DEGREE + degree);
}
assert degree == 1;
return addClause(literals);
......@@ -142,7 +144,7 @@ public class DimacsOutputSolver extends AbstractOutputSolver
throws ContradictionException {
if (n > 1) {
throw new UnsupportedOperationException(
"Not a clausal problem! degree " + n);
NOT_A_CLAUSAL_PROBLEM_DEGREE + n);
}
assert n == 1;
addAtMost(literals, n);
......
......@@ -58,6 +58,8 @@ import org.sat4j.specs.UnitClauseConsumer;
public class DimacsStringSolver extends AbstractOutputSolver
implements IGroupSolver {
private static final String NOT_A_CLAUSAL_PROBLEM_DEGREE = "Not a clausal problem! degree ";
/**
*
*/
......@@ -130,7 +132,7 @@ public class DimacsStringSolver extends AbstractOutputSolver
throws ContradictionException {
if (degree > 1) {
throw new UnsupportedOperationException(
"Not a clausal problem! degree " + degree);
NOT_A_CLAUSAL_PROBLEM_DEGREE + degree);
}
assert degree == 1;
if (this.firstConstr) {
......@@ -159,7 +161,7 @@ public class DimacsStringSolver extends AbstractOutputSolver
throws ContradictionException {
if (n > 1) {
throw new UnsupportedOperationException(
"Not a clausal problem! degree " + n);
NOT_A_CLAUSAL_PROBLEM_DEGREE + n);
}
assert n == 1;
addAtMost(literals, n);
......@@ -171,7 +173,7 @@ public class DimacsStringSolver extends AbstractOutputSolver
throws ContradictionException {
if (degree > 1) {
throw new UnsupportedOperationException(
"Not a clausal problem! degree " + degree);
NOT_A_CLAUSAL_PROBLEM_DEGREE + degree);
}
assert degree == 1;
return addClause(literals);
......
......@@ -66,6 +66,7 @@ public class MultiTracing<T extends ISolverService>
this.listeners.addAll(listenersList);
}
@Override
public void assuming(int p) {
for (SearchListener<T> sl : this.listeners) {
sl.assuming(p);
......@@ -73,24 +74,28 @@ public class MultiTracing<T extends ISolverService>
}
@Override
public void propagating(int p) {
for (SearchListener<T> sl : this.listeners) {
sl.propagating(p);
}
}
@Override
public void enqueueing(int p, IConstr reason) {
for (SearchListener<T> sl : this.listeners) {
sl.enqueueing(p, reason);
}
}
@Override
public void backtracking(int p) {
for (SearchListener<T> sl : this.listeners) {
sl.backtracking(p);
}
}
@Override
public void adding(int p) {
for (SearchListener<T> sl : this.listeners) {
sl.adding(p);
......@@ -98,6 +103,7 @@ public class MultiTracing<T extends ISolverService>
}
@Override
public void learn(IConstr c) {
for (SearchListener<T> sl : this.listeners) {
sl.learn(c);
......@@ -105,12 +111,14 @@ public class MultiTracing<T extends ISolverService>
}
@Override
public void learnUnit(int p) {
for (SearchListener<T> sl : this.listeners) {
sl.learnUnit(p);
}
}
@Override
public void delete(IConstr c) {
for (SearchListener<T> sl : this.listeners) {
sl.delete(c);
......@@ -118,6 +126,7 @@ public class MultiTracing<T extends ISolverService>
}
@Override
public void conflictFound(IConstr confl, int dlevel, int trailLevel) {
for (SearchListener<T> sl : this.listeners) {
sl.conflictFound(confl, dlevel, trailLevel);
......@@ -125,6 +134,7 @@ public class MultiTracing<T extends ISolverService>
}
@Override
public void conflictFound(int p) {
for (SearchListener<T> sl : this.listeners) {
sl.conflictFound(p);
......@@ -132,6 +142,7 @@ public class MultiTracing<T extends ISolverService>
}
@Override
public void solutionFound(int[] model, RandomAccessModel lazyModel) {
for (SearchListener<T> sl : this.listeners) {
sl.solutionFound(model, lazyModel);
......@@ -139,12 +150,14 @@ public class MultiTracing<T extends ISolverService>
}
@Override
public void beginLoop() {
for (SearchListener<T> sl : this.listeners) {
sl.beginLoop();
}
}
@Override
public void start() {
for (SearchListener<T> sl : this.listeners) {
sl.start();
......@@ -152,12 +165,14 @@ public class MultiTracing<T extends ISolverService>
}
@Override
public void end(Lbool result) {
for (SearchListener<T> sl : this.listeners) {
sl.end(result);
}
}
@Override
public void restarting() {
for (SearchListener<T> sl : this.listeners) {
sl.restarting();
......@@ -165,6 +180,7 @@ public class MultiTracing<T extends ISolverService>
}
@Override
public void backjump(int backjumpLevel) {
for (SearchListener<T> sl : this.listeners) {
sl.backjump(backjumpLevel);
......@@ -172,12 +188,14 @@ public class MultiTracing<T extends ISolverService>
}
@Override
public void init(T solverService) {
for (SearchListener<T> sl : this.listeners) {
sl.init(solverService);
}
}
@Override
public void cleaning() {
for (SearchListener<T> sl : this.listeners) {
sl.cleaning();
......
......@@ -31,7 +31,6 @@ package org.sat4j.tools;
import static org.sat4j.Messages.NOT_IMPLEMENTED_YET;
import java.io.PrintStream;
import java.io.PrintWriter;
import java.util.HashMap;
import java.util.Locale;
......@@ -157,19 +156,9 @@ public class StatisticsSolver implements ISolver {
return this.nbvars;
}
@Deprecated
public void printInfos(PrintWriter out, String prefix) {
}
public void printInfos(PrintWriter out) {
}
@Deprecated
public int newVar() {
throw new UnsupportedOperationException(NOT_IMPLEMENTED_YET);
}
public int nextFreeVarId(boolean reserve) {
throw new UnsupportedOperationException(NOT_IMPLEMENTED_YET);
}
......@@ -289,16 +278,6 @@ public class StatisticsSolver implements ISolver {
public void reset() {
}
@Deprecated
public void printStat(PrintStream out, String prefix) {
throw new UnsupportedOperationException(NOT_IMPLEMENTED_YET);
}
@Deprecated
public void printStat(PrintWriter out, String prefix) {
throw new UnsupportedOperationException(NOT_IMPLEMENTED_YET);
}
public void printStat(PrintWriter out) {
var realNumberOfVariables = 0;
var realNumberOfLiterals = 0;
......
......@@ -73,82 +73,76 @@ public class TextOutputTracing<T> implements SearchListener<ISolverService> {
return Integer.toString(dimacs);
}
@Override
public void assuming(int p) {
System.out.println("assuming " + node(p));
}
/**
* @since 2.1
*/
@Override
public void propagating(int p) {
System.out.println("propagating " + node(p));
}
@Override
public void enqueueing(int p, IConstr reason) {
System.out.println("enqueueing " + node(p));
}
@Override
public void backtracking(int p) {
System.out.println("backtracking " + node(p));
}
@Override
public void adding(int p) {
System.out.println("adding " + node(p));
}
/**
* @since 2.1
*/
@Override
public void learn(IConstr clause) {
System.out.println("learning " + clause);
}
/**
* @since 2.3.4
*/
@Override
public void learnUnit(int p) {
System.out.println("learning unit " + p);
}
@Override
public void delete(IConstr c) {
}
/**
* @since 2.1
*/
@Override
public void conflictFound(IConstr confl, int dlevel, int trailLevel) {
System.out.println("conflict ");
}
/**
* @since 2.1
*/
@Override
public void conflictFound(int p) {
System.out.println("conflict during propagation");
}
@Override
public void solutionFound(int[] model, RandomAccessModel lazyModel) {
System.out.println("solution found ");
}
@Override
public void beginLoop() {
}
@Override
public void start() {
}
/**
* @since 2.1
*/
@Override
public void end(Lbool result) {
}
/**
* @since 2.2
*/
@Override
public void restarting() {
System.out.println("restarting ");
}
......@@ -157,15 +151,11 @@ public class TextOutputTracing<T> implements SearchListener<ISolverService> {
System.out.println("backjumping to decision level " + backjumpLevel);
}
/**
* @since 2.3.2
*/
@Override
public void init(ISolverService solverService) {
}
/**
* @since 2.3.2
*/
@Override
public void cleaning() {
System.out.println("cleaning");
}
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment