0.4.3 (#78) (#80)

* simplify and fix layout of ``count`` examples

* fix some more examples

* add docs readme.md

* add table constraint doc

* add disjunctive constraint

* add disjunctive constraint

---------

Co-authored-by: Artsiom Kaltovich <[email protected]>

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

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
+```

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
 ----------------------
 

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
 -----

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 <https://www.minizinc.org/doc-2.7.6/en/predicates.html#ex-jobshop3>`_
+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]])

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])

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
 

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,
 }

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

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()

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()