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

Using a constant for error messages

parent 564208ab
Pipeline #20203 passed with stages
in 64 minutes and 56 seconds
......@@ -29,6 +29,8 @@
*******************************************************************************/
package org.sat4j;
import static org.sat4j.Messages.NOT_IMPLEMENTED_YET;
import java.io.PrintWriter;
import org.sat4j.annotations.Feature;
......@@ -195,7 +197,7 @@ public final class DecisionMode implements ILauncherMode {
@Override
public void onSolutionFound(IVecInt solution) {
throw new UnsupportedOperationException("Not implemented yet!");
throw new UnsupportedOperationException(NOT_IMPLEMENTED_YET);
}
@Override
......
......@@ -46,6 +46,8 @@ import org.sat4j.tools.xplain.Xplain;
public class MUSLauncher extends AbstractLauncher {
private static final String HIGH_LEVEL = "high level ";
/**
*
*/
......@@ -199,19 +201,19 @@ public class MUSLauncher extends AbstractLauncher {
+ (System.currentTimeMillis() - beginmus) / 1000.0);
} else {
log("Size of initial "
+ (this.highLevel ? "high level " : "")
+ (this.highLevel ? HIGH_LEVEL : "")
+ "unsat subformula: "
+ this.solver.unsatExplanation().size());
log("Computing " + (this.highLevel ? "high level " : "")
log("Computing " + (this.highLevel ? HIGH_LEVEL : "")
+ "MUS ...");
this.mus = this.xplain.minimalExplanation();
log("Size of the " + (this.highLevel ? "high level " : "")
log("Size of the " + (this.highLevel ? HIGH_LEVEL : "")
+ "MUS: " + this.mus.length);
log("Unsat core computation wall clock time (in seconds) : "
+ (System.currentTimeMillis() - beginmus) / 1000.0);
}
} catch (TimeoutException e) {
log("Cannot compute " + (this.highLevel ? "high level " : "")
log("Cannot compute " + (this.highLevel ? HIGH_LEVEL : "")
+ "MUS within the timeout.");
}
}
......
......@@ -39,6 +39,8 @@ import java.util.ResourceBundle;
*
*/
public final class Messages {
public static final String NOT_IMPLEMENTED_YET = "Not implemented yet!";
private static final String BUNDLE_NAME = "org.sat4j.messages"; //$NON-NLS-1$
private static final ResourceBundle RESOURCE_BUNDLE = ResourceBundle
......
......@@ -29,6 +29,8 @@
*******************************************************************************/
package org.sat4j;
import static org.sat4j.Messages.NOT_IMPLEMENTED_YET;
import java.io.PrintWriter;
import org.sat4j.annotations.Feature;
......@@ -190,7 +192,7 @@ public final class OptimizationMode implements ILauncherMode {
@Override
public void onSolutionFound(IVecInt solution) {
throw new UnsupportedOperationException("Not implemented yet!");
throw new UnsupportedOperationException(NOT_IMPLEMENTED_YET);
}
public void setExitCode(ExitCode exitCode) {
......
......@@ -29,6 +29,8 @@
*******************************************************************************/
package org.sat4j.minisat.constraints.card;
import static org.sat4j.Messages.NOT_IMPLEMENTED_YET;
import java.io.Serializable;
import java.util.HashSet;
import java.util.Set;
......@@ -412,11 +414,11 @@ public final class MaxWatchCard
}
public void calcReasonOnTheFly(int p, IVecInt trail, IVecInt outReason) {
throw new UnsupportedOperationException("Not implemented yet!");
throw new UnsupportedOperationException(NOT_IMPLEMENTED_YET);
}
public void propagatePI(MandatoryLiteralListener l, int p) {
throw new UnsupportedOperationException("Not implemented yet!");
throw new UnsupportedOperationException(NOT_IMPLEMENTED_YET);
}
......@@ -429,7 +431,7 @@ public final class MaxWatchCard
}
public boolean isSatisfied() {
throw new UnsupportedOperationException("Not implemented yet!");
throw new UnsupportedOperationException(NOT_IMPLEMENTED_YET);
}
public int getAssertionLevel(IVecInt trail, int decisionLevel) {
......
......@@ -29,6 +29,8 @@
*******************************************************************************/
package org.sat4j.minisat.constraints.card;
import static org.sat4j.Messages.NOT_IMPLEMENTED_YET;
import java.io.Serializable;
import java.util.HashSet;
import java.util.Set;
......@@ -665,7 +667,7 @@ public class MinWatchCard
}
public boolean isSatisfied() {
throw new UnsupportedOperationException("Not implemented yet!");
throw new UnsupportedOperationException(NOT_IMPLEMENTED_YET);
}
public int getAssertionLevel(IVecInt trail, int decisionLevel) {
......
......@@ -27,6 +27,8 @@
*******************************************************************************/
package org.sat4j.minisat.constraints.cnf;
import static org.sat4j.Messages.NOT_IMPLEMENTED_YET;
import java.io.Serializable;
import org.sat4j.annotations.Feature;
......@@ -192,7 +194,7 @@ public class BinaryClauses implements Constr, Propagatable, Serializable {
}
public String toString(VarMapper mapper) {
throw new UnsupportedOperationException("Not implemented yet!");
throw new UnsupportedOperationException(NOT_IMPLEMENTED_YET);
}
public void propagatePI(MandatoryLiteralListener l, int p) {
......@@ -211,31 +213,31 @@ public class BinaryClauses implements Constr, Propagatable, Serializable {
}
public void calcReasonOnTheFly(int p, IVecInt trail, IVecInt outReason) {
throw new UnsupportedOperationException("Not implemented yet!");
throw new UnsupportedOperationException(NOT_IMPLEMENTED_YET);
}
public void assertConstraintIfNeeded(UnitPropagationListener s) {
throw new UnsupportedOperationException("Not implemented yet!");
throw new UnsupportedOperationException(NOT_IMPLEMENTED_YET);
}
public boolean canBeSatisfiedByCountingLiterals() {
throw new UnsupportedOperationException("Not implemented yet!");
throw new UnsupportedOperationException(NOT_IMPLEMENTED_YET);
}
public int requiredNumberOfSatisfiedLiterals() {
throw new UnsupportedOperationException("Not implemented yet!");
throw new UnsupportedOperationException(NOT_IMPLEMENTED_YET);
}
public boolean isSatisfied() {
throw new UnsupportedOperationException("Not implemented yet!");
throw new UnsupportedOperationException(NOT_IMPLEMENTED_YET);
}
public int getAssertionLevel(IVecInt trail, int decisionLevel) {
throw new UnsupportedOperationException("Not implemented yet!");
throw new UnsupportedOperationException(NOT_IMPLEMENTED_YET);
}
@Override
public String dump() {
throw new UnsupportedOperationException("Not implemented yet!");
throw new UnsupportedOperationException(NOT_IMPLEMENTED_YET);
}
}
......@@ -27,6 +27,8 @@
*******************************************************************************/
package org.sat4j.minisat.constraints.cnf;
import static org.sat4j.Messages.NOT_IMPLEMENTED_YET;
import java.io.Serializable;
import org.sat4j.annotations.Feature;
......@@ -276,43 +278,43 @@ public class CBClause implements Constr, Undoable, Propagatable, Serializable {
}
public boolean canBePropagatedMultipleTimes() {
throw new UnsupportedOperationException("Not implemented yet!");
throw new UnsupportedOperationException(NOT_IMPLEMENTED_YET);
}
public String toString(VarMapper mapper) {
throw new UnsupportedOperationException("Not implemented yet!");
throw new UnsupportedOperationException(NOT_IMPLEMENTED_YET);
}
public void remove(UnitPropagationListener upl) {
throw new UnsupportedOperationException("Not implemented yet!");
throw new UnsupportedOperationException(NOT_IMPLEMENTED_YET);
}
public void calcReasonOnTheFly(int p, IVecInt trail, IVecInt outReason) {
throw new UnsupportedOperationException("Not implemented yet!");
throw new UnsupportedOperationException(NOT_IMPLEMENTED_YET);
}
public void assertConstraintIfNeeded(UnitPropagationListener s) {
throw new UnsupportedOperationException("Not implemented yet!");
throw new UnsupportedOperationException(NOT_IMPLEMENTED_YET);
}
public boolean canBeSatisfiedByCountingLiterals() {
throw new UnsupportedOperationException("Not implemented yet!");
throw new UnsupportedOperationException(NOT_IMPLEMENTED_YET);
}
public int requiredNumberOfSatisfiedLiterals() {
throw new UnsupportedOperationException("Not implemented yet!");
throw new UnsupportedOperationException(NOT_IMPLEMENTED_YET);
}
public boolean isSatisfied() {
throw new UnsupportedOperationException("Not implemented yet!");
throw new UnsupportedOperationException(NOT_IMPLEMENTED_YET);
}
public int getAssertionLevel(IVecInt trail, int decisionLevel) {
throw new UnsupportedOperationException("Not implemented yet!");
throw new UnsupportedOperationException(NOT_IMPLEMENTED_YET);
}
public void propagatePI(MandatoryLiteralListener l, int p) {
throw new UnsupportedOperationException("Not implemented yet!");
throw new UnsupportedOperationException(NOT_IMPLEMENTED_YET);
}
public Constr toConstraint() {
......
......@@ -29,6 +29,7 @@
*******************************************************************************/
package org.sat4j.minisat.constraints.cnf;
import static org.sat4j.Messages.NOT_IMPLEMENTED_YET;
import static org.sat4j.core.LiteralsUtils.neg;
import org.sat4j.annotations.Feature;
......@@ -103,7 +104,7 @@ public class LearntHTClause extends HTClause {
}
public void propagatePI(MandatoryLiteralListener l, int p) {
throw new UnsupportedOperationException("Not implemented yet!");
throw new UnsupportedOperationException(NOT_IMPLEMENTED_YET);
}
}
......@@ -29,6 +29,8 @@
*******************************************************************************/
package org.sat4j.minisat.constraints.cnf;
import static org.sat4j.Messages.NOT_IMPLEMENTED_YET;
import org.sat4j.annotations.Feature;
import org.sat4j.core.LiteralsUtils;
import org.sat4j.minisat.core.ILits;
......@@ -78,14 +80,17 @@ public class UnitClause implements Constr {
}
}
@Override
public double getActivity() {
return activity;
}
@Override
public void incActivity(double claInc) {
// silent to prevent problems with xplain trick.
}
@Override
public void setActivity(double claInc) {
activity = claInc;
}
......@@ -94,6 +99,7 @@ public class UnitClause implements Constr {
throw new UnsupportedOperationException();
}
@Override
public void register() {
}
......@@ -151,7 +157,7 @@ public class UnitClause implements Constr {
}
public void propagatePi(MandatoryLiteralListener m) {
throw new UnsupportedOperationException("Not implemented yet!");
throw new UnsupportedOperationException(NOT_IMPLEMENTED_YET);
}
......
......@@ -29,6 +29,8 @@
*******************************************************************************/
package org.sat4j.minisat.constraints.cnf;
import static org.sat4j.Messages.NOT_IMPLEMENTED_YET;
import org.sat4j.annotations.Feature;
import org.sat4j.specs.Constr;
import org.sat4j.specs.IVecInt;
......@@ -126,15 +128,15 @@ public class UnitClauses implements Constr {
}
public void propagatePi(MandatoryLiteralListener m) {
throw new UnsupportedOperationException("Not implemented yet!");
throw new UnsupportedOperationException(NOT_IMPLEMENTED_YET);
}
public boolean canBeSatisfiedByCountingLiterals() {
throw new UnsupportedOperationException("Not implemented yet!");
throw new UnsupportedOperationException(NOT_IMPLEMENTED_YET);
}
public int requiredNumberOfSatisfiedLiterals() {
throw new UnsupportedOperationException("Not implemented yet!");
throw new UnsupportedOperationException(NOT_IMPLEMENTED_YET);
}
public boolean isSatisfied() {
......@@ -142,11 +144,11 @@ public class UnitClauses implements Constr {
}
public int getAssertionLevel(IVecInt trail, int decisionLevel) {
throw new UnsupportedOperationException("Not implemented yet!");
throw new UnsupportedOperationException(NOT_IMPLEMENTED_YET);
}
public String toString(VarMapper mapper) {
throw new UnsupportedOperationException("Not implemented yet!");
throw new UnsupportedOperationException(NOT_IMPLEMENTED_YET);
}
@Override
......
package org.sat4j.minisat.constraints.xor;
import static org.sat4j.Messages.NOT_IMPLEMENTED_YET;
import org.sat4j.annotations.Feature;
import org.sat4j.core.LiteralsUtils;
import org.sat4j.minisat.core.ILits;
......@@ -73,7 +75,7 @@ public class Xor implements Constr, Propagatable {
@Override
public double getActivity() {
throw new UnsupportedOperationException("Not implemented yet!");
throw new UnsupportedOperationException(NOT_IMPLEMENTED_YET);
}
@Override
......@@ -83,7 +85,7 @@ public class Xor implements Constr, Propagatable {
@Override
public String toString(VarMapper mapper) {
throw new UnsupportedOperationException("Not implemented yet!");
throw new UnsupportedOperationException(NOT_IMPLEMENTED_YET);
}
@Override
......@@ -124,7 +126,7 @@ public class Xor implements Constr, Propagatable {
@Override
public void propagatePI(MandatoryLiteralListener l, int p) {
throw new UnsupportedOperationException("Not implemented yet!");
throw new UnsupportedOperationException(NOT_IMPLEMENTED_YET);
}
@Override
......@@ -162,17 +164,17 @@ public class Xor implements Constr, Propagatable {
@Override
public void calcReasonOnTheFly(int p, IVecInt trail, IVecInt outReason) {
throw new UnsupportedOperationException("Not implemented yet!");
throw new UnsupportedOperationException(NOT_IMPLEMENTED_YET);
}
@Override
public boolean locked() {
throw new UnsupportedOperationException("Not implemented yet!");
throw new UnsupportedOperationException(NOT_IMPLEMENTED_YET);
}
@Override
public void setLearnt() {
throw new UnsupportedOperationException("Not implemented yet!");
throw new UnsupportedOperationException(NOT_IMPLEMENTED_YET);
}
@Override
......@@ -185,12 +187,12 @@ public class Xor implements Constr, Propagatable {
@Override
public void assertConstraint(UnitPropagationListener s) {
throw new UnsupportedOperationException("Not implemented yet!");
throw new UnsupportedOperationException(NOT_IMPLEMENTED_YET);
}
@Override
public void assertConstraintIfNeeded(UnitPropagationListener s) {
throw new UnsupportedOperationException("Not implemented yet!");
throw new UnsupportedOperationException(NOT_IMPLEMENTED_YET);
}
@Override
......@@ -200,22 +202,22 @@ public class Xor implements Constr, Propagatable {
@Override
public int requiredNumberOfSatisfiedLiterals() {
throw new UnsupportedOperationException("Not implemented yet!");
throw new UnsupportedOperationException(NOT_IMPLEMENTED_YET);
}
@Override
public boolean isSatisfied() {
throw new UnsupportedOperationException("Not implemented yet!");
throw new UnsupportedOperationException(NOT_IMPLEMENTED_YET);
}
@Override
public int getAssertionLevel(IVecInt trail, int decisionLevel) {
throw new UnsupportedOperationException("Not implemented yet!");
throw new UnsupportedOperationException(NOT_IMPLEMENTED_YET);
}
@Override
public String dump() {
throw new UnsupportedOperationException("Not implemented yet!");
throw new UnsupportedOperationException(NOT_IMPLEMENTED_YET);
}
@Override
......
......@@ -29,6 +29,7 @@
*******************************************************************************/
package org.sat4j.minisat.core;
import static org.sat4j.Messages.NOT_IMPLEMENTED_YET;
import static org.sat4j.core.LiteralsUtils.toDimacs;
import static org.sat4j.core.LiteralsUtils.toInternal;
import static org.sat4j.core.LiteralsUtils.var;
......@@ -2373,14 +2374,14 @@ public class Solver<D extends DataStructureFactory>
* @since 2.3.2
*/
public int[] getLiteralsPropagatedAt(int decisionLevel) {
throw new UnsupportedOperationException("Not implemented yet!");
throw new UnsupportedOperationException(NOT_IMPLEMENTED_YET);
}
/**
* @since 2.3.2
*/
public void suggestNextLiteralToBranchOn(int l) {
throw new UnsupportedOperationException("Not implemented yet!");
throw new UnsupportedOperationException(NOT_IMPLEMENTED_YET);
}
protected boolean isNeedToReduceDB() {
......
......@@ -88,6 +88,6 @@ public final class FakeConstr implements IConstr {
@Override
public String dump() {
throw new UnsupportedOperationException("Not implemented yet!");
throw new UnsupportedOperationException(FAKE_I_CONSTR_MSG);
}
}
......@@ -29,6 +29,8 @@
*******************************************************************************/
package org.sat4j.tools;
import static org.sat4j.Messages.NOT_IMPLEMENTED_YET;
import java.io.ObjectInputStream;
import java.io.PrintWriter;
import java.util.Collection;
......@@ -231,25 +233,25 @@ public class DimacsOutputSolver extends AbstractOutputSolver
}
public Collection<Integer> getAddedVars() {
throw new UnsupportedOperationException("Not implemented yet!");
throw new UnsupportedOperationException(NOT_IMPLEMENTED_YET);
}
@Override
public IConstr addParity(IVecInt literals, boolean even) {
throw new UnsupportedOperationException("Not implemented yet!");
throw new UnsupportedOperationException(NOT_IMPLEMENTED_YET);
}
public AssignmentOrigin getOriginInModel(int p) {
throw new UnsupportedOperationException("Not implemented yet!");
throw new UnsupportedOperationException(NOT_IMPLEMENTED_YET);
}
@Override
public void setUnitClauseConsumer(UnitClauseConsumer ucc) {
throw new UnsupportedOperationException("Not implemented yet!");
throw new UnsupportedOperationException(NOT_IMPLEMENTED_YET);
}
@Override
public int[] decisions() {
throw new UnsupportedOperationException("Not implemented yet!");
throw new UnsupportedOperationException(NOT_IMPLEMENTED_YET);
}
}
......@@ -29,6 +29,8 @@
*******************************************************************************/
package org.sat4j.tools;
import static org.sat4j.Messages.NOT_IMPLEMENTED_YET;
import java.io.PrintWriter;
import java.util.Collection;
import java.util.Iterator;
......@@ -260,7 +262,7 @@ public class DimacsStringSolver extends AbstractOutputSolver
}
public Collection<Integer> getAddedVars() {
throw new UnsupportedOperationException("Not implemented yet!");
throw new UnsupportedOperationException(NOT_IMPLEMENTED_YET);
}
@Override
......@@ -272,20 +274,20 @@ public class DimacsStringSolver extends AbstractOutputSolver
@Override
public IConstr addParity(IVecInt literals, boolean even) {
throw new UnsupportedOperationException("Not implemented yet!");
throw new UnsupportedOperationException(NOT_IMPLEMENTED_YET);
}
public AssignmentOrigin getOriginInModel(int p) {
throw new UnsupportedOperationException("Not implemented yet!");
throw new UnsupportedOperationException(NOT_IMPLEMENTED_YET);
}
@Override
public void setUnitClauseConsumer(UnitClauseConsumer ucc) {
throw new UnsupportedOperationException("Not implemented yet!");
throw new UnsupportedOperationException(NOT_IMPLEMENTED_YET);
}
@Override
public int[] decisions() {
throw new UnsupportedOperationException("Not implemented yet!");
throw new UnsupportedOperationException(NOT_IMPLEMENTED_YET);
}
}
......@@ -29,6 +29,8 @@
*******************************************************************************/
package org.sat4j.tools;
import static org.sat4j.Messages.NOT_IMPLEMENTED_YET;
import java.io.PrintStream;
import java.io.PrintWriter;
import java.util.Map;
......@@ -65,41 +67,41 @@ public abstract class EmptySolver implements ISolver {
private int nbClauses;
public int[] model() {
throw new UnsupportedOperationException("Not implemented yet!");
throw new UnsupportedOperationException(NOT_IMPLEMENTED_YET);
}
public int[] primeImplicant() {
throw new UnsupportedOperationException("Not implemented yet!");
throw new UnsupportedOperationException(NOT_IMPLEMENTED_YET);
}