Commit 6cb70377 authored by Daniel Le Berre's avatar Daniel Le Berre

Small fixed for KTH launcher

parent dc158277
Pipeline #276 passed with stages
in 25 minutes and 35 seconds
......@@ -1230,8 +1230,10 @@ public class Solver<D extends DataStructureFactory>
assert nAssigns() <= this.voc.realnVars();
if (nAssigns() == this.voc.realnVars()) {
modelFound();
this.slistener.solutionFound((this.fullmodel != null)
? this.fullmodel : this.model, this);
this.slistener.solutionFound(
(this.fullmodel != null) ? this.fullmodel
: this.model,
this);
if (this.sharedConflict == null) {
cancelUntil(this.rootLevel);
return Lbool.TRUE;
......@@ -1276,10 +1278,10 @@ public class Solver<D extends DataStructureFactory>
}
if (allsat) {
modelFound();
this.slistener.solutionFound(
(this.fullmodel != null)
? this.fullmodel : this.model,
this);
this.slistener
.solutionFound((this.fullmodel != null)
? this.fullmodel
: this.model, this);
return Lbool.TRUE;
} else {
confl = preventTheSameDecisionsToBeMade();
......@@ -1866,6 +1868,9 @@ public class Solver<D extends DataStructureFactory>
* @since 2.1
*/
public void printLearntClausesInfos(PrintWriter out, String prefix) {
if (this.learnts.isEmpty()) {
return;
}
Map<String, Counter> learntTypes = new HashMap<String, Counter>();
for (Iterator<Constr> it = this.learnts.iterator(); it.hasNext();) {
String type = it.next().getClass().getName();
......
......@@ -225,7 +225,8 @@ public class VarOrderHeap implements IOrder, Serializable {
@Override
public String toString() {
return "VSIDS like heuristics from MiniSAT using a heap " + this.phaseStrategy; //$NON-NLS-1$
return "VSIDS like heuristics from MiniSAT using a heap " //$NON-NLS-1$
+ this.phaseStrategy;
}
public ILits getVocabulary() {
......@@ -233,7 +234,7 @@ public class VarOrderHeap implements IOrder, Serializable {
}
public void printStat(PrintWriter out, String prefix) {
out.println(prefix + "non guided choices\t" + this.nullchoice); //$NON-NLS-1$
out.println(prefix + "non guided choices\t: " + this.nullchoice); //$NON-NLS-1$
}
public void assignLiteral(int p) {
......
......@@ -4,6 +4,7 @@ import java.io.BufferedReader;
import java.io.IOException;
import java.io.InputStreamReader;
import java.net.URL;
import java.util.Map;
import org.apache.commons.cli.CommandLine;
import org.apache.commons.cli.CommandLineParser;
......@@ -12,7 +13,6 @@ import org.apache.commons.cli.Option;
import org.apache.commons.cli.Options;
import org.apache.commons.cli.ParseException;
import org.apache.commons.cli.PosixParser;
import org.sat4j.pb.IPBSolver;
import org.sat4j.pb.OptToPBSATAdapter;
import org.sat4j.pb.PBSolverHandle;
import org.sat4j.pb.PseudoOptDecorator;
......@@ -96,9 +96,9 @@ public class KTHLauncher {
}
CommandLineParser parser = new PosixParser();
Options options = createCLIOptions();
if (args.length==0) {
if (args.length == 0) {
HelpFormatter formatter = new HelpFormatter();
formatter.printHelp( "KTHLauncher", options );
formatter.printHelp("KTHLauncher", options);
return;
}
try {
......@@ -127,7 +127,7 @@ public class KTHLauncher {
if (line.hasOption("when-resolve")) {
String value = line.getOptionValue("when-resolve");
switch (value) {
case "always":
case "always":
solver.setSkipAllow(false);
break;
case "skip":
......@@ -168,20 +168,26 @@ public class KTHLauncher {
return;
}
System.out.println(solver.toString("c "));
String [] leftArgs = line.getArgs();
if (leftArgs.length==0) {
String[] leftArgs = line.getArgs();
if (leftArgs.length == 0) {
System.err.println("Missing filename");
return;
}
String filename = leftArgs[leftArgs.length-1];
PBSolverHandle handle = new PBSolverHandle(new PseudoOptDecorator(solver));
String filename = leftArgs[leftArgs.length - 1];
PBSolverHandle handle = new PBSolverHandle(
new PseudoOptDecorator(solver));
OPBReader2012 reader = new OPBReader2012(handle);
IPBSolver optimizer = new OptToPBSATAdapter(handle);
OptToPBSATAdapter optimizer = new OptToPBSATAdapter(handle);
try {
reader.parseInstance(filename);
if (optimizer.isSatisfiable()) {
System.out.println("s OPTIMUM FOUND");
System.out.println("v "+reader.decode(optimizer.model())+" 0");
if (optimizer.isOptimal()) {
System.out.println("s OPTIMUM FOUND");
} else {
System.out.println("s SATISFIABLE");
}
System.out.println(
"v " + reader.decode(optimizer.model()) + " 0");
} else {
System.out.println("s UNSATISFIABLE");
}
......
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