diff --git a/changelog.md b/changelog.md index b3dae5b..cb067fe 100644 --- a/changelog.md +++ b/changelog.md @@ -1,11 +1,20 @@ -## 0.4.2 +### 0.4.3 +#### Added +- `disjunctive` constraint +#### Fixed +- array slices with upper slice as operations should compile correctly now +#### Documentation +- simplify and fix layout of ``count``, ``cumulative`` + ``table`` and ``max`` examples + +### 0.4.2 #### CI changes - use minizinc 2.7.6 as maximum version in CI (as in minizinc-python) - use minizinc 2.6.0 as minimum version in CI (as in minizinc-python) #### Python interpreters support - add 3.12 CPython -## 0.4.1 +### 0.4.1 #### Added - ``table`` constraint - ``contains`` method for arrays and sets, to check if elem presented diff --git a/doc/readme.md b/doc/readme.md new file mode 100644 index 0000000..82c1f4e --- /dev/null +++ b/doc/readme.md @@ -0,0 +1,12 @@ +To generate sphinx documentation from source doc comments +you should run following command (from project root) + +```shell +sphinx-apidoc -f -o docs/source/api zython +``` + +To build html doc (which will be in doc/build/html/index.html): + +```shell +python -m sphinx -T -E -b html -d _build/doctrees -D language=en doc/source doc/build/html +``` diff --git a/doc/source/guides/array_advanced/cumulative.rst b/doc/source/guides/array_advanced/cumulative.rst index 2de5002..dab96ea 100644 --- a/doc/source/guides/array_advanced/cumulative.rst +++ b/doc/source/guides/array_advanced/cumulative.rst @@ -7,6 +7,11 @@ It requires that a set of tasks given by start times, durations, and resource requirements, never require more than a global resource limit at any one time. +.. note:: + + It is suggested to use ranges and sequences of ranges instead of int, + because minizinc can return strange result when type of any arg is int + Moving Furniture Model ---------------------- diff --git a/doc/source/guides/array_advanced/table.rst b/doc/source/guides/array_advanced/table.rst index dc2e8e1..3ec1178 100644 --- a/doc/source/guides/array_advanced/table.rst +++ b/doc/source/guides/array_advanced/table.rst @@ -2,7 +2,7 @@ Table ===== The table constraint is used to specify if one dimensional array -should be equal to any row of two dimensional array. +should be equal to any row of a two dimensional array. Model ----- diff --git a/doc/source/guides/array_advanced/tasks_sheduling.rst b/doc/source/guides/array_advanced/tasks_sheduling.rst new file mode 100644 index 0000000..8edd7f5 --- /dev/null +++ b/doc/source/guides/array_advanced/tasks_sheduling.rst @@ -0,0 +1,94 @@ +Tasks Scheduling +================ + +The disjunctive constraint takes an array of start times for each task and +an array of their durations and makes sure that only one task is active at +any one time. + +.. note:: + + It is suggested to use ranges and sequences of ranges instead of int, + because minizinc can return strange result when type of any arg is int + +Model +----- + +We will recreate the example of task sheduling problem from the +`minizinc `_ +documentation. + +The model consists of several jobs, which can be separated into several +steps. There are following restrictions: + +- to complete job, all steps should be executed +- different steps are independent: + if there is a job on first step, other job can be processed on second step, + without necessity to wait. +- if there is an active task on any step, not other job can be executed + on this step and should wait. + +You can think about this as a conveyor with `n_jobs` lines, +one part on every line and +`n_steps` independent machines which is shared between lines. +Every machine can complete only one manipulation with any part +and should work with a part processed by previous machine. +We are searching for the fastest way to processed all the parts. + +Python Model +------------ + +.. testcode:: + + import zython as zn + + + durations = [ + [1, 4, 5, 3, 6], + [3, 2, 7, 1, 2], + [4, 4, 4, 4, 4], + [1, 1, 1, 6, 8], + [7, 3, 2, 2, 1], + ] + + + class MyModel(zn.Model): + def __init__(self, durations): + self.durations = zn.Array(durations) + self.n_jobs = len(durations) + self.n_tasks = len(durations[0]) + self.total = zn.sum(self.durations) + self.end = zn.var(zn.range(self.total + 1)) + self.start = zn.Array( + zn.var(zn.range(self.total + 1)), shape=(self.n_jobs, self.n_tasks) + ) + self.constraints = [self.in_sequence(), self.no_overlap()] + + def no_overlap(self): + return zn.forall( + zn.range(self.n_tasks), + lambda j: zn.disjunctive( + [self.start[i, j] for i in range(self.n_jobs)], + [self.durations[i, j] for i in range(self.n_jobs)], + ) + ) + + def in_sequence(self): + return zn.forall( + range(self.n_jobs), + lambda i: zn.forall( + zn.range(self.n_tasks - 1), + lambda j: self.start[i, j] + self.durations[i, j] <= self.start[i, j + 1], + ) & ( + self.start[i, self.n_tasks - 1] + self.durations[i, self.n_tasks - 1] <= self.end + ) + ) + + + model = MyModel(durations) + result = model.solve_minimize(model.end) + print(result) + + +.. testoutput:: + + Solution(objective=30, total=86, end=30, start=[[8, 9, 13, 18, 21], [5, 13, 18, 25, 27], [1, 5, 9, 13, 17], [0, 1, 2, 3, 9], [9, 16, 25, 27, 29]]) diff --git a/test/operations/test_disjunctive.py b/test/operations/test_disjunctive.py new file mode 100644 index 0000000..b252556 --- /dev/null +++ b/test/operations/test_disjunctive.py @@ -0,0 +1,7 @@ +import zython as zn + + +def test_ok(): + array = zn.Array(zn.var(zn.range(10)), shape=3) + array._name = "array" + zn.disjunctive(array, [1, 2, 3]) diff --git a/zython/__init__.py b/zython/__init__.py index d3da4c5..2b9744b 100644 --- a/zython/__init__.py +++ b/zython/__init__.py @@ -5,7 +5,7 @@ from zython.var_par.collections.array import Array from zython.var_par.collections.set import Set from zython.operations.functions_and_predicates import exists, forall, sum, alldifferent, circuit, count, min, max,\ - allequal, ndistinct, increasing, decreasing, cumulative, table + allequal, ndistinct, increasing, decreasing, cumulative, disjunctive, table from zython.model import Model from zython.result import as_original diff --git a/zython/_compile/zinc/flags.py b/zython/_compile/zinc/flags.py index e440b28..69d2a7c 100644 --- a/zython/_compile/zinc/flags.py +++ b/zython/_compile/zinc/flags.py @@ -18,6 +18,7 @@ class Flags(enum.Flag): decreasing = enum.auto() strictly_decreasing = enum.auto() cumulative = enum.auto() + disjunctive = enum.auto() table = enum.auto() float_used = enum.auto() @@ -38,6 +39,7 @@ def append(src: SourceCode, line: str): Flags.decreasing: partial(append, line='include "decreasing.mzn";'), Flags.strictly_decreasing: partial(append, line='include "strictly_decreasing.mzn";'), Flags.cumulative: partial(append, line='include "cumulative.mzn";'), + Flags.disjunctive: partial(append, line='include "disjunctive.mzn";'), Flags.table: partial(append, line='include "table.mzn";'), Flags.float_used: lambda x: x, } diff --git a/zython/_compile/zinc/to_str.py b/zython/_compile/zinc/to_str.py index 46ae3df..b73e92b 100644 --- a/zython/_compile/zinc/to_str.py +++ b/zython/_compile/zinc/to_str.py @@ -124,7 +124,7 @@ def _call_func(func, *params, flatten_args=False, flags_): def _get_array_shape_decl(shape): - result = [f'0..{s - 1}' for s in shape] + result = [f'0..{to_str(s - 1)}' for s in shape] return f"{', '.join(result)}" @@ -213,6 +213,7 @@ def __init__(self): self[_Op_code.decreasing] = partial(_global_constraint, "decreasing") self[_Op_code.strictly_decreasing] = partial(_global_constraint, "strictly_decreasing") self[_Op_code.cumulative] = partial(_global_constraint, "cumulative") + self[_Op_code.disjunctive] = partial(_global_constraint, "disjunctive") self[_Op_code.table] = partial(_global_constraint, "table", flatten_args=False) def __missing__(self, key): # pragma: no cover diff --git a/zython/operations/_op_codes.py b/zython/operations/_op_codes.py index aeb128d..17112e5 100644 --- a/zython/operations/_op_codes.py +++ b/zython/operations/_op_codes.py @@ -38,4 +38,5 @@ class _Op_code(enum.Enum): decreasing = enum.auto() strictly_decreasing = enum.auto() cumulative = enum.auto() + disjunctive = enum.auto() table = enum.auto() diff --git a/zython/operations/functions_and_predicates.py b/zython/operations/functions_and_predicates.py index 008b1f6..5d9c3d9 100644 --- a/zython/operations/functions_and_predicates.py +++ b/zython/operations/functions_and_predicates.py @@ -167,12 +167,16 @@ def count(seq: ZnSequence, value: Union[int, Operation, Callable[[ZnSequence], O Counter({1: 4, 0: 3}) ``zn.alldifferent`` could be emulated via ``zn.count`` + >>> import zython as zn + >>> def all_different(array): + ... return zn.forall(array, lambda elem: zn.count(array, elem) == 1) + ... >>> class MyModel(zn.Model): ... def __init__(self): - ... self.a = zn.Array(zn.var(range(10)), shape=4) - ... self.constraints = [zn.forall(zn.range(self.a.size(0)), - ... lambda i: zn.count(self.a, lambda elem: elem == self.a[i]) == 1)] + ... self.a = zn.Array(zn.var(range(4)), shape=4) + ... self.constraints = [all_different(self.a)] + ... >>> model = MyModel() >>> result = model.solve_satisfy() >>> Counter(result["a"]) @@ -224,7 +228,11 @@ def cumulative( ... def __init__(self): ... self.limit = zn.var(range(0, 10)) ... self.constraints = [ - ... zn.cumulative(start_times=[1, 2, 4], durations=[3, 2, 1], requirements=[1, 1, 1], limit=self.limit), + ... zn.cumulative(start_times=[1, 2, 4], + ... durations=[3, 2, 1], + ... requirements=[1, 1, 1], + ... limit=self.limit, + ... ), ... ] ... >>> model = MyModel() @@ -235,10 +243,81 @@ def cumulative( return constraint_module.cumulative(start_times, durations, requirements, limit) +def disjunctive( + start_times: ZnSequence, + durations: ZnSequence, +) -> Constraint: + """ The disjunctive constraint takes an array of start times for each task and + an array of their durations and makes sure that only one task is active at any one time. + + Parameters + ---------- + start_times: range, array of var, or sequence (list or tuple) of var + Sequence with start time of the tasks + durations: range, array of var, or sequence (list or tuple) of var + Sequence with durations of the tasks + + Returns + ------- + result: Constraint + + Notes + ----- + It is suggested to use ranges and sequences of ranges instead of int, + because minizinc can return strange result when type of any arg is int + + Examples + -------- + + >>> import zython as zn + >>> class MyModel(zn.Model): + ... def __init__(self): + ... self.start = zn.Array(zn.var(zn.range(0, 10)), shape=3) + ... self.constraints = [ + ... zn.disjunctive(start_times=self.start, durations=[3, 2, 1]), + ... ] + ... + >>> model = MyModel() + >>> result = model.solve_satisfy() + >>> result["start"] + [3, 1, 0] + """ + return Constraint(_Op_code.disjunctive, start_times, durations) + + def table( - x: ZnSequence, - t: ZnSequence, + x: ZnSequence, + t: ZnSequence, ) -> Constraint: + """The table constraint is used to specify if one dimensional array + should be equal to any row of a two-dimensional array. + + Or, in more strict form: + the table constraint enforces that a tuple of variables takes a value from a set of tuples. + Since there are no tuples in MiniZinc this is encoded using arrays. + The constraint enforces x in t, where we consider x and each row in t to be a tuple, + and t to be a set of tuples. + + Parameters + ---------- + x: one-dimentional array + t: two-dimentional array, `x` should be one of the rows of `t` + + Examples + -------- + + >>> import zython as zn + >>> class MyModel(zn.Model): + ... def __init__(self): + ... self.a = zn.Array(zn.var(zn.range(1, 5)), shape=4) + ... self.choose_from = zn.Array([[1, 2, 3, 4], [0, 1, 2, 3]]) + ... self.constraints = [zn.table(self.a, self.choose_from)] + ... + >>> model = MyModel() + >>> result = model.solve_satisfy() + >>> result["a"] + [1, 2, 3, 4] + """ return constraint_module.table(x, t) @@ -283,7 +362,7 @@ def max(seq: ZnSequence, key: Union[Operation, Callable[[ZnSequence], Operation] Parameters ---------- seq: range, array of var, or sequence (list or tuple) of var - Sequence to find smallest element in + Sequence to find the biggest element in key: Operation or Callable, optional The parameter has the same semantic as in python: specify the operation which result will be latter compared. @@ -299,10 +378,12 @@ def max(seq: ZnSequence, key: Union[Operation, Callable[[ZnSequence], Operation] Examples -------- + Calculate the biggest number of negative numbers in a row of an array + >>> import zython as zn >>> class MyModel(zn.Model): ... def __init__(self): - ... self.a = zn.Array([[1, 2, 3], [-1, -2, -3]]) + ... self.a = zn.Array([[0, 0, 0, 0], [0, 0, -1, -1], [0, -1, -1, -1]]) ... self.m = zn.max(zn.range(self.a.size(0)), ... lambda row: zn.count(self.a[row, :], lambda elem: elem < 0)) >>> model = MyModel()