Commit aba92b7b authored by leberre's avatar leberre
Browse files

Added messages to explain what the solver is doing.

git-svn-id: svn+ssh://svn.forge.ow2.org/svnroot/sat4j/maven/trunk@1679 ba638df5-4473-46d1-82f8-c3ae2a17a6e1
parent 015d7a34
......@@ -53,8 +53,6 @@ public class AllMUSes {
private final List<IVecInt> secondPhaseClauses;
private final List<IVecInt> musList;
private final boolean group;
public AllMUSes(boolean group) {
if (!group) {
this.css = new FullClauseSelectorSolver<ISolver>(
......@@ -66,7 +64,6 @@ public class AllMUSes {
mssList = new ArrayList<IVecInt>();
musList = new ArrayList<IVecInt>();
secondPhaseClauses = new ArrayList<IVecInt>();
this.group = group;
}
public AllMUSes() {
......@@ -98,6 +95,9 @@ public class AllMUSes {
if (secondPhaseClauses.isEmpty()) {
computeAllMSS();
}
if (css.isVerbose()) {
System.out.println(css.getLogPrefix() + "Computing all MUSes ...");
}
css.internalState();
ISolver solver = SolverFactory.newDefault();
......@@ -136,6 +136,9 @@ public class AllMUSes {
} catch (TimeoutException e) {
e.printStackTrace();
}
if (css.isVerbose()) {
System.out.println(css.getLogPrefix() + "... done.");
}
css.externalState();
return musList;
}
......@@ -147,7 +150,9 @@ public class AllMUSes {
public List<IVecInt> computeAllMSS(SolutionFoundListener listener) {
css.internalState();
int nVar = css.nVars();
if (css.isVerbose()) {
System.out.println(css.getLogPrefix() + "Computing all MSSes ...");
}
IVecInt pLits = new VecInt();
for (Integer i : css.getAddedVars()) {
pLits.push(i);
......@@ -201,6 +206,9 @@ public class AllMUSes {
e.printStackTrace();
} catch (ContradictionException e) {
}
if (css.isVerbose()) {
System.out.println(css.getLogPrefix() + "... done.");
}
css.externalState();
return mssList;
......
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