Commit 69264549 authored by Daniel Le Berre's avatar Daniel Le Berre
Browse files

Reusing the same FileWriter object for each method

parent 6b5ac387
Pipeline #17830 passed with stages
in 49 minutes and 29 seconds
......@@ -21,6 +21,7 @@ public class VERIPBSearchListener implements PBSearchListener<ISolverService> {
private String filename;
private int nConstraints;
private boolean foundContradiction;
private FileWriter fw;
public VERIPBSearchListener(String problemname) {
int positionDot;
......@@ -36,6 +37,17 @@ public class VERIPBSearchListener implements PBSearchListener<ISolverService> {
if (f.exists()) {
f.delete();
}
try {
fw = new FileWriter(this.filename, false);
} catch (IOException e) {
throw new IllegalStateException(e);
}
}
private void assumeFileWriter() {
if (fw == null) {
throw new IllegalStateException("Proof file not set");
}
}
@Override
......@@ -43,12 +55,10 @@ public class VERIPBSearchListener implements PBSearchListener<ISolverService> {
this.nConstraints = ((IProblem) solverService).nConstraints();
this.foundContradiction = false;
try {
FileWriter fw = new FileWriter(this.filename, true);
fw.write("pseudo-Boolean proof version 1.0\n");
fw.write("f " + this.nConstraints + "\n");
fw.close();
} catch (IOException e) {
e.printStackTrace();
throw new IllegalStateException(e);
}
}
......@@ -95,26 +105,22 @@ public class VERIPBSearchListener implements PBSearchListener<ISolverService> {
this.foundContradiction = true;
}
try {
FileWriter fw = new FileWriter(this.filename, true);
fw.write("p " + this.conflict.toString() + "\n");
if (c != null) {
fw.write("e " + this.nConstraints + " " + conversion(c)
+ " ;\n");
}
fw.close();
} catch (IOException e) {
e.printStackTrace();
throw new IllegalStateException(e);
}
}
@Override
public void delete(IConstr c) {
try {
FileWriter fw = new FileWriter(this.filename, true);
fw.write("d " + c.getId() + "\n");
fw.close();
} catch (IOException e) {
e.printStackTrace();
throw new IllegalStateException(e);
}
}
......@@ -142,7 +148,6 @@ public class VERIPBSearchListener implements PBSearchListener<ISolverService> {
public void end(Lbool result) {
if (result.toString().equals("F")) {
try {
FileWriter fw = new FileWriter(this.filename, true);
if (!this.foundContradiction) {
fw.write("u >= 1 ;\n");
this.nConstraints++;
......@@ -150,7 +155,7 @@ public class VERIPBSearchListener implements PBSearchListener<ISolverService> {
fw.write("c " + this.nConstraints + "\n");
fw.close();
} catch (IOException e) {
e.printStackTrace();
throw new IllegalStateException(e);
}
}
}
......@@ -170,11 +175,9 @@ public class VERIPBSearchListener implements PBSearchListener<ISolverService> {
@Override
public void learnUnit(int p) {
try {
FileWriter fw = new FileWriter(this.filename, true);
fw.write("p " + this.conflict.toString() + "\n");
fw.close();
} catch (IOException e) {
e.printStackTrace();
throw new IllegalStateException(e);
}
this.nConstraints++;
}
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment