Skip to content

Commit

Permalink
Fix incorrect simplification of Boolean constraints that contain a fi…
Browse files Browse the repository at this point in the history
…xed Boolean variable in an annotation.
  • Loading branch information
guidotack committed Mar 29, 2023
1 parent c522052 commit 0df7c49
Show file tree
Hide file tree
Showing 3 changed files with 71 additions and 0 deletions.
2 changes: 2 additions & 0 deletions changes.rst
Original file line number Diff line number Diff line change
Expand Up @@ -71,6 +71,8 @@ Bug fixes:
- Fix index set checking for tuples and records which contain arrays.
- Fix the handling of domain and index set expressions in aliases.
- Fix incorrect coercion of sets into multidimensional arrays (:bugref:`656`).
- Fix incorrect simplification of Boolean constraints that contain a fixed Boolean
variable in an annotation.

.. _v2.7.0:

Expand Down
34 changes: 34 additions & 0 deletions lib/optimize.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -1624,6 +1624,40 @@ void simplify_bool_constraint(EnvI& env, Item* ii, VarDecl* vd, bool& remove,
Expression* e = nullptr;
auto* ci = ii->dynamicCast<ConstraintI>();
auto* vdi = ii->dynamicCast<VarDeclI>();

Call* call;
if (ci != nullptr) {
call = Expression::dynamicCast<Call>(ci->e());
} else {
call = Expression::dynamicCast<Call>(vdi->e()->e());
}

if (call != nullptr) {
// Check that the vd actually occurs in the arguments of the call,
// and not just in an annotation
bool foundVd = false;
for (unsigned int i = 0; !foundVd && i < call->argCount(); i++) {
if (call->arg(i) == vd->id()) {
foundVd = true;
break;
}
auto* a = call->arg(i)->dynamicCast<ArrayLit>();
if (a != nullptr) {
for (unsigned int j = 0; j < a->size(); j++) {
if (Expression::equal((*a)[j], vd->id())) {
foundVd = true;
break;
}
}
}
}

if (!foundVd) {
remove = false;
return;
}
}

if (ci != nullptr) {
e = ci->e();

Expand Down
35 changes: 35 additions & 0 deletions tests/spec/unit/regression/test_annotation_on_exists.mzn
Original file line number Diff line number Diff line change
@@ -0,0 +1,35 @@
/***
!Test
check_against: []
expected:
- !Result
solution:
- !Solution
b: true
c: true
d: false
- !Solution
b: true
c: false
d: true
- !Solution
b: true
c: true
d: true
status: ALL_SOLUTIONS
extra_files: []
markers: []
name: ''
options:
all_solutions: true
solvers:
- gecode
type: solve
***/

var bool: b;
annotation remove(var bool: b);
var bool: c;
var bool: d;
constraint (c \/ d )::remove(b);
constraint b;

0 comments on commit 0df7c49

Please sign in to comment.