1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
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.PercentLengthLearning;
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
68
69
70
71
72
73
74
75
76
77
78
79
80 public class Lanceur extends AbstractLauncher {
81
82
83
84
85 private static final long serialVersionUID = 1L;
86
87
88
89
90
91
92
93
94 public static void main(final String[] args) {
95 Lanceur lanceur = new Lanceur();
96 lanceur.run(args);
97 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 @SuppressWarnings("nls")
111 private Options createCLIOptions() {
112 Options options = new Options();
113
114 options.addOption("l", "library", true,
115 "specifies the name of the library used (minisat by default)");
116 options.addOption("s", "solver", true,
117 "specifies the name of a prebuilt solver from the library");
118 options.addOption("S", "Solver", true,
119 "setup a solver using a solver config string");
120 options.addOption("t", "timeout", true,
121 "specifies the timeout (in seconds)");
122 options.addOption("T", "timeoutms", true,
123 "specifies the timeout (in milliseconds)");
124 options
125 .addOption("d", "dot", true,
126 "create a sat4j.dot file in current directory representing the search");
127 options
128 .addOption("f", "filename", true,
129 "specifies the file to use (in conjunction with -d for instance)");
130 options.addOption("r", "replay", true, "replay stored results");
131 options.addOption("b", "backup", true,
132 "backup results in specified file");
133 options
134 .addOption("u", "update", false,
135 "update results file if needed");
136 options.addOption("m", "mute", false, "Set launcher in silent mode");
137 Option op = options.getOption("l");
138 op.setArgName("libname");
139 op = options.getOption("s");
140 op.setArgName("solvername");
141 op = options.getOption("t");
142 op.setArgName("delay");
143 options.getOption("d");
144 return options;
145 }
146
147
148
149
150
151
152 @SuppressWarnings("nls")
153 @Override
154 protected ISolver configureSolver(String[] args) {
155 Options options = createCLIOptions();
156 if (args.length == 0) {
157 HelpFormatter helpf = new HelpFormatter();
158 helpf.printHelp("java -jar sat4j.jar", options, true);
159 return null;
160 }
161 try {
162 CommandLine cmd = new PosixParser().parse(options, args);
163
164 String framework = cmd.getOptionValue("l");
165 if (framework == null) {
166 framework = "minisat";
167 }
168 assert "minisat".equals(framework) || "ubcsat".equals(framework);
169
170 try {
171 Class<?> clazz = Class
172 .forName("org.sat4j." + framework + ".SolverFactory");
173 Class<?>[] params = {};
174 Method m = clazz.getMethod("instance", params);
175 factory = (ASolverFactory) m.invoke(null, (Object[]) null);
176 } catch (Exception e) {
177 System.err.println(Messages
178 .getString("Lanceur.wrong.framework"));
179 e.printStackTrace();
180 }
181
182 ISolver asolver;
183 if (cmd.hasOption("S")) {
184 asolver = configureFromString(cmd.getOptionValue("S"));
185 } else {
186 String solvername = cmd.getOptionValue("s");
187 if (solvername == null) {
188 asolver = factory.defaultSolver();
189 } else {
190 asolver = factory.createSolverByName(solvername);
191 }
192 }
193 String timeout = cmd.getOptionValue("t");
194 if (timeout == null) {
195 timeout = cmd.getOptionValue("T");
196 if (timeout != null) {
197 asolver.setTimeoutMs(Long.parseLong(timeout));
198 }
199 } else {
200 asolver.setTimeout(Integer.parseInt(timeout));
201 }
202 filename = cmd.getOptionValue("f");
203
204 if (cmd.hasOption("d")) {
205 String dotfilename = null;
206 if (filename != null) {
207 dotfilename = cmd.getOptionValue("d");
208 }
209 if (dotfilename == null) {
210 dotfilename = "sat4j.dot";
211 }
212 ((Solver<?>) asolver).setSearchListener(new DotSearchListener(
213 dotfilename));
214 }
215
216 if (cmd.hasOption("m")) {
217 setSilent(true);
218 }
219 int others = 0;
220 String[] rargs = cmd.getArgs();
221 if (filename == null) {
222 filename = rargs[others++];
223 }
224
225 update = cmd.hasOption("u");
226
227 resultsfile = cmd.getOptionValue("r");
228
229 if (resultsfile == null) {
230 replay = false;
231 resultsfile = cmd.getOptionValue("b");
232 } else
233 replay = true;
234
235
236 while (others < rargs.length) {
237 String[] param = rargs[others].split("=");
238 assert param.length == 2;
239 log("setting " + param[0] + " to " + param[1]);
240 try {
241 BeanUtils.setProperty(asolver, param[0], param[1]);
242 } catch (Exception e) {
243 log("Cannot set parameter : "
244 + args[others]);
245 }
246 others++;
247 }
248
249 log(asolver.toString(COMMENT_PREFIX));
250 log("timeout: " + asolver.getTimeout() + "s");
251 return asolver;
252 } catch (ParseException e1) {
253 HelpFormatter helpf = new HelpFormatter();
254 helpf.printHelp("java -jar sat4j.jar", options, true);
255 usage();
256 }
257 return null;
258 }
259
260 @Override
261 protected Reader createReader(ISolver solver, String problemname) {
262 return new InstanceReader(solver);
263 }
264
265 @Override
266 public void run(String[] args) {
267 if (replay) {
268 displayHeader();
269
270 solver = configureSolver(args);
271
272 if (solver == null)
273 return;
274
275 runValidationFile(solver, resultsfile, update);
276 } else
277 super.run(args);
278 }
279
280 void showAvailableSolvers() {
281 if (factory != null) {
282 log("Available solvers: ");
283 String[] names = factory.solverNames();
284 for (int i = 0; i < names.length; i++) {
285 log(names[i]);
286 }
287 }
288 }
289
290 @Override
291 protected void usage() {
292 showAvailableSolvers();
293 }
294
295 @Override
296 protected String getInstanceName(String[] args) {
297 return filename;
298 }
299
300 private void runValidationFile(ISolver solver, String filename,
301 boolean tosave) {
302 final ResultsManager unitTest;
303 try {
304
305 unitTest = new ResultsManager(filename, tosave);
306 final int[] results = new int[ResultCode.values().length + 1];
307 for (String file : unitTest.getFiles()) {
308 ExitCode exitCode = ExitCode.UNKNOWN;
309 Reader reader = createReader(solver, file);
310 IProblem problem;
311 try {
312 problem = reader.parseInstance(file);
313 if (problem.isSatisfiable()) {
314 exitCode = ExitCode.SATISFIABLE;
315 } else {
316 exitCode = ExitCode.UNSATISFIABLE;
317 }
318 } catch (FileNotFoundException e) {
319 log("FATAL "+e.getMessage());
320 } catch (ParseFormatException e) {
321 log("FATAL "+e.getMessage());
322 } catch (IOException e) {
323 log("FATAL "+e.getMessage());
324 } catch (ContradictionException e) {
325 log("Trivial inconsistency");
326 exitCode = ExitCode.UNSATISFIABLE;
327 } catch (TimeoutException e) {
328 log("Timeout");
329 }
330 final ResultCode resultCode = unitTest.compare(file, exitCode);
331 results[resultCode.getValue()]++;
332 getLogWriter().println(
333 ResultsManager.printLine(file, exitCode, resultCode));
334 }
335 getLogWriter().println(getSummary(results));
336
337 if ((tosave) && (getSuccess(results))) {
338 final String path = ResultsManager.createPath()
339 + "."
340 + ResultsManager.EXT_JU
341 .toLowerCase(Locale.getDefault());
342 unitTest.save(path);
343 System.out.println("File Saved As <"
344 + (new File(path)).getCanonicalPath() + ">");
345 }
346 } catch (MalformedURLException e1) {
347
348 e1.printStackTrace();
349 } catch (IOException e1) {
350
351 e1.printStackTrace();
352 }
353
354 }
355
356 private static final boolean getSuccess(final int[] results) {
357 if ((results[ResultCode.KO.getValue()] > 0)
358 || (results[ResultCode.WARNING.getValue()] > 0)) {
359 return false;
360 }
361 return true;
362 }
363
364 private static final String getSummary(final int[] results) {
365 final StringBuffer sb = new StringBuffer("\n\nValidation Tests ");
366
367 if (getSuccess(results)) {
368 sb.append("Success");
369 } else {
370 sb.append("Failed");
371 }
372
373 sb.append("\nsummary : number of OKs ");
374 sb.append(results[ResultCode.OK.getValue()]);
375 sb.append("\n number of KOs ");
376 sb.append(results[ResultCode.KO.getValue()]);
377 sb.append("\n number of WARNINGs ");
378 sb.append(results[ResultCode.WARNING.getValue()]);
379 sb.append("\n number of UPDATEDs ");
380 sb.append(results[ResultCode.UPDATED.getValue()]);
381 sb.append("\n number of UNKNOWNs ");
382 sb.append(results[ResultCode.UNKNOWN.getValue()]);
383 sb.append('\n');
384 return sb.toString();
385 }
386
387 @SuppressWarnings("unchecked")
388 private final ISolver configureFromString(String solverconfig) {
389
390
391 StringTokenizer stk = new StringTokenizer(solverconfig, ",");
392 Properties pf = new Properties();
393 String token;
394 String[] couple;
395 while (stk.hasMoreElements()) {
396 token = stk.nextToken();
397 couple = token.split("=");
398 pf.setProperty(couple[0], couple[1]);
399 }
400 DataStructureFactory dsf = setupObject("DSF", pf,
401 new MixedDataStructureDaniel());
402 LearningStrategy learning = setupObject("LEARNING", pf,
403 new PercentLengthLearning());
404 IOrder order = setupObject("ORDER", pf, new VarOrderHeap());
405 RestartStrategy restarter = setupObject("RESTARTS",pf,new MiniSATRestarts());
406 Solver solver = new Solver(new FirstUIP(), learning, dsf, order,restarter);
407 learning.setSolver(solver);
408 solver.setSimplifier(pf.getProperty("SIMP", "NO_SIMPLIFICATION"));
409 SearchParams params = setupObject("PARAMS", pf, new SearchParams());
410 solver.setSearchParams(params);
411 return solver;
412 }
413
414 @SuppressWarnings("unchecked")
415 private final <T> T setupObject(String component, Properties pf,
416 T defaultcomp) {
417 try {
418 String configline = pf.getProperty(component);
419 if (configline == null) {
420 log("using default component " + defaultcomp + " for "
421 + component);
422 return defaultcomp;
423 }
424 log("configuring " + component);
425 String[] config = configline.split("/");
426 T comp = (T) Class.forName(config[0]).newInstance();
427 for (int i = 1; i < config.length; i++) {
428 String[] param = config[i].split(":");
429 assert param.length == 2;
430 try {
431
432 BeanUtils.getProperty(comp, param[0]);
433 BeanUtils.setProperty(comp, param[0], param[1]);
434 } catch (Exception e) {
435 log("Problem with component " + config[0] + " " + e);
436 }
437 }
438 return comp;
439 } catch (InstantiationException e) {
440 log("Problem with component " + component + " " + e);
441 } catch (IllegalAccessException e) {
442 log("Problem with component " + component + " " + e);
443 } catch (ClassNotFoundException e) {
444 log("Problem with component " + component + " " + e);
445 }
446 log("using default component " + defaultcomp + " for " + component);
447 return defaultcomp;
448 }
449 }