1 |
|
|
2 |
|
|
3 |
|
|
4 |
|
|
5 |
|
|
6 |
|
|
7 |
|
|
8 |
|
|
9 |
|
|
10 |
|
|
11 |
|
|
12 |
|
|
13 |
|
|
14 |
|
|
15 |
|
|
16 |
|
|
17 |
|
|
18 |
|
|
19 |
|
|
20 |
|
|
21 |
|
|
22 |
|
|
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 |
|
|
43 |
|
|
44 |
|
|
45 |
|
|
46 |
|
@author |
47 |
|
|
|
|
| 32,1% |
Uncovered Elements: 38 (56) |
Complexity: 1 |
Complexity Density: 1 |
|
48 |
|
public abstract class SolverDecorator implements ISolver, Serializable { |
49 |
|
|
50 |
|
|
51 |
|
|
52 |
|
|
53 |
|
@see |
54 |
|
|
|
|
| 0% |
Uncovered Elements: 1 (1) |
Complexity: 1 |
Complexity Density: 1 |
|
55 |
0
|
public void clearLearntClauses() {... |
56 |
0
|
solver.clearLearntClauses(); |
57 |
|
} |
58 |
|
|
59 |
|
|
60 |
|
|
61 |
|
|
62 |
|
@see |
63 |
|
|
|
|
| 0% |
Uncovered Elements: 1 (1) |
Complexity: 1 |
Complexity Density: 1 |
|
64 |
0
|
public int[] findModel() throws TimeoutException {... |
65 |
0
|
return solver.findModel(); |
66 |
|
} |
67 |
|
|
68 |
|
|
69 |
|
|
70 |
|
|
71 |
|
@see |
72 |
|
|
|
|
| 0% |
Uncovered Elements: 1 (1) |
Complexity: 1 |
Complexity Density: 1 |
|
73 |
0
|
public int[] findModel(IVecInt assumps) throws TimeoutException {... |
74 |
0
|
return solver.findModel(assumps); |
75 |
|
} |
76 |
|
|
77 |
|
|
78 |
|
|
79 |
|
|
80 |
|
@see |
81 |
|
|
|
|
| 0% |
Uncovered Elements: 1 (1) |
Complexity: 1 |
Complexity Density: 1 |
|
82 |
0
|
public boolean model(int var) {... |
83 |
0
|
return solver.model(var); |
84 |
|
} |
85 |
|
|
|
|
| 0% |
Uncovered Elements: 1 (1) |
Complexity: 1 |
Complexity Density: 1 |
|
86 |
0
|
public void setExpectedNumberOfClauses(int nb) {... |
87 |
0
|
solver.setExpectedNumberOfClauses(nb); |
88 |
|
} |
89 |
|
|
90 |
|
|
91 |
|
|
92 |
|
|
93 |
|
@see |
94 |
|
|
|
|
| 0% |
Uncovered Elements: 1 (1) |
Complexity: 1 |
Complexity Density: 1 |
|
95 |
0
|
public int getTimeout() {... |
96 |
0
|
return solver.getTimeout(); |
97 |
|
} |
98 |
|
|
99 |
|
|
100 |
|
|
101 |
|
|
102 |
|
@see |
103 |
|
|
|
|
| 0% |
Uncovered Elements: 1 (1) |
Complexity: 1 |
Complexity Density: 1 |
|
104 |
0
|
public String toString(String prefix) {... |
105 |
0
|
return solver.toString(prefix); |
106 |
|
} |
107 |
|
|
108 |
|
|
109 |
|
|
110 |
|
|
111 |
|
@see |
112 |
|
|
113 |
|
|
|
|
| 0% |
Uncovered Elements: 1 (1) |
Complexity: 1 |
Complexity Density: 1 |
|
114 |
0
|
@Deprecated... |
115 |
|
public void printStat(PrintStream out, String prefix) { |
116 |
0
|
solver.printStat(out, prefix); |
117 |
|
} |
118 |
|
|
|
|
| 0% |
Uncovered Elements: 1 (1) |
Complexity: 1 |
Complexity Density: 1 |
|
119 |
0
|
public void printStat(PrintWriter out, String prefix) {... |
120 |
0
|
solver.printStat(out, prefix); |
121 |
|
} |
122 |
|
|
123 |
|
private final ISolver solver; |
124 |
|
|
125 |
|
|
126 |
|
|
127 |
|
|
|
|
| 100% |
Uncovered Elements: 0 (1) |
Complexity: 1 |
Complexity Density: 1 |
|
128 |
5
|
public SolverDecorator(ISolver solver) {... |
129 |
5
|
this.solver = solver; |
130 |
|
} |
131 |
|
|
132 |
|
|
133 |
|
|
134 |
|
|
135 |
|
@see |
136 |
|
|
|
|
| 0% |
Uncovered Elements: 1 (1) |
Complexity: 1 |
Complexity Density: 1 |
|
137 |
0
|
public int newVar() {... |
138 |
0
|
return solver.newVar(); |
139 |
|
} |
140 |
|
|
141 |
|
|
142 |
|
|
143 |
|
|
144 |
|
@see |
145 |
|
|
|
|
| 100% |
Uncovered Elements: 0 (1) |
Complexity: 1 |
Complexity Density: 1 |
|
146 |
5
|
public int newVar(int howmany) {... |
147 |
5
|
return solver.newVar(howmany); |
148 |
|
} |
149 |
|
|
150 |
|
|
151 |
|
|
152 |
|
|
153 |
|
@see |
154 |
|
|
|
|
| 100% |
Uncovered Elements: 0 (1) |
Complexity: 1 |
Complexity Density: 1 |
|
155 |
38
|
public IConstr addClause(IVecInt literals) throws ContradictionException {... |
156 |
38
|
return solver.addClause(literals); |
157 |
|
} |
158 |
|
|
|
|
| 0% |
Uncovered Elements: 1 (1) |
Complexity: 1 |
Complexity Density: 1 |
|
159 |
0
|
public void addAllClauses(IVec<IVecInt> clauses)... |
160 |
|
throws ContradictionException { |
161 |
0
|
solver.addAllClauses(clauses); |
162 |
|
} |
163 |
|
|
164 |
|
|
165 |
|
|
166 |
|
|
167 |
|
@see |
168 |
|
|
|
|
| 100% |
Uncovered Elements: 0 (1) |
Complexity: 1 |
Complexity Density: 1 |
|
169 |
13
|
public IConstr addAtMost(IVecInt literals, int degree)... |
170 |
|
throws ContradictionException { |
171 |
13
|
return solver.addAtMost(literals, degree); |
172 |
|
} |
173 |
|
|
174 |
|
|
175 |
|
|
176 |
|
|
177 |
|
@see |
178 |
|
|
|
|
| 0% |
Uncovered Elements: 1 (1) |
Complexity: 1 |
Complexity Density: 1 |
|
179 |
0
|
public IConstr addAtLeast(IVecInt literals, int degree)... |
180 |
|
throws ContradictionException { |
181 |
0
|
return solver.addAtLeast(literals, degree); |
182 |
|
} |
183 |
|
|
|
|
| 0% |
Uncovered Elements: 1 (1) |
Complexity: 1 |
Complexity Density: 1 |
|
184 |
0
|
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 |
|
|
191 |
|
|
192 |
|
@see |
193 |
|
|
|
|
| 100% |
Uncovered Elements: 0 (1) |
Complexity: 1 |
Complexity Density: 1 |
|
194 |
40
|
public int[] model() {... |
195 |
40
|
return solver.model(); |
196 |
|
} |
197 |
|
|
198 |
|
|
199 |
|
|
200 |
|
|
201 |
|
@see |
202 |
|
|
|
|
| 100% |
Uncovered Elements: 0 (1) |
Complexity: 1 |
Complexity Density: 1 |
|
203 |
35
|
public boolean isSatisfiable() throws TimeoutException {... |
204 |
35
|
return solver.isSatisfiable(); |
205 |
|
} |
206 |
|
|
207 |
|
|
208 |
|
|
209 |
|
|
210 |
|
@see |
211 |
|
|
|
|
| 100% |
Uncovered Elements: 0 (1) |
Complexity: 1 |
Complexity Density: 1 |
|
212 |
12
|
public boolean isSatisfiable(IVecInt assumps) throws TimeoutException {... |
213 |
12
|
return solver.isSatisfiable(assumps); |
214 |
|
} |
215 |
|
|
216 |
|
|
217 |
|
|
218 |
|
|
219 |
|
@see |
220 |
|
|
|
|
| 0% |
Uncovered Elements: 1 (1) |
Complexity: 1 |
Complexity Density: 1 |
|
221 |
0
|
public void setTimeout(int t) {... |
222 |
0
|
solver.setTimeout(t); |
223 |
|
} |
224 |
|
|
225 |
|
|
226 |
|
|
227 |
|
|
228 |
|
@see |
229 |
|
|
|
|
| 0% |
Uncovered Elements: 1 (1) |
Complexity: 1 |
Complexity Density: 1 |
|
230 |
0
|
public void setTimeoutMs(long t) {... |
231 |
0
|
solver.setTimeoutMs(t); |
232 |
|
} |
233 |
|
|
234 |
|
|
235 |
|
|
236 |
|
|
237 |
|
@see |
238 |
|
|
|
|
| 0% |
Uncovered Elements: 1 (1) |
Complexity: 1 |
Complexity Density: 1 |
|
239 |
0
|
public int nConstraints() {... |
240 |
0
|
return solver.nConstraints(); |
241 |
|
} |
242 |
|
|
243 |
|
|
244 |
|
|
245 |
|
|
246 |
|
@see |
247 |
|
|
|
|
| 100% |
Uncovered Elements: 0 (1) |
Complexity: 1 |
Complexity Density: 1 |
|
248 |
52
|
public int nVars() {... |
249 |
52
|
return solver.nVars(); |
250 |
|
} |
251 |
|
|
252 |
|
|
253 |
|
|
254 |
|
|
255 |
|
@see |
256 |
|
|
|
|
| 0% |
Uncovered Elements: 1 (1) |
Complexity: 1 |
Complexity Density: 1 |
|
257 |
0
|
public void reset() {... |
258 |
0
|
solver.reset(); |
259 |
|
} |
260 |
|
|
|
|
| 0% |
Uncovered Elements: 1 (1) |
Complexity: 1 |
Complexity Density: 1 |
|
261 |
0
|
public ISolver decorated() {... |
262 |
0
|
return solver; |
263 |
|
} |
264 |
|
|
265 |
|
|
266 |
|
|
267 |
|
|
268 |
|
@see |
269 |
|
|
|
|
| 100% |
Uncovered Elements: 0 (1) |
Complexity: 1 |
Complexity Density: 1 |
|
270 |
4
|
public boolean removeConstr(IConstr c) {... |
271 |
4
|
return solver.removeConstr(c); |
272 |
|
} |
273 |
|
|
274 |
|
|
275 |
|
|
276 |
|
|
277 |
|
@see |
278 |
|
|
|
|
| 0% |
Uncovered Elements: 1 (1) |
Complexity: 1 |
Complexity Density: 1 |
|
279 |
0
|
public Map<String, Number> getStat() {... |
280 |
0
|
return solver.getStat(); |
281 |
|
} |
282 |
|
} |