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

diamond operator

parent 7bf61213
Pipeline #20022 failed with stages
in 17 minutes and 50 seconds
......@@ -159,14 +159,10 @@ public final class DecisionMode implements ILauncherMode {
try {
if (problem.isSatisfiable()) {
if (this.exitCode == ExitCode.UNKNOWN) {
this.exitCode = ExitCode.SATISFIABLE;
}
} else {
if (this.exitCode == ExitCode.UNKNOWN) {
this.exitCode = ExitCode.UNSATISFIABLE;
}
}
} catch (TimeoutException e) {
logger.log("timeout");
}
......
......@@ -74,10 +74,11 @@ public class LightFactory extends ASolverFactory<ISolver> {
@Override
public ISolver defaultSolver() {
MiniSATLearning<DataStructureFactory> learning = new MiniSATLearning<DataStructureFactory>();
Solver<DataStructureFactory> solver = new Solver<DataStructureFactory>(
learning, new MixedDataStructureDanielWL(), new VarOrderHeap(
new RSATPhaseSelectionStrategy()), new ArminRestarts());
MiniSATLearning<DataStructureFactory> learning = new MiniSATLearning<>();
Solver<DataStructureFactory> solver = new Solver<>(learning,
new MixedDataStructureDanielWL(),
new VarOrderHeap(new RSATPhaseSelectionStrategy()),
new ArminRestarts());
learning.setSolver(solver);
solver.setSimplifier(solver.EXPENSIVE_SIMPLIFICATION);
solver.setSearchParams(new SearchParams(1.1, 100));
......
......@@ -89,12 +89,12 @@ public class MUSLauncher extends AbstractLauncher {
}
ISolver solver;
if (this.highLevel) {
HighLevelXplain<ISolver> hlxp = new HighLevelXplain<ISolver>(
HighLevelXplain<ISolver> hlxp = new HighLevelXplain<>(
SolverFactory.newDefault());
this.xplain = hlxp;
solver = hlxp;
} else {
Xplain<ISolver> xp = new Xplain<ISolver>(SolverFactory.newDefault(),
Xplain<ISolver> xp = new Xplain<>(SolverFactory.newDefault(),
false);
this.xplain = xp;
solver = xp;
......
Supports Markdown
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