Skip to content

Commit

Permalink
Make the mzn_in_root_context function more flexible in where it can…
Browse files Browse the repository at this point in the history
… be called. Previously, this could only be called directly in an if-then-else (as the only condition). Now, it can be called from anywhere. The semantics is now better defined: it returns whether the surrounding call is in root context.
  • Loading branch information
guidotack committed Oct 30, 2024
1 parent 58d2d79 commit a61b555
Show file tree
Hide file tree
Showing 13 changed files with 126 additions and 93 deletions.
2 changes: 2 additions & 0 deletions changes.rst
Original file line number Diff line number Diff line change
Expand Up @@ -12,6 +12,8 @@ Changes:
`else` branch.
- Make ``sort`` functions return array of enum when input is array of
enum (:bugref:`853`).
- Make the ``mzn_in_root_context`` function (which is used only internally and
should not be used in user models) more flexible in where it can be called.

Bug fixes:
^^^^^^^^^^
Expand Down
39 changes: 4 additions & 35 deletions include/minizinc/flatten_internal.hh
Original file line number Diff line number Diff line change
Expand Up @@ -41,39 +41,6 @@ public:
explicit EE(Expression* r0 = nullptr, Expression* b0 = nullptr) : r(r0), b(b0) {}
};

/// Boolean evaluation context
enum BCtx { C_ROOT, C_POS, C_NEG, C_MIX };

/// Evaluation context
struct Ctx {
/// Boolean context
BCtx b;
/// Integer context
BCtx i;
/// Boolen negation flag
bool neg;
/// Default constructor (root context)
Ctx() : b(C_ROOT), i(C_MIX), neg(false) {}
/// Copy constructor
Ctx(const Ctx& ctx) : b(ctx.b), i(ctx.i), neg(ctx.neg) {}
/// Assignment operator
Ctx& operator=(const Ctx& ctx) {
if (this != &ctx) {
b = ctx.b;
i = ctx.i;
neg = ctx.neg;
}
return *this;
}
/// Return true variable if in root context, nullptr otherwise
VarDecl* partialityVar(EnvI& env) const;
};

/// Turn \a c into positive context
BCtx operator+(const BCtx& c);
/// Negate context \a c
BCtx operator-(const BCtx& c);

struct MultiPassInfo {
// The current pass number (used for unifying and disabling path construction in final pass)
unsigned int currentPassNumber;
Expand Down Expand Up @@ -375,10 +342,12 @@ public:
bool ignoreUnknownIds;
struct CallStackEntry {
Expression* e;
Ctx ctx;
bool tag;
bool replaced;
CallStackEntry(Expression* e0 = nullptr, bool tag0 = false)
: e(e0), tag(tag0), replaced(false) {}
CallStackEntry() : e(nullptr), tag(false), replaced(false) {}
CallStackEntry(Expression* e0, bool tag0, const Ctx& ctx0)
: e(e0), ctx(ctx0), tag(tag0), replaced(false) {}
};
std::vector<CallStackEntry> callStack;
std::vector<int> idStack;
Expand Down
35 changes: 34 additions & 1 deletion include/minizinc/model.hh
Original file line number Diff line number Diff line change
Expand Up @@ -388,14 +388,47 @@ public:
std::ostream& evalOutput(std::ostream& os, std::ostream& log);
};

/// Boolean evaluation context
enum BCtx { C_ROOT, C_POS, C_NEG, C_MIX };

/// Evaluation context
struct Ctx {
/// Boolean context
BCtx b;
/// Integer context
BCtx i;
/// Boolen negation flag
bool neg;
/// Default constructor (root context)
Ctx() : b(C_ROOT), i(C_MIX), neg(false) {}
/// Copy constructor
Ctx(const Ctx& ctx) : b(ctx.b), i(ctx.i), neg(ctx.neg) {}
/// Assignment operator
Ctx& operator=(const Ctx& ctx) {
if (this != &ctx) {
b = ctx.b;
i = ctx.i;
neg = ctx.neg;
}
return *this;
}
/// Return true variable if in root context, nullptr otherwise
VarDecl* partialityVar(EnvI& env) const;
};

