Patches from Simon de Givry.

fzn/fzn2py.py

@@ -30,13 +30,13 @@ def array_bool_xor(x):
 
 def array_int_element(x, y, z):
     # Buggy Workaround, produces invalid values in some optimization cases.
-    # aux = Variable(x.lb-1, x.ub-1, "somevar_minus1")
-    # return [(z == Element([Variable(e,e,str(e)) if type(e) is int else e for e in y], aux)), (x >= 1), (x <= len(y)), (aux == x - 1)]
-
+    #aux = Variable(x.lb-1, x.ub-1, "somevar_minus1")
+    #return [(z == Element([Variable(e,e,str(e)) if type(e) is int else e for e in y], aux)), (x >= 1), (x <= len(y)), (aux == x - 1)]
+    #return [(z == Element([Variable(e,e,str(e)) if type(e) is int else e for e in y], x - 1)), int_le(1,x), int_le(x,len(y))]
     u = set()
     for e in y:
         u = u | set([e] if type(e) is int else range(e.lb, e.ub + 1))
-    return [(x >= 1), (x <= len(y)), set_in(z, u)] + [((z == e) | (x != i+1)) for i, e in enumerate(y)]
+    return [int_le(1,x), int_le(x,len(y)), set_in(z, u)] + [((z == e) | (x != i+1)) for i, e in enumerate(y)]
 
 def array_var_int_element(x,y,z):
     return (array_int_element(x,y,z))
@@ -85,15 +85,15 @@ def bool_xor(x, y, z):
     return (z == (x != y))
 
 def int_eq(x,y):
-    return (x == y)
-'''
+        '''
     if (type(y) is int) and issubclass(type(x), Expression) and x.is_var() and y >= x.lb and y <= x.ub:
         x.domain_ = None
         x.lb = y
         x.ub = y
         return []
     else:
-'''
+        '''
+        return (x == y)
 
 def int_eq_reif(x,y,z):
     return (z == (x == y))
@@ -105,13 +105,31 @@ def bool_eq_reif(x, y, z):
     return (int_eq_reif(x, y, z))
 
 def int_le(x,y):
-    return (x <= y)
+        '''
+    if (type(y) is int) and issubclass(type(x), Expression) and x.is_var() and y >= x.lb: # and (x.domain_ is None)
+        x.ub = min(x.ub, y)
+        return []
+    elif (type(x) is int) and issubclass(type(y), Expression) and y.is_var() and x <= y.ub: # and (y.domain_ is None)
+        y.lb = max(y.lb, x)
+        return []
+    else:
+        '''
+        return (x <= y)
 
 def int_le_reif(x,y,z):
     return (z == (x <= y))
 
 def int_lt(x,y):
-    return (x < y)
+        '''
+    if (type(y) is int) and issubclass(type(x), Expression) and x.is_var() and y > x.lb: # and (x.domain_ is None)
+        x.ub = min(x.ub, y-1)
+        return []
+    elif (type(x) is int) and issubclass(type(y), Expression) and y.is_var() and x < y.ub: # and (y.domain_ is None)
+        y.lb = max(y.lb, x+1)
+        return []
+    else:
+        '''
+        return (x < y)
 
 def int_lt_reif(x,y,z):
     return (z == (x < y))
@@ -123,34 +141,58 @@ def int_ne_reif(x,y,z):
     return (z == (x != y))
 
 def int_lin_eq(coef,vars,res):
-    return (res == Sum(vars,coef))
+    if ((len(coef) == 1) and (coef[0] == 1)):
+       return int_eq(vars[0],res)
+    else:
+       return (res == Sum(vars,coef))
 
 def bool_lin_eq(coef,vars,res):
     return (int_lin_eq(coef,vars,res))
 
 def int_lin_eq_reif(coef,vars,res,z):
-    return (z == (res == Sum(vars, coef)))
+    if ((len(coef) == 1) and (coef[0] == 1)):
+       return int_eq_reif(vars[0],res,z)
+    else:
+       return (z == (res == Sum(vars, coef)))
 
 def int_lin_le(coef,vars,res):
