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