1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30 package org.sat4j.sat;
31
32 import java.awt.BorderLayout;
33 import java.awt.Dimension;
34 import java.awt.FlowLayout;
35 import java.awt.event.ActionEvent;
36 import java.awt.event.ActionListener;
37 import java.io.File;
38 import java.io.FileNotFoundException;
39 import java.io.FileOutputStream;
40 import java.io.IOException;
41 import java.io.PrintStream;
42 import java.io.PrintWriter;
43 import java.io.StringWriter;
44 import java.util.ArrayList;
45 import java.util.Collections;
46 import java.util.List;
47
48 import javax.swing.BoxLayout;
49 import javax.swing.ButtonGroup;
50 import javax.swing.JButton;
51 import javax.swing.JCheckBox;
52 import javax.swing.JComboBox;
53 import javax.swing.JFileChooser;
54 import javax.swing.JLabel;
55 import javax.swing.JPanel;
56 import javax.swing.JRadioButton;
57 import javax.swing.JScrollPane;
58 import javax.swing.JTabbedPane;
59 import javax.swing.JTextArea;
60 import javax.swing.JTextField;
61 import javax.swing.border.CompoundBorder;
62 import javax.swing.border.EmptyBorder;
63 import javax.swing.border.TitledBorder;
64
65 import org.sat4j.core.ASolverFactory;
66 import org.sat4j.minisat.core.ICDCL;
67 import org.sat4j.minisat.core.ICDCLLogger;
68 import org.sat4j.minisat.core.IOrder;
69 import org.sat4j.minisat.core.IPhaseSelectionStrategy;
70 import org.sat4j.minisat.core.LearnedConstraintsEvaluationType;
71 import org.sat4j.minisat.core.RestartStrategy;
72 import org.sat4j.minisat.core.SearchParams;
73 import org.sat4j.minisat.core.SimplificationType;
74 import org.sat4j.minisat.orders.RandomWalkDecorator;
75 import org.sat4j.minisat.orders.VarOrderHeap;
76 import org.sat4j.pb.IPBSolver;
77 import org.sat4j.pb.OptToPBSATAdapter;
78 import org.sat4j.pb.PseudoOptDecorator;
79 import org.sat4j.pb.core.IPBCDCLSolver;
80 import org.sat4j.pb.orders.RandomWalkDecoratorObjective;
81 import org.sat4j.pb.orders.VarOrderHeapObjective;
82 import org.sat4j.pb.reader.PBInstanceReader;
83 import org.sat4j.reader.InstanceReader;
84 import org.sat4j.reader.ParseFormatException;
85 import org.sat4j.reader.Reader;
86 import org.sat4j.sat.visu.ChartBasedVisualizationTool;
87 import org.sat4j.sat.visu.GnuplotBasedSolverVisualisation;
88 import org.sat4j.sat.visu.JChartBasedSolverVisualisation;
89 import org.sat4j.sat.visu.SolverVisualisation;
90 import org.sat4j.sat.visu.TraceComposite;
91 import org.sat4j.sat.visu.VisuPreferences;
92 import org.sat4j.specs.ContradictionException;
93 import org.sat4j.specs.IConstr;
94 import org.sat4j.specs.IProblem;
95 import org.sat4j.specs.ISolver;
96 import org.sat4j.specs.ISolverService;
97 import org.sat4j.specs.Lbool;
98 import org.sat4j.specs.SearchListener;
99 import org.sat4j.specs.TimeoutException;
100 import org.sat4j.tools.ConflictDepthTracing;
101 import org.sat4j.tools.ConflictLevelTracing;
102 import org.sat4j.tools.DecisionTracing;
103 import org.sat4j.tools.FileBasedVisualizationTool;
104 import org.sat4j.tools.HeuristicsTracing;
105 import org.sat4j.tools.LearnedClausesSizeTracing;
106 import org.sat4j.tools.LearnedTracing;
107 import org.sat4j.tools.MultiTracing;
108 import org.sat4j.tools.SpeedTracing;
109
110
111
112
113
114
115
116
117
118 public class DetailedCommandPanel extends JPanel implements SolverController,
119 SearchListener, ICDCLLogger {
120
121 private static final long serialVersionUID = 1L;
122
123 public static final EmptyBorder border5 = new EmptyBorder(5, 5, 5, 5);
124
125 private String ramdisk;
126
127 private RemoteControlStrategy telecomStrategy;
128 private RandomWalkDecorator randomWalk;
129 private ICDCL solver;
130 private Reader reader;
131 private IProblem problem;
132 private boolean optimizationMode = false;
133
134 private String[] commandLines;
135
136 private boolean firstStart;
137
138
139
140
141 private StartSolverEnum startConfig;
142
143 private Thread solveurThread;
144
145 private StringWriter stringWriter;
146
147 private MyTabbedPane tabbedPane;
148
149 private JPanel aboutSolverPanel;
150 private JTextArea textArea;
151
152 private JPanel instancePanel;
153 private final static String INSTANCE_PANEL = "Instance";
154 private JLabel instanceLabel;
155 private final static String INSTANCE = "Path to instance: ";
156 private JTextField instancePathField;
157 private String instancePath;
158 private JButton browseButton;
159 private final static String BROWSE = "Browse";
160
161 private String whereToWriteFiles;
162
163 private final static String MINISAT_PREFIX = "minisat";
164 private final static String PB_PREFIX = "pb";
165 private JPanel choixSolverPanel;
166 private final static String CHOIX_SOLVER_PANEL = "Solver";
167 private JLabel choixSolver;
168 private final static String CHOIX_SOLVER = "Choose solver: ";
169 private String selectedSolver;
170 private JComboBox listeSolvers;
171
172 private final static String OPTMIZATION_MODE = "Use optimization mode";
173 private JCheckBox optimisationModeCB;
174
175
176
177
178
179 private JRadioButton solverLineParamLineRadio;
180 private JRadioButton solverLineParamRemoteRadio;
181 private JRadioButton solverListParamListRadio;
182 private JRadioButton solverListParamRemoteRadio;
183 private ButtonGroup solverConfigGroup;
184
185 private final static String SOLVER_LINE_PARAM_LINE_CONFIG = "Start customized solver as given in command line";
186 private final static String SOLVER_LINE_PARAM_REMOTE_CONFIG = "Start customized solver as given in command line with configuration given in the remote";
187 private final static String SOLVER_LIST_PARAM_LIST_CONFIG = "Start solver as chosen in list with its default configuration";
188 private final static String SOLVER_LIST_PARAM_REMOTE_CONFIG = "Start solver as chosen in list with configuration given in the remote";
189
190 private JLabel chooseStartConfigLabel;
191 private final static String CHOOSE_START_CONFIG = "Choose start configuration : ";
192
193 private JButton startStopButton;
194 private static final String START = "Start";
195 private static final String STOP = "Stop";
196
197 private JButton pauseButton;
198 private static final String PAUSE = "Pause";
199 private static final String RESUME = "Resume";
200
201
202 private final static String RESTART_PANEL = "Restart strategy";
203 private RestartCommandComponent restartPanel;
204
205 private final static String RW_PANEL = "Random Walk";
206 private RandomWalkCommandComponent rwPanel;
207
208 private final static String CLEAN_PANEL = "Learned Constraint Deletion Strategy";
209 private CleanCommandComponent cleanPanel;
210
211 private PhaseCommandComponent phasePanel;
212 private final static String PHASE_PANEL = "Phase Strategy";
213
214 private SimplifierCommandComponent simplifierPanel;
215 private final static String SIMPLIFIER_PANEL = "Simplification strategy";
216
217 private HotSolverCommandComponent hotSolverPanel;
218 private final static String HOT_SOLVER_PANEL = "Hot solver";
219
220 private JTextArea console;
221 private JScrollPane scrollPane;
222
223 private boolean isPlotActivated;
224
225 private SolverVisualisation solverVisu;
226 private VisuPreferences visuPreferences;
227
228 private boolean gnuplotBased = false;
229 private boolean chartBased = false;
230
231 private RemoteControlFrame frame;
232
233 public DetailedCommandPanel(String filename, RemoteControlFrame frame) {
234 this(filename, "", frame);
235 }
236
237 public DetailedCommandPanel(String filename, String ramdisk,
238 RemoteControlFrame frame) {
239 this(filename, ramdisk, null, frame);
240 }
241
242 public DetailedCommandPanel(String filename, String ramdisk, String[] args,
243 RemoteControlFrame frame) {
244 super();
245
246 this.frame = frame;
247
248 this.visuPreferences = new VisuPreferences();
249
250 this.telecomStrategy = new RemoteControlStrategy(this);
251 this.instancePath = filename;
252 this.ramdisk = ramdisk;
253
254 this.console = new JTextArea();
255
256 this.commandLines = args;
257 if (args.length > 0) {
258 this.solver = Solvers.configureSolver(args, this);
259 }
260
261 this.isPlotActivated = false;
262
263 if (this.solver != null) {
264 this.startConfig = StartSolverEnum.SOLVER_LINE_PARAM_LINE;
265 } else {
266 this.startConfig = StartSolverEnum.SOLVER_LIST_PARAM_DEFAULT;
267 }
268
269 this.firstStart = true;
270
271 this.setPreferredSize(new Dimension(750, 800));
272 this.setLayout(new BoxLayout(this, BoxLayout.Y_AXIS));
273
274 createInstancePanel();
275 createChoixSolverPanel();
276
277 this.restartPanel = new RestartCommandComponent(RESTART_PANEL, this,
278 this.telecomStrategy.getRestartStrategy().getClass()
279 .getSimpleName());
280 this.rwPanel = new RandomWalkCommandComponent(RW_PANEL, this);
281 this.cleanPanel = new CleanCommandComponent(CLEAN_PANEL, this);
282 this.phasePanel = new PhaseCommandComponent(PHASE_PANEL, this,
283 this.telecomStrategy.getPhaseSelectionStrategy().getClass()
284 .getSimpleName());
285 this.simplifierPanel = new SimplifierCommandComponent(SIMPLIFIER_PANEL,
286 this);
287 this.hotSolverPanel = new HotSolverCommandComponent(HOT_SOLVER_PANEL,
288 this);
289
290 this.scrollPane = new JScrollPane(this.console);
291
292
293 this.scrollPane.setPreferredSize(new Dimension(400, 200));
294 this.scrollPane.getVerticalScrollBar().setValue(
295 this.scrollPane.getVerticalScrollBar().getMaximum());
296
297
298 this.tabbedPane = new MyTabbedPane();
299
300 JPanel solverBigPanel = new JPanel();
301 solverBigPanel
302 .setLayout(new BoxLayout(solverBigPanel, BoxLayout.Y_AXIS));
303 solverBigPanel.add(this.instancePanel);
304 solverBigPanel.add(this.choixSolverPanel);
305
306 this.tabbedPane.addTab("Solver", null, solverBigPanel,
307 "instance & solver options");
308
309 JPanel restartBigPanel = new JPanel();
310 restartBigPanel.setLayout(new BoxLayout(restartBigPanel,
311 BoxLayout.Y_AXIS));
312 restartBigPanel.add(this.restartPanel);
313
314
315 this.tabbedPane.addTab("Restart", null, restartBigPanel,
316 "restart strategy & options");
317
318 JPanel rwPhaseBigPanel = new JPanel();
319 rwPhaseBigPanel.setLayout(new BoxLayout(rwPhaseBigPanel,
320 BoxLayout.Y_AXIS));
321 rwPhaseBigPanel.add(this.rwPanel);
322 rwPhaseBigPanel.add(this.phasePanel);
323 rwPhaseBigPanel.add(this.hotSolverPanel);
324
325 this.tabbedPane.addTab("Heuristics", null, rwPhaseBigPanel,
326 "random walk and phase strategy");
327
328 JPanel clausesBigPanel = new JPanel();
329 clausesBigPanel.setLayout(new BoxLayout(clausesBigPanel,
330 BoxLayout.Y_AXIS));
331 clausesBigPanel.add(this.cleanPanel);
332 clausesBigPanel.add(this.simplifierPanel);
333
334 this.tabbedPane.addTab("Learned Constraints", null, clausesBigPanel,
335 "deletion and simplification strategy");
336
337 this.aboutSolverPanel = new JPanel();
338 this.textArea = new JTextArea("No solver is running at the moment");
339 this.textArea.setColumns(50);
340 this.aboutSolverPanel.add(this.textArea);
341
342 this.tabbedPane.addTab("About Solver", null, this.aboutSolverPanel,
343 "information about solver");
344
345 this.add(this.tabbedPane);
346 this.add(this.scrollPane);
347
348 this.restartPanel.setRestartPanelEnabled(false);
349 this.rwPanel.setRWPanelEnabled(false);
350 this.cleanPanel.setCleanPanelEnabled(false);
351 this.phasePanel.setPhasePanelEnabled(false);
352 this.simplifierPanel.setSimplifierPanelEnabled(false);
353 this.hotSolverPanel.setKeepSolverHotPanelEnabled(false);
354
355 this.solverVisu = new JChartBasedSolverVisualisation(
356 this.visuPreferences);
357
358 updateWriter();
359 }
360
361 public void createInstancePanel() {
362 this.instancePanel = new JPanel();
363
364 this.instancePanel.setName(INSTANCE_PANEL);
365 this.instancePanel.setBorder(new CompoundBorder(new TitledBorder(null,
366 this.instancePanel.getName(), TitledBorder.LEFT,
367 TitledBorder.TOP), border5));
368
369 this.instancePanel.setLayout(new BorderLayout(0, 0));
370
371 this.instanceLabel = new JLabel(INSTANCE);
372 this.instancePathField = new JTextField(20);
373 this.instancePathField.setText(this.instancePath);
374
375 this.instanceLabel.setLabelFor(this.instancePathField);
376
377 JPanel tmpPanel1 = new JPanel();
378 tmpPanel1.add(this.instanceLabel);
379 tmpPanel1.add(this.instancePathField);
380
381 this.browseButton = new JButton(BROWSE);
382
383 this.browseButton.addActionListener(new ActionListener() {
384 public void actionPerformed(ActionEvent e) {
385 openFileChooser();
386 }
387 });
388
389 JPanel tmpPanel2 = new JPanel();
390 tmpPanel2.add(this.browseButton);
391
392 this.instancePanel.add(tmpPanel1, BorderLayout.CENTER);
393 }
394
395 public void createChoixSolverPanel() {
396 this.choixSolverPanel = new JPanel();
397
398 this.choixSolverPanel.setName(CHOIX_SOLVER_PANEL);
399 this.choixSolverPanel.setBorder(new CompoundBorder(new TitledBorder(
400 null, this.choixSolverPanel.getName(), TitledBorder.LEFT,
401 TitledBorder.TOP), border5));
402
403 this.choixSolverPanel.setLayout(new BorderLayout());
404
405 this.choixSolver = new JLabel(CHOIX_SOLVER);
406 updateListOfSolvers();
407
408 this.optimisationModeCB = new JCheckBox(OPTMIZATION_MODE);
409 this.optimisationModeCB.setSelected(this.optimizationMode);
410
411 JPanel tmpPanel1 = new JPanel();
412 tmpPanel1.add(this.choixSolver);
413 tmpPanel1.add(this.listeSolvers);
414 tmpPanel1.add(this.optimisationModeCB);
415
416 this.optimisationModeCB.addActionListener(new ActionListener() {
417 public void actionPerformed(ActionEvent e) {
418 DetailedCommandPanel.this.optimizationMode = DetailedCommandPanel.this.optimisationModeCB
419 .isSelected();
420 log("use optimization mode: "
421 + DetailedCommandPanel.this.optimizationMode);
422 }
423 });
424
425 this.startStopButton = new JButton(START);
426
427 this.startStopButton.addActionListener(new ActionListener() {
428 public void actionPerformed(ActionEvent e) {
429 if (DetailedCommandPanel.this.startStopButton.getText().equals(
430 START)) {
431
432 launchSolverWithConfigs();
433 DetailedCommandPanel.this.pauseButton.setEnabled(true);
434 setInstancePanelEnabled(false);
435 DetailedCommandPanel.this.restartPanel
436 .setRestartPanelEnabled(true);
437 DetailedCommandPanel.this.rwPanel.setRWPanelEnabled(true);
438 DetailedCommandPanel.this.cleanPanel
439 .setCleanPanelEnabled(true);
440 DetailedCommandPanel.this.cleanPanel
441 .setCleanPanelOriginalStrategyEnabled(true);
442 DetailedCommandPanel.this.phasePanel
443 .setPhasePanelEnabled(true);
444 setChoixSolverPanelEnabled(false);
445 DetailedCommandPanel.this.simplifierPanel
446 .setSimplifierPanelEnabled(true);
447 DetailedCommandPanel.this.hotSolverPanel
448 .setKeepSolverHotPanelEnabled(true);
449 DetailedCommandPanel.this.startStopButton.setText(STOP);
450 getThis().paintAll(getThis().getGraphics());
451 DetailedCommandPanel.this.frame
452 .setActivateTracingEditableUnderCondition(false);
453 } else {
454
455
456 ((ISolver) DetailedCommandPanel.this.problem)
457 .expireTimeout();
458 DetailedCommandPanel.this.pauseButton.setEnabled(false);
459 log("Asked the solver to stop");
460 setInstancePanelEnabled(true);
461 setChoixSolverPanelEnabled(true);
462
463
464
465
466
467
468 DetailedCommandPanel.this.startStopButton.setText(START);
469 getThis().paintAll(getThis().getGraphics());
470 DetailedCommandPanel.this.frame
471 .setActivateTracingEditable(true);
472
473 }
474 }
475 });
476
477 this.pauseButton = new JButton(PAUSE);
478 this.pauseButton.setEnabled(false);
479
480 this.pauseButton.addActionListener(new ActionListener() {
481 public void actionPerformed(ActionEvent e) {
482 if (DetailedCommandPanel.this.pauseButton.getText().equals(
483 PAUSE)) {
484 DetailedCommandPanel.this.pauseButton.setText(RESUME);
485 DetailedCommandPanel.this.telecomStrategy
486 .setInterrupted(true);
487 } else {
488 DetailedCommandPanel.this.pauseButton.setText(PAUSE);
489 DetailedCommandPanel.this.telecomStrategy
490 .setInterrupted(false);
491 }
492
493 }
494 });
495
496 JPanel tmpPanel2 = new JPanel();
497 tmpPanel2.setLayout(new FlowLayout());
498 tmpPanel2.add(this.startStopButton);
499 tmpPanel2.add(this.pauseButton);
500
501 this.solverLineParamLineRadio = new JRadioButton(
502 SOLVER_LINE_PARAM_LINE_CONFIG);
503 this.solverLineParamRemoteRadio = new JRadioButton(
504 SOLVER_LINE_PARAM_REMOTE_CONFIG);
505 this.solverListParamRemoteRadio = new JRadioButton(
506 SOLVER_LIST_PARAM_REMOTE_CONFIG);
507 this.solverListParamListRadio = new JRadioButton(
508 SOLVER_LIST_PARAM_LIST_CONFIG);
509
510 this.solverConfigGroup = new ButtonGroup();
511 this.solverConfigGroup.add(this.solverLineParamLineRadio);
512 this.solverConfigGroup.add(this.solverLineParamRemoteRadio);
513 this.solverConfigGroup.add(this.solverListParamListRadio);
514 this.solverConfigGroup.add(this.solverListParamRemoteRadio);
515
516 this.chooseStartConfigLabel = new JLabel(CHOOSE_START_CONFIG);
517
518 JPanel tmpPanel3 = new JPanel();
519 tmpPanel3.setLayout(new BoxLayout(tmpPanel3, BoxLayout.Y_AXIS));
520
521 tmpPanel3.add(this.chooseStartConfigLabel);
522 tmpPanel3.add(this.solverLineParamLineRadio);
523 tmpPanel3.add(this.solverLineParamRemoteRadio);
524 tmpPanel3.add(this.solverListParamListRadio);
525 tmpPanel3.add(this.solverListParamRemoteRadio);
526
527 this.solverLineParamLineRadio.addActionListener(new ActionListener() {
528 public void actionPerformed(ActionEvent e) {
529 if (DetailedCommandPanel.this.solverLineParamLineRadio
530 .isSelected()) {
531 DetailedCommandPanel.this.startConfig = StartSolverEnum.SOLVER_LINE_PARAM_LINE;
532 }
533 }
534 });
535
536 this.solverLineParamRemoteRadio.addActionListener(new ActionListener() {
537 public void actionPerformed(ActionEvent e) {
538 if (DetailedCommandPanel.this.solverLineParamRemoteRadio
539 .isSelected()) {
540 DetailedCommandPanel.this.startConfig = StartSolverEnum.SOLVER_LINE_PARAM_REMOTE;
541 }
542 }
543 });
544
545 this.solverListParamListRadio.addActionListener(new ActionListener() {
546 public void actionPerformed(ActionEvent e) {
547 if (DetailedCommandPanel.this.solverListParamListRadio
548 .isSelected()) {
549 DetailedCommandPanel.this.startConfig = StartSolverEnum.SOLVER_LIST_PARAM_DEFAULT;
550 }
551 }
552 });
553
554 this.solverListParamRemoteRadio.addActionListener(new ActionListener() {
555 public void actionPerformed(ActionEvent e) {
556 if (DetailedCommandPanel.this.solverListParamRemoteRadio
557 .isSelected()) {
558 DetailedCommandPanel.this.startConfig = StartSolverEnum.SOLVER_LIST_PARAM_REMOTE;
559 }
560 }
561 });
562
563 setChoixSolverPanelEnabled(true);
564
565 if (this.solver == null) {
566 this.solverLineParamLineRadio.setEnabled(false);
567 this.solverLineParamRemoteRadio.setEnabled(false);
568 }
569
570 if (this.firstStart) {
571 this.solverLineParamRemoteRadio.setEnabled(false);
572 this.solverListParamRemoteRadio.setEnabled(false);
573 }
574
575 this.choixSolverPanel.add(tmpPanel1, BorderLayout.NORTH);
576 this.choixSolverPanel.add(tmpPanel3, BorderLayout.CENTER);
577 this.choixSolverPanel.add(tmpPanel2, BorderLayout.SOUTH);
578 }
579
580 public String getStartStopText() {
581 return this.startStopButton.getText();
582 }
583
584 public void setOptimisationMode(boolean optimizationMode) {
585 this.optimizationMode = optimizationMode;
586 this.optimisationModeCB.setSelected(optimizationMode);
587 }
588
589 public void launchSolverWithConfigs() {
590 if (this.startConfig.equals(StartSolverEnum.SOLVER_LIST_PARAM_DEFAULT)) {
591 this.selectedSolver = (String) this.listeSolvers.getSelectedItem();
592 String[] partsSelectedSolver = this.selectedSolver.split("\\.");
593
594 assert partsSelectedSolver.length == 2;
595 assert partsSelectedSolver[0].equals(MINISAT_PREFIX)
596 || partsSelectedSolver[0].equals(PB_PREFIX);
597
598 ASolverFactory factory;
599
600 if (partsSelectedSolver[0].equals(MINISAT_PREFIX)) {
601 factory = org.sat4j.minisat.SolverFactory.instance();
602 } else {
603 factory = org.sat4j.pb.SolverFactory.instance();
604 }
605 this.solver = (ICDCL) factory
606 .createSolverByName(partsSelectedSolver[1]);
607
608 this.telecomStrategy.setSolver(this.solver);
609 this.telecomStrategy.setRestartStrategy(this.solver
610 .getRestartStrategy());
611 this.solver.setRestartStrategy(this.telecomStrategy);
612
613 this.restartPanel.setCurrentRestart(this.telecomStrategy
614 .getRestartStrategy().getClass().getSimpleName());
615
616 IOrder order = this.solver.getOrder();
617
618 double proba = 0;
619
620 if (this.optimizationMode) {
621 if (order instanceof RandomWalkDecoratorObjective) {
622 this.randomWalk = (RandomWalkDecorator) order;
623 proba = this.randomWalk.getProbability();
624 } else if (order instanceof VarOrderHeapObjective) {
625 this.randomWalk = new RandomWalkDecoratorObjective(
626 (VarOrderHeapObjective) order, 0);
627 }
628 } else if (this.solver.getOrder() instanceof RandomWalkDecorator) {
629 this.randomWalk = (RandomWalkDecorator) order;
630 proba = this.randomWalk.getProbability();
631 } else {
632 this.randomWalk = new RandomWalkDecorator((VarOrderHeap) order,
633 0);
634 }
635
636 this.randomWalk.setProbability(proba);
637 this.rwPanel.setProba(proba);
638
639 this.solver.setOrder(this.randomWalk);
640
641 this.telecomStrategy.setPhaseSelectionStrategy(this.solver
642 .getOrder().getPhaseSelectionStrategy());
643 this.phasePanel.setPhaseListSelectedItem(this.telecomStrategy
644 .getPhaseSelectionStrategy().getClass().getSimpleName());
645 this.solver.getOrder().setPhaseSelectionStrategy(
646 this.telecomStrategy);
647 this.simplifierPanel.setSelectedSimplification(this.solver
648 .getSimplifier().toString());
649 }
650
651 else if (this.startConfig
652 .equals(StartSolverEnum.SOLVER_LIST_PARAM_REMOTE)) {
653 this.selectedSolver = (String) this.listeSolvers.getSelectedItem();
654 String[] partsSelectedSolver = this.selectedSolver.split("\\.");
655
656 assert partsSelectedSolver.length == 2;
657 assert partsSelectedSolver[0].equals(MINISAT_PREFIX)
658 || partsSelectedSolver[0].equals(PB_PREFIX);
659
660 ASolverFactory factory;
661
662 if (partsSelectedSolver[0].equals(MINISAT_PREFIX)) {
663 factory = org.sat4j.minisat.SolverFactory.instance();
664 } else {
665 factory = org.sat4j.pb.SolverFactory.instance();
666 }
667 this.solver = (ICDCL) factory
668 .createSolverByName(partsSelectedSolver[1]);
669
670 this.telecomStrategy.setSolver(this.solver);
671
672 this.solver.setRestartStrategy(this.telecomStrategy);
673 this.solver.setOrder(this.randomWalk);
674 this.solver.getOrder().setPhaseSelectionStrategy(
675 this.telecomStrategy);
676
677 this.restartPanel.hasClickedOnRestart();
678 this.rwPanel.hasClickedOnApplyRW();
679 this.phasePanel.hasClickedOnApplyPhase();
680 this.simplifierPanel.hasClickedOnApplySimplification();
681 }
682
683 else if (this.startConfig
684 .equals(StartSolverEnum.SOLVER_LINE_PARAM_LINE)) {
685
686 this.solver = Solvers.configureSolver(this.commandLines, this);
687
688 this.telecomStrategy.setSolver(this.solver);
689 this.telecomStrategy.setRestartStrategy(this.solver
690 .getRestartStrategy());
691 this.solver.setRestartStrategy(this.telecomStrategy);
692
693 this.restartPanel.setCurrentRestart(this.telecomStrategy
694 .getRestartStrategy().getClass().getSimpleName());
695
696 IOrder order = this.solver.getOrder();
697
698 double proba = 0;
699
700 if (this.optimizationMode) {
701 if (order instanceof RandomWalkDecoratorObjective) {
702 this.randomWalk = (RandomWalkDecorator) order;
703 proba = this.randomWalk.getProbability();
704 } else if (order instanceof VarOrderHeapObjective) {
705 this.randomWalk = new RandomWalkDecoratorObjective(
706 (VarOrderHeapObjective) order, 0);
707 }
708 } else if (this.solver.getOrder() instanceof RandomWalkDecorator) {
709 this.randomWalk = (RandomWalkDecorator) order;
710 proba = this.randomWalk.getProbability();
711 } else {
712 this.randomWalk = new RandomWalkDecorator((VarOrderHeap) order,
713 0);
714 }
715
716 this.randomWalk.setProbability(proba);
717 this.rwPanel.setProba(proba);
718 this.solver.setOrder(this.randomWalk);
719 this.telecomStrategy.setPhaseSelectionStrategy(this.solver
720 .getOrder().getPhaseSelectionStrategy());
721 this.solver.getOrder().setPhaseSelectionStrategy(
722 this.telecomStrategy);
723 this.phasePanel.setPhaseListSelectedItem(this.telecomStrategy
724 .getPhaseSelectionStrategy().getClass().getSimpleName());
725 this.simplifierPanel.setSelectedSimplification(this.solver
726 .getSimplifier().toString());
727
728 this.phasePanel.repaint();
729 }
730
731 else if (this.startConfig
732 .equals(StartSolverEnum.SOLVER_LINE_PARAM_REMOTE)) {
733
734 this.solver = Solvers.configureSolver(this.commandLines, this);
735
736 this.solver.setRestartStrategy(this.telecomStrategy);
737 this.solver.setOrder(this.randomWalk);
738 this.solver.getOrder().setPhaseSelectionStrategy(
739 this.telecomStrategy);
740
741 this.restartPanel.hasClickedOnRestart();
742 this.rwPanel.hasClickedOnApplyRW();
743 this.phasePanel.hasClickedOnApplyPhase();
744 this.simplifierPanel.hasClickedOnApplySimplification();
745 }
746
747 this.whereToWriteFiles = this.instancePath;
748
749 if (this.ramdisk.length() > 0) {
750 String[] instancePathSplit = this.instancePath.split("/");
751 this.whereToWriteFiles = this.ramdisk + "/"
752 + instancePathSplit[instancePathSplit.length - 1];
753 }
754
755 this.solver.setVerbose(true);
756 initSearchListeners();
757 this.solver.setLogger(this);
758 this.reader = createReader(this.solver, this.instancePath);
759
760 try {
761 this.problem = this.reader.parseInstance(this.instancePath);
762 } catch (FileNotFoundException e) {
763 e.printStackTrace();
764 } catch (ParseFormatException e) {
765 e.printStackTrace();
766 } catch (IOException e) {
767 e.printStackTrace();
768 } catch (ContradictionException e) {
769 log("Unsatisfiable (trivial)!");
770 }
771
772 boolean optimisation = false;
773 if (this.reader instanceof PBInstanceReader) {
774 optimisation = ((PBInstanceReader) this.reader)
775 .hasObjectiveFunction();
776 if (optimisation) {
777 this.problem = new OptToPBSATAdapter(new PseudoOptDecorator(
778 (IPBCDCLSolver) this.solver));
779 }
780 }
781
782 log("# Started solver " + this.solver.getClass().getSimpleName());
783 log("# on instance " + this.instancePath);
784 log("# Optimisation = " + optimisation);
785 log("# Restart strategy = "
786 + this.telecomStrategy.getRestartStrategy().getClass()
787 .getSimpleName());
788 log("# Random walk probability = " + this.randomWalk.getProbability());
789
790
791 this.solveurThread = new Thread() {
792 @Override
793 public void run() {
794
795
796
797
798
799 try {
800 DetailedCommandPanel.this.stringWriter = new StringWriter();
801 if (DetailedCommandPanel.this.problem.isSatisfiable()) {
802 log("Satisfiable !");
803 if (DetailedCommandPanel.this.problem instanceof OptToPBSATAdapter) {
804 log(((OptToPBSATAdapter) DetailedCommandPanel.this.problem)
805 .getCurrentObjectiveValue() + "");
806 DetailedCommandPanel.this.reader
807 .decode(((OptToPBSATAdapter) DetailedCommandPanel.this.problem)
808 .model(new PrintWriter(
809 DetailedCommandPanel.this.stringWriter)),
810 new PrintWriter(
811 DetailedCommandPanel.this.stringWriter));
812 } else {
813 DetailedCommandPanel.this.reader
814 .decode(DetailedCommandPanel.this.problem
815 .model(),
816 new PrintWriter(
817 DetailedCommandPanel.this.stringWriter));
818 }
819 log(DetailedCommandPanel.this.stringWriter.toString());
820 } else {
821 log("Unsatisfiable !");
822 }
823 } catch (TimeoutException e) {
824 log("Timeout, sorry!");
825 }
826
827
828 }
829 };
830 this.solveurThread.start();
831
832 if (this.isPlotActivated) {
833 this.solverVisu.setnVar(this.solver.nVars());
834 startVisu();
835 }
836 }
837
838 public void initSearchListeners() {
839 List<SearchListener> listeners = new ArrayList<SearchListener>();
840
841 if (this.isPlotActivated) {
842 if (this.gnuplotBased) {
843 this.solverVisu = new GnuplotBasedSolverVisualisation(
844 this.visuPreferences, this.solver.nVars(),
845 this.instancePath, this);
846 if (this.visuPreferences.isDisplayClausesEvaluation()) {
847 listeners.add(new LearnedTracing(
848 new FileBasedVisualizationTool(
849 this.whereToWriteFiles + "-learned")));
850 }
851 if (this.visuPreferences.isDisplayClausesSize()) {
852 listeners.add(new LearnedClausesSizeTracing(
853 new FileBasedVisualizationTool(
854 this.whereToWriteFiles
855 + "-learned-clauses-size"),
856 new FileBasedVisualizationTool(
857 this.whereToWriteFiles
858 + "-learned-clauses-size-restart"),
859 new FileBasedVisualizationTool(
860 this.whereToWriteFiles
861 + "-learned-clauses-size-clean")));
862 }
863 if (this.visuPreferences.isDisplayConflictsDecision()) {
864 listeners
865 .add(new ConflictLevelTracing(
866 new FileBasedVisualizationTool(
867 this.whereToWriteFiles
868 + "-conflict-level"),
869 new FileBasedVisualizationTool(
870 this.whereToWriteFiles
871 + "-conflict-level-restart"),
872 new FileBasedVisualizationTool(
873 this.whereToWriteFiles
874 + "-conflict-level-clean")));
875 }
876 if (this.visuPreferences.isDisplayConflictsTrail()) {
877 listeners
878 .add(new ConflictDepthTracing(
879 new FileBasedVisualizationTool(
880 this.whereToWriteFiles
881 + "-conflict-depth"),
882 new FileBasedVisualizationTool(
883 this.whereToWriteFiles
884 + "-conflict-depth-restart"),
885 new FileBasedVisualizationTool(
886 this.whereToWriteFiles
887 + "-conflict-depth-clean")));
888 }
889
890 if (this.visuPreferences.isDisplayDecisionIndexes()) {
891 listeners.add(new DecisionTracing(
892 new FileBasedVisualizationTool(
893 this.whereToWriteFiles
894 + "-decision-indexes-pos"),
895 new FileBasedVisualizationTool(
896 this.whereToWriteFiles
897 + "-decision-indexes-neg"),
898 new FileBasedVisualizationTool(
899 this.whereToWriteFiles
900 + "-decision-indexes-restart"),
901 new FileBasedVisualizationTool(
902 this.whereToWriteFiles
903 + "-decision-indexes-clean")));
904 }
905
906 if (this.visuPreferences.isDisplaySpeed()) {
907 listeners
908 .add(new SpeedTracing(
909 new FileBasedVisualizationTool(
910 this.whereToWriteFiles + "-speed"),
911 new FileBasedVisualizationTool(
912 this.whereToWriteFiles
913 + "-speed-clean"),
914 new FileBasedVisualizationTool(
915 this.whereToWriteFiles
916 + "-speed-restart")));
917 }
918 if (this.visuPreferences.isDisplayVariablesEvaluation()) {
919 listeners.add(new HeuristicsTracing(
920 new FileBasedVisualizationTool(
921 this.whereToWriteFiles + "-heuristics")));
922 }
923 }
924
925 else if (this.chartBased) {
926
927 if (this.solverVisu != null) {
928 this.solverVisu.end();
929 }
930
931 this.solverVisu = new JChartBasedSolverVisualisation(
932 this.visuPreferences);
933
934 ((JChartBasedSolverVisualisation) this.solverVisu)
935 .setnVar(this.solver.nVars());
936 if (this.visuPreferences.isDisplayClausesEvaluation()) {
937 listeners
938 .add(new LearnedTracing(
939 new ChartBasedVisualizationTool(
940 ((JChartBasedSolverVisualisation) this.solverVisu)
941 .getClausesEvaluationTrace())));
942 }
943 if (this.visuPreferences.isDisplayClausesSize()) {
944 listeners
945 .add(new LearnedClausesSizeTracing(
946 new ChartBasedVisualizationTool(
947 ((JChartBasedSolverVisualisation) this.solverVisu)
948 .getLearnedClausesSizeTrace()),
949 new ChartBasedVisualizationTool(
950 ((JChartBasedSolverVisualisation) this.solverVisu)
951 .getLearnedClausesSizeRestartTrace()),
952 new ChartBasedVisualizationTool(
953 ((JChartBasedSolverVisualisation) this.solverVisu)
954 .getLearnedClausesSizeCleanTrace())));
955 }
956 if (this.visuPreferences.isDisplayConflictsDecision()) {
957 listeners
958 .add(new ConflictLevelTracing(
959 new ChartBasedVisualizationTool(
960 ((JChartBasedSolverVisualisation) this.solverVisu)
961 .getConflictLevelTrace()),
962 new ChartBasedVisualizationTool(
963 ((JChartBasedSolverVisualisation) this.solverVisu)
964 .getConflictLevelRestartTrace()),
965 new ChartBasedVisualizationTool(
966 ((JChartBasedSolverVisualisation) this.solverVisu)
967 .getConflictLevelCleanTrace())));
968 }
969 if (this.visuPreferences.isDisplayConflictsTrail()) {
970 listeners
971 .add(new ConflictDepthTracing(
972 new ChartBasedVisualizationTool(
973 ((JChartBasedSolverVisualisation) this.solverVisu)
974 .getConflictDepthTrace()),
975 new ChartBasedVisualizationTool(
976 ((JChartBasedSolverVisualisation) this.solverVisu)
977 .getConflictDepthRestartTrace()),
978 new ChartBasedVisualizationTool(
979 ((JChartBasedSolverVisualisation) this.solverVisu)
980 .getConflictDepthCleanTrace())));
981 }
982 if (this.visuPreferences.isDisplayDecisionIndexes()) {
983 listeners
984 .add(new DecisionTracing(
985 new ChartBasedVisualizationTool(
986 ((JChartBasedSolverVisualisation) this.solverVisu)
987 .getPositiveDecisionTrace()),
988 new ChartBasedVisualizationTool(
989 ((JChartBasedSolverVisualisation) this.solverVisu)
990 .getNegativeDecisionTrace()),
991 new ChartBasedVisualizationTool(
992 new TraceComposite(
993 ((JChartBasedSolverVisualisation) this.solverVisu)
994 .getRestartPosDecisionTrace(),
995 ((JChartBasedSolverVisualisation) this.solverVisu)
996 .getRestartNegDecisionTrace())),
997 new ChartBasedVisualizationTool(
998 new TraceComposite(
999 ((JChartBasedSolverVisualisation) this.solverVisu)
1000 .getCleanPosDecisionTrace(),
1001 ((JChartBasedSolverVisualisation) this.solverVisu)
1002 .getCleanNegDecisionTrace()))));
1003 }
1004 if (this.visuPreferences.isDisplaySpeed()) {
1005 listeners
1006 .add(new SpeedTracing(
1007 new ChartBasedVisualizationTool(
1008 ((JChartBasedSolverVisualisation) this.solverVisu)
1009 .getSpeedTrace()),
1010 new ChartBasedVisualizationTool(
1011 ((JChartBasedSolverVisualisation) this.solverVisu)
1012 .getSpeedCleanTrace()),
1013 new ChartBasedVisualizationTool(
1014 ((JChartBasedSolverVisualisation) this.solverVisu)
1015 .getSpeedRestartTrace())));
1016 }
1017 if (this.visuPreferences.isDisplayVariablesEvaluation()) {
1018 listeners
1019 .add(new HeuristicsTracing(
1020 new ChartBasedVisualizationTool(
1021 ((JChartBasedSolverVisualisation) this.solverVisu)
1022 .getHeuristicsTrace())));
1023 }
1024 }
1025
1026 }
1027 listeners.add(this);
1028
1029 this.solver.setSearchListener(new MultiTracing(listeners));
1030
1031 }
1032
1033 public int getNVar() {
1034 if (this.solver != null) {
1035 return this.solver.nVars();
1036 }
1037 return 0;
1038 }
1039
1040 public void setPhaseSelectionStrategy(IPhaseSelectionStrategy phase) {
1041 this.telecomStrategy.setPhaseSelectionStrategy(phase);
1042 log("Told the solver to apply a new phase strategy :"
1043 + phase.getClass().getSimpleName());
1044 }
1045
1046 public void shouldRestartNow() {
1047 this.telecomStrategy.setHasClickedOnRestart(true);
1048 }
1049
1050 public void setRestartStrategy(RestartStrategy strategy) {
1051 this.telecomStrategy.setRestartStrategy(strategy);
1052 log("Set Restart to " + strategy);
1053 }
1054
1055 public RestartStrategy getRestartStrategy() {
1056 return this.telecomStrategy.getRestartStrategy();
1057 }
1058
1059 public SearchParams getSearchParams() {
1060 return this.telecomStrategy.getSearchParams();
1061 }
1062
1063 public void init(SearchParams params) {
1064 this.telecomStrategy.init(params);
1065 log("Init restart with params");
1066 }
1067
1068 public void setNbClausesAtWhichWeShouldClean(int nbConflicts) {
1069 this.telecomStrategy.setNbClausesAtWhichWeShouldClean(nbConflicts);
1070 log("Changed number of conflicts before cleaning to " + nbConflicts);
1071 }
1072
1073 public void setUseTelecomStrategyAsLearnedConstraintsDeletionStrategy() {
1074 this.telecomStrategy
1075 .setUseTelecomStrategyAsLearnedConstraintsDeletionStrategy(true);
1076 log("Solver now cleans clauses every "
1077 + this.cleanPanel.getCleanSliderValue()
1078 + " conflicts and bases evaluation of clauses on activity");
1079 }
1080
1081 public void setLearnedDeletionStrategyTypeToSolver(
1082 LearnedConstraintsEvaluationType type) {
1083 this.solver.setLearnedConstraintsDeletionStrategy(this.telecomStrategy,
1084 type);
1085 log("Changed clauses evaluation type to " + type);
1086 }
1087
1088 public LearnedConstraintsEvaluationType getLearnedConstraintsEvaluationType() {
1089
1090 return LearnedConstraintsEvaluationType.ACTIVITY;
1091 }
1092
1093 public void shouldCleanNow() {
1094 log("Told the solver to clean");
1095 this.telecomStrategy.setHasClickedOnClean(true);
1096 }
1097
1098 public void setKeepSolverHot(boolean keepHot) {
1099 this.solver.setKeepSolverHot(keepHot);
1100 if (keepHot) {
1101 log("Keep hot solver is now activated");
1102 } else {
1103 log("Keep hot solver is now desactivated");
1104 }
1105 }
1106
1107 public boolean isGnuplotBased() {
1108 return this.gnuplotBased;
1109 }
1110
1111 public void setGnuplotBased(boolean gnuplotBased) {
1112 this.gnuplotBased = gnuplotBased;
1113 }
1114
1115 public boolean isChartBased() {
1116 return this.chartBased;
1117 }
1118
1119 public void setChartBased(boolean chartBased) {
1120 this.chartBased = chartBased;
1121 }
1122
1123 public boolean isPlotActivated() {
1124 return this.isPlotActivated;
1125 }
1126
1127 public void setPlotActivated(boolean isPlotActivated) {
1128 this.isPlotActivated = isPlotActivated;
1129 }
1130
1131 public void setRandomWalkProba(double proba) {
1132 this.randomWalk.setProbability(proba);
1133 log("Set probability to " + proba);
1134 }
1135
1136 public void setSimplifier(SimplificationType type) {
1137 this.solver.setSimplifier(type);
1138 log("Told the solver to use " + type);
1139 }
1140
1141 public List<String> getListOfSolvers() {
1142 ASolverFactory factory;
1143
1144 List<String> result = new ArrayList<String>();
1145
1146 factory = org.sat4j.minisat.SolverFactory.instance();
1147 for (String s : factory.solverNames()) {
1148 result.add(MINISAT_PREFIX + "." + s);
1149 }
1150
1151 factory = org.sat4j.pb.SolverFactory.instance();
1152 for (String s : factory.solverNames()) {
1153 result.add(PB_PREFIX + "." + s);
1154 }
1155
1156 Collections.sort(result);
1157
1158 return result;
1159 }
1160
1161 public List<String> getListOfPBSolvers() {
1162 ASolverFactory factory;
1163
1164 List<String> result = new ArrayList<String>();
1165
1166 factory = org.sat4j.pb.SolverFactory.instance();
1167 for (String s : factory.solverNames()) {
1168 result.add(PB_PREFIX + "." + s);
1169 }
1170 Collections.sort(result);
1171
1172 return result;
1173 }
1174
1175 public void log(String message) {
1176 logsameline(message + "\n");
1177 }
1178
1179 public void logsameline(String message) {
1180 if (this.console != null) {
1181 this.console.append(message);
1182 this.console.setCaretPosition(this.console.getDocument()
1183 .getLength());
1184 this.console.repaint();
1185 }
1186 this.repaint();
1187 }
1188
1189 public void openFileChooser() {
1190 JFileChooser fc = new JFileChooser();
1191 int returnVal = fc.showDialog(this, "Choose instance");
1192 if (returnVal == JFileChooser.APPROVE_OPTION) {
1193 File file = fc.getSelectedFile();
1194 this.instancePath = file.getAbsolutePath();
1195 this.instancePathField.setText(this.instancePath);
1196 updateListOfSolvers();
1197 }
1198 }
1199
1200 protected Reader createReader(ICDCL theSolver, String problemname) {
1201 if (theSolver instanceof IPBSolver) {
1202 return new PBInstanceReader((IPBSolver) theSolver);
1203 }
1204 return new InstanceReader(theSolver);
1205 }
1206
1207 public void updateListOfSolvers() {
1208 if (this.instancePath.endsWith(".opb")) {
1209 this.listeSolvers = new JComboBox(getListOfPBSolvers().toArray());
1210 this.listeSolvers.setSelectedItem("pb.Default");
1211 this.selectedSolver = "pb.Default";
1212 } else {
1213 this.listeSolvers = new JComboBox(getListOfSolvers().toArray());
1214 this.listeSolvers.setSelectedItem("minisat.Default");
1215 this.selectedSolver = "minisat.Default";
1216 }
1217 }
1218
1219 public void setInstancePanelEnabled(boolean enabled) {
1220 this.instanceLabel.setEnabled(enabled);
1221 this.instancePathField.setEnabled(enabled);
1222 this.browseButton.setEnabled(enabled);
1223 this.instancePanel.repaint();
1224 }
1225
1226 public void setChoixSolverPanelEnabled(boolean enabled) {
1227 this.listeSolvers.setEnabled(enabled);
1228 this.choixSolver.setEnabled(enabled);
1229 this.solverLineParamLineRadio.setEnabled(enabled);
1230 this.solverLineParamRemoteRadio.setEnabled(enabled);
1231 this.solverListParamListRadio.setEnabled(enabled);
1232 this.solverListParamRemoteRadio.setEnabled(enabled);
1233 this.optimisationModeCB.setEnabled(enabled);
1234
1235
1236 this.choixSolverPanel.repaint();
1237 }
1238
1239 public void setSolverVisualisation(SolverVisualisation visu) {
1240 this.solverVisu = visu;
1241 }
1242
1243 public void activateGnuplotTracing(boolean b) {
1244 this.isPlotActivated = b;
1245 if (this.solver != null) {
1246 initSearchListeners();
1247 }
1248 }
1249
1250 public void startVisu() {
1251 this.solverVisu.start();
1252 }
1253
1254 public void stopVisu() {
1255 this.solverVisu.end();
1256 }
1257
1258 public VisuPreferences getGnuplotPreferences() {
1259 return this.visuPreferences;
1260 }
1261
1262 public void setGnuplotPreferences(VisuPreferences gnuplotPreferences) {
1263 this.visuPreferences = gnuplotPreferences;
1264 }
1265
1266 public DetailedCommandPanel getThis() {
1267 return this;
1268 }
1269
1270 public ISolver getSolver() {
1271 return (ISolver) this.problem;
1272 }
1273
1274 private long begin, end;
1275 private int propagationsCounter;
1276
1277 private int conflictCounter;
1278
1279 private PrintStream outSolutionFound;
1280
1281 private void updateWriter() {
1282 try {
1283 this.outSolutionFound = new PrintStream(new FileOutputStream(
1284 this.whereToWriteFiles + "_solutions.dat"));
1285 } catch (FileNotFoundException e) {
1286 this.outSolutionFound = System.out;
1287 }
1288
1289 }
1290
1291 public void init(ISolverService solverService) {
1292
1293 this.conflictCounter = 0;
1294 }
1295
1296 public void assuming(int p) {
1297 }
1298
1299 public void propagating(int p, IConstr reason) {
1300 this.end = System.currentTimeMillis();
1301 if (this.end - this.begin >= 2000) {
1302 long tmp = this.end - this.begin;
1303
1304
1305 this.cleanPanel.setSpeedLabeltext(this.propagationsCounter / tmp
1306 * 1000 + "");
1307
1308 this.begin = System.currentTimeMillis();
1309 this.propagationsCounter = 0;
1310 }
1311 this.propagationsCounter++;
1312 }
1313
1314 public void backtracking(int p) {
1315 }
1316
1317 public void adding(int p) {
1318 }
1319
1320 public void learn(IConstr c) {
1321 }
1322
1323 public void delete(int[] clause) {
1324 }
1325
1326 public void conflictFound(IConstr confl, int dlevel, int trailLevel) {
1327 this.conflictCounter++;
1328 }
1329
1330 public void conflictFound(int p) {
1331 }
1332
1333 public void solutionFound(int[] model) {
1334
1335 log("Found a solution !! ");
1336 logsameline(this.stringWriter.toString());
1337 this.stringWriter.getBuffer().delete(0,
1338 this.stringWriter.getBuffer().length());
1339 this.outSolutionFound.println(this.conflictCounter + "\t");
1340 }
1341
1342 public void beginLoop() {
1343 }
1344
1345 public void start() {
1346 }
1347
1348 public void end(Lbool result) {
1349 }
1350
1351 public void restarting() {
1352 this.end = System.currentTimeMillis();
1353 this.cleanPanel.setSpeedLabeltext(this.propagationsCounter
1354 / (this.end - this.begin) * 1000 + "");
1355 }
1356
1357 public void backjump(int backjumpLevel) {
1358 }
1359
1360 public void cleaning() {
1361 this.end = System.currentTimeMillis();
1362 this.cleanPanel.setSpeedLabeltext(this.propagationsCounter
1363 / (this.end - this.begin) * 1000 + "");
1364 }
1365
1366 public class MyTabbedPane extends JTabbedPane {
1367 private static final long serialVersionUID = 1L;
1368
1369 @Override
1370 public void setSelectedIndex(int index) {
1371 if (this.getTabCount() == 5) {
1372 if (index == this.getTabCount() - 1) {
1373
1374 if (DetailedCommandPanel.this.solver != null
1375 && DetailedCommandPanel.this.startStopButton
1376 .getText().equals(STOP)) {
1377 String s = DetailedCommandPanel.this.solver.toString();
1378 String res = DetailedCommandPanel.this.solver
1379 .toString();
1380 int j = 0;
1381 for (int i = 0; i < s.length(); i++) {
1382 if (s.charAt(i) != '\n') {
1383 j++;
1384 } else {
1385 j = 0;
1386 }
1387 if (j > 80) {
1388 res = new StringBuffer(res).insert(i, '\n')
1389 .toString();
1390 j = 0;
1391 }
1392 }
1393 DetailedCommandPanel.this.textArea.setText(res);
1394 DetailedCommandPanel.this.textArea.setEditable(false);
1395 DetailedCommandPanel.this.textArea.repaint();
1396 DetailedCommandPanel.this.aboutSolverPanel
1397 .paint(DetailedCommandPanel.this.aboutSolverPanel
1398 .getGraphics());
1399 DetailedCommandPanel.this.aboutSolverPanel.repaint();
1400 } else {
1401 DetailedCommandPanel.this.textArea
1402 .setText("No solver is running at the moment");
1403 DetailedCommandPanel.this.textArea.repaint();
1404 DetailedCommandPanel.this.textArea.setEditable(false);
1405 DetailedCommandPanel.this.aboutSolverPanel
1406 .paint(DetailedCommandPanel.this.aboutSolverPanel
1407 .getGraphics());
1408 DetailedCommandPanel.this.aboutSolverPanel.repaint();
1409 }
1410
1411
1412 }
1413 }
1414
1415 super.setSelectedIndex(index);
1416 };
1417 }
1418
1419 }