Commit adcf3806 authored by leberre's avatar leberre
Browse files

added support for pmin models

git-svn-id: svn+ssh://svn.forge.ow2.org/svnroot/sat4j/maven/trunk@2532 ba638df5-4473-46d1-82f8-c3ae2a17a6e1
parent 33982ba9
......@@ -52,17 +52,18 @@ final class DecisionMode implements ILauncherMode {
private PrintWriter out;
private long beginTime;
public void displayResult(ISolver solver, IProblem problem,
ILogAble logger, PrintWriter out, Reader reader, long beginTime,
public void displayResult(ISolver solver, IProblem problem, ILogAble logger,
PrintWriter out, Reader reader, long beginTime,
boolean displaySolutionLine) {
if (solver != null) {
out.flush();
double wallclocktime = (System.currentTimeMillis() - beginTime) / 1000.0;
double wallclocktime = (System.currentTimeMillis() - beginTime)
/ 1000.0;
solver.printStat(out);
out.println(ANSWER_PREFIX + exitCode);
if (exitCode != ExitCode.UNKNOWN
&& exitCode != ExitCode.UNSATISFIABLE) {
int[] model = solver.model();
int[] model = problem.model();
if (System.getProperty("prime") != null) {
int initiallength = model.length;
logger.log("returning a prime implicant ...");
......
......@@ -42,6 +42,7 @@ import org.sat4j.specs.ContradictionException;
import org.sat4j.specs.IProblem;
import org.sat4j.specs.ISolver;
import org.sat4j.specs.IVecInt;
import org.sat4j.tools.Minimal4InclusionModel;
/**
* Dimacs Reader written by Frederic Laihem. It is much faster than DimacsReader
......@@ -61,7 +62,7 @@ public class LecteurDimacs extends Reader implements Serializable {
/* taille du buffer */
private static final int TAILLE_BUF = 16384;
private final ISolver s;
private ISolver s;
private transient BufferedInputStream in;
......@@ -72,6 +73,8 @@ public class LecteurDimacs extends Reader implements Serializable {
private static final char EOF = (char) -1;
private final boolean pminimal = false;
/*
* nomFichier repr?sente le nom du fichier ? lire
*/
......@@ -257,8 +260,15 @@ public class LecteurDimacs extends Reader implements Serializable {
stb.append(car);
} while (car != '\n' && car != EOF);
String str = stb.toString().trim();
if (isUsingMapping()) {
if (str.startsWith("pmin")) {
String[] tokens = str.split(" ");
IVecInt p = new VecInt(tokens.length - 2);
for (int i = 1; i < tokens.length - 1; i++) {
p.push(Integer.parseInt(tokens[i]));
}
s = new Minimal4InclusionModel(s, p);
System.out.println("c computing p-minimal model for p=" + p);
} else if (isUsingMapping()) {
String[] values = str.split("=");
if (values.length == 2) {
if (mapping == null) {
......
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