Clover Coverage Report
Coverage timestamp: mer. juin 27 2007 07:27:16 CEST
Overview   Package   File
    FRAMES   NO FRAMES     
45   225   12   2,65
26   110   0,62   17
17     1,65  
1    
 
  VarOrderHeap       Line # 43 45 12 71,6% 0.71590906
 
  (162)
 
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.orders;
27   
28    import java.io.PrintWriter;
29    import java.io.Serializable;
30   
31    import org.sat4j.minisat.core.Heap;
32    import org.sat4j.minisat.core.ILits;
33    import org.sat4j.minisat.core.IOrder;
34   
35    /*
36    * Created on 16 oct. 2003
37    */
38   
39    /**
40    * @author leberre Heuristique du prouveur. Changement par rapport au MiniSAT
41    * original : la gestion activity est faite ici et non plus dans Solver.
42    */
 
43    public class VarOrderHeap<L extends ILits> implements IOrder<L>, Serializable {
44   
45    private static final long serialVersionUID = 1L;
46   
47    private static final double VAR_RESCALE_FACTOR = 1e-100;
48   
49    private static final double VAR_RESCALE_BOUND = 1 / VAR_RESCALE_FACTOR;
50   
51    /**
52    * mesure heuristique de l'activite d'une variable.
53    */
54    protected double[] activity = new double[1];
55   
56    private double varDecay = 1.0;
57   
58    /**
59    * increment pour l'activite des variables.
60    */
61    private double varInc = 1.0;
62   
63    protected L lits;
64   
65    private long nullchoice = 0;
66   
67    protected Heap heap;
68   
69    protected int[] phase;
70   
 
71  1292 toggle public void setLits(L lits) {
72  1292 this.lits = lits;
73    }
74   
75    /**
76    * Appelee quand une nouvelle variable est creee.
77    */
 
78  734940 toggle public void newVar() {
79  734940 newVar(1);
80    }
81   
82    /**
83    * Appelee lorsque plusieurs variables sont creees
84    *
85    * @param howmany
86    * le nombre de variables creees
87    */
 
88  735592 toggle public void newVar(int howmany) {
89    }
90   
91    /**
92    * Selectionne une nouvelle variable, non affectee, ayant l'activite
93    * la plus elevee.
94    *
95    * @return Lit.UNDEFINED si aucune variable n'est trouvee
96    */
 
97  91476196 toggle public int select() {
98  164960057 while (!heap.empty()) {
99  164960057 int var = heap.getmin();
100  164960057 int next = phase[var];
101  164960057 if (lits.isUnassigned(next)) {
102  91476196 if (activity[var] < 0.0001) {
103  346359 nullchoice++;
104    }
105  91476196 return next;
106    }
107    }
108  0 return ILits.UNDEFINED;
109    }
110   
111    /**
112    * Change la valeur de varDecay.
113    *
114    * @param d
115    * la nouvelle valeur de varDecay
116    */
 
117  26550 toggle public void setVarDecay(double d) {
118  26550 varDecay = d;
119    }
120   
121    /**
122    * Methode appelee quand la variable x est desaffectee.
123    *
124    * @param x
125    */
 
126  1425374365 toggle public void undo(int x) {
127  1425374365 if (!heap.inHeap(x))
128  164956337 heap.insert(x);
129    }
130   
131    /**
132    * Appelee lorsque l'activite de la variable x a change.
133    *
134    * @param p
135    * a literal
136    */
 
137  414087579 toggle public void updateVar(int p) {
138  414087579 int var = p >> 1;
139  414087579 updateActivity(var);
140  414087579 phase[var] = p;
141  414087579 if (heap.inHeap(var))
142  1063104175 heap.increase(var);
143    }
144   
 
145  1698938576 toggle protected void updateActivity(final int var) {
146  1698938576 if ((activity[var] += varInc) > VAR_RESCALE_BOUND) {
147  13888 varRescaleActivity();
148    }
149    }
150   
151    /**
152    *
153    */
 
154  62691748 toggle public void varDecayActivity() {
155  62691748 varInc *= varDecay;
156    }
157   
158    /**
159    *
160    */
 
161  13888 toggle private void varRescaleActivity() {
162  2972572 for (int i = 1; i < activity.length; i++) {
163  2958684 activity[i] *= VAR_RESCALE_FACTOR;
164    }
165  13888 varInc *= VAR_RESCALE_FACTOR;
166    }
167   
 
168  0 toggle public double varActivity(int p) {
169  0 return activity[p >> 1];
170    }
171   
172    /**
173    *
174    */
 
175  0 toggle public int numberOfInterestingVariables() {
176  0 int cpt = 0;
177  0 for (int i = 1; i < activity.length; i++) {
178  0 if (activity[i] > 1.0) {
179  0 cpt++;
180    }
181    }
182  0 return cpt;
183    }
184   
185    /**
186    * that method has the responsability to initialize all arrays in the
187    * heuristics. PLEASE CALL super.init() IF YOU OVERRIDE THAT METHOD.
188    */
 
189  1280 toggle public void init() {
190  1280 int nlength = lits.nVars() + 1;
191  1280 activity = new double[nlength];
192  1280 phase = new int[nlength];
193  1280 activity[0] = -1;
194  1280 heap = new Heap(activity);
195  1280 heap.setBounds(nlength);
196  891410 for (int i = 1; i < nlength; i++) {
197  890130 assert i > 0;
198  890130 assert i <= lits.nVars() : "" + lits.nVars() + "/" + i; //$NON-NLS-1$ //$NON-NLS-2$
199  890130 activity[i] = 0.0;
200  890130 if (lits.belongsToPool(i)) {
201  890130 heap.insert(i);
202  890130 phase[i] = (i << 1) ^ 1;
203    } else {
204  0 phase[i] = ILits.UNDEFINED;
205    }
206    }
207    }
208   
 
209  0 toggle @Override
210    public String toString() {
211  0 return "VSIDS like heuristics from MiniSAT using a heap"; //$NON-NLS-1$
212    }
213   
 
214  0 toggle public ILits getVocabulary() {
215  0 return lits;
216    }
217   
 
218  0 toggle public void printStat(PrintWriter out, String prefix) {
219  0 out.println(prefix + "non guided choices\t" + nullchoice); //$NON-NLS-1$
220    }
221   
 
222  880106749 toggle public void assignLiteral(int p) {
223    // do nothing
224    }
225    }
 
CloverReport generated by Clover Code Coverage v2.0a5
mer. juin 27 2007 07:27:33 CEST.		   Beta Testers License registered to clover-support@cenqua.com. This license of Clover2 is provided for beta testing only. You have 5 day(s) before your Beta Tester License expires.