Clover coverage report -
Coverage timestamp: jeu. sept. 29 2005 23:57:39 CEST
file stats: LOC: 138   Methods: 8
NCLOC: 70   Classes: 2
 
 Source file Conditionals Statements Methods TOTAL
JWOrder.java 100% 93,5% 75% 91,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.util.ArrayList;
 31    import java.util.Collections;
 32   
 33    import org.sat4j.minisat.core.ILits;
 34    import org.sat4j.minisat.core.ILits23;
 35   
 36    /*
 37    * Created on 16 oct. 2003
 38    */
 39   
 40    /**
 41    * @author leberre Heuristique du prouveur. Changement par rapport au MiniSAT
 42    * original : la gestion activity est faite ici et non plus dans Solver.
 43    */
 44    public class JWOrder extends VarOrder {
 45   
 46    private static final long serialVersionUID = 1L;
 47   
 48    private ILits23 lits;
 49   
 50  475778573 private int computeWeight(int var) {
 51  475778573 final int p = (var << 1);
 52  475778573 int pos2 = lits.nBinaryClauses(p);
 53  475778573 int neg2 = lits.nBinaryClauses(p ^ 1);
 54  475778573 int pos3 = lits.nTernaryClauses(p);
 55  475778573 int neg3 = lits.nTernaryClauses(p ^ 1);
 56  475778573 return (pos2 * neg2 * 100 + pos2 + neg2) * 5 + pos3 * neg3 * 10 + pos3
 57    + neg3;
 58    }
 59   
 60    class Temp implements Comparable<Temp> {
 61    private int id;
 62   
 63    private int count;
 64   
 65  25475 Temp(int id) {
 66  25475 this.id = id;
 67  25475 count = computeWeight(id >> 1);
 68    }
 69   
 70  76834 public int compareTo(Temp t) {
 71  76834 if (count == 0) {
 72  49 return Integer.MAX_VALUE;
 73    }
 74  76785 if (t.count == 0) {
 75  10 return -1;
 76    }
 77  76775 return t.count - count;
 78    }
 79   
 80  0 @Override
 81    public String toString() {
 82  0 return "" + id + "(" + count + ")";
 83    }
 84    }
 85   
 86    /*
 87    * (non-Javadoc)
 88    *
 89    * @see org.sat4j.minisat.VarOrder#setLits(org.sat4j.minisat.Lits)
 90    */
 91  103 @Override
 92    public void setLits(ILits lits) {
 93  103 super.setLits(lits);
 94  103 this.lits = (ILits23) lits;
 95    }
 96   
 97    /*
 98    * (non-Javadoc)
 99    *
 100    * @see org.sat4j.minisat.IHeuristics#init()
 101    */
 102  103 @Override
 103    public void init() {
 104  103 super.init();
 105  103 ArrayList<Temp> v = new ArrayList<Temp>(order.length);
 106   
 107  103 for (int i = 1; i < order.length; i++) {
 108  25475 Temp t = new Temp(order[i]);
 109  25475 v.add(t);
 110    }
 111  103 Collections.sort(v);
 112    // System.out.println(v);
 113  103 for (int i = 0; i < v.size(); i++) {
 114  25475 Temp t = v.get(i);
 115  25475 order[i + 1] = t.id;
 116  25475 int index = t.id >> 1;
 117  25475 varpos[index] = i + 1;
 118  25475 activity[t.id >> 1] = t.count;
 119    }
 120  103 lastVar = 1;
 121   
 122    }
 123   
 124    /*
 125    * (non-Javadoc)
 126    *
 127    * @see org.sat4j.minisat.core.VarOrder#updateActivity(int)
 128    */
 129  475753098 @Override
 130    protected void updateActivity(int var) {
 131  475753098 activity[var] = computeWeight(var);
 132    }
 133   
 134  0 @Override
 135    public String toString() {
 136  0 return "Jeroslow-Wang static like heuristics updated when new clauses are learnt";
 137    }
 138    }