Merge branch 'hotfix/2.1.4'

CHANGES.txt

@@ -5,6 +5,31 @@
 All bug numbers refer to the issue tracker at
 https://github.com/MiniZinc/libminizinc/issues
 
+Version 2.1.4
+=============
+
+Changes:
+ - Add warning for MIP solvers that do not support -a option for satisfaction
+   problems.
+ - Print introduced variable names with additional underscore to make
+   debugging FlatZinc easier. Fixes #147.
+ - Add support for pow function in linearisation library.
+ - Add support for parallel solving with CBC.
+ - Flatten top-level conjunctions in the order defined in the model.
+
+Bug fixes:
+ - Fix a garbage collection bug that could cause dangling pointers when
+   expressions were copied.
+ - Fix type checker to allow empty arrays to be assigned to variables
+   declared as arrays of enums.
+ - Fix infeasibility check in MIP translation for some inequality constraints.
+ - Improved defines_var annotations for reified xor constraints. Fixes #146.
+ - Fix output of empty integer sets and deal with empty arrays in output models.
+ - Fix MIP translation when boolean variables were removed due to aliasing.
+ - Improve corner cases for linearisation of cumulative constraint.
+ - Properly report undefinedness in par bool expressions.
+ - Enable some additional constant folding during flattening. Fixes #149.
+
 Version 2.1.3
 =============
 

CMakeLists.txt

@@ -27,7 +27,7 @@ endif()
 # The version number.
 set (libminizinc_VERSION_MAJOR 2)
 set (libminizinc_VERSION_MINOR 1)
-set (libminizinc_VERSION_PATCH 3)
+set (libminizinc_VERSION_PATCH 4)
 
 if (ADDITIONAL_DATE_STRING)
   set (libminizinc_VERSION_PATCH "${libminizinc_VERSION_PATCH}.${ADDITIONAL_DATE_STRING}")

README_MIP.txt

@@ -5,16 +5,15 @@ The executables mzn-cplex, mzn-gurobi, mzn-scip and mzn-cbc use the
 corresponding MIP solver library. They can interpret FlatZinc code compiled with
 -Glinear, as well as handle original model files (by flattening + solving).
 
-All MIP solvers except OSI CBC directly support multi-threading. For CBC
-compiled with enable-parallel, it is possible through --cbc-flags.
-For models with non-integral objective function you might need to adjust
---absGap/--relGap/--objDiff.
+All MIP solvers directly support multi-threading. For this, CBC needs to be
+configured with --enable-cbc-parallel. Use svn/git to get the latest CBC revision,
+see https://projects.coin-or.org/Cbc.
 
-Calling mzn-gurobi directly:
+Calling a solver on a MiniZinc directly:
 
       mzn-gurobi -v -s -a -G linear model.mzn data.dzn
 
-or, more stable but slower due to file I/O:
+or separated flattening+solving - sometimes more stable but slower due to file I/O:
 
       mzn2fzn -G linear model.mzn data.dzn; mzn-gorubi -v -s -a model.fzn | solns2out model.ozn
 

include/minizinc/copy.hh