/// Turn \a c into positive context
BCtx operator+(const BCtx& c);
/// Negate context \a c
BCtx operator-(const BCtx& c);

class CallStackItem {
private:
EnvI& _env;
enum CSIType { CSI_NONE, CSI_VD, CSI_REDUNDANT, CSI_SYMMETRY } _csiType;
bool _maybePartial;

public:
CallStackItem(EnvI& env0, Expression* e);
CallStackItem(EnvI& env0, Expression* e, const Ctx& ctx = Ctx());
CallStackItem(EnvI& env0, Id* ident, IntVal i);
void replace();
~CallStackItem();
Expand Down
15 changes: 15 additions & 0 deletions lib/builtins.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -2200,6 +2200,17 @@ bool b_in_symmetry_breaking_constraint(EnvI& env, Call* /*call*/) {
return env.inSymmetryBreakingConstraint > 0;
}

bool b_mzn_in_root_context(EnvI& env, Call* call) {
// Find context of enclosing call
for (unsigned int i = env.callStack.size(); (i--) != 0U;) {
if (env.callStack[i].e != nullptr && Expression::isa<Call>(env.callStack[i].e) &&
Expression::cast<Call>(env.callStack[i].e)->id() != env.constants.ids.mzn_in_root_context) {
return env.callStack[i].ctx.b == C_ROOT;
}
}
throw EvalError(env, Expression::loc(call), "mzn_in_root_context used outside of predicate");
}

Expression* b_set2array(EnvI& env, Call* call) {
assert(call->argCount() == 1);
GCLock lock;
Expand Down Expand Up @@ -3931,6 +3942,10 @@ void register_builtins(Env& e) {
rb(env, m, env.constants.ids.mzn_redundant_constraint, {Type::varbool()},
b_mzn_redundant_constraint);
}
{
rb(env, m, env.constants.ids.mzn_in_root_context, {}, b_mzn_in_root_context);
rb(env, m, env.constants.ids.mzn_in_root_context, {Type::vartop()}, b_mzn_in_root_context);
}
{
std::vector<Type> t(1);
t[0] = Type::parstring();
Expand Down
10 changes: 4 additions & 6 deletions lib/flatten.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -1894,7 +1894,8 @@ std::string EnvI::show(IntSetVal* isv, unsigned int enumId) {
return show(sl);
}

CallStackItem::CallStackItem(EnvI& env0, Expression* e) : _env(env0), _csiType(CSI_NONE) {
CallStackItem::CallStackItem(EnvI& env0, Expression* e, const Ctx& ctx)
: _env(env0), _csiType(CSI_NONE) {
assert(Expression::type(e).bt() != Type::BT_UNKNOWN);

env0.checkCancel();
Expand All @@ -1917,12 +1918,12 @@ CallStackItem::CallStackItem(EnvI& env0, Expression* e) : _env(env0), _csiType(C
} else {
_maybePartial = false;
}
_env.callStack.emplace_back(e, false);
_env.callStack.emplace_back(e, false, ctx);
_env.maxCallStack = std::max(_env.maxCallStack, static_cast<unsigned int>(_env.callStack.size()));
}
CallStackItem::CallStackItem(EnvI& env0, Id* ident, IntVal i)
: _env(env0), _csiType(CSI_NONE), _maybePartial(false) {
_env.callStack.emplace_back(ident, true);
_env.callStack.emplace_back(ident, true, Ctx());
_env.maxCallStack = std::max(_env.maxCallStack, static_cast<unsigned int>(_env.callStack.size()));
}
void CallStackItem::replace() { _env.callStack.back().replaced = true; }
Expand Down Expand Up @@ -3827,9 +3828,6 @@ KeepAlive flat_cv_exp(EnvI& env, Ctx ctx, Expression* e) {
}
case Expression::E_CALL: {
Call* c = Expression::cast<Call>(e);
if (c->id() == env.constants.ids.mzn_in_root_context) {
return env.constants.boollit(ctx.b == C_ROOT);
}
if (ctx.b == C_ROOT && (c->decl()->e() != nullptr) &&
Expression::isa<BoolLit>(c->decl()->e())) {
bool allBool = true;
Expand Down
2 changes: 1 addition & 1 deletion lib/flatten/flatten_call.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -365,7 +365,7 @@ EE flatten_call(EnvI& env, const Ctx& input_ctx, Expression* e, VarDecl* r, VarD
Ctx nctx = ctx;
nctx.neg = false;
ASTString cid = c->id();
CallStackItem _csi(env, e);
CallStackItem _csi(env, e, input_ctx);

if (cid == env.constants.ids.bool2int && c->type().dim() == 0) {
if (ctx.neg) {
Expand Down
13 changes: 4 additions & 9 deletions lib/flatten/flatten_ite.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -295,15 +295,10 @@ EE flatten_ite(EnvI& env, const Ctx& ctx, Expression* e, VarDecl* r, VarDecl* b)
for (int i = 0; i < ite->size() && !foundTrueBranch; i++) {
bool cond = true;
EE e_if;
if (Expression::isa<Call>(ite->ifExpr(i)) &&
Expression::cast<Call>(ite->ifExpr(i))->id() == env.constants.ids.mzn_in_root_context) {
e_if = EE(env.constants.boollit(ctx.b == C_ROOT), env.constants.literalTrue);
} else {
Ctx cmix_not_negated;
cmix_not_negated.b = C_MIX;
cmix_not_negated.i = C_MIX;
e_if = flat_exp(env, cmix_not_negated, ite->ifExpr(i), nullptr, env.constants.varTrue);
}
Ctx cmix_not_negated;
cmix_not_negated.b = C_MIX;
cmix_not_negated.i = C_MIX;
e_if = flat_exp(env, cmix_not_negated, ite->ifExpr(i), nullptr, env.constants.varTrue);
if (Expression::type(e_if.r()) == Type::parbool()) {
{
GCLock lock;
Expand Down
12 changes: 4 additions & 8 deletions lib/stackdump.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -50,10 +50,8 @@ void StackDump::print(std::ostream& os) const {
long long int curloc_l = -1;

for (auto it = _stack.rbegin(); it != _stack.rend(); it++) {
EnvI::CallStackEntry entry(it->first, it->second);

Expression* e = entry.e;
bool isCompIter = entry.tag;
Expression* e = it->first;
bool isCompIter = it->second;
ASTString newloc_f = Expression::loc(e).filename();
if (Expression::loc(e).isIntroduced()) {
continue;
Expand Down Expand Up @@ -179,10 +177,8 @@ void StackDump::json(std::ostream& os) const {
os << "[";

for (auto it = _stack.rbegin(); it != _stack.rend(); it++) {
EnvI::CallStackEntry entry(it->first, it->second);

Expression* e = entry.e;
bool isCompIter = entry.tag;
Expression* e = it->first;
bool isCompIter = it->second;
ASTString newloc_f = Expression::loc(e).filename();
if (Expression::loc(e).isIntroduced()) {
continue;
Expand Down
6 changes: 3 additions & 3 deletions share/minizinc/std/redefinitions-2.1.1.mzn
Original file line number Diff line number Diff line change
Expand Up @@ -11,7 +11,7 @@ function var $$E: min(var set of $$E: s) =
% predicate set_min(var set of int: s, var int: m);
%
% function var $$E: min(var set of $$E: s) =
% if mzn_in_root_context(s) then min_t(s) else
% if mzn_in_root_context() then min_t(s) else
% let { constraint card(s) > 0 } in min_mt(s) endif;
%
% function var $$E: min_t(var set of $$E: s) ::promise_total =
Expand Down Expand Up @@ -39,8 +39,8 @@ function var $$E: max(var set of $$E: s) =
% predicate set_max(var set of int: s, var int: m);
%
% function var $$E: max(var set of $$E: s) =
% if mzn_in_root_context(s) then max_t(s) else
% let { constraint card(s) > 0 } in max_mt(s) endif;
% if mzn_in_root_context() then max_t(s) else
% let { constraint card() > 0 } in max_mt(s) endif;
%
% function var $$E: max_t(var set of $$E: s) ::promise_total =
% let {
Expand Down
Loading

0 comments on commit a61b555

Please sign in to comment.