View Javadoc

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         // Create the label table
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 }