Clover coverage report -

Coverage timestamp: jeu. sept. 29 2005 23:57:39 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	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		}