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