Skip to content

Commit

Permalink
Use isEmpty methods
Browse files Browse the repository at this point in the history
  • Loading branch information
@czengler
czengler committed Sep 17, 2024
1 parent 52b2070 commit 2fbf7fc
Show file tree
Hide file tree
Showing 21 changed files with 71 additions and 71 deletions.
4 changes: 2 additions & 2 deletions core/src/main/java/com/booleworks/logicng/encodings/CcIncrementalData.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -162,7 +162,7 @@ private void computeUbConstraint(final EncodingResult result, final int rhs) {
}
switch (amkEncoder) {
case MODULAR_TOTALIZER:
assert vector1.size() != 0 || vector2.size() != 0;
assert !vector1.isEmpty() || !vector2.isEmpty();
final int ulimit = (rhs + 1) / mod;
final int llimit = (rhs + 1) - ulimit * mod;
assert ulimit <= vector1.size();
Expand Down Expand Up @@ -241,7 +241,7 @@ private void computeLbConstraint(final EncodingResult result, final int rhs) {
break;
case MODULAR_TOTALIZER:
int newRhs = nVars - rhs;
assert vector1.size() != 0 || vector2.size() != 0;
assert !vector1.isEmpty() || !vector2.isEmpty();
final int ulimit = (newRhs + 1) / mod;
final int llimit = (newRhs + 1) - ulimit * mod;
assert ulimit <= vector1.size();
Expand Down
4 changes: 2 additions & 2 deletions core/src/main/java/com/booleworks/logicng/encodings/cc/CcAmo.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -188,7 +188,7 @@ private static void commanderRec(final EncodingResult result, final int groupSiz
pure(result, literals);
literals.push(result.newCcVariable());
nextLiterals.push(literals.back().negate(f));
if (isExactlyOne && literals.size() > 0) {
if (isExactlyOne && !literals.isEmpty()) {
result.addClause(literals);
}
for (int j = 0; j < literals.size() - 1; j++) {
Expand All @@ -201,7 +201,7 @@ private static void commanderRec(final EncodingResult result, final int groupSiz
isExactlyOne = true;
}
pure(result, currentLiterals);
if (isExactlyOne && currentLiterals.size() > 0) {
if (isExactlyOne && !currentLiterals.isEmpty()) {
result.addClause(currentLiterals);
}
}
Expand Down
16 changes: 8 additions & 8 deletions core/src/main/java/com/booleworks/logicng/encodings/cc/CcModularTotalizer.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -55,7 +55,7 @@ public static CcIncrementalData amk(final EncodingResult result, final Variable[
state.inlits.push(var);
}
toCnf(result, mod, state.cardinalityUpOutvars, state.cardinalityLwOutvars, vars.length, state);
assert state.inlits.size() == 0;
assert state.inlits.isEmpty();
encodeOutput(result, rhs, mod, state);
state.currentCardinalityRhs = rhs + 1;
return new CcIncrementalData(result, EncoderConfig.AmkEncoder.MODULAR_TOTALIZER, rhs,
Expand Down Expand Up @@ -98,14 +98,14 @@ private static int initialize(final EncodingResult result, final int rhs, final
}
state.inlits = new LngVector<>(n);
state.currentCardinalityRhs = rhs + 1;
if (state.cardinalityUpOutvars.size() == 0) {
if (state.cardinalityUpOutvars.isEmpty()) {
state.cardinalityUpOutvars.push(state.h0);
}
return mod;
}

private static void encodeOutput(final EncodingResult result, final int rhs, final int mod, final State state) {
assert state.cardinalityUpOutvars.size() != 0 || state.cardinalityLwOutvars.size() != 0;
assert !state.cardinalityUpOutvars.isEmpty() || !state.cardinalityLwOutvars.isEmpty();
final FormulaFactory f = result.getFactory();
final int ulimit = (rhs + 1) / mod;
final int llimit = (rhs + 1) - ulimit * mod;
Expand Down Expand Up @@ -143,7 +143,7 @@ private static void toCnf(final EncodingResult result, final int mod, final LngV
int left = 1;
int right = 1;
if (split == 1) {
assert state.inlits.size() > 0;
assert !state.inlits.isEmpty();
lupper.push(state.h0);
llower.push(state.inlits.back());
state.inlits.pop();
Expand All @@ -161,7 +161,7 @@ private static void toCnf(final EncodingResult result, final int mod, final LngV
}
}
if (rhs - split == 1) {
assert state.inlits.size() > 0;
assert !state.inlits.isEmpty();
rupper.push(state.h0);
rlower.push(state.inlits.back());
state.inlits.pop();
Expand All @@ -178,10 +178,10 @@ private static void toCnf(final EncodingResult result, final int mod, final LngV
rlower.push(result.newCcVariable());
}
}
if (lupper.size() == 0) {
if (lupper.isEmpty()) {
lupper.push(state.h0);
}
if (rupper.size() == 0) {
if (rupper.isEmpty()) {
rupper.push(state.h0);
}
adder(result, mod, ubvars, lwvars, rupper, rlower, lupper, llower, state);
Expand All @@ -200,7 +200,7 @@ private static void adder(final EncodingResult result, final int mod, final LngV
final LngVector<Literal> lupper, final LngVector<Literal> llower,
final LngVector<Literal> rupper,
final LngVector<Literal> rlower, final State state) {
assert upper.size() != 0;
assert !upper.isEmpty();
assert lower.size() >= llower.size() && lower.size() >= rlower.size();
final FormulaFactory f = result.getFactory();
Variable carry = state.varUndef;
Expand Down
10 changes: 5 additions & 5 deletions core/src/main/java/com/booleworks/logicng/encodings/cc/CcSorting.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -156,7 +156,7 @@ private static void recursiveSorter(final FormulaFactory f, final int m, final i
final LngVector<Literal> input, final EncodingResult result,
final LngVector<Literal> output, final ImplicationDirection direction) {
final int n = input.size();
assert output.size() == 0;
assert output.isEmpty();
assert n > 1;
assert m <= n;
final LngVector<Literal> tmpLitsA = new LngVector<>();
Expand Down Expand Up @@ -186,7 +186,7 @@ private static void recursiveSorter(final FormulaFactory f, final int m, final L
final EncodingResult result,
final LngVector<Literal> output, final ImplicationDirection direction) {
assert m > 0;
assert input.size() > 0;
assert !input.isEmpty();
output.clear();
final int n = input.size();
assert n > 1;
Expand Down Expand Up @@ -308,8 +308,8 @@ private static void recursiveMerger(final FormulaFactory f, final int c, final L
final int a, final LngVector<Literal> inputB, final int b,
final EncodingResult formula, final LngVector<Literal> output,
final ImplicationDirection direction) {
assert inputA.size() > 0;
assert inputB.size() > 0;
assert !inputA.isEmpty();
assert !inputB.isEmpty();
assert c > 0;
output.clear();
int a2 = a;
Expand Down Expand Up @@ -358,7 +358,7 @@ private static void recursiveMerger(final FormulaFactory f, final int c, final L
merge(f, c / 2 + 1, tmpLitsOddA, tmpLitsOddB, formula, oddMerge, direction);
merge(f, c / 2, tmpLitsEvenA, tmpLitsEvenB, formula, evenMerge, direction);

assert oddMerge.size() > 0;
assert !oddMerge.isEmpty();

output.push(oddMerge.get(0));

Expand Down
10 changes: 5 additions & 5 deletions core/src/main/java/com/booleworks/logicng/encodings/cc/CcTotalizer.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -58,7 +58,7 @@ private CcTotalizer() {
public static CcIncrementalData amk(final EncodingResult result, final Variable[] vars, final int rhs) {
final TotalizerVars tv = initializeConstraint(result, vars);
toCnf(result, tv, rhs, Bound.UPPER);
assert tv.invars.size() == 0;
assert tv.invars.isEmpty();
for (int i = rhs; i < tv.outvars.size(); i++) {
result.addClause(tv.outvars.get(i).negate(result.getFactory()));
}
Expand All @@ -77,7 +77,7 @@ public static CcIncrementalData amk(final EncodingResult result, final Variable[
public static CcIncrementalData alk(final EncodingResult result, final Variable[] vars, final int rhs) {
final TotalizerVars tv = initializeConstraint(result, vars);
toCnf(result, tv, rhs, Bound.LOWER);
assert tv.invars.size() == 0;
assert tv.invars.isEmpty();
for (int i = 0; i < rhs; i++) {
result.addClause(tv.outvars.get(i));
}
Expand All @@ -95,7 +95,7 @@ public static CcIncrementalData alk(final EncodingResult result, final Variable[
public static void exk(final EncodingResult result, final Variable[] vars, final int rhs) {
final TotalizerVars tv = initializeConstraint(result, vars);
toCnf(result, tv, rhs, Bound.BOTH);
assert tv.invars.size() == 0;
assert tv.invars.isEmpty();
for (int i = 0; i < rhs; i++) {
result.addClause(tv.outvars.get(i));
}
Expand All @@ -121,15 +121,15 @@ private static void toCnf(final EncodingResult result, final TotalizerVars tv, f
for (int i = 0; i < tv.outvars.size(); i++) {
if (i < split) {
if (split == 1) {
assert tv.invars.size() > 0;
assert !tv.invars.isEmpty();
left.push(tv.invars.back());
tv.invars.pop();
} else {
left.push(result.newCcVariable());
}
} else {
if (tv.outvars.size() - split == 1) {
assert tv.invars.size() > 0;
assert !tv.invars.isEmpty();
right.push(tv.invars.back());
tv.invars.pop();
} else {
Expand Down
2 changes: 1 addition & 1 deletion core/src/main/java/com/booleworks/logicng/formulas/PbConstraint.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -274,7 +274,7 @@ private Formula normalize(final FormulaFactory f, final LngVector<Literal> ps, f
if (sum <= c) {
return f.verum();
}
assert cs.size() > 0;
assert !cs.isEmpty();
int div = c;
for (int i = 0; i < cs.size(); i++) {
div = gcd(div, cs.get(i));
Expand Down
2 changes: 1 addition & 1 deletion core/src/main/java/com/booleworks/logicng/solvers/datastructures/LngHeap.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -94,7 +94,7 @@ public int size() {
* @return {@code true} if the heap ist empty
*/
public boolean empty() {
return heap.size() == 0;
return heap.isEmpty();
}

/**
Expand Down
10 changes: 5 additions & 5 deletions core/src/main/java/com/booleworks/logicng/solvers/maxsat/algorithms/IncWbo.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -141,7 +141,7 @@ protected void incrementalBuildWeightSolver(final MaxSatConfig.WeightStrategy st
}

protected void relaxCore(final LngIntVector conflict, final int weightCore) {
assert conflict.size() > 0;
assert !conflict.isEmpty();
assert weightCore > 0;
final LngIntVector lits = new LngIntVector();
for (int i = 0; i < conflict.size(); i++) {
Expand Down Expand Up @@ -237,7 +237,7 @@ protected void relaxCore(final LngIntVector conflict, final int weightCore) {

@Override
protected void symmetryBreaking() {
if (indexSoftCore.size() != 0 && nbSymmetryClauses < symmetryBreakingLimit) {
if (!indexSoftCore.isEmpty() && nbSymmetryClauses < symmetryBreakingLimit) {
final LngIntVector[] coreIntersection = new LngIntVector[nbCores];
final LngIntVector[] coreIntersectionCurrent = new LngIntVector[nbCores];
for (int i = 0; i < nbCores; i++) {
Expand All @@ -251,7 +251,7 @@ protected void symmetryBreaking() {
for (int j = 0; j < softMapping.get(p).size() - 1; j++) {
final int core = softMapping.get(p).get(j);
addCores.push(core);
if (coreIntersection[core].size() == 0) {
if (coreIntersection[core].isEmpty()) {
coreList.push(core);
}
assert j < relaxationMapping.get(p).size();
Expand Down Expand Up @@ -331,7 +331,7 @@ protected LngResult<MaxSatResult> weightSearch(final ComputationHandler handler)
return LngResult.canceled(res.getCancelCause());
} else if (!res.getResult()) {
nbCores++;
assert solver.assumptionsConflict().size() > 0;
assert !solver.assumptionsConflict().isEmpty();
final int coreCost = computeCostCore(solver.assumptionsConflict());
lbCost += coreCost;
if (verbosity != MaxSatConfig.Verbosity.NONE) {
Expand Down Expand Up @@ -433,7 +433,7 @@ protected LngResult<MaxSatResult> normalSearch(final ComputationHandler handler)
return LngResult.canceled(res.getCancelCause());
} else if (!res.getResult()) {
nbCores++;
assert solver.assumptionsConflict().size() > 0;
assert !solver.assumptionsConflict().isEmpty();
final int coreCost = computeCostCore(solver.assumptionsConflict());
lbCost += coreCost;
if (verbosity != MaxSatConfig.Verbosity.NONE) {
Expand Down
6 changes: 3 additions & 3 deletions core/src/main/java/com/booleworks/logicng/solvers/maxsat/algorithms/LinearSu.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -98,7 +98,7 @@ protected LngResult<MaxSatResult> internalSearch(final ComputationHandler handle
}

protected LngResult<MaxSatResult> bmoSearch(final ComputationHandler handler) {
assert orderWeights.size() > 0;
assert !orderWeights.isEmpty();
initRelaxation();
int currentWeight = orderWeights.get(0);
final int minWeight = orderWeights.get(orderWeights.size() - 1);
Expand Down Expand Up @@ -156,7 +156,7 @@ protected LngResult<MaxSatResult> bmoSearch(final ComputationHandler handler) {
} else {
nbCores++;
if (currentWeight == minWeight) {
if (model.size() == 0) {
if (model.isEmpty()) {
assert nbSatisfiable == 0;
return unsat();
} else {
Expand Down Expand Up @@ -221,7 +221,7 @@ protected LngResult<MaxSatResult> normalSearch(final ComputationHandler handler)
}
} else {
nbCores++;
if (model.size() == 0) {
if (model.isEmpty()) {
assert nbSatisfiable == 0;
return unsat();
} else {
Expand Down
4 changes: 2 additions & 2 deletions core/src/main/java/com/booleworks/logicng/solvers/maxsat/algorithms/MaxSat.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -468,7 +468,7 @@ public int computeCostModel(final LngBooleanVector currentModel, final int weigh
* criterion
*/
public boolean isBmo(final boolean cache) {
assert orderWeights.size() == 0;
assert orderWeights.isEmpty();
boolean bmo = true;
final SortedSet<Integer> partitionWeights = new TreeSet<>();
final SortedMap<Integer, Integer> nbPartitionWeights = new TreeMap<>();
Expand Down Expand Up @@ -562,7 +562,7 @@ public class Stats {
protected final int nbSc;

protected Stats() {
ubC = model.size() == 0 ? -1 : ubCost;
ubC = model.isEmpty() ? -1 : ubCost;
nbS = nbSatisfiable;
nbC = nbCores;
avgCs = nbCores != 0 ? (double) sumSizeCores / nbCores : 0.0;
Expand Down
2 changes: 1 addition & 1 deletion core/src/main/java/com/booleworks/logicng/solvers/maxsat/algorithms/Msu3.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -231,7 +231,7 @@ protected LngResult<MaxSatResult> iterative(final ComputationHandler handler) {
return optimum();
}
sumSizeCores += solver.assumptionsConflict().size();
if (solver.assumptionsConflict().size() == 0) {
if (solver.assumptionsConflict().isEmpty()) {
return unsat();
}
final LngEvent lowerBoundEvent = foundLowerBound(lbCost, handler);
Expand Down
4 changes: 2 additions & 2 deletions core/src/main/java/com/booleworks/logicng/solvers/maxsat/algorithms/Oll.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -178,7 +178,7 @@ private LngResult<MaxSatResult> unweighted(final ComputationHandler handler) {
}

assert softRelax.size() + cardinalityRelax.size() > 0;
if (softRelax.size() == 1 && cardinalityRelax.size() == 0) {
if (softRelax.size() == 1 && cardinalityRelax.isEmpty()) {
solver.addClause(softRelax.get(0), null);
}

Expand Down Expand Up @@ -430,7 +430,7 @@ private LngResult<MaxSatResult> weighted(final ComputationHandler handler) {
}
}
assert softRelax.size() + cardinalityRelax.size() > 0;
if (softRelax.size() == 1 && cardinalityRelax.size() == 0) {
if (softRelax.size() == 1 && cardinalityRelax.isEmpty()) {
solver.addClause(softRelax.get(0), null);
}
if (softRelax.size() + cardinalityRelax.size() > 1) {
Expand Down
16 changes: 8 additions & 8 deletions core/src/main/java/com/booleworks/logicng/solvers/maxsat/algorithms/Wbo.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -235,7 +235,7 @@ protected int findNextWeightDiversity(final int weight) {
}

protected void encodeEo(final LngIntVector lits) {
assert lits.size() != 0;
assert !lits.isEmpty();
final LngIntVector clause = new LngIntVector();
if (lits.size() == 1) {
clause.push(lits.get(0));
Expand Down Expand Up @@ -288,7 +288,7 @@ protected void encodeEo(final LngIntVector lits) {
}

protected void relaxCore(final LngIntVector conflict, final int weightCore, final LngIntVector assumps) {
assert conflict.size() > 0;
assert !conflict.isEmpty();
assert weightCore > 0;
final LngIntVector lits = new LngIntVector();
for (int i = 0; i < conflict.size(); i++) {
Expand Down Expand Up @@ -326,7 +326,7 @@ protected void relaxCore(final LngIntVector conflict, final int weightCore, fina
}

int computeCostCore(final LngIntVector conflict) {
assert conflict.size() != 0;
assert !conflict.isEmpty();
if (problemType == ProblemType.UNWEIGHTED) {
return 1;
}
Expand Down Expand Up @@ -362,7 +362,7 @@ void symmetryLog(final int p) {
}

protected void symmetryBreaking() {
if (indexSoftCore.size() != 0 && nbSymmetryClauses < symmetryBreakingLimit) {
if (!indexSoftCore.isEmpty() && nbSymmetryClauses < symmetryBreakingLimit) {
final LngIntVector[] coreIntersection = new LngIntVector[nbCores];
final LngIntVector[] coreIntersectionCurrent = new LngIntVector[nbCores];
for (int i = 0; i < nbCores; i++) {
Expand All @@ -376,7 +376,7 @@ protected void symmetryBreaking() {
for (int j = 0; j < softMapping.get(p).size() - 1; j++) {
final int core = softMapping.get(p).get(j);
addCores.push(core);
if (coreIntersection[core].size() == 0) {
if (coreIntersection[core].isEmpty()) {
coreList.push(core);
}
assert j < relaxationMapping.get(p).size();
Expand Down Expand Up @@ -431,7 +431,7 @@ protected void symmetryBreaking() {
}

LngResult<Boolean> unsatSearch(final ComputationHandler handler) {
assert assumptions.size() == 0;
assert assumptions.isEmpty();
solver = rebuildHardSolver();
final LngResult<Boolean> res = searchSatSolver(solver, handler, assumptions);
if (!res.isSuccess()) {
Expand Down Expand Up @@ -469,7 +469,7 @@ protected LngResult<MaxSatResult> weightSearch(final ComputationHandler handler)
return LngResult.canceled(res.getCancelCause());
} else if (!res.getResult()) {
nbCores++;
assert solver.assumptionsConflict().size() > 0;
assert !solver.assumptionsConflict().isEmpty();
final int coreCost = computeCostCore(solver.assumptionsConflict());
lbCost += coreCost;
if (verbosity != Verbosity.NONE) {
Expand Down Expand Up @@ -538,7 +538,7 @@ protected LngResult<MaxSatResult> normalSearch(final ComputationHandler handler)
return LngResult.canceled(res.getCancelCause());
} else if (!res.getResult()) {
nbCores++;
assert solver.assumptionsConflict().size() > 0;
assert !solver.assumptionsConflict().isEmpty();
final int coreCost = computeCostCore(solver.assumptionsConflict());
lbCost += coreCost;
if (verbosity != Verbosity.NONE) {
Expand Down
Loading

0 comments on commit 2fbf7fc

Please sign in to comment.