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