@@ -18,8 +18,10 @@ namespace MiniZinc {
 
   class CopyMap {
   protected:
-    typedef UNORDERED_NAMESPACE::unordered_map<void*,void*> MyMap;
-    MyMap m;
+    typedef UNORDERED_NAMESPACE::unordered_map<Model*,Model*> ModelMap;
+    ModelMap model_m;
+
+    ASTNodeWeakMap node_m;
   public:
     void insert(Expression* e0, Expression* e1);
     Expression* find(Expression* e);
@@ -35,13 +37,12 @@ namespace MiniZinc {
     FloatSetVal* find(FloatSetVal* e);
     template<class T>
     void insert(ASTExprVec<T> e0, ASTExprVec<T> e1) {
-      m.insert(std::pair<void*,void*>(e0.vec(),e1.vec()));
+      node_m.insert(e0.vec(),e1.vec());
     }
     template<class T>
     ASTExprVecO<T*>* find(ASTExprVec<T> e) {
-      MyMap::iterator it = m.find(e.vec());
-      if (it==m.end()) return NULL;
-      return static_cast<ASTExprVecO<T*>*>(it->second);
+      ASTNode* n = node_m.find(e.vec());
+      return static_cast<ASTExprVecO<T*>*>(n);
     }
   };
 

include/minizinc/gc.hh

@@ -15,6 +15,7 @@
 #include <cstdlib>
 #include <cassert>
 #include <new>
+#include <minizinc/stl_map_set.hh>
 
 namespace MiniZinc {
 
@@ -109,13 +110,16 @@ namespace MiniZinc {
   class KeepAlive;
   class WeakRef;
 
+  class ASTNodeWeakMap;
+
   /// Garbage collector
   class GC {
     friend class ASTNode;
     friend class ASTVec;
     friend class ASTChunk;
     friend class KeepAlive;
     friend class WeakRef;
+    friend class ASTNodeWeakMap;
   private:
     class Heap;
     /// The memory controlled by the collector
@@ -134,6 +138,9 @@ namespace MiniZinc {
     static void removeKeepAlive(KeepAlive* e);
     static void addWeakRef(WeakRef* e);
     static void removeWeakRef(WeakRef* e);
+    static void addNodeWeakMap(ASTNodeWeakMap* m);
+    static void removeNodeWeakMap(ASTNodeWeakMap* m);
+
   public:
     /// Acquire garbage collector lock for this thread
     static void lock(void);
@@ -201,6 +208,24 @@ namespace MiniZinc {
     WeakRef* next(void) const { return _n; }
   };
 
+  class ASTNodeWeakMap {
+    friend class GC;
+  private:
+    ASTNodeWeakMap(const WeakRef& e);
+    ASTNodeWeakMap& operator =(const ASTNodeWeakMap& e);
+
+  protected:
+    typedef UNORDERED_NAMESPACE::unordered_map<ASTNode*, ASTNode*> NodeMap;
+    ASTNodeWeakMap* _p;
+    ASTNodeWeakMap* _n;
+    ASTNodeWeakMap* next(void) const { return _n; }
+    NodeMap _m;
+  public:
+    ASTNodeWeakMap(void);
+    ~ASTNodeWeakMap(void);
+    void insert(ASTNode* n0, ASTNode* n1);
+    ASTNode* find(ASTNode* n);
+  };
 }
 
 #endif

include/minizinc/solvers/MIP/MIP_wrap.hh

@@ -90,6 +90,8 @@ class MIP_wrapper {
   public:
     /// Parameter
     bool fVerbose = false;
+
+    int nProbType = -2;  // +-1: max/min; 0: sat
 
   public:
     struct Output {
@@ -207,6 +209,8 @@ class MIP_wrapper {
 //     set<double> sLitValues;
     std::unordered_map<double, VarId> sLitValues;
 
+    void setProbType( int t ) { nProbType=t; }
+
     /// adding a variable, at once to the solver, this is for the 2nd phase
     virtual VarId addVar(double obj, double lb, double ub, 
                              VarType vt, std::string name=0) {

include/minizinc/values.hh

@@ -692,8 +692,12 @@ namespace MiniZinc {
   template<class Char, class Traits>
   std::basic_ostream<Char,Traits>&
   operator <<(std::basic_ostream<Char,Traits>& os, const IntSetVal& s) {
-    for (IntSetRanges isr(&s); isr(); ++isr)
-      os << isr.min() << ".." << isr.max() << " ";
+    if (s.size()==0) {
+      os << "1..0";
+    } else {
+      for (IntSetRanges isr(&s); isr(); ++isr)
+        os << isr.min() << ".." << isr.max() << " ";
+    }
     return os;
   }
 

lib/ast.cpp

@@ -227,7 +227,7 @@ namespace MiniZinc {
     if (idn()==-1)
       return v();
     std::ostringstream oss;
-    oss << "X_INTRODUCED_" << idn();
+    oss << "X_INTRODUCED_" << idn() << "_";
     return oss.str();
   }
 

lib/copy.cpp

@@ -15,52 +15,43 @@
 namespace MiniZinc {
 
   void CopyMap::insert(Expression* e0, Expression* e1) {
-    m.insert(std::pair<void*,void*>(e0,e1));
+    if (!e0->isUnboxedInt() && !e1->isUnboxedInt())
+      node_m.insert(e0,e1);
   }
   Expression* CopyMap::find(Expression* e) {
-    MyMap::iterator it = m.find(e);
-    if (it==m.end()) return NULL;
-    return static_cast<Expression*>(it->second);
+    return static_cast<Expression*>(node_m.find(e));
   }
   void CopyMap::insert(Item* e0, Item* e1) {
-    m.insert(std::pair<void*,void*>(e0,e1));
+    node_m.insert(e0,e1);
   }
   Item* CopyMap::find(Item* e) {
-    MyMap::iterator it = m.find(e);
-    if (it==m.end()) return NULL;
-    return static_cast<Item*>(it->second);
+    return static_cast<Item*>(node_m.find(e));
   }
   void CopyMap::insert(Model* e0, Model* e1) {
-    m.insert(std::pair<void*,void*>(e0,e1));
+    model_m.insert(std::make_pair(e0,e1));
   }
   Model* CopyMap::find(Model* e) {
-    MyMap::iterator it = m.find(e);
-    if (it==m.end()) return NULL;
-    return static_cast<Model*>(it->second);
+    ModelMap::iterator it = model_m.find(e);
+    if (it==model_m.end()) return NULL;
+    return it->second;
   }
   void CopyMap::insert(const ASTString& e0, const ASTString& e1) {
-    m.insert(std::pair<void*,void*>(e0.aststr(),e1.aststr()));
+    node_m.insert(e0.aststr(),e1.aststr());
   }
   ASTStringO* CopyMap::find(const ASTString& e) {
-    MyMap::iterator it = m.find(e.aststr());
-    if (it==m.end()) return NULL;
-    return static_cast<ASTStringO*>(it->second);
+    return static_cast<ASTStringO*>(node_m.find(e.aststr()));
   }
   void CopyMap::insert(IntSetVal* e0, IntSetVal* e1) {
-    m.insert(std::pair<void*,void*>(e0,e1));
+    node_m.insert(e0,e1);
   }
   IntSetVal* CopyMap::find(IntSetVal* e) {
-    MyMap::iterator it = m.find(e);
-    if (it==m.end()) return NULL;
-    return static_cast<IntSetVal*>(it->second);
+    return static_cast<IntSetVal*>(node_m.find(e));
   }
   void CopyMap::insert(FloatSetVal* e0, FloatSetVal* e1) {
-    m.insert(std::pair<void*,void*>(e0,e1));
+    node_m.insert(e0,e1);
   }
   FloatSetVal* CopyMap::find(FloatSetVal* e) {
-    MyMap::iterator it = m.find(e);
-    if (it==m.end()) return NULL;
-    return static_cast<FloatSetVal*>(it->second);
+    return static_cast<FloatSetVal*>(node_m.find(e));
   }
 
   Location copy_location(CopyMap& m, const Location& _loc) {