Clover coverage report -
Coverage timestamp: jeu. sept. 29 2005 23:57:39 CEST
file stats: LOC: 133   Methods: 5
NCLOC: 85   Classes: 1
 
 Source file Conditionals Statements Methods TOTAL
LanceurPseudo2005.java 0% 0% 0% 0%
coverage
 1    /*
 2    * Created on 14 mars 2005
 3    *
 4    * TODO To change the template for this generated file go to
 5    * Window - Preferences - Java - Code Style - Code Templates
 6    */
 7    package org.sat4j;
 8   
 9    import static java.lang.System.out;
 10   
 11    import java.math.BigInteger;
 12   
 13    import org.sat4j.minisat.SolverFactory;
 14    import org.sat4j.reader.OPBReader2005;
 15    import org.sat4j.reader.ObjectiveFunction;
 16    import org.sat4j.reader.Reader;
 17    import org.sat4j.specs.ContradictionException;
 18    import org.sat4j.specs.IProblem;
 19    import org.sat4j.specs.ISolver;
 20    import org.sat4j.specs.TimeoutException;
 21   
 22    /**
 23    * Launcher especially dedicated to the pseudo boolean 05 evaluation
 24    * (@link http://www.cril.univ-artois.fr/PB05/).
 25    *
 26    * @author mederic
 27    */
 28    public class LanceurPseudo2005 extends Lanceur {
 29   
 30    /**
 31    * Lance le prouveur sur un fichier Dimacs
 32    *
 33    * @param args
 34    * doit contenir le nom d'un fichier Dimacs, eventuellement
 35    * compress?.
 36    */
 37  0 @Override
 38    public static void main(String[] args) {
 39  0 Lanceur lanceur = new LanceurPseudo2005();
 40  0 lanceur.run(args);
 41    }
 42   
 43    protected int[] bestSolution;
 44   
 45    protected ObjectiveFunction obfct;
 46   
 47  0 @Override
 48    protected void displayResult(ISolver solver, long begintime,
 49    ExitCode exitcode) {
 50  0 if (solver != null) {
 51  0 solver.printStat(System.out, "c ");
 52  0 out.println("s " + exitcode);
 53  0 if (exitcode == ExitCode.SATISFIABLE
 54    || exitcode == ExitCode.OPTIMUM_FOUND) {
 55  0 out.println("v " + reader.decode(bestSolution));
 56  0 if (obfct != null) {
 57  0 System.out.println("c objective function="
 58    + obfct.calculateDegree(bestSolution));
 59    }
 60   
 61    }
 62  0 out.println("c Total CPU time (ms) : "
 63    + (System.currentTimeMillis() - begintime) / 1000.0);
 64    }
 65   
 66    }
 67   
 68    /*
 69    * (non-Javadoc)
 70    *
 71    * @see org.sat4j.Lanceur#createReader(org.sat4j.specs.ISolver)
 72    */
 73  0 @Override
 74    protected Reader createReader(ISolver solver) {
 75  0 return new OPBReader2005(solver);
 76    }
 77   
 78    /*
 79    * (non-Javadoc)
 80    *
 81    * @see org.sat4j.Lanceur#solve()
 82    */
 83  0 @Override
 84    protected void solve(IProblem problem) throws TimeoutException {
 85  0 boolean isSatisfiable = false;
 86  0 obfct = ((OPBReader2005) reader).getObjectiveFunction();
 87   
 88  0 try {
 89  0 while (problem.isSatisfiable()) {
 90  0 if (!isSatisfiable) {
 91  0 exitcode = ExitCode.SATISFIABLE;
 92  0 bestSolution = problem.model();
 93  0 if (obfct == null)
 94  0 return;
 95  0 isSatisfiable = true;
 96  0 System.out.println("c SATISFIABLE");
 97  0 System.out.println("c OPTIMIZING...");
 98    } else {
 99  0 bestSolution = problem.model();
 100    }
 101  0 System.out
 102    .printf(
 103    "c CURRENT OPTIMUM=%20d \t\tCurrent CPU time: %.2f ms\n",
 104    obfct.calculateDegree(bestSolution),
 105    (System.currentTimeMillis() - begintime) / 1000.0);
 106  0 solver.addPseudoBoolean(obfct.getVars(), obfct.getCoeffs(),
 107    false, obfct.calculateDegree(bestSolution).subtract(
 108    BigInteger.ONE));
 109    }
 110  0 if (isSatisfiable) {
 111  0 exitcode = ExitCode.OPTIMUM_FOUND;
 112    } else {
 113  0 exitcode = ExitCode.UNSATISFIABLE;
 114    }
 115    } catch (ContradictionException ex) {
 116    assert isSatisfiable;
 117  0 exitcode = ExitCode.OPTIMUM_FOUND;
 118    }
 119    }
 120   
 121    /*
 122    * (non-Javadoc)
 123    *
 124    * @see org.sat4j.Lanceur#configureSolver(java.lang.String[])
 125    */
 126  0 @Override
 127    protected ISolver configureSolver(String[] args) {
 128  0 ISolver solver = SolverFactory.newMiniOPBMin();
 129  0 solver.setTimeout(Integer.MAX_VALUE);
 130  0 out.println(solver.toString("c "));
 131  0 return solver;
 132    }
 133    }