Clover Coverage Report
Coverage timestamp: mer. juin 27 2007 07:27:16 CEST
Overview   Package   File
    FRAMES   NO FRAMES     
83   303   18   4,88
20   183   0,41   17
17     2  
1    
 
  AbstractLauncher       Line # 52 83 18 0% 0.0
 
No Tests
 
1    /*
2    * SAT4J: a SATisfiability library for Java Copyright (C) 2004-2006 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    package org.sat4j;
26   
27    import java.io.BufferedReader;
28    import java.io.FileNotFoundException;
29    import java.io.IOException;
30    import java.io.InputStreamReader;
31    import java.io.ObjectInputStream;
32    import java.io.PrintWriter;
33    import java.io.Serializable;
34    import java.lang.management.ManagementFactory;
35    import java.net.URL;
36    import java.util.Properties;
37   
38    import org.sat4j.reader.ParseFormatException;
39    import org.sat4j.reader.Reader;
40    import org.sat4j.specs.ContradictionException;
41    import org.sat4j.specs.IProblem;
42    import org.sat4j.specs.ISolver;
43    import org.sat4j.specs.TimeoutException;
44   
45    /**
46    * That class is used by launchers used to solve decision problems, i.e.
47    * problems with YES/NO/UNKNOWN answers.
48    *
49    * @author leberre
50    *
51    */
 
