Clover coverage report -
Coverage timestamp: jeu. juin 15 2006 08:24:33 CEST
Overview   Package   File
    FRAMES   NO FRAMES  
file stats: LOC: 396   Methods: 12
NCLOC: 299   Classes: 1
 
 Source file Conditionals Statements Methods TOTAL
Lanceur.java 0% 0% 0% 0%
coverage
 1    /*
 2    * SAT4J: a SATisfiability library for Java Copyright (C) 2004 Daniel Le Berre
 3    *
 4    * Based on the original minisat specification from:
 5    *
 6    * An extensible SAT solver. Niklas E?n and Niklas S?rensson. Proceedings of the
 7    * Sixth International Conference on Theory and Applications of Satisfiability
 8    * Testing, LNCS 2919, pp 502-518, 2003.
 9    *
 10    * This library is free software; you can redistribute it and/or modify it under
 11    * the terms of the GNU Lesser General Public License as published by the Free
 12    * Software Foundation; either version 2.1 of the License, or (at your option)
 13    * any later version.
 14    *
 15    * This library is distributed in the hope that it will be useful, but WITHOUT
 16    * ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS
 17    * FOR A PARTICULAR PURPOSE. See the GNU Lesser General Public License for more
 18    * details.
 19    *
 20    * You should have received a copy of the GNU Lesser General Public License
 21    * along with this library; if not, write to the Free Software Foundation, Inc.,
 22    * 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA
 23    *
 24    */
 25   
 26    package org.sat4j;
 27   
 28    import java.io.File;
 29    import java.io.FileNotFoundException;
 30    import java.io.FileWriter;
 31    import java.io.IOException;
 32    import java.lang.reflect.Method;
 33    import java.net.MalformedURLException;
 34    import java.util.Locale;
 35   
 36    import org.apache.commons.beanutils.BeanUtils;
 37    import org.apache.commons.cli.CommandLine;
 38    import org.apache.commons.cli.HelpFormatter;
 39    import org.apache.commons.cli.Option;
 40    import org.apache.commons.cli.Options;
 41    import org.apache.commons.cli.ParseException;
 42    import org.apache.commons.cli.PosixParser;
 43    import org.sat4j.core.ASolverFactory;
 44    import org.sat4j.minisat.core.DotSearchListener;
 45    import org.sat4j.minisat.core.Solver;
 46    import org.sat4j.reader.InstanceReader;
 47    import org.sat4j.reader.ParseFormatException;
 48    import org.sat4j.reader.Reader;
 49    import org.sat4j.specs.ContradictionException;
 50    import org.sat4j.specs.IProblem;
 51    import org.sat4j.specs.ISolver;
 52    import org.sat4j.specs.TimeoutException;
 53   
 54    /**
 55    * This class is used to launch the SAT solvers from the command line. It is
 56    * compliant with the SAT competition (www.satcompetition.org) I/O format. The
 57    * launcher is to be used as follows:
 58    *
 59    * <pre>
 60    * [solvername] filename [key=value]*
 61    * </pre>
 62    *
 63    * If no solver name is given, then the default solver of the solver factory is
 64    * used (@see org.sat4j.core.ASolverFactory#defaultSolver()).
 65    *
 66    * @author leberre
 67    */
 68    public class Lanceur extends AbstractLauncher {
 69   
 70    /**
 71    *
 72    */
 73    private static final long serialVersionUID = 1L;
 74   
 75    /**
 76    * Lance le prouveur sur un fichier Dimacs.
 77    *
 78    * @param args doit contenir le nom d'un fichier Dimacs, eventuellement
 79    * compress?.
 80    */
 81  0 public static void main(final String[] args) {
 82  0 Lanceur lanceur = new Lanceur();
 83  0 lanceur.run(args);
 84  0 System.exit(lanceur.getExitCode().value());
 85    }
 86   
 87    protected ASolverFactory factory;
 88   
 89    private String filename;
 90   
 91    private String resultsfile;
 92   
 93    private boolean update;
 94   
 95    private boolean replay;
 96   
 97  0 @SuppressWarnings("nls")
 98    private Options createCLIOptions() {
 99  0 Options options = new Options();
 100   
 101  0 options.addOption("l", "library", true,
 102    "specifies the name of the library used (minisat by default)");
 103  0 options.addOption("s", "solver", true,
 104    "specifies the name of the solver to use");
 105  0 options.addOption("t", "timeout", true,
 106    "specifies the timeout (in seconds)");
 107  0 options
 108    .addOption("d", "dot", true,
 109    "create a sat4j.dot file in current directory representing the search");
 110  0 options
 111    .addOption("f", "filename", true,
 112    "specifies the file to use (in conjunction with -d for instance)");
 113  0 options.addOption("r", "replay", true, "replay stored results");
 114  0 options.addOption("b", "backup", true,
 115    "backup results in specified file");
 116  0 options
 117    .addOption("u", "update", false,
 118    "update results file if needed");
 119  0 Option op = options.getOption("l");
 120  0 op.setArgName("libname");
 121  0 op = options.getOption("s");
 122  0 op.setArgName("solvername");
 123  0 op = options.getOption("t");
 124  0 op.setArgName("delay");
 125  0 op = options.getOption("d");
 126  0 return options;
 127    }
 128   
 129    /**
 130    * @param args
 131    * @return
 132    */
 133  0 @SuppressWarnings("nls")
 134    @Override
 135    protected ISolver configureSolver(String[] args) {
 136  0 Options options = createCLIOptions();
 137  0 if (args.length==0) {
 138  0 HelpFormatter helpf = new HelpFormatter();
 139  0 helpf.printHelp("java -jar sat4j.jar", options, true);
 140  0 return null;
 141    }
 142  0 try {
 143  0 CommandLine cmd = new PosixParser().parse(options, args);
 144   
 145  0 String framework = cmd.getOptionValue("l"); //$NON-NLS-1$
 146  0 if (framework == null) { //$NON-NLS-1$
 147  0 framework = "minisat";
 148    }
 149    assert framework.equals("minisat") || framework.equals("ubcsat"); //$NON-NLS-1$//$NON-NLS-2$
 150   
 151  0 try {
 152  0 Class clazz = Class
 153    .forName("org.sat4j." + framework + ".SolverFactory"); //$NON-NLS-1$ //$NON-NLS-2$
 154  0 Class[] params = {};
 155  0 Method m = clazz.getMethod("instance", params); //$NON-NLS-1$
 156  0 factory = (ASolverFactory) m.invoke(null, (Object[]) null);
 157    } catch (Exception e) {
 158  0 System.err.println(Messages
 159    .getString("Lanceur.wrong.framework")); //$NON-NLS-1$
 160  0 e.printStackTrace();
 161    }
 162   
 163  0 ISolver asolver;
 164  0 String solvername = cmd.getOptionValue("s");
 165  0 if (solvername == null) {
 166  0 asolver = factory.defaultSolver();
 167    } else {
 168  0 asolver = factory.createSolverByName(solvername);
 169    }
 170  0 String timeout = cmd.getOptionValue("t");
 171  0 if (timeout != null) {
 172  0 asolver.setTimeout(Integer.parseInt(timeout));
 173    }
 174  0 filename = cmd.getOptionValue("f");
 175   
 176  0 if (cmd.hasOption("d")) {
 177  0 String dotfilename = null;
 178  0 if (filename != null) {
 179  0 dotfilename = cmd.getOptionValue("d");
 180    }
 181  0 if (dotfilename == null) {
 182  0 dotfilename = "sat4j.dot";
 183    }
 184  0 ((Solver) asolver).setSearchListener(new DotSearchListener(
 185    dotfilename));
 186    }
 187  0 int others = 0;
 188  0 String[] rargs = cmd.getArgs();
 189  0 if (filename == null) {
 190  0 filename = rargs[others++];
 191    }
 192   
 193  0 update = cmd.hasOption("u");
 194   
 195  0 resultsfile = cmd.getOptionValue("r");
 196   
 197  0 if (resultsfile == null) {
 198  0 replay = false;
 199  0 resultsfile = cmd.getOptionValue("b");
 200    } else
 201  0 replay = true;
 202   
 203    // use remaining data to configure the solver
 204  0 while (others < rargs.length) {
 205  0 String[] param = rargs[others].split("="); //$NON-NLS-1$
 206    assert param.length == 2;
 207  0 log("setting " + param[0] + " to " + param[1]); //$NON-NLS-1$ //$NON-NLS-2$
 208  0 try {
 209  0 BeanUtils.setProperty(asolver, param[0], param[1]);
 210    } catch (Exception e) {
 211  0 log("Cannot set parameter : " //$NON-NLS-1$
 212    + args[others]);
 213    }
 214  0 others++;
 215    }
 216   
 217  0 log(asolver.toString(COMMENT_PREFIX)); //$NON-NLS-1$
 218  0 log("timeout: " + asolver.getTimeout() + "s"); //$NON-NLS-1$ //$NON-NLS-2$
 219  0 return asolver;
 220    } catch (ParseException e1) {
 221  0 HelpFormatter helpf = new HelpFormatter();
 222  0 helpf.printHelp("java -jar sat4j.jar", options, true);
 223  0 usage();
 224    }
 225  0 return null;
 226    }
 227   
 228  0 @Override
 229    protected Reader createReader(ISolver solver, String problemname) {
 230  0 return new InstanceReader(solver);
 231    }
 232   
 233  0 @Override
 234    public void run(String[] args) {
 235  0 if (replay) {
 236  0 try {
 237  0 displayHeader();
 238    } catch (IOException e) {
 239  0 e.printStackTrace();
 240    }
 241   
 242  0 solver = configureSolver(args);
 243   
 244  0 if (solver == null)
 245  0 return;
 246   
 247  0 runValidationFile(solver, resultsfile, update);
 248    } else
 249  0 super.run(args);
 250    }
 251   
 252  0 void showAvailableSolvers() {
 253  0 if (factory != null) {
 254  0 log("Available solvers: "); //$NON-NLS-1$
 255  0 String[] names = factory.solverNames();
 256  0 for (int i = 0; i < names.length; i++) {
 257  0 log(names[i]);
 258    }
 259    }
 260    }
 261   
 262  0 @Override
 263    protected void usage() {
 264  0 showAvailableSolvers();
 265    }
 266   
 267  0 @Override
 268    protected String getInstanceName(String[] args) {
 269  0 return filename;
 270    }
 271   
 272   
 273  0 private final void stockValidationFile(final ISolver solver, final String filename, final String wxpFileName, final boolean tosave) {
 274  0 try {
 275  0 if (tosave) {
 276  0 (new FileWriter(wxpFileName, true)).close();
 277    }
 278  0 final ResultsManager unitTest = new ResultsManager(wxpFileName, tosave);
 279  0 ExitCode exitCode = ExitCode.UNKNOWN;
 280  0 Reader reader = createReader(solver, filename);
 281  0 IProblem problem;
 282  0 problem = reader.parseInstance(filename);
 283  0 if (problem.isSatisfiable()) {
 284  0 exitCode = ExitCode.SATISFIABLE;
 285    } else {
 286  0 exitCode = ExitCode.UNSATISFIABLE;
 287    }
 288  0 final ResultCode resultCode = unitTest.compare(filename, exitCode);
 289  0 getLogWriter().println(ResultsManager.printLine(filename, exitCode, resultCode));
 290   
 291  0 if ((tosave) && ((resultCode != ResultCode.KO) && (resultCode != ResultCode.WARNING))) {
 292  0 unitTest.save(wxpFileName);
 293  0 System.out.println("File Saved As <" + wxpFileName + ">");
 294    }
 295    } catch (MalformedURLException e1) {
 296  0 e1.printStackTrace();
 297    } catch (IOException e1) {
 298  0 e1.printStackTrace();
 299    } catch (ParseFormatException e) {
 300  0 e.printStackTrace();
 301    } catch (ContradictionException e) {
 302  0 e.printStackTrace();
 303    } catch (TimeoutException e) {
 304  0 e.printStackTrace();
 305    }
 306   
 307    }
 308  0 private void runValidationFile(ISolver solver, String filename,
 309    boolean tosave) {
 310  0 final ResultsManager unitTest;
 311  0 try {
 312   
 313  0 unitTest = new ResultsManager(filename, tosave);
 314  0 final int[] results = new int[ResultCode.values().length + 1];
 315  0 for (String file : unitTest.getFiles()) {
 316  0 ExitCode exitCode = ExitCode.UNKNOWN;
 317  0 Reader reader = createReader(solver, file);
 318  0 IProblem problem;
 319  0 try {
 320  0 problem = reader.parseInstance(file);
 321  0 if (problem.isSatisfiable()) {
 322  0 exitCode = ExitCode.SATISFIABLE;
 323    } else {
 324  0 exitCode = ExitCode.UNSATISFIABLE;
 325    }
 326    } catch (FileNotFoundException e) {
 327  0 log(e.getMessage());
 328    } catch (ParseFormatException e) {
 329  0 log(e.getMessage());
 330    } catch (IOException e) {
 331  0 log(e.getMessage());
 332    } catch (ContradictionException e) {
 333  0 log(e.getMessage());
 334    } catch (TimeoutException e) {
 335  0 log(e.getMessage());
 336    }
 337  0 final ResultCode resultCode = unitTest.compare(file, exitCode);
 338  0 results[resultCode.getValue()]++;
 339  0 getLogWriter().println(
 340    ResultsManager.printLine(file, exitCode, resultCode));
 341    }
 342  0 getLogWriter().println(getSummary(results));
 343   
 344  0 if ((tosave) && (getSuccess(results))) {
 345  0 final String path = ResultsManager.createPath() + "."
 346    + ResultsManager.EXT_JU.toLowerCase(Locale.getDefault());
 347  0 unitTest.save(path);
 348  0 System.out.println("File Saved As <"
 349    + (new File(path)).getCanonicalPath() + ">");
 350    }
 351    } catch (MalformedURLException e1) {
 352    // TODO Auto-generated catch block
 353  0 e1.printStackTrace();
 354    } catch (IOException e1) {
 355    // TODO Auto-generated catch block
 356  0 e1.printStackTrace();
 357    }
 358   
 359    }
 360   
 361  0 private static final boolean getSuccess(final int[] results) {
 362  0 if ((results[ResultCode.KO.getValue()] > 0)
 363    || (results[ResultCode.WARNING.getValue()] > 0)) {
 364  0 return false;
 365    }
 366  0 return true;
 367    }
 368   
 369  0 private static final String getSummary(final int[] results) {
 370  0 final StringBuffer sb = new StringBuffer("\n\nValidation Tests ");
 371   
 372  0 if (getSuccess(results)) {
 373  0 sb.append("Success");
 374    } else {
 375  0 sb.append("Failed");
 376    }
 377   
 378  0 sb.append('\n');
 379  0 sb.append("summary : number of OKs ");
 380  0 sb.append(results[ResultCode.OK.getValue()]);
 381  0 sb.append('\n');
 382  0 sb.append(" number of KOs ");
 383  0 sb.append(results[ResultCode.KO.getValue()]);
 384  0 sb.append('\n');
 385  0 sb.append(" number of WARNINGs ");
 386  0 sb.append(results[ResultCode.WARNING.getValue()]);
 387  0 sb.append('\n');
 388  0 sb.append(" number of UPDATEDs ");
 389  0 sb.append(results[ResultCode.UPDATED.getValue()]);
 390  0 sb.append('\n');
 391  0 sb.append(" number of UNKNOWNs ");
 392  0 sb.append(results[ResultCode.UNKNOWN.getValue()]);
 393  0 sb.append('\n');
 394  0 return sb.toString();
 395    }
 396    }
 
CloverReport generated by Clover Code Coverage v1.3.9
jeu. juin 15 2006 08:24:39 CEST.		   Open Source License registered to the OpenSAT Project. This license of Clover is provided to support the development of OpenSAT only.