diff --git a/CHANGES.txt b/CHANGES.txt index db316c713..75705e030 100644 --- a/CHANGES.txt +++ b/CHANGES.txt @@ -5,6 +5,29 @@ All bug numbers refer to the issue tracker at https://github.com/MiniZinc/libminizinc/issues +Version 2.0.14 +============== + +Changes: + + - Less aggressive aggregation of linear expressions in cases where it + leads to much less efficient FlatZinc. + - Don't create temporary variable for an array literal if it is discarded + immediately anyway. + - Only create new partiality variable for if-then-else expression if there's + at least one var condition. + - Replace recursive definitions of array_intersect and array_union with + iterative ones. + +Bug fixes: + - Don't report warnings about partiality when using extended generator + expressions. + - Include cmath to enable building with some versions of gcc. + - Constrain result of function call based on function return type if necessary. + - Make sure linear expressions generated during binding of variables are + properly flattened (including simplification of the linear expression) + + Version 2.0.13 ============== diff --git a/CMakeLists.txt b/CMakeLists.txt index bff8e9273..b264889ee 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -17,7 +17,7 @@ project (libminizinc CXX) # The version number. set (libminizinc_VERSION_MAJOR 2) set (libminizinc_VERSION_MINOR 0) -set (libminizinc_VERSION_PATCH 13) +set (libminizinc_VERSION_PATCH 14) if (ADDITIONAL_DATE_STRING) set (libminizinc_VERSION_PATCH "${libminizinc_VERSION_PATCH}.${ADDITIONAL_DATE_STRING}") diff --git a/include/minizinc/ast.hh b/include/minizinc/ast.hh index 3716ae972..71f2d47d9 100644 --- a/include/minizinc/ast.hh +++ b/include/minizinc/ast.hh @@ -1244,6 +1244,8 @@ namespace MiniZinc { BoolLit* lit_false; /// Variable bound to false VarDecl* var_false; + /// Special variable to signal compiler to ignore result + VarDecl* var_ignore; /// Infinite set SetLit* infinity; /// Function item used to keep track of redefined variables diff --git a/include/minizinc/flatten_internal.hh b/include/minizinc/flatten_internal.hh index f6a0a0d58..1870641eb 100644 --- a/include/minizinc/flatten_internal.hh +++ b/include/minizinc/flatten_internal.hh @@ -12,6 +12,8 @@ #ifndef __MINIZINC_FLATTEN_INTERNAL_HH__ #define __MINIZINC_FLATTEN_INTERNAL_HH__ +#include + #include #include #include @@ -193,6 +195,9 @@ namespace MiniZinc { IntSetRanges d2(dom2); return Ranges::equal(d1,d2); } + static bool domain_tighter(Domain dom, Bounds b) { + return !b.valid || dom->min() > b.l || dom->max() < b.u; + } static bool domain_intersects(Domain dom, Val v0, Val v1) { return (v0 > v1) || (dom->size() > 0 && dom->min(0) <= v1 && v0 <= dom->max(dom->size()-1)); } @@ -307,6 +312,10 @@ namespace MiniZinc { static bool domain_contains(Domain dom, Val v) { return dom==NULL || (dom->lhs()->cast()->v() <= v && dom->rhs()->cast()->v() >= v); } + static bool domain_tighter(Domain dom, Bounds b) { + return dom != NULL && (!b.valid || dom->lhs()->cast()->v() > b.l || + dom->rhs()->cast()->v() < b.u); + } static bool domain_intersects(Domain dom, Val v0, Val v1) { return dom==NULL || (dom->lhs()->cast()->v() <= v1 && dom->rhs()->cast()->v() >= v0); } diff --git a/lib/ast.cpp b/lib/ast.cpp index 8471949ae..61b8d0df1 100644 --- a/lib/ast.cpp +++ b/lib/ast.cpp @@ -960,6 +960,7 @@ namespace MiniZinc { var_true = new VarDecl(Location(), ti, "_bool_true", lit_true); lit_false = new BoolLit(Location(), false); var_false = new VarDecl(Location(), ti, "_bool_false", lit_false); + var_ignore = new VarDecl(Location(), ti, "_bool_ignore"); absent = new Id(Location(),"_absent",NULL); Type absent_t; absent_t.bt(Type::BT_BOT); @@ -1097,6 +1098,7 @@ namespace MiniZinc { v.push_back(var_true); v.push_back(lit_false); v.push_back(var_false); + v.push_back(var_ignore); v.push_back(absent); v.push_back(infinity); v.push_back(new StringLit(Location(),ids.forall)); diff --git a/lib/flatten.cpp b/lib/flatten.cpp index 860878ec8..a407f5597 100644 --- a/lib/flatten.cpp +++ b/lib/flatten.cpp @@ -781,6 +781,8 @@ namespace MiniZinc { KeepAlive bind(EnvI& env, Ctx ctx, VarDecl* vd, Expression* e) { assert(e==NULL || !e->isa()); + if (vd==constants().var_ignore) + return e; if (Id* ident = e->dyn_cast()) { if (ident->decl()) { VarDecl* e_vd = follow_id_to_decl(ident)->cast(); @@ -1255,15 +1257,18 @@ namespace MiniZinc { nx.push_back(vd->id()); args.push_back(new ArrayLit(Location().introduce(),nx)); args[1]->type(le_x->type()); - if (c->type().bt()==Type::BT_INT) { - IntVal d = c->args()[2]->cast()->v(); - args.push_back(IntLit::a(-d)); - nc = new Call(c->loc().introduce(), constants().ids.int_.lin_eq, args); - } else { - FloatVal d = c->args()[2]->cast()->v(); - args.push_back(FloatLit::a(-d)); - nc = new Call(c->loc().introduce(), constants().ids.float_.lin_eq, args); + args.push_back(c->args()[2]); + nc = new Call(c->loc().introduce(), constants().ids.lin_exp, args); + nc->decl(env.orig->matchFn(env,nc)); + if (nc->decl() == NULL) { + throw InternalError("undeclared function or predicate " + +nc->id().str()); } + nc->type(nc->decl()->rtype(env,args)); + BinOp* bop = new BinOp(nc->loc(), nc, BOT_EQ, IntLit::a(0)); + bop->type(Type::varbool()); + flat_exp(env, Ctx(), bop, constants().var_true, constants().var_true); + return vd->id(); } else { args.resize(c->args().size()); std::copy(c->args().begin(),c->args().end(),args.begin()); @@ -1769,11 +1774,6 @@ namespace MiniZinc { VarDecl* nr = r; - if (b==NULL) { - b = newVarDecl(env, Ctx(), new TypeInst(Location().introduce(),Type::varbool()), NULL, NULL, NULL); - } - - Ctx cmix; cmix.b = C_MIX; cmix.i = C_MIX; @@ -1853,7 +1853,11 @@ namespace MiniZinc { eq_then = new BinOp(Location().introduce(),nr->id(),BOT_EQ,ethen.r()); eq_then->type(Type::varbool()); } - + + if (b==NULL) { + b = newVarDecl(env, Ctx(), new TypeInst(Location().introduce(),Type::varbool()), NULL, NULL, NULL); + } + { // Create a clause with all the previous conditions negated, the // current condition, and the then branch. @@ -2416,6 +2420,18 @@ namespace MiniZinc { std::vector alv; for (unsigned int i=0; iv().size(); i++) { if (Call* sc = same_call(al->v()[i],cid)) { + if (VarDecl* alvi_decl = follow_id_to_decl(al->v()[i])->dyn_cast()) { + if (alvi_decl->ti()->domain()) { + typename LinearTraits::Domain sc_dom = LinearTraits::eval_domain(env,alvi_decl->ti()->domain()); + typename LinearTraits::Bounds sc_bounds = LinearTraits::compute_bounds(env,sc); + if (LinearTraits::domain_tighter(sc_dom, sc_bounds)) { + coeffv.push_back(c_coeff[i]); + alv.push_back(al->v()[i]); + continue; + } + } + } + Val cd = c_coeff[i]; GCLock lock; ArrayLit* sc_coeff = eval_array_lit(env,sc->args()[0]); @@ -3452,6 +3468,7 @@ namespace MiniZinc { let_exprs[1] = new BinOp(Location().introduce(),cond,BOT_IMPL,r_eq_e); let_exprs[1]->type(Type::varbool()); let_exprs[1]->addAnnotation(constants().ann.promise_total); + let_exprs[1]->addAnnotation(constants().ann.maybe_partial); std::vector absent_r_args(1); absent_r_args[0] = r->id(); Call* absent_r = new Call(Location().introduce(), "absent", absent_r_args); @@ -4411,7 +4428,7 @@ namespace MiniZinc { if (ctx.b==C_ROOT && decl->e()==NULL && cid == constants().ids.forall && r==constants().var_true) { ret.b = bind(env,ctx,b,constants().lit_true); - EE flat_al = flat_exp(env,Ctx(),c->args()[0],NULL,constants().var_true); + EE flat_al = flat_exp(env,Ctx(),c->args()[0],constants().var_ignore,constants().var_true); ArrayLit* al = follow_id(flat_al.r())->cast(); nctx.b = C_ROOT; for (unsigned int i=0; iv().size(); i++) @@ -4797,6 +4814,37 @@ namespace MiniZinc { } else { ret = flat_exp(env,ctx,decl->e(),r,NULL); args_ee.push_back(ret); + if (decl->ti()->domain() && !decl->ti()->domain()->isa()) { + BinOpType bot; + if (ret.r()->type().st() == Type::ST_SET) { + bot = BOT_SUBSET; + } else { + bot = BOT_IN; + } + + KeepAlive domconstraint; + if (decl->e()->type().dim() > 0) { + GCLock lock; + std::vector domargs(2); + domargs[0] = ret.r(); + domargs[1] = decl->ti()->domain(); + Call* c = new Call(Location().introduce(),"var_dom",domargs); + c->type(Type::varbool()); + c->decl(env.orig->matchFn(env,c)); + domconstraint = c; + } else { + GCLock lock; + domconstraint = new BinOp(Location().introduce(),ret.r(),bot,decl->ti()->domain()); + } + domconstraint()->type(ret.r()->type().ispar() ? Type::parbool() : Type::varbool()); + if (ctx.b == C_ROOT) { + (void) flat_exp(env, Ctx(), domconstraint(), constants().var_true, constants().var_true); + } else { + EE ee = flat_exp(env, Ctx(), domconstraint(), NULL, constants().var_true); + ee.b = ee.r; + args_ee.push_back(ee); + } + } } ret.b = conj(env,b,Ctx(),args_ee); } diff --git a/share/minizinc/std/builtins.mzn b/share/minizinc/std/builtins.mzn index 1108d083a..36ae8ee9e 100644 --- a/share/minizinc/std/builtins.mzn +++ b/share/minizinc/std/builtins.mzn @@ -648,13 +648,36 @@ function var int: card(var set of int: x); /** @group builtins.set Return the union of the sets in array \a x */ function set of $U: array_union(array[$T] of set of $U: x); /** @group builtins.set Return the union of the sets in array \a x */ -function var set of int: array_union(array[$T] of var set of int: x) = - array_union_rec(array1d(x)); +function var set of int: array_union(array[int] of var set of int: x) ::promise_total = + if length(x)=0 then {} + elseif length(x)=1 then x[min(index_set(x))] + else + let { + int: l=min(index_set(x)); + int: u=max(index_set(x)); + array[l..u-1] of var set of ub_array(x): y; + constraint y[l]=x[l] union x[l+1]; + constraint forall (i in l+2..u) (y[i-1]=y[i-2] union x[i]); + } in y[u-1] + endif; + /** @group builtins.set Return the intersection of the sets in array \a x */ function set of $U: array_intersect(array[$T] of set of $U: x); -function var set of int: array_intersect(array[$T] of var set of int: x) = - array_intersect_rec(array1d(x)); + +/** @group builtins.set Return the intersection of the sets in array \a x */ +function var set of int: array_intersect(array[int] of var set of int: x) ::promise_total = + if length(x)=0 then assert(false,"can't be!",-infinity..infinity) + elseif length(x)=1 then x[min(index_set(x))] + else + let { + int: l=min(index_set(x)); + int: u=max(index_set(x)); + array[l..u-1] of var set of ub_array(x): y; + constraint y[l]=x[l] intersect x[l+1]; + constraint forall (i in l+2..u) (y[i-1]=y[i-2] intersect x[i]); + } in y[u-1] + endif; /*** @groupdef builtins.array Array operations @@ -1850,21 +1873,6 @@ function var float: min_t(array[int] of var float: x) :: promise_total = constraint array_float_minimum(m,x); } in m endif; - -function var set of int: array_union_rec(array[int] of var set of int: x) = - if length(x)=0 then {} - elseif length(x)=1 then x[min(index_set(x))] - else x[min(index_set(x))] union - array_union_rec([x[i] | i in min(index_set(x))+1..max(index_set(x))]) - endif; - -function var set of int: array_intersect_rec(array[int] of var set of int: x) = - if length(x)=0 then {} - elseif length(x)=1 then x[min(index_set(x))] - else x[min(index_set(x))] intersect - array_intersect_rec([x[i] | i in min(index_set(x))+1..max(index_set(x))]) - endif; - /*** @groupdef builtins.random Random Number Generator builtins