Clover Coverage Report
Coverage timestamp: mer. juin 27 2007 07:27:16 CEST
Overview   Package   File
    FRAMES   NO FRAMES     
56   300   14   3,29
46   133   0,54   17
17     1,76  
1    
 
  VarOrder       Line # 42 56 14 67,2% 0.6722689
 
  (141)
 
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.ILits;
32    import org.sat4j.minisat.core.IOrder;
33   
34    /*
35    * Created on 16 oct. 2003
36    */
37   
38    /**
39    * @author leberre Heuristique du prouveur. Changement par rapport au MiniSAT
40    * original : la gestion activity est faite ici et non plus dans Solver.
41    */
 
42    public class VarOrder<L extends ILits> implements Serializable, IOrder<L> {
43   
44    private static final long serialVersionUID = 1L;
45   
46    /**
47    * Comparateur permettant de trier les variables
48    */
49    private static final double VAR_RESCALE_FACTOR = 1e-100;
50   
51    private static final double VAR_RESCALE_BOUND = 1 / VAR_RESCALE_FACTOR;
52   
53    /**
54    * mesure heuristique de l'activite d'une variable.
55    */
56    protected double[] activity = new double[1];
57   
58    /**
59    * Derniere variable choisie
60    */
61    protected int lastVar = 1;
62   
63    /**
64    * Ordre des variables
65    */
66    protected int[] order = new int[1];
67   
68    private double varDecay = 1.0;
69   
70    /**
71    * increment pour l'activite des variables.
72    */
73    private double varInc = 1.0;
74   
75    /**
76    * position des variables
77    */
78    protected int[] varpos = new int[1];
79   
80    protected L lits;
81   
82    private long nullchoice = 0;
83   
84    // private long randchoice = 0;
85   
86    // private Random rand = new Random(12345);
87   
88    // private final static double RANDOM_WALK = 0.05;
89   
90    /*
91    * (non-Javadoc)
92    *
93    * @see org.sat4j.minisat.core.IOrder#setLits(org.sat4j.minisat.core.ILits)
94    */
 
95  1236 toggle public void setLits(L lits) {
96  1236 this.lits = lits;
97    }
98   
99    /*
100    * (non-Javadoc)
101    *
102    * @see org.sat4j.minisat.core.IOrder#newVar()
103    */
 
104  6774 toggle public void newVar() {
105  6774 newVar(1);
106    }
107   
108    /*
109    * (non-Javadoc)
110    *
111    * @see org.sat4j.minisat.core.IOrder#newVar(int)
112    */
 
113  7808 toggle public void newVar(int howmany) {
114    }
115   
116    /*
117    * (non-Javadoc)
118    *
119    * @see org.sat4j.minisat.core.IOrder#select()
120    */
 
121  175125351 toggle public int select() {
122  175125351 assert lastVar > 0;
123    for (int i = lastVar; i < order.length; i++) {
124    assert i > 0;
125    if (lits.isUnassigned(order[i])) {
126  175125350 lastVar = i;
127  175125350 if (activity[i] < 0.0001) {
128    // if (rand.nextDouble() <= RANDOM_WALK) {
129    // int randomchoice = rand.nextInt(order.length - i) + i;
130    // assert randomchoice >= i;
131    // if ((randomchoice > i)
132    // && lits.isUnassigned(order[randomchoice])) {
133    // randchoice++;
134    // return order[randomchoice];
135    // }
136    // }
137  26413070 nullchoice++;
138    }
139  175125350 return order[i];
140    }
141    }
142  1 return ILits.UNDEFINED;
143    }
144   
145    /**
146    * Change la valeur de varDecay.
147    *
148    * @param d
149    * la nouvelle valeur de varDecay
150    */
 
151  2443 toggle public void setVarDecay(double d) {
152  2443 varDecay = d;
153    }
154   
155    /*
156    * (non-Javadoc)
157    *
158    * @see org.sat4j.minisat.core.IOrder#undo(int)
159    */
 
160    toggle public void undo(int x) {
161    assert x > 0;
162    assert x < order.length;
163    int pos = varpos[x];
164    if (pos < lastVar) {
165  4268758 lastVar = pos;
166    }
167    assert lastVar > 0;
168    }
169   
170    /*
171    * (non-Javadoc)
172    *
173    * @see org.sat4j.minisat.core.IOrder#updateVar(int)
174    */
 
175  485218855 toggle public void updateVar(int p) {
176  485218855 assert p > 1;
177  485218855 final int var = p >> 1;
178   
179  485218855 updateActivity(var);
180  485218855 int i = varpos[var];
181  1799743914 for (; i > 1 // because there is nothing at i=0
182    && (activity[order[i - 1] >> 1] < activity[var]); i--) {
183  1314525059 assert i > 1;
184    // echange p avec son predecesseur
185  1314525059 final int orderpm1 = order[i - 1];
186  1314525059 assert varpos[orderpm1 >> 1] == i - 1;
187  1314525059 varpos[orderpm1 >> 1] = i;
188  1314525059 order[i] = orderpm1;
189    }
190  485218855 assert i >= 1;
191  485218855 varpos[var] = i;
192  485218855 order[i] = p;
193   
194  485218855 if (i < lastVar) {
195  186362035 lastVar = i;
196    }
197    }
198   
 
199  329093883 toggle protected void updateActivity(final int var) {
200  329093883 if ((activity[var] += varInc) > VAR_RESCALE_BOUND) {
201  26465 varRescaleActivity();
202    }
203    }
204   
205    /**
206    *
207    */
 
208  121307602 toggle public void varDecayActivity() {
209  121307602 varInc *= varDecay;
210    }
211   
212    /**
213    *
214    */
 
215  26465 toggle private void varRescaleActivity() {
216  2361621 for (int i = 1; i < activity.length; i++) {
217  2335156 activity[i] *= VAR_RESCALE_FACTOR;
218    }
219  26465 varInc *= VAR_RESCALE_FACTOR;
220    }
221   
 
222  2498007 toggle public double varActivity(int p) {
223  2498007 return activity[p >> 1];
224    }
225   
226    /**
227    *
228    */
 
229  0 toggle public int numberOfInterestingVariables() {
230  0 int cpt = 0;
231  0 for (int i = 1; i < activity.length; i++) {
232  0 if (activity[i] > 1.0) {
233  0 cpt++;
234    }
235    }
236  0 return cpt;
237    }
238   
239    /*
240    * (non-Javadoc)
241    *
242    * @see org.sat4j.minisat.core.IOrder#init()
243    */
 
244  1183 toggle public void init() {
245  1183 int nlength = lits.nVars() + 1;
246  1183 int reallength = lits.realnVars() + 1;
247  1183 int[] nvarpos = new int[nlength];
248  1183 double[] nactivity = new double[nlength];
249  1183 int[] norder = new int[reallength];
250  1183 nvarpos[0] = -1;
251  1183 nactivity[0] = -1;
252  1183 norder[0] = ILits.UNDEFINED;
253  260408 for (int i = 1, j = 1; i < nlength; i++) {
254  259225 assert i > 0;
255  259225 assert i <= lits.nVars() : "" + lits.nVars() + "/" + i; //$NON-NLS-1$ //$NON-NLS-2$
256  259225 if (lits.belongsToPool(i)) {
257  259211 norder[j] = lits.getFromPool(i) ^ 1; // Looks a
258    // promising
259    // approach
260  259211 nvarpos[i] = j++;
261    }
262  259225 nactivity[i] = 0.0;
263    }
264  1183 varpos = nvarpos;
265  1183 activity = nactivity;
266  1183 order = norder;
267  1183 lastVar = 1;
268    }
269   
270    /**
271    * Affiche les litteraux dans l'ordre de l'heuristique, la valeur de
272    * l'activite entre ().
273    *
274    * @return les litteraux dans l'ordre courant.
275    */
 
276  0 toggle @Override
277    public String toString() {
278  0 return "VSIDS like heuristics from MiniSAT using a sorted array"; //$NON-NLS-1$
279    }
280   
 
281  0 toggle public ILits getVocabulary() {
282  0 return lits;
283    }
284   
285    /*
286    * (non-Javadoc)
287    *
288    * @see org.sat4j.minisat.core.IOrder#printStat(java.io.PrintStream,
289    * java.lang.String)
290    */
 
291  0 toggle public void printStat(PrintWriter out, String prefix) {
292  0 out.println(prefix + "non guided choices\t" + nullchoice); //$NON-NLS-1$
293    // out.println(prefix + "random choices\t" + randchoice);
294    }
295   
 
296    toggle public void assignLiteral(int p) {
297    // do nothing
298    }
299   
300    }
 
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.