Commit 4701c779 authored by Anne Parrain's avatar Anne Parrain

corrected a wrong call to createConflict

parent 846d229e
Pipeline #858 passed with stages
in 26 minutes and 48 seconds
......@@ -33,8 +33,11 @@ import org.sat4j.minisat.core.IOrder;
import org.sat4j.minisat.core.LearningStrategy;
import org.sat4j.minisat.core.RestartStrategy;
import org.sat4j.minisat.core.SearchParams;
import org.sat4j.pb.constraints.pb.AutoDivisionStrategy;
import org.sat4j.pb.constraints.pb.ConflictMapReduceToClause;
import org.sat4j.pb.constraints.pb.IConflict;
import org.sat4j.pb.constraints.pb.IWeakeningStrategy;
import org.sat4j.pb.constraints.pb.NoPostProcess;
import org.sat4j.pb.constraints.pb.PBConstr;
public class PBSolverCPLong extends PBSolverCP {
......@@ -81,7 +84,9 @@ public class PBSolverCPLong extends PBSolverCP {
@Override
protected IConflict chooseConflict(PBConstr myconfl, int level) {
return ConflictMapReduceToClause.createConflict(myconfl, level,
isNoRemove(), isSkipAllow(), stats);
isNoRemove(), isSkipAllow(), NoPostProcess.instance(),
IWeakeningStrategy.UNASSIGNED_FIRST,
AutoDivisionStrategy.ENABLED, stats);
}
@Override
......
......@@ -33,8 +33,11 @@ import org.sat4j.minisat.core.IOrder;
import org.sat4j.minisat.core.LearningStrategy;
import org.sat4j.minisat.core.RestartStrategy;
import org.sat4j.minisat.core.SearchParams;
import org.sat4j.pb.constraints.pb.AutoDivisionStrategy;
import org.sat4j.pb.constraints.pb.ConflictMapReduceToCard;
import org.sat4j.pb.constraints.pb.IConflict;
import org.sat4j.pb.constraints.pb.IWeakeningStrategy;
import org.sat4j.pb.constraints.pb.NoPostProcess;
import org.sat4j.pb.constraints.pb.PBConstr;
@SuppressWarnings("serial")
......@@ -89,7 +92,9 @@ public class PBSolverCPLongReduceToCard extends PBSolverCPLong {
@Override
protected IConflict chooseConflict(PBConstr myconfl, int level) {
return ConflictMapReduceToCard.createConflict(myconfl, level,
isNoRemove(), isSkipAllow(), stats);
isNoRemove(), isSkipAllow(), NoPostProcess.instance(),
IWeakeningStrategy.UNASSIGNED_FIRST,
AutoDivisionStrategy.ENABLED, stats);
}
@Override
......
......@@ -33,8 +33,11 @@ import org.sat4j.minisat.core.IOrder;
import org.sat4j.minisat.core.LearningStrategy;
import org.sat4j.minisat.core.RestartStrategy;
import org.sat4j.minisat.core.SearchParams;
import org.sat4j.pb.constraints.pb.AutoDivisionStrategy;
import org.sat4j.pb.constraints.pb.ConflictMapRounding;
import org.sat4j.pb.constraints.pb.IConflict;
import org.sat4j.pb.constraints.pb.IWeakeningStrategy;
import org.sat4j.pb.constraints.pb.NoPostProcess;
import org.sat4j.pb.constraints.pb.PBConstr;
public class PBSolverCPLongRounding extends PBSolverCPLong {
......@@ -87,7 +90,9 @@ public class PBSolverCPLongRounding extends PBSolverCPLong {
@Override
protected IConflict chooseConflict(PBConstr myconfl, int level) {
return ConflictMapRounding.createConflict(myconfl, level, isNoRemove(),
isSkipAllow(), stats);
isSkipAllow(), NoPostProcess.instance(),
IWeakeningStrategy.UNASSIGNED_FIRST,
AutoDivisionStrategy.ENABLED, stats);
}
@Override
......
......@@ -4,8 +4,11 @@ import org.sat4j.minisat.core.IOrder;
import org.sat4j.minisat.core.LearningStrategy;
import org.sat4j.minisat.core.RestartStrategy;
import org.sat4j.minisat.core.SearchParams;
import org.sat4j.pb.constraints.pb.AutoDivisionStrategy;
import org.sat4j.pb.constraints.pb.ConflictMapReduceByGCD;
import org.sat4j.pb.constraints.pb.IConflict;
import org.sat4j.pb.constraints.pb.IWeakeningStrategy;
import org.sat4j.pb.constraints.pb.NoPostProcess;
import org.sat4j.pb.constraints.pb.PBConstr;
public class PBSolverCPReduceByGCD extends PBSolverCP {
......@@ -64,7 +67,9 @@ public class PBSolverCPReduceByGCD extends PBSolverCP {
@Override
protected IConflict chooseConflict(PBConstr myconfl, int level) {
return ConflictMapReduceByGCD.createConflict(myconfl, level,
isNoRemove(), isSkipAllow(), stats);
isNoRemove(), isSkipAllow(), NoPostProcess.instance(),
IWeakeningStrategy.UNASSIGNED_FIRST,
AutoDivisionStrategy.ENABLED, stats);
}
@Override
......
......@@ -4,8 +4,11 @@ import org.sat4j.minisat.core.IOrder;
import org.sat4j.minisat.core.LearningStrategy;
import org.sat4j.minisat.core.RestartStrategy;
import org.sat4j.minisat.core.SearchParams;
import org.sat4j.pb.constraints.pb.AutoDivisionStrategy;
import org.sat4j.pb.constraints.pb.ConflictMapReduceByPowersOf2;
import org.sat4j.pb.constraints.pb.IConflict;
import org.sat4j.pb.constraints.pb.IWeakeningStrategy;
import org.sat4j.pb.constraints.pb.NoPostProcess;
import org.sat4j.pb.constraints.pb.PBConstr;
public class PBSolverCPReduceByPowersOf2 extends PBSolverCP {
......@@ -64,7 +67,9 @@ public class PBSolverCPReduceByPowersOf2 extends PBSolverCP {
@Override
protected IConflict chooseConflict(PBConstr myconfl, int level) {
return ConflictMapReduceByPowersOf2.createConflict(myconfl, level,
isNoRemove(), isSkipAllow(), stats);
isNoRemove(), isSkipAllow(), NoPostProcess.instance(),
IWeakeningStrategy.UNASSIGNED_FIRST,
AutoDivisionStrategy.ENABLED, stats);
}
@Override
......
......@@ -31,8 +31,11 @@ package org.sat4j.pb.core;
import org.sat4j.minisat.core.IOrder;
import org.sat4j.minisat.core.LearningStrategy;
import org.sat4j.pb.constraints.pb.AutoDivisionStrategy;
import org.sat4j.pb.constraints.pb.ConflictMapSwitchToClause;
import org.sat4j.pb.constraints.pb.IConflict;
import org.sat4j.pb.constraints.pb.IWeakeningStrategy;
import org.sat4j.pb.constraints.pb.NoPostProcess;
import org.sat4j.pb.constraints.pb.PBConstr;
public class PBSolverCautious extends PBSolverCP {
......@@ -54,14 +57,15 @@ public class PBSolverCautious extends PBSolverCP {
@Override
protected IConflict chooseConflict(PBConstr myconfl, int level) {
return ConflictMapSwitchToClause.createConflict(myconfl, level);
return ConflictMapSwitchToClause.createConflict(myconfl, level,
isNoRemove(), isSkipAllow(), NoPostProcess.instance(),
IWeakeningStrategy.UNASSIGNED_FIRST,
AutoDivisionStrategy.ENABLED, null);
}
@Override
public String toString(String prefix) {
return super.toString(prefix)
+ "\n"
+ prefix
return super.toString(prefix) + "\n" + prefix
+ "When dealing with too large coefficients, simplify asserted PB constraints to clauses";
}
......
......@@ -31,8 +31,11 @@ package org.sat4j.pb.core;
import org.sat4j.minisat.core.IOrder;
import org.sat4j.minisat.core.LearningStrategy;
import org.sat4j.pb.constraints.pb.AutoDivisionStrategy;
import org.sat4j.pb.constraints.pb.ConflictMapClause;
import org.sat4j.pb.constraints.pb.IConflict;
import org.sat4j.pb.constraints.pb.IWeakeningStrategy;
import org.sat4j.pb.constraints.pb.NoPostProcess;
import org.sat4j.pb.constraints.pb.PBConstr;
public class PBSolverClause extends PBSolverCP {
......@@ -50,7 +53,9 @@ public class PBSolverClause extends PBSolverCP {
@Override
protected IConflict chooseConflict(PBConstr myconfl, int level) {
return ConflictMapClause.createConflict(myconfl, level, isNoRemove(),
isSkipAllow(), stats);
isSkipAllow(), NoPostProcess.instance(),
IWeakeningStrategy.UNASSIGNED_FIRST,
AutoDivisionStrategy.ENABLED, stats);
}
@Override
......
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