Clover Coverage Report
Coverage timestamp: mer. juin 27 2007 07:27:16 CEST
20   110   2   1,82
2   60   0,6   11
11     1,09  
1    
 
  LimitedLearning       Line # 40 20 2 81,8% 0.8181818
 
  (123)
 
1    /*
2    * SAT4J: a SATisfiability library for Java Copyright (C) 2004-2006 Daniel Le Berre
3    *
4    * Based on the original minisat specification from:
5    *
6    * An extensible SAT solver. Niklas E?n and Niklas S?rensson. Proceedings of the
7    * Sixth International Conference on Theory and Applications of Satisfiability
8    * Testing, LNCS 2919, pp 502-518, 2003.
9    *
10    * This library is free software; you can redistribute it and/or modify it under
11    * the terms of the GNU Lesser General Public License as published by the Free
12    * Software Foundation; either version 2.1 of the License, or (at your option)
13    * any later version.
14    *
15    * This library is distributed in the hope that it will be useful, but WITHOUT
16    * ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS
17    * FOR A PARTICULAR PURPOSE. See the GNU Lesser General Public License for more
18    * details.
19    *
20    * You should have received a copy of the GNU Lesser General Public License
21    * along with this library; if not, write to the Free Software Foundation, Inc.,
22    * 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA
23    *
24    */
25   
26    package org.sat4j.minisat.learning;
27   
28    import org.sat4j.minisat.core.Constr;
29    import org.sat4j.minisat.core.ILits;
30    import org.sat4j.minisat.core.LearningStrategy;
31    import org.sat4j.minisat.core.Solver;
32    import org.sat4j.minisat.core.VarActivityListener;
33   
34    /**
35    * Learn only clauses which size is smaller than a percentage of the number of
36    * variables.
37    *
38    * @author leberre
39    */
 
40    public class LimitedLearning<L extends ILits> implements LearningStrategy<L> {
41   
42    private static final long serialVersionUID = 1L;
43   
44    private final NoLearningButHeuristics<L> none;
45   
46    private final MiniSATLearning<L> all;
47   
48    private int maxpercent;
49   
50    private L lits;
51   
52    private int bound;
53   
 
54  205 toggle public LimitedLearning() {
55  205 this(10);
56    }
57   
 
58  1128 toggle public LimitedLearning(int percent) {
59  1128 maxpercent = percent;
60  1128 none = new NoLearningButHeuristics<L>();
61  1128 all = new MiniSATLearning<L>();
62    }
63   
 
64  0 toggle public void setLimit(int percent) {
65  0 maxpercent = percent;
66    }
67   
 
68  0 toggle public int getLimit() {
69  0 return maxpercent;
70    }
71   
 
72  1128 toggle public void setSolver(Solver<L> s) {
73  1128 this.lits = s.getVocabulary();
74  1128 setVarActivityListener(s);
75  1128 all.setDataStructureFactory(s.getDSFactory());
76    }
77   
 
78  164465757 toggle public void learns(Constr constr) {
79  164465757 if (learningCondition(constr)) {
80  104703 all.learns(constr);
81    } else {
82  164361054 none.learns(constr);
83    }
84    }
85   
 
86  164379648 toggle protected boolean learningCondition(Constr constr) {
87  164379648 return constr.size() <= bound;
88    }
89   
 
90  972 toggle public void init() {
91  972 setBound(lits.realnVars() * maxpercent / 100);
92  972 all.init();
93  972 none.init();
94    }
95   
 
96  1075 toggle protected void setBound(int newbound) {
97  1075 bound = newbound;
98    }
99   
 
100  0 toggle @Override
101    public String toString() {
102  0 return "Limit learning to clauses of size smaller or equal to " //$NON-NLS-1$
103    + maxpercent + "% of the number of variables"; //$NON-NLS-1$
104    }
105   
 
106  1128 toggle public void setVarActivityListener(VarActivityListener s) {
107  1128 none.setVarActivityListener(s);
108  1128 all.setVarActivityListener(s);
109    }
110    }