Commit 3c92dfc8 authored by Daniel Le Berre's avatar Daniel Le Berre

Display reason treatment and postprocess on solver's info header.

parent 24844f7a
Pipeline #280 passed with stages
in 22 minutes and 59 seconds
...@@ -118,6 +118,11 @@ public class ConflictMap extends MapPb implements IConflict { ...@@ -118,6 +118,11 @@ public class ConflictMap extends MapPb implements IConflict {
return ConflictMap.createConflict(cpb, level, noRemove, skip, return ConflictMap.createConflict(cpb, level, noRemove, skip,
postprocess, stats); postprocess, stats);
} }
@Override
public String toString() {
return "Default Sat4j cutting planes";
}
}; };
} }
......
...@@ -39,6 +39,11 @@ public class ConflictMapReduceByGCD extends ConflictMap { ...@@ -39,6 +39,11 @@ public class ConflictMapReduceByGCD extends ConflictMap {
return ConflictMapReduceByGCD.createConflict(cpb, level, return ConflictMapReduceByGCD.createConflict(cpb, level,
noRemove, skip, postprocess, stats); noRemove, skip, postprocess, stats);
} }
@Override
public String toString() {
return "Divide by gcd the constraint during conflict analysis if gcd>1";
}
}; };
} }
......
...@@ -26,6 +26,11 @@ public class ConflictMapReduceByPowersOf2 extends ConflictMap { ...@@ -26,6 +26,11 @@ public class ConflictMapReduceByPowersOf2 extends ConflictMap {
return ConflictMapReduceByPowersOf2.createConflict(cpb, level, return ConflictMapReduceByPowersOf2.createConflict(cpb, level,
noRemove, skip, postprocess, stats); noRemove, skip, postprocess, stats);
} }
@Override
public String toString() {
return "Divide by two the constraint during conflict analysis if all coefficients are even";
}
}; };
} }
......
...@@ -56,6 +56,11 @@ public class ConflictMapReduceToCard extends ConflictMap { ...@@ -56,6 +56,11 @@ public class ConflictMapReduceToCard extends ConflictMap {
return ConflictMapReduceToCard.createConflict(cpb, level, return ConflictMapReduceToCard.createConflict(cpb, level,
noRemove, skip, postprocess, stats); noRemove, skip, postprocess, stats);
} }
@Override
public String toString() {
return "Reduce to cardinality constraint during conflict analysis if necessary";
}
}; };
} }
......
...@@ -74,6 +74,11 @@ public final class ConflictMapReduceToClause extends ConflictMap { ...@@ -74,6 +74,11 @@ public final class ConflictMapReduceToClause extends ConflictMap {
return ConflictMapReduceToClause.createConflict(cpb, level, return ConflictMapReduceToClause.createConflict(cpb, level,
noRemove, skip, postprocess, stats); noRemove, skip, postprocess, stats);
} }
@Override
public String toString() {
return "Reduce to clause during conflict analysis if necessary";
}
}; };
} }
......
...@@ -45,4 +45,9 @@ public class NoPostProcess implements IPostProcess { ...@@ -45,4 +45,9 @@ public class NoPostProcess implements IPostProcess {
public void postProcess(int dl, ConflictMap conflictMap) { public void postProcess(int dl, ConflictMap conflictMap) {
// nothing to do // nothing to do
} }
@Override
public String toString() {
return "No postprocessing";
}
} }
\ No newline at end of file
...@@ -51,4 +51,9 @@ public class PostProcessDivideBy2 implements IPostProcess { ...@@ -51,4 +51,9 @@ public class PostProcessDivideBy2 implements IPostProcess {
} }
@Override
public String toString() {
return "Performs a post-processing after conflict analysis in order to divide by 2 as much as possible coefficients of learned constraints";
}
} }
\ No newline at end of file
...@@ -20,4 +20,8 @@ public class PostProcessDivideByGCD implements IPostProcess { ...@@ -20,4 +20,8 @@ public class PostProcessDivideByGCD implements IPostProcess {
} }
@Override
public String toString() {
return "Performs a post-processing after conflict analysis in order to divide by gcd over coefficients of learned constraints";
}
} }
...@@ -191,4 +191,8 @@ public class PostProcessToCard implements IPostProcess { ...@@ -191,4 +191,8 @@ public class PostProcessToCard implements IPostProcess {
return maxLit; return maxLit;
} }
@Override
public String toString() {
return "Performs a post-processing after conflict analysis in order to learn only cardinality constraints (Dixon's procedure)";
}
} }
\ No newline at end of file
...@@ -133,4 +133,8 @@ public class PostProcessToClause implements IPostProcess { ...@@ -133,4 +133,8 @@ public class PostProcessToClause implements IPostProcess {
return conflictMap.assertiveLiteral; return conflictMap.assertiveLiteral;
} }
@Override
public String toString() {
return "Performs a post-processing after conflict analysis in order to learn clauses";
}
} }
\ No newline at end of file
...@@ -206,13 +206,14 @@ public class PBSolverCP extends PBSolver { ...@@ -206,13 +206,14 @@ public class PBSolverCP extends PBSolver {
@Override @Override
public String toString(String prefix) { public String toString(String prefix) {
return prefix + "Cutting planes based inference (" return prefix + "Cutting planes based inference ("
+ this.getClass().getName() + ")" + this.getClass().getName() + ")\n"
+ (this.noRemove ? "" + (this.noRemove ? ""
: " - removing satisfied literals at a higher level before CP -") : prefix + " - removing satisfied literals at a higher level before CP \n")
+ (this.skipAllow + (this.skipAllow ? prefix
? " - skipping as much as possible cutting planes during analysis conflict- Jan Elffers's algorithm -" + " - skipping as much as possible cutting planes during analysis conflict- Jan Elffers's algorithm \n"
: "") : "")
+ "\n" + super.toString(prefix); + prefix + postprocess + "\n" + prefix + conflictFactory + "\n"
+ super.toString(prefix);
} }
private final IVec<String> conflictVariables = new Vec<String>(); private final IVec<String> conflictVariables = new Vec<String>();
......
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