Skip to content

Commit

Permalink
Simplify fixed arrays by pushing them on the queue, rather than using…
Browse files Browse the repository at this point in the history
… simplify_bool_constraint. Handle boolean variables with fixed domain correctly in fixed literal counting. Fixes #671.
  • Loading branch information
guidotack committed Apr 18, 2023
1 parent 8f1e8e5 commit c41171d
Show file tree
Hide file tree
Showing 3 changed files with 33 additions and 12 deletions.
3 changes: 3 additions & 0 deletions changes.rst
Expand Up @@ -39,6 +39,9 @@ Bug fixes:
- Fix crash when flattening variable declaration annotations for tuple
variables with paths enabled (:bugref:`675`).
- Fix incorrect ordering of enum parts when using separate assignment items.
- Simplify fixed arrays by pushing them on the queue, rather than using
simplify_bool_constraint. Handle boolean variables with fixed domain
correctly in fixed literal counting (:bugref:`671`).

.. _v2.7.2:

Expand Down
17 changes: 5 additions & 12 deletions lib/optimize.cpp
Expand Up @@ -783,17 +783,9 @@ void optimize(Env& env, bool chain_compression) {
}
if (auto* vdi = item->dynamicCast<VarDeclI>()) {
// The variable occurs in the RHS of another variable, so
// if that is an array variable, simplify all constraints that
// mention the array variable
if ((vdi->e()->e() != nullptr) && vdi->e()->e()->isa<ArrayLit>()) {
auto ait = envi.varOccurrences.itemMap.find(vdi->e()->id()->decl()->id());
if (ait.first) {
for (auto* aitem : *ait.second) {
simplify_bool_constraint(envi, aitem, vd, remove, vardeclQueue,
constraintQueue, toRemove, deletedVarDecls,
nonFixedLiteralCount);
}
}
// if that is an array variable, push it onto the stack for processing
if (vdi->e()->e() != nullptr && vdi->e()->e()->isa<ArrayLit>()) {
push_vardecl(envi, envi.varOccurrences.idx.get(vdi->e()->id()), vardeclQueue);
continue;
}
}
Expand Down Expand Up @@ -1600,7 +1592,8 @@ int decrement_non_fixed_vars(std::unordered_map<Expression*, int>& nonFixedLiter
auto* al = follow_id(c->arg(i))->cast<ArrayLit>();
nonFixedVars += static_cast<int>(al->size());
for (unsigned int j = al->size(); (j--) != 0U;) {
if ((*al)[j]->type().isPar()) {
if ((*al)[j]->type().isPar() ||
((*al)[j]->isa<Id>() && (*al)[j]->cast<Id>()->decl()->ti()->domain() != nullptr)) {
nonFixedVars--;
}
}
Expand Down
25 changes: 25 additions & 0 deletions tests/spec/unit/regression/github_671.mzn
@@ -0,0 +1,25 @@
/***
!Test
check_against: []
expected:
- !Result
solution: !Solution
arr:
- true
status: SATISFIED
extra_files: []
markers: []
name: ''
options:
all_solutions: false
solvers:
- gecode
type: solve
***/

array[1..1] of var bool: arr ::output = let {
array[1..1] of var bool: res;
constraint res[1];
} in res;

solve satisfy;

0 comments on commit c41171d

Please sign in to comment.