1 package org.sat4j.sat;
2
3 import java.awt.BorderLayout;
4 import java.awt.Dimension;
5 import java.awt.event.ActionEvent;
6 import java.awt.event.ActionListener;
7 import java.util.Dictionary;
8 import java.util.Hashtable;
9
10 import javax.swing.ButtonGroup;
11 import javax.swing.JButton;
12 import javax.swing.JCheckBox;
13 import javax.swing.JLabel;
14 import javax.swing.JPanel;
15 import javax.swing.JRadioButton;
16 import javax.swing.JSlider;
17 import javax.swing.SwingConstants;
18 import javax.swing.border.CompoundBorder;
19 import javax.swing.border.TitledBorder;
20
21 import org.sat4j.minisat.core.LearnedConstraintsEvaluationType;
22
23 public class CleanCommandComponent extends CommandComponent {
24
25
26
27
28 private static final long serialVersionUID = 1L;
29
30 private JSlider cleanSlider;
31
32 private static final String EVALUATION_TYPE = "Clauses evaluation type";
33 private static final String ACTIVITY_BASED = "Activity";
34 private static final String LBD_BASED = "LBD";
35 private static final String LBD2_BASED = "LBD 2";
36 private JLabel evaluationLabel;
37 private JRadioButton activityRadio;
38 private JRadioButton lbdRadio;
39 private JRadioButton lbd2Radio;
40
41 private JButton cleanAndEvaluationApplyButton;
42
43 private JButton cleanButton;
44 private static final String CLEAN = "Clean now";
45 private static final String MANUAL_CLEAN = "Manual clean: ";
46 private JLabel manualCleanLabel;
47
48 private JLabel speedLabel;
49 private JLabel speedNameLabel;
50 private static final String SPEED = "Speed :";
51 private JLabel speedUnitLabel;
52 private static final String SPEED_UNIT = " propagations per second";
53
54 private final JLabel deleteClauseLabel = new JLabel(DELETE_CLAUSES);
55 private static final String DELETE_CLAUSES = "Automated clean: ";
56
57 private final JLabel clean5000Label = new JLabel(CLEAN_5000);
58 private final JLabel clean10000Label = new JLabel(CLEAN_10000);
59 private final JLabel clean20000Label = new JLabel(CLEAN_20000);
60 private final JLabel clean50000Label = new JLabel(CLEAN_50000);
61 private final JLabel clean100000Label = new JLabel(CLEAN_100000);
62 private final JLabel clean500000Label = new JLabel(CLEAN_500000);
63 private static final int[] CLEAN_VALUES = { 5000, 10000, 20000, 50000,
64 100000, 500000 };
65 private static final int CLEAN_MIN = 0;
66 private static final int CLEAN_MAX = 5;
67 private static final int CLEAN_INIT = 1;
68 private static final int CLEAN_SPACE = 1;
69
70 private static final String CLEAN_5000 = "5000";
71 private static final String CLEAN_10000 = "10000";
72 private static final String CLEAN_20000 = "20000";
73 private static final String CLEAN_50000 = "50000";
74 private static final String CLEAN_100000 = "100000";
75 private static final String CLEAN_500000 = "500000";
76
77 private SolverController controller;
78
79 private JCheckBox cleanUseOriginalStrategyCB;
80 private static final String USE_ORIGINAL_STRATEGY = "Use solver's original deletion strategy";
81
82 public CleanCommandComponent(String name, SolverController controller) {
83 super();
84 setName(name);
85 this.controller = controller;
86 createPanel();
87 }
88
89 @Override
90 public void createPanel() {
91
92 this.setBorder(new CompoundBorder(new TitledBorder(null,
93 this.getName(), TitledBorder.LEFT, TitledBorder.TOP),
94 DetailedCommandPanel.BORDER5));
95
96 this.setLayout(new BorderLayout());
97
98 this.cleanSlider = new JSlider(SwingConstants.HORIZONTAL, CLEAN_MIN,
99 CLEAN_MAX, CLEAN_INIT);
100
101 this.cleanSlider.setMajorTickSpacing(CLEAN_SPACE);
102 this.cleanSlider.setPaintTicks(true);
103
104
105 Dictionary<Integer, JLabel> cleanValuesTable = new Hashtable<Integer, JLabel>();
106 cleanValuesTable.put(0, this.clean5000Label);
107 cleanValuesTable.put(1, this.clean10000Label);
108 cleanValuesTable.put(2, this.clean20000Label);
109 cleanValuesTable.put(3, this.clean50000Label);
110 cleanValuesTable.put(4, this.clean100000Label);
111 cleanValuesTable.put(5, this.clean500000Label);
112 this.cleanSlider.setLabelTable(cleanValuesTable);
113
114 this.cleanSlider.setPaintLabels(true);
115 this.cleanSlider.setSnapToTicks(true);
116
117 this.cleanSlider.setPreferredSize(new Dimension(400, 50));
118
119 JPanel tmpPanel1 = new JPanel();
120 tmpPanel1.add(this.deleteClauseLabel);
121 tmpPanel1.add(this.cleanSlider);
122
123 JPanel tmpPanel4 = new JPanel();
124
125 this.evaluationLabel = new JLabel(EVALUATION_TYPE);
126 ButtonGroup evaluationGroup = new ButtonGroup();
127 this.activityRadio = new JRadioButton(ACTIVITY_BASED);
128 this.lbdRadio = new JRadioButton(LBD_BASED);
129 this.lbd2Radio = new JRadioButton(LBD2_BASED);
130
131 evaluationGroup.add(this.activityRadio);
132 evaluationGroup.add(this.lbdRadio);
133 evaluationGroup.add(this.lbd2Radio);
134
135 tmpPanel4.add(this.evaluationLabel);
136 tmpPanel4.add(this.activityRadio);
137 tmpPanel4.add(this.lbdRadio);
138 tmpPanel4.add(this.lbd2Radio);
139
140 this.cleanAndEvaluationApplyButton = new JButton("Apply changes");
141 this.cleanAndEvaluationApplyButton
142 .addActionListener(new ActionListener() {
143 public void actionPerformed(ActionEvent e) {
144 hasChangedCleaningValue();
145 }
146 });
147
148 JPanel tmpPanel5 = new JPanel();
149 tmpPanel5.add(this.cleanAndEvaluationApplyButton);
150
151 JPanel tmpPanel = new JPanel();
152 tmpPanel.setBorder(new CompoundBorder(new TitledBorder(null, "",
153 TitledBorder.LEFT, TitledBorder.TOP),
154 DetailedCommandPanel.BORDER5));
155
156 tmpPanel.setLayout(new BorderLayout());
157
158 tmpPanel.add(tmpPanel1, BorderLayout.NORTH);
159 tmpPanel.add(tmpPanel4, BorderLayout.CENTER);
160 tmpPanel.add(tmpPanel5, BorderLayout.SOUTH);
161
162 JPanel tmpPanel2 = new JPanel();
163
164 this.manualCleanLabel = new JLabel(MANUAL_CLEAN);
165
166 this.cleanButton = new JButton(CLEAN);
167
168 this.cleanButton.addActionListener(new ActionListener() {
169 public void actionPerformed(ActionEvent e) {
170 hasClickedOnClean();
171 }
172 });
173
174 tmpPanel2.add(this.manualCleanLabel);
175 tmpPanel2.add(this.cleanButton);
176
177 JPanel tmpPanel3 = new JPanel();
178 this.cleanUseOriginalStrategyCB = new JCheckBox(USE_ORIGINAL_STRATEGY);
179 this.cleanUseOriginalStrategyCB.setSelected(true);
180
181 this.cleanUseOriginalStrategyCB.addActionListener(new ActionListener() {
182 public void actionPerformed(ActionEvent e) {
183 hasClickedOnUseOriginalStrategy();
184 }
185 });
186
187 tmpPanel3.add(this.cleanUseOriginalStrategyCB);
188
189 JPanel tmpPanel6 = new JPanel();
190 this.speedLabel = new JLabel("");
191 this.speedNameLabel = new JLabel(SPEED);
192 this.speedUnitLabel = new JLabel(SPEED_UNIT);
193
194 tmpPanel6.add(this.speedNameLabel);
195 tmpPanel6.add(this.speedLabel);
196 tmpPanel6.add(this.speedUnitLabel);
197
198 JPanel tmpPanel7 = new JPanel();
199 tmpPanel7.setLayout(new BorderLayout());
200
201 tmpPanel7.add(tmpPanel2, BorderLayout.SOUTH);
202 tmpPanel7.add(tmpPanel6, BorderLayout.CENTER);
203
204 this.add(tmpPanel3, BorderLayout.NORTH);
205 this.add(tmpPanel7, BorderLayout.CENTER);
206 this.add(tmpPanel, BorderLayout.SOUTH);
207
208 }
209
210 public void hasChangedCleaningValue() {
211 int nbConflicts = CLEAN_VALUES[this.cleanSlider.getValue()];
212 this.controller.setNbClausesAtWhichWeShouldClean(nbConflicts);
213 if (this.activityRadio.isSelected()) {
214 this.controller
215 .setLearnedDeletionStrategyTypeToSolver(LearnedConstraintsEvaluationType.ACTIVITY);
216 } else if (this.lbdRadio.isSelected()) {
217 this.controller
218 .setLearnedDeletionStrategyTypeToSolver(LearnedConstraintsEvaluationType.LBD);
219 } else if (this.lbd2Radio.isSelected()) {
220 this.controller
221 .setLearnedDeletionStrategyTypeToSolver(LearnedConstraintsEvaluationType.LBD2);
222 }
223 }
224
225 public void hasClickedOnUseOriginalStrategy() {
226 int nbConflicts = CLEAN_VALUES[this.cleanSlider.getValue()];
227 this.controller.setNbClausesAtWhichWeShouldClean(nbConflicts);
228
229 this.controller
230 .setUseTelecomStrategyAsLearnedConstraintsDeletionStrategy();
231
232 this.controller
233 .setLearnedDeletionStrategyTypeToSolver(LearnedConstraintsEvaluationType.ACTIVITY);
234 this.activityRadio.setSelected(true);
235
236 setCleanPanelOriginalStrategyEnabled(false);
237 }
238
239 public int getCleanSliderValue() {
240 return CLEAN_VALUES[this.cleanSlider.getValue()];
241 }
242
243 public void hasClickedOnClean() {
244 this.controller.shouldCleanNow();
245 }
246
247 public void setCleanPanelEnabled(boolean enabled) {
248 this.manualCleanLabel.setEnabled(enabled);
249 this.deleteClauseLabel.setEnabled(enabled);
250 this.cleanSlider.setEnabled(enabled);
251 this.cleanButton.setEnabled(enabled);
252 this.evaluationLabel.setEnabled(enabled);
253 this.activityRadio.setEnabled(enabled);
254 this.lbdRadio.setEnabled(enabled);
255 this.lbd2Radio.setEnabled(enabled);
256 this.cleanAndEvaluationApplyButton.setEnabled(enabled);
257 this.cleanUseOriginalStrategyCB.setEnabled(enabled);
258 this.speedLabel.setEnabled(enabled);
259 this.speedUnitLabel.setEnabled(enabled);
260 this.speedNameLabel.setEnabled(enabled);
261 this.repaint();
262 }
263
264 public void setCleanPanelOriginalStrategyEnabled(boolean enabled) {
265 this.cleanUseOriginalStrategyCB.setEnabled(enabled);
266 this.manualCleanLabel.setEnabled(!enabled);
267 this.deleteClauseLabel.setEnabled(!enabled);
268 this.activityRadio.setEnabled(!enabled);
269 this.evaluationLabel.setEnabled(!enabled);
270 this.lbdRadio.setEnabled(!enabled);
271 this.lbd2Radio.setEnabled(!enabled);
272 this.cleanAndEvaluationApplyButton.setEnabled(!enabled);
273 this.cleanSlider.setEnabled(!enabled);
274 this.cleanButton.setEnabled(!enabled);
275 this.repaint();
276 }
277
278 public void setSpeedLabeltext(String speed) {
279 this.speedLabel.setText(speed);
280 this.speedLabel.invalidate();
281 }
282
283 }