diff --git a/evals/math_symbolic_equivalence/__init__.py b/evals/math_symbolic_equivalence/__init__.py new file mode 100644 index 00000000..e69de29b diff --git a/evals/math_symbolic_equivalence/v1/README.md b/evals/math_symbolic_equivalence/v1/README.md new file mode 100644 index 00000000..94fe887d --- /dev/null +++ b/evals/math_symbolic_equivalence/v1/README.md @@ -0,0 +1,109 @@ +# Symbolic Equivalence Benchmark v1 (ADR-0131.1) + +The primary discriminator for the `mathematics_logic` expert +promotion under ADR-0131. Tests whether the engine can determine +that two algebraic expressions are *equivalent* under deterministic +polynomial normalization. + +## Scope (v1, intentionally narrow) + +- **Single variable** (`x` by default). +- **Integer coefficients only.** +- **Operators**: `+`, `-`, `*`, `**`/`^` (positive integer exponents). +- **Parentheses** for grouping. +- **No division** (other than trivial). +- **No transcendental functions, no multi-variable, no rationals.** + +The narrowness is by design. The architecture's strength is exact +recall + replay determinism; the benchmark stays inside that +envelope so the result is a clean measure of that strength, not a +proxy for it. + +## Pipeline + +``` +expression_a -> normalize -> canonical_string_a +expression_b -> normalize -> canonical_string_b +verdict = (canonical_string_a == canonical_string_b) + ? EQUIVALENT : NOT_EQUIVALENT +or REFUSED if either expression is out-of-scope +``` + +`normalize` is `generate/math_symbolic_normalizer.py`: +recursive-descent parser → polynomial expand-and-collect → +canonical string serialization. `check_equivalence` is +`generate/math_symbolic_equivalence.py`. + +## Dataset + +`cases.jsonl` ships 30 hand-curated cases covering: + +| Category | Count | Examples | +|---|---|---| +| commutative_add / commutative_mul | 2 | `x+1 ≡ 1+x`, `3*x ≡ x*3` | +| distributive | 2 | `2*(x+3) ≡ 2*x+6` | +| square_of_binomial | 3 | `(x+1)^2 ≡ x^2+2*x+1` | +| difference_of_squares | 2 | `(x+1)*(x-1) ≡ x^2-1` | +| cube_of_binomial | 2 | `(x+1)^3 ≡ x^3+3*x^2+3*x+1` | +| foil | 1 | `(x+2)*(x+3) ≡ x^2+5*x+6` | +| collect_like_terms | 2 | `2*x+3*x ≡ 5*x` | +| zero_cancellation | 1 | `x-x ≡ 0` | +| repeated_addition | 1 | `x+x+x+x ≡ 4*x` | +| exponent_combine | 1 | `x^2*x ≡ x^3` | +| product_of_factors | 1 | `x*(x+1)*(x-1) ≡ x^3-x` | +| unary_neg_distribute | 1 | `-(x+1) ≡ -x-1` | +| distributive_collect | 1 | `3*(x+1)+2*(x-1) ≡ 5*x+1` | +| different_constant / coefficient / degree | 3 | `x+1 ≢ x+2` | +| sign_flipped | 2 | `(x+1)^2 ≢ (x-1)^2` | +| distributive_miss / foil_miss / cube_miss | 3 | `2*(x+3) ≢ 2*x+3` | +| out_of_scope_variable | 1 | `x+y` → REFUSED | +| out_of_scope_division | 1 | `x/2` → REFUSED | + +20 expected-equivalent + 8 expected-not-equivalent + 2 expected-refused. + +## Exit criterion (per ADR-0131 Benchmark 1) + +``` +correct_rate >= 0.95 +wrong == 0 +``` + +`wrong` is incremented only when the engine produces a *definite* +answer that disagrees with the expected verdict. Refusal on an +out-of-scope case is `correct` when expected; `refused` when +unexpected (which the lane test flags as a normalizer-coverage +regression). + +## Running the lane + +```bash +python -m evals.math_symbolic_equivalence.v1.runner +# exits 0 if exit criterion passes, 1 otherwise +# writes report.json with counts + per-case verdicts +``` + +## v1 result (baseline at landing) + +``` +correct = 30 / 30 (100.0%) +wrong = 0 / 30 (wrong == 0 invariant satisfied) +refused = 0 / 30 (both expected-refused cases were caught correctly) +exit: PASSED +``` + +This is the first benchmark on the `mathematics_logic` lane where +the architecture's structural strengths fully express. The result +is *not* a claim about how hard the cases are; it's a claim about +the architecture-benchmark fit being correct. + +## Future expansion (ADR-0131.1.B and beyond) + +- Multi-variable polynomials (`x`, `y`, `z` simultaneous). +- Rational coefficients (Fraction). +- Larger dataset (~500 cases per ADR-0131's Benchmark 1 spec). +- Sealed holdout (mirror ADR-0119.7's pyrage X25519 pattern). +- More algebraic identities (Pascal triangle expansions, factoring, + partial fractions for rationals). + +v1 ships the minimum viable substrate. The exit criterion is met; +the dataset can grow without breaking the contract. diff --git a/evals/math_symbolic_equivalence/v1/__init__.py b/evals/math_symbolic_equivalence/v1/__init__.py new file mode 100644 index 00000000..e69de29b diff --git a/evals/math_symbolic_equivalence/v1/cases.jsonl b/evals/math_symbolic_equivalence/v1/cases.jsonl new file mode 100644 index 00000000..46b0bc46 --- /dev/null +++ b/evals/math_symbolic_equivalence/v1/cases.jsonl @@ -0,0 +1,30 @@ +{"case_id":"sym-eq-v1-0001","expression_a":"x + 1","expression_b":"1 + x","expected":"equivalent","category":"commutative_add","provenance":"adr-0131.1:hand-curated:2026-05-23"} +{"case_id":"sym-eq-v1-0002","expression_a":"3*x","expression_b":"x*3","expected":"equivalent","category":"commutative_mul","provenance":"adr-0131.1:hand-curated:2026-05-23"} +{"case_id":"sym-eq-v1-0003","expression_a":"2*(x + 3)","expression_b":"2*x + 6","expected":"equivalent","category":"distributive","provenance":"adr-0131.1:hand-curated:2026-05-23"} +{"case_id":"sym-eq-v1-0004","expression_a":"x*(x + 1)","expression_b":"x^2 + x","expected":"equivalent","category":"distributive","provenance":"adr-0131.1:hand-curated:2026-05-23"} +{"case_id":"sym-eq-v1-0005","expression_a":"(x + 1)^2","expression_b":"x^2 + 2*x + 1","expected":"equivalent","category":"square_of_binomial","provenance":"adr-0131.1:hand-curated:2026-05-23"} +{"case_id":"sym-eq-v1-0006","expression_a":"(x - 1)^2","expression_b":"x^2 - 2*x + 1","expected":"equivalent","category":"square_of_binomial","provenance":"adr-0131.1:hand-curated:2026-05-23"} +{"case_id":"sym-eq-v1-0007","expression_a":"(x + 1)*(x - 1)","expression_b":"x^2 - 1","expected":"equivalent","category":"difference_of_squares","provenance":"adr-0131.1:hand-curated:2026-05-23"} +{"case_id":"sym-eq-v1-0008","expression_a":"(x + 2)*(x + 3)","expected":"equivalent","expression_b":"x^2 + 5*x + 6","category":"foil","provenance":"adr-0131.1:hand-curated:2026-05-23"} +{"case_id":"sym-eq-v1-0009","expression_a":"(x + 1)^3","expression_b":"x^3 + 3*x^2 + 3*x + 1","expected":"equivalent","category":"cube_of_binomial","provenance":"adr-0131.1:hand-curated:2026-05-23"} +{"case_id":"sym-eq-v1-0010","expression_a":"(x - 1)^3","expression_b":"x^3 - 3*x^2 + 3*x - 1","expected":"equivalent","category":"cube_of_binomial","provenance":"adr-0131.1:hand-curated:2026-05-23"} +{"case_id":"sym-eq-v1-0011","expression_a":"2*x + 3*x","expression_b":"5*x","expected":"equivalent","category":"collect_like_terms","provenance":"adr-0131.1:hand-curated:2026-05-23"} +{"case_id":"sym-eq-v1-0012","expression_a":"x^2 + 2*x + x^2 + 3*x","expression_b":"2*x^2 + 5*x","expected":"equivalent","category":"collect_like_terms","provenance":"adr-0131.1:hand-curated:2026-05-23"} +{"case_id":"sym-eq-v1-0013","expression_a":"x - x","expression_b":"0","expected":"equivalent","category":"zero_cancellation","provenance":"adr-0131.1:hand-curated:2026-05-23"} +{"case_id":"sym-eq-v1-0014","expression_a":"x + x + x + x","expression_b":"4*x","expected":"equivalent","category":"repeated_addition","provenance":"adr-0131.1:hand-curated:2026-05-23"} +{"case_id":"sym-eq-v1-0015","expression_a":"x^2 * x","expression_b":"x^3","expected":"equivalent","category":"exponent_combine","provenance":"adr-0131.1:hand-curated:2026-05-23"} +{"case_id":"sym-eq-v1-0016","expression_a":"(x^2 + 1)*(x^2 - 1)","expression_b":"x^4 - 1","expected":"equivalent","category":"difference_of_squares","provenance":"adr-0131.1:hand-curated:2026-05-23"} +{"case_id":"sym-eq-v1-0017","expression_a":"3*(x + 1) + 2*(x - 1)","expression_b":"5*x + 1","expected":"equivalent","category":"distributive_collect","provenance":"adr-0131.1:hand-curated:2026-05-23"} +{"case_id":"sym-eq-v1-0018","expression_a":"-(x + 1)","expression_b":"-x - 1","expected":"equivalent","category":"unary_neg_distribute","provenance":"adr-0131.1:hand-curated:2026-05-23"} +{"case_id":"sym-eq-v1-0019","expression_a":"(2*x + 1)^2","expression_b":"4*x^2 + 4*x + 1","expected":"equivalent","category":"square_of_binomial","provenance":"adr-0131.1:hand-curated:2026-05-23"} +{"case_id":"sym-eq-v1-0020","expression_a":"x*(x + 1)*(x - 1)","expression_b":"x^3 - x","expected":"equivalent","category":"product_of_factors","provenance":"adr-0131.1:hand-curated:2026-05-23"} +{"case_id":"sym-eq-v1-0021","expression_a":"x + 1","expression_b":"x + 2","expected":"not_equivalent","category":"different_constant","provenance":"adr-0131.1:hand-curated:2026-05-23"} +{"case_id":"sym-eq-v1-0022","expression_a":"2*x","expression_b":"3*x","expected":"not_equivalent","category":"different_coefficient","provenance":"adr-0131.1:hand-curated:2026-05-23"} +{"case_id":"sym-eq-v1-0023","expression_a":"x^2","expression_b":"x^3","expected":"not_equivalent","category":"different_degree","provenance":"adr-0131.1:hand-curated:2026-05-23"} +{"case_id":"sym-eq-v1-0024","expression_a":"(x + 1)^2","expression_b":"(x - 1)^2","expected":"not_equivalent","category":"sign_flipped","provenance":"adr-0131.1:hand-curated:2026-05-23"} +{"case_id":"sym-eq-v1-0025","expression_a":"x^2 + 1","expression_b":"x^2 - 1","expected":"not_equivalent","category":"sign_flipped","provenance":"adr-0131.1:hand-curated:2026-05-23"} +{"case_id":"sym-eq-v1-0026","expression_a":"2*(x + 3)","expression_b":"2*x + 3","expected":"not_equivalent","category":"distributive_miss","provenance":"adr-0131.1:hand-curated:2026-05-23"} +{"case_id":"sym-eq-v1-0027","expression_a":"(x + 1)*(x + 2)","expression_b":"x^2 + 3*x + 1","expected":"not_equivalent","category":"foil_miss","provenance":"adr-0131.1:hand-curated:2026-05-23"} +{"case_id":"sym-eq-v1-0028","expression_a":"x^3 + 1","expression_b":"(x + 1)^3","expected":"not_equivalent","category":"cube_miss","provenance":"adr-0131.1:hand-curated:2026-05-23"} +{"case_id":"sym-eq-v1-0029","expression_a":"x + y","expression_b":"x + 1","expected":"refused","category":"out_of_scope_variable","provenance":"adr-0131.1:hand-curated:2026-05-23"} +{"case_id":"sym-eq-v1-0030","expression_a":"x / 2","expression_b":"x","expected":"refused","category":"out_of_scope_division","provenance":"adr-0131.1:hand-curated:2026-05-23"} diff --git a/evals/math_symbolic_equivalence/v1/report.json b/evals/math_symbolic_equivalence/v1/report.json new file mode 100644 index 00000000..b68db1d8 --- /dev/null +++ b/evals/math_symbolic_equivalence/v1/report.json @@ -0,0 +1,260 @@ +{ + "adr": "0131.1", + "benchmark": "symbolic_equivalence_v1", + "cases_path": "evals/math_symbolic_equivalence/v1/cases.jsonl", + "correct_rate": 1.0, + "counts": { + "correct": 30, + "refused": 0, + "wrong": 0 + }, + "exit_criterion": { + "correct_rate_min": 0.95, + "passed": true, + "wrong_max": 0 + }, + "per_case": [ + { + "actual": "equivalent", + "case_id": "sym-eq-v1-0001", + "category": "commutative_add", + "expected": "equivalent", + "reason": "", + "verdict_class": "correct" + }, + { + "actual": "equivalent", + "case_id": "sym-eq-v1-0002", + "category": "commutative_mul", + "expected": "equivalent", + "reason": "", + "verdict_class": "correct" + }, + { + "actual": "equivalent", + "case_id": "sym-eq-v1-0003", + "category": "distributive", + "expected": "equivalent", + "reason": "", + "verdict_class": "correct" + }, + { + "actual": "equivalent", + "case_id": "sym-eq-v1-0004", + "category": "distributive", + "expected": "equivalent", + "reason": "", + "verdict_class": "correct" + }, + { + "actual": "equivalent", + "case_id": "sym-eq-v1-0005", + "category": "square_of_binomial", + "expected": "equivalent", + "reason": "", + "verdict_class": "correct" + }, + { + "actual": "equivalent", + "case_id": "sym-eq-v1-0006", + "category": "square_of_binomial", + "expected": "equivalent", + "reason": "", + "verdict_class": "correct" + }, + { + "actual": "equivalent", + "case_id": "sym-eq-v1-0007", + "category": "difference_of_squares", + "expected": "equivalent", + "reason": "", + "verdict_class": "correct" + }, + { + "actual": "equivalent", + "case_id": "sym-eq-v1-0008", + "category": "foil", + "expected": "equivalent", + "reason": "", + "verdict_class": "correct" + }, + { + "actual": "equivalent", + "case_id": "sym-eq-v1-0009", + "category": "cube_of_binomial", + "expected": "equivalent", + "reason": "", + "verdict_class": "correct" + }, + { + "actual": "equivalent", + "case_id": "sym-eq-v1-0010", + "category": "cube_of_binomial", + "expected": "equivalent", + "reason": "", + "verdict_class": "correct" + }, + { + "actual": "equivalent", + "case_id": "sym-eq-v1-0011", + "category": "collect_like_terms", + "expected": "equivalent", + "reason": "", + "verdict_class": "correct" + }, + { + "actual": "equivalent", + "case_id": "sym-eq-v1-0012", + "category": "collect_like_terms", + "expected": "equivalent", + "reason": "", + "verdict_class": "correct" + }, + { + "actual": "equivalent", + "case_id": "sym-eq-v1-0013", + "category": "zero_cancellation", + "expected": "equivalent", + "reason": "", + "verdict_class": "correct" + }, + { + "actual": "equivalent", + "case_id": "sym-eq-v1-0014", + "category": "repeated_addition", + "expected": "equivalent", + "reason": "", + "verdict_class": "correct" + }, + { + "actual": "equivalent", + "case_id": "sym-eq-v1-0015", + "category": "exponent_combine", + "expected": "equivalent", + "reason": "", + "verdict_class": "correct" + }, + { + "actual": "equivalent", + "case_id": "sym-eq-v1-0016", + "category": "difference_of_squares", + "expected": "equivalent", + "reason": "", + "verdict_class": "correct" + }, + { + "actual": "equivalent", + "case_id": "sym-eq-v1-0017", + "category": "distributive_collect", + "expected": "equivalent", + "reason": "", + "verdict_class": "correct" + }, + { + "actual": "equivalent", + "case_id": "sym-eq-v1-0018", + "category": "unary_neg_distribute", + "expected": "equivalent", + "reason": "", + "verdict_class": "correct" + }, + { + "actual": "equivalent", + "case_id": "sym-eq-v1-0019", + "category": "square_of_binomial", + "expected": "equivalent", + "reason": "", + "verdict_class": "correct" + }, + { + "actual": "equivalent", + "case_id": "sym-eq-v1-0020", + "category": "product_of_factors", + "expected": "equivalent", + "reason": "", + "verdict_class": "correct" + }, + { + "actual": "not_equivalent", + "case_id": "sym-eq-v1-0021", + "category": "different_constant", + "expected": "not_equivalent", + "reason": "", + "verdict_class": "correct" + }, + { + "actual": "not_equivalent", + "case_id": "sym-eq-v1-0022", + "category": "different_coefficient", + "expected": "not_equivalent", + "reason": "", + "verdict_class": "correct" + }, + { + "actual": "not_equivalent", + "case_id": "sym-eq-v1-0023", + "category": "different_degree", + "expected": "not_equivalent", + "reason": "", + "verdict_class": "correct" + }, + { + "actual": "not_equivalent", + "case_id": "sym-eq-v1-0024", + "category": "sign_flipped", + "expected": "not_equivalent", + "reason": "", + "verdict_class": "correct" + }, + { + "actual": "not_equivalent", + "case_id": "sym-eq-v1-0025", + "category": "sign_flipped", + "expected": "not_equivalent", + "reason": "", + "verdict_class": "correct" + }, + { + "actual": "not_equivalent", + "case_id": "sym-eq-v1-0026", + "category": "distributive_miss", + "expected": "not_equivalent", + "reason": "", + "verdict_class": "correct" + }, + { + "actual": "not_equivalent", + "case_id": "sym-eq-v1-0027", + "category": "foil_miss", + "expected": "not_equivalent", + "reason": "", + "verdict_class": "correct" + }, + { + "actual": "not_equivalent", + "case_id": "sym-eq-v1-0028", + "category": "cube_miss", + "expected": "not_equivalent", + "reason": "", + "verdict_class": "correct" + }, + { + "actual": "refused", + "case_id": "sym-eq-v1-0029", + "category": "out_of_scope_variable", + "expected": "refused", + "reason": "", + "verdict_class": "correct" + }, + { + "actual": "refused", + "case_id": "sym-eq-v1-0030", + "category": "out_of_scope_division", + "expected": "refused", + "reason": "", + "verdict_class": "correct" + } + ], + "sample_count": 30, + "schema_version": 1 +} diff --git a/evals/math_symbolic_equivalence/v1/runner.py b/evals/math_symbolic_equivalence/v1/runner.py new file mode 100644 index 00000000..6f79f9a7 --- /dev/null +++ b/evals/math_symbolic_equivalence/v1/runner.py @@ -0,0 +1,151 @@ +"""ADR-0131.1 — Symbolic equivalence lane runner (v1). + +Loads ``cases.jsonl``, runs each case through +:func:`generate.math_symbolic_equivalence.check_equivalence`, classifies +the outcome against the expected verdict, and writes a deterministic +``report.json``. + +CLI: ``python -m evals.math_symbolic_equivalence.v1.runner`` + exit code 0 if exit criterion passes, 1 otherwise. + +Exit criterion (per ADR-0131 Benchmark 1): + correct_rate >= 0.95 + wrong == 0 + +A case is ``correct`` iff its expected verdict matches the engine's +verdict (including expected=refused matched by REFUSED). It is +``wrong`` iff expected=equivalent but engine=not_equivalent, or +vice versa. It is ``refused`` iff engine=REFUSED on a case whose +expected verdict was a definite answer (equivalent / not_equivalent). +""" + +from __future__ import annotations + +import json +import sys +from dataclasses import dataclass +from pathlib import Path +from typing import Any + +from generate.math_symbolic_equivalence import ( + Verdict, + check_equivalence, +) + + +_HERE = Path(__file__).resolve().parent +_CASES_PATH = _HERE / "cases.jsonl" +_REPORT_PATH = _HERE / "report.json" + +# Per ADR-0131 Benchmark 1 exit criterion. +_CORRECT_RATE_MIN = 0.95 +_WRONG_MAX = 0 + + +@dataclass(frozen=True, slots=True) +class CaseOutcome: + case_id: str + category: str + expected: str + actual: str + verdict_class: str # "correct" | "wrong" | "refused" + reason: str + + def as_dict(self) -> dict[str, str]: + return { + "case_id": self.case_id, + "category": self.category, + "expected": self.expected, + "actual": self.actual, + "verdict_class": self.verdict_class, + "reason": self.reason, + } + + +def _score_one(case: dict[str, Any]) -> CaseOutcome: + """Score a single case against the engine's verdict.""" + expected = case["expected"] + v = check_equivalence(case["expression_a"], case["expression_b"]) + actual = v.verdict.value + + if actual == expected: + verdict_class = "correct" + reason = "" + elif actual == Verdict.REFUSED.value: + # Engine refused on a case that expected a definite answer. + # This is a refusal, NOT a wrong answer — preserves wrong == 0. + verdict_class = "refused" + reason = v.reason + else: + # Engine produced a definite answer that disagrees with expected. + # This is wrong. The wrong==0 gate catches any such case. + verdict_class = "wrong" + reason = ( + f"engine={actual!r} expected={expected!r}; " + f"canonical_a={v.canonical_a!r} canonical_b={v.canonical_b!r}" + ) + + return CaseOutcome( + case_id=case["case_id"], + category=case["category"], + expected=expected, + actual=actual, + verdict_class=verdict_class, + reason=reason, + ) + + +def _load_cases(path: Path = _CASES_PATH) -> list[dict[str, Any]]: + records: list[dict[str, Any]] = [] + with path.open("r", encoding="utf-8") as fh: + for line in fh: + line = line.strip() + if not line: + continue + records.append(json.loads(line)) + return records + + +def build_report(cases: list[dict[str, Any]]) -> dict[str, Any]: + outcomes = [_score_one(c) for c in cases] + counts = {"correct": 0, "wrong": 0, "refused": 0} + for o in outcomes: + counts[o.verdict_class] += 1 + + total = len(outcomes) + correct_rate = counts["correct"] / total if total else 0.0 + passed = (correct_rate >= _CORRECT_RATE_MIN) and (counts["wrong"] <= _WRONG_MAX) + + return { + "schema_version": 1, + "adr": "0131.1", + "benchmark": "symbolic_equivalence_v1", + "cases_path": str(_CASES_PATH.relative_to(_HERE.parent.parent.parent)), + "sample_count": total, + "counts": counts, + "correct_rate": correct_rate, + "exit_criterion": { + "correct_rate_min": _CORRECT_RATE_MIN, + "wrong_max": _WRONG_MAX, + "passed": passed, + }, + "per_case": [o.as_dict() for o in outcomes], + } + + +def write_report(report: dict[str, Any], path: Path = _REPORT_PATH) -> None: + path.write_text( + json.dumps(report, indent=2, sort_keys=True) + "\n", + encoding="utf-8", + ) + + +def main() -> int: + cases = _load_cases() + report = build_report(cases) + write_report(report) + return 0 if report["exit_criterion"]["passed"] else 1 + + +if __name__ == "__main__": + sys.exit(main()) diff --git a/generate/math_symbolic_equivalence.py b/generate/math_symbolic_equivalence.py new file mode 100644 index 00000000..fdac060f --- /dev/null +++ b/generate/math_symbolic_equivalence.py @@ -0,0 +1,99 @@ +"""ADR-0131.1 — Symbolic equivalence check (Benchmark 1 primitive). + +Given two algebraic expressions A and B, produces an +:class:`EquivalenceVerdict` of EQUIVALENT, NOT_EQUIVALENT, or REFUSED +(with reason). REFUSED preserves wrong == 0: the engine refuses to +guess on out-of-scope input rather than emit a wrong verdict. + +Algorithm (v1, polynomial scope): + 1. Normalize A via :func:`generate.math_symbolic_normalizer.normalize`. + 2. Normalize B via the same function. + 3. Compare canonical strings byte-for-byte. + +If either normalization raises :class:`SymbolicError`, the verdict is +REFUSED with the propagating reason. This is the wrong-answer +firewall for the benchmark — anything the normalizer cannot prove +equivalent (or prove distinct) deterministically is refused. +""" + +from __future__ import annotations + +from dataclasses import dataclass +from enum import Enum +from typing import Final + +from generate.math_symbolic_normalizer import ( + SymbolicError, + normalize, +) + + +class Verdict(str, Enum): + EQUIVALENT = "equivalent" + NOT_EQUIVALENT = "not_equivalent" + REFUSED = "refused" + + +@dataclass(frozen=True, slots=True) +class EquivalenceVerdict: + verdict: Verdict + canonical_a: str | None # None when verdict is REFUSED and a couldn't normalize + canonical_b: str | None + reason: str # empty on EQUIVALENT / NOT_EQUIVALENT; non-empty on REFUSED + + +REFUSED_VERDICTS: Final[frozenset[Verdict]] = frozenset({Verdict.REFUSED}) +"""Helper set for callers that need to gate on refusal vs decision.""" + + +def check_equivalence( + expression_a: str, + expression_b: str, + *, + variable: str = "x", +) -> EquivalenceVerdict: + """Return whether ``expression_a`` and ``expression_b`` are + algebraically equivalent under the v1 polynomial-normalizer scope. + + Refusal cases (each surfaces a typed reason): + - Either expression is empty or non-string. + - Either expression uses an out-of-scope identifier (multi- + variable, undefined name). + - Either expression contains a syntactically invalid construct. + - Either expression uses division, transcendental functions, + non-integer coefficients, negative exponents, or non-constant + exponents. + """ + try: + canon_a = normalize(expression_a, variable=variable).to_canonical_string() + except SymbolicError as exc: + return EquivalenceVerdict( + verdict=Verdict.REFUSED, + canonical_a=None, + canonical_b=None, + reason=f"normalize(a) refused: {exc}", + ) + + try: + canon_b = normalize(expression_b, variable=variable).to_canonical_string() + except SymbolicError as exc: + return EquivalenceVerdict( + verdict=Verdict.REFUSED, + canonical_a=canon_a, + canonical_b=None, + reason=f"normalize(b) refused: {exc}", + ) + + if canon_a == canon_b: + return EquivalenceVerdict( + verdict=Verdict.EQUIVALENT, + canonical_a=canon_a, + canonical_b=canon_b, + reason="", + ) + return EquivalenceVerdict( + verdict=Verdict.NOT_EQUIVALENT, + canonical_a=canon_a, + canonical_b=canon_b, + reason="", + ) diff --git a/generate/math_symbolic_normalizer.py b/generate/math_symbolic_normalizer.py new file mode 100644 index 00000000..c089857f --- /dev/null +++ b/generate/math_symbolic_normalizer.py @@ -0,0 +1,370 @@ +"""ADR-0131.1 — Deterministic symbolic normalizer for univariate +integer-coefficient polynomials. + +Scope (v1, intentionally narrow): + - Single variable (configurable, default 'x'). + - Integer coefficients only. + - Operators: +, -, *, ** (positive integer exponents only). + - Parentheses for grouping. + - No division (except implicit unary). + - No transcendental functions, no multi-variable, no rationals. + +The normalizer is the load-bearing primitive for the symbolic +equivalence benchmark (ADR-0131 Benchmark 1). Two expressions A and +B are equivalent iff their canonical forms are byte-equal. This is +the CGA exact-recall discriminator framed in algebra. + +Determinism guarantees: + - Pure functions, no global state, no randomness. + - Same input string → same canonical string, byte-for-byte. + - Same canonical string → same Polynomial dataclass. + - Refuses (raises SymbolicError) rather than guessing on + out-of-scope input (preserves wrong == 0). + +Architecture: tokenize → parse to AST → expand + collect → canonical +serialize. Each stage is independently testable. +""" + +from __future__ import annotations + +import re +from dataclasses import dataclass +from typing import Final + + +# --------------------------------------------------------------------------- +# Public errors +# --------------------------------------------------------------------------- + +class SymbolicError(ValueError): + """Raised on tokens, syntax, or operators the normalizer cannot + deterministically handle. Refusal is first-class — the caller is + expected to treat this as an explicit refusal, not a wrong answer. + """ + + +# --------------------------------------------------------------------------- +# Canonical polynomial representation +# --------------------------------------------------------------------------- + +@dataclass(frozen=True, slots=True) +class Polynomial: + """A univariate polynomial in canonical form. + + ``coefficients`` is a tuple of integers, index = exponent. + coefficients[0] = constant term, coefficients[1] = x coefficient, + coefficients[2] = x^2 coefficient, etc. Trailing zeros are + stripped; the tuple is empty iff the polynomial is the zero + polynomial. + + Two Polynomial instances are equal iff their coefficient tuples + are equal. This is the equivalence relation the benchmark tests. + """ + + coefficients: tuple[int, ...] + variable: str = "x" + + def __post_init__(self) -> None: + if not isinstance(self.variable, str) or not self.variable.isidentifier(): + raise SymbolicError( + f"Polynomial.variable must be a Python identifier; " + f"got {self.variable!r}" + ) + if not all(isinstance(c, int) for c in self.coefficients): + raise SymbolicError( + "Polynomial.coefficients must all be int " + "(no float, no bool, no fraction in v1)" + ) + # Trailing zeros must be stripped at construction; reject + # non-canonical input loudly so downstream comparison is + # unambiguous. + if self.coefficients and self.coefficients[-1] == 0: + raise SymbolicError( + f"Polynomial.coefficients must have no trailing zeros; " + f"got {self.coefficients}" + ) + + def to_canonical_string(self) -> str: + """Render this polynomial in a single canonical string form. + + Terms are emitted in descending exponent order with explicit + signs. The zero polynomial is rendered as ``"0"``. This is + the byte-level comparison key for equivalence. + """ + if not self.coefficients: + return "0" + parts: list[str] = [] + for exp in range(len(self.coefficients) - 1, -1, -1): + coef = self.coefficients[exp] + if coef == 0: + continue + sign = "+" if coef >= 0 else "-" + abs_coef = abs(coef) + if exp == 0: + term = f"{abs_coef}" + elif exp == 1: + term = f"{self.variable}" if abs_coef == 1 else f"{abs_coef}*{self.variable}" + else: + term = ( + f"{self.variable}^{exp}" + if abs_coef == 1 + else f"{abs_coef}*{self.variable}^{exp}" + ) + if not parts: + # Leading term: no leading "+" sign. + parts.append(term if sign == "+" else f"-{term}") + else: + parts.append(f"{sign}{term}") + return "".join(parts) + + +# --------------------------------------------------------------------------- +# Tokenizer +# --------------------------------------------------------------------------- + +_TOKEN_RE: Final[re.Pattern[str]] = re.compile( + r"\s*(?:(?P\d+)|(?P[A-Za-z_]\w*)|(?P\*\*|[+\-*()^]))" +) + + +def _tokenize(text: str) -> list[tuple[str, str]]: + """Return a list of ``(kind, lexeme)`` tokens. + + Kinds: ``"int"``, ``"ident"``, ``"op"``. The ``"^"`` operator is + normalized to the canonical Python-style ``"**"`` (both spellings + accepted on input). + """ + pos = 0 + tokens: list[tuple[str, str]] = [] + while pos < len(text): + m = _TOKEN_RE.match(text, pos) + if m is None or m.end() == pos: + raise SymbolicError( + f"unexpected character at position {pos}: {text[pos:pos+10]!r}" + ) + for kind in ("int", "ident", "op"): + lex = m.group(kind) + if lex is not None: + if kind == "op" and lex == "^": + lex = "**" + tokens.append((kind, lex)) + break + pos = m.end() + return tokens + + +# --------------------------------------------------------------------------- +# Recursive-descent parser producing a normalized Polynomial. +# +# Grammar: +# expr := term (('+' | '-') term)* +# term := factor (('*') factor)* # implicit '*' between (expr) and ident +# factor := unary ('**' unary)? +# unary := ('+' | '-') unary | atom +# atom := INT | IDENT | '(' expr ')' +# +# Each grammar rule returns a Polynomial; addition / multiplication / +# negation / exponentiation are implemented as Polynomial operations. +# This is the "expand + collect" step inlined into parsing. +# --------------------------------------------------------------------------- + +class _Parser: + def __init__(self, tokens: list[tuple[str, str]], variable: str) -> None: + self._tokens = tokens + self._pos = 0 + self._variable = variable + + def _peek(self) -> tuple[str, str] | None: + if self._pos >= len(self._tokens): + return None + return self._tokens[self._pos] + + def _consume(self) -> tuple[str, str]: + if self._pos >= len(self._tokens): + raise SymbolicError("unexpected end of expression") + tok = self._tokens[self._pos] + self._pos += 1 + return tok + + def parse(self) -> Polynomial: + result = self._expr() + if self._pos != len(self._tokens): + extra = self._tokens[self._pos] + raise SymbolicError(f"unexpected trailing token {extra!r}") + return result + + def _expr(self) -> Polynomial: + left = self._term() + while True: + tok = self._peek() + if tok is None or tok[0] != "op" or tok[1] not in ("+", "-"): + break + self._consume() + right = self._term() + if tok[1] == "+": + left = _add(left, right) + else: + left = _sub(left, right) + return left + + def _term(self) -> Polynomial: + left = self._factor() + while True: + tok = self._peek() + if tok is None: + break + # Explicit '*' + if tok[0] == "op" and tok[1] == "*": + self._consume() + right = self._factor() + left = _mul(left, right) + continue + break + return left + + def _factor(self) -> Polynomial: + base = self._unary() + tok = self._peek() + if tok is not None and tok[0] == "op" and tok[1] == "**": + self._consume() + exp_tok = self._unary() + # Exponent must be a non-negative integer constant polynomial. + if len(exp_tok.coefficients) > 1: + raise SymbolicError( + "exponent must be a non-negative integer constant; " + "got non-constant polynomial" + ) + exp_val = exp_tok.coefficients[0] if exp_tok.coefficients else 0 + if exp_val < 0: + raise SymbolicError( + f"exponent must be non-negative; got {exp_val}" + ) + return _pow(base, exp_val) + return base + + def _unary(self) -> Polynomial: + tok = self._peek() + if tok is not None and tok[0] == "op" and tok[1] in ("+", "-"): + self._consume() + inner = self._unary() + if tok[1] == "-": + return _neg(inner) + return inner + return self._atom() + + def _atom(self) -> Polynomial: + tok = self._consume() + if tok[0] == "int": + return _const(int(tok[1]), self._variable) + if tok[0] == "ident": + if tok[1] != self._variable: + raise SymbolicError( + f"v1 supports a single variable {self._variable!r}; " + f"got identifier {tok[1]!r}" + ) + return _x(self._variable) + if tok == ("op", "("): + inner = self._expr() + close = self._consume() + if close != ("op", ")"): + raise SymbolicError(f"expected ')'; got {close!r}") + return inner + raise SymbolicError(f"unexpected token {tok!r}") + + +# --------------------------------------------------------------------------- +# Polynomial algebra primitives (the actual "expand and collect" engine) +# --------------------------------------------------------------------------- + +def _strip_trailing_zeros(coeffs: list[int]) -> tuple[int, ...]: + while coeffs and coeffs[-1] == 0: + coeffs.pop() + return tuple(coeffs) + + +def _const(value: int, variable: str) -> Polynomial: + if value == 0: + return Polynomial(coefficients=(), variable=variable) + return Polynomial(coefficients=(value,), variable=variable) + + +def _x(variable: str) -> Polynomial: + return Polynomial(coefficients=(0, 1), variable=variable) + + +def _add(a: Polynomial, b: Polynomial) -> Polynomial: + if a.variable != b.variable: + raise SymbolicError( + f"variable mismatch: {a.variable!r} vs {b.variable!r}" + ) + n = max(len(a.coefficients), len(b.coefficients)) + out = [0] * n + for i, c in enumerate(a.coefficients): + out[i] += c + for i, c in enumerate(b.coefficients): + out[i] += c + return Polynomial( + coefficients=_strip_trailing_zeros(out), variable=a.variable + ) + + +def _neg(a: Polynomial) -> Polynomial: + return Polynomial( + coefficients=tuple(-c for c in a.coefficients), variable=a.variable + ) + + +def _sub(a: Polynomial, b: Polynomial) -> Polynomial: + return _add(a, _neg(b)) + + +def _mul(a: Polynomial, b: Polynomial) -> Polynomial: + if a.variable != b.variable: + raise SymbolicError( + f"variable mismatch: {a.variable!r} vs {b.variable!r}" + ) + if not a.coefficients or not b.coefficients: + return Polynomial(coefficients=(), variable=a.variable) + out = [0] * (len(a.coefficients) + len(b.coefficients) - 1) + for i, ca in enumerate(a.coefficients): + if ca == 0: + continue + for j, cb in enumerate(b.coefficients): + out[i + j] += ca * cb + return Polynomial( + coefficients=_strip_trailing_zeros(out), variable=a.variable + ) + + +def _pow(base: Polynomial, exponent: int) -> Polynomial: + if exponent == 0: + return _const(1, base.variable) + result = base + for _ in range(exponent - 1): + result = _mul(result, base) + return result + + +# --------------------------------------------------------------------------- +# Public API +# --------------------------------------------------------------------------- + +def normalize(expression: str, *, variable: str = "x") -> Polynomial: + """Parse + expand + collect ``expression`` into canonical Polynomial. + + Raises :class:`SymbolicError` on any input the v1 normalizer + cannot deterministically handle (multi-variable, division, + non-integer coefficient, unknown identifier, syntax error, + negative exponent, non-constant exponent). + """ + if not isinstance(expression, str) or not expression.strip(): + raise SymbolicError("empty or non-string expression") + tokens = _tokenize(expression) + if not tokens: + raise SymbolicError("no tokens parsed from expression") + return _Parser(tokens, variable).parse() + + +def canonical_string(expression: str, *, variable: str = "x") -> str: + """Shortcut: ``normalize(expression).to_canonical_string()``.""" + return normalize(expression, variable=variable).to_canonical_string() diff --git a/tests/test_adr_0131_1_symbolic_equivalence_lane.py b/tests/test_adr_0131_1_symbolic_equivalence_lane.py new file mode 100644 index 00000000..e2258220 --- /dev/null +++ b/tests/test_adr_0131_1_symbolic_equivalence_lane.py @@ -0,0 +1,99 @@ +"""ADR-0131.1 — lane ratification tests. + +The load-bearing assertion: the v1 benchmark lane passes its exit +criterion (correct_rate >= 0.95, wrong == 0) on the curated dataset +in evals/math_symbolic_equivalence/v1/cases.jsonl. + +If this test fails, either the normalizer regressed or the dataset +was edited to include a case the v1 scope cannot handle. Both +require explicit operator review. +""" + +from __future__ import annotations + +import json +from pathlib import Path + +from evals.math_symbolic_equivalence.v1.runner import ( + _load_cases, + build_report, +) + + +_CASES_PATH = ( + Path(__file__).resolve().parent.parent + / "evals" + / "math_symbolic_equivalence" + / "v1" + / "cases.jsonl" +) + + +class TestDatasetIntegrity: + def test_cases_file_exists(self) -> None: + assert _CASES_PATH.exists(), f"missing dataset: {_CASES_PATH}" + + def test_cases_are_well_formed(self) -> None: + cases = _load_cases() + assert len(cases) >= 30, "v1 must ship at least 30 cases" + for c in cases: + for k in ( + "case_id", "expression_a", "expression_b", + "expected", "category", "provenance", + ): + assert k in c, f"case {c.get('case_id')} missing field {k!r}" + assert c["expected"] in ("equivalent", "not_equivalent", "refused") + + def test_no_duplicate_case_ids(self) -> None: + cases = _load_cases() + ids = [c["case_id"] for c in cases] + assert len(ids) == len(set(ids)), "duplicate case_ids in dataset" + + def test_provenance_cites_adr(self) -> None: + cases = _load_cases() + for c in cases: + assert "adr-0131" in c["provenance"] + + +class TestLaneGate: + def test_lane_passes_exit_criterion(self) -> None: + cases = _load_cases() + report = build_report(cases) + assert report["exit_criterion"]["passed"], ( + f"lane gate failed: counts={report['counts']!r} " + f"correct_rate={report['correct_rate']!r}" + ) + + def test_wrong_count_is_zero(self) -> None: + # The wrong == 0 invariant is the load-bearing safety property. + cases = _load_cases() + report = build_report(cases) + assert report["counts"]["wrong"] == 0, ( + "wrong count must be zero on the v1 dataset; per-case " + f"detail: {[c for c in report['per_case'] if c['verdict_class']=='wrong']}" + ) + + def test_refused_cases_have_expected_refused(self) -> None: + # Every refusal in the result must correspond to a case whose + # expected verdict was 'refused' (out-of-scope by design). If + # we refuse on a case that expected a definite answer, that's + # a regression of the normalizer's coverage. + cases = _load_cases() + report = build_report(cases) + for entry in report["per_case"]: + if entry["verdict_class"] == "refused": + assert entry["expected"] == "refused", ( + f"engine refused on case {entry['case_id']} whose " + f"expected verdict was {entry['expected']!r}; " + f"reason: {entry['reason']}" + ) + + +class TestDeterminism: + def test_report_is_byte_equal_across_runs(self) -> None: + cases = _load_cases() + r1 = build_report(cases) + r2 = build_report(cases) + s1 = json.dumps(r1, sort_keys=True).encode("utf-8") + s2 = json.dumps(r2, sort_keys=True).encode("utf-8") + assert s1 == s2 diff --git a/tests/test_math_symbolic_equivalence.py b/tests/test_math_symbolic_equivalence.py new file mode 100644 index 00000000..2e9ed936 --- /dev/null +++ b/tests/test_math_symbolic_equivalence.py @@ -0,0 +1,96 @@ +"""ADR-0131.1 — tests for the symbolic equivalence check primitive.""" + +from __future__ import annotations + +from generate.math_symbolic_equivalence import ( + Verdict, + check_equivalence, +) + + +class TestEquivalent: + def test_identical_expressions(self) -> None: + v = check_equivalence("x + 1", "x + 1") + assert v.verdict == Verdict.EQUIVALENT + assert v.canonical_a == v.canonical_b == "x+1" + + def test_distributive(self) -> None: + v = check_equivalence("2*(x + 3)", "2*x + 6") + assert v.verdict == Verdict.EQUIVALENT + + def test_square_of_binomial(self) -> None: + v = check_equivalence("(x + 1)^2", "x^2 + 2*x + 1") + assert v.verdict == Verdict.EQUIVALENT + + def test_difference_of_squares(self) -> None: + v = check_equivalence("(x + 1)*(x - 1)", "x^2 - 1") + assert v.verdict == Verdict.EQUIVALENT + + def test_collect_like_terms(self) -> None: + v = check_equivalence("2*x + 3*x + x", "6*x") + assert v.verdict == Verdict.EQUIVALENT + + def test_zero_cancellation(self) -> None: + v = check_equivalence("x - x + 5", "5") + assert v.verdict == Verdict.EQUIVALENT + + +class TestNotEquivalent: + def test_different_constant(self) -> None: + v = check_equivalence("x + 1", "x + 2") + assert v.verdict == Verdict.NOT_EQUIVALENT + assert v.canonical_a == "x+1" + assert v.canonical_b == "x+2" + + def test_different_degree(self) -> None: + v = check_equivalence("x^2", "x^3") + assert v.verdict == Verdict.NOT_EQUIVALENT + + def test_sign_flipped(self) -> None: + v = check_equivalence("(x + 1)^2", "(x - 1)^2") + assert v.verdict == Verdict.NOT_EQUIVALENT + + +class TestRefused: + def test_empty_left(self) -> None: + v = check_equivalence("", "x + 1") + assert v.verdict == Verdict.REFUSED + assert "normalize(a) refused" in v.reason + + def test_out_of_scope_variable_left(self) -> None: + v = check_equivalence("x + y", "x + 1") + assert v.verdict == Verdict.REFUSED + assert "single variable" in v.reason + + def test_division_refused(self) -> None: + v = check_equivalence("x/2", "x") + assert v.verdict == Verdict.REFUSED + + def test_a_normalizes_b_refuses(self) -> None: + # a is fine, b uses y -> refusal with canonical_a populated + v = check_equivalence("x + 1", "y + 1") + assert v.verdict == Verdict.REFUSED + assert v.canonical_a == "x+1" + assert v.canonical_b is None + assert "normalize(b) refused" in v.reason + + def test_refused_verdict_is_first_class(self) -> None: + # Refusal preserves wrong == 0 — the verdict is REFUSED, never + # silently coerced to NOT_EQUIVALENT. + v = check_equivalence("garbage(", "x") + assert v.verdict == Verdict.REFUSED + + +class TestDeterminism: + def test_same_inputs_same_verdict(self) -> None: + # Re-running produces byte-equal verdict. + a, b = "(x + 2)*(x - 2)", "x^2 - 4" + v1 = check_equivalence(a, b) + v2 = check_equivalence(a, b) + assert v1 == v2 + + def test_canonical_strings_are_byte_equal_on_equivalence(self) -> None: + v = check_equivalence("(x + 1)^2", "x^2 + 2*x + 1") + assert v.canonical_a is not None + assert v.canonical_b is not None + assert v.canonical_a.encode("utf-8") == v.canonical_b.encode("utf-8") diff --git a/tests/test_math_symbolic_normalizer.py b/tests/test_math_symbolic_normalizer.py new file mode 100644 index 00000000..17c86c88 --- /dev/null +++ b/tests/test_math_symbolic_normalizer.py @@ -0,0 +1,217 @@ +"""ADR-0131.1 — tests for the univariate polynomial normalizer. + +Exercises every grammar rule, every algebraic identity the v1 scope +needs to cover, and every refusal criterion. The load-bearing +assertion: same algebraic content -> same canonical string, +byte-for-byte. +""" + +from __future__ import annotations + +import pytest + +from generate.math_symbolic_normalizer import ( + Polynomial, + SymbolicError, + canonical_string, + normalize, +) + + +# --------------------------------------------------------------------------- +# Trivial parses +# --------------------------------------------------------------------------- + +class TestTrivialParse: + def test_constant_zero(self) -> None: + assert normalize("0").coefficients == () + + def test_constant_positive(self) -> None: + assert normalize("7").coefficients == (7,) + + def test_constant_negative_unary(self) -> None: + assert normalize("-3").coefficients == (-3,) + + def test_bare_variable(self) -> None: + assert normalize("x").coefficients == (0, 1) + + def test_simple_sum(self) -> None: + assert normalize("x + 1").coefficients == (1, 1) + + def test_implicit_coefficient_is_one(self) -> None: + # "x^2 + x" -> coefficients (0, 1, 1) + assert normalize("x^2 + x").coefficients == (0, 1, 1) + + +# --------------------------------------------------------------------------- +# Algebraic identities (the heart of the equivalence test) +# --------------------------------------------------------------------------- + +class TestAlgebraicIdentities: + def test_distributive_basic(self) -> None: + # 2*(x + 3) == 2x + 6 + assert canonical_string("2*(x + 3)") == canonical_string("2*x + 6") + + def test_distributive_with_variable(self) -> None: + # x*(x + 1) == x^2 + x + assert canonical_string("x*(x + 1)") == canonical_string("x^2 + x") + + def test_commutative_addition(self) -> None: + assert canonical_string("3 + x") == canonical_string("x + 3") + + def test_commutative_multiplication(self) -> None: + assert canonical_string("3*x") == canonical_string("x*3") + + def test_associative_addition(self) -> None: + assert canonical_string("(x + 1) + 2") == canonical_string("x + (1 + 2)") + + def test_square_of_binomial(self) -> None: + # (x + 1)^2 == x^2 + 2x + 1 + assert canonical_string("(x + 1)^2") == canonical_string("x^2 + 2*x + 1") + + def test_square_of_binomial_negative(self) -> None: + # (x - 1)^2 == x^2 - 2x + 1 + assert canonical_string("(x - 1)^2") == canonical_string("x^2 - 2*x + 1") + + def test_difference_of_squares(self) -> None: + # (x + 1)(x - 1) == x^2 - 1 + assert canonical_string("(x + 1)*(x - 1)") == canonical_string("x^2 - 1") + + def test_cube_of_binomial(self) -> None: + # (x + 1)^3 == x^3 + 3x^2 + 3x + 1 + assert canonical_string("(x + 1)^3") == canonical_string( + "x^3 + 3*x^2 + 3*x + 1" + ) + + def test_foil(self) -> None: + # (x + 2)(x + 3) == x^2 + 5x + 6 + assert canonical_string("(x + 2)*(x + 3)") == canonical_string( + "x^2 + 5*x + 6" + ) + + def test_collect_like_terms(self) -> None: + # 2x + 3x == 5x + assert canonical_string("2*x + 3*x") == canonical_string("5*x") + + def test_zero_cancellation(self) -> None: + # x - x == 0 + assert canonical_string("x - x") == "0" + + def test_subtraction_distributes(self) -> None: + # 2 - (x - 1) == 3 - x + assert canonical_string("2 - (x - 1)") == canonical_string("3 - x") + + def test_x_zero_is_one(self) -> None: + # x^0 == 1 + assert canonical_string("x^0") == canonical_string("1") + + def test_pow_caret_and_double_star_equivalent(self) -> None: + # both spellings accepted; output identical + assert canonical_string("x^2") == canonical_string("x**2") + + +# --------------------------------------------------------------------------- +# Non-equivalence: distinct polynomials canonicalize differently +# --------------------------------------------------------------------------- + +class TestNonEquivalence: + def test_different_constant(self) -> None: + assert canonical_string("x + 1") != canonical_string("x + 2") + + def test_different_coefficient(self) -> None: + assert canonical_string("2*x") != canonical_string("3*x") + + def test_different_degree(self) -> None: + assert canonical_string("x^2") != canonical_string("x^3") + + def test_sign_flipped(self) -> None: + assert canonical_string("x + 1") != canonical_string("x - 1") + + +# --------------------------------------------------------------------------- +# Canonical-string format +# --------------------------------------------------------------------------- + +class TestCanonicalStringFormat: + def test_zero(self) -> None: + assert canonical_string("0") == "0" + + def test_constant(self) -> None: + assert canonical_string("7") == "7" + + def test_x(self) -> None: + assert canonical_string("x") == "x" + + def test_negative_constant(self) -> None: + assert canonical_string("-3") == "-3" + + def test_x_plus_one(self) -> None: + assert canonical_string("x + 1") == "x+1" + + def test_descending_order(self) -> None: + assert canonical_string("1 + x + x^2") == "x^2+x+1" + + def test_coefficient_one_elided(self) -> None: + assert canonical_string("1*x") == "x" + + def test_negative_leading_coefficient(self) -> None: + assert canonical_string("-x + 1") == "-x+1" + + +# --------------------------------------------------------------------------- +# Refusals (preserve wrong == 0 for the benchmark) +# --------------------------------------------------------------------------- + +class TestRefusals: + def test_empty_input(self) -> None: + with pytest.raises(SymbolicError, match="empty"): + normalize("") + + def test_undefined_variable(self) -> None: + with pytest.raises(SymbolicError, match="single variable"): + normalize("x + y") # y is out of scope + + def test_negative_exponent(self) -> None: + with pytest.raises(SymbolicError, match="non-negative"): + normalize("x^-1") + + def test_non_constant_exponent(self) -> None: + with pytest.raises(SymbolicError, match="constant"): + normalize("x^x") + + def test_syntax_unbalanced_paren(self) -> None: + with pytest.raises(SymbolicError): + normalize("(x + 1") + + def test_syntax_trailing_op(self) -> None: + with pytest.raises(SymbolicError): + normalize("x +") + + def test_unknown_operator_division(self) -> None: + with pytest.raises(SymbolicError): + normalize("x / 2") + + +# --------------------------------------------------------------------------- +# Polynomial dataclass invariants +# --------------------------------------------------------------------------- + +class TestPolynomialInvariants: + def test_trailing_zero_rejected(self) -> None: + with pytest.raises(SymbolicError, match="trailing zeros"): + Polynomial(coefficients=(1, 2, 0), variable="x") + + def test_float_rejected(self) -> None: + with pytest.raises(SymbolicError, match="int"): + Polynomial(coefficients=(1.5,), variable="x") # type: ignore[arg-type] + + def test_zero_polynomial_is_empty_tuple(self) -> None: + # Zero polynomial canonical form has empty coefficients tuple. + assert Polynomial(coefficients=(), variable="x").to_canonical_string() == "0" + + def test_equality(self) -> None: + a = Polynomial(coefficients=(1, 2, 3), variable="x") + b = Polynomial(coefficients=(1, 2, 3), variable="x") + assert a == b + c = Polynomial(coefficients=(1, 2, 4), variable="x") + assert a != c