diff --git a/cpmpy/expressions/__init__.py b/cpmpy/expressions/__init__.py index 835215800..f57ac6ffb 100644 --- a/cpmpy/expressions/__init__.py +++ b/cpmpy/expressions/__init__.py @@ -21,9 +21,9 @@ # others need to be imported by the developer explicitely from .variables import boolvar, intvar, cpm_array from .variables import BoolVar, IntVar, cparray # Old, to be deprecated -from .globalconstraints import AllDifferent, AllDifferentExcept0, AllEqual, Circuit, Inverse, Table, ShortTable, Xor, Cumulative, \ - IfThenElse, GlobalCardinalityCount, DirectConstraint, InDomain, Increasing, Decreasing, IncreasingStrict, DecreasingStrict +from .globalconstraints import AllDifferent, AllDifferentExcept0, AllDifferentLists, AllEqual, Circuit, SubCircuit, SubCircuitWithStart, Inverse, Table, ShortTable, Xor, Cumulative, \ + IfThenElse, GlobalCardinalityCount, DirectConstraint, InDomain, Increasing, Decreasing, IncreasingStrict, DecreasingStrict, LexLess, LexLessEq, LexChainLess, LexChainLessEq, Precedence, NoOverlap, NoOverlap2d from .globalconstraints import alldifferent, allequal, circuit # Old, to be deprecated -from .globalfunctions import Maximum, Minimum, Abs, Element, Count, NValue, NValueExcept +from .globalfunctions import Maximum, Minimum, Abs, Element, Count, NValue, NValueExcept, IfThenElseNum, Among from .core import BoolVal from .python_builtins import all, any, max, min, sum diff --git a/cpmpy/expressions/core.py b/cpmpy/expressions/core.py index 3d4f80224..7a343c3cf 100644 --- a/cpmpy/expressions/core.py +++ b/cpmpy/expressions/core.py @@ -71,7 +71,8 @@ from types import GeneratorType import numpy as np -from .utils import is_bool, is_num, is_any_list, flatlist, argval, get_bounds, is_boolexpr, is_true_cst, is_false_cst, is_leaf + +from .utils import is_num, is_any_list, flatlist, argval, get_bounds, is_boolexpr, is_true_cst, is_false_cst, is_leaf, argvals from ..exceptions import IncompleteFunctionError, TypeError class Expression(object): @@ -177,6 +178,7 @@ def is_leaf(self): def value(self): return None # default + def get_bounds(self): if self.is_bool(): return 0, 1 #default for boolean expressions @@ -436,7 +438,8 @@ def __repr__(self): # return the value of the expression # optional, default: None def value(self): - arg_vals = [argval(a) for a in self.args] + arg_vals = argvals(self.args) + if any(a is None for a in arg_vals): return None if self.name == "==": return arg_vals[0] == arg_vals[1] elif self.name == "!=": return arg_vals[0] != arg_vals[1] @@ -562,11 +565,12 @@ def wrap_bracket(arg): return "{}({})".format(self.name, self.args) def value(self): + if self.name == "wsum": # wsum: arg0 is list of constants, no .value() use as is - arg_vals = [self.args[0], [argval(arg) for arg in self.args[1]]] + arg_vals = [self.args[0], argvals(self.args[1])] else: - arg_vals = [argval(arg) for arg in self.args] + arg_vals = argvals(self.args) if any(a is None for a in arg_vals): return None @@ -582,7 +586,8 @@ def value(self): try: return arg_vals[0] // arg_vals[1] except ZeroDivisionError: - raise IncompleteFunctionError(f"Division by zero during value computation for expression {self}") + raise IncompleteFunctionError(f"Division by zero during value computation for expression {self}" + + "\n Use argval(expr) to get the value of expr with relational semantics.") # boolean elif self.name == "and": return all(arg_vals) diff --git a/cpmpy/expressions/globalconstraints.py b/cpmpy/expressions/globalconstraints.py index 560cde462..2d77fbc84 100644 --- a/cpmpy/expressions/globalconstraints.py +++ b/cpmpy/expressions/globalconstraints.py @@ -98,8 +98,11 @@ def my_circuit_decomp(self): AllDifferent AllDifferentExcept0 + AllDifferentLists AllEqual Circuit + SubCircuit + SubCircuitWithStart Inverse Table ShortTable @@ -121,7 +124,7 @@ def my_circuit_decomp(self): from ..exceptions import CPMpyException, IncompleteFunctionError, TypeError from .core import Expression, Operator, Comparison from .variables import boolvar, intvar, cpm_array, _NumVarImpl, _IntVarImpl -from .utils import flatlist, all_pairs, argval, is_num, eval_comparison, is_any_list, is_boolexpr, get_bounds +from .utils import flatlist, all_pairs, argval, is_num, eval_comparison, is_any_list, is_boolexpr, get_bounds, argvals from .globalfunctions import * # XXX make this file backwards compatible @@ -179,7 +182,7 @@ def decompose(self): return [var1 != var2 for var1, var2 in all_pairs(self.args)], [] def value(self): - return len(set(a.value() for a in self.args)) == len(self.args) + return len(set(argvals(self.args))) == len(self.args) class AllDifferentExcept0(GlobalConstraint): @@ -194,10 +197,36 @@ def decompose(self): return [(var1 == var2).implies(var1 == 0) for var1, var2 in all_pairs(self.args)], [] def value(self): - vals = [a.value() for a in self.args if a.value() != 0] + vals = [argval(a) for a in self.args if argval(a) != 0] return len(set(vals)) == len(vals) +class AllDifferentLists(GlobalConstraint): + """ + Ensures none of the lists given are exactly the same. + Called 'lex_alldifferent' in the global constraint catalog: + https://sofdem.github.io/gccat/gccat/Clex_alldifferent.html#uid24923 + """ + def __init__(self, lists): + if any(not is_any_list(lst) for lst in lists): + raise TypeError(f"AllDifferentLists expects a list of lists, but got {lists}") + if any(len(lst) != len(lists[0]) for lst in lists): + raise ValueError("Lists should have equal length, but got these lengths:", list(map(len, lists))) + super().__init__("alldifferent_lists", [flatlist(lst) for lst in lists]) + + def decompose(self): + """Returns the decomposition + """ + from .python_builtins import any as cpm_any + constraints = [] + for lst1, lst2 in all_pairs(self.args): + constraints += [cpm_any(var1 != var2 for var1, var2 in zip(lst1, lst2))] + return constraints, [] + + def value(self): + lst_vals = [tuple(argvals(a)) for a in self.args] + return len(set(lst_vals)) == len(self.args) + def allequal(args): warnings.warn("Deprecated, use AllEqual(v1,v2,...,vn) instead, will be removed in stable version", DeprecationWarning) return AllEqual(*args) # unfold list as individual arguments @@ -216,8 +245,7 @@ def decompose(self): return [var1 == var2 for var1, var2 in zip(self.args[:-1], self.args[1:])], [] def value(self): - return len(set(a.value() for a in self.args)) == 1 - + return len(set(argvals(self.args))) == 1 def circuit(args): warnings.warn("Deprecated, use Circuit(v1,v2,...,vn) instead, will be removed in stable version", DeprecationWarning) @@ -231,9 +259,9 @@ def __init__(self, *args): flatargs = flatlist(args) if any(is_boolexpr(arg) for arg in flatargs): raise TypeError("Circuit global constraint only takes arithmetic arguments: {}".format(flatargs)) - super().__init__("circuit", flatargs) if len(flatargs) < 2: raise CPMpyException('Circuit constraint must be given a minimum of 2 variables') + super().__init__("circuit", flatargs) def decompose(self): """ @@ -260,7 +288,8 @@ def value(self): pathlen = 0 idx = 0 visited = set() - arr = [argval(a) for a in self.args] + arr = argvals(self.args) + while idx not in visited: if idx is None: return False @@ -272,6 +301,191 @@ def value(self): return pathlen == len(self.args) and idx == 0 +class SubCircuit(GlobalConstraint): + """ + The sequence of variables form a subcircuit, where x[i] = j means that j is the successor of i. + Contrary to Circuit, there is no requirement on all nodes needing to be part of the circuit. + Nodes which aren't part of the subcircuit, should self loop i.e. x[i] = i. + The subcircuit can be empty (all stops self-loop). + A length 1 subcircuit is treated as an empty subcircuit. + + Global Constraint Catalog: + https://sofdem.github.io/gccat/gccat/Cproper_circuit.html + """ + + def __init__(self, *args): + flatargs = flatlist(args) + + # Ensure all args are integer successor values + if any(is_boolexpr(arg) for arg in flatargs): + raise TypeError("SubCircuit global constraint only takes arithmetic arguments: {}".format(flatargs)) + # Ensure there are at least two stops to create a circuit with + if len(flatargs) < 2: + raise CPMpyException("SubCircuitWithStart constraint must be given a minimum of 2 variables for field 'args' as stops to route between.") + + # Create the object + super().__init__("subcircuit", flatargs) + + def decompose(self): + """ + Decomposition for SubCircuit + + A mix of the above Circuit decomposition, with elements from the Minizinc implementation for the support of optional visits: + https://github.com/MiniZinc/minizinc-old/blob/master/lib/minizinc/std/subcircuit.mzn + """ + from .python_builtins import min as cpm_min + from .python_builtins import all as cpm_all + + # Input arguments + succ = cpm_array(self.args) # Successor variables + n = len(succ) + + # Decision variables + start_node = intvar(0, n-1) # The first stop in the subcircuit. + end_node = intvar(0, n-1) # The last stop in the subcircuit, before looping back to the "start_node". + index_within_subcircuit = intvar(0, n-1, shape=n) # The position each stop takes within the subcircuit, with the assumption that the stop "start_node" gets index 0. + is_part_of_circuit = boolvar(shape=n) # Whether a stop is part of the subcircuit. + empty = boolvar() # To detect when a subcircuit is completely empty + + # Constraining + constraining = [] + constraining += [AllDifferent(succ)] # All stops should have a unique successor. + constraining += list( is_part_of_circuit.implies(succ < len(succ)) ) # Successor values should remain within domain. + for i in range(0, n): + # If a stop is on the subcircuit and it is not the last one, than its successor should have +1 as index. + constraining += [(is_part_of_circuit[i] & (i != end_node)).implies( + index_within_subcircuit[succ[i]] == (index_within_subcircuit[i] + 1) + )] + constraining += list( is_part_of_circuit == (succ != np.arange(n)) ) # When a node is part of the subcircuit it should not self loop, if it is not part it should self loop. + + # Defining + defining = [] + defining += [ empty == cpm_all(succ == np.arange(n)) ] # Definition of empty subcircuit (all nodes self-loop) + defining += [ empty.implies(cpm_all(index_within_subcircuit == cpm_array([0]*n))) ] # If the subcircuit is empty, default all index values to 0 + defining += [ empty.implies(start_node == 0) ] # If the subcircuit is empty, any node could be a start of a 0-length circuit. Default to node 0 as symmetry breaking. + defining += [succ[end_node] == start_node] # Definition of the last node. As the successor we should cycle back to the start. + defining += [ index_within_subcircuit[start_node] == 0 ] # The ordering starts at the start_node. + defining += [ ( empty | (is_part_of_circuit[start_node] == True) ) ] # The start node can only NOT belong to the subcircuit when the subcircuit is empty. + # Nodes which are not part of the subcircuit get an index fixed to +1 the index of "end_node", which equals the length of the subcircuit. + # Nodes part of the subcircuit must have an index <= index_within_subcircuit[end_node]. + # The case of an empty subcircuit is an exception, since "end_node" itself is not part of the subcircuit + defining += [ (is_part_of_circuit[i] == ((~empty) & (index_within_subcircuit[end_node] + 1 != index_within_subcircuit[i]))) for i in range(n)] + # In a subcircuit any of the visited nodes can be the "start node", resulting in symmetrical solutions -> Symmetry breaking + # Part of the formulation from the following is used: https://sofdem.github.io/gccat/gccat/Ccycle.html#uid18336 + subcircuit_visits = intvar(0, n-1, shape=n) # The visited nodes in sequence of length n, with possible repeated stops. e.g. subcircuit [0, 2, 1] -> [0, 2, 1, 0, 2, 1] + defining += [subcircuit_visits[0] == start_node] # The start nodes is the first stop + defining += [subcircuit_visits[i+1] == succ[subcircuit_visits[i]] for i in range(n-1)] # We follow the successor values + # The free "start_node" could be any of the values of aux_subcircuit_visits (the actually visited nodes), resulting in degenerate solutions. + # By enforcing "start_node" to take the smallest value, symmetry breaking is ensured. + defining += [start_node == cpm_min(subcircuit_visits)] + + return constraining, defining + + def value(self): + + succ = [argval(a) for a in self.args] + n = len(succ) + + # Find a start_index + start_index = None + for i,s in enumerate(succ): + if i != s: + # first non self-loop found is taken as start + start_index = i + break + # No valid start found, thus empty subcircuit + if start_index is None: + return True # Change to False if empty subcircuits not allowed + + # Check AllDiff + if not AllDifferent(s).value(): + return False + + # Collect subcircuit + visited = set([start_index]) + idx = succ[start_index] + for i in range(len(succ)): + if idx ==start_index: + break + else: + if idx in visited: + return False + # Check bounds on successor value + if not (0 <= idx < n): return False + # Collect + visited.add(idx) + idx = succ[idx] + + # Check subcircuit + for i in range(n): + # A stop is either visited or self-loops + if not ( (i in visited) or (succ[i] == i) ): + return False + + # Check that subcircuit has length of at least 1. + return succ[start_index] != start_index + +class SubCircuitWithStart(GlobalConstraint): + + """ + The sequence of variables form a subcircuit, where x[i] = j means that j is the successor of i. + Contrary to Circuit, there is no requirement on all nodes needing to be part of the circuit. + Nodes which aren't part of the subcircuit, should self loop i.e. x[i] = i. + The size of the subcircuit should be strictly greater than 1, so not all stops can self loop + (as otherwise the start_index will never get visited). + start_index will be treated as the start of the subcircuit. + The only impact of start_index is that it will be guaranteed to be inside the subcircuit. + + Global Constraint Catalog: + https://sofdem.github.io/gccat/gccat/Cproper_circuit.html + """ + + def __init__(self, *args, start_index:int=0): + flatargs = flatlist(args) + + # Ensure all args are integer successor values + if any(is_boolexpr(arg) for arg in flatargs): + raise TypeError("SubCircuitWithStart global constraint only takes arithmetic arguments: {}".format(flatargs)) + # Ensure start_index is an integer + if not isinstance(start_index, int): + raise TypeError("SubCircuitWithStart global constraint's start_index argument must be an integer: {}".format(start_index)) + # Ensure that the start_index is within range + if not ((start_index >= 0) and (start_index < len(flatargs))): + raise ValueError("SubCircuitWithStart's start_index must be within the range [0, #stops-1] and thus refer to an actual stop as provided through 'args'.") + # Ensure there are at least two stops to create a circuit with + if len(flatargs) < 2: + raise CPMpyException("SubCircuitWithStart constraint must be given a minimum of 2 variables for field 'args' as stops to route between.") + + # Create the object + super().__init__("subcircuitwithstart", flatargs) + self.start_index = start_index + + def decompose(self): + """ + Decomposition for SubCircuitWithStart. + + SubCircuitWithStart simply gets decomposed into SubCircuit and a constraint + enforcing the start_index to be part of the subcircuit. + """ + # Get the arguments + start_index = self.start_index + succ = cpm_array(self.args) # Successor variables + + constraining = [] + constraining += [SubCircuit(self.args)] # The successor variables should form a subcircuit. + constraining += [succ[start_index] != start_index] # The start_index should be inside the subcircuit. + + defining = [] + + return constraining, defining + + def value(self): + start_index = self.start_index + succ = [argval(a) for a in self.args] # Successor variables + + # Check if we have a valid subcircuit and that the start_index is part of it. + return SubCircuit(succ).value() and (succ[start_index] != start_index) + class Inverse(GlobalConstraint): """ @@ -295,9 +509,13 @@ def decompose(self): return [all(rev[x] == i for i, x in enumerate(fwd))], [] def value(self): - fwd = [argval(a) for a in self.args[0]] - rev = [argval(a) for a in self.args[1]] - return all(rev[x] == i for i, x in enumerate(fwd)) + fwd = argvals(self.args[0]) + rev = argvals(self.args[1]) + # args are fine, now evaluate actual inverse cons + try: + return all(rev[x] == i for i, x in enumerate(fwd)) + except IndexError: # partiality of Element constraint + return False class Table(GlobalConstraint): @@ -316,7 +534,7 @@ def decompose(self): def value(self): arr, tab = self.args - arrval = [argval(a) for a in arr] + arrval = argvals(arr) return arrval in tab class ShortTable(GlobalConstraint): @@ -350,21 +568,27 @@ def value(self): #didn't find tuple that matches return False + # syntax of the form 'if b then x == 9 else x == 0' is not supported (no override possible) # same semantic as CPLEX IfThenElse constraint # https://www.ibm.com/docs/en/icos/12.9.0?topic=methods-ifthenelse-method class IfThenElse(GlobalConstraint): def __init__(self, condition, if_true, if_false): - if not is_boolexpr(condition) or not is_boolexpr(if_true) or not is_boolexpr(if_false): - raise TypeError("only boolean expression allowed in IfThenElse") + if not is_boolexpr(condition): + raise TypeError("only Boolean expression allowed as condition") + if not is_boolexpr(if_true) or not is_boolexpr(if_false): + raise TypeError("only Boolean expressions allowed as result, use cpmpy.expressions.globalfunctions.IfThenElseNum instead") super().__init__("ite", [condition, if_true, if_false]) def value(self): condition, if_true, if_false = self.args - if argval(condition): - return argval(if_true) - else: - return argval(if_false) + try: + if argval(condition): + return argval(if_true) + else: + return argval(if_false) + except IncompleteFunctionError: + return False def decompose(self): condition, if_true, if_false = self.args @@ -410,7 +634,7 @@ def decompose(self): def value(self): - return argval(self.args[0]) in argval(self.args[1]) + return argval(self.args[0]) in argvals(self.args[1]) def __repr__(self): return "{} in {}".format(self.args[0], self.args[1]) @@ -440,7 +664,7 @@ def decompose(self): return decomp, [] def value(self): - return sum(argval(a) for a in self.args) % 2 == 1 + return sum(argvals(self.args)) % 2 == 1 def __repr__(self): if len(self.args) == 2: @@ -451,7 +675,8 @@ def __repr__(self): class Cumulative(GlobalConstraint): """ Global cumulative constraint. Used for resource aware scheduling. - Ensures no overlap between tasks and never exceeding the capacity of the resource + Ensures that the capacity of the resource is never exceeded + Equivalent to noOverlap when demand and capacity are equal to 1 Supports both varying demand across tasks or equal demand for all jobs """ def __init__(self, start, duration, end, demand, capacity): @@ -509,14 +734,14 @@ def decompose(self): return cons, [] def value(self): - argvals = [np.array([argval(a) for a in arg]) if is_any_list(arg) + arg_vals = [np.array(argvals(arg)) if is_any_list(arg) else argval(arg) for arg in self.args] - if any(a is None for a in argvals): + if any(a is None for a in arg_vals): return None # start, dur, end are np arrays - start, dur, end, demand, capacity = argvals + start, dur, end, demand, capacity = arg_vals # start and end seperated by duration if not (start + dur == end).all(): return False @@ -530,22 +755,129 @@ def value(self): return True +class Precedence(GlobalConstraint): + """ + Constraint enforcing some values have precedence over others. + Given an array of variables X and a list of precedences P: + Then in order to satisfy the constraint, if X[i] = P[j+1], then there exists a X[i'] = P[j] with i' < i + """ + def __init__(self, vars, precedence): + if not is_any_list(vars): + raise TypeError("Precedence expects a list of variables, but got", vars) + if not is_any_list(precedence) or any(isinstance(x, Expression) for x in precedence): + raise TypeError("Precedence expects a list of values as precedence, but got", precedence) + super().__init__("precedence", [vars, precedence]) + + def decompose(self): + """ + Decomposition based on: + Law, Yat Chiu, and Jimmy HM Lee. "Global constraints for integer and set value precedence." + Principles and Practice of Constraint Programming–CP 2004: 10th International Conference, CP 2004 + """ + from .python_builtins import any as cpm_any + + args, precedence = self.args + constraints = [] + for s,t in zip(precedence[:-1], precedence[1:]): + for j in range(len(args)): + constraints += [(args[j] == t).implies(cpm_any(args[:j] == s))] + return constraints, [] + + def value(self): + + args, precedence = self.args + vals = np.array(argvals(args)) + for s,t in zip(precedence[:-1], precedence[1:]): + if vals[0] == t: return False + for j in range(len(args)): + if vals[j] == t and sum(vals[:j] == s) == 0: + return False + return True + + +class NoOverlap(GlobalConstraint): + + def __init__(self, start, dur, end): + assert is_any_list(start), "start should be a list" + assert is_any_list(dur), "duration should be a list" + assert is_any_list(end), "end should be a list" + + start = flatlist(start) + dur = flatlist(dur) + end = flatlist(end) + assert len(start) == len(dur) == len(end), "Start, duration and end should have equal length in NoOverlap constraint" + + super().__init__("no_overlap", [start, dur, end]) + + def decompose(self): + start, dur, end = self.args + cons = [s + d == e for s,d,e in zip(start, dur, end)] + for (s1, e1), (s2, e2) in all_pairs(zip(start, end)): + cons += [(e1 <= s2) | (e2 <= s1)] + return cons, [] + def value(self): + start, dur, end = argvals(self.args) + if any(s + d != e for s,d,e in zip(start, dur, end)): + return False + for (s1,d1, e1), (s2,d2, e2) in all_pairs(zip(start,dur, end)): + if e1 > s2 and e2 > s1: + return False + return True + +class NoOverlap2d(GlobalConstraint): + """ + 2D-version of the NoOverlap constraint. + Ensures a set of rectangles is placed on a grid such that they do not overlap. + """ + def __init__(self, start_x, dur_x, end_x, start_y, dur_y, end_y): + assert len(start_x) == len(dur_x) == len(end_x) == len(start_y) == len(dur_y) == len(end_y) + super().__init__("no_overlap2d", [start_x, dur_x, end_x, start_y, dur_y, end_y]) + + def decompose(self): + from .python_builtins import any as cpm_any + + start_x, dur_x, end_x, start_y, dur_y, end_y = self.args + n = len(start_x) + cons = [s + d == e for s,d,e in zip(start_x, dur_x, end_x)] + cons += [s + d == e for s,d,e in zip(start_y, dur_y, end_y)] + + for i,j in all_pairs(list(range(n))): + cons += [cpm_any([end_x[i] <= start_x[j], end_x[j] <= start_x[i], + end_y[i] <= start_y[j], end_y[j] <= start_y[i]])] + return cons,[] + def value(self): + start_x, dur_x, end_x, start_y, dur_y, end_y = argvals(self.args) + n = len(start_x) + if any(s + d != e for s, d, e in zip(start_x, dur_x, end_x)): + return False + if any(s + d != e for s, d, e in zip(start_y, dur_y, end_y)): + return False + for i,j in all_pairs(list(range(n))): + if end_x[i] > start_x[j] and end_x[j] > start_x[i] and \ + end_y[i] > start_y[j] and end_y[j] > start_y[i]: + return False + return True + class GlobalCardinalityCount(GlobalConstraint): """ GlobalCardinalityCount(vars,vals,occ): The number of occurrences of each value vals[i] in the list of variables vars must be equal to occ[i]. """ - def __init__(self, vars, vals, occ): + def __init__(self, vars, vals, occ, closed=False): flatargs = flatlist([vars, vals, occ]) if any(is_boolexpr(arg) for arg in flatargs): raise TypeError("Only numerical arguments allowed for gcc global constraint: {}".format(flatargs)) super().__init__("gcc", [vars,vals,occ]) + self.closed = closed def decompose(self): from .globalfunctions import Count vars, vals, occ = self.args - return [Count(vars, i) == v for i, v in zip(vals, occ)], [] + constraints = [Count(vars, i) == v for i, v in zip(vals, occ)] + if self.closed: + constraints += [InDomain(v, vals) for v in vars] + return constraints, [] def value(self): from .python_builtins import all @@ -571,9 +903,8 @@ def decompose(self): return [args[i] <= args[i+1] for i in range(len(args)-1)], [] def value(self): - from .python_builtins import all - args = self.args - return all(args[i].value() <= args[i+1].value() for i in range(len(args)-1)) + args = argvals(self.args) + return all(args[i] <= args[i+1] for i in range(len(args)-1)) class Decreasing(GlobalConstraint): @@ -594,9 +925,8 @@ def decompose(self): return [args[i] >= args[i+1] for i in range(len(args)-1)], [] def value(self): - from .python_builtins import all - args = self.args - return all(args[i].value() >= args[i+1].value() for i in range(len(args)-1)) + args = argvals(self.args) + return all(args[i] >= args[i+1] for i in range(len(args)-1)) class IncreasingStrict(GlobalConstraint): @@ -617,9 +947,8 @@ def decompose(self): return [args[i] < args[i+1] for i in range(len(args)-1)], [] def value(self): - from .python_builtins import all - args = self.args - return all((args[i].value() < args[i+1].value()) for i in range(len(args)-1)) + args = argvals(self.args) + return all(args[i] < args[i+1] for i in range(len(args)-1)) class DecreasingStrict(GlobalConstraint): @@ -640,9 +969,134 @@ def decompose(self): return [(args[i] > args[i+1]) for i in range(len(args)-1)], [] def value(self): - from .python_builtins import all - args = self.args - return all((args[i].value() > args[i+1].value()) for i in range(len(args)-1)) + args = argvals(self.args) + return all(args[i] > args[i+1] for i in range(len(args)-1)) + + +class LexLess(GlobalConstraint): + """ Given lists X,Y, enforcing that X is lexicographically less than Y. + """ + def __init__(self, list1, list2): + X = flatlist(list1) + Y = flatlist(list2) + if len(X) != len(Y): + raise CPMpyException(f"The 2 lists given in LexLess must have the same size: X length is {len(X)} and Y length is {len(Y)}") + super().__init__("lex_less", [X, Y]) + + def decompose(self): + """ + Implementation inspired by Hakan Kjellerstrand (http://hakank.org/cpmpy/cpmpy_hakank.py) + + The decomposition creates auxiliary Boolean variables and constraints that + collectively ensure X is lexicographically less than Y + The auxiliary boolean vars are defined to represent if the given lists are lexicographically ordered + (less or equal) up to the given index. + Decomposition enforces through the constraining part that the first boolean variable needs to be true, and thus + through the defining part it is enforced that if it is not strictly lexicographically less in a given index, + then next index must be lexicographically less or equal. It needs to be strictly less in at least one index. + + The use of auxiliary Boolean variables bvar ensures that the constraints propagate immediately, + maintaining arc-consistency. Each bvar[i] enforces the lexicographic ordering at each position, ensuring that + every value in the domain of X[i] can be extended to a consistent value in the domain of $Y_i$ for all + subsequent positions. + """ + X, Y = cpm_array(self.args) + + bvar = boolvar(shape=(len(X) + 1)) + + # Constraint ensuring that each element in X is less than or equal to the corresponding element in Y, + # until a strict inequality is encountered. + defining = [bvar == ((X <= Y) & ((X < Y) | bvar[1:]))] + # enforce the last element to be true iff (X[-1] < Y[-1]), enforcing strict lexicographic order + defining.append(bvar[-1] == (X[-1] < Y[-1])) + constraining = [bvar[0]] + + return constraining, defining + + def value(self): + X, Y = argvals(self.args) + return any((X[i] < Y[i]) & all(X[j] <= Y[j] for j in range(i)) for i in range(len(X))) + + +class LexLessEq(GlobalConstraint): + """ Given lists X,Y, enforcing that X is lexicographically less than Y (or equal). + """ + def __init__(self, list1, list2): + X = flatlist(list1) + Y = flatlist(list2) + if len(X) != len(Y): + raise CPMpyException(f"The 2 lists given in LexLessEq must have the same size: X length is {len(X)} and Y length is {len(Y)}") + super().__init__("lex_lesseq", [X, Y]) + + def decompose(self): + """ + Implementation inspired by Hakan Kjellerstrand (http://hakank.org/cpmpy/cpmpy_hakank.py) + + The decomposition creates auxiliary Boolean variables and constraints that + collectively ensure X is lexicographically less than Y + The auxiliary boolean vars are defined to represent if the given lists are lexicographically ordered + (less or equal) up to the given index. + Decomposition enforces through the constraining part that the first boolean variable needs to be true, and thus + through the defining part it is enforced that if it is not strictly lexicographically less in a given index, + then next index must be lexicographically less or equal. + + The use of auxiliary Boolean variables bvar ensures that the constraints propagate immediately, + maintaining arc-consistency. Each bvar[i] enforces the lexicographic ordering at each position, ensuring that + every value in the domain of X[i] can be extended to a consistent value in the domain of $Y_i$ for all + subsequent positions. + """ + X, Y = cpm_array(self.args) + + bvar = boolvar(shape=(len(X) + 1)) + defining = [bvar == ((X <= Y) & ((X < Y) | bvar[1:]))] + defining.append(bvar[-1] == (X[-1] <= Y[-1])) + constraining = [bvar[0]] + + return constraining, defining + + def value(self): + X, Y = argvals(self.args) + return any((X[i] < Y[i]) & all(X[j] <= Y[j] for j in range(i)) for i in range(len(X))) | all(X[i] == Y[i] for i in range(len(X))) + + +class LexChainLess(GlobalConstraint): + """ Given a matrix X, LexChainLess enforces that all rows are lexicographically ordered. + """ + def __init__(self, X): + # Ensure the numpy array is 2D + X = cpm_array(X) + assert X.ndim == 2, "Input must be a 2D array or a list of lists" + super().__init__("lex_chain_less", X.tolist()) + + def decompose(self): + """ Decompose to a series of LexLess constraints between subsequent rows + """ + X = self.args + return [LexLess(prev_row, curr_row) for prev_row, curr_row in zip(X, X[1:])], [] + + def value(self): + X = argvals(self.args) + return all(LexLess(prev_row, curr_row).value() for prev_row, curr_row in zip(X, X[1:])) + + +class LexChainLessEq(GlobalConstraint): + """ Given a matrix X, LexChainLessEq enforces that all rows are lexicographically ordered. + """ + def __init__(self, X): + # Ensure the numpy array is 2D + X = cpm_array(X) + assert X.ndim == 2, "Input must be a 2D array or a list of lists" + super().__init__("lex_chain_lesseq", X.tolist()) + + def decompose(self): + """ Decompose to a series of LexLessEq constraints between subsequent rows + """ + X = self.args + return [LexLessEq(prev_row, curr_row) for prev_row, curr_row in zip(X, X[1:])], [] + + def value(self): + X = argvals(self.args) + return all(LexLessEq(prev_row, curr_row).value() for prev_row, curr_row in zip(X, X[1:])) class DirectConstraint(Expression): diff --git a/cpmpy/expressions/globalfunctions.py b/cpmpy/expressions/globalfunctions.py index 1562ee5fa..4d49ab0b2 100644 --- a/cpmpy/expressions/globalfunctions.py +++ b/cpmpy/expressions/globalfunctions.py @@ -57,6 +57,7 @@ def decompose_comparison(self): Maximum Element Count + Among NValue Abs @@ -67,7 +68,7 @@ def decompose_comparison(self): from ..exceptions import CPMpyException, IncompleteFunctionError, TypeError from .core import Expression, Operator, Comparison from .variables import boolvar, intvar, cpm_array, _NumVarImpl -from .utils import flatlist, all_pairs, argval, is_num, eval_comparison, is_any_list, is_boolexpr, get_bounds +from .utils import flatlist, all_pairs, argval, is_num, eval_comparison, is_any_list, is_boolexpr, get_bounds, argvals class GlobalFunction(Expression): @@ -257,7 +258,8 @@ def value(self): if idxval is not None: if idxval >= 0 and idxval < len(arr): return argval(arr[idxval]) - raise IncompleteFunctionError(f"Index {idxval} out of range for array of length {len(arr)} while calculating value for expression {self}") + raise IncompleteFunctionError(f"Index {idxval} out of range for array of length {len(arr)} while calculating value for expression {self}" + + "\n Use argval(expr) to get the value of expr with relational semantics.") return None # default def decompose_comparison(self, cpm_op, cpm_rhs): @@ -318,6 +320,36 @@ def get_bounds(self): arr, val = self.args return 0, len(arr) + + +class Among(GlobalFunction): + """ + The Among (numerical) global constraint represents the number of variable that take values among the values in arr + """ + + def __init__(self,arr,vals): + if not is_any_list(arr) or not is_any_list(vals): + raise TypeError("Among takes as input two arrays, not: {} and {}".format(arr,vals)) + if any(isinstance(val, Expression) for val in vals): + raise TypeError(f"Among takes a set of values as input, not {vals}") + super().__init__("among", [arr,vals]) + + def decompose_comparison(self, cmp_op, cmp_rhs): + """ + Among(arr, vals) can only be decomposed if it's part of a comparison' + """ + from .python_builtins import sum, any + arr, values = self.args + count_for_each_val = [Count(arr, val) for val in values] + return [eval_comparison(cmp_op, sum(count_for_each_val), cmp_rhs)], [] + + def value(self): + return int(sum(np.isin(argvals(self.args[0]), self.args[1]))) + + def get_bounds(self): + return 0, len(self.args[0]) + + class NValue(GlobalFunction): """ @@ -418,4 +450,35 @@ def get_bounds(self): """ Returns the bounds of the (numerical) global constraint """ - return 0, len(self.args) \ No newline at end of file + return 0, len(self.args) + + +class IfThenElseNum(GlobalFunction): + """ + Function returning x if b is True and otherwise y + """ + def __init__(self, b, x,y): + super().__init__("IfThenElseNum",[b,x,y]) + + def decompose_comparison(self, cmp_op, cpm_rhs): + b,x,y = self.args + + lbx,ubx = get_bounds(x) + lby,uby = get_bounds(y) + iv = intvar(min(lbx,lby), max(ubx,uby)) + defining = [b.implies(x == iv), (~b).implies(y == iv)] + + return [eval_comparison(cmp_op, iv, cpm_rhs)], defining + + def get_bounds(self): + b,x,y = self.args + lbs,ubs = get_bounds([x,y]) + return min(lbs), max(ubs) + def value(self): + b,x,y = self.args + if argval(b): + return argval(x) + else: + return argval(y) + + diff --git a/cpmpy/expressions/utils.py b/cpmpy/expressions/utils.py index 30b757e64..9e476ca04 100644 --- a/cpmpy/expressions/utils.py +++ b/cpmpy/expressions/utils.py @@ -121,11 +121,21 @@ def argval(a): We check with hasattr instead of isinstance to avoid circular dependency """ - try: - return a.value() if hasattr(a, "value") else a - except IncompleteFunctionError as e: - if a.is_bool(): return False - raise e + if hasattr(a, "value"): + try: + return a.value() + except IncompleteFunctionError as e: + if a.is_bool(): + return False + else: + raise e + return a + + +def argvals(arr): + if is_any_list(arr): + return [argvals(arg) for arg in arr] + return argval(arr) def is_leaf(a): diff --git a/cpmpy/solvers/choco.py b/cpmpy/solvers/choco.py index d2d502794..01f48fca7 100644 --- a/cpmpy/solvers/choco.py +++ b/cpmpy/solvers/choco.py @@ -29,7 +29,7 @@ from ..expressions.globalconstraints import DirectConstraint from ..expressions.variables import _NumVarImpl, _IntVarImpl, _BoolVarImpl, NegBoolView, intvar from ..expressions.globalconstraints import GlobalConstraint -from ..expressions.utils import is_num, is_int, is_boolexpr, is_any_list, get_bounds +from ..expressions.utils import is_num, is_int, is_boolexpr, is_any_list, get_bounds, argval, argvals from ..transformations.decompose_global import decompose_in_tree from ..transformations.get_variables import get_variables from ..transformations.flatten_model import flatten_constraint, flatten_objective @@ -208,9 +208,9 @@ def solveAll(self, display=None, time_limit=None, solution_limit=None, call_from cpm_var._value = value # print the desired display if isinstance(display, Expression): - print(display.value()) + print(argval(display)) elif isinstance(display, list): - print([v.value() for v in display]) + print(argvals(display)) else: display() # callback @@ -313,13 +313,17 @@ def transform(self, cpm_expr): cpm_cons = toplevel_list(cpm_expr) supported = {"min", "max", "abs", "count", "element", "alldifferent", "alldifferent_except0", "allequal", - "table", "InDomain", "cumulative", "circuit", "gcc", "inverse", "nvalue", "increasing", - "decreasing","strictly_increasing","strictly_decreasing"} + "table", "InDomain", "cumulative", "circuit", "subcircuit", "gcc", "inverse", "nvalue", "increasing", + "decreasing","strictly_increasing","strictly_decreasing", "lex_lesseq", "lex_less", "among", "precedence"} - # choco supports reification of any constraint, but has a bug in increasing and decreasing + # choco supports reification of any constraint, but has a bug in increasing, decreasing and subcircuit (#1085) supported_reified = {"min", "max", "abs", "count", "element", "alldifferent", "alldifferent_except0", - "allequal", "table", "InDomain", "cumulative", "circuit", "gcc", "inverse", "nvalue"} - # for when choco new release comes, fixing the bug on increasing and decreasing + # for when choco new release comes, fixing the bug on increasing and decreasing + "allequal", "table", "InDomain", "cumulative", "circuit", "gcc", "inverse", "nvalue", + "among", + "lex_lesseq", "lex_less"} + + # for when choco new release comes, fixing the bug on increasing, decreasing and subcircuit #supported_reified = supported cpm_cons = decompose_in_tree(cpm_cons, supported, supported_reified) cpm_cons = flatten_constraint(cpm_cons) # flat normal form @@ -349,6 +353,7 @@ def __add__(self, cpm_expr): """ # add new user vars to the set get_variables(cpm_expr, collect=self.user_vars) + # ensure all vars are known to solver # transform and post the constraints for con in self.transform(cpm_expr): @@ -480,6 +485,9 @@ def _get_constraint(self, cpm_expr): elif lhs.name == 'count': # count(vars, var/int) = var arr, val = lhs.args return self.chc_model.count(self.solver_var(val), self._to_vars(arr), chc_rhs) + elif lhs.name == "among": + arr, vals = lhs.args + return self.chc_model.among(chc_rhs, self._to_vars(arr), vals) elif lhs.name == 'mul': # var * var/int = var/int a,b = self.solver_vars(lhs.args) if isinstance(a, int): @@ -489,14 +497,17 @@ def _get_constraint(self, cpm_expr): chc_rhs = self._to_var(rhs) return self.chc_model.pow(*self.solver_vars(lhs.args),chc_rhs) + + raise NotImplementedError( "Not a known supported Choco left-hand-side '{}' {}".format(lhs.name, cpm_expr)) # base (Boolean) global constraints elif isinstance(cpm_expr, GlobalConstraint): - # many globals require all variables as arguments - if cpm_expr.name in {"alldifferent", "alldifferent_except0", "allequal", "circuit", "inverse","increasing","decreasing","strictly_increasing","strictly_decreasing"}: + if cpm_expr.name in {"alldifferent", "alldifferent_except0", "allequal", "circuit", + "inverse", "increasing", "decreasing", "strictly_increasing", "strictly_decreasing", + "lex_lesseq", "lex_less"}: chc_args = self._to_vars(cpm_expr.args) if cpm_expr.name == 'alldifferent': return self.chc_model.all_different(chc_args) @@ -516,6 +527,13 @@ def _get_constraint(self, cpm_expr): return self.chc_model.increasing(chc_args,1) elif cpm_expr.name == "strictly_decreasing": return self.chc_model.decreasing(chc_args,1) + elif cpm_expr.name in ["lex_lesseq", "lex_less"]: + if cpm_expr.name == "lex_lesseq": + return self.chc_model.lex_less_eq(*chc_args) + return self.chc_model.lex_less(*chc_args) +# Ready for when it is fixed in pychoco (https://github.com/chocoteam/pychoco/issues/30) +# elif cpm_expr.name == "lex_chain_less": +# return self.chc_model.lex_chain_less(chc_args) # but not all elif cpm_expr.name == 'table': @@ -535,9 +553,17 @@ def _get_constraint(self, cpm_expr): # Create task variables. Choco can create them only one by one tasks = [self.chc_model.task(s, d, e) for s, d, e in zip(start, dur, end)] return self.chc_model.cumulative(tasks, demand, cap) + elif cpm_expr.name == "precedence": + return self.chc_model.int_value_precede_chain(self._to_vars(cpm_expr.args[0]), cpm_expr.args[1]) + elif cpm_expr.name == "subcircuit": + # Successor variables + succ = self.solver_vars(cpm_expr.args) + # Add an unused variable for the subcircuit length. + subcircuit_length = self.solver_var(intvar(0, len(succ))) + return self.chc_model.sub_circuit(succ, 0, subcircuit_length) elif cpm_expr.name == "gcc": vars, vals, occ = cpm_expr.args - return self.chc_model.global_cardinality(*self.solver_vars([vars, vals]), self._to_vars(occ)) + return self.chc_model.global_cardinality(*self.solver_vars([vars, vals]), self._to_vars(occ), cpm_expr.closed) else: raise NotImplementedError(f"Unknown global constraint {cpm_expr}, should be decomposed! If you reach this, please report on github.") diff --git a/cpmpy/solvers/exact.py b/cpmpy/solvers/exact.py index 2d1c37ffd..5f0598cfb 100644 --- a/cpmpy/solvers/exact.py +++ b/cpmpy/solvers/exact.py @@ -37,7 +37,7 @@ from ..transformations.normalize import toplevel_list from ..expressions.globalconstraints import DirectConstraint from ..exceptions import NotSupportedError -from ..expressions.utils import flatlist +from ..expressions.utils import flatlist, argvals import numpy as np import numbers @@ -263,9 +263,9 @@ def solveAll(self, display=None, time_limit=None, solution_limit=None, call_from if display is not None: self._fillObjAndVars() if isinstance(display, Expression): - print(display.value()) + print(argval(display)) elif isinstance(display, list): - print([v.value() for v in display]) + print(argvals(display)) else: display() # callback elif my_status == 2: # found inconsistency diff --git a/cpmpy/solvers/gurobi.py b/cpmpy/solvers/gurobi.py index 7223ad33f..dbe3618bf 100644 --- a/cpmpy/solvers/gurobi.py +++ b/cpmpy/solvers/gurobi.py @@ -28,6 +28,7 @@ from .solver_interface import SolverInterface, SolverStatus, ExitStatus from ..expressions.core import * +from ..expressions.utils import argvals from ..expressions.variables import _BoolVarImpl, NegBoolView, _IntVarImpl, _NumVarImpl, intvar from ..expressions.globalconstraints import DirectConstraint from ..transformations.comparison import only_numexpr_equality @@ -461,9 +462,9 @@ def solveAll(self, display=None, time_limit=None, solution_limit=None, call_from if display is not None: if isinstance(display, Expression): - print(display.value()) + print(argval(display)) elif isinstance(display, list): - print([v.value() for v in display]) + print(argvals(display)) else: display() # callback diff --git a/cpmpy/solvers/minizinc.py b/cpmpy/solvers/minizinc.py index 0bb6bd9fd..5698def66 100644 --- a/cpmpy/solvers/minizinc.py +++ b/cpmpy/solvers/minizinc.py @@ -34,9 +34,9 @@ from .solver_interface import SolverInterface, SolverStatus, ExitStatus from ..exceptions import MinizincNameException, MinizincBoundsException from ..expressions.core import Expression, Comparison, Operator, BoolVal -from ..expressions.variables import _NumVarImpl, _IntVarImpl, _BoolVarImpl, NegBoolView, intvar +from ..expressions.variables import _NumVarImpl, _IntVarImpl, _BoolVarImpl, NegBoolView, intvar, cpm_array from ..expressions.globalconstraints import DirectConstraint -from ..expressions.utils import is_num, is_any_list, eval_comparison +from ..expressions.utils import is_num, is_any_list, eval_comparison, argvals, argval from ..transformations.decompose_global import decompose_in_tree from ..transformations.get_variables import get_variables from ..exceptions import MinizincPathException, NotSupportedError @@ -74,17 +74,27 @@ class CPM_minizinc(SolverInterface): required_version = (2, 8, 2) @staticmethod def supported(): - return CPM_minizinc.installed() and not CPM_minizinc.outdated() + return CPM_minizinc.installed() and CPM_minizinc.executable_installed() and not CPM_minizinc.outdated() @staticmethod def installed(): # try to import the package try: + # check if MiniZinc Python is installed import minizinc return True except ImportError as e: return False + @staticmethod + def executable_installed(): + # check if MiniZinc executable is installed + from minizinc import default_driver + if default_driver is None: + warnings.warn("MiniZinc Python is installed, but the MiniZinc executable is missing in path.") + return False + return True + @staticmethod def outdated(): from minizinc import default_driver @@ -135,6 +145,8 @@ def __init__(self, cpm_model=None, subsolver=None): """ if not self.installed(): raise Exception("CPM_minizinc: Install the python package 'minizinc'") + if not self.executable_installed(): + raise Exception("CPM_minizinc: Install the MiniZinc executable and make it available in path.") elif self.outdated(): version = str(self.required_version[0]) for x in self.required_version[1:]: @@ -323,9 +335,9 @@ async def _solveAll(self, display=None, time_limit=None, solution_limit=None, ** # and the actual displaying if isinstance(display, Expression): - print(display.value()) + print(argval(display)) elif isinstance(display, list): - print([v.value() for v in display]) + print(argvals(display)) else: display() # callback @@ -418,10 +430,11 @@ def transform(self, cpm_expr): """ cpm_cons = toplevel_list(cpm_expr) supported = {"min", "max", "abs", "element", "count", "nvalue", "alldifferent", "alldifferent_except0", "allequal", - "inverse", "ite" "xor", "table", "cumulative", "circuit", "gcc", "increasing", - "decreasing","strictly_increasing","strictly_decreasing"} - return decompose_in_tree(cpm_cons, supported, supported_reified=supported - {"circuit"}) - + "inverse", "ite" "xor", "table", "cumulative", "circuit", "subcircuit", "gcc", "increasing", + "precedence", "no_overlap", + "decreasing","strictly_increasing","strictly_decreasing", "lex_lesseq", "lex_less", "lex_chain_less", + "lex_chain_lesseq", "among"} + return decompose_in_tree(cpm_cons, supported, supported_reified=supported - {"circuit", "subcircuit"}) def __add__(self, cpm_expr): """ @@ -503,6 +516,20 @@ def zero_based(array): args_str = [self._convert_expression(e) for e in expr.args] return "alldifferent_except_0([{}])".format(",".join(args_str)) + if expr.name in ["lex_lesseq", "lex_less"]: + X = [self._convert_expression(e) for e in expr.args[0]] + Y = [self._convert_expression(e) for e in expr.args[1]] + return f"{expr.name}({{}}, {{}})".format(X, Y) + + + if expr.name in ["lex_chain_less", "lex_chain_lesseq"]: + X = cpm_array([[self._convert_expression(e) for e in row] for row in expr.args]) + str_X = "[|\n" # opening + for row in X.T: # Minizinc enforces lexicographic order on columns + str_X += ",".join(map(str, row)) + " |" # rows + str_X += "\n|]" # closing + return f"{expr.name}({{}})".format(str_X) + args_str = [self._convert_expression(e) for e in expr.args] # standard expressions: comparison, operator, element if isinstance(expr, Comparison): @@ -572,9 +599,15 @@ def zero_based(array): return txt # rest: global constraints - elif expr.name.endswith('circuit'): # circuit, subcircuit + elif expr.name == 'circuit': # minizinc is offset 1, which can be problematic here... args_str = ["{}+1".format(self._convert_expression(e)) for e in expr.args] + return "{}([{}])".format(expr.name, ",".join(args_str)) + + elif expr.name == 'subcircuit': + # minizinc is offset 1, which can be problematic here... + args_str = ["{}+1".format(self._convert_expression(e)) for e in expr.args] + return "{}([{}])".format(expr.name, ",".join(args_str)) elif expr.name == "cumulative": start, dur, end, _, _ = expr.args @@ -584,6 +617,15 @@ def zero_based(array): return format_str.format(args_str[0], args_str[1], args_str[3], args_str[4]) + elif expr.name == "precedence": + return "value_precede_chain({},{})".format(args_str[1], args_str[0]) + + elif expr.name == "no_overlap": + start, dur, end = expr.args + durstr = self._convert_expression([s + d == e for s, d, e in zip(start, dur, end)]) + format_str = "forall(" + durstr + " ++ [disjunctive({},{})])" + return format_str.format(args_str[0], args_str[1]) + elif expr.name == 'ite': cond, tr, fal = expr.args return "if {} then {} else {} endif".format(self._convert_expression(cond), self._convert_expression(tr), @@ -594,7 +636,11 @@ def zero_based(array): vars = self._convert_expression(vars) vals = self._convert_expression(vals) occ = self._convert_expression(occ) - return "global_cardinality({},{},{})".format(vars,vals,occ) + if expr.closed is False: + name = "global_cardinality" + else: + name = "global_cardinality_closed" + return "{}({},{},{})".format(name,vars,vals,occ) elif expr.name == "abs": return "abs({})".format(args_str[0]) @@ -605,6 +651,12 @@ def zero_based(array): val = self._convert_expression(val) return "count({},{})".format(vars, val) + elif expr.name == "among": + vars, vals = expr.args + vars = self._convert_expression(vars) + vals = self._convert_expression(vals).replace("[", "{").replace("]", "}") # convert to set + return "among({},{})".format(vars, vals) + # a direct constraint, treat differently for MiniZinc, a text-based language # use the name as, unpack the arguments from the argument tuple elif isinstance(expr, DirectConstraint): diff --git a/cpmpy/solvers/ortools.py b/cpmpy/solvers/ortools.py index a8f92878a..3bdc8fd80 100644 --- a/cpmpy/solvers/ortools.py +++ b/cpmpy/solvers/ortools.py @@ -30,9 +30,9 @@ from ..exceptions import NotSupportedError from ..expressions.core import Expression, Comparison, Operator, BoolVal from ..expressions.globalconstraints import DirectConstraint -from ..expressions.variables import _NumVarImpl, _IntVarImpl, _BoolVarImpl, NegBoolView, boolvar +from ..expressions.variables import _NumVarImpl, _IntVarImpl, _BoolVarImpl, NegBoolView, boolvar, cpm_array from ..expressions.globalconstraints import GlobalConstraint -from ..expressions.utils import is_num, is_any_list, eval_comparison, flatlist +from ..expressions.utils import is_num, is_any_list, eval_comparison, flatlist, argval, argvals from ..transformations.decompose_global import decompose_in_tree from ..transformations.get_variables import get_variables from ..transformations.flatten_model import flatten_constraint, flatten_objective @@ -334,7 +334,7 @@ def transform(self, cpm_expr): cpm_cons = toplevel_list(cpm_expr) print(f"c ort:toplevel_list took {(time.time()-t0):.4f} -- {len(cpm_expr)}") t0 = time.time() - supported = {"min", "max", "abs", "element", "alldifferent", "xor", "table", "cumulative", "circuit", "inverse"} + supported = {"min", "max", "abs", "element", "alldifferent", "xor", "table", "cumulative", "circuit", "subcircuit", "subcircuitwithstart", "inverse", "no_overlap", "nooverlap2d"} print(f"c ort:has_nested took {(time.time()-t0):.4f} -- {len(cpm_expr)}") t0 = time.time() cpm_cons = decompose_in_tree(cpm_cons, supported) @@ -497,9 +497,18 @@ def _post_constraint(self, cpm_expr, reifiable=False): start, dur, end, demand, cap = self.solver_vars(cpm_expr.args) intervals = [self.ort_model.NewIntervalVar(s,d,e,f"interval_{s}-{d}-{e}") for s,d,e in zip(start,dur,end)] return self.ort_model.AddCumulative(intervals, demand, cap) + elif cpm_expr.name == "no_overlap": + start, dur, end = self.solver_vars(cpm_expr.args) + intervals = [self.ort_model.NewIntervalVar(s,d,e, f"interval_{s}-{d}-{d}") for s,d,e in zip(start,dur,end)] + return self.ort_model.add_no_overlap(intervals) + elif cpm_expr.name == "no_overlap2d": + start_x, dur_x, end_x, start_y, dur_y, end_y = self.solver_vars(cpm_expr.args) + intervals_x = [self.ort_model.NewIntervalVar(s,d,e, f"xinterval_{s}-{d}-{d}") for s,d,e in zip(start_x,dur_x,end_x)] + intervals_y = [self.ort_model.NewIntervalVar(s,d,e, f"yinterval_{s}-{d}-{d}") for s,d,e in zip(start_y,dur_y,end_y)] + return self.ort_model.add_no_overlap_2d(intervals_x, intervals_y) elif cpm_expr.name == "circuit": # ortools has a constraint over the arcs, so we need to create these - # when using an objective over arcs, using these vars direclty is recommended + # when using an objective over arcs, using these vars directly is recommended # (see PCTSP-path model in the future) x = cpm_expr.args N = len(x) @@ -507,9 +516,29 @@ def _post_constraint(self, cpm_expr, reifiable=False): # post channeling constraints from int to bool self += [b == (x[i] == j) for (i,j),b in np.ndenumerate(arcvars)] # post the global constraint - # when posting arcs on diagonal (i==j), it would do subcircuit + # when posting arcs on diagonal (i==j), it would do subcircuit (see subcircuit) ort_arcs = [(i,j,self.solver_var(b)) for (i,j),b in np.ndenumerate(arcvars) if i != j] return self.ort_model.AddCircuit(ort_arcs) + elif cpm_expr.name == "subcircuit": + x = cpm_expr.args + N = len(x) + arcvars = boolvar(shape=(N,N)) + # post channeling constraints from int to bool + self += [b == (x[i] == j) for (i,j),b in np.ndenumerate(arcvars)] + # post the global constraint + # posting arcs on diagonal (i==j) allows for subcircuits + ort_arcs = [(i,j,self.solver_var(b)) for (i,j),b in np.ndenumerate(arcvars)] # Allows for empty subcircuits + return self.ort_model.AddCircuit(ort_arcs) + elif cpm_expr.name == "subcircuitwithstart": + x = cpm_expr.args + N = len(x) + arcvars = boolvar(shape=(N,N)) + # post channeling constraints from int to bool + self += [b == (x[i] == j) for (i,j),b in np.ndenumerate(arcvars)] + # post the global constraint + # posting arcs on diagonal (i==j) allows for subcircuits + ort_arcs = [(i,j,self.solver_var(b)) for (i,j),b in np.ndenumerate(arcvars) if not ((i == j) and (i == cpm_expr.start_index))] # The start index cannot self loop and thus must be part of the subcircuit. + return self.ort_model.AddCircuit(ort_arcs) elif cpm_expr.name == 'inverse': assert len(cpm_expr.args) == 2, "inverse() expects two args: fwd, rev" fwd, rev = self.solver_vars(cpm_expr.args) @@ -716,10 +745,10 @@ def on_solution_callback(self): cpm_var._value = self.Value(self._varmap[cpm_var]) if isinstance(self._display, Expression): - print(self._display.value()) + print(argval(self._display)) elif isinstance(self._display, list): # explicit list of expressions to display - print([v.value() for v in self._display]) + print(argvals(self._display)) else: # callable self._display() diff --git a/cpmpy/solvers/pysat.py b/cpmpy/solvers/pysat.py index 32c0b1edf..889e48aa8 100644 --- a/cpmpy/solvers/pysat.py +++ b/cpmpy/solvers/pysat.py @@ -38,7 +38,7 @@ from ..transformations.decompose_global import decompose_in_tree from ..transformations.get_variables import get_variables from ..transformations.flatten_model import flatten_constraint -from ..transformations.normalize import toplevel_list +from ..transformations.normalize import toplevel_list, simplify_boolean from ..transformations.reification import only_implies, only_bv_reifies @@ -233,6 +233,7 @@ def transform(self, cpm_expr): """ cpm_cons = toplevel_list(cpm_expr) cpm_cons = decompose_in_tree(cpm_cons) + cpm_cons = simplify_boolean(cpm_cons) cpm_cons = flatten_constraint(cpm_cons) cpm_cons = only_bv_reifies(cpm_cons) cpm_cons = only_implies(cpm_cons) diff --git a/cpmpy/solvers/pysdd.py b/cpmpy/solvers/pysdd.py index 03003256d..a00800121 100644 --- a/cpmpy/solvers/pysdd.py +++ b/cpmpy/solvers/pysdd.py @@ -26,7 +26,7 @@ from ..expressions.core import Expression, Comparison, Operator, BoolVal from ..expressions.variables import _BoolVarImpl, NegBoolView, boolvar from ..expressions.globalconstraints import DirectConstraint -from ..expressions.utils import is_any_list, is_bool +from ..expressions.utils import is_any_list, is_bool, argval, argvals from ..transformations.decompose_global import decompose_in_tree from ..transformations.get_variables import get_variables from ..transformations.normalize import toplevel_list, simplify_boolean @@ -121,7 +121,8 @@ def solve(self, time_limit=None, assumptions=None): if lit in sol: cpm_var._value = bool(sol[lit]) else: - raise ValueError(f"Var {cpm_var} is unknown to the PySDD solver, this is unexpected - please report on github...") + cpm_var._value = cpm_var.get_bounds()[0] # dummy value - TODO: ensure Pysdd assigns an actual value + # cpm_var._value = None # not specified... return has_sol @@ -177,9 +178,9 @@ def solveAll(self, display=None, time_limit=None, solution_limit=None, call_from # display is not None: if isinstance(display, Expression): - print(display.value()) + print(argval(display)) elif isinstance(display, list): - print([v.value() for v in display]) + print(argvals(display)) else: display() # callback return solution_count diff --git a/cpmpy/transformations/decompose_global.py b/cpmpy/transformations/decompose_global.py index b3213cd4b..71f933e4e 100644 --- a/cpmpy/transformations/decompose_global.py +++ b/cpmpy/transformations/decompose_global.py @@ -82,7 +82,7 @@ def decompose_in_tree(lst_of_expr, supported=set(), supported_reified=set(), _to _toplevel.extend(define) # definitions should be added toplevel # the `decomposed` expression might contain other global constraints, check it - decomposed = decompose_in_tree(decomposed, supported, supported_reified, [], nested=nested) + decomposed = decompose_in_tree(decomposed, supported, supported_reified, _toplevel, nested=nested) newlist.append(all(decomposed)) else: @@ -162,7 +162,7 @@ def decompose_in_tree(lst_of_expr, supported=set(), supported_reified=set(), _to return toplevel_list(newlist) else: # we are toplevel and some new constraints are introduced, decompose new constraints! - return toplevel_list(newlist) + decompose_in_tree(_toplevel, supported, supported_reified, nested=False) + return toplevel_list(newlist) + decompose_in_tree(toplevel_list(_toplevel), supported, supported_reified, nested=False) # DEPRECATED! diff --git a/cpmpy/transformations/normalize.py b/cpmpy/transformations/normalize.py index a188e8e08..87d880718 100644 --- a/cpmpy/transformations/normalize.py +++ b/cpmpy/transformations/normalize.py @@ -147,6 +147,8 @@ def simplify_boolean(lst_of_expr, num_context=False, filter=None): """ if is_boolexpr(lhs) and is_num(rhs): # direct simplification of boolean comparisons + if isinstance(rhs, BoolVal): + rhs = int(rhs.value()) # ensure proper comparisons below if rhs < 0: newlist.append(BoolVal(name in {"!=", ">", ">="})) # all other operators evaluate to False elif rhs == 0: @@ -155,15 +157,15 @@ def simplify_boolean(lst_of_expr, num_context=False, filter=None): if name == "==" or name == "<=": newlist.append(recurse_negation(lhs)) if name == "<": - newlist.append(BoolVal(False)) + newlist.append(0 if num_context else BoolVal(False)) if name == ">=": - newlist.append(BoolVal(True)) + newlist.append(1 if num_context else BoolVal(True)) elif 0 < rhs < 1: # a floating point value if name == "==": - newlist.append(BoolVal(False)) + newlist.append(0 if num_context else BoolVal(False)) if name == "!=": - newlist.append(BoolVal(True)) + newlist.append(1 if num_context else BoolVal(True)) if name == "<" or name == "<=": newlist.append(recurse_negation(lhs)) if name == ">" or name == ">=": @@ -174,9 +176,9 @@ def simplify_boolean(lst_of_expr, num_context=False, filter=None): if name == "!=" or name == "<": newlist.append(recurse_negation(lhs)) if name == ">": - newlist.append(BoolVal(False)) + newlist.append(0 if num_context else BoolVal(False)) if name == "<=": - newlist.append(BoolVal(True)) + newlist.append(1 if num_context else BoolVal(True)) elif rhs > 1: newlist.append(BoolVal(name in {"!=", "<", "<="})) # all other operators evaluate to False else: diff --git a/tests/test_constraints.py b/tests/test_constraints.py index 123045418..0500a8209 100644 --- a/tests/test_constraints.py +++ b/tests/test_constraints.py @@ -1,3 +1,6 @@ +import inspect + +import cpmpy from cpmpy import Model, SolverLookup, BoolVal from cpmpy.expressions.globalconstraints import * from cpmpy.expressions.globalfunctions import * @@ -8,17 +11,29 @@ # make sure that `SolverLookup.get(solver)` works # also add exclusions to the 3 EXCLUDE_* below as needed SOLVERNAMES = [name for name, solver in SolverLookup.base_solvers() if solver.supported()] -SOLVERNAMES.remove('minizinc') +ALL_SOLS = False # test wheter all solutions returned by the solver satisfy the constraint # Exclude some global constraints for solvers -# Can be used when .value() method is not implemented/contains bugs -EXCLUDE_GLOBAL = {"ortools": {}, - "gurobi": {}, - "minizinc": {"circuit"}, - "pysat": {"circuit", "element","min","max","count", "nvalue", "allequal","alldifferent","cumulative","increasing","decreasing","strictly_increasing","strictly_decreasing"}, - "pysdd": {"circuit", "element","min","max","count", "nvalue", "allequal","alldifferent","cumulative","xor","increasing","decreasing","strictly_increasing","strictly_decreasing"}, - "exact": {}, - "choco": {} +NUM_GLOBAL = { + "AllEqual", "AllDifferent", "AllDifferentExcept0", "AllDifferentLists", + "Cumulative", "GlobalCardinalityCount", "InDomain", "Inverse", + "Table", "ShortTable", "Precedence", "NoOverlap", "NoOverlap2d", + "Circuit", "SubCircuit", "SubCircuitWithStart", + "Increasing", "IncreasingStrict", "Decreasing", "DecreasingStrict","LexLess", "LexLessEq", "LexChainLess", "LexChainLessEq", + # also global functions + "Abs", "Element", "Minimum", "Maximum", "Count", "NValue", "NValueExcept", "IfThenElseNum", "Among" +} + +# Solvers not supporting arithmetic constraints +SAT_SOLVERS = {"pysat", "pysdd"} + +EXCLUDE_GLOBAL = {"pysat": NUM_GLOBAL, + "pysdd": NUM_GLOBAL | {"Xor"}, + "z3": {"Inverse"}, + "choco": {"Inverse"}, + "ortools":{"Inverse"}, + "exact": {"Inverse"}, + "minizinc": {"IncreasingStrict"} # bug #813 reported on libminizinc } # Exclude certain operators for solvers. @@ -29,16 +44,6 @@ "exact": {"mod","pow","div","mul"}, } -# Some solvers only support a subset of operators in imply-constraints -# This subset can differ between left and right hand side of the implication -EXCLUDE_IMPL = {"ortools": {}, - "minizinc": {}, - "z3": {}, - "pysat": {}, - "pysdd": {}, - "exact": {"mod","pow","div","mul"}, - } - # Variables to use in the rest of the test script NUM_ARGS = [intvar(-3, 5, name=n) for n in "xyz"] # Numerical variables NN_VAR = intvar(0, 10, name="n_neg") # Non-negative variable, needed in power functions @@ -61,8 +66,7 @@ def numexprs(solver): Numexpr: - Operator (non-Boolean) with all args Var/constant (examples: +,*,/,mod,wsum) (CPMpy class 'Operator', not is_bool()) - - Global constraint (non-Boolean) (examples: Max,Min,Element) - (CPMpy class 'GlobalConstraint', not is_bool())) + - Global functions (examples: Max,Min,Element) (CPMpy class 'GlobalFunction') """ names = [(name, arity) for name, (arity, is_bool) in Operator.allowed.items() if not is_bool] if solver in EXCLUDE_OPERATORS: @@ -81,6 +85,37 @@ def numexprs(solver): yield Operator(name, operator_args) + # boolexprs are also numeric + for expr in bool_exprs(solver): + yield expr + + # also global functions + classes = inspect.getmembers(cpmpy.expressions.globalfunctions, inspect.isclass) + classes = [(name, cls) for name, cls in classes if issubclass(cls, GlobalFunction) and name != "GlobalFunction"] + classes = [(name, cls) for name, cls in classes if name not in EXCLUDE_GLOBAL.get(solver, {})] + + for name, cls in classes: + if name == "Abs": + expr = cls(NUM_ARGS[0]) + elif name == "Count": + expr = cls(NUM_ARGS, NUM_VAR) + elif name == "Element": + expr = cls(NUM_ARGS, POS_VAR) + elif name == "NValueExcept": + expr = cls(NUM_ARGS, 3) + elif name == "IfThenElseNum": + expr = cls(BOOL_VAR, NUM_ARGS[0], NUM_ARGS[1]) + elif name == "Among": + expr = cls(NUM_ARGS, [1,2]) + else: + expr = cls(NUM_ARGS) + + if solver in EXCLUDE_GLOBAL and expr.name in EXCLUDE_GLOBAL[solver]: + continue + else: + yield expr + + # Generate all possible comparison constraints def comp_constraints(solver): @@ -93,30 +128,19 @@ def comp_constraints(solver): - Numeric inequality (>=,>,<,<=): Numexpr >=< Var (CPMpy class 'Comparison') """ for comp_name in Comparison.allowed: + for numexpr in numexprs(solver): - for rhs in [NUM_VAR, BOOL_VAR, 1, BoolVal(True)]: + # numeric vs bool/num var/val (incl global func) + lb, ub = get_bounds(numexpr) + for rhs in [NUM_VAR, BOOL_VAR, BoolVal(True), 1]: + if solver in SAT_SOLVERS and not is_num(rhs): + continue + if comp_name == ">" and ub <= get_bounds(rhs)[1]: + continue + if comp_name == "<" and lb >= get_bounds(rhs)[0]: + continue yield Comparison(comp_name, numexpr, rhs) - for comp_name in Comparison.allowed: - for glob_expr in global_constraints(solver): - if not glob_expr.is_bool(): - for rhs in [NUM_VAR, BOOL_VAR, 1, BoolVal(True)]: - if comp_name == "<" and get_bounds(glob_expr)[0] >= get_bounds(rhs)[1]: - continue - yield Comparison(comp_name, glob_expr, rhs) - - if solver == "z3": - for comp_name in Comparison.allowed: - for boolexpr in bool_exprs(solver): - for rhs in [NUM_VAR, BOOL_VAR, 1, BoolVal(True)]: - if comp_name == '>': - # >1 is unsat for boolean expressions, so change it to 0 - if isinstance(rhs, int) and rhs == 1: - rhs = 0 - if isinstance(rhs, BoolVal) and rhs.args[0] == True: - rhs = BoolVal(False) - yield Comparison(comp_name, boolexpr, rhs) - # Generate all possible boolean expressions def bool_exprs(solver): @@ -124,6 +148,7 @@ def bool_exprs(solver): Generate all boolean expressions: - Boolean operators: and([Var]), or([Var]) (CPMpy class 'Operator', is_bool()) - Boolean equality: Var == Var (CPMpy class 'Comparison') + - Global constraints """ names = [(name, arity) for name, (arity, is_bool) in Operator.allowed.items() if is_bool] @@ -144,38 +169,95 @@ def bool_exprs(solver): yield Comparison(eq_name, *BOOL_ARGS[:2]) for cpm_cons in global_constraints(solver): - if cpm_cons.is_bool(): - yield cpm_cons + yield cpm_cons def global_constraints(solver): """ Generate all global constraints - - AllDifferent, AllEqual, Circuit, Minimum, Maximum, Element, - Xor, Cumulative, NValue, Count + - AllDifferent, AllEqual, Circuit, SubCircuit, SubCircuitWithStart, Minimum, Maximum, Element, + Xor, Cumulative, NValue, Count, Increasing, Decreasing, IncreasingStrict, DecreasingStrict, LexLessEq, LexLess """ - global_cons = [AllDifferent, AllEqual, Minimum, Maximum, NValue, Increasing, Decreasing, IncreasingStrict, DecreasingStrict] - for global_type in global_cons: - cons = global_type(NUM_ARGS) - if solver not in EXCLUDE_GLOBAL or cons.name not in EXCLUDE_GLOBAL[solver]: - yield cons - - # "special" constructors - if solver not in EXCLUDE_GLOBAL or "element" not in EXCLUDE_GLOBAL[solver]: - yield cpm_array(NUM_ARGS)[NUM_VAR] - - if solver not in EXCLUDE_GLOBAL or "xor" not in EXCLUDE_GLOBAL[solver]: - yield Xor(BOOL_ARGS) - - if solver not in EXCLUDE_GLOBAL or "count" not in EXCLUDE_GLOBAL[solver]: - yield Count(NUM_ARGS, NUM_VAR) - - if solver not in EXCLUDE_GLOBAL or "cumulative" not in EXCLUDE_GLOBAL[solver]: - s = intvar(0,10,shape=3,name="start") - e = intvar(0,10,shape=3,name="end") - dur = [1,4,3] - demand = [4,5,7] - cap = 10 - yield Cumulative(s, dur, e, demand, cap) + classes = inspect.getmembers(cpmpy.expressions.globalconstraints, inspect.isclass) + classes = [(name, cls) for name, cls in classes if issubclass(cls, GlobalConstraint) and name != "GlobalConstraint"] + classes = [(name, cls) for name, cls in classes if name not in EXCLUDE_GLOBAL.get(solver, {})] + + for name, cls in classes: + + if name == "Xor": + expr = cls(BOOL_ARGS) + elif name == "Inverse": + expr = cls(NUM_ARGS, [1,0,2]) + elif name == "Table": + expr = cls(NUM_ARGS, [[0,1,2],[1,2,0],[1,0,2]]) + elif name == "ShortTable": + expr = cls(NUM_ARGS, [[0,"*",2], ["*","*",1]]) + elif name == "IfThenElse": + expr = cls(*BOOL_ARGS) + elif name == "InDomain": + expr = cls(NUM_VAR, [0,1,6]) + elif name == "Cumulative": + s = intvar(0, 10, shape=3, name="start") + e = intvar(0, 10, shape=3, name="end") + dur = [1, 4, 3] + demand = [4, 5, 7] + cap = 10 + expr = Cumulative(s, dur, e, demand, cap) + elif name == "Circuit": + S = intvar(0, 9, shape=10) + expr = Circuit(S) + elif name == "SubCircuit": + S = intvar(0, 9, shape=10) + expr = SubCircuit(S) + elif name == "SubCircuitWithStart": + S = intvar(0, 9, shape=10) + expr = SubCircuitWithStart(S, start_index=0) + elif name == "Precedence": + x = intvar(0,5, shape=3, name="x") + expr = cls(x, [3,1,0]) + elif name == "NoOverlap": + s = intvar(0, 10, shape=3, name="start") + e = intvar(0, 10, shape=3, name="end") + dur = [1,4,3] + expr = cls(s, dur, e) + elif name == "NoOverlap2d": + start_x = intvar(0,10, shape=3, name="startx") + start_y = intvar(0,10, shape=3, name="starty") + end_x = intvar(0,10, shape=3, name="endx") + end_y = intvar(0,10, shape=3, name="endy") + dur_x = [3,4,5] + dur_y = intvar(3,5, shape=3, name="ly") + expr = cls(start_x, dur_x, end_x, start_y, dur_y, end_y) + elif name == "GlobalCardinalityCount": + vals = [1, 2, 3] + cnts = intvar(0,10,shape=3) + expr = cls(NUM_ARGS, vals, cnts) + elif name == "LexLessEq": + X = intvar(0, 3, shape=3) + Y = intvar(0, 3, shape=3) + expr = LexLessEq(X, Y) + + elif name == "LexLess": + X = intvar(0, 3, shape=3) + Y = intvar(0, 3, shape=3) + expr = LexLess(X, Y) + + elif name == "LexChainLess": + X = intvar(0, 3, shape=(3,3)) + expr = LexChainLess(X) + + elif name == "LexChainLessEq": + X = intvar(0, 3, shape=(3,3)) + expr = LexChainLess(X) + elif name == "AllDifferentLists": + vars = intvar(0,10, shape=(3,4)) + expr = cls(vars) + else: # default constructor, list of numvars + expr= cls(NUM_ARGS) + + if solver in EXCLUDE_GLOBAL and name in EXCLUDE_GLOBAL[solver]: + continue + else: + yield expr def reify_imply_exprs(solver): @@ -185,44 +267,59 @@ def reify_imply_exprs(solver): Var -> Boolexpr (CPMpy class 'Operator', is_bool()) """ for bool_expr in bool_exprs(solver): - if solver not in EXCLUDE_IMPL or \ - bool_expr.name not in EXCLUDE_IMPL[solver]: - yield bool_expr.implies(BOOL_VAR) - yield BOOL_VAR.implies(bool_expr) - yield bool_expr == BOOL_VAR + yield bool_expr.implies(BOOL_VAR) + yield BOOL_VAR.implies(bool_expr) + yield bool_expr == BOOL_VAR for comp_expr in comp_constraints(solver): lhs, rhs = comp_expr.args - if solver not in EXCLUDE_IMPL or \ - (not isinstance(lhs, Expression) or lhs.name not in EXCLUDE_IMPL[solver]) and \ - (not isinstance(rhs, Expression) or rhs.name not in EXCLUDE_IMPL[solver]): - yield comp_expr.implies(BOOL_VAR) - yield BOOL_VAR.implies(comp_expr) - yield comp_expr == BOOL_VAR + yield comp_expr.implies(BOOL_VAR) + yield BOOL_VAR.implies(comp_expr) + yield comp_expr == BOOL_VAR + + +def verify(cons): + assert argval(cons) + assert cons.value() -@pytest.mark.parametrize(("solver","constraint"),_generate_inputs(bool_exprs), ids=str) +@pytest.mark.parametrize(("solver","constraint"),list(_generate_inputs(bool_exprs)), ids=str) def test_bool_constaints(solver, constraint): """ Tests boolean constraint by posting it to the solver and checking the value after solve. """ - assert SolverLookup.get(solver, Model(constraint)).solve() - assert constraint.value() + if ALL_SOLS: + n_sols = SolverLookup.get(solver, Model(constraint)).solveAll(display=lambda: verify(constraint)) + assert n_sols >= 1 + else: + assert SolverLookup.get(solver, Model(constraint)).solve() + assert argval(constraint) + assert constraint.value() -@pytest.mark.parametrize(("solver","constraint"), _generate_inputs(comp_constraints), ids=str) +@pytest.mark.parametrize(("solver","constraint"), list(_generate_inputs(comp_constraints)), ids=str) def test_comparison_constraints(solver, constraint): """ Tests comparison constraint by posting it to the solver and checking the value after solve. """ - assert SolverLookup.get(solver,Model(constraint)).solve() - assert constraint.value() + if ALL_SOLS: + n_sols = SolverLookup.get(solver, Model(constraint)).solveAll(display= lambda: verify(constraint)) + assert n_sols >= 1 + else: + assert SolverLookup.get(solver,Model(constraint)).solve() + assert argval(constraint) + assert constraint.value() -@pytest.mark.parametrize(("solver","constraint"), _generate_inputs(reify_imply_exprs), ids=str) +@pytest.mark.parametrize(("solver","constraint"), list(_generate_inputs(reify_imply_exprs)), ids=str) def test_reify_imply_constraints(solver, constraint): """ Tests boolean expression by posting it to solver and checking the value after solve. """ - assert SolverLookup.get(solver, Model(constraint)).solve() - assert constraint.value() + if ALL_SOLS: + n_sols = SolverLookup.get(solver, Model(constraint)).solveAll(display=lambda: verify(constraint)) + assert n_sols >= 1 + else: + assert SolverLookup.get(solver, Model(constraint)).solve() + assert argval(constraint) + assert constraint.value() diff --git a/tests/test_expressions.py b/tests/test_expressions.py index 8921aa5ea..7ff22e88e 100644 --- a/tests/test_expressions.py +++ b/tests/test_expressions.py @@ -6,7 +6,7 @@ from cpmpy.expressions import * from cpmpy.expressions.variables import NDVarArray from cpmpy.expressions.core import Operator, Expression -from cpmpy.expressions.utils import get_bounds +from cpmpy.expressions.utils import get_bounds, argval class TestComparison(unittest.TestCase): def test_comps(self): @@ -437,6 +437,7 @@ def test_incomplete_func(self): if cp.SolverLookup.lookup("z3").supported(): self.assertTrue(m.solve(solver="z3")) # ortools does not support divisor spanning 0 work here self.assertRaises(IncompleteFunctionError, cons.value) + self.assertFalse(argval(cons)) # mayhem cons = (arr[10 // (a - b)] == 1).implies(p) diff --git a/tests/test_globalconstraints.py b/tests/test_globalconstraints.py index 6a7b6cb90..e01d465fd 100644 --- a/tests/test_globalconstraints.py +++ b/tests/test_globalconstraints.py @@ -55,6 +55,26 @@ def test_alldifferent2(self): var._value = val assert (c.value() == oracle), f"Wrong value function for {vals,oracle}" + def test_alldifferent_lists(self): + # test known input/outputs + tuples = [ + ([(1,2,3),(1,3,3),(1,2,4)], True), + ([(1,2,3),(1,3,3),(1,2,3)], False), + ([(0,0,3),(1,3,3),(1,2,4)], True), + ([(1,2,3),(1,3,3),(3,3,3)], True) + ] + iv = cp.intvar(0,4, shape=(3,3)) + c = cp.AllDifferentLists(iv) + for (vals, oracle) in tuples: + ret = cp.Model(c, iv == vals).solve() + assert (ret == oracle), f"Mismatch solve for {vals,oracle}" + # don't try this at home, forcibly overwrite variable values (so even when ret=false) + for (var,val) in zip(iv,vals): + for (vr, vl) in zip(var, val): + vr._value = vl + assert (c.value() == oracle), f"Wrong value function for {vals,oracle}" + + def test_not_alldifferent(self): # from fuzztester of Ruben Kindt, #143 pos = cp.intvar(lb=0, ub=5, shape=3, name="positions") @@ -169,6 +189,153 @@ def test_not_circuit(self): self.assertEqual(total, len(circuit_sols) + len(not_circuit_sols)) + def test_subcircuit(self): + + import numpy as np + + n = 6 + + # Find a subcircuit + x = cp.intvar(0, n-1, n) + model = cp.Model( [cp.SubCircuit(x)] ) + self.assertTrue(model.solve()) + self.assertTrue(cp.SubCircuit(x).value()) + self.assertTrue(model.solveAll() == 410) + + # Find a max subcircuit (subcircuit = circuit) + x = cp.intvar(0, n-1, n) + model = cp.Model( [cp.SubCircuit(x)] + list(x != np.arange(n)) ) + self.assertTrue(model.solve()) + self.assertTrue(cp.SubCircuit(x).value()) + self.assertTrue(circuit_length(x.value()) == n) + self.assertTrue(model.solveAll() == 120) # 5 x 4 x 3 x 2 x 1 + + # Find a non-max subcircuit + x = cp.intvar(0, n-1, n) + model = cp.Model( [cp.SubCircuit(x)] + [x[0] == 0] ) # Often index 0 is assumed to be the start_index internally + self.assertTrue(model.solve()) + self.assertTrue(cp.SubCircuit(x).value()) + self.assertTrue(circuit_length(x.value()) < n) + self.assertTrue(model.solveAll() == 85) + + # Find an empty subcircuit + x = cp.intvar(0, n-1, n) + sc = cp.SubCircuit(x) + model = cp.Model( [sc] + list(x == np.arange(n)) ) + self.assertTrue(model.solve()) + self.assertTrue(cp.SubCircuit(x).value()) + self.assertTrue(circuit_length(x.value()) == 0) + self.assertTrue(model.solveAll() == 1) + + # Find a non-empty subcircuit + x = cp.intvar(0, n-1, n) + model = cp.Model( [cp.SubCircuit(x)] + [x[0] != 0] ) + self.assertTrue(model.solve()) + self.assertTrue(cp.SubCircuit(x).value()) + self.assertTrue(circuit_length(x.value()) > 1) + self.assertTrue(model.solveAll() == 325) + + # Unsat subcircuit + x = cp.intvar(0, n-1, n) + model = cp.Model( [cp.SubCircuit(x)] + [x[0] == 1, x[1] == 1] ) # 0 -> 1 -> 1 + self.assertTrue(not model.solve()) + + def test_subcircuit_reified(self): + + import numpy as np + + n = 6 + + # Find a subcircuit + x = cp.intvar(0, n-1, n) + a = cp.boolvar() + model = cp.Model([a.implies(cp.SubCircuit(x)), a == True]) + self.assertTrue(model.solve()) + self.assertTrue(cp.SubCircuit(x).value()) + self.assertTrue(model.solveAll() == 410) + + # Find a max subcircuit (subcircuit = circuit) + x = cp.intvar(0, n-1, n) + a = cp.boolvar() + model = cp.Model( [a.implies(cp.SubCircuit(x)), a == True] + list(x != np.arange(n)) ) + self.assertTrue(model.solve()) + self.assertTrue(cp.SubCircuit(x).value()) + self.assertTrue(circuit_length(x.value()) == n) + self.assertTrue(model.solveAll() == 120) # 5 x 4 x 3 x 2 x 1 + + # Find a non-max subcircuit + x = cp.intvar(0, n-1, n) + a = cp.boolvar() + model = cp.Model( [a.implies(cp.SubCircuit(x)), a == True] + [x[0] == 0] ) # Often index 0 is assumed to be the start_index internally + self.assertTrue(model.solve()) + self.assertTrue(cp.SubCircuit(x).value()) + self.assertTrue(circuit_length(x.value()) < n) + self.assertTrue(model.solveAll() == 85) + + # Find an empty subcircuit + x = cp.intvar(0, n-1, n) + a = cp.boolvar() + model = cp.Model( [a.implies(cp.SubCircuit(x)), a == True] + list(x == np.arange(n)) ) + self.assertTrue(model.solve()) + self.assertTrue(cp.SubCircuit(x).value()) + self.assertTrue(circuit_length(x.value()) == 0) + self.assertTrue(model.solveAll() == 1) + + # Find a non-empty subcircuit + x = cp.intvar(0, n-1, n) + a = cp.boolvar() + model = cp.Model( [a.implies(cp.SubCircuit(x)), a == True] + [x[0] != 0] ) + self.assertTrue(model.solve()) + self.assertTrue(cp.SubCircuit(x).value()) + self.assertTrue(circuit_length(x.value()) > 1) + self.assertTrue(model.solveAll() == 325) + + # Unsat subcircuit + x = cp.intvar(0, n-1, n) + a = cp.boolvar() + model = cp.Model( [a.implies(cp.SubCircuit(x)), a == True] + [x[0] == 1, x[1] == 1] ) # 0 -> 1 -> 1 + self.assertTrue(not model.solve()) + + # Unsat subcircuit + x = cp.intvar(0, n-1, n) + a = cp.boolvar() + model = cp.Model( [a.implies(cp.SubCircuit(x))] + [x[0] == 1, x[1] == 1] ) # 0 -> 1 -> 1 + self.assertTrue(model.solve()) + self.assertTrue(a.value() == False) + + def test_subcircuit_choco(self): + """ + See issue #1095: https://github.com/chocoteam/choco-solver/issues/1095 + """ + + n = 3 + x = cp.intvar(0, n-1, n) + a = cp.boolvar() + + model = cp.Model([a.implies(cp.SubCircuit(x)), a == True] + [(x[0] == 2), (x[1] == 1), (x[2] == 0)]) + assert( model.solve() ) + + model = cp.Model([a.implies(cp.SubCircuit(x)), a == True] + [(x[0] != 0), (x[1] == 1), (x[2] != 2)]) + assert( model.solve() ) + + def test_subcircuitwithstart(self): + n = 5 + x = cp.intvar(0, n-1, n) + + # Test satisfiability + model = cp.Model( [cp.SubCircuitWithStart(x)] ) + self.assertTrue( model.solve() ) + self.assertTrue( cp.SubCircuitWithStart(x).value() ) + + # Test default start position of 0 + model = cp.Model( [cp.SubCircuitWithStart(x)] + [x[0] == 0] ) # force default start_index 0 to not be in the circuit + self.assertFalse( model.solve() ) + + # Test start position + start_index = 3 + model = cp.Model( [cp.SubCircuitWithStart(x, start_index=start_index)] + [x[start_index] == start_index] ) # force start_index to not be in the circuit + self.assertFalse(model.solve()) + def test_inverse(self): # Arrays @@ -253,6 +420,78 @@ def test_InDomain(self): self.assertTrue(model.solve()) self.assertIn(bv.value(), vals) + def test_lex_lesseq(self): + from cpmpy import BoolVal + X = cp.intvar(0, 3, shape=10) + c1 = X[:-1] == 1 + Y = [1, 1, 1, 1, 1, 1, 1, 1, 1, 1] + c = cp.LexLessEq(X, Y) + c2 = c != (BoolVal(True)) + m = cp.Model([c1, c2]) + self.assertTrue(m.solve()) + self.assertTrue(c2.value()) + self.assertFalse(c.value()) + + Y = cp.intvar(0, 0, shape=10) + c = cp.LexLessEq(X, Y) + m = cp.Model(c) + self.assertTrue(m.solve("ortools")) + from cpmpy.expressions.utils import argval + self.assertTrue(sum(argval(X)) == 0) + + def test_lex_less(self): + from cpmpy import BoolVal + X = cp.intvar(0, 3, shape=10) + c1 = X[:-1] == 1 + Y = [1, 1, 1, 1, 1, 1, 1, 1, 1, 1] + c = cp.LexLess(X, Y) + c2 = c != (BoolVal(True)) + m = cp.Model([c1, c2]) + self.assertTrue(m.solve()) + self.assertTrue(c2.value()) + self.assertFalse(c.value()) + + Y = cp.intvar(0, 0, shape=10) + c = cp.LexLess(X, Y) + m = cp.Model(c) + self.assertFalse(m.solve("ortools")) + + Z = [0, 0, 0, 0, 0, 0, 0, 0, 0, 1] + c = cp.LexLess(X, Z) + m = cp.Model(c) + self.assertTrue(m.solve("ortools")) + from cpmpy.expressions.utils import argval + self.assertTrue(sum(argval(X)) == 0) + + + def test_lex_chain(self): + from cpmpy import BoolVal + X = cp.intvar(0, 3, shape=10) + c1 = X[:-1] == 1 + Y = [1, 1, 1, 1, 1, 1, 1, 1, 1, 1] + c = cp.LexChainLess([X, Y]) + c2 = c != (BoolVal(True)) + m = cp.Model([c1, c2]) + self.assertTrue(m.solve()) + self.assertTrue(c2.value()) + self.assertFalse(c.value()) + + Y = cp.intvar(0, 0, shape=10) + c = cp.LexChainLessEq([X, Y]) + m = cp.Model(c) + self.assertTrue(m.solve("ortools")) + from cpmpy.expressions.utils import argval + self.assertTrue(sum(argval(X)) == 0) + + Z = cp.intvar(0, 1, shape=(3,2)) + c = cp.LexChainLess(Z) + m = cp.Model(c) + self.assertTrue(m.solve()) + self.assertTrue(sum(argval(Z[0])) == 0) + self.assertTrue(sum(argval(Z[1])) == 1) + self.assertTrue(sum(argval(Z[2])) >= 1) + + def test_indomain_onearg(self): iv = cp.intvar(0, 10) @@ -736,6 +975,32 @@ def check_true(): cp.Model(cons).solveAll(solver='minizinc') + + def test_precedence(self): + iv = cp.intvar(0,5, shape=6, name="x") + + cons = cp.Precedence(iv, [0,2,1]) + self.assertTrue(cp.Model([cons, iv == [5,0,2,0,0,1]]).solve()) + self.assertTrue(cons.value()) + self.assertTrue(cp.Model([cons, iv == [0,0,0,0,0,0]]).solve()) + self.assertTrue(cons.value()) + self.assertFalse(cp.Model([cons, iv == [0,1,2,0,0,0]]).solve()) + + + def test_no_overlap(self): + start = cp.intvar(0,5, shape=3) + end = cp.intvar(0,5, shape=3) + cons = cp.NoOverlap(start, [2,1,1], end) + self.assertTrue(cp.Model(cons).solve()) + self.assertTrue(cons.value()) + self.assertTrue(cp.Model(cons.decompose()).solve()) + self.assertTrue(cons.value()) + + def check_val(): + assert cons.value() is False + + cp.Model(~cons).solveAll(display=check_val) + class TestBounds(unittest.TestCase): def test_bounds_minimum(self): x = cp.intvar(-8, 8) @@ -963,7 +1228,7 @@ def test_gcc(self): b = cp.boolvar() a = cp.boolvar() - self.assertTrue(cp.Model([cp.GlobalCardinalityCount([x,y], [z,q], [h,v])]).solve()) + # type checks self.assertRaises(TypeError, cp.GlobalCardinalityCount, [x,y], [x,False], [h,v]) self.assertRaises(TypeError, cp.GlobalCardinalityCount, [x,y], [z,b], [h,v]) self.assertRaises(TypeError, cp.GlobalCardinalityCount, [b,a], [a,b], [h,v]) @@ -971,6 +1236,13 @@ def test_gcc(self): self.assertRaises(TypeError, cp.GlobalCardinalityCount, [x, y], [x, h], [True, v]) self.assertRaises(TypeError, cp.GlobalCardinalityCount, [x, y], [x, h], [v, a]) + iv = cp.intvar(0,10, shape=3) + SOLVERNAMES = [name for name, solver in cp.SolverLookup.base_solvers() if solver.supported()] + for name in SOLVERNAMES: + if name in ("pysat", "pysdd"): continue + self.assertTrue(cp.Model([cp.GlobalCardinalityCount(iv, [1,4], [1,1])]).solve(solver=name)) + # test closed version + self.assertFalse(cp.Model(cp.GlobalCardinalityCount(iv, [1,4], [0,0], closed=True)).solve(solver=name)) def test_count(self): x = cp.intvar(0, 1) @@ -983,6 +1255,23 @@ def test_count(self): self.assertTrue(cp.Model([cp.Count([x,y],z) == 1]).solve()) self.assertRaises(TypeError, cp.Count, [x,y],[x,False]) + def test_among(self): + + iv = cp.intvar(0,10, shape=3, name="x") + + for name, cls in cp.SolverLookup.base_solvers(): + + if cls.supported() is False: + continue + try: + self.assertTrue(cp.Model([cp.Among(iv, [1,2]) == 3]).solve(solver=name)) + self.assertTrue(all(x.value() in [1,2] for x in iv)) + self.assertTrue(cp.Model([cp.Among(iv, [1,100]) > 2]).solve(solver=name)) + self.assertTrue(all(x.value() == 1 for x in iv)) + except NotSupportedError: + continue + + def test_table(self): iv = cp.intvar(-8,8,3) @@ -993,3 +1282,25 @@ def test_table(self): self.assertRaises(TypeError, cp.Table, [iv[0], iv[1], iv[2], 5], [(5, 2, 2)]) self.assertRaises(TypeError, cp.Table, [iv[0], iv[1], iv[2], [5]], [(5, 2, 2)]) self.assertRaises(TypeError, cp.Table, [iv[0], iv[1], iv[2], ['a']], [(5, 2, 2)]) + +def circuit_length(succ): + # Find a start_index + start_index = None + for i,s in enumerate(succ): + if i != s: + # first non self-loop found is taken as start + start_index = i + break + # No valid start found, thus empty subcircuit + if start_index is None: + return 0 + + # Collect subcircuit + visited = set([start_index]) + idx = succ[start_index] + while idx != start_index: + # Collect + visited.add(idx) + idx = succ[idx] + + return len(visited) diff --git a/tests/test_solvers.py b/tests/test_solvers.py index 38136db1d..55108c91d 100644 --- a/tests/test_solvers.py +++ b/tests/test_solvers.py @@ -693,7 +693,7 @@ def test_vars_not_removed(self): #test unique sols, should be same number self.assertEqual(len(sols),8) - + @pytest.mark.skipif(not CPM_minizinc.supported(), reason="Minizinc not installed") def test_count_mzn(self): @@ -707,4 +707,3 @@ def test_count_mzn(self): m = cp.Model([x + y == 2, wsum == 9]) self.assertTrue(m.solve(solver="minizinc")) - diff --git a/tests/test_trans_simplify.py b/tests/test_trans_simplify.py index b44c980ef..454e0c0f7 100644 --- a/tests/test_trans_simplify.py +++ b/tests/test_trans_simplify.py @@ -100,3 +100,11 @@ def test_with_floats(self): self.assertEqual(str(self.transform(expr)), '[(iv[0]) == (iv[1])]') + def test_nested_boolval(self): + + bv = cp.boolvar(name="bv") + x = cp.intvar(0, 3, name="x") + cons = (x == 2) == (bv == 4) + self.assertEquals(str(self.transform(cons)), "[x != 2]") + self.assertTrue(cp.Model(cons).solve()) + diff --git a/xcsp3/executable/callbacks.py b/xcsp3/executable/callbacks.py index 9d707ec8e..9534f5e81 100644 --- a/xcsp3/executable/callbacks.py +++ b/xcsp3/executable/callbacks.py @@ -12,7 +12,7 @@ from pycsp3.tools.utilities import _Star import cpmpy as cp -from cpmpy.expressions.utils import is_any_list, get_bounds +from cpmpy.expressions.utils import is_any_list, get_bounds, is_boolexpr class CallbacksCPMPy(Callbacks): @@ -24,11 +24,6 @@ def __init__(self): self.print_general_methods = False self.print_specific_methods = False - def get_condition(self, condition): - map = {"LT": "<", "LE": "<=", "EQ": "=", "GE": ">=", "GT": ">"} - if condition.operator.name not in map: - raise ValueError("Unknown condition operator", condition.operator.name, "expected any of", set(map.keys())) - def var_integer_range(self, x: Variable, min_value: int, max_value: int): if min_value == 0 and max_value == 1: #boolvar @@ -95,9 +90,19 @@ def ctr_intension(self, scope: list[Variable], tree: Node): "iff": (0, lambda x: cp.all(a == b for a, b in zip(x[:-1], x[1:]))), "imp": (2, lambda x, y: x.implies(y)), # control - "if": (3, lambda b, x, y: cp.IfThenElse(b, x, y)) + "if": (3, lambda b, x, y: cp.IfThenElse(b, x, y) if is_boolexpr(x) and is_boolexpr(y) + else cp.IfThenElseNum(b,x,y)) } + def eval_cpm_comp(self, lhs, op:TypeConditionOperator, rhs): + arity, cpm_op = self.funcmap[op.name.lower()] + if arity == 2: + return cpm_op(lhs, rhs) + elif arity == 0: + return cpm_op([lhs,rhs]) + else: + raise ValueError(f"Expected operator of arity 0 or 2 but got {cpm_op} which is of arity {arity}") + def intentionfromtree(self, node): if isinstance(node, Node): if node.type.lowercase_name == 'var': @@ -116,14 +121,8 @@ def intentionfromtree(self, node): def ctr_primitive1a(self, x: Variable, op: TypeConditionOperator, k: int): assert op.is_rel() - x = self.get_cpm_var(x) - arity, cpm_op = self.funcmap[op.name.lower()] - if arity == 2: - self.cpm_model += cpm_op(x, k) - elif arity == 0: - self.cpm_model += cpm_op([x, k]) - else: - self._unimplemented(x, op, k) + cpm_x = self.get_cpm_var(x) + self.cpm_model += self.eval_cpm_comp(cpm_x, op, k) def ctr_primitive1b(self, x: Variable, op: TypeConditionOperator, term: list[int] | range): assert op.is_set() @@ -175,14 +174,30 @@ def ctr_primitive3(self, x: Variable, aop: TypeArithmeticOperator, y: Variable, self.cpm_model += cpm_op([cpm_aop([x, y]), z]) def ctr_logic(self, lop: TypeLogicalOperator, scope: list[Variable]): # lop(scope) - self._unimplemented(lop, scope) + if lop == TypeLogicalOperator.AND: + self.cpm_model += self.get_cpm_vars(scope) + elif lop == TypeLogicalOperator.OR: + self.cpm_model += cp.any(self.get_cpm_vars(scope)) + elif lop ==TypeLogicalOperator.IFF: + assert len(scope) == 2 + a,b = scope + self.cpm_model += self.get_cpm_var(a) == self.get_cpm_var(b) + elif lop == TypeLogicalOperator.IMP: + assert len(scope) == 2 + a,b = scope + self.cpm_model += self.get_cpm_var(a).implies(self.get_cpm_var(b)) + elif lop == TypeLogicalOperator.XOR: + self.cpm_model += cp.Xor(self.get_cpm_vars(scope)) + else: + self._unimplemented(lop, scope) def ctr_logic_reif(self, x: Variable, y: Variable, op: TypeConditionOperator, k: int | Variable): # x = y k assert op.is_rel() - self._unimplemented(x, y, op, k) + cpm_x, cpm_y, cpm_k = self.get_cpm_vars([x,y, k]) + self.cpm_model += self.eval_cpm_comp(cpm_x == cpm_y, op, cpm_k) def ctr_logic_eqne(self, x: Variable, op: TypeConditionOperator, lop: TypeLogicalOperator, scope: list[Variable]): # x = lop(scope) or x != lop(scope) - assert op in (TypeConditionOperator.EQ, TypeConditionOperator.NE) + assert op in (TypeConditionOperator.EQ, TypeConditionOperator.NE) # TODO: what is this??? self._unimplemented(x, op, lop, scope) def ctr_extension_unary(self, x: Variable, values: list[int], positive: bool, flags: set[str]): @@ -220,28 +235,27 @@ def strwildcard(x): def ctr_regular(self, scope: list[Variable], transitions: list, start_state: str, final_states: list[str]): - #raise NotImplementedError('no cpmpy equivalent yet') - pass - #self._unimplemented(scope, transitions, start_state, final_states) + # return + self._unimplemented(scope, transitions, start_state, final_states) # TODO: add after Helene PR def ctr_mdd(self, scope: list[Variable], transitions: list): - #raise NotImplementedError('no cpmpy equivalent yet') - #self._unimplemented(scope, transitions) - pass + self._unimplemented(scope, transitions) # TODO: add after Helene PR def ctr_all_different(self, scope: list[Variable] | list[Node], excepting: None | list[int]): + cpm_exprs = self.get_cpm_exprs(scope) if excepting is None: - cpm_exprs = self.exprs_from_node(scope) - return cp.AllDifferent(cpm_exprs) + self.cpm_model += cp.AllDifferent(cpm_exprs) elif excepting == [0]: - return cp.AllDifferentExcept0(self.exprs_from_node(scope)) + self.cpm_model += cp.AllDifferentExcept0(cpm_exprs) else: - self._unimplemented(scope, excepting) + self._unimplemented(scope, excepting) # TODO: parse to AllDifferentExceptN def ctr_all_different_lists(self, lists: list[list[Variable]], excepting: None | list[list[int]]): - self._unimplemented(lists, excepting) + self.cpm_model += cp.AllDifferentLists([self.get_cpm_vars(lst) for lst in lists]) # TODO: what about the excepting arg?? - def ctr_all_different_matrix(self, matrix: list[list[Variable]], excepting: None | list[int]): + def ctr_all_different_matrix(self, matrix: list[list[Variable]], excepting: None | list[int]): # TODO check this... + # TODO: ignace: I'm pretty sure this is incorrect... + # Have to check but think its alldiff on rows and alldiff on cols if excepting is None: cpm_exprs = self.exprs_from_node(matrix) return cp.AllDifferent(cpm_exprs) @@ -254,23 +268,45 @@ def ctr_all_equal(self, scope: list[Variable] | list[Node], excepting: None | li self.cpm_model += cp.AllEqual(self.get_cpm_exprs(scope)) def ctr_ordered(self, lst: list[Variable], operator: TypeOrderedOperator, lengths: None | list[int] | list[Variable]): - #raise NotImplementedError('Increasing global not in cpmpy') - pass - #self._unimplemented(lst, operator, lengths) + cpm_vars = self.get_cpm_vars(lst) + if operator == TypeOrderedOperator.INCREASING: + self.cpm_model += cp.Increasing(cpm_vars) + elif operator == TypeOrderedOperator.STRICTLY_INCREASING: + self.cpm_model += cp.IncreasingStrict(cpm_vars) + elif operator == TypeOrderedOperator.DECREASING: + self.cpm_model += cp.Decreasing(cpm_vars) + elif operator == TypeOrderedOperator.STRICTLY_DECREASING: + self.cpm_model += cp.DecreasingStrict(cpm_vars) + else: + self._unimplemented(lst, operator, lengths) def ctr_lex_limit(self, lst: list[Variable], limit: list[int], operator: TypeOrderedOperator): # should soon enter XCSP3-core self._unimplemented(lst, limit, operator) def ctr_lex(self, lists: list[list[Variable]], operator: TypeOrderedOperator): - pass - #self._unimplemented(lists, operator) + cpm_lists = [self.get_cpm_vars(lst) for lst in lists] + if operator == TypeOrderedOperator.STRICTLY_INCREASING: + self.cpm_model += cp.LexChainLess(cpm_lists) + elif operator == TypeOrderedOperator.INCREASING: + self.cpm_model += cp.LexChainLessEq(cpm_lists) + elif operator == TypeOrderedOperator.STRICTLY_DECREASING: + rev_lsts = [list(reversed(lst)) for lst in cpm_lists] + self.cpm_model += cp.LexChainLess(rev_lsts) + elif operator == TypeOrderedOperator.DECREASING: + rev_lsts = [list(reversed(lst)) for lst in cpm_lists] + self.cpm_model += cp.LexChainLessEq(rev_lsts) + else: + self._unimplemented(lists, operator) def ctr_lex_matrix(self, matrix: list[list[Variable]], operator: TypeOrderedOperator): - pass - #self._unimplemented(matrix, operator) + import numpy as np + # lex_chain on rows + self.ctr_lex(matrix, operator) + # lex chain on columns + self.ctr_lex(np.array(matrix).T.tolist(), operator) def ctr_precedence(self, lst: list[Variable], values: None | list[int], covered: bool): - self._unimplemented(lst, values, covered) + self._unimplemented(lst, values, covered) # TODO: after merge of Ignace PR def ctr_sum(self, lst: list[Variable] | list[Node], coefficients: None | list[int] | list[Variable], condition: Condition): cpm_vars = [] @@ -318,8 +354,7 @@ def ctr_exactly(self, lst: list[Variable], value: int, k: int | Variable): self.cpm_model += (cp.Count(cpm_vars, value) == k) def ctr_among(self, lst: list[Variable], values: list[int], k: int | Variable): - pass - #self._unimplemented(lst, values, k) + self.cpm_model += cp.Among(self.get_cpm_vars(lst), values) == self.get_cpm_var(k) def ctr_nvalues(self, lst: list[Variable] | list[Node], excepting: None | list[int], condition: Condition): arity, op = self.funcmap[condition.operator.name.lower()] @@ -336,28 +371,24 @@ def ctr_not_all_qual(self, lst: list[Variable]): self.cpm_model += ~cp.AllEqual(cpm_vars) def ctr_cardinality(self, lst: list[Variable], values: list[int] | list[Variable], occurs: list[int] | list[Variable] | list[range], closed: bool): - if closed == False: - self.cpm_model += cp.GlobalCardinalityCount(self.get_cpm_exprs(lst), self.get_cpm_exprs(values), self.get_cpm_exprs(occurs)) - else: - self._unimplemented() + self.cpm_model += cp.GlobalCardinalityCount(self.get_cpm_exprs(lst), + self.get_cpm_exprs(values), + self.get_cpm_exprs(occurs), + closed=closed) + def ctr_minimum(self, lst: list[Variable] | list[Node], condition: Condition): - cpm_vars = self.get_cpm_vars(lst) - arity, op = self.funcmap[condition.operator.name.lower()] - cpm_rhs = self.cpm_variables[condition.variable] - if arity == 0: - self.cpm_model += op([cp.Minimum(cpm_vars), cpm_rhs]) - else: - self.cpm_model += op(cp.Minimum(cpm_vars), cpm_rhs) + cpm_vars = self.get_cpm_vars(lst) # TODO: check if list can be list of expressions too in comp? + self.cpm_model += self.eval_cpm_comp(cp.Minimum(cpm_vars), + condition.operator, + self.get_cpm_var(condition.right_operand())) + def ctr_maximum(self, lst: list[Variable] | list[Node], condition: Condition): - cpm_vars = self.get_cpm_vars(lst) - arity, op = self.funcmap[condition.operator.name.lower()] - cpm_rhs = self.cpm_variables[condition.variable] - if arity == 0: - self.cpm_model += op([cp.Maximum(cpm_vars), cpm_rhs]) - else: - self.cpm_model += op(cp.Maximum(cpm_vars), cpm_rhs) + cpm_vars = self.get_cpm_vars(lst) # TODO: check if list can be list of expressions too in comp? + self.cpm_model += self.eval_cpm_comp(cp.Maximum(cpm_vars), + condition.operator, + self.get_cpm_var(condition.right_operand())) def ctr_minimum_arg(self, lst: list[Variable] | list[Node], condition: Condition, rank: TypeRank): # should enter XCSP3-core self._unimplemented(lst, condition, rank) @@ -366,22 +397,17 @@ def ctr_maximum_arg(self, lst: list[Variable] | list[Node], condition: Condition self._unimplemented(lst, condition, rank) def ctr_element(self, lst: list[Variable] | list[int], i: Variable, condition: Condition): - cpm_list = self.get_cpm_vars(lst) - arity, op = self.funcmap[condition.operator.name.lower()] - if hasattr(condition, 'variable'): - cpm_rhs = self.cpm_variables[condition.variable] - elif hasattr(condition, 'value'): - cpm_rhs = condition.value - else: - self._unimplemented(lst, condition) - cpm_index = self.cpm_variables[i] - if arity == 0: - self.cpm_model += op([cp.Element(cpm_list,cpm_index), cpm_rhs]) - else: - self.cpm_model += op(cp.Element(cpm_list, cpm_index), cpm_rhs) + cpm_lst = self.get_cpm_vars(lst) + cpm_index = self.get_cpm_var(i) + cpm_rhs = self.get_cpm_var(condition.right_operand()) + self.cpm_model += self.eval_cpm_comp(cp.Element(cpm_lst, cpm_index), condition.operator, cpm_rhs) def ctr_element_matrix(self, matrix: list[list[Variable]] | list[list[int]], i: Variable, j: Variable, condition: Condition): - pass#self._unimplemented(matrix, i, j, condition) + mtrx = cp.cpm_array([self.get_cpm_vars(lst) for lst in matrix]) + cpm_i, cpm_j = self.get_cpm_vars([i,j]) + cpm_rhs = self.get_cpm_var(condition.right_operand()) + + self.cpm_model += self.eval_cpm_comp(mtrx[cpm_i, cpm_j], condition.operator, cpm_rhs) def ctr_channel(self, lst1: list[Variable], lst2: None | list[Variable]): if lst2 is None: @@ -398,41 +424,72 @@ def ctr_channel(self, lst1: list[Variable], lst2: None | list[Variable]): def ctr_channel_value(self, lst: list[Variable], value: Variable): self._unimplemented(lst, value) - def ctr_nooverlap(self, origins: list[Variable], lengths: list[int] | list[Variable], - zero_ignored: bool): # in XCSP3 competitions, no 0 permitted in lengths - self._unimplemented(origins, lengths, zero_ignored) + def ctr_nooverlap(self, origins: list[Variable], lengths: list[int] | list[Variable], zero_ignored: bool): # in XCSP3 competitions, no 0 permitted in lengths + cpm_start = self.get_cpm_vars(origins) + cpm_dur = self.get_cpm_vars(lengths) + cpm_end = [cp.intvar(*((s+d).get_bounds())) for s,d in zip(cpm_start, cpm_dur)] + self.cpm_model += cp.NoOverlap(cpm_start, cpm_dur, cpm_end) def ctr_nooverlap_multi(self, origins: list[list[Variable]], lengths: list[list[int]] | list[list[Variable]], zero_ignored: bool): - self._unimplemented(origins, lengths, zero_ignored) - + dim = len(origins) + if dim == 2: + assert len(origins) == 2 + assert len(lengths) == 2 + + start_x, start_y = self.get_cpm_vars(origins[0]), self.get_cpm_vars(origins[1]) + dur_x, dur_y = self.get_cpm_vars(origins[0]), self.get_cpm_vars(origins[1]) + + end_x = [cp.intvar(*get_bounds(s + d)) for s, d in zip(start_x, dur_x)] + end_y = [cp.intvar(*get_bounds(s + d)) for s, d in zip(start_y, dur_y)] + + self.cpm_model += cp.NoOverlap2d(start_x, dur_x, end_x, + start_y, dur_y, end_y) + + else: # n-dimensional, post decomposition directly + from cpmpy.expressions.utils import all_pairs + from cpmpy import any as cpm_any + n = len(origins[0]) + starts = cp.cpm_array([self.get_cpm_vars(lst) for lst in origins]) + durs = cp.cpm_array([self.get_cpm_vars(lst) for lst in lengths]) + + for i, j in all_pairs(list(range(n))): + self.cpm_model += cpm_any([starts[d,i] + durs[d,i] <= starts[d,j] |\ + starts[d,j] + durs[d,j] <= starts[d,i] for d in range(dim)]) + def ctr_nooverlap_mixed(self, xs: list[Variable], ys: list[Variable], lx: list[Variable], ly: list[int], zero_ignored: bool): - #self._unimplemented(xs, ys, lx, ly, zero_ignored) - pass + start_x = self.get_cpm_vars(xs) + start_y = self.get_cpm_vars(ys) + dur_x = self.get_cpm_vars(lx) + dur_y = ly + + end_x = [cp.intvar(*get_bounds(s + d)) for s, d in zip(start_x, dur_x)] + end_y = [cp.intvar(*get_bounds(s + d)) for s, d in zip(start_y, dur_y)] + + self.cpm_model += cp.NoOverlap2d(start_x, dur_x, end_x, + start_y, dur_y, end_y) def ctr_cumulative(self, origins: list[Variable], lengths: list[int] | list[Variable], heights: list[int] | list[Variable], condition: Condition): - #self._unimplemented(origins, lengths, heights, condition) cpm_start = self.get_cpm_exprs(origins) cpm_durations = self.get_cpm_exprs(lengths) cpm_demands = self.get_cpm_exprs(heights) - cpm_cap = self.get_cpm_var(condition.right_operand()) cpm_ends = [] for s,d in zip(cpm_start, cpm_durations): expr = s + d cpm_ends.append(cp.intvar(*get_bounds(expr))) - if condition.operator.name == 'LE': - self.cpm_model += cp.Cumulative(cpm_start, cpm_durations, cpm_ends, cpm_demands, cpm_cap) + if condition.operator == TypeConditionOperator.LE: + self.cpm_model += cp.Cumulative(cpm_start, cpm_durations, cpm_ends, cpm_demands, self.get_cpm_var(condition.right_operand())) else: # post decomposition directly # be smart and chose task or time decomposition if max(get_bounds(cpm_ends)) >= 100: - self._cumulative_task_decomp(cpm_start, cpm_durations, cpm_ends, heights, cpm_cap, condition.operator.to_str()) + self._cumulative_task_decomp(cpm_start, cpm_durations, cpm_ends, heights, condition) else: - self._cumulative_task_decomp(cpm_start, cpm_durations, cpm_ends, heights, cpm_cap, condition.operator.to_str()) + self._cumulative_task_decomp(cpm_start, cpm_durations, cpm_ends, heights, condition) - def _cumulative_task_decomp(self, cpm_start, cpm_duration, cpm_ends, cpm_demands, capacity, condition): - from cpmpy.expressions.utils import eval_comparison + def _cumulative_task_decomp(self, cpm_start, cpm_duration, cpm_ends, cpm_demands,condition:Condition): cpm_demands = cp.cpm_array(cpm_demands) + cpm_cap = self.get_cpm_var(condition.right_operand()) # ensure durations are satisfied for s,d,e in zip(cpm_start, cpm_duration, cpm_ends): self.cpm_model += s + d == e @@ -441,12 +498,11 @@ def _cumulative_task_decomp(self, cpm_start, cpm_duration, cpm_ends, cpm_demands for s,d,e in zip(cpm_start, cpm_duration, cpm_ends): # find overlapping tasks total_running = cp.sum(cpm_demands * ((cpm_start <= s) & (cpm_ends > s))) - self.cpm_model += eval_comparison(condition, total_running, capacity) + self.cpm_model += self.eval_cpm_comp(total_running, condition.operator, cpm_cap) - def _cumulative_time_decomp(self, cpm_start, cpm_duration, cpm_ends, cpm_demands, capacity, condition): - from cpmpy.expressions.utils import eval_comparison + def _cumulative_time_decomp(self, cpm_start, cpm_duration, cpm_ends, cpm_demands, condition:Condition): cpm_demands = cp.cpm_array(cpm_demands) - + cpm_cap = self.get_cpm_var(condition.right_operand) # ensure durations are satisfied for s, d, e in zip(cpm_start, cpm_duration, cpm_ends): self.cpm_model += s + d == e @@ -456,33 +512,41 @@ def _cumulative_time_decomp(self, cpm_start, cpm_duration, cpm_ends, cpm_demands # time decomposition for t in range(lb,ub+1): total_running = cp.sum(cpm_demands * ((cpm_start <= t) & (cpm_ends > t))) - self.cpm_model += eval_comparison(condition, total_running, capacity) + self.cpm_model += self.eval_cpm_comp(total_running, condition.operator, cpm_cap) def ctr_binpacking(self, lst: list[Variable], sizes: list[int], condition: Condition): - from cpmpy.expressions.utils import eval_comparison - cpm_vars = self.get_cpm_vars(lst) - rhs = self.get_cpm_var(condition.right_operand()) + cpm_rhs = self.get_cpm_var(condition.right_operand()) for bin in range(1, len(cpm_vars)+1): - self.cpm_model += eval_comparison(condition.operator.to_str(), - cp.sum((cpm_vars == bin) * sizes), - rhs) - + self.cpm_model += self.eval_cpm_comp(cp.sum((cpm_vars == bin) * sizes), + condition.operator, + cpm_rhs) + def ctr_binpacking_limits(self, lst: list[Variable], sizes: list[int], limits: list[int] | list[Variable]): + from cpmpy.expressions.utils import eval_comparison - self._unimplemented(lst, sizes, condition) + cpm_vars = self.get_cpm_vars(lst) - def ctr_binpacking_limits(self, lst: list[Variable], sizes: list[int], limits: list[int] | list[Variable]): - self._unimplemented(lst, sizes, limits) + for bin, lim in enumerate(limits): + self.cpm_model += eval_comparison("<=", + cp.sum((cpm_vars == (bin+1)) * sizes), + lim) def ctr_binpacking_loads(self, lst: list[Variable], sizes: list[int], loads: list[int] | list[Variable]): - self._unimplemented(lst, sizes, loads) + from cpmpy.expressions.utils import eval_comparison + + cpm_vars = self.get_cpm_vars(lst) + cpm_loads = self.get_cpm_vars(loads) + + for bin, load in enumerate(cpm_loads): + self.cpm_model += eval_comparison("==", + cp.sum((cpm_vars == (bin + 1)) * sizes), + load) def ctr_binpacking_conditions(self, lst: list[Variable], sizes: list[int], conditions: list[Condition]): # not in XCSP3-core self._unimplemented(lst, sizes, conditions) def ctr_knapsack(self, lst: list[Variable], weights: list[int], wcondition: Condition, profits: list[int], pcondition: Condition): - from cpmpy.expressions.utils import eval_comparison vars = self.get_cpm_vars(lst) cpm_weight = self.get_cpm_var(wcondition.right_operand()) @@ -490,8 +554,8 @@ def ctr_knapsack(self, lst: list[Variable], weights: list[int], wcondition: Cond total_weight = cp.sum(vars * weights) total_profit = cp.sum(vars * profits) - self.cpm_model += eval_comparison(wcondition.operator.to_str(), total_weight, cpm_weight) - self.cpm_model += eval_comparison(pcondition.operator.to_str(), total_profit, cpm_profit) + self.cpm_model += self.eval_cpm_comp(total_weight, wcondition.operator, cpm_weight) + self.cpm_model += self.eval_cpm_comp(total_profit, pcondition.operator, cpm_profit) def ctr_flow(self, lst: list[Variable], balance: list[int] | list[Variable], arcs: list, capacities: None | list[range]): # not in XCSP3-core @@ -509,7 +573,7 @@ def ctr_clause(self, pos: list[Variable], neg: list[Variable]): # not in XCSP3- self._unimplemented(pos, neg) def ctr_circuit(self, lst: list[Variable], size: None | int | Variable): # size is None in XCSP3 competitions - return cp.Circuit(lst) + return cp.SubCircuitWithStart(lst, start_index=0) # # # # # # # # # # # All methods about objectives to be implemented @@ -517,73 +581,67 @@ def ctr_circuit(self, lst: list[Variable], size: None | int | Variable): # size def obj_minimize(self, term: Variable | Node): if isinstance(term, Node): - term = term.cnt - self.cpm_model.minimize(self.get_cpm_var(term)) + cpm_expr = self.exprs_from_node([term]) + assert len(cpm_expr) == 1 + cpm_expr = cpm_expr[0] + else: + cpm_expr = self.get_cpm_var(term) + self.cpm_model.minimize(cpm_expr) def obj_maximize(self, term: Variable | Node): - self.cpm_model.maximize(self.get_cpm_exprs(term)[0]) + if isinstance(term, Node): + cpm_expr = self.exprs_from_node([term]) + assert len(cpm_expr) == 1 + cpm_expr = cpm_expr[0] + else: + cpm_expr = self.get_cpm_var(term) + self.cpm_model.maximize(cpm_expr) def obj_minimize_special(self, obj_type: TypeObj, terms: list[Variable] | list[Node], coefficients: None | list[int]): + import numpy as np + if coefficients is None: + coefficients = np.ones(len(terms)) + else: + coefficients = np.array(coefficients) + if obj_type == TypeObj.SUM: - if coefficients is None: - self.cpm_model.minimize(cp.sum(self.get_cpm_exprs(terms))) - else: - self.cpm_model.minimize(cp.sum(cp.cpm_array(self.get_cpm_exprs(terms)) * coefficients)) - elif obj_type == TypeObj.PRODUCT: - if coefficients is None: - self.cpm_model.minimize(reduce((lambda x, y: x*y),self.get_cpm_exprs(terms))) - else: - self._unimplemented(obj_type, terms, coefficients) - elif obj_type == TypeObj.EXPRESSION: - self._unimplemented(obj_type, terms, coefficients) + self.cpm_model.minimize(cp.sum(coefficients * self.get_cpm_exprs(terms))) elif obj_type == TypeObj.MAXIMUM: - if coefficients is None: - self.cpm_model.minimize(cp.Maximum(self.get_cpm_exprs(terms))) - else: - self.cpm_model.minimize(cp.Maximum(cp.cpm_array(self.get_cpm_exprs(terms)) * coefficients)) + self.cpm_model.minimize(cp.max(coefficients * self.get_cpm_exprs(terms))) elif obj_type == TypeObj.MINIMUM: - if coefficients is None: - self.cpm_model.minimize(cp.Minimum(self.get_cpm_exprs(terms))) - else: - self.cpm_model.minimize(cp.Minimum(cp.cpm_array(self.get_cpm_exprs(terms)) * coefficients)) + self.cpm_model.minimize(cp.min(coefficients * self.get_cpm_exprs(terms))) elif obj_type == TypeObj.NVALUES: - if coefficients is None: - self.cpm_model.minimize(cp.NValue(self.get_cpm_exprs(terms))) - else: - self.cpm_model.minimize(cp.NValue(cp.cpm_array(self.get_cpm_exprs(terms)) * coefficients)) + self.cpm_model.minimize(cp.NValue(coefficients * self.get_cpm_exprs(terms))) + elif obj_type == TypeObj.EXPRESSION: + assert all(coeff == 1 for coeff in coefficients) + assert len(terms) == 1 + cpm_expr = self.get_cpm_exprs(terms)[0] + self.cpm_model.minimize(cpm_expr) else: - self._unimplemented(obj_type, terms, coefficients) + self._unimplemented(obj_type, coefficients, terms) def obj_maximize_special(self, obj_type: TypeObj, terms: list[Variable] | list[Node], coefficients: None | list[int]): + import numpy as np + if coefficients is None: + coefficients = np.ones(len(terms)) + else: + coefficients = np.array(coefficients) + if obj_type == TypeObj.SUM: - if coefficients is None: - self.cpm_model.maximize(cp.sum(self.get_cpm_exprs(terms))) - else: - self.cpm_model.maximize(cp.sum(cp.cpm_array(self.get_cpm_exprs(terms)) * coefficients)) - elif obj_type == TypeObj.PRODUCT: - if coefficients is None: - self.cpm_model.maximize(reduce((lambda x, y: x * y), self.get_cpm_exprs(terms))) - else: - self._unimplemented(obj_type, terms, coefficients) - elif obj_type == TypeObj.EXPRESSION: - self._unimplemented(obj_type, terms, coefficients) + self.cpm_model.maximize(cp.sum(coefficients * self.get_cpm_exprs(terms))) elif obj_type == TypeObj.MAXIMUM: - if coefficients is None: - self.cpm_model.maximize(cp.Maximum(self.get_cpm_exprs(terms))) - else: - self.cpm_model.maximize(cp.Maximum(cp.cpm_array(self.get_cpm_exprs(terms)) * coefficients)) + self.cpm_model.maximize(cp.max(coefficients * self.get_cpm_exprs(terms))) elif obj_type == TypeObj.MINIMUM: - if coefficients is None: - self.cpm_model.maximize(cp.Minimum(self.get_cpm_exprs(terms))) - else: - self.cpm_model.maximize(cp.Minimum(cp.cpm_array(self.get_cpm_exprs(terms)) * coefficients)) + self.cpm_model.maximize(cp.min(coefficients * self.get_cpm_exprs(terms))) elif obj_type == TypeObj.NVALUES: - if coefficients is None: - self.cpm_model.maximize(cp.NValue(self.get_cpm_exprs(terms))) - else: - self.cpm_model.maximize(cp.NValue(cp.cpm_array(self.get_cpm_exprs(terms)) * coefficients)) + self.cpm_model.maximize(cp.NValue(coefficients * self.get_cpm_exprs(terms))) + elif obj_type == TypeObj.EXPRESSION: + assert all(coeff == 1 for coeff in coefficients) + assert len(terms) == 1 + cpm_expr = self.get_cpm_exprs(terms)[0] + self.cpm_model.maximize(cpm_expr) else: - self._unimplemented(obj_type, terms, coefficients) + self._unimplemented(obj_type, coefficients, terms) def vars_from_node(self, scope): cpm_vars = [] diff --git a/xcsp3/executable/test/conftest.py b/xcsp3/executable/test/conftest.py index 79a4142d9..fcdfb1b76 100644 --- a/xcsp3/executable/test/conftest.py +++ b/xcsp3/executable/test/conftest.py @@ -93,8 +93,8 @@ def pytest_addoption(parser): parser.addoption("--subsolver", action="store", default=None) parser.addoption("--all", action="store_true", help="run all combinations") parser.addoption("--fresh", action="store_true", help="reset all stored results") - parser.addoption("--time_limit", action="store", default=None) - parser.addoption("--memory_limit", action="store", default=None) + parser.addoption("--time_limit", action="store", default=None, type=int) + parser.addoption("--memory_limit", action="store", default=None, type=int) parser.addoption("--type", action="store", default=None) parser.addoption("--intermediate", action="store_true") parser.addoption("--competition", action="store_true")