1 package org.sat4j.sat.visu;
2
3 import info.monitorenter.gui.chart.Chart2D;
4 import info.monitorenter.gui.chart.IAxis.AxisTitle;
5 import info.monitorenter.gui.chart.ITrace2D;
6 import info.monitorenter.gui.chart.rangepolicies.RangePolicyHighestValues;
7 import info.monitorenter.gui.chart.traces.Trace2DLtd;
8 import info.monitorenter.gui.chart.traces.Trace2DSimple;
9 import info.monitorenter.gui.chart.traces.painters.TracePainterVerticalBar;
10
11 import java.awt.Color;
12 import java.awt.Container;
13 import java.awt.GridLayout;
14 import java.awt.event.WindowAdapter;
15 import java.awt.event.WindowEvent;
16
17 import javax.swing.JFrame;
18
19 public class JChartBasedSolverVisualisation implements SolverVisualisation {
20
21 private static final String CLEAN = "Clean";
22
23 private static final String RESTART = "Restart";
24
25
26
27
28 private static final long serialVersionUID = 1L;
29
30 private JFrame visuFrame;
31
32 private int nVar;
33
34 private Chart2D variablesEvaluationChart;
35 private Chart2D clausesEvaluationChart;
36 private Chart2D learnedClausesSizeChart;
37 private Chart2D decisionLevelWhenConflictChart;
38 private Chart2D trailLevelWhenConflictChart;
39 private Chart2D positiveDecisionVariableChart;
40 private Chart2D negativeDecisionVariableChart;
41 private Chart2D propagationPerSecondChart;
42
43 private ITrace2D positiveDecisionTrace;
44 private ITrace2D negativeDecisionTrace;
45 private ITrace2D restartPosDecisionTrace;
46 private ITrace2D restartNegDecisionTrace;
47 private ITrace2D cleanPosDecisionTrace;
48 private ITrace2D cleanNegDecisionTrace;
49
50 private ITrace2D learnedClausesSizeTrace;
51 private ITrace2D learnedClausesSizeRestartTrace;
52 private ITrace2D learnedClausesSizeCleanTrace;
53
54 private ITrace2D conflictDepthTrace;
55 private ITrace2D conflictDepthRestartTrace;
56 private ITrace2D conflictDepthCleanTrace;
57
58 private ITrace2D clausesEvaluationTrace;
59
60 private ITrace2D conflictLevelTrace;
61 private ITrace2D conflictLevelRestartTrace;
62 private ITrace2D conflictLevelCleanTrace;
63
64 private ITrace2D heuristicsTrace;
65
66 private ITrace2D speedTrace;
67 private ITrace2D speedCleanTrace;
68 private ITrace2D speedRestartTrace;
69
70 private VisuPreferences pref;
71
72 public JChartBasedSolverVisualisation(VisuPreferences pref) {
73 this.pref = pref;
74 init();
75 }
76
77 public void init() {
78 this.visuFrame = new JFrame("Visualisation");
79
80 Container c = this.visuFrame.getContentPane();
81
82 int nbGraphs = this.pref.getNumberOfDisplayedGraphs();
83 int[] nbLinesTab = new int[] { 1, 2, 3, 2 };
84
85 int nbLines = 3;
86 if (nbGraphs < 5) {
87 nbLines = nbLinesTab[nbGraphs - 1];
88 }
89
90 int nbCols = (nbGraphs - 1) / 3 + 1;
91
92 c.setLayout(new GridLayout(nbLines, nbCols, 5, 5));
93
94 initCharts();
95
96 addChartsToFrame();
97
98 initTraces();
99
100 this.visuFrame.setBackground(this.pref.getBackgroundColor());
101 this.visuFrame.setForeground(this.pref.getBorderColor());
102
103 this.visuFrame.setSize(800, 400);
104
105
106 this.visuFrame.addWindowListener(new WindowAdapter() {
107 @Override
108 public void windowClosing(WindowEvent e) {
109 visuFrame.setVisible(false);
110 }
111 });
112
113 }
114
115 public void initCharts() {
116 this.variablesEvaluationChart = new Chart2D();
117 this.clausesEvaluationChart = new Chart2D();
118 this.learnedClausesSizeChart = new Chart2D();
119 this.decisionLevelWhenConflictChart = new Chart2D();
120 this.trailLevelWhenConflictChart = new Chart2D();
121 this.positiveDecisionVariableChart = new Chart2D();
122 this.negativeDecisionVariableChart = new Chart2D();
123 this.propagationPerSecondChart = new Chart2D();
124
125 AxisTitle voidTitle = new AxisTitle("");
126 this.variablesEvaluationChart.getAxisX().setAxisTitle(voidTitle);
127 this.variablesEvaluationChart.getAxisY().setAxisTitle(voidTitle);
128 this.clausesEvaluationChart.getAxisX().setAxisTitle(voidTitle);
129 this.clausesEvaluationChart.getAxisY().setAxisTitle(voidTitle);
130 this.learnedClausesSizeChart.getAxisX().setAxisTitle(voidTitle);
131 this.learnedClausesSizeChart.getAxisY().setAxisTitle(voidTitle);
132 this.decisionLevelWhenConflictChart.getAxisX().setAxisTitle(voidTitle);
133 this.decisionLevelWhenConflictChart.getAxisY().setAxisTitle(voidTitle);
134 this.trailLevelWhenConflictChart.getAxisX().setAxisTitle(voidTitle);
135 this.trailLevelWhenConflictChart.getAxisY().setAxisTitle(voidTitle);
136 this.positiveDecisionVariableChart.getAxisX().setAxisTitle(voidTitle);
137 this.positiveDecisionVariableChart.getAxisY().setAxisTitle(voidTitle);
138 this.negativeDecisionVariableChart.getAxisX().setAxisTitle(voidTitle);
139 this.negativeDecisionVariableChart.getAxisY().setAxisTitle(voidTitle);
140 this.propagationPerSecondChart.getAxisX().setAxisTitle(voidTitle);
141 this.propagationPerSecondChart.getAxisY().setAxisTitle(voidTitle);
142 }
143
144 public void addChartsToFrame() {
145 MyChartPanel variablesEvaluationPanel = new MyChartPanel(
146 this.variablesEvaluationChart, "Variables evaluation",
147 this.pref.getBackgroundColor(), this.pref.getBorderColor());
148 MyChartPanel clausesEvaluationPanel = new MyChartPanel(
149 this.clausesEvaluationChart, "Clauses evaluation",
150 this.pref.getBackgroundColor(), this.pref.getBorderColor());
151 MyChartPanel learnedClausesSizePanel = new MyChartPanel(
152 this.learnedClausesSizeChart, "Size of learned clauses",
153 this.pref.getBackgroundColor(), this.pref.getBorderColor());
154 MyChartPanel decisionLevelWhenConflictPanel = new MyChartPanel(
155 this.decisionLevelWhenConflictChart,
156 "Decision level when conflict", this.pref.getBackgroundColor(),
157 this.pref.getBorderColor());
158 MyChartPanel trailLevelWhenConflictPanel = new MyChartPanel(
159 this.trailLevelWhenConflictChart, "Trail level when conflict",
160 this.pref.getBackgroundColor(), this.pref.getBorderColor());
161 MyChartPanel positiveDecisionVariablePanel = new MyChartPanel(
162 this.positiveDecisionVariableChart, "Positive decision phases",
163 this.pref.getBackgroundColor(), this.pref.getBorderColor());
164 MyChartPanel negativeDecisionVariablePanel = new MyChartPanel(
165 this.negativeDecisionVariableChart, "Negative decision phases",
166 this.pref.getBackgroundColor(), this.pref.getBorderColor());
167 MyChartPanel propagationPerSecondPanel = new MyChartPanel(
168 this.propagationPerSecondChart,
169 "Number of propagations per second",
170 this.pref.getBackgroundColor(), this.pref.getBorderColor());
171
172 if (this.pref.isDisplayClausesSize()) {
173 this.visuFrame.add(learnedClausesSizePanel);
174 }
175 if (this.pref.isDisplayClausesEvaluation()) {
176 this.visuFrame.add(clausesEvaluationPanel);
177 }
178 if (this.pref.isDisplayConflictsTrail()) {
179 this.visuFrame.add(trailLevelWhenConflictPanel);
180 }
181 if (this.pref.isDisplayDecisionIndexes()) {
182 this.visuFrame.add(negativeDecisionVariablePanel);
183 }
184 if (this.pref.isDisplayVariablesEvaluation()) {
185 this.visuFrame.add(variablesEvaluationPanel);
186 }
187 if (this.pref.isDisplayConflictsDecision()) {
188 this.visuFrame.add(decisionLevelWhenConflictPanel);
189 }
190 if (this.pref.isDisplayDecisionIndexes()) {
191 this.visuFrame.add(positiveDecisionVariablePanel);
192 }
193 if (this.pref.isDisplaySpeed()) {
194 this.visuFrame.add(propagationPerSecondPanel);
195 }
196 }
197
198 public void initTraces() {
199 this.positiveDecisionTrace = new Trace2DSimple("Positive decision");
200 this.positiveDecisionTrace.setTracePainter(new TracePainterPlus());
201 this.positiveDecisionTrace.setColor(new Color(0f, 0.78f, 0.09f));
202
203 this.negativeDecisionTrace = new Trace2DSimple("Negative decision");
204 this.negativeDecisionTrace.setTracePainter(new TracePainterPlus());
205 this.negativeDecisionTrace.setColor(Color.RED);
206
207 this.restartPosDecisionTrace = new Trace2DSimple(RESTART);
208 this.restartPosDecisionTrace
209 .setTracePainter(new TracePainterVerticalBar(2,
210 this.positiveDecisionVariableChart));
211 this.restartPosDecisionTrace.setColor(Color.LIGHT_GRAY);
212
213 this.restartNegDecisionTrace = new Trace2DSimple(RESTART);
214 this.restartNegDecisionTrace
215 .setTracePainter(new TracePainterVerticalBar(2,
216 this.negativeDecisionVariableChart));
217 this.restartNegDecisionTrace.setColor(Color.LIGHT_GRAY);
218
219 this.cleanPosDecisionTrace = new Trace2DSimple(CLEAN);
220 this.cleanPosDecisionTrace.setTracePainter(new TracePainterVerticalBar(
221 2, this.positiveDecisionVariableChart));
222 this.cleanPosDecisionTrace.setColor(Color.ORANGE);
223
224 this.cleanNegDecisionTrace = new Trace2DSimple(CLEAN);
225 this.cleanNegDecisionTrace.setTracePainter(new TracePainterVerticalBar(
226 2, this.negativeDecisionVariableChart));
227 this.cleanNegDecisionTrace.setColor(Color.ORANGE);
228
229 this.positiveDecisionVariableChart.addTrace(this.positiveDecisionTrace);
230 this.positiveDecisionVariableChart
231 .addTrace(this.restartPosDecisionTrace);
232 this.positiveDecisionVariableChart.addTrace(this.cleanPosDecisionTrace);
233 this.positiveDecisionTrace.setZIndex(ITrace2D.ZINDEX_MAX);
234
235 this.positiveDecisionVariableChart.getAxisX().setRangePolicy(
236 new RangePolicyHighestValues(8000));
237
238 this.negativeDecisionVariableChart
239 .addTrace(this.restartNegDecisionTrace);
240 this.negativeDecisionVariableChart.addTrace(this.cleanNegDecisionTrace);
241 this.negativeDecisionVariableChart.addTrace(this.negativeDecisionTrace);
242 this.negativeDecisionTrace.setZIndex(ITrace2D.ZINDEX_MAX);
243 this.negativeDecisionVariableChart.getAxisX().setRangePolicy(
244 this.positiveDecisionVariableChart.getAxisX().getRangePolicy());
245
246 this.conflictDepthTrace = new Trace2DLtd(15000, "Trail level");
247 this.conflictDepthTrace.setTracePainter(new TracePainterPlus());
248 this.conflictDepthTrace.setColor(Color.MAGENTA);
249 this.trailLevelWhenConflictChart
250 .setName("Trail level when the conflict occurs");
251 this.trailLevelWhenConflictChart.addTrace(this.conflictDepthTrace);
252 this.conflictDepthTrace.setZIndex(ITrace2D.ZINDEX_MAX);
253
254 this.conflictDepthRestartTrace = new Trace2DSimple(RESTART);
255 this.conflictDepthRestartTrace
256 .setTracePainter(new TracePainterVerticalBar(2,
257 this.trailLevelWhenConflictChart));
258 this.conflictDepthRestartTrace.setColor(Color.LIGHT_GRAY);
259 this.trailLevelWhenConflictChart
260 .addTrace(this.conflictDepthRestartTrace);
261
262 this.conflictDepthCleanTrace = new Trace2DSimple(CLEAN);
263 this.conflictDepthCleanTrace
264 .setTracePainter(new TracePainterVerticalBar(2,
265 this.trailLevelWhenConflictChart));
266 this.conflictDepthCleanTrace.setColor(Color.ORANGE);
267 this.trailLevelWhenConflictChart.addTrace(this.conflictDepthCleanTrace);
268 this.trailLevelWhenConflictChart.getAxisX().setRangePolicy(
269 new RangePolicyHighestValues(2000));
270
271 this.conflictLevelTrace = new Trace2DSimple("Decision level");
272 this.conflictLevelTrace.setTracePainter(new TracePainterPlus());
273 this.conflictLevelTrace.setColor(Color.MAGENTA);
274 this.decisionLevelWhenConflictChart
275 .setName("Decision level chen the conflict occurs");
276 this.decisionLevelWhenConflictChart.addTrace(this.conflictLevelTrace);
277 this.conflictLevelTrace.setZIndex(ITrace2D.ZINDEX_MAX);
278
279 this.conflictLevelRestartTrace = new Trace2DSimple(RESTART);
280 this.conflictLevelRestartTrace
281 .setTracePainter(new TracePainterVerticalBar(2,
282 this.decisionLevelWhenConflictChart));
283 this.conflictLevelRestartTrace.setColor(Color.LIGHT_GRAY);
284 this.decisionLevelWhenConflictChart
285 .addTrace(this.conflictLevelRestartTrace);
286
287 this.conflictLevelCleanTrace = new Trace2DSimple(CLEAN);
288 this.conflictLevelCleanTrace
289 .setTracePainter(new TracePainterVerticalBar(2,
290 this.decisionLevelWhenConflictChart));
291 this.conflictLevelCleanTrace.setColor(Color.ORANGE);
292 this.decisionLevelWhenConflictChart
293 .addTrace(this.conflictLevelCleanTrace);
294
295 this.decisionLevelWhenConflictChart.getAxisX().setRangePolicy(
296 new RangePolicyHighestValues(2000));
297
298 this.learnedClausesSizeTrace = new Trace2DSimple("Size");
299 this.learnedClausesSizeTrace.setTracePainter(new TracePainterPlus());
300 this.learnedClausesSizeTrace.setColor(Color.BLUE);
301 this.learnedClausesSizeChart.setName("Learned clauses size");
302 this.learnedClausesSizeChart.addTrace(this.learnedClausesSizeTrace);
303 this.learnedClausesSizeTrace.setZIndex(ITrace2D.ZINDEX_MAX);
304 this.learnedClausesSizeChart.getAxisX().setRangePolicy(
305 new RangePolicyHighestValues(2000));
306
307 this.learnedClausesSizeRestartTrace = new Trace2DSimple(RESTART);
308 this.learnedClausesSizeRestartTrace
309 .setTracePainter(new TracePainterVerticalBar(2,
310 this.learnedClausesSizeChart));
311 this.learnedClausesSizeRestartTrace.setColor(Color.LIGHT_GRAY);
312 this.learnedClausesSizeChart
313 .addTrace(this.learnedClausesSizeRestartTrace);
314
315 this.learnedClausesSizeCleanTrace = new Trace2DSimple(CLEAN);
316 this.learnedClausesSizeCleanTrace
317 .setTracePainter(new TracePainterVerticalBar(2,
318 this.learnedClausesSizeChart));
319 this.learnedClausesSizeCleanTrace.setColor(Color.ORANGE);
320 this.learnedClausesSizeChart
321 .addTrace(this.learnedClausesSizeCleanTrace);
322
323 this.clausesEvaluationTrace = new Trace2DSimple("Evaluation");
324 this.clausesEvaluationTrace.setTracePainter(new TracePainterPlus());
325 this.clausesEvaluationTrace.setColor(Color.BLUE);
326 this.clausesEvaluationTrace.setName("Clauses evaluation");
327 this.clausesEvaluationChart.addTrace(this.clausesEvaluationTrace);
328
329 this.heuristicsTrace = new Trace2DSimple("Evaluation");
330 this.heuristicsTrace.setTracePainter(new TracePainterPlus());
331 this.heuristicsTrace.setColor(Color.ORANGE);
332 this.variablesEvaluationChart.setName("Variables evaluation");
333 this.variablesEvaluationChart.addTrace(this.heuristicsTrace);
334
335 this.speedTrace = new Trace2DSimple("Speed");
336 this.speedTrace.setColor(new Color(0.02f, .78f, .76f));
337 this.speedCleanTrace = new Trace2DSimple(CLEAN);
338 this.speedCleanTrace.setColor(Color.ORANGE);
339 this.speedCleanTrace.setTracePainter(new TracePainterVerticalBar(2,
340 this.propagationPerSecondChart));
341 this.speedRestartTrace = new Trace2DSimple(RESTART);
342 this.speedRestartTrace.setColor(Color.LIGHT_GRAY);
343 this.speedRestartTrace.setTracePainter(new TracePainterVerticalBar(2,
344 this.propagationPerSecondChart));
345
346 this.propagationPerSecondChart.addTrace(this.speedCleanTrace);
347 this.propagationPerSecondChart.addTrace(this.speedRestartTrace);
348 this.propagationPerSecondChart.addTrace(this.speedTrace);
349 this.propagationPerSecondChart.getAxisX().setRangePolicy(
350 new RangePolicyHighestValues(30));
351
352 this.speedTrace.setZIndex(ITrace2D.ZINDEX_MAX);
353
354 }
355
356 public void setVisible(boolean b) {
357 this.visuFrame.setVisible(b);
358 }
359
360 public ITrace2D getPositiveDecisionTrace() {
361 return this.positiveDecisionTrace;
362 }
363
364 public void setPositiveDecisionTrace(ITrace2D positiveDecisionTrace) {
365 this.positiveDecisionTrace = positiveDecisionTrace;
366 }
367
368 public ITrace2D getNegativeDecisionTrace() {
369 return this.negativeDecisionTrace;
370 }
371
372 public void setNegativeDecisionTrace(ITrace2D negativeDecisionTrace) {
373 this.negativeDecisionTrace = negativeDecisionTrace;
374 }
375
376 public ITrace2D getRestartNegDecisionTrace() {
377 return this.restartNegDecisionTrace;
378 }
379
380 public void setRestartNegDecisionTrace(ITrace2D restartNegDecisionTrace) {
381 this.restartNegDecisionTrace = restartNegDecisionTrace;
382 }
383
384 public ITrace2D getRestartPosDecisionTrace() {
385 return this.restartPosDecisionTrace;
386 }
387
388 public void setRestartPosDecisionTrace(ITrace2D restartPosDecisionTrace) {
389 this.restartPosDecisionTrace = restartPosDecisionTrace;
390 }
391
392 public ITrace2D getConflictDepthTrace() {
393 return this.conflictDepthTrace;
394 }
395
396 public void setConflictDepthTrace(ITrace2D conflictDepthTrace) {
397 this.conflictDepthTrace = conflictDepthTrace;
398 }
399
400 public ITrace2D getLearnedClausesSizeTrace() {
401 return this.learnedClausesSizeTrace;
402 }
403
404 public void setLearnedClausesSizeTrace(ITrace2D learnedClausesSizeTrace) {
405 this.learnedClausesSizeTrace = learnedClausesSizeTrace;
406 }
407
408 public ITrace2D getClausesEvaluationTrace() {
409 return this.clausesEvaluationTrace;
410 }
411
412 public void setClausesEvaluationTrace(ITrace2D clausesEvaluationTrace) {
413 this.clausesEvaluationTrace = clausesEvaluationTrace;
414 }
415
416 public ITrace2D getConflictLevelTrace() {
417 return this.conflictLevelTrace;
418 }
419
420 public void setConflictLevelTrace(ITrace2D conflictLevelTrace) {
421 this.conflictLevelTrace = conflictLevelTrace;
422 }
423
424 public ITrace2D getConflictLevelRestartTrace() {
425 return this.conflictLevelRestartTrace;
426 }
427
428 public void setConflictLevelRestartTrace(ITrace2D conflictLevelRestartTrace) {
429 this.conflictLevelRestartTrace = conflictLevelRestartTrace;
430 }
431
432 public ITrace2D getHeuristicsTrace() {
433 return this.heuristicsTrace;
434 }
435
436 public void setHeuristicsTrace(ITrace2D heuristicsTrace) {
437 this.heuristicsTrace = heuristicsTrace;
438 }
439
440 public ITrace2D getSpeedTrace() {
441 return this.speedTrace;
442 }
443
444 public void setSpeedTrace(ITrace2D speedTrace) {
445 this.speedTrace = speedTrace;
446 }
447
448 public ITrace2D getSpeedCleanTrace() {
449 return this.speedCleanTrace;
450 }
451
452 public void setSpeedCleanTrace(ITrace2D speedCleanTrace) {
453 this.speedCleanTrace = speedCleanTrace;
454 }
455
456 public ITrace2D getSpeedRestartTrace() {
457 return this.speedRestartTrace;
458 }
459
460 public void setSpeedRestartTrace(ITrace2D speedRestartTrace) {
461 this.speedRestartTrace = speedRestartTrace;
462 }
463
464 public ITrace2D getConflictDepthRestartTrace() {
465 return this.conflictDepthRestartTrace;
466 }
467
468 public void setConflictDepthRestartTrace(ITrace2D conflictDepthRestartTrace) {
469 this.conflictDepthRestartTrace = conflictDepthRestartTrace;
470 }
471
472 public ITrace2D getLearnedClausesSizeRestartTrace() {
473 return this.learnedClausesSizeRestartTrace;
474 }
475
476 public void setLearnedClausesSizeRestartTrace(
477 ITrace2D learnedClausesSizeRestartTrace) {
478 this.learnedClausesSizeRestartTrace = learnedClausesSizeRestartTrace;
479 }
480
481 public ITrace2D getLearnedClausesSizeCleanTrace() {
482 return this.learnedClausesSizeCleanTrace;
483 }
484
485 public void setLearnedClausesSizeCleanTrace(
486 ITrace2D learnedClausesSizeCleanTrace) {
487 this.learnedClausesSizeCleanTrace = learnedClausesSizeCleanTrace;
488 }
489
490 public ITrace2D getConflictLevelCleanTrace() {
491 return this.conflictLevelCleanTrace;
492 }
493
494 public void setConflictLevelCleanTrace(ITrace2D conflictLevelCleanTrace) {
495 this.conflictLevelCleanTrace = conflictLevelCleanTrace;
496 }
497
498 public ITrace2D getConflictDepthCleanTrace() {
499 return this.conflictDepthCleanTrace;
500 }
501
502 public void setConflictDepthCleanTrace(ITrace2D conflictDepthCleanTrace) {
503 this.conflictDepthCleanTrace = conflictDepthCleanTrace;
504 }
505
506 public ITrace2D getCleanPosDecisionTrace() {
507 return this.cleanPosDecisionTrace;
508 }
509
510 public void setCleanPosDecisionTrace(ITrace2D cleanPosDecisionTrace) {
511 this.cleanPosDecisionTrace = cleanPosDecisionTrace;
512 }
513
514 public ITrace2D getCleanNegDecisionTrace() {
515 return this.cleanNegDecisionTrace;
516 }
517
518 public void setCleanNegDecisionTrace(ITrace2D cleanNegDecisionTrace) {
519 this.cleanNegDecisionTrace = cleanNegDecisionTrace;
520 }
521
522 public int getnVar() {
523 return this.nVar;
524 }
525
526 public void setnVar(int nVar) {
527 this.nVar = nVar;
528 }
529
530 public void start() {
531 this.visuFrame.setVisible(true);
532 }
533
534 public void end() {
535 this.visuFrame.setVisible(false);
536 }
537
538 }