Clover coverage report -
Coverage timestamp: jeu. sept. 29 2005 23:57:39 CEST
Overview   Package   File
    FRAMES   NO FRAMES  
file stats: LOC: 282   Methods: 16
NCLOC: 136   Classes: 1
 
 Source file Conditionals Statements Methods TOTAL
VarOrder.java 83,3% 84,2% 75% 82,5%
coverage coverage
 1    /*
 2    * SAT4J: a SATisfiability library for Java
 3    * Copyright (C) 2004 Daniel Le Berre
 4    *
 5    * Based on the original minisat specification from:
 6    *
 7    * An extensible SAT solver. Niklas Eï¿œn and Niklas Sï¿œrensson.
 8    * Proceedings of the Sixth International Conference on Theory
 9    * and Applications of Satisfiability Testing, LNCS 2919,
 10    * pp 502-518, 2003.
 11    *
 12    * This library is free software; you can redistribute it and/or
 13    * modify it under the terms of the GNU Lesser General Public
 14    * License as published by the Free Software Foundation; either
 15    * version 2.1 of the License, or (at your option) any later version.
 16    *
 17    * This library is distributed in the hope that it will be useful,
 18    * but WITHOUT ANY WARRANTY; without even the implied warranty of
 19    * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU
 20    * Lesser General Public License for more details.
 21    *
 22    * You should have received a copy of the GNU Lesser General Public
 23    * License along with this library; if not, write to the Free Software
 24    * Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA
 25    *
 26    */
 27   
 28    package org.sat4j.minisat.orders;
 29   
 30    import java.io.PrintStream;
 31    import java.io.Serializable;
 32    import java.util.Random;
 33   
 34    import org.sat4j.minisat.core.ILits;
 35    import org.sat4j.minisat.core.IOrder;
 36   
 37    /*
 38    * Created on 16 oct. 2003
 39    */
 40   
 41    /**
 42    * @author leberre Heuristique du prouveur. Changement par rapport au MiniSAT
 43    * original : la gestion activity est faite ici et non plus dans Solver.
 44    */
 45    public class VarOrder implements Serializable, IOrder {
 46   
 47    private static final long serialVersionUID = 1L;
 48   
 49    /**
 50    * Comparateur permettant de trier les variables
 51    */
 52    private static final double VAR_RESCALE_FACTOR = 1e-100;
 53   
 54    private static final double VAR_RESCALE_BOUND = 1 / VAR_RESCALE_FACTOR;
 55   
 56    /**
 57    * mesure heuristique de l'activitï¿œ d'une variable.
 58    */
 59    protected double[] activity = new double[1];
 60   
 61    /**
 62    * Derniï¿œre variable choisie
 63    */
 64    protected int lastVar = 1;
 65   
 66    /**
 67    * Ordre des variables
 68    */
 69    protected int[] order = new int[1];
 70   
 71    private double varDecay = 1.0;
 72   
 73    /**
 74    * incrï¿œment pour l'activitï¿œ des variables.
 75    */
 76    private double varInc = 1.0;
 77   
 78    /**
 79    * position des variables
 80    */
 81    protected int[] varpos = new int[1];
 82   
 83    protected ILits lits;
 84   
 85    private long nullchoice = 0;
 86   
 87    private long randchoice = 0;
 88   
 89    private Random rand = new Random(12345);
 90   
 91    private final static double RANDOM_WALK = 0.05;
 92   
 93    /* (non-Javadoc)
 94    * @see org.sat4j.minisat.core.IOrder#setLits(org.sat4j.minisat.core.ILits)
 95    */
 96  2137 public void setLits(ILits lits) {
 97  2137 this.lits = lits;
 98    }
 99   
 100    /* (non-Javadoc)
 101    * @see org.sat4j.minisat.core.IOrder#newVar()
 102    */
 103  250626 public void newVar() {
 104  250626 newVar(1);
 105    }
 106   
 107    /* (non-Javadoc)
 108    * @see org.sat4j.minisat.core.IOrder#newVar(int)
 109    */
 110  252278 public void newVar(int howmany) {
 111    }
 112   
 113    /* (non-Javadoc)
 114    * @see org.sat4j.minisat.core.IOrder#select()
 115    */
 116  130602264 public int select() {
 117    assert lastVar > 0;
 118  130602264 for (int i = lastVar; i < order.length; i++) {
 119    assert i > 0;
 120  1967877296 if (lits.isUnassigned(order[i])) {
 121  130602263 lastVar = i;
 122  130602263 if (activity[i] < 0.0001) {
 123    // if (rand.nextDouble() <= RANDOM_WALK) {
 124    // int randomchoice = rand.nextInt(order.length - i) + i;
 125    // assert randomchoice >= i;
 126    // if ((randomchoice > i)
 127    // && lits.isUnassigned(order[randomchoice])) {
 128    // randchoice++;
 129    // return order[randomchoice];
 130    // }
 131    // }
 132  15509425 nullchoice++;
 133    }
 134  130602263 return order[i];
 135    }
 136    }
 137  1 return ILits.UNDEFINED;
 138    }
 139   
 140    /**
 141    * Change la valeur de varDecay.
 142    *
 143    * @param d
 144    * la nouvelle valeur de varDecay
 145    */
 146  4242 public void setVarDecay(double d) {
 147  4242 varDecay = d;
 148    }
 149   
 150    /* (non-Javadoc)
 151    * @see org.sat4j.minisat.core.IOrder#undo(int)
 152    */
 153    public void undo(int x) {
 154    assert x > 0;
 155    assert x < order.length;
 156    int pos = varpos[x];
 157    if (pos < lastVar) {
 158  3031133 lastVar = pos;
 159    }
 160    assert lastVar > 0;
 161    }
 162   
 163    /* (non-Javadoc)
 164    * @see org.sat4j.minisat.core.IOrder#updateVar(int)
 165    */
 166    public void updateVar(int p) {
 167    assert p > 1;
 168    final int var = p >> 1;
 169   
 170    updateActivity(var);
 171    int i = varpos[var];
 172  2092083337 for (; i > 1 // because there is nothing at i=0
 173    && (activity[order[i - 1] >> 1] < activity[var]); i--) {
 174    assert i > 1;
 175    // echange p avec son predecesseur
 176    final int orderpm1 = order[i - 1];
 177    assert varpos[orderpm1 >> 1] == i - 1;
 178    varpos[orderpm1 >> 1] = i;
 179    order[i] = orderpm1;
 180    }
 181    assert i >= 1;
 182    varpos[var] = i;
 183    order[i] = p;
 184   
 185    if (i < lastVar) {
 186  125723577 lastVar = i;
 187    }
 188    }
 189   
 190    protected void updateActivity(final int var) {
 191    if ((activity[var] += varInc) > VAR_RESCALE_BOUND) {
 192  17353 varRescaleActivity();
 193    }
 194    }
 195   
 196    /**
 197    *
 198    */
 199  82945129 public void varDecayActivity() {
 200  82945129 varInc *= varDecay;
 201    }
 202   
 203    /**
 204    *
 205    */
 206  17353 private void varRescaleActivity() {
 207  17353 for (int i = 1; i < activity.length; i++) {
 208  1917964 activity[i] *= VAR_RESCALE_FACTOR;
 209    }
 210  17353 varInc *= VAR_RESCALE_FACTOR;
 211    }
 212   
 213  17347341 public double varActivity(int p) {
 214  17347341 return activity[p >> 1];
 215    }
 216   
 217    /**
 218    *
 219    */
 220  0 public int numberOfInterestingVariables() {
 221  0 int cpt = 0;
 222  0 for (int i = 1; i < activity.length; i++) {
 223  0 if (activity[i] > 1.0) {
 224  0 cpt++;
 225    }
 226    }
 227  0 return cpt;
 228    }
 229   
 230    /* (non-Javadoc)
 231    * @see org.sat4j.minisat.core.IOrder#init()
 232    */
 233  1981 public void init() {
 234  1981 int nlength = lits.nVars() + 1;
 235  1981 int reallength = lits.realnVars()+1;
 236  1981 int[] nvarpos = new int[nlength];
 237  1981 double[] nactivity = new double[nlength];
 238  1981 int[] norder = new int[reallength];
 239  1981 nvarpos[0] = -1;
 240  1981 nactivity[0] = -1;
 241  1981 norder[0] = ILits.UNDEFINED;
 242  1981 for (int i = 1,j=1; i < nlength; i++) {
 243    assert i > 0;
 244    assert i <= lits.nVars() : "" + lits.nVars() + "/" + i;
 245  655771 if (lits.belongsToPool(i)) {
 246  655767 norder[j] = lits.getFromPool(i) ^ 1; // Looks a
 247    // promising
 248    // approach
 249  655767 nvarpos[i] = j++;
 250    }
 251  655771 nactivity[i] = 0.0;
 252    }
 253  1981 varpos = nvarpos;
 254  1981 activity = nactivity;
 255  1981 order = norder;
 256  1981 lastVar = 1;
 257    }
 258   
 259    /**
 260    * Affiche les littï¿œraux dans l'ordre de l'heuristique, la valeur de
 261    * l'activite entre ().
 262    *
 263    * @return les littï¿œraux dans l'ordre courant.
 264    */
 265  0 @Override
 266    public String toString() {
 267  0 return "VSIDS like heuristics from MiniSAT using a sorted array";
 268    }
 269   
 270  0 public ILits getVocabulary() {
 271  0 return lits;
 272    }
 273   
 274    /* (non-Javadoc)
 275    * @see org.sat4j.minisat.core.IOrder#printStat(java.io.PrintStream, java.lang.String)
 276    */
 277  0 public void printStat(PrintStream out, String prefix) {
 278  0 out.println(prefix + "non guided choices\t" + nullchoice);
 279  0 out.println(prefix + "random choices\t" + randchoice);
 280    }
 281   
 282    }
 
CloverReport generated by Clover Code Coverage v1.3.9
jeu. sept. 29 2005 23:57:47 CEST.		   Open Source License registered to the OpenSAT Project. This license of Clover is provided to support the development of OpenSAT only.