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

fixed more sonarqube violatons (cardinality constraints)

parent 0f236732
Pipeline #20063 failed with stages
in 15 seconds
......@@ -183,7 +183,6 @@ public final class VecInt implements IVecInt {
}
public void set(int i, int o) {
assert i >= 0 && i < this.nbelem;
this.myarray[i] = o;
}
......
......@@ -405,7 +405,7 @@ public final class SolverFactory extends ASolverFactory<ISolver> {
* instance of ASolverFactory.
*/
public static ISolver newDefault() {
return newGlucose21(); // newMiniLearningHeapRsatExpSimpBiere();
return newGlucose21();
}
@Override
......
......@@ -46,12 +46,12 @@ import org.sat4j.specs.UnitPropagationListener;
* @author leberre To change the template for this generated type comment go to
* Window&gt;Preferences&gt;Java&gt;Code Generation&gt;Code and Comments
*/
public abstract class AbstractDataStructureFactory implements
DataStructureFactory, Serializable {
public abstract class AbstractDataStructureFactory
implements DataStructureFactory, Serializable {
/**
*
*/
*
*/
private static final long serialVersionUID = 1L;
/*
......@@ -86,7 +86,7 @@ public abstract class AbstractDataStructureFactory implements
protected abstract ILits createLits();
private final IVec<Propagatable> tmp = new Vec<Propagatable>();
private final IVec<Propagatable> tmp = new Vec<>();
/*
* (non-Javadoc)
......
......@@ -72,6 +72,7 @@ public class CardinalityDataStructure extends AbstractCardinalityDataStructure {
degree);
}
@Override
public Constr createUnregisteredCardinalityConstraint(IVecInt literals,
int degree) {
return new AtLeast(getVocabulary(), literals, degree);
......
......@@ -40,8 +40,8 @@ import org.sat4j.specs.IVecInt;
* @author leberre To change the template for this generated type comment go to
* Window - Preferences - Java - Code Generation - Code and Comments
*/
public class CardinalityDataStructureYanMax extends
AbstractCardinalityDataStructure {
public class CardinalityDataStructureYanMax
extends AbstractCardinalityDataStructure {
private static final long serialVersionUID = 1L;
......@@ -75,10 +75,11 @@ public class CardinalityDataStructureYanMax extends
literals, MinWatchCard.ATLEAST, degree);
}
@Override
public Constr createUnregisteredCardinalityConstraint(IVecInt literals,
int degree) {
return new MaxWatchCard(getVocabulary(), literals,
MinWatchCard.ATLEAST, degree);
return new MaxWatchCard(getVocabulary(), literals, MinWatchCard.ATLEAST,
degree);
}
}
......@@ -39,8 +39,8 @@ import org.sat4j.specs.IVecInt;
* @author leberre To change the template for this generated type comment go to
* Window - Preferences - Java - Code Generation - Code and Comments
*/
public class CardinalityDataStructureYanMin extends
AbstractCardinalityDataStructure {
public class CardinalityDataStructureYanMin
extends AbstractCardinalityDataStructure {
private static final long serialVersionUID = 1L;
......@@ -74,9 +74,10 @@ public class CardinalityDataStructureYanMin extends
literals, MinWatchCard.ATLEAST, degree);
}
@Override
public Constr createUnregisteredCardinalityConstraint(IVecInt literals,
int degree) {
return new MinWatchCard(getVocabulary(), literals,
MinWatchCard.ATLEAST, degree);
return new MinWatchCard(getVocabulary(), literals, MinWatchCard.ATLEAST,
degree);
}
}
......@@ -90,8 +90,6 @@ public class MixedDataStructureDanielWLConciseBinary
return new UnitClause(v.last());
}
if (v.size() == 2) {
// return OriginalBinaryClause.brandNewClause(this.solver,
// getVocabulary(), v);
return createConciseBinaryClause(v);
}
return OriginalWLClause.brandNewClause(this.solver, getVocabulary(), v);
......@@ -102,8 +100,8 @@ public class MixedDataStructureDanielWLConciseBinary
if (binaryClauses == null) {
binaryClauses = new BinaryClauses[getVocabulary().nVars() * 2 + 2];
} else if (binaryClauses.length < getVocabulary().nVars() * 2) {
BinaryClauses[] newBinaryClauses = new BinaryClauses[getVocabulary()
.nVars() * 2 + 2];
var newBinaryClauses = new BinaryClauses[getVocabulary().nVars() * 2
+ 2];
System.arraycopy(binaryClauses, 0, newBinaryClauses, 0,
binaryClauses.length);
binaryClauses = newBinaryClauses;
......
......@@ -96,7 +96,7 @@ public class AtLeast implements Propagatable, Constr, Undoable, Serializable {
throw new ContradictionException();
}
int degree = deg;
for (int i = 0; i < ps.size();) {
for (var i = 0; i < ps.size();) {
// on verifie si le litteral est affecte
if (voc.isUnassigned(ps.get(i))) {
// go to next literal
......@@ -120,7 +120,7 @@ public class AtLeast implements Propagatable, Constr, Undoable, Serializable {
// clause
if (ps.size() == degree) {
for (int i = 0; i < ps.size(); i++) {
for (var i = 0; i < ps.size(); i++) {
if (!s.enqueue(ps.get(i))) {
throw new ContradictionException();
}
......@@ -291,13 +291,13 @@ public class AtLeast implements Propagatable, Constr, Undoable, Serializable {
}
public void assertConstraint(UnitPropagationListener s) {
boolean ret = true;
var ret = true;
for (Integer lit : this.lits) {
if (this.voc.isUnassigned(lit)) {
ret &= s.enqueue(lit, this);
}
}
assert ret == true;
assert ret;
}
public void assertConstraintIfNeeded(UnitPropagationListener s) {
......@@ -311,10 +311,9 @@ public class AtLeast implements Propagatable, Constr, Undoable, Serializable {
*/
@Override
public String toString() {
StringBuilder stb = new StringBuilder();
var stb = new StringBuilder();
stb.append("Card (" + this.lits.length + ") : ");
for (int lit : this.lits) {
// if (voc.isUnassigned(lits[i])) {
for (var lit : this.lits) {
stb.append(" + "); //$NON-NLS-1$
stb.append(Lits.toString(lit));
stb.append("[");
......@@ -333,8 +332,6 @@ public class AtLeast implements Propagatable, Constr, Undoable, Serializable {
* @since 2.1
*/
public void forwardActivity(double claInc) {
// TODO Auto-generated method stub
}
public boolean canBePropagatedMultipleTimes() {
......@@ -399,11 +396,11 @@ public class AtLeast implements Propagatable, Constr, Undoable, Serializable {
}
public int getAssertionLevel(IVecInt trail, int decisionLevel) {
int nUnsat = 0;
Set<Integer> litsSet = new HashSet<Integer>();
var nUnsat = 0;
Set<Integer> litsSet = new HashSet<>();
for (Integer i : this.lits)
litsSet.add(i);
for (int i = 0; i < trail.size(); ++i) {
for (var i = 0; i < trail.size(); ++i) {
if (litsSet.contains(trail.get(i) ^ 1)) {
++nUnsat;
if (nUnsat == this.maxUnsatisfied)
......@@ -414,7 +411,7 @@ public class AtLeast implements Propagatable, Constr, Undoable, Serializable {
}
public String toString(VarMapper mapper) {
StringBuilder stb = new StringBuilder();
var stb = new StringBuilder();
for (int lit : this.lits) {
stb.append(" + "); //$NON-NLS-1$
stb.append(mapper.map(LiteralsUtils.toDimacs(lit)));
......@@ -430,9 +427,9 @@ public class AtLeast implements Propagatable, Constr, Undoable, Serializable {
@Override
public String dump() {
StringBuilder stb = new StringBuilder();
var stb = new StringBuilder();
stb.append(LiteralsUtils.toOPB(this.lits[0]));
int i = 1;
var i = 1;
while (i < this.lits.length) {
stb.append(" + "); //$NON-NLS-1$
stb.append(LiteralsUtils.toOPB(lits[i++]));
......
......@@ -100,12 +100,12 @@ public final class MaxWatchCard
this.moreThan = moreThan;
// Simply ps
int[] index = new int[voc.nVars() * 2 + 2];
for (int i = 0; i < index.length; i++) {
var index = new int[voc.nVars() * 2 + 2];
for (var i = 0; i < index.length; i++) {
index[i] = 0;
}
// Look for opposite literals
for (int i = 0; i < ps.size(); i++) {
for (var i = 0; i < ps.size(); i++) {
if (index[ps.get(i) ^ 1] == 0) {
index[ps.get(i)]++;
} else {
......@@ -113,7 +113,7 @@ public final class MaxWatchCard
}
}
// Update degree according to removed literals
int ind = 0;
var ind = 0;
while (ind < ps.size()) {
if (index[ps.get(ind)] > 0) {
index[ps.get(ind)]--;
......@@ -137,7 +137,7 @@ public final class MaxWatchCard
// Watch all non falsified literals
this.watchCumul = 0;
for (int i = 0; i < this.lits.length; i++) {
for (var i = 0; i < this.lits.length; i++) {
// Note: those falsified literals will never be unset
if (!voc.isFalsified(this.lits[i])) {
this.watchCumul++;
......@@ -170,7 +170,6 @@ public final class MaxWatchCard
* @see Constr#getActivity()
*/
public double getActivity() {
// TODO getActivity
return 0;
}
......@@ -182,7 +181,6 @@ public final class MaxWatchCard
* @see Constr#incActivity(double claInc)
*/
public void incActivity(double claInc) {
// TODO incActivity
}
public void setActivity(double d) {
......@@ -206,7 +204,6 @@ public final class MaxWatchCard
* @see Constr#locked()
*/
public boolean locked() {
// TODO locked
return true;
}
......@@ -237,7 +234,7 @@ public final class MaxWatchCard
throw new ContradictionException(
"Creating trivially inconsistent constraint"); //$NON-NLS-1$
} else if (ps.size() == degree) {
for (int i = 0; i < ps.size(); i++) {
for (var i = 0; i < ps.size(); i++) {
if (!s.enqueue(ps.get(i))) {
throw new ContradictionException(
"Contradiction with implied literal"); //$NON-NLS-1$
......@@ -261,7 +258,7 @@ public final class MaxWatchCard
// Si les litt?raux observ?s sont impliqu?s
if (outclause.watchCumul == outclause.degree) {
for (int i = 0; i < outclause.lits.length; i++) {
for (var i = 0; i < outclause.lits.length; i++) {
if (!s.enqueue(outclause.lits[i])) {
throw new ContradictionException(
"Contradiction with implied literal"); //$NON-NLS-1$
......@@ -282,7 +279,7 @@ public final class MaxWatchCard
// On multiplie le degr? par -1
this.degree = 0 - this.degree;
// On r?vise chaque litt?ral
for (int indLit = 0; indLit < this.lits.length; indLit++) {
for (var indLit = 0; indLit < this.lits.length; indLit++) {
this.lits[indLit] = this.lits[indLit] ^ 1;
this.degree++;
}
......@@ -316,7 +313,7 @@ public final class MaxWatchCard
// Si les litt?raux restant sont impliqu?s
if (this.watchCumul == this.degree) {
for (int q : this.lits) {
for (var q : this.lits) {
if (this.voc.isUnassigned(q) && !s.enqueue(q, this)) {
return false;
}
......@@ -350,10 +347,10 @@ public final class MaxWatchCard
*/
public boolean simplify() {
int i = 0;
var i = 0;
// On esp?re le maximum de la somme
int curr = this.watchCumul;
var curr = this.watchCumul;
// Pour chaque litt?ral
while (i < this.lits.length) {
......@@ -376,14 +373,14 @@ public final class MaxWatchCard
*/
@Override
public String toString() {
StringBuilder stb = new StringBuilder();
var stb = new StringBuilder();
if (this.lits.length > 0) {
if (this.voc.isUnassigned(this.lits[0])) {
stb.append(Lits.toString(this.lits[0]));
stb.append(" "); //$NON-NLS-1$
}
for (int i = 1; i < this.lits.length; i++) {
for (var i = 1; i < this.lits.length; i++) {
if (this.voc.isUnassigned(this.lits[i])) {
stb.append(" + "); //$NON-NLS-1$
stb.append(Lits.toString(this.lits[i]));
......@@ -423,13 +420,13 @@ public final class MaxWatchCard
}
public void assertConstraint(UnitPropagationListener s) {
boolean ret = true;
for (Integer lit : this.lits) {
var ret = true;
for (var lit : this.lits) {
if (this.voc.isUnassigned(lit)) {
ret &= s.enqueue(lit, this);
}
}
assert ret == true;
assert ret;
}
public void assertConstraintIfNeeded(UnitPropagationListener s) {
......@@ -462,8 +459,6 @@ public final class MaxWatchCard
* @since 2.1
*/
public void forwardActivity(double claInc) {
// TODO Auto-generated method stub
}
public boolean canBePropagatedMultipleTimes() {
......@@ -496,11 +491,11 @@ public final class MaxWatchCard
}
public int getAssertionLevel(IVecInt trail, int decisionLevel) {
int nUnsat = 0;
Set<Integer> litsSet = new HashSet<Integer>();
for (Integer i : this.lits)
var nUnsat = 0;
Set<Integer> litsSet = new HashSet<>();
for (var i : this.lits)
litsSet.add(i);
for (int i = 0; i < trail.size(); ++i) {
for (var i = 0; i < trail.size(); ++i) {
if (litsSet.contains(trail.get(i) ^ 1)) {
++nUnsat;
if (nUnsat == this.lits.length - this.degree)
......@@ -511,14 +506,14 @@ public final class MaxWatchCard
}
public String toString(VarMapper mapper) {
StringBuilder stb = new StringBuilder();
var stb = new StringBuilder();
if (this.lits.length > 0) {
if (this.voc.isUnassigned(this.lits[0])) {
stb.append(mapper.map(LiteralsUtils.toDimacs(this.lits[0])));
stb.append(" "); //$NON-NLS-1$
}
for (int i = 1; i < this.lits.length; i++) {
for (var i = 1; i < this.lits.length; i++) {
if (this.voc.isUnassigned(this.lits[i])) {
stb.append(" + "); //$NON-NLS-1$
stb.append(
......@@ -534,9 +529,9 @@ public final class MaxWatchCard
@Override
public String dump() {
StringBuilder stb = new StringBuilder();
var stb = new StringBuilder();
stb.append(LiteralsUtils.toOPB(this.lits[0]));
int i = 1;
var i = 1;
while (i < this.lits.length) {
stb.append(" + "); //$NON-NLS-1$
stb.append(LiteralsUtils.toOPB(lits[i++]));
......
......@@ -108,11 +108,11 @@ public class MinWatchCard
this.moreThan = moreThan;
// On simplifie ps
int[] index = new int[voc.nVars() * 2 + 2];
var index = new int[voc.nVars() * 2 + 2];
// Fresh array should have all elements set to 0
// On repertorie les litt?raux utiles
for (int i = 0; i < ps.size(); i++) {
for (var i = 0; i < ps.size(); i++) {
int p = ps.get(i);
if (index[p ^ 1] == 0) {
index[p]++;
......@@ -121,7 +121,7 @@ public class MinWatchCard
}
}
// On supprime les litt?raux inutiles
int ind = 0;
var ind = 0;
while (ind < ps.size()) {
if (index[ps.get(ind)] > 0) {
index[ps.get(ind)]--;
......@@ -180,8 +180,8 @@ public class MinWatchCard
* @see Constr#calcReason(int p, IVecInt outReason)
*/
public void calcReason(int p, IVecInt outReason) {
int c = p == ILits.UNDEFINED ? -1 : 0;
for (int q : this.lits) {
var c = p == ILits.UNDEFINED ? -1 : 0;
for (var q : this.lits) {
if (this.voc.isFalsified(q)) {
outReason.push(q ^ 1);
if (++c >= this.maxUnsatisfied) {
......@@ -236,9 +236,9 @@ public class MinWatchCard
*/
protected static int linearisation(ILits voc, IVecInt ps) {
// Stockage de l'influence des modifications
int modif = 0;
var modif = 0;
for (int i = 0; i < ps.size();) {
for (var i = 0; i < ps.size();) {
// on verifie si le litteral est affecte
if (voc.isUnassigned(ps.get(i))) {
i++;
......@@ -292,12 +292,12 @@ public class MinWatchCard
IVecInt ps, boolean moreThan, int degree)
throws ContradictionException {
int mydegree = degree + linearisation(voc, ps);
var mydegree = degree + linearisation(voc, ps);
if (ps.size() < mydegree) {
throw new ContradictionException();
} else if (ps.size() == mydegree) {
for (int i = 0; i < ps.size(); i++) {
for (var i = 0; i < ps.size(); i++) {
if (!s.enqueue(ps.get(i))) {
throw new ContradictionException();
}
......@@ -306,7 +306,7 @@ public class MinWatchCard
}
// La contrainte est maintenant cr??e
MinWatchCard retour = new MinWatchCard(voc, ps, moreThan, mydegree);
var retour = new MinWatchCard(voc, ps, moreThan, mydegree);
if (retour.degree <= 0) {
return null;
......@@ -328,7 +328,7 @@ public class MinWatchCard
// On multiplie le degr? par -1
this.degree = 0 - this.degree;
// On r?vise chaque litt?ral
for (int indLit = 0; indLit < this.lits.length; indLit++) {
for (var indLit = 0; indLit < this.lits.length; indLit++) {
this.lits[indLit] = this.lits[indLit] ^ 1;
this.degree++;
}
......@@ -354,14 +354,14 @@ public class MinWatchCard
}
// Recherche du litt?ral falsifi?
int indFalsified = 0;
var indFalsified = 0;
while ((this.lits[indFalsified] ^ 1) != p) {
indFalsified++;
}
assert this.watchCumul > this.degree;
// Recherche du litt?ral swap
int indSwap = this.degree + 1;
var indSwap = this.degree + 1;
while (indSwap < this.lits.length
&& this.voc.isFalsified(this.lits[indSwap])) {
indSwap++;
......@@ -377,7 +377,7 @@ public class MinWatchCard
this.voc.undos(p).push(this);
// On met en queue les litt?raux impliqu?s
for (int i = 0; i <= this.degree; i++) {
for (var i = 0; i <= this.degree; i++) {
if (p != (this.lits[i] ^ 1) && !s.enqueue(this.lits[i], this)) {
return false;
}
......@@ -386,7 +386,7 @@ public class MinWatchCard
return true;
}
// Si un litt?ral a ?t? trouv? on les ?change
int tmpInt = this.lits[indSwap];
var tmpInt = this.lits[indSwap];
this.lits[indSwap] = this.lits[indFalsified];
this.lits[indFalsified] = tmpInt;
......@@ -402,7 +402,7 @@ public class MinWatchCard
* @since 2.1
*/
public void remove(UnitPropagationListener upl) {
for (int i = 0; i < Math.min(this.degree + 1, this.lits.length); i++) {
for (var i = 0; i < Math.min(this.degree + 1, this.lits.length); i++) {
this.voc.watches(this.lits[i] ^ 1).remove(this);
}
}
......@@ -414,7 +414,6 @@ public class MinWatchCard
* rescale factor
*/
public void rescaleBy(double d) {
// TODO rescaleBy
}
/**
......@@ -424,7 +423,7 @@ public class MinWatchCard
*/
public boolean simplify() {
// Calcul de la valeur actuelle
for (int i = 0, count = 0; i < this.lits.length; i++) {
for (var i = 0, count = 0; i < this.lits.length; i++) {
if (this.voc.isSatisfied(this.lits[i]) && ++count == this.degree) {
return true;
}
......@@ -440,29 +439,19 @@ public class MinWatchCard
*/
@Override
public String toString() {
StringBuilder stb = new StringBuilder();
// stb.append("Card (" + this.lits.length + ") : ");
var stb = new StringBuilder();
if (this.lits.length > 0) {
// if (voc.isUnassigned(lits[0])) {
stb.append(Lits.toStringX(this.lits[0]));
stb.append("[");
stb.append(this.voc.valueToString(this.lits[0]));
// stb.append("@");
// stb.append(this.voc.getLevel(this.lits[0]));
stb.append("]");
stb.append(" "); //$NON-NLS-1$
// }
for (int i = 1; i < this.lits.length; i++) {
// if (voc.isUnassigned(lits[i])) {
// stb.append(" + "); //$NON-NLS-1$
stb.append(Lits.toStringX(this.lits[i]));
stb.append("[");
stb.append(this.voc.valueToString(this.lits[i]));
// stb.append("@");
// stb.append(this.voc.getLevel(this.lits[i]));
stb.append("]");
stb.append(" "); //$NON-NLS-1$
// }
}
stb.append(">= "); //$NON-NLS-1$
stb.append(this.degree);
......@@ -498,27 +487,27 @@ public class MinWatchCard