-    return (res >= Sum(vars,coef))
+    if ((len(coef) == 1) and (coef[0] == 1)):
+       return int_le(vars[0],res)
+    else:
+       return (res >= Sum(vars,coef))
 
 def bool_lin_le(coef,vars,res):
     return (int_lin_le(coef,vars,res))
 
 def int_lin_le_reif(coef,vars,res,z):
-    return (z == (res >= Sum(vars,coef)))
+    if ((len(coef) == 1) and (coef[0] == 1)):
+       return int_le_reif(vars[0],res,z)
+    else:
+       return (z == (res >= Sum(vars,coef)))
 
 def int_lin_lt(coef,vars,res):
-    return (res > Sum(vars,coef))
+    if ((len(coef) == 1) and (coef[0] == 1)):
+       return int_lt(vars[0],res)
+    else:
+       return (res > Sum(vars,coef))
 
 def int_lin_lt_reif(coef,vars,res,z):
-    return (z == (res > Sum(vars,coef)))
+    if ((len(coef) == 1) and (coef[0] == 1)):
+       return int_lt_reif(vars[0],res,z)
+    else:
+       return (z == (res > Sum(vars,coef)))
 
 def int_lin_ne(coef,vars,res):
-    return (res != Sum(vars,coef))
+    if ((len(coef) == 1) and (coef[0] == 1)):
+       return int_ne(vars[0],res)
+    else:
+       return (res != Sum(vars,coef))
 
 def int_lin_ne_reif(coef,vars,res,z):
-    return (z == (res != Sum(vars,coef)))
+    if ((len(coef) == 1) and (coef[0] == 1)):
+       return int_ne_reif(vars[0],res,z)
+    else:
+       return (z == (res != Sum(vars,coef)))
 
 def int_abs(x,y):
     return (y == Abs(x))
@@ -178,6 +220,11 @@ def int_times(x,y,z):
     return (z == (x * y))
 
 def set_in(x,dom):