52    public abstract class AbstractLauncher implements Serializable {
53   
54    public static final String SOLUTION_PREFIX = "v "; //$NON-NLS-1$
55   
56    public static final String ANSWER_PREFIX = "s "; //$NON-NLS-1$
57   
58    public static final String COMMENT_PREFIX = "c "; //$NON-NLS-1$
59   
60    private long beginTime;
61   
62    private ExitCode exitCode = ExitCode.UNKNOWN;
63   
64    protected Reader reader;
65   
66    private transient PrintWriter out = new PrintWriter(System.out, true);
67   
68    private static final boolean cputimesupported = ManagementFactory.getThreadMXBean().isCurrentThreadCpuTimeSupported();
69   
70    protected transient Thread shutdownHook = new Thread() {
 
71  0 toggle @Override
72    public void run() {
73  0 displayResult();
74    }
75    };
76   
77    protected ISolver solver;
78   
79    private boolean silent = false;
80   
81    private double cputime;
82   
 
83  0 toggle protected AbstractLauncher() {
84  0 Runtime.getRuntime().addShutdownHook(shutdownHook);
85    }
86   
 
87  0 toggle protected void displayResult() {
88  0 if (solver != null) {
89  0 double wallclocktime = (System.currentTimeMillis() - beginTime) / 1000.0;
90  0 solver.printStat(out, COMMENT_PREFIX);
91  0 out.println(ANSWER_PREFIX + exitCode);
92  0 if (exitCode == ExitCode.SATISFIABLE) {
93  0 int[] model = solver.model();
94  0 out.print(SOLUTION_PREFIX);
95  0 reader.decode(model, out);
96  0 out.println();
97    }
98  0 log("Total wall clock time (in seconds) : " + wallclocktime); //$NON-NLS-1$
99  0 if (cputimesupported) {
100  0 log("Total CPU time (experimental, in seconds) : " + cputime) ; //$NON-NLS-1$
101    }
102    }
103    }
104   
105    protected abstract void usage();
106   
107    /**
108    * @throws IOException
109    */
 
110  0 toggle protected final void displayHeader() {
111  0 log("SAT4J: a SATisfiability library for Java (c) 2004-2007 Daniel Le Berre"); //$NON-NLS-1$
112  0 log("This is free software under the GNU LGPL licence. See www.sat4j.org for details."); //$NON-NLS-1$
113  0 log("This software uses some libraries from the Jakarta project. See jakarta.apache.org for details."); //$NON-NLS-1$
114  0 URL url = Lanceur.class.getResource("/sat4j.version"); //$NON-NLS-1$
115  0 if (url == null) {
116  0 log("no version file found!!!"); //$NON-NLS-1$
117    } else {
118  0 BufferedReader in = null;
119  0 try {
120  0 in = new BufferedReader(new InputStreamReader(url
121    .openStream()));
122  0 log("version " + in.readLine()); //$NON-NLS-1$
123    } catch (IOException e) {
124  0 log("c ERROR: "+e.getMessage());
125    } finally {
126  0 if (in!=null) {
127  0 try {
128  0 in.close();
129    } catch (IOException e) {
130  0 log("c ERROR: "+e.getMessage());
131    }
132    }
133    }
134    }
135  0 Properties prop = System.getProperties();
136  0 String[] infoskeys = {
137    "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$
138  0 for (String key : infoskeys) {
139  0 log(key + "\t" + prop.getProperty(key)); //$NON-NLS-1$
140    }
141  0 Runtime runtime = Runtime.getRuntime();
142  0 log("Free memory " + runtime.freeMemory()); //$NON-NLS-1$
143  0 log("Max memory " + runtime.maxMemory()); //$NON-NLS-1$
144  0 log("Total memory " + runtime.totalMemory()); //$NON-NLS-1$
145  0 log("Number of processors " + runtime.availableProcessors()); //$NON-NLS-1$
146    }
147   
148    /**
149    * Reads a problem file from the command line.
150    *
151    * @param args
152    * command line arguments
153    * @param solver
154    * the solver to feed
155    * @param begintime
156    * program begin time
157    * @return a reference to the problem to solve
158    * @throws FileNotFoundException
159    * if the file is not found
160    * @throws ParseFormatException
161    * if the problem is not expressed using the right format
162    * @throws IOException
163    * for other IO problems
164    * @throws ContradictionException
165    * if the problem is found trivially unsat
166    */
 
167  0 toggle protected IProblem readProblem(String problemname)
168    throws FileNotFoundException, ParseFormatException, IOException,
169    ContradictionException {
170  0 log("solving " + problemname); //$NON-NLS-1$
171  0 log("reading problem ... "); //$NON-NLS-1$
172  0 reader = createReader(solver, problemname);
173  0 IProblem problem = reader.parseInstance(problemname);
174  0 log("... done. Wall clock time " //$NON-NLS-1$
175    + (System.currentTimeMillis() - beginTime) / 1000.0 + "s."); //$NON-NLS-1$
176  0 if (cputimesupported) {
177  0 log("CPU time (experimental) "+ManagementFactory.getThreadMXBean().getCurrentThreadCpuTime() /1000000000.0+"s.");
178    }
179  0 log("#vars " + solver.nVars()); //$NON-NLS-1$
180  0 log("#constraints " + solver.nConstraints()); //$NON-NLS-1$
181  0 return problem;
182    }
183   
184    protected abstract Reader createReader(ISolver solver, String problemname);
185   
 
186  0 toggle public void run(String[] args) {
187   
188  0 try {
189  0 displayHeader();
190  0 solver = configureSolver(args);
191  0 if (solver == null)
192  0 return;
193  0 String instanceName = getInstanceName(args);
194  0 beginTime = System.currentTimeMillis();
195  0 IProblem problem = readProblem(instanceName);
196  0 try {
197  0 solve(problem);
198    } catch (TimeoutException e) {
199  0 log("timeout"); //$NON-NLS-1$
200    }
201    } catch (FileNotFoundException e) {
202  0 log("FATAL");
203  0 e.printStackTrace();
204    } catch (IOException e) {
205  0 log("FATAL");
206  0 e.printStackTrace();
207    } catch (ContradictionException e) {
208  0 exitCode = ExitCode.UNSATISFIABLE;
209  0 log("(trivial inconsistency)"); //$NON-NLS-1$
210    } catch (ParseFormatException e) {
211  0 log("FATAL");
212  0 e.printStackTrace();
213    }
214  0 if (cputimesupported) {
215  0 cputime = ManagementFactory.getThreadMXBean().getCurrentThreadCpuTime() /1000000000.0;
216    }
217    }
218   
219    protected abstract String getInstanceName(String[] args);
220   
221    protected abstract ISolver configureSolver(String[] args);
222   
223    /**
224    * Display messages as comments on STDOUT
225    *
226    * @param message
227    */
 
228  0 toggle protected void log(String message) {
229  0 if (!silent)
230  0 out.println(COMMENT_PREFIX + message);
231    }
232   
 
233  0 toggle protected void solve(IProblem problem) throws TimeoutException {
234  0 exitCode = problem.isSatisfiable() ? ExitCode.SATISFIABLE
235    : ExitCode.UNSATISFIABLE;
236    }
237   
238    /**
239    * Change the value of the exit code in the Launcher
240    *
241    * @param exitCode
242    * the new ExitCode
243    */
 
244  0 toggle public final void setExitCode(ExitCode exitCode) {
245  0 this.exitCode = exitCode;
246    }
247   
248    /**
249    * Get the value of the ExitCode
250    *
251    * @return the current value of the Exitcode
252    */
 
253  0 toggle public final ExitCode getExitCode() {
254  0 return exitCode;
255    }
256   
257    /**
258    * Obtaining the current time spent since the beginning of the solving
259    * process.
260    *
261    * @return the time signature at the beginning of the run() method.
262    */
 
263  0 toggle public final long getBeginTime() {
264  0 return beginTime;
265    }
266   
267    /**
268    *
269    * @return the reader used to parse the instance
270    */
 
271  0 toggle public final Reader getReader() {
272  0 return reader;
273    }
274   
275    /**
276    * To change the output stream on which statistics are displayed. By
277    * default, the solver displays everything on System.out.
278    *
279    * @param out
280    */
 
281  0 toggle public void setLogWriter(PrintWriter out) {
282  0 this.out = out;
283    }
284   
 
285  0 toggle public PrintWriter getLogWriter() {
286  0 return out;
287    }
288   
 
289  0 toggle protected void setSilent(boolean b) {
290  0 silent = b;
291    }
292   
 
293  0 toggle private void readObject(ObjectInputStream stream) throws IOException, ClassNotFoundException {
294  0 stream.defaultReadObject();
295  0 out = new PrintWriter(System.out, true);
296  0 shutdownHook = new Thread() {
 
297  0 toggle @Override
298    public void run() {
299  0 displayResult();
300    }
301    };
302    }
303    }
 
CloverReport generated by Clover Code Coverage v2.0a5
mer. juin 27 2007 07:27:33 CEST.		   Beta Testers License registered to clover-support@cenqua.com. This license of Clover2 is provided for beta testing only. You have 5 day(s) before your Beta Tester License expires.