Repository: CPMpy/cpmpy

Issue:
Time limit semantics
Every solver has the optional argument `time_limit` in its solve call.

Right now there are some inconsistencies:

```python
from cpmpy import *
model  = Model(boolvar())
model.solve(solver="ortools", time_limit=-1)
>> error
model.solve(solver="gurobi", time_limit=-1)
>> error
model.solve(solver="pysat", time_limit=-1)
>> True
model.solve(solver="z3", time_limit=-1)
>> True
model.solve(solver="minizinc", time_limit=-1)
>> False
```
I think a value <= 0 as time limit should correspond to "no time limit"

Thoughts?

Discussion:
@Wout4: There is no other viable way to interpret a negative time limit, so no time limit is the best option yes@hbierlee: I think a value of `<=0` should raise an exception (the user likely has made some mistake here).@Dimosts: On the other hand, I believe a value <=0 should be interpreted as do not solve.

This can happen in processes involving multiple solve calls e.g. in a loop, with a time limit for the entire process. Then, you want to stop and return in case you have already reached the time limit instead of giving infinite time!
@IgnaceBleukx: I think it's most appropriate to raise a TimeOutError when the time-limit is less than or equal to 0; this is easy to understand and catch by the caller too (and built into Python 😉 )
________________________________
From: Dimos Tsouros ***@***.***>
Sent: Thursday, April 10, 2025 11:42 PM
To: CPMpy/cpmpy ***@***.***>
Cc: Ignace Bleukx ***@***.***>; Author ***@***.***>
Subject: Re: [CPMpy/cpmpy] Time limit semantics (Issue #279)


On the other hand, I believe a value <=0 should be interpreted as do not solve.

This can happen in processes involving multiple solve calls e.g. in a loop, with a time limit for the entire process. Then, you want to stop and return in case you have already reached the time limit instead of giving infinite time!

—
Reply to this email directly, view it on GitHub<https://github.com/CPMpy/cpmpy/issues/279#issuecomment-2795229131>, or unsubscribe<https://github.com/notifications/unsubscribe-auth/AGG7YUPPF3KE3ZGREUIK3XL2Y3QTTAVCNFSM6AAAAAB23YN2VSVHI2DSMVQWIX3LMV43OSLTON2WKQ3PNVWWK3TUHMZDOOJVGIZDSMJTGE>.
You are receiving this because you authored the thread.Message ID: ***@***.***>

[https://avatars.githubusercontent.com/u/12712780?s=20&v=4]Dimosts left a comment (CPMpy/cpmpy#279)<https://github.com/CPMpy/cpmpy/issues/279#issuecomment-2795229131>

On the other hand, I believe a value <=0 should be interpreted as do not solve.

This can happen in processes involving multiple solve calls e.g. in a loop, with a time limit for the entire process. Then, you want to stop and return in case you have already reached the time limit instead of giving infinite time!

—
Reply to this email directly, view it on GitHub<https://github.com/CPMpy/cpmpy/issues/279#issuecomment-2795229131>, or unsubscribe<https://github.com/notifications/unsubscribe-auth/AGG7YUPPF3KE3ZGREUIK3XL2Y3QTTAVCNFSM6AAAAAB23YN2VSVHI2DSMVQWIX3LMV43OSLTON2WKQ3PNVWWK3TUHMZDOOJVGIZDSMJTGE>.
You are receiving this because you authored the thread.Message ID: ***@***.***>

[ { ***@***.***": "http://schema.org", ***@***.***": "EmailMessage", "potentialAction": { ***@***.***": "ViewAction", "target": "https://github.com/CPMpy/cpmpy/issues/279#issuecomment-2795229131", "url": "https://github.com/CPMpy/cpmpy/issues/279#issuecomment-2795229131", "name": "View Issue" }, "description": "View this Issue on GitHub", "publisher": { ***@***.***": "Organization", "name": "GitHub", "url": "https://github.com" } } ]
@hbierlee: I'd have a slight preference for `ValueError(f"Expected timeout to be positive but was {timeout}")` because we don't throw the TimeOutError when a regular timeout occurs. This regards -5 as an invalid timeout duration. If you think -5 can be interpreted as a valid timeout, then I agree it should timeout immediately rather than have no timeout.

Solution patch:
diff --git a/cpmpy/solvers/choco.py b/cpmpy/solvers/choco.py
index 52a8b704..10cfe9c6 100644
--- a/cpmpy/solvers/choco.py
+++ b/cpmpy/solvers/choco.py
@@ -157,8 +157,11 @@ class CPM_choco(SolverInterface):
         self.chc_solver = self.chc_model.get_solver()
 
         start = time.time()
-
+        
+        # set time limit
         if time_limit is not None:
+            if time_limit <= 0:
+                raise ValueError("Time limit must be positive")
             self.chc_solver.limit_time(str(time_limit) + "s")
 
         if self.has_objective():
diff --git a/cpmpy/solvers/cpo.py b/cpmpy/solvers/cpo.py
index 846e0e32..9f38efad 100644
--- a/cpmpy/solvers/cpo.py
+++ b/cpmpy/solvers/cpo.py
@@ -160,6 +160,10 @@ class CPM_cpo(SolverInterface):
         # call the solver, with parameters
         if 'LogVerbosity' not in kwargs:
             kwargs['LogVerbosity'] = 'Quiet'
+        
+        # set time limit
+        if time_limit is not None and time_limit <= 0:
+            raise ValueError("Time limit must be positive")
         self.cpo_result = self.cpo_model.solve(TimeLimit=time_limit, **kwargs)
 
         # new status, translate runtime
diff --git a/cpmpy/solvers/exact.py b/cpmpy/solvers/exact.py
index 03617599..2323dd45 100644
--- a/cpmpy/solvers/exact.py
+++ b/cpmpy/solvers/exact.py
@@ -198,10 +198,17 @@ class CPM_exact(SolverInterface):
             self.assumption_dict = {xct_var: (xct_val,cpm_assump) for (xct_var, xct_val, cpm_assump) in zip(assump_vars,assump_vals,assumptions)}
             self.xct_solver.setAssumptions(list(zip(assump_vars,assump_vals)))
 
+        # set time limit
+        if time_limit is not None:
+            if time_limit <= 0:
+                raise ValueError("Time limit must be positive")
+            timeout = time_limit
+        else:
+            timeout = 0
+            
         # call the solver, with parameters
         start = time.time()
-        my_status, obj_val = self.xct_solver.toOptimum(timeout=time_limit if time_limit is not None else 0)
-        #                                     timeout=time_limit if time_limit is not None else 0)
+        my_status, obj_val = self.xct_solver.toOptimum(timeout=timeout)
         end = time.time()
 
         # new status, translate runtime
diff --git a/cpmpy/solvers/gcs.py b/cpmpy/solvers/gcs.py
index 49b8dfdf..0da94f3d 100644
--- a/cpmpy/solvers/gcs.py
+++ b/cpmpy/solvers/gcs.py
@@ -162,6 +162,10 @@ class CPM_gcs(SolverInterface):
             self.proof_name = proof_name
         self.proof_location = proof_location
      
+        # set time limit
+        if time_limit is not None and time_limit <= 0:
+            raise ValueError("Time limit must be positive")
+                 
         # call the solver, with parameters    
         self.gcs_result = self.gcs.solve(
             all_solutions=self.has_objective(), 
@@ -209,6 +213,12 @@ class CPM_gcs(SolverInterface):
 
         # Verify proof, if requested
         if verify:
+
+            # set time limit
+            if verify_time_limit is not None:
+                if verify_time_limit <= 0:
+                    raise ValueError("Time limit for verifying must be positive")
+
             self.verify(name=self.proof_name, location=proof_location, time_limit=verify_time_limit,
                         veripb_args=veripb_args, display_output=display_verifier_output)
             
diff --git a/cpmpy/solvers/gurobi.py b/cpmpy/solvers/gurobi.py
index c859d55f..0b8afdde 100644
--- a/cpmpy/solvers/gurobi.py
+++ b/cpmpy/solvers/gurobi.py
@@ -161,8 +161,11 @@ class CPM_gurobi(SolverInterface):
 
         # ensure all vars are known to solver
         self.solver_vars(list(self.user_vars))
-
+        
+        # set time limit
         if time_limit is not None:
+            if time_limit <= 0:
+                raise ValueError("Time limit must be positive")
             self.grb_model.setParam("TimeLimit", time_limit)
 
         # call the solver, with parameters
diff --git a/cpmpy/solvers/minizinc.py b/cpmpy/solvers/minizinc.py
index 8c14f477..c575ce41 100644
--- a/cpmpy/solvers/minizinc.py
+++ b/cpmpy/solvers/minizinc.py
@@ -250,6 +250,9 @@ class CPM_minizinc(SolverInterface):
             Does not store the ``minizinc.Instance()`` or ``minizinc.Result()``
         """
 
+        if time_limit is not None and time_limit <= 0:
+            raise ValueError("Time limit must be positive")
+
         # ensure all vars are known to solver
         self.solver_vars(list(self.user_vars))
 
@@ -736,6 +739,11 @@ class CPM_minizinc(SolverInterface):
 
         import asyncio
 
+        # set time limit
+        if time_limit is not None:
+            if time_limit <= 0:
+                raise ValueError("Time limit must be positive")
+
         # HAD TO DEFINE OUR OWN ASYNC HANDLER
         coroutine = self._solveAll(display=display, time_limit=time_limit,
                                     solution_limit=solution_limit, **kwargs)
diff --git a/cpmpy/solvers/ortools.py b/cpmpy/solvers/ortools.py
index 6b86d728..9b754bc7 100644
--- a/cpmpy/solvers/ortools.py
+++ b/cpmpy/solvers/ortools.py
@@ -174,8 +174,10 @@ class CPM_ortools(SolverInterface):
         # ensure all user vars are known to solver
         self.solver_vars(list(self.user_vars))
 
-        # set time limit?
+        # set time limit
         if time_limit is not None:
+            if time_limit <= 0:
+                raise ValueError("Time limit must be positive")
             self.ort_solver.parameters.max_time_in_seconds = float(time_limit)
 
         if assumptions is not None:
diff --git a/cpmpy/solvers/pysat.py b/cpmpy/solvers/pysat.py
index c42a9122..6e8e614e 100644
--- a/cpmpy/solvers/pysat.py
+++ b/cpmpy/solvers/pysat.py
@@ -191,8 +191,11 @@ class CPM_pysat(SolverInterface):
             self.assumption_vars = assumptions
 
         import time
-        # set time limit?
+        # set time limit
         if time_limit is not None:
+            if time_limit <= 0:
+                raise ValueError("Time limit must be positive")
+            
             from threading import Timer
             t = Timer(time_limit, lambda s: s.interrupt(), [self.pysat_solver])
             t.start()
diff --git a/cpmpy/solvers/pysdd.py b/cpmpy/solvers/pysdd.py
index dbe126e8..d5c1e1a4 100644
--- a/cpmpy/solvers/pysdd.py
+++ b/cpmpy/solvers/pysdd.py
@@ -119,6 +119,9 @@ class CPM_pysdd(SolverInterface):
             - checking for a solution is trivial after that
         """
 
+        if time_limit is not None:
+            raise NotImplementedError("PySDD.solve(), time_limit not (yet?) supported")
+        
         # ensure all vars are known to solver
         self.solver_vars(list(self.user_vars))
 
diff --git a/cpmpy/solvers/z3.py b/cpmpy/solvers/z3.py
index dc0e4009..156a9c63 100644
--- a/cpmpy/solvers/z3.py
+++ b/cpmpy/solvers/z3.py
@@ -161,7 +161,10 @@ class CPM_z3(SolverInterface):
         # ensure all vars are known to solver
         self.solver_vars(list(self.user_vars))
 
+        # set time limit
         if time_limit is not None:
+            if time_limit <= 0:
+                raise ValueError("Time limit must be positive")
             # z3 expects milliseconds in int
             self.z3_solver.set(timeout=int(time_limit*1000))
 


Test patch:
diff --git a/tests/test_solvers.py b/tests/test_solvers.py
index 2705df7d..0db8ef33 100644
--- a/tests/test_solvers.py
+++ b/tests/test_solvers.py
@@ -694,6 +694,20 @@ class TestSupportedSolvers:
         s.solve()
         assert [int(a) for a in v.value()] == [0, 1, 0]
 
+    def test_time_limit(self, solver):
+        if solver == "pysdd": # pysdd does not support time limit
+            return
+        
+        x = cp.boolvar(shape=3)
+        m = cp.Model(x[0] | x[1] | x[2])
+        assert m.solve(solver=solver, time_limit=1)
+
+        try:
+            m.solve(solver=solver, time_limit=-1)
+            assert False
+        except ValueError:
+            pass
+
     def test_installed_solvers_solveAll(self, solver):
         # basic model
         v = cp.boolvar(3)