Skip to content

Commit

Permalink
Fix domain constraint for array of structs parameters
Browse files Browse the repository at this point in the history 
Fixes #732 on GitHub
  • Loading branch information
@Dekker1
Dekker1 committed Sep 28, 2023
1 parent 0aaf9ab commit 23e35f9
Show file tree
Hide file tree
Showing 7 changed files with 157 additions and 170 deletions.
3 changes: 3 additions & 0 deletions changes.rst
View file
Original file line number Diff line number Diff line change
Expand Up @@ -67,6 +67,9 @@ Bug fixes:
- Fix a problem in the parser where a nullptr would be used before a syntax
error was thrown (:bugref:`730`).
- Fix error management when reading preference files (:bugref:`729`).
- Fix segmentation fault caused by the creation of invalid domain constraints
generated for functions with arrays of tuples or records paramgeters
(:bugref:`732`).

.. _v2.7.6:

Expand Down
3 changes: 3 additions & 0 deletions include/minizinc/flat_exp.hh
View file
Original file line number Diff line number Diff line change
Expand Up @@ -32,6 +32,9 @@ KeepAlive flat_cv_exp(EnvI& env, Ctx ctx, Expression* e);

void make_defined_var(EnvI& env, VarDecl* vd, Call* c);
void check_index_sets(EnvI& env, VarDecl* vd, Expression* e, bool isArg = false);
/// Create a domain constraint that enforces that `expr` falls within `dom`
///
/// This function might return nullptr if no constraint is required
Expression* mk_domain_constraint(EnvI& env, Expression* expr, Expression* dom);

