fix: make SIGALRM-based timeout no-op on Windows for cross-platform support

[Stevekaplanai]

Problem

On Windows, running mcp-solver-z3, mcp-solver-pysat, or mcp-solver-maxsat fails immediately when solve_model is called:

{'success': True, 'message': 'Failed to solve model', 'status': 'error', 'output': [], 'error': "AttributeError: module 'signal' has no attribute 'SIGALRM'"}

Root cause: time_limit() in each backend's environment.py uses signal.SIGALRM and signal.setitimer(signal.ITIMER_REAL, ...). Both are Unix-only — Windows' signal module doesn't expose them. This makes the entire Windows install path non-functional for these three backends. MiniZinc and ASP backends are unaffected (they use subprocess-based execution).

Fix

Patched time_limit() in all three affected environment.py files to detect the absence of SIGALRM / ITIMER_REAL at runtime via hasattr() and gracefully no-op the outer timeout on Windows. Unix behavior is unchanged.

The rationale for no-op (rather than emulating SIGALRM with threading.Timer):

• All three solvers expose their own internal timeout mechanism:
  • Z3: opt.set('timeout', ms) / solver.set('timeout', ms)
  • PySAT: Solver.conf_budget / Solver.prop_budget
  • MaxSAT: RC2(timeout=...) plus inherited PySAT budgets
• The outer wrapper was belt-and-suspenders for the case where user code runs longer than expected outside the solver call itself.
• Emulating signal-based interruption on Windows via threading.Timer can only set a flag, not preempt running code, so the semantics would diverge silently from the Unix path. Skipping the outer timeout entirely is more honest.
• Updated docstrings on each time_limit() make this tradeoff explicit and direct users to the solver-native timeout API.

Verification

Tested locally on Windows 11 (Python 3.13.13). Before the patch, the Z3 backend errored immediately on any solve_model call. After the patch, the canonical 3-of-6 picking problem solves correctly:

values = [10, 8, 7, 9, 6, 5]
pick = [Bool(f'p{i}') for i in range(6)]
opt = Optimize()
opt.set('timeout', 5000)
opt.add(Sum([If(p, 1, 0) for p in pick]) == 3)
opt.maximize(Sum([If(pick[i], values[i], 0) for i in range(6)]))

Returns picked: [0, 1, 3] (values 10 + 8 + 9 = 27), matching what the MiniZinc backend produces for the equivalent model and what the Z3 Python smoke test in INSTALL.md documents.

The patch is also a no-op on Linux/macOS — the hasattr() check passes, the full SIGALRM path runs as before. No CI changes required for Unix runners.

Files changed

• src/mcp_solver/z3/environment.py
• src/mcp_solver/pysat/environment.py
• src/mcp_solver/maxsat/environment.py

Notes for the maintainer

Happy to add a Windows runner to CI if you'd like — would catch this class of regression early. Just say the word and I'll send a follow-up PR.