Skip to content

Commit

Permalink
Fix unification and dependency management for bool2int calls. Fixes #70.
Browse files Browse the repository at this point in the history
  • Loading branch information
@guidotack
guidotack committed Dec 9, 2015
1 parent 23a91af commit 55542c0
Show file tree
Hide file tree
Showing 3 changed files with 58 additions and 19 deletions.
65 changes: 46 additions & 19 deletions lib/optimize.cpp
View file
Expand Up @@ -130,15 +130,25 @@ namespace MiniZinc {
return false;
}

void unify(EnvI& env, Id* id0, Id* id1) {
void unify(EnvI& env, std::vector<VarDecl*>& deletedVarDecls, Id* id0, Id* id1) {
if (id0->decl() != id1->decl()) {
if (isOutput(id0->decl())) {
std::swap(id0,id1);
}

if (id0->decl()->e() != NULL) {
id1->decl()->e(id0->decl()->e());
Expression* rhs = id0->decl()->e();

VarDeclI* vdi1 = (*env.flat())[env.vo.find(id1->decl())]->cast<VarDeclI>();
CollectOccurrencesE ce(env.vo, vdi1);
topDown(ce, rhs);

id1->decl()->e(rhs);
id0->decl()->e(NULL);

VarDeclI* vdi0 = (*env.flat())[env.vo.find(id0->decl())]->cast<VarDeclI>();
CollectDecls cd(env.vo, deletedVarDecls, vdi0);
topDown(cd, rhs);
}

// Compute intersection of domains
Expand Down Expand Up @@ -240,6 +250,9 @@ namespace MiniZinc {
q.push_back(ci);
}
} else if (VarDeclI* vdi = (*item)->dyn_cast<VarDeclI>()) {
if (vdi->e()->id()->decl() != vdi->e()) {
vdi = (*env.flat())[env.vo.find(vdi->e()->id()->decl())]->cast<VarDeclI>();
}
if (!vdi->removed() && !vdi->flag() && vdi->e()->e()) {
vdi->flag(true);
q.push_back(vdi);
Expand Down Expand Up @@ -285,7 +298,7 @@ namespace MiniZinc {
if ( (c->id() == constants().ids.int_.eq || c->id() == constants().ids.bool_eq || c->id() == constants().ids.float_.eq || c->id() == constants().ids.set_eq) &&
c->args()[0]->isa<Id>() && c->args()[1]->isa<Id>() &&
(c->args()[0]->cast<Id>()->decl()->e()==NULL || c->args()[1]->cast<Id>()->decl()->e()==NULL) ) {
unify(envi, c->args()[0]->cast<Id>(), c->args()[1]->cast<Id>());
unify(envi, deletedVarDecls, c->args()[0]->cast<Id>(), c->args()[1]->cast<Id>());
{
VarDecl* vd = c->args()[0]->cast<Id>()->decl();
int v0idx = envi.vo.find(vd);
Expand Down Expand Up @@ -330,7 +343,7 @@ namespace MiniZinc {
if (vdi->e()->e() && vdi->e()->e()->isa<Id>() && vdi->e()->type().dim()==0) {
Id* id1 = vdi->e()->e()->cast<Id>();
vdi->e()->e(NULL);
unify(envi, vdi->e()->id(), id1);
unify(envi, deletedVarDecls, vdi->e()->id(), id1);
pushDependentConstraints(envi, id1, constraintQueue);
}
if (vdi->e()->type().isbool() && vdi->e()->type().isvar() && vdi->e()->type().dim()==0
Expand Down Expand Up @@ -841,7 +854,7 @@ namespace MiniZinc {
c->id()==constants().ids.float_.eq) {
if (is_true && c->args()[0]->isa<Id>() && c->args()[1]->isa<Id>() &&
(c->args()[0]->cast<Id>()->decl()->e()==NULL || c->args()[1]->cast<Id>()->decl()->e()==NULL) ) {
unify(env, c->args()[0]->cast<Id>(), c->args()[1]->cast<Id>());
unify(env, deletedVarDecls, c->args()[0]->cast<Id>(), c->args()[1]->cast<Id>());
pushDependentConstraints(env, c->args()[0]->cast<Id>(), constraintQueue);
CollectDecls cd(env.vo,deletedVarDecls,ii);
topDown(cd,c);
Expand All @@ -856,12 +869,19 @@ namespace MiniZinc {
env.flat()->fail(env);
} else {
VarDeclI* vdi = ii->cast<VarDeclI>();
CollectDecls cd(env.vo,deletedVarDecls,ii);
topDown(cd,c);
vdi->e()->e(constants().boollit(is_equal));
vdi->e()->ti()->domain(constants().boollit(is_equal));
vdi->e()->ti()->setComputedDomain(true);
pushVarDecl(env, vdi, env.vo.find(vdi->e()), vardeclQueue);
pushDependentConstraints(env, vdi->e()->id(), constraintQueue);
}
if (ii->isa<ConstraintI>()) {
CollectDecls cd(env.vo,deletedVarDecls,ii);
topDown(cd,c);
env.flat_removeItem(ii);
}
CollectDecls cd(env.vo,deletedVarDecls,ii);
topDown(cd,c);
env.flat_removeItem(ii);
} else if (is_true &&
((c->args()[0]->isa<Id>() && c->args()[1]->type().ispar()) ||
(c->args()[1]->isa<Id>() && c->args()[0]->type().ispar())) )
Expand Down Expand Up @@ -966,14 +986,15 @@ namespace MiniZinc {
VarDeclI* vdi = ii->cast<VarDeclI>();
bool fixed = false;
bool b_val = false;
IntSetVal* vdi_dom = NULL;
if (vdi->e()->ti()->domain()) {
IntSetVal* isv = eval_intset(env, vdi->e()->ti()->domain());
if (isv->min()<0 || isv->min()>1) {
vdi_dom = eval_intset(env, vdi->e()->ti()->domain());
if (vdi_dom->max()<0 || vdi_dom->min()>1) {
env.flat()->fail(env);
return true;
}
fixed = isv->min()==isv->max();
b_val = (isv->min() == 1);
fixed = vdi_dom->min()==vdi_dom->max();
b_val = (vdi_dom->min() == 1);
}
if (fixed) {
if (c->args()[0]->type().ispar()) {
Expand All @@ -997,19 +1018,25 @@ namespace MiniZinc {
}
}
} else {
IntVal v = -1;
if (BoolLit* bl = c->args()[0]->dyn_cast<BoolLit>()) {
IntVal v = bl->v() ? 1 : 0;
CollectDecls cd(env.vo,deletedVarDecls,ii);
topDown(cd,c);
vdi->e()->e(IntLit::a(v));
pushVarDecl(env, vdi, env.vo.find(vdi->e()), vardeclQueue);
v = bl->v() ? 1 : 0;
} else if (Id* ident = c->args()[0]->dyn_cast<Id>()) {
if (ident->decl()->ti()->domain()) {
IntVal v = eval_bool(env,ident->decl()->ti()->domain()) ? 1 : 0;
v = eval_bool(env,ident->decl()->ti()->domain()) ? 1 : 0;
}
}
if (v != -1) {
if (vdi_dom && !vdi_dom->contains(v)) {
env.flat()->fail(env);
} else {
CollectDecls cd(env.vo,deletedVarDecls,ii);
topDown(cd,c);
vdi->e()->e(IntLit::a(v));
vdi->e()->ti()->domain(new SetLit(Location().introduce(),IntSetVal::a(v, v)));
vdi->e()->ti()->setComputedDomain(true);
pushVarDecl(env, vdi, env.vo.find(vdi->e()), vardeclQueue);
pushDependentConstraints(env, vdi->e()->id(), constraintQueue);
}
}
}
Expand Down Expand Up @@ -1077,7 +1104,7 @@ namespace MiniZinc {
if (vdi->e()->e() && vdi->e()->e()->isa<Id>() && vdi->e()->type().dim()==0) {
Id* id1 = vdi->e()->e()->cast<Id>();
vdi->e()->e(NULL);
unify(env, vdi->e()->id(), id1);
unify(env, deletedVarDecls, vdi->e()->id(), id1);
pushDependentConstraints(env, id1, constraintQueue);
}
pushVarDecl(env, vdi, env.vo.find(vdi->e()), vardeclQueue);
Expand Down
3 changes: 3 additions & 0 deletions tests/unit/evaluation/minizinc/regression/test_bug70.exp
View file
@@ -0,0 +1,3 @@
killed = 1;
eFailureModes = 1;
----------
9 changes: 9 additions & 0 deletions tests/unit/evaluation/minizinc/regression/test_bug70.mzn
View file
@@ -0,0 +1,9 @@
% RUNS ON mzn20_fd

var int: killed;
constraint killed = bool2int(eFailureModes = 1);

var int: eFailureModes;
constraint eFailureModes = 1;

solve satisfy;

0 comments on commit 55542c0

Please sign in to comment.