feat(constraint): exact integer 2-var solver — Cramer's rule, refusal-first (R2 C3)

generate/constraint_comprehension/solver.py: solve_two_var_linear (order-independent 2x2 integer Cramer's rule over typed constraints), the solve_two_var_count_weight specialization, and solve/answer_constraint_problem driving it from a ConstraintProblem. Four typed refusals: indistinguishable_weights (det==0), non_integer_solution (numer%det!=0, never rounds), negative_solution, verification_failed (identity backstop).

Ties to the C2 gold: solves all 7 solved fixtures to their gold value and refuses all 3 solver_refuses fixtures with EXACTLY the gold-claimed reason (the gold's reason is now solver-verified, not just annotation). Per-refusal meaningful-fail + positive re-substitution. Off-serving. 9 tests.

generate/constraint_comprehension/__init__.py

@@ -24,6 +24,12 @@ from generate.constraint_comprehension.model import (
     Domain,
     Unknown,
 )
+from generate.constraint_comprehension.solver import (
+    answer_constraint_problem,
+    solve_constraint_problem,
+    solve_two_var_count_weight,
+    solve_two_var_linear,
+)
 
 __all__ = [
     "AttributeFact",
@@ -34,4 +40,8 @@ __all__ = [
     "LinearExpr",
     "Relation",
     "Unknown",
+    "answer_constraint_problem",
+    "solve_constraint_problem",
+    "solve_two_var_count_weight",
+    "solve_two_var_linear",
 ]

generate/constraint_comprehension/solver.py

@@ -0,0 +1,106 @@
+"""Independent exact integer solver for the R2 two-variable linear system.
+
+Solves a two-variable, two-equation integer linear system by **exact Cramer's rule** — no
+floats, no nearest-option snapping. The R2 analogue of the relational-metric answer oracle:
+an independent decision procedure that consumes the *structured* constraints, never the text.
+
+Refusal-first (the wrong=0 boundary). The four ways a count/weight system has no honest
+nonnegative-integer answer each REFUSE with a typed reason, never a guessed value:
+
+- ``indistinguishable_weights`` — the system is singular (``det == 0``): the two equations
+  cannot separate the unknowns (e.g. equal per-category coefficients), so no unique solution.
+- ``non_integer_solution``      — Cramer's numerator is not divisible by the determinant:
+  no integer solution exists; the solver refuses rather than round.
+- ``negative_solution``         — a solved value is negative: invalid in the count domain.
+- ``verification_failed``       — a defensive re-substitution backstop (an algebraic identity
+  for the closed-form Cramer solution, so unreachable while the derivation is correct; retained
+  as a structural guard against future edits, NOT claimed as an independently-triggerable gate).
+
+The convenience ``solve_two_var_count_weight`` is the canonical ``x + y = N`` /
+``a·x + b·y = T`` specialization; ``solve_constraint_problem`` / ``answer_constraint_problem``
+drive it from a typed :class:`ConstraintProblem`. Off-serving: imports no
+``generate.derivation`` / ``core.reliability_gate``. Deterministic; no clock, no randomness.
+"""
+
+from __future__ import annotations
+
+from generate.constraint_comprehension.expr import LinearConstraint, LinearExpr
+from generate.constraint_comprehension.model import ConstraintProblem
+from generate.meaning_graph.reader import Refusal
+
+
+def _coeffs(constraint: LinearConstraint, x: str, y: str) -> tuple[int, int, int]:
+    """``(coeff_x, coeff_y, rhs - lhs_constant)`` for ``constraint`` over the variables x, y."""
+    cx = cy = 0
+    for symbol, coeff in constraint.lhs.terms:
+        if symbol == x:
+            cx += coeff
+        elif symbol == y:
+            cy += coeff
+    return cx, cy, constraint.rhs - constraint.lhs.constant
+
+
+def solve_two_var_linear(
+    c0: LinearConstraint, c1: LinearConstraint, *, nonnegative: bool = True
+) -> dict[str, int] | Refusal:
+    """Solve a 2-variable, 2-equation integer system over the SAME two symbols by Cramer's rule.
+
+    Precondition (guaranteed upstream by the C2 setup validator / the reader): both constraints
+    are ``eq`` over exactly two shared symbols. Returns ``{symbol: value}`` or a typed
+    :class:`Refusal` carrying one of the four solver reasons.
+    """
+    symbols = sorted({s for c in (c0, c1) for s, _ in c.lhs.terms})
+    if len(symbols) != 2:  # contract violation — upstream must guarantee two variables
+        raise ValueError(f"solver expects exactly two variables; got {symbols}")
+    x, y = symbols
+    p, q, r0 = _coeffs(c0, x, y)
+    r, s, r1 = _coeffs(c1, x, y)
+
+    det = p * s - q * r
+    if det == 0:
+        return Refusal("indistinguishable_weights", f"singular system over {x}/{y}")
+    num_x = r0 * s - q * r1
+    num_y = p * r1 - r0 * r
+    if num_x % det != 0 or num_y % det != 0:
+        return Refusal("non_integer_solution", f"no integer solution for {x}/{y}")
+    vx, vy = num_x // det, num_y // det
+    if nonnegative and (vx < 0 or vy < 0):
+        return Refusal("negative_solution", f"{x}={vx}, {y}={vy}")
+    if p * vx + q * vy != r0 or r * vx + s * vy != r1:  # pragma: no cover - identity backstop
+        return Refusal("verification_failed", "solution failed re-substitution")
+    return {x: vx, y: vy}
+
+
+def solve_two_var_count_weight(
+    x: str, y: str, total_count: int, x_weight: int, y_weight: int, weighted_total: int
+) -> dict[str, int] | Refusal:
+    """The canonical specialization: ``x + y = total_count`` and
+    ``x_weight·x + y_weight·y = weighted_total``. ``x`` / ``y`` are the symbol names."""
+    count = LinearConstraint(LinearExpr(((x, 1), (y, 1))), "eq", total_count)
+    weighted = LinearConstraint(LinearExpr(((x, x_weight), (y, y_weight))), "eq", weighted_total)
+    return solve_two_var_linear(count, weighted)
+
+
+def solve_constraint_problem(problem: ConstraintProblem) -> dict[str, int] | Refusal:
+    """Solve a two-constraint :class:`ConstraintProblem`'s system (order-independent)."""
+    if len(problem.constraints) != 2:  # contract violation — upstream guarantees two
+        raise ValueError(f"solver expects exactly two constraints; got {len(problem.constraints)}")
+    return solve_two_var_linear(problem.constraints[0], problem.constraints[1])
+
+
+def answer_constraint_problem(problem: ConstraintProblem) -> int | Refusal:
+    """Solve, then project to the asked unknown's value (or propagate the refusal)."""
+    solution = solve_constraint_problem(problem)
+    if isinstance(solution, Refusal):
+        return solution
+    if problem.query.symbol not in solution:  # pragma: no cover - query is a category (C2)
+        return Refusal("query_target_unsolved", problem.query.symbol)
+    return solution[problem.query.symbol]
+
+
+__all__ = [
+    "answer_constraint_problem",
+    "solve_constraint_problem",
+    "solve_two_var_count_weight",
+    "solve_two_var_linear",
+]

tests/test_constraint_solver.py

@@ -0,0 +1,98 @@
+"""Tests for the R2 exact integer solver (C3).
+
+Ties the solver to the C2 gold: every ``solved`` fixture computes its ``gold`` and every
+``solver_refuses`` fixture refuses with EXACTLY the reason the gold claims (so the gold's
+stated refusal reason is not just an annotation — the independent solver agrees). Each of the
+three reachable refusals is proven meaningful-fail, and every solution is re-substituted into
+its constraints (the verification backstop, exercised positively).
+"""
+
+from __future__ import annotations
+
+from evals.constraint_oracle.runner import _load_r2_gold, gold_to_problem
+from evals.constraint_oracle.signature import canonical_constraint
+from generate.constraint_comprehension.solver import (
+    answer_constraint_problem,
+    solve_constraint_problem,
+    solve_two_var_count_weight,
+    solve_two_var_linear,
+)
+from generate.meaning_graph.reader import Refusal
+
+
+def _solved() -> list[dict]:
+    return [f for f in _load_r2_gold() if f["expect"] == "solved"]
+
+
+def _solver_refuses() -> list[dict]:
+    return [f for f in _load_r2_gold() if f["expect"] == "solver_refuses"]
+
+
+def test_solver_solves_every_solved_gold_to_its_gold_value() -> None:
+    for fx in _solved():
+        problem = gold_to_problem(fx)
+        got = answer_constraint_problem(problem)
+        assert got == fx["gold"], f"{fx['id']}: got {got!r}, gold {fx['gold']!r}"
+
+
+def test_solver_solution_satisfies_both_constraints() -> None:
+    # The verification backstop, exercised positively: the solved values re-substitute exactly.
+    for fx in _solved():
+        problem = gold_to_problem(fx)
+        sol = solve_constraint_problem(problem)
+        assert isinstance(sol, dict), fx["id"]
+        for c in problem.constraints:
+            terms, _rel, rhs = canonical_constraint(c)
+            assert sum(coeff * sol[s] for s, coeff in terms) == rhs
+
+
+def test_solver_refuses_every_solver_refuse_gold_with_its_claimed_reason() -> None:
+    for fx in _solver_refuses():
+        problem = gold_to_problem(fx)
+        got = answer_constraint_problem(problem)
+        assert isinstance(got, Refusal), f"{fx['id']} should refuse"
+        assert got.reason == fx["solver_reason"], f"{fx['id']}: {got.reason} != {fx['solver_reason']}"
+
+
+def test_count_weight_convenience_matches_buses() -> None:
+    assert solve_two_var_count_weight("large_bus", "small_bus", 6, 50, 30, 260) == {
+        "large_bus": 4,
+        "small_bus": 2,
+    }
+
+
+def test_solver_is_constraint_order_independent() -> None:
+    fx = next(f for f in _solved() if f["id"] == "r2-002-chickens")
+    p = gold_to_problem(fx)
+    swapped = solve_two_var_linear(p.constraints[1], p.constraints[0])
+    assert swapped == solve_two_var_linear(p.constraints[0], p.constraints[1]) == {"chicken": 11, "cow": 7}
+
+
+# --- meaningful-fail: each reachable refusal fires under exactly its violation --------- #
+
+
+def test_indistinguishable_weights_refuses() -> None:
+    # Equal coefficients -> singular system -> no unique solution.
+    out = solve_two_var_count_weight("car", "truck", 8, 4, 4, 32)
+    assert isinstance(out, Refusal) and out.reason == "indistinguishable_weights"
+
+
+def test_non_integer_solution_refuses() -> None:
+    # 3*pen + 5*notebook = 37, pen+notebook=10 -> pen = 6.5: refuse, never round.
+    out = solve_two_var_count_weight("pen", "notebook", 10, 3, 5, 37)
+    assert isinstance(out, Refusal) and out.reason == "non_integer_solution"
+
+
+def test_negative_solution_refuses() -> None:
+    # 50*large + 30*small = 400, large+small=6 -> small=-5: refuse.
+    out = solve_two_var_count_weight("large_bus", "small_bus", 6, 50, 30, 400)
+    assert isinstance(out, Refusal) and out.reason == "negative_solution"
+
+
+def test_exact_integer_path_is_not_rounded() -> None:
+    # A near-miss that would round to a plausible integer: 3x+5y=38, x+y=10 -> x=6 exactly.
+    # (Guards that the solver computes exactly, not by snapping 37/38/39 to the same answer.)
+    assert solve_two_var_count_weight("x", "y", 10, 3, 5, 38) == {"x": 6, "y": 4}
+    assert isinstance(
+        solve_two_var_count_weight("x", "y", 10, 3, 5, 37), Refusal
+    )  # one less dollar -> no integer split