1 package org.sat4j.sat.visu;
2
3 import java.awt.Color;
4 import java.io.BufferedReader;
5 import java.io.FileOutputStream;
6 import java.io.IOException;
7 import java.io.InputStreamReader;
8 import java.io.PrintStream;
9
10 import org.sat4j.specs.ILogAble;
11
12 public class GnuplotBasedSolverVisualisation implements SolverVisualisation {
13
14 private static final double TWO_THIRDS = 0.66;
15
16 private static final double ONE_THIRD = 0.33;
17
18 private static final double ZERO = 0.0;
19
20 private static final String SPEED = "Speed";
21
22 private static final String SET_XRANGE_0_5 = "set xrange [0.5:*]";
23
24 private static final String IMPULSES = "impulses";
25
26 private static final String EVALUATION = "Evaluation";
27
28 private static final String SIZE = "Size";
29
30 private static final String CLEAN = "Clean";
31
32 private static final String RESTART = "Restart";
33
34 private static final String CONFLICT_LEVEL = "Conflict Level";
35
36 private static final String GNUPLOT_GNUPLOT = "-gnuplot.gnuplot";
37
38 private static final String SET_MULTIPLOT = "set multiplot";
39
40 private static final String SET_TERMINAL_X11 = "set terminal x11";
41
42 private static final String SPEED_RESTART_DAT = "-speed-restart.dat";
43
44 private static final String SPEED_DAT = "-speed.dat";
45
46 private static final String GNUPLOT_SHOULD_BE_DEACTIVATED = "Gnuplot should be deactivated...";
47
48 private static final String GNUPLOT_SHOULD_HAVE_STARTED_NOW = "Gnuplot should have started now.";
49
50 private static final String GNUPLOT_WILL_START_IN_A_FEW_SECONDS = "Gnuplot will start in a few seconds.";
51
52 private static final String REREAD = "reread";
53
54 private static final String SET_YTICS_AUTO = "set ytics auto";
55
56 private static final String UNSET_MULTIPLOT = "unset multiplot";
57
58 private static final String UNSET_AUTOSCALE = "unset autoscale";
59
60 private static final String SET_Y2RANGE_0 = "set y2range [0:]";
61
62 private static final String SET_AUTOSCALE_YMAX = "set autoscale ymax";
63
64 private static final String SET_NOLOGSCALE_Y = "set nologscale y";
65
66 private static final String SET_NOLOGSCALE_X = "set nologscale x";
67
68 private static final String SET_AUTOSCALE_Y = "set autoscale y";
69
70 private static final String SET_AUTOSCALE_X = "set autoscale x";
71
72
73
74
75 private static final long serialVersionUID = 1L;
76
77 private VisuPreferences visuPreferences;
78 private int nVar;
79 private Process gnuplotProcess;
80 private String dataPath;
81 private ILogAble logger;
82
83 public GnuplotBasedSolverVisualisation(VisuPreferences visuPref, int nbVar,
84 String path, ILogAble logger) {
85 this.visuPreferences = visuPref;
86 this.nVar = nbVar;
87 this.dataPath = path;
88 this.logger = logger;
89 }
90
91 public void start() {
92 traceGnuplot();
93 }
94
95 public void end() {
96 stopGnuplot();
97 }
98
99 public void traceGnuplot() {
100
101 if (this.gnuplotProcess == null) {
102 try {
103
104 double verybottom = ZERO;
105 double bottom = ONE_THIRD;
106 double top = TWO_THIRDS;
107 double left = ZERO;
108 double middle = ONE_THIRD;
109 double right = TWO_THIRDS;
110
111 double width = ONE_THIRD;
112 double height = ONE_THIRD;
113
114 PrintStream out = new PrintStream(new FileOutputStream(
115 this.dataPath + GNUPLOT_GNUPLOT));
116 out.println(SET_TERMINAL_X11);
117 out.println(SET_MULTIPLOT);
118 out.println(SET_AUTOSCALE_X);
119 out.println(SET_AUTOSCALE_Y);
120 out.println(SET_NOLOGSCALE_X);
121 out.println(SET_NOLOGSCALE_Y);
122 out.println(SET_YTICS_AUTO);
123
124 GnuplotFunction f = new GnuplotFunction("2", Color.black, "");
125
126
127 if (this.visuPreferences.isDisplayConflictsDecision()) {
128 out.println(setSize(width, height));
129 out.println(setOrigin(bottom, right));
130 out.println(setTitle("Decision level at which the conflict occurs"));
131 out.println(SET_AUTOSCALE_YMAX);
132 out.println(SET_Y2RANGE_0);
133 GnuplotDataFile conflictLevelDF = new GnuplotDataFile(
134 this.dataPath + "-conflict-level.dat",
135 Color.magenta, CONFLICT_LEVEL);
136 GnuplotDataFile conflictLevelRestartDF = new GnuplotDataFile(
137 this.dataPath + "-conflict-level-restart.dat",
138 Color.gray, RESTART, IMPULSES);
139 GnuplotDataFile conflictLevelCleanDF = new GnuplotDataFile(
140 this.dataPath + "-conflict-level-clean.dat",
141 Color.orange, CLEAN, IMPULSES);
142 out.println(this.visuPreferences
143 .generatePlotLineOnDifferenteAxes(
144 new GnuplotDataFile[] { conflictLevelDF },
145 new GnuplotDataFile[] {
146 conflictLevelRestartDF,
147 conflictLevelCleanDF }, true));
148 }
149
150
151 if (this.visuPreferences.isDisplayClausesSize()) {
152 out.println(UNSET_AUTOSCALE);
153 out.println(SET_AUTOSCALE_X);
154 out.println(SET_AUTOSCALE_YMAX);
155 out.println(SET_Y2RANGE_0);
156 out.println(setSize(width, height));
157 out.println(setOrigin(top, left));
158 out.println(setTitle("Size of the clause learned (after minimization if any)"));
159 GnuplotDataFile learnedClausesDF = new GnuplotDataFile(
160 this.dataPath + "-learned-clauses-size.dat",
161 Color.blue, SIZE);
162 GnuplotDataFile learnedClausesRestartDF = new GnuplotDataFile(
163 this.dataPath + "-learned-clauses-size-restart.dat",
164 Color.gray, RESTART, IMPULSES);
165 GnuplotDataFile learnedClausesCleanDF = new GnuplotDataFile(
166 this.dataPath + "-learned-clauses-size-clean.dat",
167 Color.orange, CLEAN, IMPULSES);
168 out.println(this.visuPreferences
169 .generatePlotLineOnDifferenteAxes(
170 new GnuplotDataFile[] { learnedClausesDF },
171 new GnuplotDataFile[] {
172 learnedClausesCleanDF,
173 learnedClausesRestartDF }, true));
174 }
175
176
177 if (this.visuPreferences.isDisplayConflictsDecision()) {
178 out.println(SET_AUTOSCALE_X);
179 out.println(SET_AUTOSCALE_Y);
180 out.println(setSize(width, height));
181 out.println(setOrigin(top, middle));
182 out.println(setTitle("Value of learned clauses evaluation"));
183 GnuplotDataFile learnedDF = new GnuplotDataFile(
184 this.dataPath + "-learned.dat", Color.blue,
185 EVALUATION);
186 out.println(this.visuPreferences.generatePlotLine(
187 learnedDF, f, "", false));
188 }
189
190
191 out.println(SET_AUTOSCALE_X);
192 out.println(SET_NOLOGSCALE_X);
193 out.println(SET_NOLOGSCALE_Y);
194 out.println(SET_AUTOSCALE_Y);
195 out.println(setYRangeFrom1ToNvar());
196 out.println(setYTicsFrom1ToNVar());
197
198
199 if (this.visuPreferences.isDisplayDecisionIndexes()) {
200 out.println(UNSET_AUTOSCALE);
201 out.println("if(system(\"head "
202 + this.dataPath
203 + "-decision-indexes-pos.dat | wc -l\")!=0){set autoscale x;}");
204 out.println("if(system(\"head "
205 + this.dataPath
206 + "-decision-indexes-pos.dat | wc -l\")!=0){set yrange [1:"
207 + this.nVar + "]};");
208 out.println(setSize(width, height));
209 out.println(setOrigin(bottom, left));
210 out.println(setTitle("Index of the decision variables"));
211 GnuplotDataFile negativeDF = new GnuplotDataFile(
212 this.dataPath + "-decision-indexes-neg.dat",
213 Color.red, "Negative Decision");
214 GnuplotDataFile decisionRestartDF = new GnuplotDataFile(
215 this.dataPath + "-decision-indexes-restart.dat",
216 Color.gray, RESTART, IMPULSES);
217 GnuplotDataFile decisionCleanDF = new GnuplotDataFile(
218 this.dataPath + "-decision-indexes-clean.dat",
219 Color.orange, CLEAN, IMPULSES);
220 out.println(this.visuPreferences
221 .generatePlotLineOnDifferenteAxes(
222 new GnuplotDataFile[] { negativeDF },
223 new GnuplotDataFile[] { decisionRestartDF,
224 decisionCleanDF }, true,
225 this.visuPreferences.getNbLinesRead() * 4));
226
227
228 out.println(UNSET_AUTOSCALE);
229 out.println("if(system(\"head "
230 + this.dataPath
231 + "-decision-indexes-pos.dat | wc -l\")!=0){set autoscale x;set yrange [1:"
232 + this.nVar + "]; set y2range [0:]; }");
233 out.println(setSize(width, height));
234 out.println(setOrigin(verybottom, left));
235 out.println(setTitle("Index of the decision variables"));
236 GnuplotDataFile positiveDF = new GnuplotDataFile(
237 this.dataPath + "-decision-indexes-pos.dat",
238 Color.green, "Positive Decision");
239 out.println(this.visuPreferences
240 .generatePlotLineOnDifferenteAxes(
241 new GnuplotDataFile[] { positiveDF },
242 new GnuplotDataFile[] { decisionRestartDF,
243 decisionCleanDF }, true,
244 this.visuPreferences.getNbLinesRead() * 4));
245 }
246
247
248 if (this.visuPreferences.isDisplayConflictsTrail()) {
249 out.println(SET_AUTOSCALE_X);
250 out.println(SET_AUTOSCALE_Y);
251 out.println(SET_NOLOGSCALE_X);
252 out.println(SET_NOLOGSCALE_Y);
253 out.println(setSize(width, height));
254 out.println(setOrigin(top, right));
255 out.println(setTitle("Trail level when the conflict occurs"));
256 out.println(SET_Y2RANGE_0);
257 GnuplotDataFile trailLevelDF = new GnuplotDataFile(
258 this.dataPath + "-conflict-depth.dat",
259 Color.magenta, "Trail level");
260 GnuplotFunction nbVar2 = new GnuplotFunction("" + this.nVar
261 / 2, Color.green, "#Var/2");
262 GnuplotDataFile trailLevelRestartDF = new GnuplotDataFile(
263 this.dataPath + "-conflict-depth-restart.dat",
264 Color.gray, RESTART, IMPULSES);
265 GnuplotDataFile trailLevelCleanDF = new GnuplotDataFile(
266 this.dataPath + "-conflict-depth-clean.dat",
267 Color.orange, CLEAN, IMPULSES);
268 out.println(this.visuPreferences
269 .generatePlotLineOnDifferenteAxes(
270 new GnuplotDataFile[] { trailLevelDF },
271 new GnuplotDataFile[] {
272 trailLevelRestartDF,
273 trailLevelCleanDF },
274 new GnuplotFunction[] { nbVar2 }, true));
275 out.println(this.visuPreferences.generatePlotLine(
276 trailLevelDF, nbVar2, this.dataPath
277 + "-conflict-level-restart.dat", true));
278 }
279
280
281 if (this.visuPreferences.isDisplayVariablesEvaluation()) {
282 out.println(UNSET_AUTOSCALE);
283 out.println(SET_AUTOSCALE_Y);
284 out.println(SET_NOLOGSCALE_X);
285 out.println(SET_NOLOGSCALE_Y);
286 out.println(setYRangeFrom1ToNvar());
287 out.println(SET_XRANGE_0_5);
288 out.println(setSize(width, height));
289 out.println(setOrigin(bottom, middle));
290 out.println(setTitle("Value of variables activity"));
291 GnuplotDataFile heuristicsDF = new GnuplotDataFile(
292 this.dataPath + "-heuristics.dat", Color.red,
293 "Activity", "lines");
294 out.println(this.visuPreferences.generatePlotLine(
295 heuristicsDF, f, "", false));
296 }
297
298 if (this.visuPreferences.isDisplaySpeed()) {
299 out.println(SET_AUTOSCALE_X);
300 out.println(SET_NOLOGSCALE_X);
301 out.println(SET_NOLOGSCALE_Y);
302 out.println(setSize(width, height));
303 out.println(setOrigin(verybottom, middle));
304 out.println(setTitle("Number of propagations per second"));
305 out.println(SET_Y2RANGE_0);
306 GnuplotDataFile speedDF = new GnuplotDataFile(this.dataPath
307 + SPEED_DAT, Color.cyan, SPEED, "lines");
308 GnuplotDataFile cleanDF = new GnuplotDataFile(this.dataPath
309 + "-speed-clean.dat", Color.orange, CLEAN, IMPULSES);
310 GnuplotDataFile restartDF = new GnuplotDataFile(
311 this.dataPath + SPEED_RESTART_DAT, Color.gray,
312 RESTART, IMPULSES);
313 out.println(this.visuPreferences
314 .generatePlotLineOnDifferenteAxes(
315 new GnuplotDataFile[] { speedDF },
316 new GnuplotDataFile[] { cleanDF, restartDF },
317 true, 50));
318 }
319 out.println(UNSET_MULTIPLOT);
320 int pauseTime = this.visuPreferences.getRefreshTime() / 1000;
321 out.println("pause " + pauseTime);
322 out.println(REREAD);
323 out.close();
324
325 this.logger.log(GNUPLOT_WILL_START_IN_A_FEW_SECONDS);
326
327 Thread errorStreamThread = new Thread() {
328 @Override
329 public void run() {
330
331 try {
332 try {
333 Thread.sleep(GnuplotBasedSolverVisualisation.this.visuPreferences
334 .getTimeBeforeLaunching());
335 } catch (InterruptedException e) {
336 GnuplotBasedSolverVisualisation.this.logger
337 .log(e.getMessage());
338 }
339
340 GnuplotBasedSolverVisualisation.this.logger
341 .log("reads "
342 + GnuplotBasedSolverVisualisation.this.dataPath
343 + GNUPLOT_GNUPLOT);
344 GnuplotBasedSolverVisualisation.this.gnuplotProcess = Runtime
345 .getRuntime()
346 .exec(GnuplotBasedSolverVisualisation.this.visuPreferences
347 .createCommandLine(GnuplotBasedSolverVisualisation.this.dataPath
348 + GNUPLOT_GNUPLOT));
349
350 GnuplotBasedSolverVisualisation.this.logger
351 .log(GNUPLOT_SHOULD_HAVE_STARTED_NOW);
352
353 BufferedReader gnuInt = new BufferedReader(
354 new InputStreamReader(
355 GnuplotBasedSolverVisualisation.this.gnuplotProcess
356 .getErrorStream()));
357 String s;
358
359 while ((s = gnuInt.readLine()) != null) {
360 if (s.trim().length() > 0
361 && !s.toLowerCase().contains("warning")
362 && !s.toLowerCase().contains("plot")) {
363 GnuplotBasedSolverVisualisation.this.logger
364 .log(s);
365 }
366 }
367 gnuInt.close();
368 } catch (IOException e) {
369 GnuplotBasedSolverVisualisation.this.logger.log(e
370 .getMessage());
371 }
372 }
373 };
374 errorStreamThread.start();
375
376 } catch (IOException e) {
377 GnuplotBasedSolverVisualisation.this.logger.log(e.getMessage());
378 }
379 }
380 }
381
382 private String setYTicsFrom1ToNVar() {
383 return "set ytics add (1," + this.nVar + ")";
384 }
385
386 private String setYRangeFrom1ToNvar() {
387 return "set yrange [1:" + this.nVar + "]";
388 }
389
390 private String setOrigin(double bottom, double right) {
391 return "set origin " + right + "," + bottom;
392 }
393
394 private String setSize(double width, double height) {
395 return "set size " + width + "," + height;
396 }
397
398 private String setTitle(String title) {
399 return "set title \"" + title + "\"";
400
401 }
402
403 public void stopGnuplot() {
404 if (this.gnuplotProcess != null) {
405 this.gnuplotProcess.destroy();
406 this.logger.log(GNUPLOT_SHOULD_BE_DEACTIVATED);
407 }
408 this.gnuplotProcess = null;
409 }
410
411 public void setnVar(int n) {
412 this.nVar = n;
413 }
414
415 }