169cec710e
* feat(evals): add deterministic symbolic equivalence generated corpus
* feat(evals): add symbolic equivalence replay helpers
* feat(evals): load generated symbolic equivalence corpus
* feat(evals): emit symbolic equivalence replay manifest
* feat(symbolic): support multivariable integer polynomials
* feat(symbolic): support exact rational polynomial coefficients
* feat(symbolic): align equivalence API with multivariable normalization
* test(ADR-0131.1.B): reconcile v1 expectations to v1.B scope expansion
The v1.B refactor (univariate int → sparse multivariable Fraction) deliberately
admits multivariable polynomials and constant-denominator division. The v1
dataset and tests pinned the old refusal behavior, so the lane runner reported
wrong=4 and 10 unit tests failed.
Reconcile:
- cases.jsonl: flip sym-eq-v1-0029 ('x+y' vs 'x+1') and sym-eq-v1-0030
('x/2' vs 'x') from expected=refused to expected=not_equivalent; rename
categories to multivariable_distinct / constant_denominator_distinct;
extend provenance with adr-0131.1b:scope-expanded.
- generated_cases.py: split _refusal_cases into scope_expanded (admits)
and templates (still refused); the first two adversarial cases move to
the scope-expanded list with expected=not_equivalent.
- test_math_symbolic_normalizer.py: replace test_undefined_variable and
test_unknown_operator_division with positive scope-expansion tests +
symbolic-denominator refusal; rewrite TestPolynomialInvariants for the
new terms/variables constructor (Polynomial(terms={...}, variables=(...)))
with float-rejection and zero-coef-collapse invariants.
- test_math_symbolic_equivalence.py: TestRefused.test_empty_left reason
string matches new normalizer error; flip multivariable + constant-
denominator cases to NOT_EQUIVALENT; add symbolic-denominator-refused
case; relax canonical_a assertion in test_a_normalizes_b_refuses (engine
now zeroes both on either-side refusal).
- report.json + manifest.json: regenerated; lane PASS 185/185 wrong=0.
Lane invariants reaffirmed by the new tests: wrong==0, refusal-first for
truly out-of-scope inputs (symbolic denominator, transcendental, malformed,
negative exponent), determinism via byte-equal report.
100 lines
3.6 KiB
Python
100 lines
3.6 KiB
Python
"""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 "empty" in v.reason
|
|
|
|
def test_multivariable_now_admits(self) -> None:
|
|
# ADR-0131.1.B scope expansion: multivariable polynomials are admissible.
|
|
v = check_equivalence("x + y", "x + 1")
|
|
assert v.verdict == Verdict.NOT_EQUIVALENT
|
|
|
|
def test_constant_denominator_now_admits(self) -> None:
|
|
# ADR-0131.1.B scope expansion: constant-denominator division admits.
|
|
v = check_equivalence("x/2", "x")
|
|
assert v.verdict == Verdict.NOT_EQUIVALENT
|
|
|
|
def test_symbolic_denominator_still_refused(self) -> None:
|
|
# Symbolic-denominator division stays out of scope.
|
|
v = check_equivalence("x/y", "x")
|
|
assert v.verdict == Verdict.REFUSED
|
|
|
|
def test_a_normalizes_b_refuses(self) -> None:
|
|
# a is fine, b uses a transcendental -> refusal.
|
|
v = check_equivalence("x + 1", "sin(x)")
|
|
assert v.verdict == Verdict.REFUSED
|
|
assert v.canonical_b is None
|
|
|
|
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")
|