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 |
| |
21 |
| |
22 |
| |
23 |
| |
24 |
| |
25 |
| public abstract class AbstractLauncher implements Serializable { |
26 |
| |
27 |
| public static final String SOLUTION_PREFIX = "v "; |
28 |
| |
29 |
| public static final String ANSWER_PREFIX = "s "; |
30 |
| |
31 |
| public static final String COMMENT_PREFIX = "c "; |
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);
|
58 |
0
| out.println(ANSWER_PREFIX + exitCode);
|
59 |
0
| if (exitCode == ExitCode.SATISFIABLE) {
|
60 |
0
| int[] model = solver.model();
|
61 |
0
| out.println(SOLUTION_PREFIX + reader.decode(model));
|
62 |
| } |
63 |
0
| log("Total wall clock time (in seconds) : " + wallclocktime);
|
64 |
| } |
65 |
| } |
66 |
| |
67 |
| protected abstract void usage(); |
68 |
| |
69 |
| |
70 |
| |
71 |
| |
72 |
0
| protected final void displayHeader() throws IOException {
|
73 |
0
| log("SAT4J: a SATisfiability library for Java (c) 2004-2006 Daniel Le Berre");
|
74 |
0
| log("This is free software under the GNU LGPL licence. See www.sat4j.org for details.");
|
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");
|
77 |
0
| if (url == null) {
|
78 |
0
| log("no version file found!!!");
|
79 |
| } else { |
80 |
0
| BufferedReader in = new BufferedReader(new InputStreamReader(url
|
81 |
| .openStream())); |
82 |
0
| log("version " + in.readLine());
|
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"};
|
87 |
0
| for (String key : infoskeys) {
|
88 |
0
| log(key+"\t"+prop.getProperty(key));
|
89 |
| } |
90 |
0
| Runtime runtime = Runtime.getRuntime();
|
91 |
0
| log("Free memory " + runtime.freeMemory());
|
92 |
0
| log("Max memory " + runtime.maxMemory());
|
93 |
0
| log("Total memory " + runtime.totalMemory());
|
94 |
0
| log("Number of processors " + runtime.availableProcessors());
|
95 |
| } |
96 |
| |
97 |
| |
98 |
| |
99 |
| |
100 |
| |
101 |
| |
102 |
| |
103 |
| |
104 |
| |
105 |
| |
106 |
| |
107 |
| |
108 |
| |
109 |
| |
110 |
| |
111 |
| |
112 |
| |
113 |
| |
114 |
| |
115 |
| |
116 |
0
| protected IProblem readProblem(String problemname)
|
117 |
| throws FileNotFoundException, ParseFormatException, IOException, |
118 |
| ContradictionException { |
119 |
0
| log("solving " + problemname);
|
120 |
0
| log("reading problem ... ");
|
121 |
0
| reader = createReader(solver, problemname);
|
122 |
0
| IProblem problem = reader.parseInstance(problemname);
|
123 |
0
| log("... done. Time "
|
124 |
| + (System.currentTimeMillis() - beginTime) / 1000.0 + " ms."); |
125 |
0
| log("#vars " + solver.nVars());
|
126 |
0
| log("#constraints " + solver.nConstraints());
|
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");
|
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)");
|
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 |
| |
175 |
| |
176 |
| |
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 |
| |
189 |
| |
190 |
| |
191 |
0
| public final void setExitCode(ExitCode exitCode) {
|
192 |
0
| this.exitCode = exitCode;
|
193 |
| } |
194 |
| |
195 |
| |
196 |
| |
197 |
| |
198 |
| |
199 |
0
| public final ExitCode getExitCode() {
|
200 |
0
| return exitCode;
|
201 |
| } |
202 |
| |
203 |
| |
204 |
| |
205 |
| |
206 |
| |
207 |
0
| public final long getBeginTime() {
|
208 |
0
| return beginTime;
|
209 |
| } |
210 |
| |
211 |
| |
212 |
| |
213 |
| |
214 |
| |
215 |
0
| public final Reader getReader() {
|
216 |
0
| return reader;
|
217 |
| } |
218 |
| |
219 |
| |
220 |
| |
221 |
| |
222 |
| |
223 |
| |
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 |
| } |