Clover coverage report -
Coverage timestamp: jeu. juin 15 2006 08:24:33 CEST
Overview   Package   File
    FRAMES   NO FRAMES  
file stats: LOC: 232   Methods: 14
NCLOC: 137   Classes: 1
 
 Source file Conditionals Statements Methods TOTAL
AbstractLauncher.java 0% 0% 0% 0%
coverage
 1    package org.sat4j;
 2   
 3    import java.io.BufferedReader;
 4    import java.io.FileNotFoundException;
 5    import java.io.IOException;
 6    import java.io.InputStreamReader;
 7    import java.io.PrintWriter;
 8    import java.io.Serializable;
 9    import java.net.URL;
 10    import java.util.Properties;
 11   
 12    import org.sat4j.reader.ParseFormatException;
 13    import org.sat4j.reader.Reader;
 14    import org.sat4j.specs.ContradictionException;
 15    import org.sat4j.specs.IProblem;
 16    import org.sat4j.specs.ISolver;
 17    import org.sat4j.specs.TimeoutException;
 18   
 19    /**
 20    * That class is used by launchers used to solve decision problems, i.e. problems with YES/NO/UNKNOWN answers.
 21    *
 22    * @author leberre
 23    *
 24    */
 25    public abstract class AbstractLauncher implements Serializable {
 26   
 27    public static final String SOLUTION_PREFIX = "v "; //$NON-NLS-1$
 28   
 29    public static final String ANSWER_PREFIX = "s "; //$NON-NLS-1$
 30   
 31    public static final String COMMENT_PREFIX = "c "; //$NON-NLS-1$
 32   
 33    private long beginTime;
 34   
 35    private ExitCode exitCode = ExitCode.UNKNOWN;
 36   
 37    protected Reader reader;
 38   
 39    private transient PrintWriter out = new PrintWriter(System.out, true);
 40   
 41    protected transient Thread shutdownHook = new Thread() {
 42  0 @Override
 43    public void run() {
 44  0 displayResult();
 45    }
 46    };
 47   
 48    protected ISolver solver;
 49   
 50  0 protected AbstractLauncher() {
 51  0 Runtime.getRuntime().addShutdownHook(shutdownHook);
 52    }
 53   
 54  0 protected void displayResult() {
 55  0 if (solver != null) {
 56  0 double wallclocktime = (System.currentTimeMillis() - beginTime) / 1000.0;
 57  0 solver.printStat(out, COMMENT_PREFIX); //$NON-NLS-1$
 58  0 out.println(ANSWER_PREFIX + exitCode); //$NON-NLS-1$
 59  0 if (exitCode == ExitCode.SATISFIABLE) {
 60  0 int[] model = solver.model();
 61  0 out.println(SOLUTION_PREFIX + reader.decode(model)); //$NON-NLS-1$
 62    }
 63  0 log("Total wall clock time (in seconds) : " + wallclocktime); //$NON-NLS-1$
 64    }
 65    }
 66   
 67    protected abstract void usage();
 68   
 69    /**
 70    * @throws IOException
 71    */
 72  0 protected final void displayHeader() throws IOException {
 73  0 log("SAT4J: a SATisfiability library for Java (c) 2004-2006 Daniel Le Berre"); //$NON-NLS-1$
 74  0 log("This is free software under the GNU LGPL licence. See www.sat4j.org for details."); //$NON-NLS-1$
 75  0 log("This software uses some libraries from the Jakarta project. See jakarta.apache.org for details.");
 76  0 URL url = Lanceur.class.getResource("/sat4j.version"); //$NON-NLS-1$
 77  0 if (url == null) {
 78  0 log("no version file found!!!"); //$NON-NLS-1$
 79    } else {
 80  0 BufferedReader in = new BufferedReader(new InputStreamReader(url
 81    .openStream()));
 82  0 log("version " + in.readLine()); //$NON-NLS-1$
 83  0 in.close();
 84    }
 85  0 Properties prop = System.getProperties();
 86  0 String [] infoskeys = {"sun.arch.data.model","java.version","os.name","os.version","os.arch"}; //$NON-NLS-1$//$NON-NLS-2$ //$NON-NLS-3$ //$NON-NLS-4$//$NON-NLS-5$
 87  0 for (String key : infoskeys) {
 88  0 log(key+"\t"+prop.getProperty(key)); //$NON-NLS-1$
 89    }
 90  0 Runtime runtime = Runtime.getRuntime();
 91  0 log("Free memory " + runtime.freeMemory()); //$NON-NLS-1$
 92  0 log("Max memory " + runtime.maxMemory()); //$NON-NLS-1$
 93  0 log("Total memory " + runtime.totalMemory()); //$NON-NLS-1$
 94  0 log("Number of processors " + runtime.availableProcessors()); //$NON-NLS-1$
 95    }
 96   
 97    /**
 98    * Reads a problem file from the command line.
 99    *
 100    * @param args
 101    * command line arguments
 102    * @param solver
 103    * the solver to feed
 104    * @param begintime
 105    * program begin time
 106    * @return a reference to the problem to solve
 107    * @throws FileNotFoundException
 108    * if the file is not found
 109    * @throws ParseFormatException
 110    * if the problem is not expressed using the right format
 111    * @throws IOException
 112    * for other IO problems
 113    * @throws ContradictionException
 114    * if the problem is found trivially unsat
 115    */
 116  0 protected IProblem readProblem(String problemname)
 117    throws FileNotFoundException, ParseFormatException, IOException,
 118    ContradictionException {
 119  0 log("solving " + problemname); //$NON-NLS-1$
 120  0 log("reading problem ... "); //$NON-NLS-1$
 121  0 reader = createReader(solver, problemname);
 122  0 IProblem problem = reader.parseInstance(problemname);
 123  0 log("... done. Time " //$NON-NLS-1$
 124    + (System.currentTimeMillis() - beginTime) / 1000.0 + " ms."); //$NON-NLS-1$
 125  0 log("#vars " + solver.nVars()); //$NON-NLS-1$
 126  0 log("#constraints " + solver.nConstraints()); //$NON-NLS-1$
 127  0 return problem;
 128    }
 129   
 130    protected abstract Reader createReader(ISolver solver, String problemname);
 131   
 132  0 public void run(String[] args) {
 133   
 134  0 try {
 135   
 136  0 displayHeader();
 137   
 138  0 solver = configureSolver(args);
 139   
 140  0 if (solver==null)
 141  0 return;
 142   
 143  0 String instanceName = getInstanceName(args);
 144   
 145  0 beginTime = System.currentTimeMillis();
 146   
 147  0 IProblem problem = readProblem(instanceName);
 148   
 149  0 try {
 150   
 151  0 solve(problem);
 152   
 153   
 154    } catch (TimeoutException e) {
 155  0 log("timeout"); //$NON-NLS-1$
 156    }
 157    } catch (FileNotFoundException e) {
 158  0 e.printStackTrace();
 159    } catch (IOException e) {
 160  0 e.printStackTrace();
 161    } catch (ContradictionException e) {
 162  0 exitCode = ExitCode.UNSATISFIABLE;
 163  0 log("(trivial inconsistency)"); //$NON-NLS-1$
 164    } catch (ParseFormatException e) {
 165  0 e.printStackTrace();
 166    }
 167    }
 168   
 169    protected abstract String getInstanceName(String[] args);
 170   
 171    protected abstract ISolver configureSolver(String[] args);
 172   
 173    /**
 174    * Display messages as comments on STDOUT
 175    *
 176    * @param message
 177    */
 178  0 protected void log(String message) {
 179  0 out.println(COMMENT_PREFIX + message);
 180    }
 181   
 182  0 protected void solve(IProblem problem) throws TimeoutException {
 183  0 exitCode = problem.isSatisfiable() ? ExitCode.SATISFIABLE
 184    : ExitCode.UNSATISFIABLE;
 185    }
 186   
 187    /**
 188    * Change the value of the exit code in the Launcher
 189    * @param exitCode the new ExitCode
 190    */
 191  0 public final void setExitCode(ExitCode exitCode) {
 192  0 this.exitCode = exitCode;
 193    }
 194   
 195    /**
 196    * Get the value of the ExitCode
 197    * @return the current value of the Exitcode
 198    */
 199  0 public final ExitCode getExitCode() {
 200  0 return exitCode;
 201    }
 202   
 203    /**
 204    * Obtaining the current time spent since the beginning of the solving process.
 205    * @return the time signature at the beginning of the run() method.
 206    */
 207  0 public final long getBeginTime() {
 208  0 return beginTime;
 209    }
 210   
 211    /**
 212    *
 213    * @return the reader used to parse the instance
 214    */
 215  0 public final Reader getReader() {
 216  0 return reader;
 217    }
 218   
 219    /**
 220    * To change the output stream on which statistics are displayed.
 221    * By default, the solver displays everything on System.out.
 222    *
 223    * @param out
 224    */
 225  0 public void setLogWriter(PrintWriter out) {
 226  0 this.out = out;
 227    }
 228   
 229  0 public PrintWriter getLogWriter() {
 230  0 return out;
 231    }
 232    }
 
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.