cprudhom on master
Conditional detection of redund… (compare)
cprudhom on master
Update set_version.sh Set setCloneVariableArrayInProp… Remove warnings from Propagatio… and 1 more (compare)
// Collect all values
IntIterableRangeSet set = new IntIterableRangeSet();
for (int i = 0; i < sequence.length; i++) {
set.addAll(sequence[i]);
if (i < subsequence.length) {
set.addAll(subsequence[i]);
}
}
IntVar[] allValues = ArrayUtils.concat(sequence, Arrays.stream(set.toArray()).mapToObj(k -> ref().intVar(k)).toArray(IntVar[]::new));
IntVar[] pos = ref().intVarArray(subsequence.length, 0, allValues.length);
BoolVar[] lt = ref().boolVarArray(pos.length);
for (int i = 0; i < subsequence.length; i++) {
ref().element(subsequence[i], allValues, pos[i], 0).post();
if (i > 0) {
ref().reifyXgeY(pos[i - 1], pos[i], lt[i]);
} else {
ref().reifyXgtC(pos[0], sequence.length - 1, lt[i]);
}
}
ref().addClausesBoolOrArrayEqualTrue(lt);
// Collect all from sequence
IntIterableRangeSet values = Arrays.stream(sequence)
.map(IntIterableRangeSet::new)
.collect(IntIterableRangeSet::new,
IntIterableRangeSet::addAll,
IntIterableRangeSet::addAll);
IntVar[] copySsq = Arrays.stream(subsequence).map(v -> ref().intVar("C_" + v.getName(), values.toArray())).toArray(IntVar[]::new);
IntVar[] pos = ref().intVarArray("P", subsequence.length, 0, copySsq.length);
BoolVar[] nq = ref().boolVarArray("nq", subsequence.length);
BoolVar[] np = ref().boolVarArray("np", subsequence.length-1);
for (int i = 0; i < subsequence.length; i++) {
ref().element(copySsq[i], sequence, pos[i], 0).post();
ref().reifyXneY(subsequence[i], copySsq[i], nq[i]);
if(i < subsequence.length - 1){
ref().reifyXgtY(pos[i], pos[i+1], np[i]);
}
}
ref().addClausesBoolOrArrayEqualTrue(ArrayUtils.concat(np, nq));
Model model = new Model("Two");
BoolVar g1 = model.boolVar("g1");
BoolVar g2 = model.boolVar("g2");
model.addClausesBoolOrArrayEqualTrue(new BoolVar[] {g1,g2});
model.or(new BoolVar[] {g1,g2}).post();
What is the difference between addClausesBoolOrArrayEqualTrue and Or? I tested them and they give the same result. Could it be that addClausesBoolOrArrayEqualTrue is using SAT solver?
Hello! We have found a situation where there is a "java.lang.ArrayIndexOutOfBoundsException" while performing a "model.unpost(constraint)" where the constraint has been reified and introduced in another constraint.
Example:
Constraint A = model.arithm(...);
Constraint B = model.arithm(...);
Constraint C = model.arithm(A.reify(), "<=", B.refiy());
model.post(C);
model.solve();
model.unpost(C);
model.unpost(A);
model.unpost(B);
We have created a Git Issue: chocoteam/choco-solver#823
As a workaround we have unpost the propagator constraint
Arrays.stream(A.getPropagators()).filter(Objects::nonNull).map(Propagator::getConstraint).forEach(model::unpost);
Arrays.stream(B.getPropagators()).filter(Objects::nonNull).map(Propagator::getConstraint).forEach(model::unpost);
We think that the "ArrayIndexOutOfBoundsException" is a bug, and maybe there is another way of unposting this constraints or we are missing something.
Thank you!