+    if (type(x) is int):
+        if (not(x in dom)):
+            return [Variable(x,x,str(x)) != x]
+        else:
+            return []
 #    return (Disjunction([(x == v) for v in dom]))
     return [(x != v) for v in range(x.get_min(),1+x.get_max()) if (not(v in dom))]
 '''
@@ -264,6 +311,10 @@ def run_solve(model, output_vars, param):
         solver.setOption('deadEndElimination',param['dee'])
         solver.setOption('btdMode',param['btd'])
         solver.setOption('splitClusterMaxSize',param['rds'])
+##        uncomment the following lines to save the problem in wcsp format
+#        solver.setOption('nopre')
+#        solver.setOption('lcLevel',0)
+#        solver.setOption("dumpWCSP",2)
     if param['solver'] == 'Mistral':
         solver.solveAndRestart(param['restart'], param['base'], param['factor'])
     else:

solvers/sat/src/SatWrapper.cpp

@@ -1832,7 +1832,8 @@ class TupleComparitor {
         skip one of the indices in the comparison.
     */
 public:
-    unsigned int skip_index = 0;
+    unsigned int skip_index;
+    TupleComparitor() : skip_index(0) {}
 
     bool operator()(const std::vector<int> *a, const std::vector<int> *b) const {
         for(unsigned int i=0; i<a->size() && i<b->size(); i++){

solvers/toulbar2/include/tb2globaldecomposable.hpp

@@ -215,6 +215,7 @@ class WeightedGcc : public DecomposableGlobalCostFunction{
 		void setBounds(Value value, unsigned int lb, unsigned int ub);
 
 		Cost evaluate(int* tuple) { cerr << "Not yet implemented" << endl; return 0; }
+		void rec_sum_counters(WCSP *wcsp, int *scope, int arity, int totlb, int totub, int *counters, int *lb, int *ub, int nb, int rec);
 		void addToCostFunctionNetwork(WCSP* wcsp);
 		void display(); 
 };

solvers/toulbar2/lib/src/tb2globaldecomposable.cpp

@@ -1082,19 +1082,70 @@ WeightedGcc::setBounds(Value value, unsigned int lb, unsigned int ub) {
 
 void 
 WeightedGcc::addToCostFunctionNetwork(WCSP* wcsp) {
+	int nbcounters = bounds.size();
+	int counter = 0;
+	int counters[nbcounters];
+	int clb[nbcounters];
+	int cub[nbcounters];
+	int cscope[nbcounters];
 	for (map<Value,pair <unsigned int,unsigned int> >::iterator it = bounds.begin(); it != bounds.end() ; ++it) {
 		pair<Value,pair <unsigned int,unsigned int> > bound = *it;
 
 		//Adding a wamong
 		Value value = bound.first;
 		unsigned int lb = (bound.second).first;
+		clb[counter] = lb;
 		unsigned int ub = (bound.second).second;
+		cub[counter] = ub;
 		WeightedAmong* wamong = new WeightedAmong(arity,scope);
 		wamong->setSemantics(semantics);
 		wamong->setBaseCost(baseCost);
 		wamong->addValue(value);
 		wamong->setBounds(lb,ub);
 		wamong->addToCostFunctionNetwork(wcsp);	
+		counters[counter] = wcsp->numberOfVariables() - 1;
+		counter++;
+	}
+//	if (semantics == "hard") rec_sum_counters(wcsp, cscope, 0, 0, 0, counters, clb, cub, nbcounters, 0);
+}
+
+// Special additional constraint propagation for hard decomposed GCC
+// add constraints on end-counters of wamong's decomposed GCC to enforce LB and UB for any subset of values
+void WeightedGcc::rec_sum_counters(WCSP *wcsp, int *cscope, int carity, int totlb, int totub, int *counters, int *clb, int *cub, int nb, int rec)
+{
+	if (rec==nb) {
+		if (carity==2) {
+			vector<Cost> costs(wcsp->getDomainInitSize(cscope[0]) * wcsp->getDomainInitSize(cscope[1]), wcsp->getUb());
+			for (int u=wcsp->getInf(cscope[0]); u<=wcsp->getSup(cscope[0]); u++) {
+				for (int v=wcsp->getInf(cscope[1]); v<=wcsp->getSup(cscope[1]); v++) {
+					if (u+v >= totlb && u+v <= min(totub,arity)) {
+						costs[wcsp->toIndex(cscope[0],u) * wcsp->getDomainInitSize(cscope[1]) + wcsp->toIndex(cscope[1],v)] = MIN_COST;
+					}
+				}
+			}
+			wcsp->postBinaryConstraint(cscope[0], cscope[1], costs);
+		} else if (carity==3) {
+			vector<Cost> costs(wcsp->getDomainInitSize(cscope[0]) * wcsp->getDomainInitSize(cscope[1]) * wcsp->getDomainInitSize(cscope[2]), wcsp->getUb());
+			for (int u=wcsp->getInf(cscope[0]); u<=wcsp->getSup(cscope[0]); u++) {
+				for (int v=wcsp->getInf(cscope[1]); v<=wcsp->getSup(cscope[1]); v++) {
+					for (int w=wcsp->getInf(cscope[2]); w<=wcsp->getSup(cscope[2]); w++) {
+						if (u+v+w >= totlb && u+v+w <= min(totub,arity)) {
+							costs[wcsp->toIndex(cscope[0],u) * wcsp->getDomainInitSize(cscope[1]) * wcsp->getDomainInitSize(cscope[2]) + wcsp->toIndex(cscope[1],v) * wcsp->getDomainInitSize(cscope[2]) + wcsp->toIndex(cscope[2],w)] = MIN_COST;
+						}
+					}
+				}
+			}
+			wcsp->postTernaryConstraint(cscope[0], cscope[1], cscope[2], costs);
+		} else if (carity>3) {
+			wcsp->postWSum(cscope,carity,"hard",wcsp->getUb(),">=",totlb);
+			wcsp->postWSum(cscope,carity,"hard",wcsp->getUb(),"<=",min(totub,arity));
+		}
+	} else {
+		// try without variable at position rec
+		rec_sum_counters(wcsp,cscope,carity,totlb,totub,counters,clb,cub,nb,rec+1);
+		// try with variable at position rec
+		cscope[carity]=counters[rec];
+		rec_sum_counters(wcsp,cscope,carity+1,totlb+clb[rec],totub+cub[rec],counters,clb,cub,nb,rec+1);
 	}
 }