Clover Coverage Report
Coverage timestamp: mer. juin 27 2007 07:27:16 CEST
28   282   1   1
0   104   1   28
28     1  
1    
 
  SolverDecorator       Line # 48 28 1 32,1% 0.32142857
 
  (5)
 
1    /*
2    * SAT4J: a SATisfiability library for Java Copyright (C) 2004-2006 Daniel Le Berre
3    *
4    * Based on the original minisat specification from:
5    *
6    * An extensible SAT solver. Niklas E?n and Niklas S?rensson. Proceedings of the
7    * Sixth International Conference on Theory and Applications of Satisfiability
8    * Testing, LNCS 2919, pp 502-518, 2003.
9    *
10    * This library is free software; you can redistribute it and/or modify it under
11    * the terms of the GNU Lesser General Public License as published by the Free
12    * Software Foundation; either version 2.1 of the License, or (at your option)
13    * any later version.
14    *
15    * This library is distributed in the hope that it will be useful, but WITHOUT
16    * ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS
17    * FOR A PARTICULAR PURPOSE. See the GNU Lesser General Public License for more
18    * details.
19    *
20    * You should have received a copy of the GNU Lesser General Public License
21    * along with this library; if not, write to the Free Software Foundation, Inc.,
22    * 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA
23    *
24    */
25   
26    package org.sat4j.tools;
27   
28    import java.io.PrintStream;
29    import java.io.PrintWriter;
30    import java.io.Serializable;
31    import java.math.BigInteger;
32    import java.util.Map;
33   
34    import org.sat4j.specs.ContradictionException;
35    import org.sat4j.specs.IConstr;
36    import org.sat4j.specs.ISolver;
37    import org.sat4j.specs.IVec;
38    import org.sat4j.specs.IVecInt;
39    import org.sat4j.specs.TimeoutException;
40   
41    /**
42    * The aim of that class is to allow adding dynamic responsabilities to SAT
43    * solvers using the Decorator design pattern. The class is abstract because it
44    * does not makes sense to use it "as is".
45    *
46    * @author leberre
47    */
 
