Clover coverage report -

Coverage timestamp: jeu. juin 15 2006 08:24:33 CEST

FRAMES NO FRAMES

file stats:	LOC:	138		Methods:	8
	NCLOC:	70		Classes:	2

Source file

Conditionals

Statements

Methods

TOTAL

JWOrder.java

100%

93,5%

75%

91,5%

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	802815692	private int computeWeight(int var) {
51	802815692	final int p = (var << 1);
52	802815692	int pos2 = lits.nBinaryClauses(p);
53	802815692	int neg2 = lits.nBinaryClauses(p ^ 1);
54	802815692	int pos3 = lits.nTernaryClauses(p);
55	802815692	int neg3 = lits.nTernaryClauses(p ^ 1);
56	802815692	return (pos2 * neg2 * 100 + pos2 + neg2) * 5 + pos3 * neg3 * 10 + pos3
57		+ neg3;
58		}
59
60		class Temp implements Comparable<Temp> {
61		private final int id;
62
63		private final int count;
64
65	25565	Temp(int id) {
66	25565	this.id = id;
67	25565	count = computeWeight(id >> 1);
68		}
69
70	76923	public int compareTo(Temp t) {
71	76923	if (count == 0) {
72	49	return Integer.MAX_VALUE;
73		}
74	76874	if (t.count == 0) {
75	10	return -1;
76		}
77	76864	return t.count - count;
78		}
79
80	0	@Override
81		public String toString() {
82	0	return "" + id + "(" + count + ")"; //$NON-NLS-1$//$NON-NLS-2$ //$NON-NLS-3$
83		}
84		}
85
86		/*
87		* (non-Javadoc)
88		*
89		* @see org.sat4j.minisat.VarOrder#setLits(org.sat4j.minisat.Lits)
90		*/
91	104	@Override
92		public void setLits(ILits lits) {
93	104	super.setLits(lits);
94	104	this.lits = (ILits23) lits;
95		}
96
97		/*
98		* (non-Javadoc)
99		*
100		* @see org.sat4j.minisat.IHeuristics#init()
101		*/
102	104	@Override
103		public void init() {
104	104	super.init();
105	104	ArrayList<Temp> v = new ArrayList<Temp>(order.length);
106
107	104	for (int i = 1; i < order.length; i++) {
108	25565	Temp t = new Temp(order[i]);
109	25565	v.add(t);
110		}
111	104	Collections.sort(v);
112		// System.out.println(v);
113	104	for (int i = 0; i < v.size(); i++) {
114	25565	Temp t = v.get(i);
115	25565	order[i + 1] = t.id;
116	25565	int index = t.id >> 1;
117	25565	varpos[index] = i + 1;
118	25565	activity[t.id >> 1] = t.count;
119		}
120	104	lastVar = 1;
121
122		}
123
124		/*
125		* (non-Javadoc)
126		*
127		* @see org.sat4j.minisat.core.VarOrder#updateActivity(int)
128		*/
129	802790127	@Override
130		protected void updateActivity(int var) {
131	802790127	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"; //$NON-NLS-1$
137		}
138		}