Clover coverage report -
Coverage timestamp: jeu. juin 15 2006 08:24:33 CEST
Overview   Package   File
    FRAMES   NO FRAMES  
file stats: LOC: 218   Methods: 16
NCLOC: 108   Classes: 1
 
 Source file Conditionals Statements Methods TOTAL
VarOrderHeap.java 72,7% 75,6% 68,8% 73,5%
coverage coverage
 1    /*
 2    * SAT4J: a SATisfiability library for Java Copyright (C) 2004 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
 7    * the Sixth International Conference on Theory and Applications of
 8    * Satisfiability 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 implements IOrder, 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'activitï¿œ d'une variable.
 53    */
 54    protected double[] activity = new double[1];
 55   
 56    private double varDecay = 1.0;
 57   
 58    /**
 59    * incrï¿œment pour l'activitï¿œ des variables.
 60    */
 61    private double varInc = 1.0;
 62   
 63    protected ILits lits;
 64   
 65    private long nullchoice = 0;
 66   
 67    protected Heap heap;
 68   
 69    protected int[] phase;
 70   
 71  1383 public void setLits(ILits lits) {
 72  1383 this.lits = lits;
 73    }
 74   
 75    /**
 76    * Appelï¿œe quand une nouvelle variable est crￜￜe.
 77    */
 78  659841 public void newVar() {
 79  659841 newVar(1);
 80    }
 81   
 82    /**
 83    * Appelï¿œe lorsque plusieurs variables sont crￜￜes
 84    *
 85    * @param howmany le nombre de variables crￜￜes
 86    */
 87  660484 public void newVar(int howmany) {
 88    }
 89   
 90    /**
 91    * Sï¿œlectionne une nouvelle variable, non affectï¿œe, ayant l'activitï¿œ
 92    * la plus ï¿œlevï¿œe.
 93    *
 94    * @return Lit.UNDEFINED si aucune variable n'est trouvï¿œe
 95    */
 96  53435489 public int select() {
 97  96752822 while (!heap.empty()) {
 98  96752822 int var = heap.getmin();
 99  96752822 int next = phase[var];
 100  96752822 if (lits.isUnassigned(next)) {
 101  53435489 if (activity[var] < 0.0001) {
 102  329005 nullchoice++;
 103    }
 104  53435489 return next;
 105    }
 106    }
 107  0 return ILits.UNDEFINED;
 108    }
 109   
 110    /**
 111    * Change la valeur de varDecay.
 112    *
 113    * @param d la nouvelle valeur de varDecay
 114    */
 115  2695 public void setVarDecay(double d) {
 116  2695 varDecay = d;
 117    }
 118   
 119    /**
 120    * Mï¿œthode appelï¿œe quand la variable x est dï¿œsaffectï¿œe.
 121    *
 122    * @param x
 123    */
 124  880632813 public void undo(int x) {
 125  880632813 if (!heap.inHeap(x))
 126  96744762 heap.insert(x);
 127    }
 128   
 129    /**
 130    * Appelï¿œe lorsque l'activitï¿œ de la variable x a changï¿œ.
 131    *
 132    * @param p a literal
 133    */
 134  411588354 public void updateVar(int p) {
 135  411588354 int var = p >> 1;
 136  411588354 updateActivity(var);
 137  411588354 phase[var] = p;
 138  411588354 if (heap.inHeap(var))
 139  741890987 heap.increase(var);
 140    }
 141   
 142  411588354 protected void updateActivity(final int var) {
 143  411588354 if ((activity[var] += varInc) > VAR_RESCALE_BOUND) {
 144  8422 varRescaleActivity();
 145    }
 146    }
 147   
 148    /**
 149    *
 150    */
 151  38114704 public void varDecayActivity() {
 152  38114704 varInc *= varDecay;
 153    }
 154   
 155    /**
 156    *
 157    */
 158  8422 private void varRescaleActivity() {
 159  8422 for (int i = 1; i < activity.length; i++) {
 160  1278780 activity[i] *= VAR_RESCALE_FACTOR;
 161    }
 162  8422 varInc *= VAR_RESCALE_FACTOR;
 163    }
 164   
 165  0 public double varActivity(int p) {
 166  0 return activity[p >> 1];
 167    }
 168   
 169    /**
 170    *
 171    */
 172  0 public int numberOfInterestingVariables() {
 173  0 int cpt = 0;
 174  0 for (int i = 1; i < activity.length; i++) {
 175  0 if (activity[i] > 1.0) {
 176  0 cpt++;
 177    }
 178    }
 179  0 return cpt;
 180    }
 181   
 182    /**
 183    * that method has the responsability to initialize all arrays in the
 184    * heuristics. PLEASE CALL super.init() IF YOU OVERRIDE THAT METHOD.
 185    */
 186  1245 public void init() {
 187  1245 int nlength = lits.nVars() + 1;
 188  1245 activity = new double[nlength];
 189  1245 phase = new int[nlength];
 190  1245 activity[0] = -1;
 191  1245 heap = new Heap(activity);
 192  1245 heap.setBounds(nlength);
 193  1245 for (int i = 1; i < nlength; i++) {
 194    assert i > 0;
 195    assert i <= lits.nVars() : "" + lits.nVars() + "/" + i; //$NON-NLS-1$ //$NON-NLS-2$
 196  806866 activity[i] = 0.0;
 197  806866 if (lits.belongsToPool(i)) {
 198  806866 heap.insert(i);
 199  806866 phase[i] = (i << 1) ^ 1;
 200    } else {
 201  0 phase[i] = ILits.UNDEFINED;
 202    }
 203    }
 204    }
 205   
 206  0 @Override
 207    public String toString() {
 208  0 return "VSIDS like heuristics from MiniSAT using a heap"; //$NON-NLS-1$
 209    }
 210   
 211  0 public ILits getVocabulary() {
 212  0 return lits;
 213    }
 214   
 215  0 public void printStat(PrintWriter out, String prefix) {
 216  0 out.println(prefix + "non guided choices\t" + nullchoice); //$NON-NLS-1$
 217    }
 218    }
 
CloverReport generated by Clover Code Coverage v1.3.9
jeu. juin 15 2006 08:24:39 CEST.		   Open Source License registered to the OpenSAT Project. This license of Clover is provided to support the development of OpenSAT only.