diff --git a/CHANGES.txt b/CHANGES.txt index 9420014ec..bbdba6304 100644 --- a/CHANGES.txt +++ b/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 ============= diff --git a/CMakeLists.txt b/CMakeLists.txt index a0cbf78dc..ca3732db0 100644 --- a/CMakeLists.txt +++ b/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}") diff --git a/README_MIP.txt b/README_MIP.txt index 7c5021719..8f773d7ae 100644 --- a/README_MIP.txt +++ b/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 diff --git a/include/minizinc/copy.hh b/include/minizinc/copy.hh index 45d99296b..c49a3c7d9 100644 --- a/include/minizinc/copy.hh +++ b/include/minizinc/copy.hh @@ -18,8 +18,10 @@ namespace MiniZinc { class CopyMap { protected: - typedef UNORDERED_NAMESPACE::unordered_map MyMap; - MyMap m; + typedef UNORDERED_NAMESPACE::unordered_map 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 void insert(ASTExprVec e0, ASTExprVec e1) { - m.insert(std::pair(e0.vec(),e1.vec())); + node_m.insert(e0.vec(),e1.vec()); } template ASTExprVecO* find(ASTExprVec e) { - MyMap::iterator it = m.find(e.vec()); - if (it==m.end()) return NULL; - return static_cast*>(it->second); + ASTNode* n = node_m.find(e.vec()); + return static_cast*>(n); } }; diff --git a/include/minizinc/gc.hh b/include/minizinc/gc.hh index c3bcc3c7f..68856a673 100644 --- a/include/minizinc/gc.hh +++ b/include/minizinc/gc.hh @@ -15,6 +15,7 @@ #include #include #include +#include namespace MiniZinc { @@ -109,6 +110,8 @@ namespace MiniZinc { class KeepAlive; class WeakRef; + class ASTNodeWeakMap; + /// Garbage collector class GC { friend class ASTNode; @@ -116,6 +119,7 @@ namespace MiniZinc { 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 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 diff --git a/include/minizinc/solvers/MIP/MIP_wrap.hh b/include/minizinc/solvers/MIP/MIP_wrap.hh index 70cfc3b55..349be096e 100644 --- a/include/minizinc/solvers/MIP/MIP_wrap.hh +++ b/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 sLitValues; std::unordered_map 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) { diff --git a/include/minizinc/values.hh b/include/minizinc/values.hh index 1d75bef47..a4a59e77e 100644 --- a/include/minizinc/values.hh +++ b/include/minizinc/values.hh @@ -692,8 +692,12 @@ namespace MiniZinc { template std::basic_ostream& operator <<(std::basic_ostream& 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; } diff --git a/lib/ast.cpp b/lib/ast.cpp index 51842142a..da2cc81fc 100644 --- a/lib/ast.cpp +++ b/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(); } diff --git a/lib/copy.cpp b/lib/copy.cpp index 150b52604..708f58c22 100644 --- a/lib/copy.cpp +++ b/lib/copy.cpp @@ -15,52 +15,43 @@ namespace MiniZinc { void CopyMap::insert(Expression* e0, Expression* e1) { - m.insert(std::pair(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(it->second); + return static_cast(node_m.find(e)); } void CopyMap::insert(Item* e0, Item* e1) { - m.insert(std::pair(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(it->second); + return static_cast(node_m.find(e)); } void CopyMap::insert(Model* e0, Model* e1) { - m.insert(std::pair(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(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(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(it->second); + return static_cast(node_m.find(e.aststr())); } void CopyMap::insert(IntSetVal* e0, IntSetVal* e1) { - m.insert(std::pair(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(it->second); + return static_cast(node_m.find(e)); } void CopyMap::insert(FloatSetVal* e0, FloatSetVal* e1) { - m.insert(std::pair(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(it->second); + return static_cast(node_m.find(e)); } Location copy_location(CopyMap& m, const Location& _loc) { diff --git a/lib/eval_par.cpp b/lib/eval_par.cpp index 9bad547f7..5a509ce0b 100644 --- a/lib/eval_par.cpp +++ b/lib/eval_par.cpp @@ -813,248 +813,253 @@ namespace MiniZinc { } bool eval_bool(EnvI& env, Expression* e) { - if (BoolLit* bl = e->dyn_cast()) { - return bl->v(); - } - CallStackItem csi(env,e); - switch (e->eid()) { - case Expression::E_INTLIT: - case Expression::E_FLOATLIT: - case Expression::E_STRINGLIT: - case Expression::E_ANON: - case Expression::E_TIID: - case Expression::E_SETLIT: - case Expression::E_ARRAYLIT: - case Expression::E_COMP: - case Expression::E_VARDECL: - case Expression::E_TI: - assert(false); - throw EvalError(env, e->loc(),"not a bool expression"); - break; - case Expression::E_ID: - { - GCLock lock; - return eval_id(env,e)->v(); - } - break; - case Expression::E_ARRAYACCESS: - { - GCLock lock; - return eval_bool(env,eval_arrayaccess(env,e->cast())); + try { + if (BoolLit* bl = e->dyn_cast()) { + return bl->v(); } - break; - case Expression::E_ITE: - { - ITE* ite = e->cast(); - for (int i=0; isize(); i++) { - if (eval_bool(env,ite->e_if(i))) - return eval_bool(env,ite->e_then(i)); + CallStackItem csi(env,e); + switch (e->eid()) { + case Expression::E_INTLIT: + case Expression::E_FLOATLIT: + case Expression::E_STRINGLIT: + case Expression::E_ANON: + case Expression::E_TIID: + case Expression::E_SETLIT: + case Expression::E_ARRAYLIT: + case Expression::E_COMP: + case Expression::E_VARDECL: + case Expression::E_TI: + assert(false); + throw EvalError(env, e->loc(),"not a bool expression"); + break; + case Expression::E_ID: + { + GCLock lock; + return eval_id(env,e)->v(); } - return eval_bool(env,ite->e_else()); - } - break; - case Expression::E_BINOP: - { - BinOp* bo = e->cast(); - Expression* lhs = bo->lhs(); - Expression* rhs = bo->rhs(); - if ( bo->op()==BOT_EQ && (lhs->type().isopt() || rhs->type().isopt()) ) { - if (lhs == constants().absent || rhs==constants().absent) - return lhs==rhs; + break; + case Expression::E_ARRAYACCESS: + { + GCLock lock; + return eval_bool(env,eval_arrayaccess(env,e->cast())); } - if (lhs->type().isbool() && rhs->type().isbool()) { - try { - switch (bo->op()) { - case BOT_LE: return eval_bool(env,lhs)eval_bool(env,rhs); - case BOT_GQ: return eval_bool(env,lhs)>=eval_bool(env,rhs); - case BOT_EQ: return eval_bool(env,lhs)==eval_bool(env,rhs); - case BOT_NQ: return eval_bool(env,lhs)!=eval_bool(env,rhs); - case BOT_EQUIV: return eval_bool(env,lhs)==eval_bool(env,rhs); - case BOT_IMPL: return (!eval_bool(env,lhs))||eval_bool(env,rhs); - case BOT_RIMPL: return (!eval_bool(env,rhs))||eval_bool(env,lhs); - case BOT_OR: return eval_bool(env,lhs)||eval_bool(env,rhs); - case BOT_AND: return eval_bool(env,lhs)&&eval_bool(env,rhs); - case BOT_XOR: return eval_bool(env,lhs)^eval_bool(env,rhs); - default: - assert(false); - throw EvalError(env, e->loc(),"not a bool expression", bo->opToString()); - } - } catch (ResultUndefinedError&) { - return false; + break; + case Expression::E_ITE: + { + ITE* ite = e->cast(); + for (int i=0; isize(); i++) { + if (eval_bool(env,ite->e_if(i))) + return eval_bool(env,ite->e_then(i)); } - } else if (lhs->type().isint() && rhs->type().isint()) { - try { - IntVal v0 = eval_int(env,lhs); - IntVal v1 = eval_int(env,rhs); - switch (bo->op()) { - case BOT_LE: return v0v1; - case BOT_GQ: return v0>=v1; - case BOT_EQ: return v0==v1; - case BOT_NQ: return v0!=v1; - default: - assert(false); - throw EvalError(env, e->loc(),"not a bool expression", bo->opToString()); - } - } catch (ResultUndefinedError&) { - return false; + return eval_bool(env,ite->e_else()); + } + break; + case Expression::E_BINOP: + { + BinOp* bo = e->cast(); + Expression* lhs = bo->lhs(); + Expression* rhs = bo->rhs(); + if ( bo->op()==BOT_EQ && (lhs->type().isopt() || rhs->type().isopt()) ) { + if (lhs == constants().absent || rhs==constants().absent) + return lhs==rhs; } - } else if (lhs->type().isfloat() && rhs->type().isfloat()) { - try { - FloatVal v0 = eval_float(env,lhs); - FloatVal v1 = eval_float(env,rhs); - switch (bo->op()) { - case BOT_LE: return v0v1; - case BOT_GQ: return v0>=v1; - case BOT_EQ: return v0==v1; - case BOT_NQ: return v0!=v1; + if (lhs->type().isbool() && rhs->type().isbool()) { + try { + switch (bo->op()) { + case BOT_LE: return eval_bool(env,lhs)eval_bool(env,rhs); + case BOT_GQ: return eval_bool(env,lhs)>=eval_bool(env,rhs); + case BOT_EQ: return eval_bool(env,lhs)==eval_bool(env,rhs); + case BOT_NQ: return eval_bool(env,lhs)!=eval_bool(env,rhs); + case BOT_EQUIV: return eval_bool(env,lhs)==eval_bool(env,rhs); + case BOT_IMPL: return (!eval_bool(env,lhs))||eval_bool(env,rhs); + case BOT_RIMPL: return (!eval_bool(env,rhs))||eval_bool(env,lhs); + case BOT_OR: return eval_bool(env,lhs)||eval_bool(env,rhs); + case BOT_AND: return eval_bool(env,lhs)&&eval_bool(env,rhs); + case BOT_XOR: return eval_bool(env,lhs)^eval_bool(env,rhs); default: assert(false); throw EvalError(env, e->loc(),"not a bool expression", bo->opToString()); + } + } catch (ResultUndefinedError&) { + return false; } - } catch (ResultUndefinedError&) { - return false; - } - } else if (lhs->type().isint() && rhs->type().isintset()) { - try { - IntVal v0 = eval_int(env,lhs); - GCLock lock; - IntSetVal* v1 = eval_intset(env,rhs); - switch (bo->op()) { - case BOT_IN: return v1->contains(v0); - default: - assert(false); - throw EvalError(env, e->loc(),"not a bool expression", bo->opToString()); + } else if (lhs->type().isint() && rhs->type().isint()) { + try { + IntVal v0 = eval_int(env,lhs); + IntVal v1 = eval_int(env,rhs); + switch (bo->op()) { + case BOT_LE: return v0v1; + case BOT_GQ: return v0>=v1; + case BOT_EQ: return v0==v1; + case BOT_NQ: return v0!=v1; + default: + assert(false); + throw EvalError(env, e->loc(),"not a bool expression", bo->opToString()); + } + } catch (ResultUndefinedError&) { + return false; } - } catch (ResultUndefinedError&) { - return false; - } - } else if (lhs->type().isfloat() && rhs->type().isfloatset()) { - try { - FloatVal v0 = eval_float(env,lhs); - GCLock lock; - FloatSetVal* v1 = eval_floatset(env,rhs); - switch (bo->op()) { + } else if (lhs->type().isfloat() && rhs->type().isfloat()) { + try { + FloatVal v0 = eval_float(env,lhs); + FloatVal v1 = eval_float(env,rhs); + switch (bo->op()) { + case BOT_LE: return v0v1; + case BOT_GQ: return v0>=v1; + case BOT_EQ: return v0==v1; + case BOT_NQ: return v0!=v1; + default: + assert(false); + throw EvalError(env, e->loc(),"not a bool expression", bo->opToString()); + } + } catch (ResultUndefinedError&) { + return false; + } + } else if (lhs->type().isint() && rhs->type().isintset()) { + try { + IntVal v0 = eval_int(env,lhs); + GCLock lock; + IntSetVal* v1 = eval_intset(env,rhs); + switch (bo->op()) { case BOT_IN: return v1->contains(v0); default: assert(false); throw EvalError(env, e->loc(),"not a bool expression", bo->opToString()); + } + } catch (ResultUndefinedError&) { + return false; } - } catch (ResultUndefinedError&) { - return false; - } - } else if (lhs->type().is_set() && rhs->type().is_set()) { - try { - GCLock lock; - IntSetVal* v0 = eval_intset(env,lhs); - IntSetVal* v1 = eval_intset(env,rhs); - IntSetRanges ir0(v0); - IntSetRanges ir1(v1); - switch (bo->op()) { - case BOT_LE: return Ranges::less(ir0,ir1); - case BOT_LQ: return Ranges::lessEq(ir0,ir1); - case BOT_GR: return Ranges::less(ir1,ir0); - case BOT_GQ: return Ranges::lessEq(ir1,ir0); - case BOT_EQ: return Ranges::equal(ir0,ir1); - case BOT_NQ: return !Ranges::equal(ir0,ir1); - case BOT_SUBSET: return Ranges::subset(ir0,ir1); - case BOT_SUPERSET: return Ranges::subset(ir1,ir0); - default: - throw EvalError(env, e->loc(),"not a bool expression", bo->opToString()); + } else if (lhs->type().isfloat() && rhs->type().isfloatset()) { + try { + FloatVal v0 = eval_float(env,lhs); + GCLock lock; + FloatSetVal* v1 = eval_floatset(env,rhs); + switch (bo->op()) { + case BOT_IN: return v1->contains(v0); + default: + assert(false); + throw EvalError(env, e->loc(),"not a bool expression", bo->opToString()); + } + } catch (ResultUndefinedError&) { + return false; } - } catch (ResultUndefinedError&) { - return false; - } - } else if (lhs->type().isstring() && rhs->type().isstring()) { - try { - GCLock lock; - std::string s0 = eval_string(env,lhs); - std::string s1 = eval_string(env,rhs); - switch (bo->op()) { - case BOT_EQ: return s0==s1; - case BOT_NQ: return s0!=s1; - case BOT_LE: return s0s1; - case BOT_GQ: return s0>=s1; + } else if (lhs->type().is_set() && rhs->type().is_set()) { + try { + GCLock lock; + IntSetVal* v0 = eval_intset(env,lhs); + IntSetVal* v1 = eval_intset(env,rhs); + IntSetRanges ir0(v0); + IntSetRanges ir1(v1); + switch (bo->op()) { + case BOT_LE: return Ranges::less(ir0,ir1); + case BOT_LQ: return Ranges::lessEq(ir0,ir1); + case BOT_GR: return Ranges::less(ir1,ir0); + case BOT_GQ: return Ranges::lessEq(ir1,ir0); + case BOT_EQ: return Ranges::equal(ir0,ir1); + case BOT_NQ: return !Ranges::equal(ir0,ir1); + case BOT_SUBSET: return Ranges::subset(ir0,ir1); + case BOT_SUPERSET: return Ranges::subset(ir1,ir0); default: throw EvalError(env, e->loc(),"not a bool expression", bo->opToString()); + } + } catch (ResultUndefinedError&) { + return false; } - } catch (ResultUndefinedError&) { - return false; - } - } else if (bo->op()==BOT_EQ && lhs->type().isann()) { - return Expression::equal(lhs, rhs); - } else if (bo->op()==BOT_EQ && lhs->type().dim() > 0 && - rhs->type().dim() > 0) { - try { - ArrayLit* al0 = eval_array_lit(env,lhs); - ArrayLit* al1 = eval_array_lit(env,rhs); - if (al0->v().size() != al1->v().size()) + } else if (lhs->type().isstring() && rhs->type().isstring()) { + try { + GCLock lock; + std::string s0 = eval_string(env,lhs); + std::string s1 = eval_string(env,rhs); + switch (bo->op()) { + case BOT_EQ: return s0==s1; + case BOT_NQ: return s0!=s1; + case BOT_LE: return s0s1; + case BOT_GQ: return s0>=s1; + default: + throw EvalError(env, e->loc(),"not a bool expression", bo->opToString()); + } + } catch (ResultUndefinedError&) { return false; - for (unsigned int i=0; iv().size(); i++) { - if (!Expression::equal(eval_par(env,al0->v()[i]), eval_par(env,al1->v()[i]))) { + } + } else if (bo->op()==BOT_EQ && lhs->type().isann()) { + return Expression::equal(lhs, rhs); + } else if (bo->op()==BOT_EQ && lhs->type().dim() > 0 && + rhs->type().dim() > 0) { + try { + ArrayLit* al0 = eval_array_lit(env,lhs); + ArrayLit* al1 = eval_array_lit(env,rhs); + if (al0->v().size() != al1->v().size()) return false; + for (unsigned int i=0; iv().size(); i++) { + if (!Expression::equal(eval_par(env,al0->v()[i]), eval_par(env,al1->v()[i]))) { + return false; + } } + return true; + } catch (ResultUndefinedError&) { + return false; } - return true; - } catch (ResultUndefinedError&) { - return false; + } else { + throw EvalError(env, e->loc(), "not a bool expression", bo->opToString()); } - } else { - throw EvalError(env, e->loc(), "not a bool expression", bo->opToString()); } - } - break; - case Expression::E_UNOP: - { - UnOp* uo = e->cast(); - bool v0 = eval_bool(env,uo->e()); - switch (uo->op()) { - case UOT_NOT: return !v0; - default: - assert(false); - throw EvalError(env, e->loc(),"not a bool expression", uo->opToString()); + break; + case Expression::E_UNOP: + { + UnOp* uo = e->cast(); + bool v0 = eval_bool(env,uo->e()); + switch (uo->op()) { + case UOT_NOT: return !v0; + default: + assert(false); + throw EvalError(env, e->loc(),"not a bool expression", uo->opToString()); + } } - } - break; - case Expression::E_CALL: - { - try { - Call* ce = e->cast(); - if (ce->decl()==NULL) - throw EvalError(env, e->loc(), "undeclared function", ce->id()); - - if (ce->decl()->_builtins.b) - return ce->decl()->_builtins.b(env,ce); + break; + case Expression::E_CALL: + { + try { + Call* ce = e->cast(); + if (ce->decl()==NULL) + throw EvalError(env, e->loc(), "undeclared function", ce->id()); + + if (ce->decl()->_builtins.b) + return ce->decl()->_builtins.b(env,ce); - if (ce->decl()->_builtins.e) - return eval_bool(env,ce->decl()->_builtins.e(env,ce)); + if (ce->decl()->_builtins.e) + return eval_bool(env,ce->decl()->_builtins.e(env,ce)); - if (ce->decl()->e()==NULL) - throw EvalError(env, ce->loc(), "internal error: missing builtin '"+ce->id().str()+"'"); - - return eval_call(env,ce); - } catch (ResultUndefinedError&) { - return false; + if (ce->decl()->e()==NULL) + throw EvalError(env, ce->loc(), "internal error: missing builtin '"+ce->id().str()+"'"); + + return eval_call(env,ce); + } catch (ResultUndefinedError&) { + return false; + } } + break; + case Expression::E_LET: + { + Let* l = e->cast(); + l->pushbindings(); + bool ret = eval_bool(env,l->in()); + l->popbindings(); + return ret; + } + break; + default: assert(false); return false; } - break; - case Expression::E_LET: - { - Let* l = e->cast(); - l->pushbindings(); - bool ret = eval_bool(env,l->in()); - l->popbindings(); - return ret; - } - break; - default: assert(false); return false; + } catch (ResultUndefinedError&) { + // undefined means false + return false; } } diff --git a/lib/flatten.cpp b/lib/flatten.cpp index 337b2d471..185a6d962 100644 --- a/lib/flatten.cpp +++ b/lib/flatten.cpp @@ -391,8 +391,9 @@ namespace MiniZinc { return false; } if (strictEnums && t1.dim() > 0 && t1.enumId() != t2.enumId()) { - if (t1.enumId()==0) - return false; + if (t1.enumId()==0) { + return t1.isbot(); + } if (t2.enumId()!=0) { const std::vector& t1enumIds = getArrayEnum(t1.enumId()); const std::vector& t2enumIds = getArrayEnum(t2.enumId()); @@ -401,7 +402,7 @@ namespace MiniZinc { if (t2enumIds[i] != 0 && t1enumIds[i] != t2enumIds[i]) return false; } - if (t2enumIds[t1enumIds.size()-1]!=0 && t1enumIds[t1enumIds.size()-1]!=t2enumIds[t2enumIds.size()-1]) + if (!t1.isbot() && t2enumIds[t1enumIds.size()-1]!=0 && t1enumIds[t1enumIds.size()-1]!=t2enumIds[t2enumIds.size()-1]) return false; } } @@ -1152,11 +1153,22 @@ namespace MiniZinc { Expression* ret = e; if (e==NULL || (e->type().ispar() && e->type().isbool())) { GCLock lock; - if (e==NULL || eval_bool(env,e)) { - vd->e(constants().lit_true); - } else { - vd->e(constants().lit_false); + bool isTrue = (e==NULL || eval_bool(env,e)); + + // Check if redefinition of bool_eq exists, if yes call it + std::vector args(2); + args[0] = vd->id(); + args[1] = constants().boollit(isTrue); + Call* c = new Call(Location().introduce(),constants().ids.bool_eq,args); + c->decl(env.orig->matchFn(env,c,false)); + c->type(c->decl()->rtype(env,args,false)); + bool didRewrite = false; + if (c->decl()->e()) { + flat_exp(env, Ctx(), c, constants().var_true, constants().var_true); + didRewrite = true; } + + vd->e(constants().boollit(isTrue)); if (vd->ti()->domain()) { if (vd->ti()->domain() != vd->e()) { env.fail(); @@ -1166,16 +1178,9 @@ namespace MiniZinc { vd->ti()->domain(vd->e()); vd->ti()->setComputedDomain(true); } - std::vector args(2); - args[0] = vd->id(); - args[1] = vd->e(); - Call* c = new Call(Location().introduce(),constants().ids.bool_eq,args); - c->decl(env.orig->matchFn(env,c,false)); - c->type(c->decl()->rtype(env,args,false)); - if (c->decl()->e()) { - flat_exp(env, Ctx(), c, constants().var_true, constants().var_true); + if (didRewrite) { return vd->id(); - } + } } else { if (e->type().dim() > 0) { // Check that index sets match @@ -3949,15 +3954,15 @@ namespace MiniZinc { nctx.neg = negArgs; nctx.b = negArgs ? C_NEG : C_ROOT; std::vector todo; - todo.push_back(boe0); todo.push_back(boe1); + todo.push_back(boe0); while (!todo.empty()) { Expression* e_todo = todo.back(); todo.pop_back(); BinOp* e_bo = e_todo->dyn_cast(); if (e_bo && e_bo->op()==BOT_AND) { - todo.push_back(e_bo->lhs()); todo.push_back(e_bo->rhs()); + todo.push_back(e_bo->lhs()); } else { (void) flat_exp(env,nctx,e_todo,constants().var_true,constants().var_true); } @@ -4270,6 +4275,7 @@ namespace MiniZinc { if (ctx.b==C_ROOT && r==constants().var_true && e1.r()->type().ispar() && e0.r()->isa() && (bot==BOT_IN || bot==BOT_SUBSET) ) { + /// TODO: check for float VarDecl* vd = e0.r()->cast()->decl(); if (vd->ti()->domain()==NULL) { vd->ti()->domain(e1.r()); @@ -4297,6 +4303,9 @@ namespace MiniZinc { } else if (changeDom) { id->decl()->ti()->setComputedDomain(false); id->decl()->ti()->domain(new SetLit(Location().introduce(),newdom)); + if (id->decl()->e()==NULL && newdom->min()==newdom->max()) { + id->decl()->e(IntLit::a(newdom->min())); + } } id = id->decl()->e() ? id->decl()->e()->dyn_cast() : NULL; } diff --git a/lib/gc.cpp b/lib/gc.cpp index b1594b7f5..ed8afda36 100644 --- a/lib/gc.cpp +++ b/lib/gc.cpp @@ -93,6 +93,7 @@ namespace MiniZinc { Model* _rootset; KeepAlive* _roots; WeakRef* _weakRefs; + ASTNodeWeakMap* _nodeWeakMaps; static const int _max_fl = 5; FreeListNode* _fl[_max_fl+1]; static const size_t _fl_size[_max_fl+1]; @@ -133,6 +134,7 @@ namespace MiniZinc { , _rootset(NULL) , _roots(NULL) , _weakRefs(NULL) + , _nodeWeakMaps(NULL) , _alloced_mem(0) , _free_mem(0) , _gc_threshold(10) @@ -501,6 +503,17 @@ namespace MiniZinc { fixPrev = true; } } + + for (ASTNodeWeakMap* wr = _nodeWeakMaps; wr != NULL; wr = wr->next()) { + std::vector toRemove; + for (auto n : wr->_m) { + if (n.first->_gc_mark==0 || n.second->_gc_mark==0) + toRemove.push_back(n.first); + } + for (auto n : toRemove) { + wr->_m.erase(n); + } + } #if defined(MINIZINC_GC_STATS) std::cerr << "+"; @@ -727,6 +740,27 @@ namespace MiniZinc { e->_n->_p = e->_p; } } + void + GC::addNodeWeakMap(ASTNodeWeakMap* m) { + assert(m->_p==NULL); + assert(m->_n==NULL); + m->_n = GC::gc()->_heap->_nodeWeakMaps; + if (GC::gc()->_heap->_nodeWeakMaps) + GC::gc()->_heap->_nodeWeakMaps->_p = m; + GC::gc()->_heap->_nodeWeakMaps = m; + } + void + GC::removeNodeWeakMap(ASTNodeWeakMap* m) { + if (m->_p) { + m->_p->_n = m->_n; + } else { + assert(GC::gc()->_heap->_nodeWeakMaps==m); + GC::gc()->_heap->_nodeWeakMaps = m->_n; + } + if (m->_n) { + m->_n->_p = m->_p; + } + } WeakRef::WeakRef(Expression* e) : _e(e), _p(NULL), _n(NULL), _valid(true) { @@ -757,4 +791,25 @@ namespace MiniZinc { return *this; } + ASTNodeWeakMap::ASTNodeWeakMap(void) + : _p(NULL), _n(NULL) { + GC::gc()->addNodeWeakMap(this); + } + + ASTNodeWeakMap::~ASTNodeWeakMap(void) { + GC::gc()->removeNodeWeakMap(this); + } + + void + ASTNodeWeakMap::insert(ASTNode* n0, ASTNode* n1) { + _m.insert(std::make_pair(n0,n1)); + } + + ASTNode* + ASTNodeWeakMap::find(ASTNode* n) { + NodeMap::iterator it = _m.find(n); + if (it==_m.end()) return NULL; + return it->second; + } + } diff --git a/lib/optimize.cpp b/lib/optimize.cpp index b62d2577f..7c4a47e2b 100644 --- a/lib/optimize.cpp +++ b/lib/optimize.cpp @@ -610,23 +610,27 @@ namespace MiniZinc { Item* item = constraintQueue.back(); constraintQueue.pop_back(); Call* c; - ArrayLit* al; + ArrayLit* al = NULL; if (ConstraintI* ci = item->dyn_cast()) { ci->flag(false); c = Expression::dyn_cast(ci->e()); - al = NULL; } else { + if (item->removed()) { + item = m[envi.vo.find(item->cast()->e()->id()->decl())]->cast(); + } item->cast()->flag(false); c = Expression::dyn_cast(item->cast()->e()->e()); al = Expression::dyn_cast(item->cast()->e()->e()); } - if (al) { - substituteFixedVars(envi, item, deletedVarDecls); - pushDependentConstraints(envi, item->cast()->e()->id(), constraintQueue); - } else if (!c || !(c->id()==constants().ids.forall || c->id()==constants().ids.exists || - c->id()==constants().ids.clause) ) { - substituteFixedVars(envi, item, deletedVarDecls); - handledConstraint = simplifyConstraint(envi,item,deletedVarDecls,constraintQueue,vardeclQueue); + if (!item->removed()) { + if (al) { + substituteFixedVars(envi, item, deletedVarDecls); + pushDependentConstraints(envi, item->cast()->e()->id(), constraintQueue); + } else if (!c || !(c->id()==constants().ids.forall || c->id()==constants().ids.exists || + c->id()==constants().ids.clause) ) { + substituteFixedVars(envi, item, deletedVarDecls); + handledConstraint = simplifyConstraint(envi,item,deletedVarDecls,constraintQueue,vardeclQueue); + } } } } diff --git a/lib/prettyprinter.cpp b/lib/prettyprinter.cpp index 1022fff15..cd5d7ae41 100644 --- a/lib/prettyprinter.cpp +++ b/lib/prettyprinter.cpp @@ -323,7 +323,7 @@ namespace MiniZinc { if (id->idn() == -1) { os << id->v(); } else { - os << "X_INTRODUCED_" << id->idn(); + os << "X_INTRODUCED_" << id->idn() << "_"; } } } @@ -570,7 +570,7 @@ namespace MiniZinc { const VarDecl& vd = *e->cast(); p(vd.ti()); if (vd.id()->idn() != -1) { - os << ": X_INTRODUCED_" << vd.id()->idn(); + os << ": X_INTRODUCED_" << vd.id()->idn() << "_"; } else if (vd.id()->v().size() != 0) os << ": " << vd.id()->v(); if (vd.introduced()) { @@ -1181,7 +1181,7 @@ namespace MiniZinc { return new StringDocument(id.v().str()); else { std::ostringstream oss; - oss << "X_INTRODUCED_" << id.idn(); + oss << "X_INTRODUCED_" << id.idn() << "_"; return new StringDocument(oss.str()); } } @@ -1515,7 +1515,7 @@ namespace MiniZinc { dl->addStringToList(vd.id()->v().str()); } else { std::ostringstream oss; - oss << "X_INTRODUCED_" << vd.id()->idn(); + oss << "X_INTRODUCED_" << vd.id()->idn() << "_"; dl->addStringToList(oss.str()); } diff --git a/lib/solver_instance_base.cpp b/lib/solver_instance_base.cpp index ebbf8b7a8..e9f618030 100644 --- a/lib/solver_instance_base.cpp +++ b/lib/solver_instance_base.cpp @@ -139,7 +139,11 @@ namespace MiniZinc { std::vector > dims_v; for( int i=0;ilength();i++) { IntSetVal* isv = eval_intset(getEnv()->envi(), dims->v()[i]); - dims_v.push_back(std::pair(isv->min(0).toInt(),isv->max(isv->size()-1).toInt())); + if (isv->size()==0) { + dims_v.push_back(std::pair(1,0)); + } else { + dims_v.push_back(std::pair(isv->min().toInt(),isv->max().toInt())); + } } ArrayLit* array_solution = new ArrayLit(Location(),array_elems,dims_v); KeepAlive ka(array_solution); diff --git a/share/minizinc/linear/cumulative.mzn b/share/minizinc/linear/cumulative.mzn index d0913bda4..549df440f 100644 --- a/share/minizinc/linear/cumulative.mzn +++ b/share/minizinc/linear/cumulative.mzn @@ -19,17 +19,19 @@ predicate cumulative(array[int] of var int: s, if mzn_in_redundant_constraint() /\ fMZN__IgnoreRedundantCumulative then true else - let { - set of int: tasks = - {i | i in index_set(s) where ub(r[i]) > 0 /\ ub(d[i]) > 0 }, - set of int: times = dom_array( [ s[i] | i in tasks ] ) - } in -% my_trace(" cumul: times = " ++ show(times)) /\ - if nMZN__UnarySizeMax_cumul>=card(times)*card(tasks) then %%% -- Mem overflow on rcmsp. PARAMETER? TODO - cumulative_time_decomp(s, d, r, b, times) - else - cumulative_task_decomp(s, d, r, b) - endif + let { + set of int: tasks = + {i | i in index_set(s) where ub(r[i]) > 0 /\ ub(d[i]) > 0 }, + set of int: times = dom_array( [ s[i] | i in tasks ] ) + } in + if 0==card(tasks) then /*true*/ 0==card(index_set(s)) \/ b>=0 + else + if nMZN__UnarySizeMax_cumul>=card(times)*card(tasks) then %%% -- Mem overflow on rcmsp. PARAMETER? TODO + cumulative_time_decomp(s, d, r, b, times) + else + cumulative_task_decomp(s, d, r, b) + endif + endif endif )); diff --git a/share/minizinc/linear/redefinitions.mzn b/share/minizinc/linear/redefinitions.mzn index bd2294e7e..fe799514e 100644 --- a/share/minizinc/linear/redefinitions.mzn +++ b/share/minizinc/linear/redefinitions.mzn @@ -299,6 +299,13 @@ predicate int_times_unary__NOFN(var int: x, set of int: domx__, var int: y, var ( pY[valY[j]] == sum(i in index_set(valX))( pp[i, j] ) ) endif; +%%%Define int_pow +predicate int_pow( var int: x, var int: y, var int: r ) = + let { + array[ int, int ] of int: x2y = array2d( lb(x)..ub(x), lb(y)..ub(y), + [ pow( X, Y ) | X in lb(x)..ub(x), Y in lb(y)..ub(y) ] ) + } in + r == x2y[ x, y ]; %-----------------------------------------------------------------------------% % Array 'element' constraints diff --git a/share/minizinc/std/builtins.mzn b/share/minizinc/std/builtins.mzn index 081f0872f..bcc0e6790 100644 --- a/share/minizinc/std/builtins.mzn +++ b/share/minizinc/std/builtins.mzn @@ -1492,7 +1492,7 @@ predicate bool_xor_reif(var bool: a, var bool: b, var bool: c) = bool_xor(a,b,c); predicate xorall_reif(array[int] of var bool: b, var bool: c) = - xorall([not c]++b); + let { var bool: nc ::is_defined_var; constraint xorall([nc]++b) ::defines_var(nc); } in c = not nc; function var int: lin_exp(array[int] of int, array[int] of var int, int); function var float: lin_exp(array[int] of float, array[int] of var float, float); diff --git a/share/minizinc/std/cumulative.mzn b/share/minizinc/std/cumulative.mzn index 4fe14c041..d5c2bee1a 100644 --- a/share/minizinc/std/cumulative.mzn +++ b/share/minizinc/std/cumulative.mzn @@ -26,16 +26,21 @@ predicate cumulative(array[int] of var int: s, else let { set of int: Tasks = - {i | i in index_set(s) where ub(r[i]) > 0 /\ ub(d[i]) > 0 }, - int: early = min([ lb(s[i]) | i in Tasks ]), - int: late = max([ ub(s[i]) + ub(d[i]) | i in Tasks ]) - } in ( - if late - early > 5000 then - cumulative_task(s, d, r, b) + {i | i in index_set(s) where ub(r[i]) > 0 /\ ub(d[i]) > 0 } + } in + if 0==card(Tasks) then /*true*/ 0==card(index_set(s)) \/ b>=0 else - cumulative_time(s, d, r, b) + let { + int: early = min([ lb(s[i]) | i in Tasks ]), + int: late = max([ ub(s[i]) + ub(d[i]) | i in Tasks ]) + } in ( + if late - early > 5000 then + cumulative_task(s, d, r, b) + else + cumulative_time(s, d, r, b) + endif + ) endif - ) endif )); diff --git a/solvers/MIP/MIP_cplex_wrap.cpp b/solvers/MIP/MIP_cplex_wrap.cpp index 8041f2e9a..70506c207 100644 --- a/solvers/MIP/MIP_cplex_wrap.cpp +++ b/solvers/MIP/MIP_cplex_wrap.cpp @@ -62,8 +62,8 @@ void MIP_WrapperFactory::printHelp(ostream& os) { << "--writeParam write CPLEX parameters to file" << std::endl // << "--tuneParam instruct CPLEX to tune parameters instead of solving NOT IMPL" - << "--absGap absolute gap |primal-dual| to stop. Default 0.99" << std::endl - << "--relGap relative gap |primal-dual|/ to stop. Default 1e-8" << std::endl + << "--absGap absolute gap |primal-dual| to stop" << std::endl + << "--relGap relative gap |primal-dual|/ to stop. Default 1e-8, set <0 to use backend's default" << std::endl << "--intTol integrality tolerance for a variable. Default 1e-6" << std::endl // << "--objDiff objective function discretization. Default 1.0" << std::endl @@ -83,7 +83,7 @@ void MIP_WrapperFactory::printHelp(ostream& os) { static string sWriteParams; static bool flag_all_solutions = false; - static double absGap=0.99; + static double absGap=-1; static double relGap=1e-8; static double intTol=1e-6; static double objDiff=1.0; @@ -551,11 +551,13 @@ void msgfunction(void *handle, const char *msg_string) void MIP_cplex_wrapper::solve() { // Move into ancestor? /////////////// Last-minute solver options ////////////////// + if ( flag_all_solutions && 0==nProbType ) + cerr << "WARNING. --all-solutions for SAT problems not implemented." << endl; // Before all manual params ??? - if (sReadParams.size()) { - status = CPXreadcopyparam (env, sReadParams.c_str()); - wrap_assert(!status, "Failed to read CPLEX parameters.", false); - } + if (sReadParams.size()) { + status = CPXreadcopyparam (env, sReadParams.c_str()); + wrap_assert(!status, "Failed to read CPLEX parameters.", false); + } /* Turn on output to the screen */ if (fVerbose) { @@ -601,14 +603,18 @@ void MIP_cplex_wrapper::solve() { // Move into ancestor? wrap_assert(!status, "Failed to set CPXPARAM_MIP_Limits_TreeMemory.", false); } - status = CPXsetdblparam (env, CPXPARAM_MIP_Tolerances_AbsMIPGap, absGap); - wrap_assert(!status, "Failed to set CPXPARAM_MIP_Tolerances_AbsMIPGap.", false); - - status = CPXsetdblparam (env, CPXPARAM_MIP_Tolerances_MIPGap, relGap); - wrap_assert(!status, "Failed to set CPXPARAM_MIP_Tolerances_MIPGap.", false); - - status = CPXsetdblparam (env, CPXPARAM_MIP_Tolerances_Integrality, intTol); - wrap_assert(!status, "Failed to set CPXPARAM_MIP_Tolerances_Integrality.", false); + if ( absGap>=0.0 ) { + status = CPXsetdblparam (env, CPXPARAM_MIP_Tolerances_AbsMIPGap, absGap); + wrap_assert(!status, "Failed to set CPXPARAM_MIP_Tolerances_AbsMIPGap.", false); + } + if (relGap>=0.0) { + status = CPXsetdblparam (env, CPXPARAM_MIP_Tolerances_MIPGap, relGap); + wrap_assert(!status, "Failed to set CPXPARAM_MIP_Tolerances_MIPGap.", false); + } + if (intTol>=0.0) { + status = CPXsetdblparam (env, CPXPARAM_MIP_Tolerances_Integrality, intTol); + wrap_assert(!status, "Failed to set CPXPARAM_MIP_Tolerances_Integrality.", false); + } // status = CPXsetdblparam (env, CPXPARAM_MIP_Tolerances_ObjDifference, objDiff); // wrap_assert(!status, "Failed to set CPXPARAM_MIP_Tolerances_ObjDifference.", false); diff --git a/solvers/MIP/MIP_gurobi_wrap.cpp b/solvers/MIP/MIP_gurobi_wrap.cpp index 88328976d..9356ea35b 100644 --- a/solvers/MIP/MIP_gurobi_wrap.cpp +++ b/solvers/MIP/MIP_gurobi_wrap.cpp @@ -71,8 +71,8 @@ void MIP_WrapperFactory::printHelp(ostream& os) { << "--writeParam write GUROBI parameters to file" << std::endl // << "--tuneParam instruct GUROBI to tune parameters instead of solving NOT IMPL" - << "--absGap absolute gap |primal-dual| to stop. Default 0.99" << std::endl - << "--relGap relative gap |primal-dual|/ to stop. Default 1e-8" << std::endl + << "--absGap absolute gap |primal-dual| to stop" << std::endl + << "--relGap relative gap |primal-dual|/ to stop. Default 1e-8, set <0 to use backend's default" << std::endl << "--intTol integrality tolerance for a variable. Default 1e-6" << std::endl // << "--objDiff objective function discretization. Default 1.0" << std::endl @@ -92,7 +92,7 @@ void MIP_WrapperFactory::printHelp(ostream& os) { static string sWriteParams; static bool flag_all_solutions = false; - static double absGap=0.99; + static double absGap=-1; static double relGap=1e-8; static double intTol=1e-6; static double objDiff=1.0; @@ -481,6 +481,9 @@ MIP_gurobi_wrapper::Status MIP_gurobi_wrapper::convertStatus(int gurobiStatus) void MIP_gurobi_wrapper::solve() { // Move into ancestor? + if ( flag_all_solutions && 0==nProbType ) + cerr << "WARNING. --all-solutions for SAT problems not implemented." << endl; + error = dll_GRBupdatemodel(model); // for model export wrap_assert( !error, "Failed to update model." ); @@ -538,15 +541,15 @@ void MIP_gurobi_wrapper::solve() { // Move into ancestor? // wrap_assert(!error, "Failed to set GRB_PARAM_MIP_Limits_TreeMemory.", false); // } - if ( true ) { + if ( absGap>=0.0 ) { error = dll_GRBsetdblparam( dll_GRBgetenv(model), "MIPGapAbs", absGap ); wrap_assert(!error, "Failed to set MIPGapAbs.", false); } - if ( true ) { + if ( relGap>=0.0 ) { error = dll_GRBsetdblparam( dll_GRBgetenv(model), "MIPGap", relGap ); wrap_assert(!error, "Failed to set MIPGap.", false); } - if ( true ) { + if ( intTol>=0.0 ) { error = dll_GRBsetdblparam( dll_GRBgetenv(model), "IntFeasTol", intTol ); wrap_assert(!error, "Failed to set IntFeasTol.", false); } diff --git a/solvers/MIP/MIP_osicbc_wrap.cpp b/solvers/MIP/MIP_osicbc_wrap.cpp index 1c5bdb557..a3a39a9d8 100644 --- a/solvers/MIP/MIP_osicbc_wrap.cpp +++ b/solvers/MIP/MIP_osicbc_wrap.cpp @@ -64,7 +64,7 @@ void MIP_WrapperFactory::printHelp(ostream& os) { << "--writeModel write model to (.mps)" << std::endl << "-a, --all print intermediate solutions for optimization problems\n" " (not from FeasPump. Can be slow.)" << std::endl -// << "-p use N threads, default: 1" << std::endl + << "-p use N threads, default: 1. CBC should be configured with --enable-cbc-parallel" << std::endl // << "--nomippresolve disable MIP presolving NOT IMPL" << std::endl << "--timeout stop search after N seconds" << std::endl // << "--workmem maximal amount of RAM used, MB" << std::endl @@ -72,8 +72,8 @@ void MIP_WrapperFactory::printHelp(ostream& os) { // << "--writeParam write OSICBC parameters to file" << std::endl // << "--tuneParam instruct OSICBC to tune parameters instead of solving NOT IMPL" - << "--absGap absolute gap |primal-dual| to stop. Default 0.99" << std::endl - << "--relGap relative gap |primal-dual|/ to stop. Default 1e-8" << std::endl + << "--absGap absolute gap |primal-dual| to stop" << std::endl + << "--relGap relative gap |primal-dual|/ to stop. Default 1e-8, set <0 to use backend's default" << std::endl << "--intTol integrality tolerance for a variable. Default 1e-6" << std::endl // << "--objDiff objective function discretization. Default 1.0" << std::endl @@ -95,7 +95,7 @@ void MIP_WrapperFactory::printHelp(ostream& os) { static string cbc_cmdOptions; - static double absGap=0.99; + static double absGap=-1; static double relGap=1e-8; static double intTol=1e-6; static double objDiff=1.0; @@ -657,6 +657,8 @@ MIP_osicbc_wrapper::Status MIP_osicbc_wrapper::convertStatus() void MIP_osicbc_wrapper::solve() { // Move into ancestor? + if ( flag_all_solutions && 0==nProbType ) + cerr << "WARNING. --all-solutions for SAT problems not implemented." << endl; try { /// Not using CoinPackedMatrix any more, so need to add all constraints at once: /// But this gives segf: @@ -734,10 +736,12 @@ void MIP_osicbc_wrapper::solve() { // Move into ancestor? #endif // CbcSolver control(osi); // control.solve(); - - model.setAllowableGap( absGap ); - model.setAllowableFractionGap( relGap ); - model.setIntegerTolerance( intTol ); + if ( absGap>=0.0 ) + model.setAllowableGap( absGap ); + if ( relGap>=0.0 ) + model.setAllowableFractionGap( relGap ); + if ( intTol>=0.0 ) + model.setIntegerTolerance( intTol ); // model.setCutoffIncrement( objDiff ); CoinMessageHandler msgStderr(stderr); @@ -799,6 +803,12 @@ void MIP_osicbc_wrapper::solve() { // Move into ancestor? } #endif + if ( 1 write SCIP parameters to file" << std::endl // << "--tuneParam instruct SCIP to tune parameters instead of solving NOT IMPL" - << "--absGap absolute gap |primal-dual| to stop. Default 0.99" << std::endl - << "--relGap relative gap |primal-dual|/ to stop. Default 1e-8" << std::endl -// << "--intTol integrality tolerance for a variable. Default 1e-6" << std::endl + << "--absGap absolute gap |primal-dual| to stop" << std::endl + << "--relGap relative gap |primal-dual|/ to stop. Default 1e-8, set <0 to use backend's default" << std::endl + << "--intTol integrality tolerance for a variable. Default 1e-6" << std::endl // << "--objDiff objective function discretization. Default 1.0" << std::endl << std::endl; @@ -83,7 +83,7 @@ void MIP_WrapperFactory::printHelp(ostream& os) { static string sWriteParams; static bool flag_all_solutions = false; - static double absGap=0.99; + static double absGap=-1; static double relGap=1e-8; static double intTol=1e-6; static double objDiff=1.0; @@ -408,6 +408,8 @@ SCIP_DECL_MESSAGEWARNING(printMsg) { SCIP_RETCODE MIP_scip_wrapper::solve_SCIP() { // Move into ancestor? /////////////// Last-minute solver options ////////////////// + if ( flag_all_solutions && 0==nProbType ) + cerr << "WARNING. --all-solutions for SAT problems not implemented." << endl; if (nThreads>0) SCIP_CALL( SCIPsetIntParam(scip, "lp/threads", nThreads) ); @@ -418,8 +420,12 @@ SCIP_RETCODE MIP_scip_wrapper::solve_SCIP() { // Move into ancestor? if (nWorkMemLimit>0) SCIP_CALL( SCIPsetRealParam(scip, "limits/memory", nWorkMemLimit) ); - SCIP_CALL( SCIPsetRealParam( scip, "limits/absgap", absGap ) ); - SCIP_CALL( SCIPsetRealParam( scip, "limits/gap", relGap ) ); + if ( absGap>=0.0 ) + SCIP_CALL( SCIPsetRealParam( scip, "limits/absgap", absGap ) ); + if ( relGap>=0.0 ) + SCIP_CALL( SCIPsetRealParam( scip, "limits/gap", relGap ) ); + if ( intTol>=0.0 ) + SCIP_CALL( SCIPsetRealParam( scip, "numerics/feastol", intTol ) ); // retcode = SCIP_setintparam (env, SCIP_PARAM_ClockType, 1); // CPU time // wrap_assert(!retcode, " SCIP Warning: Failure to measure CPU time.", false); diff --git a/solvers/MIP/MIP_solverinstance.cpp b/solvers/MIP/MIP_solverinstance.cpp index e61020950..46c6fba95 100644 --- a/solvers/MIP/MIP_solverinstance.cpp +++ b/solvers/MIP/MIP_solverinstance.cpp @@ -151,11 +151,25 @@ namespace SCIPConstraints { } assert(coefs.size() == vars.size()); - // See if the solver adds indexation itself: no. - std::stringstream ss; - ss << "p_lin_" << (gi.getMIPWrapper()->nAddedRows++); - gi.getMIPWrapper()->addRow(coefs.size(), &vars[0], &coefs[0], lt, rhs, - GetMaskConsType(call), ss.str()); + /// Check feas-ty + if ( coefs.empty() ) { + if ( (MIP_wrapper::LinConType::EQ==lt && 1e-5 < fabs( rhs )) + || (MIP_wrapper::LinConType::LQ==lt && -1e-5 > ( rhs )) + || (MIP_wrapper::LinConType::GQ==lt && 1e-5 < ( rhs )) + ) { + si._status = SolverInstance::UNSAT; + if ( gi.getMIPWrapper()->fVerbose ) + cerr << " Constraint '" << *call + << "' seems infeasible: simplified to 0 (rel) " << rhs + << endl; + } + } else { + // See if the solver adds indexation itself: no. + std::stringstream ss; + ss << "p_lin_" << (gi.getMIPWrapper()->nAddedRows++); + gi.getMIPWrapper()->addRow(coefs.size(), &vars[0], &coefs[0], lt, rhs, + GetMaskConsType(call), ss.str()); + } } void p_int_lin_le(SolverInstanceBase& si, const Call* call) { @@ -190,8 +204,16 @@ namespace SCIPConstraints { rhs += gi.exprToConst(args[1]); /// Check feas-ty if ( coefs.empty() ) { - if ( 1e-5 < fabs( rhs ) ) + if ( (MIP_wrapper::LinConType::EQ==nCmp && 1e-5 < fabs( rhs )) + || (MIP_wrapper::LinConType::LQ==nCmp && -1e-5 > ( rhs )) + || (MIP_wrapper::LinConType::GQ==nCmp && 1e-5 < ( rhs )) + ) { si._status = SolverInstance::UNSAT; + if ( gi.getMIPWrapper()->fVerbose ) + cerr << " Constraint '" << *call + << "' seems infeasible: simplified to 0 (rel) " << rhs + << endl; + } } else { std::stringstream ss; ss << "p_eq_" << (gi.getMIPWrapper()->nAddedRows++); @@ -325,10 +347,12 @@ SolverInstance::Status MIP_solverinstance::solve(void) { if (solveItem->st() != SolveI::SolveType::ST_SAT) { if (solveItem->st() == SolveI::SolveType::ST_MAX) { getMIPWrapper()->setObjSense(1); + getMIPWrapper()->setProbType(1); if (mip_wrap->fVerbose) cerr << " MIP_solverinstance: this is a MAXimization problem." << endl; } else { getMIPWrapper()->setObjSense(-1); + getMIPWrapper()->setProbType(-1); if (mip_wrap->fVerbose) cerr << " MIP_solverinstance: this is a MINimization problem." << endl; } @@ -337,6 +361,7 @@ SolverInstance::Status MIP_solverinstance::solve(void) { << dObjVarLB << ", " << dObjVarUB << endl; } } else { + getMIPWrapper()->setProbType(0); if (mip_wrap->fVerbose) cerr << " MIP_solverinstance: this is a SATisfiability problem." << endl; }