class CallArgItem {
Expand Down
2 changes: 2 additions & 0 deletions include/minizinc/flatten_internal.hh
View file
Original file line number Diff line number Diff line change
Expand Up @@ -595,6 +595,8 @@ EE flat_exp(EnvI& env, const Ctx& ctx, Expression* e, VarDecl* r, VarDecl* b);
EE flatten_id(EnvI& env, const Ctx& ctx, Expression* e, VarDecl* r, VarDecl* b,
bool doNotFollowChains);

ArrayLit* field_slice(EnvI& env, StructType* st, ArrayLit* al,
std::vector<std::pair<int, int>> dims, long long int field);
std::vector<Expression*> field_slices(EnvI& env, Expression* arrExpr);

class CmpExpIdx {
Expand Down
161 changes: 102 additions & 59 deletions lib/flatten.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -2514,67 +2514,103 @@ void check_index_sets(EnvI& env, VarDecl* vd, Expression* e, bool isArg) {

Expression* mk_domain_constraint(EnvI& env, Expression* expr, Expression* dom) {
assert(GC::locked());
Type t = Expression::type(expr).isPar() ? Type::parbool() : Type::varbool();

if (Expression::type(expr).structBT()) {
StructType* st = env.getStructType(Expression::type(expr));
auto* dom_al = Expression::cast<ArrayLit>(dom);
std::vector<Expression*> field_expr;
if (Expression::type(expr).dim() > 0) {
field_expr = field_slices(env, expr);
} else {
field_expr.resize(st->size());
for (int i = 0; i < st->size(); ++i) {
field_expr[i] = new FieldAccess(Location().introduce(), expr, IntLit::a(i + 1));
Expression::type(field_expr[i], (*st)[i]);
}
}
std::vector<Expression*> fieldwise;
for (int i = 0; i < st->size(); ++i) {
auto* field_ti = Expression::cast<TypeInst>((*dom_al)[i]);
if (field_ti->domain() != nullptr) {
if (Expression::type(expr).dim() > 0 && (*st)[i].dim() > 0) {
auto* bad_al = Expression::cast<ArrayLit>(field_expr[i]);
for (unsigned int i = 0; i < bad_al->size(); i++) {
fieldwise.push_back(mk_domain_constraint(env, (*bad_al)[i], field_ti->domain()));
Expression::type(fieldwise.back(), t);
}
} else {
fieldwise.push_back(mk_domain_constraint(env, field_expr[i], field_ti->domain()));
Expression::type(fieldwise.back(), t);
Type ty = Expression::type(expr);
Type retType = ty.isPar() ? Type::parbool() : Type::varbool();

std::vector<Expression*> domargs(2, nullptr);
domargs[0] = expr;

switch (ty.bt()) {
case Type::BT_INT: {
IntSetVal* isv = eval_intset(env, dom);
if (ty.st() != Type::ST_SET && ty.dim() == 0) {
IntBounds ib = compute_int_bounds(env, expr);
if (ib.valid && !isv->empty() && isv->isSubset(IntSetVal::Range(ib.l, ib.u))) {
return nullptr;
}
}
domargs[1] = new SetLit(Expression::loc(dom), isv);
break;
}
if (fieldwise.size() <= 1) {
return fieldwise.empty() ? env.constants.literalTrue : fieldwise[0];
case Type::BT_FLOAT: {
FloatSetVal* fsv = eval_floatset(env, dom);
if (ty.dim() == 0) {
FloatBounds fb = compute_float_bounds(env, expr);
if (fb.valid && !fsv->empty() && fsv->isSubset(FloatSetVal::Range(fb.l, fb.u))) {
return nullptr;
}
}
if (fsv->size() == 1) {
domargs[1] = FloatLit::a(fsv->min());
domargs.push_back(FloatLit::a(fsv->max()));
} else {
domargs[1] = new SetLit(Expression::loc(dom), fsv);
}
break;
}
auto* al = new ArrayLit(Location().introduce(), fieldwise);
Type al_t = t;
al_t.dim(1);
al->type(al_t);
auto* c = Call::a(Location().introduce(), env.constants.ids.forall, {al});
c->type(t);
c->decl(env.model->matchFn(env, c, false));
return c;
}
case Type::BT_TUPLE: // fall through
case Type::BT_RECORD: {
ArrayLit* al = eval_array_lit(env, expr);
StructType* st = env.getStructType(ty);
auto* dom_al = Expression::cast<ArrayLit>(dom);

GCLock lock;
std::vector<Expression*> domargs({expr, dom});
if (Expression::type(expr).isfloat()) {
FloatSetVal* fsv = eval_floatset(env, dom);
if (fsv->size() == 1) {
domargs[1] = FloatLit::a(fsv->min());
domargs.push_back(FloatLit::a(fsv->max()));
std::vector<std::pair<int, int>> dims;
if (ty.dim() > 0) {
dims.resize(al->dims());
for (size_t i = 0; i < al->dims(); i++) {
dims[i] = std::make_pair(al->min(i), al->max(i));
}
}
std::vector<Expression*> fieldwise;
for (long long int i = 0; i < st->size(); ++i) {
auto* field_ti = Expression::cast<TypeInst>((*dom_al)[i]);
if (field_ti->domain() != nullptr) {
if (ty.dim() > 0) {
ArrayLit* slice = field_slice(env, st, al, dims, i + 1);
for (unsigned int j = 0; j < slice->size(); j++) {
auto* con = mk_domain_constraint(env, (*slice)[j], field_ti->domain());
if (con != nullptr) {
fieldwise.push_back(con);
};
}
} else {
auto* con = mk_domain_constraint(env, (*al)[i], field_ti->domain());
if (con != nullptr) {
fieldwise.push_back(con);
};
}
}
}
if (fieldwise.size() <= 1) {
return fieldwise.empty() ? nullptr : fieldwise[0];
}
auto* forall_al = new ArrayLit(Location().introduce(), fieldwise);
Type al_t = retType;
al_t.dim(1);
forall_al->type(al_t);
auto* c = Call::a(Location().introduce(), env.constants.ids.forall, {forall_al});
c->type(retType);
c->decl(env.model->matchFn(env, c, false));
return c;
}
case Type::BT_BOT: {
// Nothing to be done for empty arrays/sets
return nullptr;
}
default: {
throw EvalError(env, Expression::loc(dom),
"domain restrictions other than int and float not supported yet");
}
}
assert(domargs[1] != nullptr);

Call* c = Call::a(Location().introduce(), "var_dom", domargs);
c->type(Type::varbool());
c->decl(env.model->matchFn(env, c, false));
if (c->decl() == nullptr) {
throw InternalError("no matching declaration found for var_dom");
}
c->type(t);
c->type(retType);
return c;
}

Expand Down Expand Up @@ -5570,6 +5606,23 @@ FlatModelStatistics statistics(Env& m) {
return stats;
}

ArrayLit* field_slice(EnvI& env, StructType* st, ArrayLit* al,
std::vector<std::pair<int, int>> dims, long long int field) {
assert(GC::locked());
assert(Expression::type(al).structBT() && Expression::type(al).dim() > 0);
Type field_ty = (*st)[field - 1];
// TODO: This could be done efficiently using slicing (if we change the memory layout for
// arrays of tuples)
std::vector<Expression*> tmp(al->size());
for (int i = 0; i < al->size(); ++i) {
tmp[i] = new FieldAccess(Expression::loc((*al)[i]).introduce(), (*al)[i], IntLit::a(field));
Expression::type(tmp[i], field_ty);
}
auto* field_slice = new ArrayLit(Expression::loc(al).introduce(), tmp, dims);
Expression::type(field_slice, Type::arrType(env, al->type(), field_ty));
return field_slice;
}

std::vector<Expression*> field_slices(EnvI& env, Expression* arrExpr) {
assert(GC::locked());
assert(Expression::type(arrExpr).structBT() && Expression::type(arrExpr).dim() > 0);
Expand All @@ -5582,18 +5635,8 @@ std::vector<Expression*> field_slices(EnvI& env, Expression* arrExpr) {
}

std::vector<Expression*> field_al(st->size());
for (int i = 0; i < st->size(); ++i) {
Type field_ty = (*st)[i];
// TODO: This could be done efficiently using slicing (if we change the memory layout for
// arrays of tuples)
GCLock lock;
std::vector<Expression*> tmp(al->size());
for (int j = 0; j < al->size(); ++j) {
tmp[j] = new FieldAccess(Expression::loc((*al)[j]).introduce(), (*al)[j], IntLit::a(i + 1));
Expression::type(tmp[j], field_ty);
}
field_al[i] = new ArrayLit(Expression::loc(al).introduce(), tmp, dims);
Expression::type(field_al[i], Type::arrType(env, al->type(), field_ty));
for (long long int i = 0; i < st->size(); ++i) {
field_al[i] = field_slice(env, st, al, dims, i + 1);
}
return field_al;
}
Expand Down
130 changes: 25 additions & 105 deletions lib/flatten/flatten_call.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -1030,107 +1030,25 @@ EE flatten_call(EnvI& env, const Ctx& input_ctx, Expression* e, VarDecl* r, VarD
} else {
for (unsigned int i = 0; i < decl->paramCount(); i++) {
if (decl->param(i)->type().dim() > 0) {
// Check array index sets
auto* al = Expression::cast<ArrayLit>(follow_id(args[i]()));
VarDecl* pi = decl->param(i);
for (unsigned int j = 0; j < pi->ti()->ranges().size(); j++) {
TypeInst* range_ti = pi->ti()->ranges()[j];
if ((range_ti->domain() != nullptr) && !Expression::isa<TIId>(range_ti->domain())) {
check_index_sets(env, decl->param(i), args[i](), true);
}
if (Expression* dom = decl->param(i)->ti()->domain()) {
if (!Expression::isa<TIId>(dom)) {
KeepAlive domconstraint;
{
GCLock lock;
IntSetVal* isv = eval_intset(env, range_ti->domain());
if (isv->min() != al->min(j) || isv->max() != al->max(j)) {
std::ostringstream oss;
oss << "array index set " << (j + 1) << " of argument " << (i + 1)
<< " does not match declared index set";
throw FlatteningError(env, Expression::loc(e), oss.str());
}
domconstraint = mk_domain_constraint(env, args[i](), dom);
}
}
}
std::vector<std::pair<KeepAlive, TypeInst*>> stack({{args[i], decl->param(i)->ti()}});
while (!stack.empty()) {
KeepAlive curArg = stack.back().first;
TypeInst* curInst = stack.back().second;
stack.pop_back();
if (Expression* dom = curInst->domain()) {
if (!Expression::isa<TIId>(dom)) {
// May have to constrain actual argument
if (Expression::type(curArg()).bt() == Type::BT_INT) {
GCLock lock;
IntSetVal* isv = eval_intset(env, dom);
bool needToConstrain;
if (Expression::type(curArg()).st() == Type::ST_SET) {
needToConstrain = true;
} else {
if (Expression::type(curArg()).dim() > 0) {
needToConstrain = true;
} else {
IntBounds ib = compute_int_bounds(env, curArg());
needToConstrain =
!ib.valid || isv->empty() || !isv->isSubset(IntSetVal::Range(ib.l, ib.u));
}
}
if (needToConstrain) {
KeepAlive domconstraint;
{
GCLock lock;
domconstraint = mk_domain_constraint(env, curArg(), dom);
}
if (ctx.b == C_ROOT) {
(void)flat_exp(env, Ctx(), domconstraint(), env.constants.varTrue,
env.constants.varTrue);
} else {
Ctx domctx = ctx;
domctx.neg = false;
EE ee = flat_exp(env, domctx, domconstraint(), nullptr, env.constants.varTrue);
ee.b = ee.r;
args_ee.push_back(ee);
}
}
} else if (Expression::type(curArg()).bt() == Type::BT_FLOAT) {
GCLock lock;

FloatSetVal* fsv = eval_floatset(env, dom);
bool needToConstrain;
if (Expression::type(curArg()).dim() > 0) {
needToConstrain = true;
} else {
FloatBounds fb = compute_float_bounds(env, curArg());
needToConstrain =
!fb.valid || fsv->empty() || !fsv->isSubset(FloatSetVal::Range(fb.l, fb.u));
}

if (needToConstrain) {
KeepAlive domconstraint;
{
GCLock lock;
domconstraint = mk_domain_constraint(env, curArg(), dom);
}
if (ctx.b == C_ROOT) {
(void)flat_exp(env, Ctx(), domconstraint(), env.constants.varTrue,
env.constants.varTrue);
} else {
Ctx domctx = ctx;
domctx.neg = false;
EE ee = flat_exp(env, domctx, domconstraint(), nullptr, env.constants.varTrue);
ee.b = ee.r;
args_ee.push_back(ee);
}
}
} else if (Expression::type(curArg()).structBT()) {
GCLock lock;
auto* al = Expression::cast<ArrayLit>(curInst->domain());
for (long long i = 0; i < al->size(); ++i) {
auto* fa = new FieldAccess(Expression::loc(curArg()).introduce(), curArg(),
IntLit::a(i + 1));
fa->type(Expression::type((*al)[i]));
stack.emplace_back(fa, Expression::cast<TypeInst>((*al)[i]));
}
} else if (Expression::type(curArg()).bt() == Type::BT_BOT) {
// Nothing to be done for empty arrays/sets
if (domconstraint() != nullptr) {
if (ctx.b == C_ROOT) {
(void)flat_exp(env, Ctx(), domconstraint(), env.constants.varTrue,
env.constants.varTrue);
} else {
throw EvalError(env, Expression::loc(curInst),
"domain restrictions other than int and float not supported yet");
Ctx domctx = ctx;
domctx.neg = false;
EE ee = flat_exp(env, domctx, domconstraint(), nullptr, env.constants.varTrue);
ee.b = ee.r;
args_ee.push_back(ee);
}
}
}
Expand Down Expand Up @@ -1322,13 +1240,15 @@ EE flatten_call(EnvI& env, const Ctx& input_ctx, Expression* e, VarDecl* r, VarD
GCLock lock;
domconstraint = mk_domain_constraint(env, ret.r(), decl->ti()->domain());
}
if (ctx.b == C_ROOT) {
(void)flat_exp(env, Ctx(), domconstraint(), env.constants.varTrue,
env.constants.varTrue);
} else {
EE ee = flat_exp(env, Ctx(), domconstraint(), nullptr, env.constants.varTrue);
ee.b = ee.r;
args_ee.push_back(ee);
if (domconstraint() != nullptr) {
if (ctx.b == C_ROOT) {
(void)flat_exp(env, Ctx(), domconstraint(), env.constants.varTrue,
env.constants.varTrue);
} else {
EE ee = flat_exp(env, Ctx(), domconstraint(), nullptr, env.constants.varTrue);
ee.b = ee.r;
args_ee.push_back(ee);
}
}
}
}
Expand Down
14 changes: 8 additions & 6 deletions lib/flatten/flatten_let.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -53,12 +53,14 @@ EE flatten_let(EnvI& env, const Ctx& ctx, Expression* e, VarDecl* r, VarDecl* b)
if (vd->ti()->domain() != nullptr) {
GCLock lock;
auto* c = mk_domain_constraint(env, ee.r(), vd->ti()->domain());
VarDecl* b_b = (nctx.b == C_ROOT && b == env.constants.varTrue) ? b : nullptr;
VarDecl* r_r = (nctx.b == C_ROOT && b == env.constants.varTrue) ? b : nullptr;
ee = flat_exp(env, nctx, c, r_r, b_b);
cs.push_back(ee);
ee.b = ee.r;
cs.push_back(ee);
if (c != nullptr) {
VarDecl* b_b = (nctx.b == C_ROOT && b == env.constants.varTrue) ? b : nullptr;
VarDecl* r_r = (nctx.b == C_ROOT && b == env.constants.varTrue) ? b : nullptr;
ee = flat_exp(env, nctx, c, r_r, b_b);
cs.push_back(ee);
ee.b = ee.r;
cs.push_back(ee);
}
}
flatten_vardecl_annotations(env, vd, nullptr, vd);
} else {
Expand Down

0 comments on commit 23e35f9

Please sign in to comment.