48    public abstract class SolverDecorator implements ISolver, Serializable {
49   
50    /*
51    * (non-Javadoc)
52    *
53    * @see org.sat4j.specs.ISolver#clearLearntClauses()
54    */
 
55  0 toggle public void clearLearntClauses() {
56  0 solver.clearLearntClauses();
57    }
58   
59    /*
60    * (non-Javadoc)
61    *
62    * @see org.sat4j.specs.IProblem#findModel()
63    */
 
64  0 toggle public int[] findModel() throws TimeoutException {
65  0 return solver.findModel();
66    }
67   
68    /*
69    * (non-Javadoc)
70    *
71    * @see org.sat4j.specs.IProblem#findModel(org.sat4j.specs.IVecInt)
72    */
 
73  0 toggle public int[] findModel(IVecInt assumps) throws TimeoutException {
74  0 return solver.findModel(assumps);
75    }
76   
77    /*
78    * (non-Javadoc)
79    *
80    * @see org.sat4j.specs.IProblem#model(int)
81    */
 
82  0 toggle public boolean model(int var) {
83  0 return solver.model(var);
84    }
85   
 
86  0 toggle public void setExpectedNumberOfClauses(int nb) {
87  0 solver.setExpectedNumberOfClauses(nb);
88    }
89   
90    /*
91    * (non-Javadoc)
92    *
93    * @see org.sat4j.specs.ISolver#getTimeout()
94    */
 
95  0 toggle public int getTimeout() {
96  0 return solver.getTimeout();
97    }
98   
99    /*
100    * (non-Javadoc)
101    *
102    * @see org.sat4j.specs.ISolver#toString(java.lang.String)
103    */
 
104  0 toggle public String toString(String prefix) {
105  0 return solver.toString(prefix);
106    }
107   
108    /*
109    * (non-Javadoc)
110    *
111    * @see org.sat4j.specs.ISolver#printStat(java.io.PrintStream,
112    * java.lang.String)
113    */
 
114  0 toggle @Deprecated
115    public void printStat(PrintStream out, String prefix) {
116  0 solver.printStat(out, prefix);
117    }
118   
 
119  0 toggle public void printStat(PrintWriter out, String prefix) {
120  0 solver.printStat(out, prefix);
121    }
122   
123    private final ISolver solver;
124   
125    /**
126    *
127    */
 
128  5 toggle public SolverDecorator(ISolver solver) {
129  5 this.solver = solver;
130    }
131   
132    /*
133    * (non-Javadoc)
134    *
135    * @see org.sat4j.ISolver#newVar()
136    */
 
137  0 toggle public int newVar() {
138  0 return solver.newVar();
139    }
140   
141    /*
142    * (non-Javadoc)
143    *
144    * @see org.sat4j.ISolver#newVar(int)
145    */
 
146  5 toggle public int newVar(int howmany) {
147  5 return solver.newVar(howmany);
148    }
149   
150    /*
151    * (non-Javadoc)
152    *
153    * @see org.sat4j.ISolver#addClause(org.sat4j.datatype.VecInt)
154    */
 
155  38 toggle public IConstr addClause(IVecInt literals) throws ContradictionException {
156  38 return solver.addClause(literals);
157    }
158   
 
159  0 toggle public void addAllClauses(IVec<IVecInt> clauses)
160    throws ContradictionException {
161  0 solver.addAllClauses(clauses);
162    }
163   
164    /*
165    * (non-Javadoc)
166    *
167    * @see org.sat4j.ISolver#addAtMost(org.sat4j.datatype.VecInt, int)
168    */
 
169  13 toggle public IConstr addAtMost(IVecInt literals, int degree)
170    throws ContradictionException {
171  13 return solver.addAtMost(literals, degree);
172    }
173   
174    /*
175    * (non-Javadoc)
176    *
177    * @see org.sat4j.ISolver#addAtLeast(org.sat4j.datatype.VecInt, int)
178    */
 
179  0 toggle public IConstr addAtLeast(IVecInt literals, int degree)
180    throws ContradictionException {
181  0 return solver.addAtLeast(literals, degree);
182    }
183   
 
184  0 toggle public IConstr addPseudoBoolean(IVecInt literals, IVec<BigInteger> coeffs,
185    boolean moreThan, BigInteger degree) throws ContradictionException {
186  0 return solver.addPseudoBoolean(literals, coeffs, moreThan, degree);
187    }
188   
189    /*
190    * (non-Javadoc)
191    *
192    * @see org.sat4j.ISolver#model()
193    */
 
194  40 toggle public int[] model() {
195  40 return solver.model();
196    }
197   
198    /*
199    * (non-Javadoc)
200    *
201    * @see org.sat4j.ISolver#isSatisfiable()
202    */
 
203  35 toggle public boolean isSatisfiable() throws TimeoutException {
204  35 return solver.isSatisfiable();
205    }
206   
207    /*
208    * (non-Javadoc)
209    *
210    * @see org.sat4j.ISolver#isSatisfiable(org.sat4j.datatype.VecInt)
211    */
 
212  12 toggle public boolean isSatisfiable(IVecInt assumps) throws TimeoutException {
213  12 return solver.isSatisfiable(assumps);
214    }
215   
216    /*
217    * (non-Javadoc)
218    *
219    * @see org.sat4j.ISolver#setTimeout(int)
220    */
 
221  0 toggle public void setTimeout(int t) {
222  0 solver.setTimeout(t);
223    }
224   
225    /*
226    * (non-Javadoc)
227    *
228    * @see org.sat4j.ISolver#setTimeoutMs(int)
229    */
 
230  0 toggle public void setTimeoutMs(long t) {
231  0 solver.setTimeoutMs(t);
232    }
233   
234    /*
235    * (non-Javadoc)
236    *
237    * @see org.sat4j.ISolver#nConstraints()
238    */
 
239  0 toggle public int nConstraints() {
240  0 return solver.nConstraints();
241    }
242   
243    /*
244    * (non-Javadoc)
245    *
246    * @see org.sat4j.ISolver#nVars()
247    */
 
248  52 toggle public int nVars() {
249  52 return solver.nVars();
250    }
251   
252    /*
253    * (non-Javadoc)
254    *
255    * @see org.sat4j.ISolver#reset()
256    */
 
257  0 toggle public void reset() {
258  0 solver.reset();
259    }
260   
 
261  0 toggle public ISolver decorated() {
262  0 return solver;
263    }
264   
265    /*
266    * (non-Javadoc)
267    *
268    * @see org.sat4j.specs.ISolver#removeConstr(org.sat4j.minisat.core.Constr)
269    */
 
270  4 toggle public boolean removeConstr(IConstr c) {
271  4 return solver.removeConstr(c);
272    }
273   
274    /*
275    * (non-Javadoc)
276    *
277    * @see org.sat4j.specs.ISolver#getStat()
278    */
 
279  0 toggle public Map<String, Number> getStat() {
280  0 return solver.getStat();
281    }
282    }