View Javadoc

1   /*******************************************************************************
2    * SAT4J: a SATisfiability library for Java Copyright (C) 2004-2008 Daniel Le Berre
3    *
4    * All rights reserved. This program and the accompanying materials
5    * are made available under the terms of the Eclipse Public License v1.0
6    * which accompanies this distribution, and is available at
7    * http://www.eclipse.org/legal/epl-v10.html
8    *
9    * Alternatively, the contents of this file may be used under the terms of
10   * either the GNU Lesser General Public License Version 2.1 or later (the
11   * "LGPL"), in which case the provisions of the LGPL are applicable instead
12   * of those above. If you wish to allow use of your version of this file only
13   * under the terms of the LGPL, and not to allow others to use your version of
14   * this file under the terms of the EPL, indicate your decision by deleting
15   * the provisions above and replace them with the notice and other provisions
16   * required by the LGPL. If you do not delete the provisions above, a recipient
17   * may use your version of this file under the terms of the EPL or the LGPL.
18   * 
19   * Based on the original MiniSat specification from:
20   * 
21   * An extensible SAT solver. Niklas Een and Niklas Sorensson. Proceedings of the
22   * Sixth International Conference on Theory and Applications of Satisfiability
23   * Testing, LNCS 2919, pp 502-518, 2003.
24   *
25   * See www.minisat.se for the original solver in C++.
26   * 
27   *******************************************************************************/
28  package org.sat4j.tools;
29  
30  import java.io.PrintStream;
31  import java.io.PrintWriter;
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.SearchListener;
40  import org.sat4j.specs.TimeoutException;
41  
42  /**
43   * The aim of that class is to allow adding dynamic responsabilities to SAT
44   * solvers using the Decorator design pattern. The class is abstract because it
45   * does not makes sense to use it "as is".
46   * 
47   * @author leberre
48   */
49  public abstract class SolverDecorator<T extends ISolver> implements ISolver {
50  
51  	/**
52  	 * 
53  	 */
54  	private static final long serialVersionUID = 1L;
55  
56  	public boolean isDBSimplificationAllowed() {
57  		return solver.isDBSimplificationAllowed();
58  	}
59  
60  	public void setDBSimplificationAllowed(boolean status) {
61  		solver.setDBSimplificationAllowed(status);
62  	}
63  
64  	/*
65  	 * (non-Javadoc)
66  	 * 
67  	 * @see org.sat4j.specs.ISolver#setTimeoutOnConflicts(int)
68  	 */
69  	public void setTimeoutOnConflicts(int count) {
70  		solver.setTimeoutOnConflicts(count);
71  	}
72  
73  	/*
74  	 * (non-Javadoc)
75  	 * 
76  	 * @see org.sat4j.specs.IProblem#printInfos(java.io.PrintWriter,
77  	 * java.lang.String)
78  	 */
79  	public void printInfos(PrintWriter out, String prefix) {
80  		solver.printInfos(out, prefix);
81  	}
82  
83  	/*
84  	 * (non-Javadoc)
85  	 * 
86  	 * @see org.sat4j.specs.IProblem#isSatisfiable(boolean)
87  	 */
88  	public boolean isSatisfiable(boolean global) throws TimeoutException {
89  		return solver.isSatisfiable(global);
90  	}
91  
92  	/*
93  	 * (non-Javadoc)
94  	 * 
95  	 * @see org.sat4j.specs.IProblem#isSatisfiable(org.sat4j.specs.IVecInt,
96  	 * boolean)
97  	 */
98  	public boolean isSatisfiable(IVecInt assumps, boolean global)
99  			throws TimeoutException {
100 		return solver.isSatisfiable(assumps, global);
101 	}
102 
103 	/*
104 	 * (non-Javadoc)
105 	 * 
106 	 * @see org.sat4j.specs.ISolver#clearLearntClauses()
107 	 */
108 	public void clearLearntClauses() {
109 		solver.clearLearntClauses();
110 	}
111 
112 	/*
113 	 * (non-Javadoc)
114 	 * 
115 	 * @see org.sat4j.specs.IProblem#findModel()
116 	 */
117 	public int[] findModel() throws TimeoutException {
118 		return solver.findModel();
119 	}
120 
121 	/*
122 	 * (non-Javadoc)
123 	 * 
124 	 * @see org.sat4j.specs.IProblem#findModel(org.sat4j.specs.IVecInt)
125 	 */
126 	public int[] findModel(IVecInt assumps) throws TimeoutException {
127 		return solver.findModel(assumps);
128 	}
129 
130 	/*
131 	 * (non-Javadoc)
132 	 * 
133 	 * @see org.sat4j.specs.IProblem#model(int)
134 	 */
135 	public boolean model(int var) {
136 		return solver.model(var);
137 	}
138 
139 	public void setExpectedNumberOfClauses(int nb) {
140 		solver.setExpectedNumberOfClauses(nb);
141 	}
142 
143 	/*
144 	 * (non-Javadoc)
145 	 * 
146 	 * @see org.sat4j.specs.ISolver#getTimeout()
147 	 */
148 	public int getTimeout() {
149 		return solver.getTimeout();
150 	}
151 
152 	/**
153 	 * @since 2.1
154 	 */
155 	public long getTimeoutMs() {
156 		return solver.getTimeoutMs();
157 	}
158 
159 	/*
160 	 * (non-Javadoc)
161 	 * 
162 	 * @see org.sat4j.specs.ISolver#toString(java.lang.String)
163 	 */
164 	public String toString(String prefix) {
165 		return solver.toString(prefix);
166 	}
167 
168 	@Override
169 	public String toString() {
170 		return solver.toString();
171 	}
172 
173 	/*
174 	 * (non-Javadoc)
175 	 * 
176 	 * @see org.sat4j.specs.ISolver#printStat(java.io.PrintStream,
177 	 * java.lang.String)
178 	 */
179 	@Deprecated
180 	public void printStat(PrintStream out, String prefix) {
181 		solver.printStat(out, prefix);
182 	}
183 
184 	public void printStat(PrintWriter out, String prefix) {
185 		solver.printStat(out, prefix);
186 	}
187 
188 	private T solver;
189 
190 	/**
191      * 
192      */
193 	public SolverDecorator(T solver) {
194 		this.solver = solver;
195 	}
196 
197 	@Deprecated
198 	public int newVar() {
199 		return solver.newVar();
200 	}
201 
202 	/*
203 	 * (non-Javadoc)
204 	 * 
205 	 * @see org.sat4j.ISolver#newVar(int)
206 	 */
207 	public int newVar(int howmany) {
208 		return solver.newVar(howmany);
209 	}
210 
211 	/*
212 	 * (non-Javadoc)
213 	 * 
214 	 * @see org.sat4j.ISolver#addClause(org.sat4j.datatype.VecInt)
215 	 */
216 	public IConstr addClause(IVecInt literals) throws ContradictionException {
217 		return solver.addClause(literals);
218 	}
219 
220 	public void addAllClauses(IVec<IVecInt> clauses)
221 			throws ContradictionException {
222 		solver.addAllClauses(clauses);
223 	}
224 
225 	/**
226 	 * @since 2.1
227 	 */
228 	public IConstr addBlockingClause(IVecInt literals)
229 			throws ContradictionException {
230 		return solver.addBlockingClause(literals);
231 	}
232 
233 	/*
234 	 * (non-Javadoc)
235 	 * 
236 	 * @see org.sat4j.ISolver#addAtMost(org.sat4j.datatype.VecInt, int)
237 	 */
238 	public IConstr addAtMost(IVecInt literals, int degree)
239 			throws ContradictionException {
240 		return solver.addAtMost(literals, degree);
241 	}
242 
243 	/*
244 	 * (non-Javadoc)
245 	 * 
246 	 * @see org.sat4j.ISolver#addAtLeast(org.sat4j.datatype.VecInt, int)
247 	 */
248 	public IConstr addAtLeast(IVecInt literals, int degree)
249 			throws ContradictionException {
250 		return solver.addAtLeast(literals, degree);
251 	}
252 
253 	/*
254 	 * (non-Javadoc)
255 	 * 
256 	 * @see org.sat4j.ISolver#model()
257 	 */
258 	public int[] model() {
259 		return solver.model();
260 	}
261 
262 	/*
263 	 * (non-Javadoc)
264 	 * 
265 	 * @see org.sat4j.ISolver#isSatisfiable()
266 	 */
267 	public boolean isSatisfiable() throws TimeoutException {
268 		return solver.isSatisfiable();
269 	}
270 
271 	/*
272 	 * (non-Javadoc)
273 	 * 
274 	 * @see org.sat4j.ISolver#isSatisfiable(org.sat4j.datatype.VecInt)
275 	 */
276 	public boolean isSatisfiable(IVecInt assumps) throws TimeoutException {
277 		return solver.isSatisfiable(assumps);
278 	}
279 
280 	/*
281 	 * (non-Javadoc)
282 	 * 
283 	 * @see org.sat4j.ISolver#setTimeout(int)
284 	 */
285 	public void setTimeout(int t) {
286 		solver.setTimeout(t);
287 	}
288 
289 	/*
290 	 * (non-Javadoc)
291 	 * 
292 	 * @see org.sat4j.ISolver#setTimeoutMs(int)
293 	 */
294 	public void setTimeoutMs(long t) {
295 		solver.setTimeoutMs(t);
296 	}
297 
298 	/*
299 	 * (non-Javadoc)
300 	 * 
301 	 * @see org.sat4j.ISolver#expireTimeout()
302 	 */
303 	public void expireTimeout() {
304 		solver.expireTimeout();
305 	}
306 
307 	/*
308 	 * (non-Javadoc)
309 	 * 
310 	 * @see org.sat4j.ISolver#nConstraints()
311 	 */
312 	public int nConstraints() {
313 		return solver.nConstraints();
314 	}
315 
316 	/*
317 	 * (non-Javadoc)
318 	 * 
319 	 * @see org.sat4j.ISolver#nVars()
320 	 */
321 	public int nVars() {
322 		return solver.nVars();
323 	}
324 
325 	/*
326 	 * (non-Javadoc)
327 	 * 
328 	 * @see org.sat4j.ISolver#reset()
329 	 */
330 	public void reset() {
331 		solver.reset();
332 	}
333 
334 	public T decorated() {
335 		return solver;
336 	}
337 
338 	/**
339 	 * Method to be called to clear the decorator from its decorated solver.
340 	 * This is especially useful to avoid memory leak in a program.
341 	 * 
342 	 * @return the decorated solver.
343 	 */
344 	public T clearDecorated() {
345 		T decorated = solver;
346 		solver = null;
347 		return decorated;
348 	}
349 
350 	/*
351 	 * (non-Javadoc)
352 	 * 
353 	 * @see org.sat4j.specs.ISolver#removeConstr(org.sat4j.minisat.core.Constr)
354 	 */
355 	public boolean removeConstr(IConstr c) {
356 		return solver.removeConstr(c);
357 	}
358 
359 	/*
360 	 * (non-Javadoc)
361 	 * 
362 	 * @see org.sat4j.specs.ISolver#getStat()
363 	 */
364 	public Map<String, Number> getStat() {
365 		return solver.getStat();
366 	}
367 
368 	/**
369 	 * @since 2.1
370 	 */
371 	public void setSearchListener(SearchListener sl) {
372 		solver.setSearchListener(sl);
373 	}
374 
375 	/**
376 	 * @since 2.1
377 	 */
378 	public int nextFreeVarId(boolean reserve) {
379 		return solver.nextFreeVarId(reserve);
380 	}
381 
382 	/**
383 	 * @since 2.1
384 	 */
385 	public boolean removeSubsumedConstr(IConstr c) {
386 		return solver.removeSubsumedConstr(c);
387 	}
388 
389 	/**
390 	 * @since 2.2
391 	 */
392 	public SearchListener getSearchListener() {
393 		return solver.getSearchListener();
394 	}
395 
396 	/**
397 	 * @since 2.2
398 	 */
399 	public boolean isVerbose() {
400 		return solver.isVerbose();
401 	}
402 
403 	/**
404 	 * @since 2.2
405 	 */
406 	public void setVerbose(boolean value) {
407 		solver.setVerbose(value);
408 	}
409 
410 	/**
411 	 * @since 2.2
412 	 */
413 	public void setLogPrefix(String prefix) {
414 		solver.setLogPrefix(prefix);
415 	}
416 
417 	/**
418 	 * @since 2.2
419 	 */
420 	public String getLogPrefix() {
421 		return solver.getLogPrefix();
422 	}
423 
424 	/**
425 	 * @since 2.2
426 	 */
427 	public IVecInt unsatExplanation() {
428 		return solver.unsatExplanation();
429 	}
430 
431 }