Clover coverage report -
Coverage timestamp: jeu. juin 15 2006 08:24:33 CEST
Overview   Package   File
    FRAMES   NO FRAMES  
file stats: LOC: 287   Methods: 16
NCLOC: 131   Classes: 1
 
 Source file Conditionals Statements Methods TOTAL
VarOrder.java 83,3% 85,7% 75% 83,3%
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.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 implements Serializable, IOrder {
 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'activitï¿œ d'une variable.
 55    */
 56    protected double[] activity = new double[1];
 57   
 58    /**
 59    * Derniï¿œre 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    * incrï¿œment pour l'activitï¿œ 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 ILits 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    * @see org.sat4j.minisat.core.IOrder#setLits(org.sat4j.minisat.core.ILits)
 93    */
 94  1236 public void setLits(ILits lits) {
 95  1236 this.lits = lits;
 96    }
 97   
 98    /*
 99    * (non-Javadoc)
 100    * @see org.sat4j.minisat.core.IOrder#newVar()
 101    */
 102  6774 public void newVar() {
 103  6774 newVar(1);
 104    }
 105   
 106    /*
 107    * (non-Javadoc)
 108    * @see org.sat4j.minisat.core.IOrder#newVar(int)
 109    */
 110  7808 public void newVar(int howmany) {
 111    }
 112   
 113    /*
 114    * (non-Javadoc)
 115    * @see org.sat4j.minisat.core.IOrder#select()
 116    */
 117  172588613 public int select() {
 118    assert lastVar > 0;
 119  172588613 for (int i = lastVar; i < order.length; i++) {
 120    assert i > 0;
 121    if (lits.isUnassigned(order[i])) {
 122  172588612 lastVar = i;
 123  172588612 if (activity[i] < 0.0001) {
 124    // if (rand.nextDouble() <= RANDOM_WALK) {
 125    // int randomchoice = rand.nextInt(order.length - i) + i;
 126    // assert randomchoice >= i;
 127    // if ((randomchoice > i)
 128    // && lits.isUnassigned(order[randomchoice])) {
 129    // randchoice++;
 130    // return order[randomchoice];
 131    // }
 132    // }
 133  18665577 nullchoice++;
 134    }
 135  172588612 return order[i];
 136    }
 137    }
 138  1 return ILits.UNDEFINED;
 139    }
 140   
 141    /**
 142    * Change la valeur de varDecay.
 143    *
 144    * @param d la nouvelle valeur de varDecay
 145    */
 146  2429 public void setVarDecay(double d) {
 147  2429 varDecay = d;
 148    }
 149   
 150    /*
 151    * (non-Javadoc)
 152    * @see org.sat4j.minisat.core.IOrder#undo(int)
 153    */
 154    public void undo(int x) {
 155    assert x > 0;
 156    assert x < order.length;
 157    int pos = varpos[x];
 158    if (pos < lastVar) {
 159  3644840 lastVar = pos;
 160    }
 161    assert lastVar > 0;
 162    }
 163   
 164    /*
 165    * (non-Javadoc)
 166    * @see org.sat4j.minisat.core.IOrder#updateVar(int)
 167    */
 168    public void updateVar(int p) {
 169    assert p > 1;
 170    final int var = p >> 1;
 171   
 172    updateActivity(var);
 173    int i = varpos[var];
 174    for (; i > 1 // because there is nothing at i=0
 175    && (activity[order[i - 1] >> 1] < activity[var]); i--) {
 176    assert i > 1;
 177    // echange p avec son predecesseur
 178  516451552 final int orderpm1 = order[i - 1];
 179    assert varpos[orderpm1 >> 1] == i - 1;
 180  516451552 varpos[orderpm1 >> 1] = i;
 181  516451552 order[i] = orderpm1;
 182    }
 183    assert i >= 1;
 184    varpos[var] = i;
 185    order[i] = p;
 186   
 187    if (i < lastVar) {
 188  155070311 lastVar = i;
 189    }
 190    }
 191   
 192    protected void updateActivity(final int var) {
 193    if ((activity[var] += varInc) > VAR_RESCALE_BOUND) {
 194  20913 varRescaleActivity();
 195    }
 196    }
 197   
 198    /**
 199    *
 200    */
 201  101675969 public void varDecayActivity() {
 202  101675969 varInc *= varDecay;
 203    }
 204   
 205    /**
 206    *
 207    */
 208  20913 private void varRescaleActivity() {
 209  20913 for (int i = 1; i < activity.length; i++) {
 210  1833160 activity[i] *= VAR_RESCALE_FACTOR;
 211    }
 212  20913 varInc *= VAR_RESCALE_FACTOR;
 213    }
 214   
 215  2498007 public double varActivity(int p) {
 216  2498007 return activity[p >> 1];
 217    }
 218   
 219    /**
 220    *
 221    */
 222  0 public int numberOfInterestingVariables() {
 223  0 int cpt = 0;
 224  0 for (int i = 1; i < activity.length; i++) {
 225  0 if (activity[i] > 1.0) {
 226  0 cpt++;
 227    }
 228    }
 229  0 return cpt;
 230    }
 231   
 232    /*
 233    * (non-Javadoc)
 234    * @see org.sat4j.minisat.core.IOrder#init()
 235    */
 236  1183 public void init() {
 237  1183 int nlength = lits.nVars() + 1;
 238  1183 int reallength = lits.realnVars() + 1;
 239  1183 int[] nvarpos = new int[nlength];
 240  1183 double[] nactivity = new double[nlength];
 241  1183 int[] norder = new int[reallength];
 242  1183 nvarpos[0] = -1;
 243  1183 nactivity[0] = -1;
 244  1183 norder[0] = ILits.UNDEFINED;
 245  1183 for (int i = 1, j = 1; i < nlength; i++) {
 246    assert i > 0;
 247    assert i <= lits.nVars() : "" + lits.nVars() + "/" + i; //$NON-NLS-1$ //$NON-NLS-2$
 248  259225 if (lits.belongsToPool(i)) {
 249  259211 norder[j] = lits.getFromPool(i) ^ 1; // Looks a
 250    // promising
 251    // approach
 252  259211 nvarpos[i] = j++;
 253    }
 254  259225 nactivity[i] = 0.0;
 255    }
 256  1183 varpos = nvarpos;
 257  1183 activity = nactivity;
 258  1183 order = norder;
 259  1183 lastVar = 1;
 260    }
 261   
 262    /**
 263    * Affiche les littï¿œraux dans l'ordre de l'heuristique, la valeur de
 264    * l'activite entre ().
 265    *
 266    * @return les littï¿œraux dans l'ordre courant.
 267    */
 268  0 @Override
 269    public String toString() {
 270  0 return "VSIDS like heuristics from MiniSAT using a sorted array"; //$NON-NLS-1$
 271    }
 272   
 273  0 public ILits getVocabulary() {
 274  0 return lits;
 275    }
 276   
 277    /*
 278    * (non-Javadoc)
 279    * @see org.sat4j.minisat.core.IOrder#printStat(java.io.PrintStream,
 280    * java.lang.String)
 281    */
 282  0 public void printStat(PrintWriter out, String prefix) {
 283  0 out.println(prefix + "non guided choices\t" + nullchoice); //$NON-NLS-1$
 284    // out.println(prefix + "random choices\t" + randchoice);
 285    }
 286   
 287    }
 
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.