Clover coverage report -

Coverage timestamp: jeu. sept. 29 2005 23:57:39 CEST

FRAMES NO FRAMES

file stats:	LOC:	116		Methods:	9
	NCLOC:	57		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 java.io.Serializable;
31
32		import org.sat4j.minisat.core.Constr;
33		import org.sat4j.minisat.core.ILits;
34		import org.sat4j.minisat.core.LearningStrategy;
35		import org.sat4j.minisat.core.Solver;
36		import org.sat4j.minisat.core.VarActivityListener;
37
38		/**
39		* Learn only clauses which size is smaller than a percentage of the number of
40		* variables.
41		*
42		* @author leberre
43		*/
44		public class LimitedLearning implements LearningStrategy, Serializable {
45
46		private static final long serialVersionUID = 1L;
47
48		private final NoLearningButHeuristics none;
49
50		private final MiniSATLearning all;
51
52		private final int maxpercent;
53
54		private ILits lits;
55
56		private int bound;
57
58	204	public LimitedLearning() {
59	204	this(10);
60		}
61
62	1089	public LimitedLearning(int percent) {
63	1089	maxpercent = percent;
64		}
65
66		{
67	1089	none = new NoLearningButHeuristics();
68	1089	all = new MiniSATLearning();
69
70		}
71
72	1089	public void setSolver(Solver s) {
73	1089	this.lits = s.getVocabulary();
74	1089	setVarActivityListener(s);
75	1089	all.setDataStructureFactory(s.getDSFactory());
76		}
77
78		/*
79		* (non-Javadoc)
80		*
81		* @see org.sat4j.minisat.LearningScheme#learns(org.sat4j.minisat.Solver,
82		* org.sat4j.minisat.datatype.Vec)
83		*/
84	69863213	public void learns(Constr constr) {
85	69863213	if (learningCondition(constr)) {
86	647015	all.learns(constr);
87		} else {
88	69216198	none.learns(constr);
89		}
90		}
91
92	69231639	protected boolean learningCondition(Constr constr) {
93	69231639	return constr.size() <= bound;
94		}
95
96	950	public void init() {
97	950	setBound(lits.realnVars() * maxpercent / 100);
98	950	all.init();
99	950	none.init();
100		}
101
102	1052	protected void setBound(int newbound) {
103	1052	bound = newbound;
104		}
105
106	0	@Override
107		public String toString() {
108	0	return "Limit learning to clauses of size smaller or equal to "
109		+ maxpercent + "% of the number of variables";
110		}
111
112	1089	public void setVarActivityListener(VarActivityListener s) {
113	1089	none.setVarActivityListener(s);
114	1089	all.setVarActivityListener(s);
115		}
116		}