From 8ffa8ce4fd23039b946f339d035cbff94df0abfe Mon Sep 17 00:00:00 2001 From: Brad Edwards Date: Thu, 13 Aug 2026 04:51:34 +0200 Subject: [PATCH 1/2] fix(processor): enforce solver deadline boundaries --- .../raes_processor/satisfiability/_solver.py | 28 ++++++++---- .../tests/test_scenario_satisfiability.py | 45 ++++++++++++++++++- 2 files changed, 64 insertions(+), 9 deletions(-) diff --git a/implementations/python/packages/raes_processor/satisfiability/_solver.py b/implementations/python/packages/raes_processor/satisfiability/_solver.py index 10ad2ce7..cb29d653 100644 --- a/implementations/python/packages/raes_processor/satisfiability/_solver.py +++ b/implementations/python/packages/raes_processor/satisfiability/_solver.py @@ -96,21 +96,26 @@ class SolverResult: def solve_model(model: NormalizedConstraintModel) -> SolverResult: """Solve one normalized model and select deterministic portable evidence.""" + started_ns = _monotonic_ns() + budget = _solver_check_budget(model, started_ns=started_ns) _require_unique_clause_ids(model) all_clause_ids = tuple(clause.clause_id for clause in model.clauses) - budget = _solver_check_budget(model) + budget.checkpoint("model-validation", check_count=budget.checks_used) session = _SolverSession(model, budget) # ``_check`` fails loudly on ``z3.unknown``, so a non-satisfiable decision # here is decisively unsatisfiable rather than an incomplete timeout. if session.check(all_clause_ids, {}, phase="initial-decision") == z3.sat: - return SolverResult( + result = SolverResult( outcome=SatisfiabilityOutcome.SATISFIABLE, assignment=_select_witness(model, all_clause_ids, session), ) - return SolverResult( - outcome=SatisfiabilityOutcome.UNSATISFIABLE, - core=_reduce_unsat_core(all_clause_ids, session), - ) + else: + result = SolverResult( + outcome=SatisfiabilityOutcome.UNSATISFIABLE, + core=_reduce_unsat_core(all_clause_ids, session), + ) + budget.checkpoint("result-selection", check_count=budget.checks_used) + return result def _require_unique_clause_ids(model: NormalizedConstraintModel) -> None: @@ -125,12 +130,19 @@ def _require_unique_clause_ids(model: NormalizedConstraintModel) -> None: ) -def _solver_check_budget(model: NormalizedConstraintModel) -> _CheckBudget: +def _solver_check_budget( + model: NormalizedConstraintModel, + *, + started_ns: int | None = None, +) -> _CheckBudget: """Bound the two possible finite algorithms without a second profile knob.""" witness_checks = sum(len(symbol.domain) for symbol in model.symbols) core_checks = len(model.clauses) - return _CheckBudget(max_checks=1 + max(witness_checks, core_checks)) + return _CheckBudget( + max_checks=1 + max(witness_checks, core_checks), + started_ns=_monotonic_ns() if started_ns is None else started_ns, + ) def _select_witness( diff --git a/implementations/python/tests/test_scenario_satisfiability.py b/implementations/python/tests/test_scenario_satisfiability.py index e243d731..a22aeba5 100644 --- a/implementations/python/tests/test_scenario_satisfiability.py +++ b/implementations/python/tests/test_scenario_satisfiability.py @@ -655,7 +655,7 @@ def test_published_maximum_witness_shape_has_a_finite_derived_budget() -> None: def test_operation_deadline_covers_model_construction(monkeypatch: pytest.MonkeyPatch) -> None: - clock = iter((0, SOLVER_TIMEOUT_MS * 1_000_000)) + clock = iter((0, 0, SOLVER_TIMEOUT_MS * 1_000_000)) monkeypatch.setattr(solver_adapter.time, "monotonic_ns", clock.__next__) model = _normalized_model([1], [[]]) @@ -667,6 +667,25 @@ def test_operation_deadline_covers_model_construction(monkeypatch: pytest.Monkey assert raised.value.reason == "operation-deadline-exhausted" +def test_operation_deadline_starts_before_model_validation(monkeypatch: pytest.MonkeyPatch) -> None: + clock = {"now": 0} + original_validation = solver_adapter._require_unique_clause_ids + + def validation_finishing_at_deadline(model: NormalizedConstraintModel) -> None: + original_validation(model) + clock["now"] = SOLVER_TIMEOUT_MS * 1_000_000 + + monkeypatch.setattr(solver_adapter.time, "monotonic_ns", lambda: clock["now"]) + monkeypatch.setattr(solver_adapter, "_require_unique_clause_ids", validation_finishing_at_deadline) + + with pytest.raises(SolverOperationalError, match="operation deadline exhausted") as raised: + solve_model(_normalized_model([1], [[]])) + + assert raised.value.phase == "model-validation" + assert raised.value.check_count == 0 + assert raised.value.reason == "operation-deadline-exhausted" + + def test_result_returned_after_operation_deadline_is_rejected(monkeypatch: pytest.MonkeyPatch) -> None: clock = {"now": 0} original_check = z3.Solver.check @@ -686,3 +705,27 @@ def complete_after_deadline(self: z3.Solver, *assumptions: object) -> z3.CheckSa assert raised.value.phase == "initial-decision" assert raised.value.check_count == 1 assert raised.value.reason == "operation-deadline-exhausted" + + +def test_result_selection_finishing_at_operation_deadline_is_rejected(monkeypatch: pytest.MonkeyPatch) -> None: + clock = {"now": 0} + original_selection = solver_adapter._select_witness + + def selection_finishing_at_deadline( + model: NormalizedConstraintModel, + all_clause_ids: tuple[str, ...], + session: solver_adapter._SolverSession, + ) -> dict[str, str | int | bool]: + assignment = original_selection(model, all_clause_ids, session) + clock["now"] = SOLVER_TIMEOUT_MS * 1_000_000 + return assignment + + monkeypatch.setattr(solver_adapter.time, "monotonic_ns", lambda: clock["now"]) + monkeypatch.setattr(solver_adapter, "_select_witness", selection_finishing_at_deadline) + + with pytest.raises(SolverOperationalError, match="operation deadline exhausted") as raised: + solve_model(_normalized_model([1], [[]])) + + assert raised.value.phase == "result-selection" + assert raised.value.check_count == 2 + assert raised.value.reason == "operation-deadline-exhausted" From d86b2a12f823c6016db455824c7411462d56db76 Mon Sep 17 00:00:00 2001 From: Brad Edwards Date: Thu, 13 Aug 2026 05:05:00 +0200 Subject: [PATCH 2/2] test(processor): isolate deadline exception calls --- .../python/tests/test_scenario_satisfiability.py | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/implementations/python/tests/test_scenario_satisfiability.py b/implementations/python/tests/test_scenario_satisfiability.py index a22aeba5..92da9f97 100644 --- a/implementations/python/tests/test_scenario_satisfiability.py +++ b/implementations/python/tests/test_scenario_satisfiability.py @@ -677,9 +677,10 @@ def validation_finishing_at_deadline(model: NormalizedConstraintModel) -> None: monkeypatch.setattr(solver_adapter.time, "monotonic_ns", lambda: clock["now"]) monkeypatch.setattr(solver_adapter, "_require_unique_clause_ids", validation_finishing_at_deadline) + model = _normalized_model([1], [[]]) with pytest.raises(SolverOperationalError, match="operation deadline exhausted") as raised: - solve_model(_normalized_model([1], [[]])) + solve_model(model) assert raised.value.phase == "model-validation" assert raised.value.check_count == 0 @@ -722,9 +723,10 @@ def selection_finishing_at_deadline( monkeypatch.setattr(solver_adapter.time, "monotonic_ns", lambda: clock["now"]) monkeypatch.setattr(solver_adapter, "_select_witness", selection_finishing_at_deadline) + model = _normalized_model([1], [[]]) with pytest.raises(SolverOperationalError, match="operation deadline exhausted") as raised: - solve_model(_normalized_model([1], [[]])) + solve_model(model) assert raised.value.phase == "result-selection" assert raised.value.check_count == 2