Skip to content

Commit 9197b4e

Browse files
IZakirzyanovIZakirzyanov
committed
added args4j lib. minor refactoring
1 parent 97d0f7d commit 9197b4e

File tree

6 files changed

+232
-105
lines changed

6 files changed

+232
-105
lines changed

‎.gitignore

+1
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,6 @@
11
ans.dot
22
table0
3+
logging.properties
34
/tests
45
/bin
56
.*

‎lib/args4j.jar

85.2 KB
Binary file not shown.

‎src/ru/ifmo/rain/zakirzyanov/DFAInductor/Buffer.java

+1-2
Original file line numberDiff line numberDiff line change
@@ -1,14 +1,13 @@
11
package ru.ifmo.rain.zakirzyanov.DFAInductor;
22

3-
import java.io.IOException;
43
import java.io.PrintWriter;
54

65
public class Buffer {
76
private StringBuilder sb;
87
private PrintWriter pw;
98
private int countClauses;
109

11-
public Buffer(PrintWriter pw) throws IOException {
10+
public Buffer(PrintWriter pw) {
1211
this.pw = pw;
1312
this.sb = new StringBuilder();
1413
this.countClauses = 0;

‎src/ru/ifmo/rain/zakirzyanov/DFAInductor/DimacsFileGenerator.java

+45-46
Original file line numberDiff line numberDiff line change
@@ -14,16 +14,28 @@
1414

1515
public class DimacsFileGenerator {
1616

17-
final static int WITHOUT_SB = 0;
18-
final static int BFS_SB = 1;
19-
final static int CLIQUE_SB = 2;
17+
enum SBStrategy {
18+
WITHOUT_SB, BFS_SB, CLIQUE_SB;
19+
}
20+
21+
// Exception??
22+
23+
public SBStrategy getSBStrategyByNum(int num) {
24+
switch (num) {
25+
case 0:
26+
return SBStrategy.WITHOUT_SB;
27+
case 2:
28+
return SBStrategy.CLIQUE_SB;
29+
default:
30+
return SBStrategy.BFS_SB;
31+
}
32+
}
2033

2134
private APTA apta;
2235
private ConsistencyGraph cg;
2336
private int colors;
2437
private int maxVar;
2538
private int vertices;
26-
private PrintWriter pwDF;
2739
private Set<String> alphabet;
2840
private int[][] x;
2941
private Map<String, Integer>[][] y;
@@ -36,37 +48,23 @@ public class DimacsFileGenerator {
3648
private String tmpFile = "tmp";
3749
private String dimacsFile;
3850
private int countClauses = 0;
39-
private int SB;
51+
private SBStrategy SB;
4052
private int noisyP;
4153
private int noisySize;
4254
private Set<Integer> acceptableClique;
4355
private Set<Integer> rejectableClique;
4456
private int color = 0;
4557
private Set<Integer> ends;
58+
4659

47-
public DimacsFileGenerator(APTA apta, ConsistencyGraph cg, int colors,
48-
int SB) throws IOException {
49-
init(apta, cg, colors, SB, 0, "dimacsFile.cnf");
50-
}
51-
52-
public DimacsFileGenerator(APTA apta, ConsistencyGraph cg, int colors,
53-
int SB, int noisyP) throws IOException {
54-
init(apta, cg, colors, SB, noisyP, "dimacsFile.cnf");
55-
}
56-
57-
public DimacsFileGenerator(APTA apta, ConsistencyGraph cg, int colors,
60+
public DimacsFileGenerator(APTA apta, ConsistencyGraph cg, int noisyP, int colors,
5861
int SB, String dimacsFile) throws IOException {
59-
init(apta, cg, colors, SB, 0, dimacsFile);
60-
}
61-
62-
public DimacsFileGenerator(APTA apta, ConsistencyGraph cg, int colors,
63-
int SB, int noisyP, String dimacsFile) throws IOException {
64-
init(apta, cg, colors, SB, noisyP, dimacsFile);
62+
init(apta, cg, colors, getSBStrategyByNum(SB), noisyP, dimacsFile);
6563
}
6664

6765
@SuppressWarnings("unchecked")
68-
private void init(APTA apta, ConsistencyGraph cg, int colors, int SB,
69-
int noisyP, String dimacsFile) throws IOException {
66+
private void init(APTA apta, ConsistencyGraph cg, int colors,
67+
SBStrategy SB, int noisyP, String dimacsFile) throws IOException {
7068
this.apta = apta;
7169
this.cg = cg;
7270
this.colors = colors;
@@ -75,10 +73,9 @@ private void init(APTA apta, ConsistencyGraph cg, int colors, int SB,
7573
this.maxVar = 1;
7674
this.vertices = apta.getSize();
7775
this.dimacsFile = dimacsFile;
78-
this.pwDF = new PrintWriter(dimacsFile);
7976
this.alphabet = apta.getAlphabet();
8077
this.ends = new HashSet<>();
81-
78+
8279
this.x = new int[vertices][colors];
8380
this.y = new HashMap[colors][colors];
8481
this.z = new int[colors];
@@ -100,7 +97,7 @@ private void init(APTA apta, ConsistencyGraph cg, int colors, int SB,
10097
}
10198
}
10299

103-
if (SB == BFS_SB) {
100+
if (SB == SBStrategy.BFS_SB) {
104101
this.e = new int[colors][colors];
105102
this.p = new int[colors][colors];
106103
for (int i = 0; i < colors; i++) {
@@ -127,7 +124,7 @@ private void init(APTA apta, ConsistencyGraph cg, int colors, int SB,
127124
}
128125
}
129126

130-
if (SB == CLIQUE_SB) {
127+
if (SB == SBStrategy.CLIQUE_SB) {
131128
int maxDegree = 0;
132129
int maxV = -1;
133130
acceptableClique = new HashSet<>();
@@ -178,7 +175,7 @@ private void init(APTA apta, ConsistencyGraph cg, int colors, int SB,
178175
if (noisyP > 0) {
179176
ends.addAll(apta.getAcceptableNodes());
180177
ends.addAll(apta.getRejectableNodes());
181-
178+
182179
noisySize = ends.size() * this.noisyP / 100;
183180
n = new int[noisySize][vertices];
184181
f = new int[vertices];
@@ -197,9 +194,12 @@ private void init(APTA apta, ConsistencyGraph cg, int colors, int SB,
197194

198195
public String generateFile() throws IOException {
199196

197+
200198
File tmp = new File(tmpFile);
201199
PrintWriter tmpPW = new PrintWriter(tmp);
202200
Buffer buffer = new Buffer(tmpPW);
201+
202+
PrintWriter pwDF = new PrintWriter(dimacsFile);
203203

204204
printOneAtLeast(buffer);
205205
printOneAtMost(buffer);
@@ -208,13 +208,13 @@ public String generateFile() throws IOException {
208208
printParrentRelationAtLeastOneColor(buffer);
209209
printParrentRelationForces(buffer);
210210

211-
if (SB == BFS_SB) {
211+
if (SB == SBStrategy.BFS_SB) {
212212
// root has 0 color
213213
buffer.addClause(x[0][0]);
214214
printSBPEdgeExist(buffer);
215215
printSBPMinimalSymbol(buffer);
216216
printSBPParent(buffer);
217-
// printSBPChildrenOrder(buffer);
217+
// printSBPChildrenOrder(buffer);
218218
if (apta.getAlphaSize() == 2) {
219219
printSBPOrderByChildrenSymbolForSizeTwo(buffer);
220220
} else {
@@ -223,7 +223,7 @@ public String generateFile() throws IOException {
223223
printSBPOrderInLayer(buffer);
224224
printSBPParentExist(buffer);
225225
}
226-
if (SB == CLIQUE_SB) {
226+
if (SB == SBStrategy.CLIQUE_SB) {
227227
printAcceptableCliqueSB(buffer);
228228
printRejectableCliqueSB(buffer);
229229
}
@@ -234,7 +234,7 @@ public String generateFile() throws IOException {
234234
printNoisyOrdered(buffer);
235235
printFProxy(buffer);
236236
printAccVertDiffColorRejNoisy(buffer);
237-
237+
238238
} else {
239239
printAccVertDiffColorRej(buffer);
240240
printConflictsFromCG(buffer);
@@ -480,17 +480,17 @@ private void printSBPParent(Buffer buffer) {
480480
buffer.flush();
481481
}
482482

483-
// p_{i,j} and !p_{i+1,j} => !p_{i+q, j}
484-
private void printSBPChildrenOrder(Buffer buffer) {
485-
for (int i = 1; i < colors; i++) {
486-
for (int j = 0; j < i; j++) {
487-
for (int k = i + 2; k < colors; k++) {
488-
buffer.addClause(-p[i][j], p[i + 1][j], -p[k][j]);
489-
}
490-
}
491-
}
492-
buffer.flush();
493-
}
483+
// // p_{i,j} and !p_{i+1,j} => !p_{i+q, j}
484+
// private void printSBPChildrenOrder(Buffer buffer) {
485+
// for (int i = 1; i < colors; i++) {
486+
// for (int j = 0; j < i; j++) {
487+
// for (int k = i + 2; k < colors; k++) {
488+
// buffer.addClause(-p[i][j], p[i + 1][j], -p[k][j]);
489+
// }
490+
// }
491+
// }
492+
// buffer.flush();
493+
// }
494494

495495
// if alphabet size greater then 2
496496
// p_{i,j} and p_{i+1,j} and m_{j,i,c_k} => !m_{j,i+1,c_(k-q)}
@@ -513,7 +513,7 @@ private void printSBPOrderByChildrenSymbol(Buffer buffer) {
513513
}
514514

515515
// if alphabet size equal to 2
516-
// p_{i,j} and p_{i+1,j} => y_{j, i, 0} and y_{j, i + 1, 1}
516+
// p_{i,j} and p_{i+1,j} => y_{j, i, 0} and y_{j, i + 1, 1}
517517
private void printSBPOrderByChildrenSymbolForSizeTwo(Buffer buffer) {
518518
for (int i = 1; i < colors - 1; i++) {
519519
for (int j = 0; j < i; j++) {
@@ -524,7 +524,6 @@ private void printSBPOrderByChildrenSymbolForSizeTwo(Buffer buffer) {
524524
buffer.flush();
525525
}
526526

527-
528527
// p_{i,j} => !p_{i+1,j-q}
529528
private void printSBPOrderInLayer(Buffer buffer) {
530529
for (int i = 1; i < colors - 1; i++) {

0 commit comments

Comments
 (0)