From 55542c07f2c6ab3bb5618663faac5970b6908682 Mon Sep 17 00:00:00 2001 From: Guido Tack Date: Wed, 9 Dec 2015 16:44:49 +1100 Subject: [PATCH] Fix unification and dependency management for bool2int calls. Fixes #70. --- lib/optimize.cpp | 65 +++++++++++++------ .../minizinc/regression/test_bug70.exp | 3 + .../minizinc/regression/test_bug70.mzn | 9 +++ 3 files changed, 58 insertions(+), 19 deletions(-) create mode 100644 tests/unit/evaluation/minizinc/regression/test_bug70.exp create mode 100644 tests/unit/evaluation/minizinc/regression/test_bug70.mzn diff --git a/lib/optimize.cpp b/lib/optimize.cpp index dd05749b6..72ef091fc 100644 --- a/lib/optimize.cpp +++ b/lib/optimize.cpp @@ -130,15 +130,25 @@ namespace MiniZinc { return false; } - void unify(EnvI& env, Id* id0, Id* id1) { + void unify(EnvI& env, std::vector& 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(); + 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(); + CollectDecls cd(env.vo, deletedVarDecls, vdi0); + topDown(cd, rhs); } // Compute intersection of domains @@ -240,6 +250,9 @@ namespace MiniZinc { q.push_back(ci); } } else if (VarDeclI* vdi = (*item)->dyn_cast()) { + if (vdi->e()->id()->decl() != vdi->e()) { + vdi = (*env.flat())[env.vo.find(vdi->e()->id()->decl())]->cast(); + } if (!vdi->removed() && !vdi->flag() && vdi->e()->e()) { vdi->flag(true); q.push_back(vdi); @@ -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() && c->args()[1]->isa() && (c->args()[0]->cast()->decl()->e()==NULL || c->args()[1]->cast()->decl()->e()==NULL) ) { - unify(envi, c->args()[0]->cast(), c->args()[1]->cast()); + unify(envi, deletedVarDecls, c->args()[0]->cast(), c->args()[1]->cast()); { VarDecl* vd = c->args()[0]->cast()->decl(); int v0idx = envi.vo.find(vd); @@ -330,7 +343,7 @@ namespace MiniZinc { if (vdi->e()->e() && vdi->e()->e()->isa() && vdi->e()->type().dim()==0) { Id* id1 = vdi->e()->e()->cast(); 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 @@ -841,7 +854,7 @@ namespace MiniZinc { c->id()==constants().ids.float_.eq) { if (is_true && c->args()[0]->isa() && c->args()[1]->isa() && (c->args()[0]->cast()->decl()->e()==NULL || c->args()[1]->cast()->decl()->e()==NULL) ) { - unify(env, c->args()[0]->cast(), c->args()[1]->cast()); + unify(env, deletedVarDecls, c->args()[0]->cast(), c->args()[1]->cast()); pushDependentConstraints(env, c->args()[0]->cast(), constraintQueue); CollectDecls cd(env.vo,deletedVarDecls,ii); topDown(cd,c); @@ -856,12 +869,19 @@ namespace MiniZinc { env.flat()->fail(env); } else { VarDeclI* vdi = ii->cast(); + 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()) { + 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() && c->args()[1]->type().ispar()) || (c->args()[1]->isa() && c->args()[0]->type().ispar())) ) @@ -966,14 +986,15 @@ namespace MiniZinc { VarDeclI* vdi = ii->cast(); 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()) { @@ -997,19 +1018,25 @@ namespace MiniZinc { } } } else { + IntVal v = -1; if (BoolLit* bl = c->args()[0]->dyn_cast()) { - 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()) { 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); } } } @@ -1077,7 +1104,7 @@ namespace MiniZinc { if (vdi->e()->e() && vdi->e()->e()->isa() && vdi->e()->type().dim()==0) { Id* id1 = vdi->e()->e()->cast(); 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); diff --git a/tests/unit/evaluation/minizinc/regression/test_bug70.exp b/tests/unit/evaluation/minizinc/regression/test_bug70.exp new file mode 100644 index 000000000..4860d85bf --- /dev/null +++ b/tests/unit/evaluation/minizinc/regression/test_bug70.exp @@ -0,0 +1,3 @@ +killed = 1; +eFailureModes = 1; +---------- diff --git a/tests/unit/evaluation/minizinc/regression/test_bug70.mzn b/tests/unit/evaluation/minizinc/regression/test_bug70.mzn new file mode 100644 index 000000000..0274da7db --- /dev/null +++ b/tests/unit/evaluation/minizinc/regression/test_bug70.mzn @@ -0,0 +1,9 @@ +% RUNS ON mzn20_fd + +var int: killed; +constraint killed = bool2int(eFailureModes = 1); + +var int: eFailureModes; +constraint eFailureModes = 1; + +solve satisfy; \ No newline at end of file