Clover coverage report -

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

FRAMES NO FRAMES

file stats:	LOC:	104		Methods:	9
	NCLOC:	54		Classes:	1

Source file

Conditionals

Statements

Methods

TOTAL

LimitedLearning.java

100%

94,4%

88,9%

93,1%

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.learning;
29
30		import org.sat4j.minisat.core.Constr;
31		import org.sat4j.minisat.core.ILits;
32		import org.sat4j.minisat.core.LearningStrategy;
33		import org.sat4j.minisat.core.Solver;
34		import org.sat4j.minisat.core.VarActivityListener;
35
36		/**
37		* Learn only clauses which size is smaller than a percentage of the number of
38		* variables.
39		*
40		* @author leberre
41		*/
42		public class LimitedLearning implements LearningStrategy {
43
44		private static final long serialVersionUID = 1L;
45
46		private final NoLearningButHeuristics none;
47
48		private final MiniSATLearning all;
49
50		private final int maxpercent;
51
52		private ILits lits;
53
54		private int bound;
55
56	205	public LimitedLearning() {
57	205	this(10);
58		}
59
60	1125	public LimitedLearning(int percent) {
61	1125	maxpercent = percent;
62	1125	none = new NoLearningButHeuristics();
63	1125	all = new MiniSATLearning();
64		}
65
66	1125	public void setSolver(Solver s) {
67	1125	this.lits = s.getVocabulary();
68	1125	setVarActivityListener(s);
69	1125	all.setDataStructureFactory(s.getDSFactory());
70		}
71
72	125758595	public void learns(Constr constr) {
73	125758595	if (learningCondition(constr)) {
74	104248	all.learns(constr);
75		} else {
76	125654347	none.learns(constr);
77		}
78		}
79
80	125672486	protected boolean learningCondition(Constr constr) {
81	125672486	return constr.size() <= bound;
82		}
83
84	969	public void init() {
85	969	setBound(lits.realnVars() * maxpercent / 100);
86	969	all.init();
87	969	none.init();
88		}
89
90	1072	protected void setBound(int newbound) {
91	1072	bound = newbound;
92		}
93
94	0	@Override
95		public String toString() {
96	0	return "Limit learning to clauses of size smaller or equal to " //$NON-NLS-1$
97		+ maxpercent + "% of the number of variables"; //$NON-NLS-1$
98		}
99
100	1125	public void setVarActivityListener(VarActivityListener s) {
101	1125	none.setVarActivityListener(s);
102	1125	all.setVarActivityListener(s);
103		}
104		}