Merge branch 'hotfix/2.0.14'

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
 ==============
 

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}")

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

include/minizinc/flatten_internal.hh

@@ -12,6 +12,8 @@
 #ifndef __MINIZINC_FLATTEN_INTERNAL_HH__
 #define __MINIZINC_FLATTEN_INTERNAL_HH__
 
+#include <cmath>
+
 #include <minizinc/copy.hh>
 #include <minizinc/flatten.hh>
 #include <minizinc/optimize.hh>
@@ -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<FloatLit>()->v() <= v && dom->rhs()->cast<FloatLit>()->v() >= v);
     }
+    static bool domain_tighter(Domain dom, Bounds b) {
+      return dom != NULL && (!b.valid || dom->lhs()->cast<FloatLit>()->v() > b.l ||
+                             dom->rhs()->cast<FloatLit>()->v() < b.u);
+    }
     static bool domain_intersects(Domain dom, Val v0, Val v1) {
       return dom==NULL || (dom->lhs()->cast<FloatLit>()->v() <= v1 && dom->rhs()->cast<FloatLit>()->v() >= v0);
     }

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));

lib/flatten.cpp

@@ -781,6 +781,8 @@ namespace MiniZinc {
 
   KeepAlive bind(EnvI& env, Ctx ctx, VarDecl* vd, Expression* e) {
     assert(e==NULL || !e->isa<VarDecl>());
+    if (vd==constants().var_ignore)
+      return e;
     if (Id* ident = e->dyn_cast<Id>()) {
       if (ident->decl()) {
         VarDecl* e_vd = follow_id_to_decl(ident)->cast<VarDecl>();
@@ -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<IntLit>()->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<FloatLit>()->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<KeepAlive> alv;
     for (unsigned int i=0; i<al->v().size(); i++) {
       if (Call* sc = same_call(al->v()[i],cid)) {
+        if (VarDecl* alvi_decl = follow_id_to_decl(al->v()[i])->dyn_cast<VarDecl>()) {
+          if (alvi_decl->ti()->domain()) {
+            typename LinearTraits<Lit>::Domain sc_dom = LinearTraits<Lit>::eval_domain(env,alvi_decl->ti()->domain());
+            typename LinearTraits<Lit>::Bounds sc_bounds = LinearTraits<Lit>::compute_bounds(env,sc);
+            if (LinearTraits<Lit>::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<Expression*> 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<ArrayLit>();
           nctx.b = C_ROOT;
           for (unsigned int i=0; i<al->v().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<TIId>()) {
+                    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<Expression*> 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);
               }

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