Merge branch 'xcsp3_executable' into exact_2.0.0

.gitignore

@@ -155,4 +155,5 @@ xcsp3/prof/
 reportlog.jsonl
 .pytest-runtimes
 perf_stats/
-perf_stats_0/
+perf_stats_0/
+checkingInstancesXCSP24/

cpmpy/expressions/core.py

@@ -533,6 +533,7 @@ class Operator(Expression):
         'sub': (2, False), # x - y
         'mul': (2, False),
         'div': (2, False),
+        'idiv': (2, False),
         'mod': (2, False),
         'pow': (2, False),
         '-':   (1, False), # -x
@@ -673,6 +674,12 @@ def value(self):
             except ZeroDivisionError:
                 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.")
+        elif self.name == "idiv":
+            try:
+                return int(arg_vals[0] / arg_vals[1])
+            except ZeroDivisionError:
+                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)
@@ -719,6 +726,13 @@ def get_bounds(self):
                 raise ZeroDivisionError("division by domain containing 0 is not supported")
             bounds = [lb1 // lb2, lb1 // ub2, ub1 // lb2, ub1 // ub2]
             lowerbound, upperbound = min(bounds), max(bounds)
+        elif self.name == 'idiv':
+            lb1, ub1 = get_bounds(self.args[0])
+            lb2, ub2 = get_bounds(self.args[1])
+            if lb2 <= 0 <= ub2:
+                raise ZeroDivisionError("division by domain containing 0 is not supported")
+            bounds = [int(lb1 / lb2), int(lb1 / ub2), int(ub1 / lb2), int(ub1 / ub2)]
+            lowerbound, upperbound = min(bounds), max(bounds)
         elif self.name == 'mod':
             lb1, ub1 = get_bounds(self.args[0])
             lb2, ub2 = get_bounds(self.args[1])

cpmpy/transformations/linearize.py

@@ -149,6 +149,23 @@ def _linearize_constraint_helper(lst_of_expr, supported={"sum","wsum"}, expr_sto
                     #newrhs = lhs.args[0]
                     #lhs = lhs.args[1] * rhs #operator is actually always '==' here due to only_numexpr_equality
                     #cpm_expr = eval_comparison(cpm_expr.name, lhs, newrhs)
+                elif lhs.name == 'idiv':
+                    a, b = lhs.args
+                    # if division is total, b is either strictly negative or strictly positive!
+                    lb, ub = get_bounds(b)
+                    if not ((lb < 0 and ub < 0) or (lb > 0 and ub > 0)):
+                        raise TypeError(
+                            f"Can't divide by a domain containing 0, safen the expression first")
+                    r = intvar(-(max(abs(lb) - 1, abs(ub) - 1)), max(abs(lb) - 1, abs(ub) - 1)) # remainder can be both positive and negative
+                    cpm_expr = [eval_comparison(cpm_expr.name, a, b * rhs + r)]
+                    cond = [Abs(r) < Abs(b), Abs(b * rhs) < Abs(a)]
+                    decomp = toplevel_list(decompose_in_tree(cond))  # decompose abs
+                    cpm_exprs = toplevel_list(decomp + cpm_expr)
+                    exprs = linearize_constraint(flatten_constraint(cpm_exprs, expr_store=expr_store, skip_simplify_bool=True), supported=supported, expr_store=expr_store)
+                    newlist.extend(exprs)
+                    continue
+
+
                 elif lhs.name == 'mod':  # x mod y == x - (x//y) * y
                     # gets handles in the solver interface
                     # We should never get here, since both Gurobi and Exact have "faked support" for "Mod"

xcsp3/competition.md

@@ -2,6 +2,25 @@
 
 These are the installation and usage instructions for the CPMpy submission to the XCSP3 2024 competition.
 
+## Submission
+
+This submission is the basis for multiple submissions with different solver backends. CPMpy is a modelling system which can translate to many different solvers, six of which have been chosen for the XCSP3 competition. 
+The data files and install instructions are shared (some solvers have additional steps). 
+From the executable's point of view, the major difference between the submissions is the actual command used to run the executable, where the correct solver must be set. These commands are listed later on.
+Internally, different solver-tailored backends will be used, where the COP and CSP models get transformed as to satisfy the modelling capabilities of the selected solver target.
+
+The CPMpy modelling system will compete in the following tracks, using the following solver backends:
+
+| CPMpy_backend | CSP sequential | COP sequential (30') | COP parallel | mini CSP | mini COP |
+| - | - | - | - | - | - |
+| cpmpy_ortools | yes | yes | yes | yes | yes |
+| cpmpy_exact | yes | yes | no | yes | yes |
+| cpmpy_z3 | yes | yes | no | yes | yes |
+| cpmpy_gurobi | yes | yes | no | yes | yes |
+| cpmpy_mnz-gecode | yes | yes | no | yes | yes |
+| cpmpy_mnz-chuffed | yes | yes | no | yes | yes |
+
+
 ## Setup
 
 Since the competition will be run on a cluster of CentOS 8.3 servers, the installation steps have been talored to that particular OS. Our submission is not inherently dependant on any particular OS, but some dependencies might be missing on a clean install (which are for example included in a standard Ubuntu install).
@@ -22,7 +41,7 @@ CPMpy is a python library, and thus python is the main dependency. But many of t
 
 2) libffi-devel
 
-    To get _ctypes in python. Similarly as the previous dependency, is required to
+    To get _ctypes in python. Similarly as the previous dependency, it is required to
     build some of the python libraries. Must be installed before compiling python3.11 (if python3.11 is not already installed)
     ```bash
     yum install -y libffi-devel
@@ -44,14 +63,16 @@ CPMpy is a python library, and thus python is the main dependency. But many of t
 
 5) libGL divers
 
-    For some reason, the `GeCode` solver requires graphics drivers to be able to run (probably uses them for vector operations?). Without them, GeCode will complain (when running, not when in stalling) about a missing shared object file: `libEGL.so.1`. This might not be present on a headless install.
+    The `GeCode` solver requires certain graphics drivers to be installed on the system (probably uses them for vector operations?).
+   Without them, GeCode will crash (when running, not when in installing) on a missing shared object file: `libEGL.so.1`.
+   This might not be present on a headless install of the OS.
 
     ```bash
     yum install mesa-libGL mesa-dri-drivers libselinux libXdamage libXxf86vm libXext
     dnf install mesa-libEGL
     ```
 
-6) Python
+7) Python
     - version: 3.11(.7)
 
     These are the steps we used to install it:
@@ -71,7 +92,6 @@ CPMpy is a python library, and thus python is the main dependency. But many of t
 
 1) Minizinc
 
-
     To download Minizinc, run the following:
     ```bash
     wget https://github.com/MiniZinc/MiniZincIDE/releases/download/2.8.5/MiniZincIDE-2.8.5-bundle-linux-x86_64.tgz
@@ -86,7 +106,9 @@ CPMpy is a python library, and thus python is the main dependency. But many of t
 
 2) Gurobi licence
 
-    It might be that you already have a licence or that, depending on how the licence was acquired, the installation of the license differs. The following steps are for installing a single-person single-machine academic license, aquired through the Gurobi User Portal.
+    Gurobi is a commercial MIP solver that requires a licence to run at its full potential.
+    Depending on the type of licence, the installation instructions differ.
+    The following instructions are tailored to installing a "Academic Named-User License", which can be aquired on the [Gurobi licence portal](https://www.gurobi.com/academia/academic-program-and-licenses).
 
     First, get a licence from Gurobi's site. It should give you a command looking like: `grbgetkey <your licence key>`
 
@@ -167,24 +189,24 @@ python executable/main.py <BENCHNAME>
     [--intermediate]                # If intermediate results should be reported (only for COP and a subset of solvers)
 ```
 
-The executable supports multiple solvers and is used for multiple submissions to the competition. The submitted solvers are:
-- ortools
-- exact
-- z3
-- gurobi
-- minizinc:chuffed
-- minizinc:gecode
+The same executable supports multiple solver backends and is used for all of the submissions to the competition. The submitted cpmpy + backends are:
+- `cpmpy_ortools`
+- `cpmpy_exact`
+- `cpmpy_z3`
+- `cpmpy_gurobi`
+- `cpmpy_mnz-chuffed`
+- `cpmpy_mnz-gecode`
 
 The commands are as follows:
 
-| Solver | Subsolver | Command |
-| - | - | - |
-| OR-Tools | / | python executable/main.py BENCHNAME --intermediate --cores=NBCORES --solver=ortools --mem-limit=MEMLIMIT --time-limit=TIMELIMIT --seed=RANDOMSEED | 
-| Exact | / | python executable/main.py <BENCHNAME> --intermediate --cores=NBCORES --solver=exact --mem-limit=MEMLIMIT --time-limit=TIMELIMIT --seed=RANDOMSEED | 
-| Z3 | / | python executable/main.py <BENCHNAME> --intermediate --cores=NBCORES --solver=z3 --mem-limit=MEMLIMIT --time-limit=TIMELIMIT --seed=RANDOMSEE | 
-| Gurobi | / | python executable/main.py <BENCHNAME> --intermediate --cores=NBCORES --solver=gurobi --mem-limit=MEMLIMIT --time-limit=TIMELIMIT --seed=RANDOMSEED | 
-| Minizinc | Chuffed | python executable/main.py <BENCHNAME> --intermediate --cores=NBCORES --profiler --solver=minizinc --subsolver=chuffed --mem-limit=MEMLIMIT --time-limit=TIMELIMIT --seed=RANDOMSEED | 
-| Minizinc | GeCode | python executable/main.py <BENCHNAME> --intermediate --cores=NBCORES --solver=minizinc --subsolver=gecode --mem-limit=MEMLIMIT --time-limit=TIMELIMIT --seed=RANDOMSEED | 
+| Submission | Command |
+| - | - |
+| **cpmpy_ortools** | python executable/main.py BENCHNAME --intermediate --cores=NBCORES --solver=ortools --mem-limit=MEMLIMIT --time-limit=TIMELIMIT --seed=RANDOMSEED | 
+| **cpmpy_exact** | python executable/main.py BENCHNAME --intermediate --cores=NBCORES --solver=exact --mem-limit=MEMLIMIT --time-limit=TIMELIMIT --seed=RANDOMSEED | 
+| **cpmpy_z3** | python executable/main.py BENCHNAME --intermediate --cores=NBCORES --solver=z3 --mem-limit=MEMLIMIT --time-limit=TIMELIMIT --seed=RANDOMSEED | 
+| **cpmpy_gurobi** | python executable/main.py BENCHNAME --intermediate --cores=NBCORES --solver=gurobi --mem-limit=MEMLIMIT --time-limit=TIMELIMIT --seed=RANDOMSEED | 
+| **cpmpy_mnz-chuffed** | python executable/main.py BENCHNAME --intermediate --cores=NBCORES --solver=minizinc --subsolver=chuffed --mem-limit=MEMLIMIT --time-limit=TIMELIMIT --seed=RANDOMSEED | 
+| **cpmpy_mnz-gecode** | python executable/main.py BENCHNAME --intermediate --cores=NBCORES --solver=minizinc --subsolver=gecode --mem-limit=MEMLIMIT --time-limit=TIMELIMIT --seed=RANDOMSEED | 
 
 
 

xcsp3/executable/callbacks.py

@@ -13,6 +13,7 @@
 
 import cpmpy as cp
 from cpmpy import cpm_array
+from cpmpy.expressions.core import Operator
 from cpmpy.expressions.utils import is_any_list, get_bounds, is_boolexpr
 
 
@@ -337,7 +338,7 @@ def ctr_ordered(self, lst: list[Variable], operator: TypeOrderedOperator, length
 
 
     def ctr_lex_limit(self, lst: list[Variable], limit: list[int], operator: TypeOrderedOperator):  # should soon enter XCSP3-core
-        self._unimplemented(lst, limit, operator)
+        self.ctr_lex([lst, limit], operator)
 
     def ctr_lex(self, lists: list[list[Variable]], operator: TypeOrderedOperator):
         cpm_lists = [self.get_cpm_vars(lst) for lst in lists]

xcsp3/executable/main.py

@@ -236,6 +236,8 @@ class Args:
     opt:bool=False
     solve:bool=True
     profiler:bool=False
+    throw:bool=False
+    solve_all:bool=False
 
     def __post_init__(self):
         if self.dir is not None:
@@ -264,6 +266,8 @@ def from_cli(args):
             intermediate = args.intermediate if args.intermediate is not None else False,
             solve = not args.only_transform,
             profiler = args.profiler,
+            throw = args.throw,
+            solve_all = args.all,
         )
 
     @property
@@ -436,8 +440,6 @@ def flush(self):
 
 def main():
 
-    start = time.time()
-
     # ------------------------------ Argument parsing ------------------------------ #
 
     parser = argparse.ArgumentParser(
@@ -476,10 +478,24 @@ def main():
     parser.add_argument("--only-transform", action=argparse.BooleanOptionalAction)
     # Enable profiling measurements
     parser.add_argument("--profiler", action=argparse.BooleanOptionalAction)
+    # Whether the executable should throw an exception (instead of capturing it) (should be off during competition)
+    parser.add_argument("--throw", action=argparse.BooleanOptionalAction)
+    # SolveAll (instead of Solve)
+    parser.add_argument("--all", action=argparse.BooleanOptionalAction)
 
     # Process cli arguments 
     args = Args.from_cli(parser.parse_args())
     print_comment(str(args))
+
+    try:
+        main_helper(args)
+    except Exception as e:
+        if args.throw:
+            raise e
+        else:
+            error_handler(e)
+
+def main_helper(args):
 
     from xml.etree.ElementTree import ParseError
     try:
@@ -583,15 +599,28 @@ def run_helper(args:Args):
     if args.solve:
         try:
             with TimerContext("solve") as tc:
-                if args.solver == "exact": # Exact2 takes its options at creation time
-                    sat = s.solve(
-                        time_limit=time_limit,
-                    ) 
+                if args.solver == "exact": # Exact takes its options at creation time
+                    if args.solve_all:
+                        nr_sols = s.solveAll(
+                            time_limit=time_limit
+                        )
+                        print_comment(f"Found {nr_sols} solutions.")
+                    else:
+                        sat = s.solve(
+                            time_limit=time_limit
+                        )
                 else:
-                    sat = s.solve(
-                        time_limit=time_limit,
-                        **solver_arguments(args, model)
-                    ) 
+                    if args.solve_all:
+                        nr_sols = s.solveAll(
+                            time_limit=time_limit,
+                            **solver_arguments(args, model)
+                        ) 
+                        print_comment(f"Found {nr_sols} solutions.")
+                    else:
+                        sat = s.solve(
+                            time_limit=time_limit,
+                            **solver_arguments(args, model)
+                        ) 
             print_comment(f"took {(tc.time):.4f} seconds to solve")
         except MemoryError:
             print_comment("Ran out of memory when trying to solve.")
@@ -624,7 +653,4 @@ def run_helper(args:Args):
     signal.signal(signal.SIGABRT, sigterm_handler)
 
     # Main program
-    try:
-        main()
-    except Exception as e:
-        error_handler(e)
+    main()