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 public void clearLearntClauses() {
56 solver.clearLearntClauses();
57 }
58
59 /*
60 * (non-Javadoc)
61 *
62 * @see org.sat4j.specs.IProblem#findModel()
63 */
64 public int[] findModel() throws TimeoutException {
65 return solver.findModel();
66 }
67
68 /*
69 * (non-Javadoc)
70 *
71 * @see org.sat4j.specs.IProblem#findModel(org.sat4j.specs.IVecInt)
72 */
73 public int[] findModel(IVecInt assumps) throws TimeoutException {
74 return solver.findModel(assumps);
75 }
76
77 /*
78 * (non-Javadoc)
79 *
80 * @see org.sat4j.specs.IProblem#model(int)
81 */
82 public boolean model(int var) {
83 return solver.model(var);
84 }
85
86 public void setExpectedNumberOfClauses(int nb) {
87 solver.setExpectedNumberOfClauses(nb);
88 }
89
90 /*
91 * (non-Javadoc)
92 *
93 * @see org.sat4j.specs.ISolver#getTimeout()
94 */
95 public int getTimeout() {
96 return solver.getTimeout();
97 }
98
99 /*
100 * (non-Javadoc)
101 *
102 * @see org.sat4j.specs.ISolver#toString(java.lang.String)
103 */
104 public String toString(String prefix) {
105 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 @Deprecated
115 public void printStat(PrintStream out, String prefix) {
116 solver.printStat(out, prefix);
117 }
118
119 public void printStat(PrintWriter out, String prefix) {
120 solver.printStat(out, prefix);
121 }
122
123 private final ISolver solver;
124
125 /**
126 *
127 */
128 public SolverDecorator(ISolver solver) {
129 this.solver = solver;
130 }
131
132 /*
133 * (non-Javadoc)
134 *
135 * @see org.sat4j.ISolver#newVar()
136 */
137 public int newVar() {
138 return solver.newVar();
139 }
140
141 /*
142 * (non-Javadoc)
143 *
144 * @see org.sat4j.ISolver#newVar(int)
145 */
146 public int newVar(int howmany) {
147 return solver.newVar(howmany);
148 }
149
150 /*
151 * (non-Javadoc)
152 *
153 * @see org.sat4j.ISolver#addClause(org.sat4j.datatype.VecInt)
154 */
155 public IConstr addClause(IVecInt literals) throws ContradictionException {
156 return solver.addClause(literals);
157 }
158
159 public void addAllClauses(IVec<IVecInt> clauses)
160 throws ContradictionException {
161 solver.addAllClauses(clauses);
162 }
163
164 /*
165 * (non-Javadoc)
166 *
167 * @see org.sat4j.ISolver#addAtMost(org.sat4j.datatype.VecInt, int)
168 */
169 public IConstr addAtMost(IVecInt literals, int degree)
170 throws ContradictionException {
171 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 public IConstr addAtLeast(IVecInt literals, int degree)
180 throws ContradictionException {
181 return solver.addAtLeast(literals, degree);
182 }
183
184 public IConstr addPseudoBoolean(IVecInt literals, IVec<BigInteger> coeffs,
185 boolean moreThan, BigInteger degree) throws ContradictionException {
186 return solver.addPseudoBoolean(literals, coeffs, moreThan, degree);
187 }
188
189 /*
190 * (non-Javadoc)
191 *
192 * @see org.sat4j.ISolver#model()
193 */
194 public int[] model() {
195 return solver.model();
196 }
197
198 /*
199 * (non-Javadoc)
200 *
201 * @see org.sat4j.ISolver#isSatisfiable()
202 */
203 public boolean isSatisfiable() throws TimeoutException {
204 return solver.isSatisfiable();
205 }
206
207 /*
208 * (non-Javadoc)
209 *
210 * @see org.sat4j.ISolver#isSatisfiable(org.sat4j.datatype.VecInt)
211 */
212 public boolean isSatisfiable(IVecInt assumps) throws TimeoutException {
213 return solver.isSatisfiable(assumps);
214 }
215
216 /*
217 * (non-Javadoc)
218 *
219 * @see org.sat4j.ISolver#setTimeout(int)
220 */
221 public void setTimeout(int t) {
222 solver.setTimeout(t);
223 }
224
225 /*
226 * (non-Javadoc)
227 *
228 * @see org.sat4j.ISolver#setTimeoutMs(int)
229 */
230 public void setTimeoutMs(long t) {
231 solver.setTimeoutMs(t);
232 }
233
234 /*
235 * (non-Javadoc)
236 *
237 * @see org.sat4j.ISolver#nConstraints()
238 */
239 public int nConstraints() {
240 return solver.nConstraints();
241 }
242
243 /*
244 * (non-Javadoc)
245 *
246 * @see org.sat4j.ISolver#nVars()
247 */
248 public int nVars() {
249 return solver.nVars();
250 }
251
252 /*
253 * (non-Javadoc)
254 *
255 * @see org.sat4j.ISolver#reset()
256 */
257 public void reset() {
258 solver.reset();
259 }
260
261 public ISolver decorated() {
262 return solver;
263 }
264
265 /*
266 * (non-Javadoc)
267 *
268 * @see org.sat4j.specs.ISolver#removeConstr(org.sat4j.minisat.core.Constr)
269 */
270 public boolean removeConstr(IConstr c) {
271 return solver.removeConstr(c);
272 }
273
274 /*
275 * (non-Javadoc)
276 *
277 * @see org.sat4j.specs.ISolver#getStat()
278 */
279 public Map<String, Number> getStat() {
280 return solver.getStat();
281 }
282 }