Clover coverage report -
Coverage timestamp: jeu. sept. 29 2005 23:57:39 CEST
Overview   Package   File
    FRAMES   NO FRAMES  
file stats: LOC: 233   Methods: 16
NCLOC: 116   Classes: 1
 
 Source file Conditionals Statements Methods TOTAL
VarOrderHeap.java 75% 72% 62,5% 71,1%
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.Heap;
 35    import org.sat4j.minisat.core.ILits;
 36    import org.sat4j.minisat.core.IOrder;
 37   
 38    /*
 39    * Created on 16 oct. 2003
 40    */
 41   
 42    /**
 43    * @author leberre Heuristique du prouveur. Changement par rapport au MiniSAT
 44    * original : la gestion activity est faite ici et non plus dans Solver.
 45    */
 46    public class VarOrderHeap implements IOrder, Serializable {
 47   
 48    private static final long serialVersionUID = 1L;
 49   
 50    private static final double VAR_RESCALE_FACTOR = 1e-100;
 51   
 52    private static final double VAR_RESCALE_BOUND = 1 / VAR_RESCALE_FACTOR;
 53   
 54    /**
 55    * mesure heuristique de l'activitï¿œ d'une variable.
 56    */
 57    protected double[] activity = new double[1];
 58   
 59    private double varDecay = 1.0;
 60   
 61    /**
 62    * incrï¿œment pour l'activitï¿œ des variables.
 63    */
 64    private double varInc = 1.0;
 65   
 66    protected ILits lits;
 67   
 68    private long nullchoice = 0;
 69   
 70    private long randchoice = 0;
 71   
 72    private Random rand = new Random(12345);
 73   
 74    private final static double RANDOM_WALK = 0.05;
 75   
 76    private Heap heap;
 77   
 78    private int [] phase;
 79   
 80  6 public void setLits(ILits lits) {
 81  6 this.lits = lits;
 82    }
 83   
 84    /**
 85    * Appelï¿œe quand une nouvelle variable est crￜￜe.
 86    */
 87  0 public void newVar() {
 88  0 newVar(1);
 89    }
 90   
 91    /**
 92    * Appelï¿œe lorsque plusieurs variables sont crￜￜes
 93    *
 94    * @param howmany
 95    * le nombre de variables crￜￜes
 96    */
 97  6 public void newVar(int howmany) {
 98    }
 99   
 100    /**
 101    * Sï¿œlectionne une nouvelle variable, non affectï¿œe, ayant l'activitï¿œ
 102    * la plus ï¿œlevï¿œe.
 103    *
 104    * @return Lit.UNDEFINED si aucune variable n'est trouvï¿œe
 105    */
 106  16084353 public int select() {
 107  27776270 while (!heap.empty()) {
 108  27776270 int var = heap.getmin();
 109  27776270 int pos = var << 1;
 110  27776270 int neg = pos ^1;
 111  27776270 int next = phase[neg]>phase[pos]?neg:pos;
 112  27776270 if (lits.isUnassigned(next)) {
 113  16084353 if (activity[var] < 0.0001) {
 114  266 nullchoice++;
 115    }
 116  16084353 return next;
 117    }
 118    }
 119  0 return ILits.UNDEFINED;
 120    }
 121   
 122    /**
 123    * Change la valeur de varDecay.
 124    *
 125    * @param d
 126    * la nouvelle valeur de varDecay
 127    */
 128  136 public void setVarDecay(double d) {
 129  136 varDecay = d;
 130    }
 131   
 132    /**
 133    * Mï¿œthode appelï¿œe quand la variable x est dï¿œsaffectï¿œe.
 134    *
 135    * @param x
 136    */
 137  189162514 public void undo(int x) {
 138  189162514 if (!heap.inHeap(x))
 139  27776240 heap.insert(x);
 140    }
 141   
 142    /**
 143    * Appelï¿œe lorsque l'activitï¿œ de la variable x a changï¿œ.
 144    *
 145    * @param p a literal
 146    */
 147  858041964 public void updateVar(int p) {
 148  858041964 int var = p >> 1;
 149  858041964 updateActivity(var);
 150  858041964 phase[p]++;
 151  858041964 if (heap.inHeap(var))
 152  160626165 heap.increase(var);
 153    }
 154   
 155  858041964 protected void updateActivity(final int var) {
 156  858041964 if ((activity[var] += varInc) > VAR_RESCALE_BOUND) {
 157  2356 varRescaleActivity();
 158    }
 159    }
 160   
 161    /**
 162    *
 163    */
 164  10586966 public void varDecayActivity() {
 165  10586966 varInc *= varDecay;
 166    }
 167   
 168    /**
 169    *
 170    */
 171  2356 private void varRescaleActivity() {
 172  2356 for (int i = 1; i < activity.length; i++) {
 173  212040 activity[i] *= VAR_RESCALE_FACTOR;
 174    }
 175  2356 varInc *= VAR_RESCALE_FACTOR;
 176    }
 177   
 178  0 public double varActivity(int p) {
 179  0 return activity[p >> 1];
 180    }
 181   
 182    /**
 183    *
 184    */
 185  0 public int numberOfInterestingVariables() {
 186  0 int cpt = 0;
 187  0 for (int i = 1; i < activity.length; i++) {
 188  0 if (activity[i] > 1.0) {
 189  0 cpt++;
 190    }
 191    }
 192  0 return cpt;
 193    }
 194   
 195    /**
 196    * that method has the responsability to initialize all arrays in the
 197    * heuristics. PLEASE CALL super.init() IF YOU OVERRIDE THAT METHOD.
 198    */
 199  6 public void init() {
 200  6 int nlength = lits.nVars() + 1;
 201  6 activity = new double[nlength];
 202  6 phase = new int[nlength<<1^1];
 203  6 activity[0] = -1;
 204  6 heap = new Heap(activity);
 205  6 heap.setBounds(nlength);
 206  6 for (int i = 1; i < nlength; i++) {
 207    assert i > 0;
 208    assert i <= lits.nVars() : "" + lits.nVars() + "/" + i;
 209  540 activity[i] = 0.0;
 210  540 if (lits.belongsToPool(i)) {
 211  540 heap.insert(i);
 212  540 phase[i<<1] = 0;
 213  540 phase[(i<<1)^1] = 1;
 214    } else {
 215  0 phase[i<<1] = ILits.UNDEFINED;
 216  0 phase[(i<<1)^1] = ILits.UNDEFINED;
 217    }
 218    }
 219    }
 220   
 221  0 public String toString() {
 222  0 return "VSIDS like heuristics from MiniSAT using a heap";
 223    }
 224   
 225  0 public ILits getVocabulary() {
 226  0 return lits;
 227    }
 228   
 229  0 public void printStat(PrintStream out, String prefix) {
 230  0 out.println(prefix + "non guided choices\t" + nullchoice);
 231  0 out.println(prefix + "random choices\t" + randchoice);
 232    }
 233    }
 
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.