Commit eaabcf6a authored by Daniel Le Berre's avatar Daniel Le Berre

Corrected issue when varid was not used in the formula

parent ac924fe8
Pipeline #346 passed with stages
in 26 minutes and 14 seconds
......@@ -60,8 +60,12 @@ public class NaturalStaticOrder implements IOrder {
@Override
public int select() {
while (!voc.isUnassigned(LiteralsUtils.posLit(index))) {
while (!voc.isUnassigned(LiteralsUtils.posLit(index))
|| !voc.belongsToPool(index)) {
index++;
if (index > voc.nVars()) {
return ILits.UNDEFINED;
}
}
return phaseSelectionStrategy.select(index);
}
......
......@@ -47,6 +47,7 @@ import org.sat4j.tools.DotSearchTracing;
*/
public class KTHLauncher {
public static Options createCLIOptions() {
Options options = new Options();
options.addOption("cl", "coeflim", true,
......@@ -305,7 +306,17 @@ public class KTHLauncher {
PBSolverHandle handle = new PBSolverHandle(
new PseudoOptDecorator(pbsolver));
OPBReader2012 reader = new OPBReader2012(handle);
OptToPBSATAdapter optimizer = new OptToPBSATAdapter(handle);
final OptToPBSATAdapter optimizer = new OptToPBSATAdapter(handle);
final Thread shutdownHook = new Thread() {
@Override
public void run() {
// stop the solver before displaying solutions
optimizer.expireTimeout();
optimizer.printStat(System.out, "c ");
}
};
Runtime.getRuntime().addShutdownHook(shutdownHook);
try {
reader.parseInstance(filename);
if (line.hasOption("dot-output")) {
......@@ -328,7 +339,6 @@ public class KTHLauncher {
} else {
System.out.println("s UNSATISFIABLE");
}
optimizer.printStat(System.out, "c ");
} catch (TimeoutException e) {
System.out.println("s UNKNOWN");
} catch (ParseFormatException e) {
......
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