Commit b9435bf0 authored by Daniel Le Berre's avatar Daniel Le Berre

Fixed a few vulnerabilities, according to Sonar.

parent dbbf6bd0
Pipeline #89 passed with stage
in 11 minutes and 31 seconds
......@@ -31,6 +31,8 @@ package org.sat4j.minisat.core;
import java.io.Serializable;
import java.lang.reflect.Field;
import java.util.logging.Level;
import java.util.logging.Logger;
/**
* Some parameters used during the search.
......@@ -42,6 +44,8 @@ public class SearchParams implements Serializable {
private static final long serialVersionUID = 1L;
private static final Logger LOGGER = Logger.getLogger("org.sat4j.core");
/**
* Default search parameters.
*
......@@ -118,9 +122,12 @@ public class SearchParams implements Serializable {
try {
stb.append(field.get(this));
} catch (IllegalArgumentException e) {
e.printStackTrace();
LOGGER.log(Level.INFO,
"Issue when reflectively accessing field", e);
} catch (IllegalAccessException e) {
e.printStackTrace();
LOGGER.log(Level.INFO,
"Access issue when reflectively accessing field",
e);
}
stb.append(" "); //$NON-NLS-1$
}
......
......@@ -47,6 +47,8 @@ import java.util.Map;
import java.util.Set;
import java.util.Timer;
import java.util.TimerTask;
import java.util.logging.Level;
import java.util.logging.Logger;
import org.sat4j.core.ConstrGroup;
import org.sat4j.core.LiteralsUtils;
......@@ -641,7 +643,6 @@ public class Solver<D extends DataStructureFactory>
this.simplifier.simplify(outLearnt);
Constr c = this.dsfactory.createUnregisteredClause(outLearnt);
// slistener.learn(c);
this.learnedConstraintsDeletionStrategy.onClauseLearning(c);
results.setReason(c);
......@@ -817,7 +818,9 @@ public class Solver<D extends DataStructureFactory>
f = Solver.class.getDeclaredField(simp.toString());
this.simplifier = (ISimplifier) f.get(this);
} catch (Exception e) {
e.printStackTrace();
Logger.getLogger("org.sat4j.core").log(Level.INFO,
"Issue when assigning simplifier: disabling simplification",
e);
this.simplifier = NO_SIMPLIFICATION;
}
}
......@@ -1317,8 +1320,10 @@ public class Solver<D extends DataStructureFactory>
} catch (TimeoutException e) {
return Lbool.UNDEFINED;
}
assert this.analysisResult.getBacktrackLevel() < decisionLevel();
backjumpLevel = Math.max(this.analysisResult.getBacktrackLevel(),
assert this.analysisResult
.getBacktrackLevel() < decisionLevel();
backjumpLevel = Math.max(
this.analysisResult.getBacktrackLevel(),
this.rootLevel);
this.slistener.backjump(backjumpLevel);
cancelUntil(backjumpLevel);
......@@ -1326,7 +1331,8 @@ public class Solver<D extends DataStructureFactory>
this.restarter.onBackjumpToRootLevel();
}
assert decisionLevel() >= this.rootLevel
&& decisionLevel() >= this.analysisResult.getBacktrackLevel();
&& decisionLevel() >= this.analysisResult
.getBacktrackLevel();
if (this.analysisResult.getReason() == null) {
return Lbool.FALSE;
}
......@@ -1381,7 +1387,6 @@ public class Solver<D extends DataStructureFactory>
// clauses
// as decisions to allow blocking models by
// decisions.
// TODO check the impact on implicant computation
|| reason != null && reason.learnt()) {
this.decisions.push(tempmodel.last());
} else {
......
package org.sat4j.pb;
import java.io.PrintWriter;
import java.util.logging.Level;
import java.util.logging.Logger;
import org.sat4j.pb.reader.OPBReader2012;
import org.sat4j.pb.tools.PreprocCardConstrLearningSolver;
......@@ -48,7 +50,6 @@ public class CardConstrLearningSolverLauncher {
try {
reader.parseInstance(instance);
} catch (Exception e) {
e.printStackTrace();
throw new IllegalStateException(e);
}
solver.setVerbose(verbose);
......@@ -89,8 +90,7 @@ public class CardConstrLearningSolverLauncher {
System.out.println("s UNSATISFIABLE");
}
} catch (TimeoutException e) {
// TODO Auto-generated catch block
e.printStackTrace();
Logger.getLogger("org.sat4j.pb").log(Level.INFO, "Timeout", e);
}
}
......
......@@ -31,6 +31,8 @@ package org.sat4j.pb.constraints;
import java.lang.reflect.Field;
import java.math.BigInteger;
import java.util.logging.Level;
import java.util.logging.Logger;
import org.sat4j.core.Vec;
import org.sat4j.core.VecInt;
......@@ -57,8 +59,8 @@ import org.sat4j.specs.IVecInt;
* @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 AbstractPBDataStructureFactory extends
AbstractDataStructureFactory implements PBDataStructureFactory {
public abstract class AbstractPBDataStructureFactory
extends AbstractDataStructureFactory implements PBDataStructureFactory {
interface INormalizer {
PBContainer nice(IVecInt ps, IVec<BigInteger> bigCoefs,
......@@ -154,7 +156,8 @@ public abstract class AbstractPBDataStructureFactory extends
f = AbstractPBDataStructureFactory.class.getDeclaredField(simp);
this.norm = (INormalizer) f.get(this);
} catch (Exception e) {
e.printStackTrace();
Logger.getLogger("org.sat4j.pb").log(Level.INFO,
"Issue when setting normalizer, using competition one", e);
this.norm = FOR_COMPETITION;
}
}
......@@ -164,8 +167,8 @@ public abstract class AbstractPBDataStructureFactory extends
}
/**
*
*/
*
*/
private static final long serialVersionUID = 1L;
public Constr createClause(IVecInt literals) throws ContradictionException {
......
......@@ -38,6 +38,8 @@ import java.util.Iterator;
import java.util.List;
import java.util.Map;
import java.util.Set;
import java.util.logging.Level;
import java.util.logging.Logger;
import org.sat4j.core.Vec;
import org.sat4j.core.VecInt;
......@@ -296,7 +298,8 @@ public class ObjectiveReducerPBSolverDecorator implements IPBSolver {
}
} catch (ContradictionException e) {
// should not occur
e.printStackTrace();
Logger.getLogger("org.sat4j.pb").log(Level.SEVERE,
"Inconsistency found, should not happen", e);
}
newVars.push(newObjVar);
......
......@@ -34,6 +34,8 @@ import java.util.ArrayList;
import java.util.Collection;
import java.util.List;
import java.util.concurrent.Semaphore;
import java.util.logging.Level;
import java.util.logging.Logger;
import org.sat4j.pb.IPBSolver;
import org.sat4j.pb.ObjectiveFunction;
......@@ -59,7 +61,7 @@ public class CriterionOptimumComputer<S extends IPBSolver> {
private final List<ObjectiveFunction> objs = new ArrayList<ObjectiveFunction>();
private BigInteger opts[];
private BigInteger[] opts;
protected Semaphore lock;
......@@ -94,7 +96,6 @@ public class CriterionOptimumComputer<S extends IPBSolver> {
try {
this.lock.acquire();
} catch (InterruptedException e) {
e.printStackTrace();
throw new RuntimeException(e);
}
}
......@@ -126,7 +127,6 @@ public class CriterionOptimumComputer<S extends IPBSolver> {
try {
this.lock.acquire(this.objs.size());
} catch (InterruptedException e) {
e.printStackTrace();
throw new RuntimeException(e);
}
}
......@@ -142,13 +142,13 @@ public class CriterionOptimumComputer<S extends IPBSolver> {
}
public synchronized void onSolutionFound(int[] solution) {
coc.opts[solverIndex] = coc.objs.get(solverIndex).calculateDegree(
coc.solvers.getSolvers().get(solverIndex));
coc.opts[solverIndex] = coc.objs.get(solverIndex)
.calculateDegree(coc.solvers.getSolvers().get(solverIndex));
}
public synchronized void onSolutionFound(IVecInt solution) {
coc.opts[solverIndex] = coc.objs.get(solverIndex).calculateDegree(
coc.solvers.getSolvers().get(solverIndex));
coc.opts[solverIndex] = coc.objs.get(solverIndex)
.calculateDegree(coc.solvers.getSolvers().get(solverIndex));
}
public synchronized void onUnsatTermination() {
......@@ -169,6 +169,7 @@ public class CriterionOptimumComputer<S extends IPBSolver> {
try {
this.solver.isSatisfiable();
} catch (TimeoutException e) {
Logger.getLogger("org.sat4j.pb").log(Level.INFO, "Timeout", e);
timeoutOccured = true;
lock.release();
}
......
......@@ -91,10 +91,8 @@ public class MinSumOWAOptimizer extends AbstractLinMultiObjOptimizer {
addConstraint(objBoundVar, permutation);
}
} catch (Exception e) {
e.printStackTrace();
throw new RuntimeException(e);
}
// setInitConstraintsAux();
}
private void addConstraint(IntegerVariable boundVar,
......@@ -128,8 +126,8 @@ public class MinSumOWAOptimizer extends AbstractLinMultiObjOptimizer {
private BigInteger globalObjBound() {
BigInteger bound = BigInteger.ONE;
for (ObjectiveFunction obj : super.objs) {
for (Iterator<BigInteger> coeffIt = obj.getCoeffs().iterator(); coeffIt
.hasNext();) {
for (Iterator<BigInteger> coeffIt = obj.getCoeffs()
.iterator(); coeffIt.hasNext();) {
bound = bound.add(coeffIt.next());
}
}
......@@ -149,14 +147,14 @@ public class MinSumOWAOptimizer extends AbstractLinMultiObjOptimizer {
super.objectiveValue = BigInteger.ZERO;
BigInteger[] objValues = getObjectiveValues();
for (int i = 0; i < objValues.length; ++i) {
super.objectiveValue = super.objectiveValue.add(objValues[i]
.multiply(this.weights[i]));
super.objectiveValue = super.objectiveValue
.add(objValues[i].multiply(this.weights[i]));
}
return getObjectiveValue();
}
class PermutationComputer implements Iterator<List<Integer>>,
Iterable<List<Integer>> {
class PermutationComputer
implements Iterator<List<Integer>>, Iterable<List<Integer>> {
private int currentElement;
......@@ -183,8 +181,8 @@ public class MinSumOWAOptimizer extends AbstractLinMultiObjOptimizer {
public boolean hasNext() {
return !soleIntegerReturned
&& (this.end == null || this.end.hasNext() || this.currentElement != this.elements
.last());
&& (this.end == null || this.end.hasNext()
|| this.currentElement != this.elements.last());
}
public List<Integer> next() {
......@@ -202,8 +200,8 @@ public class MinSumOWAOptimizer extends AbstractLinMultiObjOptimizer {
}
private void changeCurrentAndChild() {
this.currentElement = this.elements
.tailSet(this.currentElement + 1).first();
this.currentElement = this.elements.tailSet(this.currentElement + 1)
.first();
SortedSet<Integer> endElements = new TreeSet<Integer>();
for (Integer element : this.elements) {
if (!element.equals(currentElement)) {
......@@ -238,126 +236,6 @@ public class MinSumOWAOptimizer extends AbstractLinMultiObjOptimizer {
}
// modif begin
// private ObjectiveFunction sumObj;
// private ObjectiveFunction lexObj;
// private IConstr lexCstr;
// private IConstr sumCstr;
// protected final List<IntegerVariable> objBoundVariables = new
// ArrayList<IntegerVariable>();
// private final List<IVecInt> atLeastFlags = new ArrayList<IVecInt>();
//
// @Override
// public void discardCurrentSolution() throws ContradictionException {
// if (this.sumCstr != null) {
// this.decorated().removeSubsumedConstr(this.sumCstr);
// }
// if (this.lexCstr != null) {
// this.decorated().removeSubsumedConstr(this.lexCstr);
// }
// super.discardCurrentSolution();
// this.lexCstr = decorated().addAtMost(this.lexObj.getVars(),
// this.lexObj.getCoeffs(), maxLexBound());
// this.sumCstr = decorated().addAtMost(this.sumObj.getVars(),
// this.sumObj.getCoeffs(), maxSumBound());
// }
//
// private BigInteger maxSumBound() {
// BigInteger weigthsSum = BigInteger.ZERO;
// for (BigInteger weight : weights)
// weigthsSum = weigthsSum.add(weight);
// BigInteger res = super.objectiveValue.divide(weigthsSum);
// res = res.add(BigInteger.ONE);
// res = res.multiply(BigInteger.valueOf(super.objs.size()));
// return res;
// }
//
// private BigInteger maxLexBound() {
// BigInteger maxObjValue = super.objectiveValue.divide(
// BigInteger.valueOf(super.objs.size())).add(BigInteger.ONE);
// return maxObjValue.multiply(BigInteger.valueOf(
// 1 << objBoundVariables.get(0).getVars().size()).multiply(
// BigInteger.valueOf(super.objs.size() - 1)));
// }
// private void setInitConstraintsAux() {
// String owaWeightsProperty = System.getProperty("_owaWeights");
// if (owaWeightsProperty != null) {
// String[] weights = owaWeightsProperty.split(",");
// for (int i = 0; i < this.weights.length; ++i) {
// this.weights[i] = BigInteger.valueOf(Long.valueOf(weights[i]));
// }
// }
// if (decorated().isVerbose()) {
// System.out.println(getLogPrefix() + "OWA weights : "
// + Arrays.toString(weights));
// }
// BigInteger minObjValuesBound = minObjValuesBound();
// for (int i = 0; i < super.objs.size(); ++i) {
// IntegerVariable boundVar = this.integerSolver
// .newIntegerVar(minObjValuesBound);
// this.objBoundVariables.add(boundVar);
// this.atLeastFlags.add(new VecInt());
// for (int j = 0; j < super.objs.size(); ++j) {
// addBoundConstraint(i, boundVar, j);
// }
// addFlagsCardinalityConstraint(i);
// }
// createSumAndLexObjs();
// }
//
// private void addBoundConstraint(int boundVarIndex,
// IntegerVariable boundVar, int objIndex) {
// IVecInt literals = new VecInt();
// IVec<BigInteger> coeffs = new Vec<BigInteger>();
// super.objs.get(objIndex).getVars().copyTo(literals);
// super.objs.get(objIndex).getCoeffs().copyTo(coeffs);
// int flagLit = decorated().nextFreeVarId(true);
// this.atLeastFlags.get(boundVarIndex).push(flagLit);
// literals.push(flagLit);
// coeffs.push(minObjValuesBound().negate());
// try {
// this.integerSolver.addAtMost(literals, coeffs,
// new Vec<IntegerVariable>().push(boundVar),
// new Vec<BigInteger>().push(BigInteger.ONE.negate()),
// BigInteger.ZERO);
// } catch (ContradictionException e) {
// throw new RuntimeException(e);
// }
// }
// private void createSumAndLexObjs() {
// IVecInt auxObjsVars = new VecInt();
// IVec<BigInteger> sumObjCoeffs = new Vec<BigInteger>();
// IVec<BigInteger> lexObjCoeffs = new Vec<BigInteger>();
// BigInteger lexFactor = BigInteger.ONE;
// for (Iterator<IntegerVariable> intVarIt = objBoundVariables.iterator();
// intVarIt
// .hasNext();) {
// BigInteger sumFactor = BigInteger.ONE;
// IntegerVariable nextBoundVar = intVarIt.next();
// for (IteratorInt nextBoundVarLitsIt = nextBoundVar.getVars()
// .iterator(); nextBoundVarLitsIt.hasNext();) {
// auxObjsVars.push(nextBoundVarLitsIt.next());
// sumObjCoeffs.push(sumFactor);
// sumFactor = sumFactor.shiftLeft(1);
// lexObjCoeffs.push(lexFactor);
// lexFactor = lexFactor.shiftLeft(1);
// }
// }
// this.sumObj = new ObjectiveFunction(auxObjsVars, sumObjCoeffs);
// this.lexObj = new ObjectiveFunction(auxObjsVars, lexObjCoeffs);
// }
//
// private void addFlagsCardinalityConstraint(int card) {
// try {
// decorated().addAtMost(this.atLeastFlags.get(card), card);
// } catch (ContradictionException e) {
// throw new RuntimeException(e);
// }
// }
protected BigInteger minObjValuesBound() {
BigInteger maxValue = BigInteger.ZERO;
for (Iterator<ObjectiveFunction> objsIt = this.objs.iterator(); objsIt
......@@ -374,8 +252,8 @@ public class MinSumOWAOptimizer extends AbstractLinMultiObjOptimizer {
private BigInteger maxObjValue(ObjectiveFunction obj) {
IVec<BigInteger> objCoeffs = obj.getCoeffs();
BigInteger coeffsSum = BigInteger.ZERO;
for (Iterator<BigInteger> objCoeffsIt = objCoeffs.iterator(); objCoeffsIt
.hasNext();) {
for (Iterator<BigInteger> objCoeffsIt = objCoeffs
.iterator(); objCoeffsIt.hasNext();) {
coeffsSum = coeffsSum.add(objCoeffsIt.next());
}
return coeffsSum;
......
......@@ -16,6 +16,8 @@ import java.util.SortedSet;
import java.util.Timer;
import java.util.TimerTask;
import java.util.TreeSet;
import java.util.logging.Level;
import java.util.logging.Logger;
import org.sat4j.core.VecInt;
import org.sat4j.pb.IPBSolver;
......@@ -27,16 +29,13 @@ import org.sat4j.specs.SearchListener;
import org.sat4j.specs.SearchListenerAdapter;
import org.sat4j.specs.TimeoutException;
public class CardConstrFinder implements Iterator<AtLeastCard>,
Iterable<AtLeastCard> {
public class CardConstrFinder
implements Iterator<AtLeastCard>, Iterable<AtLeastCard> {
private final IPBSolver coSolver;
private BitSet propagated = null;
// private final Map<BitSet, BitSet> implied = new HashMap<BitSet,
// BitSet>();
private final SearchListener<ISolverService> oldListener;
private final SortedSet<AtLeastCard> atLeastCards = new TreeSet<AtLeastCard>(
......@@ -91,13 +90,12 @@ public class CardConstrFinder implements Iterator<AtLeastCard>,
if (verbose)
System.out.println("c executing riss subprocess");
try {
Process p = Runtime
.getRuntime()
Process p = Runtime.getRuntime()
.exec(rissLocation
+ " -findCard -card_print -no-card_amt -no-card_amo -no-card_sub -no-card_twoProd -no-card_merge -card_noLim "
+ instance);
BufferedReader reader = new BufferedReader(new InputStreamReader(
p.getErrorStream()));
BufferedReader reader = new BufferedReader(
new InputStreamReader(p.getErrorStream()));
String line;
while ((line = reader.readLine()) != null) {
if (line.startsWith("c "))
......@@ -120,18 +118,20 @@ public class CardConstrFinder implements Iterator<AtLeastCard>,
reader.close();
status = p.waitFor();
if (verbose)
System.out.println("c riss process exited with status "
+ status);
System.out
.println("c riss process exited with status " + status);
} catch (Exception e) {
e.printStackTrace();
Logger.getLogger("org.sat4j.pb").log(Level.INFO,
"Issue when riss subprocess", e);
}
for (Iterator<AtLeastCard> cardIt = this.atLeastCards.iterator(); cardIt
.hasNext();) {
AtLeastCard card = cardIt.next();
BitSet atLeastLits = new BitSet(card.getLits().size());
for (IteratorInt litIt = card.getLits().iterator(); litIt.hasNext();)
atLeastLits.set(litIt.next()
+ this.coSolver.realNumberOfVariables());
for (IteratorInt litIt = card.getLits().iterator(); litIt
.hasNext();)
atLeastLits.set(
litIt.next() + this.coSolver.realNumberOfVariables());
if (cardIsSubsumed(atLeastLits, card.getDegree())) {
cardIt.remove();
}
......@@ -155,8 +155,8 @@ public class CardConstrFinder implements Iterator<AtLeastCard>,
BitSet atLeastLits = new BitSet(atLeastCard.getLits().size());
for (IteratorInt itLits = atLeastCard.getLits().iterator(); itLits
.hasNext();) {
atLeastLits.set(itLits.next()
+ this.coSolver.realNumberOfVariables());
atLeastLits.set(
itLits.next() + this.coSolver.realNumberOfVariables());
}
if (!cardIsSubsumed(atLeastLits, atLeastCard.getDegree())) {
BitSet cardFound = searchCardFromAtLeastCard(atLeastLits,
......@@ -197,7 +197,8 @@ public class CardConstrFinder implements Iterator<AtLeastCard>,
return atMostLits;
}
private BitSet searchCardFromAtLeastCard(BitSet atLeastLits, int threshold) {
private BitSet searchCardFromAtLeastCard(BitSet atLeastLits,
int threshold) {
BitSet atMostLits = new BitSet(atLeastLits.cardinality());
int from = 0;
int cur;
......@@ -215,15 +216,15 @@ public class CardConstrFinder implements Iterator<AtLeastCard>,
return null;
storeAtLeastCard(atLeastLits, atLeastLits.cardinality() - atMostDegree);
if (this.printCards)
System.out.println("c newConstr: "
+ new AtMostCard(atMostLits, atMostDegree, -this.coSolver
.realNumberOfVariables()));
System.out.println("c newConstr: " + new AtMostCard(atMostLits,
atMostDegree, -this.coSolver.realNumberOfVariables()));
return atMostLits;
}
private boolean cardIsSubsumed(BitSet atLeastLits, int threshold) {
List<BitSet> storedCards = this.atLeastCardCache.get(atLeastLits
.nextSetBit(0) - this.coSolver.realNumberOfVariables());
List<BitSet> storedCards = this.atLeastCardCache
.get(atLeastLits.nextSetBit(0)
- this.coSolver.realNumberOfVariables());
if (storedCards == null) {
return false;
}
......@@ -236,8 +237,9 @@ public class CardConstrFinder implements Iterator<AtLeastCard>,
// L>=d dominates L'>=d' iff |L\L'| <= d-d'
BitSet intersection = ((BitSet) storedCard.clone());
intersection.andNot(atLeastLits);
if (intersection.cardinality() <= this.atLeastCardDegree
.get(storedCard) - threshold) {
if (intersection
.cardinality() <= this.atLeastCardDegree.get(storedCard)
- threshold) {
return true;
}
}
......@@ -249,8 +251,8 @@ public class CardConstrFinder implements Iterator<AtLeastCard>,
int from = 0;
int cur;
while ((cur = atLeastLits.nextSetBit(from)) != -1) {
List<BitSet> cardsList = this.atLeastCardCache.get(cur
- this.coSolver.realNumberOfVariables());
List<BitSet> cardsList = this.atLeastCardCache
.get(cur - this.coSolver.realNumberOfVariables());
if (cardsList == null) {
cardsList = new LinkedList<BitSet>();
this.atLeastCardCache.put(
......@@ -297,7 +299,8 @@ public class CardConstrFinder implements Iterator<AtLeastCard>,
int newLitInCard, BitSet candidates) {
if (degree == 1) {
BitSet newLit = new BitSet(1);
newLit.set(2 * this.coSolver.realNumberOfVariables() - newLitInCard);
newLit.set(
2 * this.coSolver.realNumberOfVariables() - newLitInCard);
BitSet implied = impliedBy(newLit);
candidates.and(implied);
} else {
......@@ -316,7 +319,8 @@ public class CardConstrFinder implements Iterator<AtLeastCard>,
private BitSet computeInitialCandidates(BitSet atMostLits, int degree) {
BitSet candidates = null;
CombinationIterator combIt = new CombinationIterator(degree, atMostLits);
CombinationIterator combIt = new CombinationIterator(degree,
atMostLits);
while (combIt.hasNext()) {
BitSet nextBitSet = combIt.nextBitSet();
BitSet implied = impliedBy(nextBitSet);
......@@ -342,8 +346,8 @@ public class CardConstrFinder implements Iterator<AtLeastCard>,
BitSet cached = this.implied.get(lits);
if (cached != null)
return cached;
IVecInt litVec = new VecInt(this.zeroProps.cardinality()
+ lits.cardinality());
IVecInt litVec = new VecInt(
this.zeroProps.cardinality() + lits.cardinality());
int from = 0;
int cur;
while ((cur = lits.nextSetBit(from)) != -1) {
......@@ -374,8 +378,8 @@ public class CardConstrFinder implements Iterator<AtLeastCard>,
this.authorizedExtLits.add(it.next());
}
private class CardConstrFinderListener extends
SearchListenerAdapter<IPBSolverService> {
private class CardConstrFinderListener
extends SearchListenerAdapter<IPBSolverService> {
private static final long serialVersionUID = 1L;
private final CardConstrFinder ccf;
......@@ -416,8 +420,8 @@ public class CardConstrFinder implements Iterator<AtLeastCard>,
cardIt.remove();
}
private static class AtLeastCardDegreeComparator implements
Comparator<AtLeastCard>, Serializable {
private static class AtLeastCardDegreeComparator
implements Comparator<AtLeastCard>, Serializable {
/**
*
......
......@@ -3,6 +3,8 @@ package org.sat4j.pb.tools;
import java.io.FileWriter;
import java.io.IOException;
import java.io.PrintWriter;
import java.util.logging.Level;
import java.util.logging.Logger;
import org.sat4j.pb.IPBSolver;
import org.sat4j.pb.OPBStringSolver;
......@@ -20,6 +22,8 @@ import org.sat4j.specs.ContradictionException;
*/
public class DimacsToOpb {
private static final Logger LOGGER = Logger.getLogger("org.sat4j.pb");
public static void main(String[] args) {
if (args.length != 1) {
System.out.println("Usage : dimacs2opb filename.cnf");
......@@ -37,14 +41,11 @@ public class DimacsToOpb {
out.close();
} catch (ParseFormatException e) {
// TODO Auto-generated catch block
e.printStackTrace();
LOGGER.log(Level.INFO, "Input format error", e);
} catch (IOException e) {
// TODO Auto-generated catch block
e.printStackTrace();
LOGGER.log(Level.INFO, "Input error", e);
} catch (ContradictionException e) {
// TODO Auto-generated catch block
e.printStackTrace();
LOGGER.log(Level.INFO, "Formula is UNSAT", e);
}
}
......
......@@ -3,6 +3,8 @@ package org.sat4j.pb.tools;
import java.io.FileWriter;
import java.io.IOException;
import java.io.PrintWriter;
import java.util.logging.Level;
import java.util.logging.Logger;
import org.sat4j.pb.IPBSolver;
import org.sat4j.pb.reader.PBInstanceReader;
......@@ -20,6 +22,8 @@ import org.sat4j.tools.DimacsStringSolver;
*/
public class OpbToDimacs {
private static final Logger LOGGER = Logger.getLogger("org.sat4j.pb");
public static void main(String[] args) {
if (args.length != 1) {
System.out.println("Usage : opb2dimacs filename.opb");
......@@ -37,14 +41,11 @@ public class OpbToDimacs {
out.close();
} catch (ParseFormatException e) {
// TODO Auto-generated catch block
e.printStackTrace();
LOGGER.log(Level.INFO, "Input format error", e);
} catch (IOException e) {
// TODO Auto-generated catch block
e.printStackTrace();
LOGGER.log(Level.INFO, "Input error", e);
} catch (ContradictionException e) {
// TODO Auto-generated catch block
e.printStackTrace();
LOGGER.log(Level.INFO, "Formula is UNSAT", e);
}
}
......