Clover coverage report -
Coverage timestamp: jeu. sept. 29 2005 23:57:39 CEST
Overview   Package   File
    FRAMES   NO FRAMES  
file stats: LOC: 318   Methods: 16
NCLOC: 175   Classes: 2
 
 Source file Conditionals Statements Methods TOTAL
Lanceur.java 0% 0% 0% 0%
coverage
 1    /*
 2    * SAT4J: a SATisfiability library for Java
 3    * Copyright (C) 2004 Daniel Le Berre
 4    *
 5    * Based on the original minisat specification from:
 6    *
 7    * An extensible SAT solver. Niklas E?n and Niklas S?rensson.
 8    * Proceedings of the Sixth International Conference on Theory
 9    * and Applications of Satisfiability Testing, LNCS 2919,
 10    * pp 502-518, 2003.
 11    *
 12    * This library is free software; you can redistribute it and/or
 13    * modify it under the terms of the GNU Lesser General Public
 14    * License as published by the Free Software Foundation; either
 15    * version 2.1 of the License, or (at your option) any later version.
 16    *
 17    * This library is distributed in the hope that it will be useful,
 18    * but WITHOUT ANY WARRANTY; without even the implied warranty of
 19    * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU
 20    * Lesser General Public License for more details.
 21    *
 22    * You should have received a copy of the GNU Lesser General Public
 23    * License along with this library; if not, write to the Free Software
 24    * Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA
 25    *
 26    */
 27   
 28    package org.sat4j;
 29   
 30    import static java.lang.System.exit;
 31    import static java.lang.System.out;
 32   
 33    import java.io.BufferedReader;
 34    import java.io.FileNotFoundException;
 35    import java.io.IOException;
 36    import java.io.InputStreamReader;
 37    import java.net.URL;
 38   
 39    import org.apache.commons.beanutils.BeanUtils;
 40    import org.sat4j.core.ASolverFactory;
 41    import org.sat4j.reader.InstanceReader;
 42    import org.sat4j.reader.ParseFormatException;
 43    import org.sat4j.reader.Reader;
 44    import org.sat4j.specs.ContradictionException;
 45    import org.sat4j.specs.IProblem;
 46    import org.sat4j.specs.ISolver;
 47    import org.sat4j.specs.TimeoutException;
 48   
 49    /**
 50    * This class is used to launch the SAT solvers from the command line.
 51    *
 52    * It is compliant with the SAT competition (www.satcompetition.org) I/O format.
 53    * The launcher is to be used as follows:
 54    *
 55    * <pre>
 56    * [solvername] finalname [key=value]*
 57    * </pre>
 58    *
 59    * If no solver name is given, then the default solver of the solver factory is
 60    * used (@see org.sat4j.core.ASolverFactory#defaultSolver()).
 61    *
 62    * @author leberre
 63    */
 64    public class Lanceur {
 65   
 66    /**
 67    * Enumeration allowing to manage easily exit code for the SAT and PB
 68    * Competitions.
 69    *
 70    * @author leberre
 71    *
 72    */
 73    public enum ExitCode {
 74    OPTIMUM_FOUND(30, "OPTIMUM FOUND"), SATISFIABLE(10), UNKNOWN(0), UNSATISFIABLE(
 75    20);
 76   
 77    /** value of the exit code. */
 78    private final int value;
 79   
 80    /** alternative textual representation of the exit code. */
 81    private final String str;
 82   
 83    /**
 84    * creates an exit code with a given value.
 85    *
 86    * @param i
 87    * the value of the exit code
 88    */
 89  0 ExitCode(final int i) {
 90  0 this.value = i;
 91  0 str = null;
 92    }
 93   
 94    /**
 95    * creates an exit code with a given value and an alternative textual
 96    * representation.
 97    *
 98    * @param i
 99    * the value of the exit code
 100    * @param str
 101    * the alternative textual representation
 102    */
 103  0 ExitCode(final int i, final String str) {
 104  0 this.value = i;
 105  0 this.str = str;
 106    }
 107   
 108    /**
 109    * @return the exit code value
 110    */
 111  0 public int value() {
 112  0 return value;
 113    }
 114   
 115    /**
 116    * @return the name of the enum or the alternative textual
 117    * representation if any.
 118    */
 119  0 @Override
 120    public String toString() {
 121  0 if (str != null) {
 122  0 return str;
 123    }
 124  0 return super.toString();
 125    }
 126    }
 127   
 128    /**
 129    * Lance le prouveur sur un fichier Dimacs.
 130    *
 131    * @param args
 132    * doit contenir le nom d'un fichier Dimacs, eventuellement
 133    * compress?.
 134    */
 135  0 public static void main(final String[] args) {
 136  0 Lanceur lanceur = new Lanceur();
 137  0 lanceur.run(args);
 138    }
 139   
 140    protected long begintime;
 141   
 142    protected ExitCode exitcode = ExitCode.UNKNOWN;
 143   
 144    protected ASolverFactory factory;
 145   
 146    protected Reader reader;
 147   
 148    protected int argindex = 0;
 149   
 150    private Thread shutdownHook = new Thread() {
 151  0 @Override
 152    public void run() {
 153  0 displayResult(solver, begintime, exitcode);
 154    }
 155    };
 156   
 157    protected ISolver solver;
 158   
 159  0 Lanceur() {
 160  0 Runtime.getRuntime().addShutdownHook(shutdownHook);
 161    }
 162   
 163    /**
 164    * @param args
 165    * @return
 166    */
 167  0 protected ISolver configureSolver(String[] args) {
 168  0 factory = new org.sat4j.minisat.SolverFactory();
 169   
 170  0 if (args.length < 1) {
 171  0 usage();
 172  0 exit(-1);
 173    }
 174   
 175  0 ISolver asolver;
 176  0 if (args.length == argindex + 1) {
 177  0 asolver = factory.defaultSolver();
 178    } else {
 179  0 asolver = factory.createSolverByName(args[argindex++]);
 180    // use remaining data to configure the solver
 181  0 int others = argindex + 1;
 182  0 while (args.length > others) {
 183  0 String[] param = args[others].split("=");
 184    assert param.length == 2;
 185  0 System.out.println("c setting " + param[0] + " to " + param[1]);
 186  0 try {
 187  0 BeanUtils.setProperty(asolver, param[0], param[1]);
 188    } catch (Exception e) {
 189  0 System.out.println("c Cannot set parameter : "
 190    + args[others]);
 191    }
 192  0 others++;
 193    }
 194    }
 195  0 out.println(asolver.toString("c "));
 196  0 out.println("c timeout: " + asolver.getTimeout() + "s");
 197  0 return asolver;
 198    }
 199   
 200  0 private void usage() {
 201  0 out
 202    .println("Usage: java -jar sat4j.jar [<solver>] <cnffile> [<timeout>]");
 203  0 showAvailableSolvers();
 204    }
 205   
 206  0 protected Reader createReader(ISolver solver) {
 207  0 return new InstanceReader(solver);
 208    }
 209   
 210    /**
 211    * @throws IOException
 212    */
 213  0 private void displayHeader() throws IOException {
 214  0 out
 215    .println("c SAT4J: a SATisfiability library for Java (c) 2004-2005 Daniel Le Berre");
 216  0 out
 217    .println("c This is free software under the GNU LGPL licence. See www.sat4j.org for details.");
 218  0 URL url = Lanceur.class.getResource("/sat4j.version");
 219  0 if (url != null) {
 220  0 BufferedReader in = new BufferedReader(new InputStreamReader(url
 221    .openStream()));
 222  0 out.println("c version " + in.readLine());
 223  0 in.close();
 224    } else {
 225  0 out.println("c no version file found!!!");
 226    }
 227    }
 228   
 229    /**
 230    * @param solver
 231    * @param begintime
 232    * @param isSat
 233    */
 234  0 protected void displayResult(final ISolver solver, final long begintime,
 235    final ExitCode exitcode) {
 236  0 if (solver != null) {
 237  0 double cputime = (System.currentTimeMillis() - begintime) / 1000.0;
 238  0 solver.printStat(System.out, "c ");
 239  0 out.println("s " + exitcode);
 240  0 if (exitcode == ExitCode.SATISFIABLE) {
 241  0 int[] model = solver.model();
 242  0 out.println("v " + reader.decode(model));
 243    }
 244  0 out.println("c Total CPU time (ms) : " + cputime);
 245    }
 246    }
 247   
 248    /**
 249    * Reads a problem file from the command line.
 250    *
 251    * @param args command line arguments
 252    * @param solver the solver to feed
 253    * @param begintime program begin time
 254    * @return a reference to the problem to solve
 255    * @throws FileNotFoundException if the file is not found
 256    * @throws ParseFormatException if the problem is not expressed using the
 257    * right format
 258    * @throws IOException for other IO problems
 259    * @throws ContradictionException if the problem is found trivially unsat
 260    */
 261  0 private IProblem readProblem(String[] args, ISolver solver, long begintime)
 262    throws FileNotFoundException, ParseFormatException, IOException,
 263    ContradictionException {
 264  0 out.println("c solving " + args[argindex]);
 265  0 out.println("c reading problem ... ");
 266  0 reader = createReader(solver);
 267  0 IProblem problem = reader.parseInstance(args[argindex]);
 268  0 out.println("c ... done. Time "
 269    + (System.currentTimeMillis() - begintime) / 1000.0 + " ms.");
 270  0 out.println("c #vars " + solver.nVars());
 271  0 out.println("c #constraints " + solver.nConstraints());
 272  0 return problem;
 273    }
 274   
 275  0 public void run(String[] args) {
 276   
 277  0 try {
 278  0 displayHeader();
 279   
 280  0 solver = configureSolver(args);
 281   
 282  0 begintime = System.currentTimeMillis();
 283   
 284  0 IProblem problem = readProblem(args, solver, begintime);
 285   
 286  0 try {
 287  0 solve(problem);
 288    } catch (TimeoutException e) {
 289  0 out.println("c timeout");
 290    }
 291    } catch (FileNotFoundException e) {
 292  0 e.printStackTrace();
 293    } catch (IOException e) {
 294  0 e.printStackTrace();
 295    } catch (ContradictionException e) {
 296  0 exitcode = ExitCode.UNSATISFIABLE;
 297  0 out.println("c (trivial inconsistency)");
 298    } catch (ParseFormatException e) {
 299  0 e.printStackTrace();
 300    }
 301  0 exit(exitcode.value());
 302    }
 303   
 304  0 void showAvailableSolvers() {
 305  0 if (factory != null) {
 306  0 out.println("Available solvers: ");
 307  0 String[] names = factory.solverNames();
 308  0 for (int i = 0; i < names.length; i++) {
 309  0 out.println(names[i]);
 310    }
 311    }
 312    }
 313   
 314  0 protected void solve(IProblem problem) throws TimeoutException {
 315  0 boolean isSat = problem.isSatisfiable();
 316  0 exitcode = isSat ? ExitCode.SATISFIABLE : ExitCode.UNSATISFIABLE;
 317    }
 318    }
 
CloverReport generated by Clover Code Coverage v1.3.9
jeu. sept. 29 2005 23:57:47 CEST.		   Open Source License registered to the OpenSAT Project. This license of Clover is provided to support the development of OpenSAT only.