solver: add a timeout handle for users (#47661)

This PR adds a configuration setting to allow setting time limits for concretization.

For backward compatibility, the default is to set no time limit.

etc/spack/defaults/concretizer.yaml

@@ -55,3 +55,11 @@ concretizer:
   splice:
     explicit: []
     automatic: false
+  # Maximum time, in seconds, allowed for the 'solve' phase. If set to 0, there is no time limit.
+  timeout: 0
+  # If set to true, exceeding the timeout will always result in a concretization error. If false,
+  # the best (suboptimal) model computed before the timeout is used.
+  #
+  # Setting this to false yields unreproducible results, so we advise to use that value only
+  # for debugging purposes (e.g. check which constraints can help Spack concretize faster).
+  error_on_timeout: true

lib/spack/spack/schema/concretizer.py

@@ -88,6 +88,8 @@
                     "strategy": {"type": "string", "enum": ["none", "minimal", "full"]}
                 },
             },
+            "timeout": {"type": "integer", "minimum": 0},
+            "error_on_timeout": {"type": "boolean"},
             "os_compatible": {"type": "object", "additionalProperties": {"type": "array"}},
         },
     }

lib/spack/spack/solver/asp.py

@@ -885,7 +885,22 @@ def on_model(model):
             solve_kwargs["on_unsat"] = cores.append
 
         timer.start("solve")
-        solve_result = self.control.solve(**solve_kwargs)
+        time_limit = spack.config.CONFIG.get("concretizer:timeout", -1)
+        error_on_timeout = spack.config.CONFIG.get("concretizer:error_on_timeout", True)
+        # Spack uses 0 to set no time limit, clingo API uses -1
+        if time_limit == 0:
+            time_limit = -1
+        with self.control.solve(**solve_kwargs, async_=True) as handle:
+            finished = handle.wait(time_limit)
+            if not finished:
+                specs_str = ", ".join(llnl.util.lang.elide_list([str(s) for s in specs], 4))
+                header = f"Spack is taking more than {time_limit} seconds to solve for {specs_str}"
+                if error_on_timeout:
+                    raise UnsatisfiableSpecError(f"{header}, stopping concretization")
+                warnings.warn(f"{header}, using the best configuration found so far")
+                handle.cancel()
+
+            solve_result = handle.get()
         timer.stop("solve")
 
         # once done, construct the solve result