1 package org.sat4j.sat.visu;
2
3 import java.awt.Color;
4
5 public class VisuPreferences {
6
7 private static final int DEFAULT_TIME_BEFORE_LAUNCHING = 8000;
8 private static final int DEFAULT_REFRESH_TIME = 500;
9 private static final int DEFAULT_LINES_READ = 11000;
10 private static final String AXIS_X1Y1 = "\" axis x1y1";
11 private static final String TITLE = "\" title \"";
12 private static final String LC_RGB = " lc rgb \"#";
13 private Color backgroundColor;
14 private Color borderColor;
15
16
17
18 private int timeBeforeLaunching;
19
20
21
22
23 private int refreshTime;
24 private int nbLinesRead;
25 private boolean displayRestarts;
26 private Color restartColor;
27 private boolean slidingWindows;
28
29 private boolean displayDecisionIndexes;
30 private boolean displaySpeed;
31 private boolean displayConflictsTrail;
32 private boolean displayConflictsDecision;
33 private boolean displayVariablesEvaluation;
34 private boolean displayClausesEvaluation;
35 private boolean displayClausesSize;
36
37 public boolean isDisplayClausesSize() {
38 return this.displayClausesSize;
39 }
40
41 public void setDisplayClausesSize(boolean displayClausesSize) {
42 this.displayClausesSize = displayClausesSize;
43 }
44
45 public VisuPreferences() {
46 this.backgroundColor = Color.white;
47 this.borderColor = Color.black;
48 this.nbLinesRead = DEFAULT_LINES_READ;
49 this.refreshTime = DEFAULT_REFRESH_TIME;
50 this.timeBeforeLaunching = DEFAULT_TIME_BEFORE_LAUNCHING;
51 this.displayRestarts = true;
52 this.restartColor = Color.LIGHT_GRAY;
53 this.slidingWindows = true;
54
55 this.displayDecisionIndexes = true;
56 this.displayConflictsTrail = true;
57 this.displaySpeed = false;
58 this.displayConflictsDecision = true;
59 this.displayVariablesEvaluation = false;
60 this.displayClausesEvaluation = true;
61 this.displayClausesSize = true;
62 }
63
64 public int getNumberOfDisplayedGraphs() {
65 int n = 0;
66
67 if (this.displayClausesEvaluation) {
68 n++;
69 }
70 if (this.displayConflictsTrail) {
71 n++;
72 }
73 if (this.displayConflictsDecision) {
74 n++;
75 }
76 if (this.displayDecisionIndexes) {
77 n += 2;
78 }
79 if (this.displaySpeed) {
80 n++;
81 }
82 if (this.displayVariablesEvaluation) {
83 n++;
84 }
85 if (this.displayClausesSize) {
86 n++;
87 }
88
89 return n;
90 }
91
92 public Color getBackgroundColor() {
93 return this.backgroundColor;
94 }
95
96 public void setBackgroundColor(Color backgroundColor) {
97 this.backgroundColor = backgroundColor;
98 }
99
100 public Color getBorderColor() {
101 return this.borderColor;
102 }
103
104 public void setBorderColor(Color borderColor) {
105 this.borderColor = borderColor;
106 }
107
108 public int getTimeBeforeLaunching() {
109 return this.timeBeforeLaunching;
110 }
111
112 public void setTimeBeforeLaunching(int timeBeforeLaunching) {
113 this.timeBeforeLaunching = timeBeforeLaunching;
114 }
115
116 public int getRefreshTime() {
117 return this.refreshTime;
118 }
119
120 public void setRefreshTime(int refreshTime) {
121 this.refreshTime = refreshTime;
122 }
123
124 public int getNbLinesRead() {
125 return this.nbLinesRead;
126 }
127
128 public void setNbLinesRead(int nbLinesRead) {
129 this.nbLinesRead = nbLinesRead;
130 }
131
132 public boolean isDisplayRestarts() {
133 return this.displayRestarts;
134 }
135
136 public void setDisplayRestarts(boolean displayRestarts) {
137 this.displayRestarts = displayRestarts;
138 }
139
140 public Color getRestartColor() {
141 return this.restartColor;
142 }
143
144 public void setRestartColor(Color restartColor) {
145 this.restartColor = restartColor;
146 }
147
148 public boolean isSlidingWindows() {
149 return this.slidingWindows;
150 }
151
152 public void setSlidingWindows(boolean slidingWindows) {
153 this.slidingWindows = slidingWindows;
154 }
155
156 public boolean isDisplayDecisionIndexes() {
157 return this.displayDecisionIndexes;
158 }
159
160 public void setDisplayDecisionIndexes(boolean displayDecisionIndexes) {
161 this.displayDecisionIndexes = displayDecisionIndexes;
162 }
163
164 public boolean isDisplaySpeed() {
165 return this.displaySpeed;
166 }
167
168 public void setDisplaySpeed(boolean displaySpeed) {
169 this.displaySpeed = displaySpeed;
170 }
171
172 public boolean isDisplayConflictsTrail() {
173 return this.displayConflictsTrail;
174 }
175
176 public void setDisplayConflictsTrail(boolean displayConflictsTrail) {
177 this.displayConflictsTrail = displayConflictsTrail;
178 }
179
180 public boolean isDisplayConflictsDecision() {
181 return this.displayConflictsDecision;
182 }
183
184 public void setDisplayConflictsDecision(boolean displayConflictsDecision) {
185 this.displayConflictsDecision = displayConflictsDecision;
186 }
187
188 public boolean isDisplayVariablesEvaluation() {
189 return this.displayVariablesEvaluation;
190 }
191
192 public void setDisplayVariablesEvaluation(boolean displayVariablesEvaluation) {
193 this.displayVariablesEvaluation = displayVariablesEvaluation;
194 }
195
196 public boolean isDisplayClausesEvaluation() {
197 return this.displayClausesEvaluation;
198 }
199
200 public void setDisplayClausesEvaluation(boolean displayClausesEvaluation) {
201 this.displayClausesEvaluation = displayClausesEvaluation;
202 }
203
204 @Override
205 public String toString() {
206 return "GnuplotPreferences [backgroundColor=" + this.backgroundColor
207 + ", borderColor=" + this.borderColor
208 + ", timeBeforeLaunching=" + this.timeBeforeLaunching
209 + ", refreshTime=" + this.refreshTime + ", slidingWindows="
210 + this.slidingWindows + ", nbLinesRead=" + this.nbLinesRead
211 + ", displayRestarts=" + this.displayRestarts + "]";
212 }
213
214 public String[] createCommandLine(String gnuplotFilename) {
215 String rgb = Integer.toHexString(this.backgroundColor.getRGB());
216 rgb = rgb.substring(2, rgb.length());
217 String rgbBorder = Integer.toHexString(this.borderColor.getRGB());
218 rgbBorder = rgbBorder.substring(2, rgbBorder.length());
219
220 String[] cmd = new String[6];
221 cmd[0] = "gnuplot";
222 cmd[1] = "-bg";
223 cmd[2] = "#" + rgb;
224 cmd[3] = "-xrm";
225 cmd[4] = "gnuplot*borderColor:#" + rgbBorder;
226 cmd[5] = gnuplotFilename;
227
228 return cmd;
229 }
230
231 public String generatePlotLine(GnuplotDataFile file,
232 boolean slidingThisWindow) {
233 return generatePlotLine(new GnuplotDataFile[] { file }, "",
234 slidingThisWindow);
235 }
236
237 public String generatePlotLine(GnuplotDataFile file) {
238 return generatePlotLine(new GnuplotDataFile[] { file }, "",
239 this.slidingWindows);
240 }
241
242 public String generatePlotLine(GnuplotDataFile file, String restartFile) {
243 return generatePlotLine(new GnuplotDataFile[] { file }, restartFile,
244 this.slidingWindows);
245 }
246
247 public String generatePlotLine(GnuplotDataFile file, String restartFile,
248 boolean slidingThisWindows) {
249 return generatePlotLine(new GnuplotDataFile[] { file }, restartFile,
250 slidingThisWindows);
251 }
252
253 public String generatePlotLine(GnuplotDataFile file, String restartFile,
254 boolean slidingThisWindows, int nbLinesToShow) {
255 return generatePlotLine(new GnuplotDataFile[] { file },
256 new GnuplotFunction[] {}, restartFile, slidingThisWindows,
257 nbLinesToShow);
258 }
259
260 public String generatePlotLine(GnuplotDataFile[] dataFilesArray,
261 String restartFileName, boolean slidingThisWindows) {
262 return generatePlotLine(dataFilesArray, new GnuplotFunction[] {},
263 restartFileName, slidingThisWindows);
264 }
265
266 public String generatePlotLine(GnuplotDataFile file,
267 GnuplotFunction function, String restartFile,
268 boolean slidingThisWindows, int nbLinesToShow) {
269 return generatePlotLine(new GnuplotDataFile[] { file },
270 new GnuplotFunction[] { function }, restartFile,
271 slidingThisWindows, nbLinesToShow);
272 }
273
274 public String generatePlotLine(GnuplotDataFile dataFile,
275 GnuplotFunction function, String restartFileName,
276 boolean slidingThisWindows) {
277 return generatePlotLine(new GnuplotDataFile[] { dataFile },
278 new GnuplotFunction[] { function }, restartFileName,
279 slidingThisWindows);
280 }
281
282 public String generatePlotLine(GnuplotDataFile[] dataFilesArray,
283 GnuplotFunction[] functions, String restartFileName,
284 boolean slidingThisWindows) {
285 return generatePlotLine(dataFilesArray, functions, restartFileName,
286 slidingThisWindows, this.nbLinesRead);
287 }
288
289 public String generatePlotLine(GnuplotDataFile[] dataFilesArray,
290 GnuplotFunction[] functions, String restartFileName,
291 boolean slidingThisWindows, int nbLinesTosShow) {
292 String result;
293 if (restartFileName.length() == 0) {
294 result = "if(system(\"head " + dataFilesArray[0].getFilename()
295 + " | wc -l\")!=0){";
296 } else {
297 result = "if(system(\"head " + dataFilesArray[0].getFilename()
298 + " | wc -l\")!=0 && system(\"head " + restartFileName
299 + " | wc -l\")!=0){";
300 }
301
302 StringBuffer buf = new StringBuffer();
303
304 buf.append("plot");
305
306 String restartString;
307 String tailString = "";
308 if (this.slidingWindows && slidingThisWindows) {
309 tailString = "< tail -" + nbLinesTosShow + " ";
310 }
311 boolean useRestart = this.displayRestarts
312 && restartFileName.length() > 0;
313 if (useRestart) {
314 String rgb = Integer.toHexString(this.restartColor.getRGB());
315 rgb = rgb.substring(2, rgb.length());
316 restartString = "\"" + tailString + restartFileName + "\""
317 + " with impulses lc rgb \"#" + rgb
318 + "\" title \"Restart\" axis x1y2";
319 buf.append(restartString);
320 }
321 for (int i = 0; i < dataFilesArray.length; i++) {
322 String rgb = Integer.toHexString(dataFilesArray[i].getColor()
323 .getRGB());
324 rgb = rgb.substring(2, rgb.length());
325 String comma = "";
326 if (useRestart || i != 0) {
327 comma = ",";
328 }
329 String style = "";
330 if (dataFilesArray[i].getStyle().length() > 0) {
331 style = " with " + dataFilesArray[i].getStyle();
332 }
333 buf.append(comma + "\"" + tailString
334 + dataFilesArray[i].getFilename() + "\"" + style
335 + LC_RGB + rgb + TITLE
336 + dataFilesArray[i].getTitle() + AXIS_X1Y1);
337 }
338
339 for (int i = 0; i < functions.length; i++) {
340 String rgb = Integer.toHexString(functions[i].getColor().getRGB());
341 rgb = rgb.substring(2, rgb.length());
342 String comma = "";
343 if (dataFilesArray.length > 0 || useRestart || i != 0) {
344 comma = ",";
345 }
346 buf.append(comma + functions[i].getFunctionExpression()
347 + LC_RGB + rgb + TITLE
348 + functions[i].getFunctionLegend() + AXIS_X1Y1);
349 }
350 result += buf.toString() + "}";
351 return result;
352 }
353
354 public String generatePlotLineOnDifferenteAxes(GnuplotDataFile[] dfArray1,
355 GnuplotDataFile[] dfArray2, boolean slidingThisWindow) {
356 return generatePlotLineOnDifferenteAxes(dfArray1, dfArray2,
357 slidingThisWindow, this.nbLinesRead);
358 }
359
360 public String generatePlotLineOnDifferenteAxes(GnuplotDataFile[] dfArray1,
361 GnuplotDataFile[] dfArray2, boolean slidingThisWindow, int nbLines) {
362 return generatePlotLineOnDifferenteAxes(dfArray1, dfArray2,
363 new GnuplotFunction[] {}, slidingThisWindow, nbLines);
364 }
365
366 public String generatePlotLineOnDifferenteAxes(GnuplotDataFile[] dfArray1,
367 GnuplotDataFile[] dfArray2, GnuplotFunction[] functions,
368 boolean slidingThisWindow) {
369 return generatePlotLineOnDifferenteAxes(dfArray1, dfArray2,
370 new GnuplotFunction[] {}, slidingThisWindow, this.nbLinesRead);
371 }
372
373 public String generatePlotLineOnDifferenteAxes(GnuplotDataFile[] dfArray1,
374 GnuplotDataFile[] dfArray2, GnuplotFunction[] functions,
375 boolean slidingThisWindows, int nbLines) {
376
377 StringBuffer buf = new StringBuffer();
378
379 buf.append("plot ");
380
381 String tailString = "";
382 if (this.slidingWindows && slidingThisWindows) {
383 tailString = "< tail -" + nbLines + " ";
384 }
385
386 for (int i = 0; i < dfArray2.length; i++) {
387 String rgb = Integer.toHexString(dfArray2[i].getColor().getRGB());
388 rgb = rgb.substring(2, rgb.length());
389 String comma = "";
390 if (i != 0) {
391 comma = ",";
392 }
393
394 String style = "";
395 if (dfArray2[i].getStyle().length() > 0) {
396 style = " with " + dfArray2[i].getStyle();
397 }
398 buf.append(comma + "\"" + tailString + dfArray2[i].getFilename()
399 + "\"" + style + LC_RGB + rgb + TITLE
400 + dfArray2[i].getTitle() + "\" axis x1y2");
401 }
402
403 for (int i = 0; i < dfArray1.length; i++) {
404 String rgb = Integer.toHexString(dfArray1[i].getColor().getRGB());
405 rgb = rgb.substring(2, rgb.length());
406 String comma = "";
407 if (dfArray2.length > 0 || i != 0) {
408 comma = ",";
409 }
410 String style = "";
411 if (dfArray1[i].getStyle().length() > 0) {
412 style = " with " + dfArray1[i].getStyle();
413 }
414 buf.append(comma + "\"" + tailString + dfArray1[i].getFilename()
415 + "\"" + style + LC_RGB + rgb + TITLE
416 + dfArray1[i].getTitle() + AXIS_X1Y1);
417 }
418
419 for (int i = 0; i < functions.length; i++) {
420 String rgb = Integer.toHexString(functions[i].getColor().getRGB());
421 rgb = rgb.substring(2, rgb.length());
422 String comma = "";
423 if (dfArray1.length > 0 || dfArray2.length > 0 || i != 0) {
424 comma = ",";
425 }
426 buf.append(comma + functions[i].getFunctionExpression()
427 + LC_RGB + rgb + TITLE
428 + functions[i].getFunctionLegend() + AXIS_X1Y1);
429 }
430
431 return buf.toString();
432 }
433
434 }