diff --git a/agent-reports/2026-09-21-sathandlers-validation-triage.md b/agent-reports/2026-09-21-sathandlers-validation-triage.md index d17d5e4..f09f136 100644 --- a/agent-reports/2026-09-21-sathandlers-validation-triage.md +++ b/agent-reports/2026-09-21-sathandlers-validation-triage.md @@ -1,95 +1,116 @@ # Agent report: would expanding sathandlers pass more validation tests? -- **Date:** 2026-09-21 (updated after the structural/function fact work landed on a branch) -- **Status:** investigation complete; number facts landed on `main`; a large part of the - handler work now lives on branch **`agent/add-mul-pow-and-function-facts`** (pushed to - the `bot` remote, `github.com/tilorc-bot/reasoning`), not yet on `main` +- **Date:** 2026-09-22 (final update - audit and tail work merged to `main`) +- **Status:** investigation complete; all four planned units landed on `main` (merge + `4ceae4b` of branch `agent/tail-audits`, tip `9320542`, pushed to the `bot` remote). + Earlier stages: number facts landed directly on `main`; the 2a/2b structural and + function work landed as branch `agent/add-mul-pow-and-function-facts` (`cde5c70`), + later folded into `agent/tail-audits`. - **Scope:** `validation/test_query.py` + `validation/test_matrices.py` against pinned SymPy `ddbb536d` (1.15.0.dev) - **Read this if:** you are editing `reasoning/sathandlers.py`, `reasoning/functionfacts.py`, - `reasoning/numberfacts.py`, the known-facts import in `reasoning/sympy_adapter.py`, or - trying to raise the validation pass rate. If you want to resume the handler work, start - from the branch above. -- **Stale after:** any change to those fact modules, the comparison policy in + `reasoning/matrixfacts.py`, `reasoning/symbolfacts.py`, `reasoning/numberfacts.py`, the + known-facts layer in `reasoning/knownfacts.py` / `reasoning/sympy_adapter.py`, or trying + to raise the validation pass rate beyond **79/104**. +- **Stale after:** any change to those modules, the comparison policy in `validation/compare_backends.py`, the SymPy pin, or the validation results -- **TL;DR:** `main` is at reasoning **40/104**, SymPy `satask` 24/104, full SymPy `ask` - 94/104. Branch `agent/add-mul-pow-and-function-facts` reaches **52/104** (18 matrix, - 12 handler tails, 2 old-assumption-flavored, 1 Symbol bridge and 9 non-handler - failures left). "Expand sathandlers" is 3-4 commits; two of them (Add/Mul/Pow - structural facts, elementary - functions) are largely done on that branch, matrix facts are untouched. +- **TL;DR:** `main` now reaches **79/104** on the two validation suites (40/104 when this + investigation started; 52/104 when the 2a/2b branch was first measured). SymPy full + `ask` is 94/104, SymPy `satask` 24/104. The remaining 15 failures are capped: 4 are + proven terminal or impossible in a global SAT fact base, 2 need upstream's + handler-local zero-blindness, and 9 are non-handler/API features. -## Where the work landed +## Final results -Branch **`agent/add-mul-pow-and-function-facts`** on the `bot` remote (PR link: -`github.com/tilorc-bot/reasoning/pull/new/agent/add-mul-pow-and-function-facts`). +| Gate | Result | +|---|---| +| `validation/test_query.py` + `test_matrices.py` | **79 passed / 15 failed / 2 xfailed / 8 xpassed** | +| `test_matrices.py` alone | 19 passed / 0 failed / 2 xfailed / 3 xpassed | +| `pytest reasoning/tests` on `main` | 180 passed / 1 xfailed | +| `mypy` (strict) | clean, 46 source files | +| `tools/check_old_assumptions.py reasoning` | 0 findings from this work; 2 pre-existing findings in `reasoning/lra_adapter.py` (LRA work already on `main`) | -- `3840c36` + `82e4186`: Add/Mul/Pow structural facts and their tests (from worktree - `/tmp/opencode/reasoning-2a`, branch `agent/2a-add-mul-pow`; the agent was cancelled - after the code was complete but before it reported, so quality gates were run and - the work committed manually). -- `fc0e6c6` + `3b34d49`: elementary-function facts and tests (worktree - `/tmp/opencode/reasoning-2b`, branch `agent/2b-elementary-functions`). -- `cde5c70`: merge of the two, created in worktree `/tmp/opencode/reasoning-combined` - (currently checked out there). +## What landed -Gates on the merged branch: `pytest reasoning/tests` **95 passed, 1 xfailed**; -`mypy` strict clean; `tools/check_old_assumptions.py reasoning` 0 findings; both -validation suites **52 passed / 42 failed / 4 xfailed / 6 xpassed** (main: 40/54/8/2). +- **Number facts** (`198df09`) and the old-assumption checker (`bbe3031`) on `main`. +- **2a Add/Mul/Pow structural facts** (`3840c36`, `82e4186`) and **2b elementary + functions** (`fc0e6c6`, `3b34d49`), merged as `cde5c70`; net +12 tests over `main`. +- **Four over-inference audits** appended to that branch: + - `8a1dba6` (T1): scope `imaginary -> ~hermitian` away from `Add` subjects. + - `26df87a` (T2): guard the Pow imaginary-exponent realness rule with + `NOT(Q.positive(base))`, plus a rational-base rule keeping `positive(2**I)` False. + - `98b1d61` (T4): stop emitting `real(sin/cos(arg))` for `Number` args. This is a + **workaround**: the root cause is the cancellation-unsound `_add_imaginary_facts` + closed-group rule (`allargs(imaginary) -> imaginary(Add)`); revert T4 if that rule + ever gets a cancellation guard. + - `15a4338` (T3-A): `NOT(Q.zero(expr))` guards on the parity-negative inferences in + `_mul_hermitian_facts`; narrower alternative `a629d94` (T3-B) left unmerged. +- **Gap P** (`fe333b3`): Pow/Mul tails - `test_real_pow`, `test_nonzero`. +- **Gap F** (`b011b70`, `a4603ab`): Add finite closure, same-sign unboundedness, function + value-at-zero facts, `complex(exp(x))`, `real(exp(x)**x)`. +- **Bounded audit** (`3eb3232`, test-only): proves `test_bounded:1108` is *forced* by + earlier assertions 1076/1081/1094; upstream's `None` comes from a handler-local bail + that a monotone fact base cannot express. +- **Matrix core** (`5c1356c`): new `reasoning/matrixfacts.py` (~450 lines) covering + MatrixSymbol, Identity/Zero/One, explicit matrices (numeric `det()`), MatAdd, MatMul, + MatPow, Transpose, Inverse, MatrixSlice, BlockMatrix, BlockDiagMatrix, + Determinant/Trace, HadamardProduct, Factorization, DFT, MatrixElement. Matrix suite + went 2P/17F -> 18P/1F. +- **Symbol bridge** (`8773c97`): new `reasoning/symbolfacts.py` harvests *declared* symbol + assumptions through the public new-assumptions API (`sympy.assumptions.ask.ask`), with a + per-symbol cache; `sympy_adapter.add_known_facts` asserts them as local premises unless + the query mentions the same predicate explicitly. This keeps + `tools/check_old_assumptions.py` at 0 findings (no `.is_*`/`.assumptions0` reads in + reasoning code); compound expressions are still never probed with old assumptions. +- **Matrix dense** (`b3337be`): explicit dense/Sparse hermitian/antihermitian via + pairwise `entry - conjugate(mirror)` checks (refutation gated to symbol-free + differences so the complex `z` cases stay `None`), plus MatPow + `integer(e) & negative(e) & invertible(X) & real_elements(X) -> real_elements(X**e)`. + Combined with the bridge this also flipped matrix-suite `test_field_assumptions`. -Merge notes for future agents: +Merges: `ebe3162` (audits), `e533b38` (gap F), `e533b38`..`67fb3ed` (matrix core), +`9320542` (matrix dense), then `main` at `4ceae4b`. The only merge conflict was the +`knownfacts` import in `sympy_adapter.py` after PR #3's sympy-free known-facts refactor. -- The merge conflict was only an import collision in `sathandlers.py`. -- A real interaction bug was fixed in the merge commit: the generic Pow rule - `imaginary(exp) -> (real(expr) <=> imaginary(log(base)))` (copied from SymPy's - `handlers/sets.py`) is wrong for base `E`, where the function facts handle realness - exactly. Both fact sets derived `positive` and `~real` for `E**(I*pi*x)` with `even(x)`, - which raised `ValueError: Inconsistent assumptions`. The rule is now restricted to - non-`E` bases. -- `functionfacts.py` deliberately returns `~algebraic` rather than `transcendental` - consequents (avoids a spurious UNSAT chain) and leaves `finite(log(x))` with - `~zero(x)` as `None` instead of upstream's `True`. +## Remaining 15 failures by group -## Remaining 42 failures on the branch by group - -| Group | Count | Notes | +| Group | Count | Tests and why they are capped | |---|---|---| -| Matrix expressions | 18 | 17 `test_matrices.py` tests plus `test_matrix`; untouched, largest remaining block | -| Handler tails | 12 | `test_I`, `complex`, `negative`, `rational`, `hermitian`, `imaginary`, `nonzero`, `real_pow` (structural tails) and `bounded`, `positive`, `real_functions`, `algebraic` (structural + function tails) | -| Old-assumption-flavored | 2 | `test_integer` (`integer(sqrt(2)*x)` -> False), `test_prime` (`prime(4*x)` -> False); upstream likely answers via old assumptions | -| Symbol old-assumption bridge | 1 | `test_check_old_assumption`; `tools/check_old_assumptions.py` flags exactly this | -| Non-handler / API | 9 | `context=` kwarg, `global_assumptions`, custom predicate/handler registration (4), relational predicates (2), `test_Add_queries` numeric evaluation | - -Watch out: `test_hermitian` now over-answers at a later assertion (first failure moved -from `None is False` to `False is None`), so the structural tail needs an audit, not -just more facts. +| Terminal tails | 4 | `test_I` (upstream `ask` itself returns None; needs old-assumption `is_integer`), `test_bounded` (line 1108 forced by 1076/1081/1094), `test_hermitian` + `test_imaginary` (global-SAT `Exclusive(real, imaginary)` versus `test_real_pow:2057`; upstream answers each test inconsistently via handler short-circuiting) | +| Old-assumption-flavored | 2 | `test_integer` (`integer(sqrt(2)*x)` -> False) and `test_prime` (`prime(4*x)` -> False); upstream's handlers ignore the `x = 0` case | +| Non-handler/API | 9 | `test_global` (`global_assumptions`), `test_custom_context` (`context=` kwarg), `test_key_extensibility`, `test_type_extensibility`, `test_custom_AskHandler`, `test_polyadic_predicate` (custom predicate/handler registration), `test_relational` (relational predicates), `test_Add_queries` (numeric evaluation), `test_issue_28127` | ## Findings that still hold - The adapter imports SymPy's complete known predicate facts, so predicate-to-predicate - relations are mostly not the gap. The encoding polarity in `_known_template` is - correct; an apparent inversion was a false alarm about `Literal.is_Not` semantics. -- Not a propagation bug: the earlier `Q.hermitian(I)` mystery was missing facts (known - facts carry `zero -> hermitian | antihermitian`, not the converse), now supplied by - `numberfacts`. -- Handler work also requires curating the known-fact layer for clauses class facts - cannot express (e.g. `hermitian & imaginary -> ~hermitian`; the branch adds such an - extra-predicate-facts table in `sympy_adapter.py`). -- Full `ask` passes every test still failing here, so the suite itself is not the - ceiling; the gap is the handler/old-assumption machinery `ask` has and `satask` does - not. + relations are mostly not the gap. The encoding polarity in the known-facts template is + correct. +- Handler work also requires curating the known-fact layer for clauses class facts cannot + express; the branch adds the `_extra_predicate_facts` table in `sympy_adapter.py`. +- The fundamental ceiling is architectural: upstream `ask` is handler-local and + short-circuits on the expression class, so it can return mutually inconsistent answers + across tests (documented for `imaginary`/`hermitian`, `finite(exp(x))` versus + `complex(exp(x))`, and the Mul finite bail). A monotone global SAT fact base cannot + reproduce those inconsistencies; each was a deliberate trade-off choice, documented in + `/tmp/opencode/agent-notes/cross-findings.md`. +- Full `ask` passes every test still failing here, so the suite itself is not the ceiling; + the gap is the handler/old-assumption machinery `ask` has and `satask` does not. -## Next steps (the old "step 2" was too broad) +## Next steps (remaining ~15 tests, all non-structural) | Unit | Status | Remaining work | Test payoff | |---|---|---|---| -| 2a. Add/Mul/Pow facts | mostly on branch; 10 of 18 targets flipped (plus 3 xfails now xpass) | structural tails above, `hermitian` over-inference audit, `integer`/`prime` may stay unreachable | ~8-10 | -| 2b. Elementary functions | on branch (`sin/cos/tan/cot/asin/acos/atan/acot/exp/log/Abs/re/im/factorial`); `test_issue_5833` and `test_issue_7246` fully pass | assertions still blocked on the 2a tails | ~3-5 additional | -| 2c. Matrix expressions | not started | ~20 matrix classes x ~15 predicates (invertible, fullrank, symmetric, orthogonal, unitary, positive_definite, triangular, diagonal, element sets, ...) | ~15-17 | -| 2d. Symbol old-assumption bridge | not started | read `Symbol('x', real=True)` etc.; flagged by the checker | 1 | +| 3a. Context/global assumptions | not started | accept and honor the `context=` kwarg; merge `sympy.assumptions.assume.global_assumptions` into the premise set (the symbol bridge is the template) | 2 | +| 3b. Extensibility | not started | custom predicate registration (`key_extensibility`, `type_extensibility`, `custom_AskHandler`, `polyadic_predicate`) via the local registry | 4 | +| 3c. Relational and numeric | not started | `test_relational` and `test_Add_queries` need relational-predicate facts and numeric evaluation paths in `satask` | 2 | +| 3d. Old-assumption-flavored | deliverable unlikely | matching upstream requires porting its zero-blind Mul handlers | 2 | +| - | terminal | the four capped tails above | 4 | + +Projected total if 3a-3c land: **~89/104**; 3d would push to ~91/104 at the cost of +soundness that earlier audits deliberately restored. -Calibration: `numberfacts` was ~320 fact lines plus ~270 test lines and netted 14 -tests; the 2a+2b branch added roughly 900 lines and netted 12 more on top of `main`. -Tests are all-or-nothing, so a single missing rule keeps a whole test red; the payoffs -are per-unit ceilings, not additive guarantees. Projected total if 2a's tail, 2c and -2d land: **~73-79/104**. +Calibration: `numberfacts` was ~320 fact lines plus ~270 test lines and netted 14 tests; +the full 2a-2d arc added 2113 lines across 11 files (facts, matrix support, the symbol +bridge and tests) and netted 27 tests over the 2a/2b branch's own 12. Tests are +all-or-nothing, so a single missing rule keeps a whole test red; the payoffs above are +per-unit ceilings. diff --git a/agent-reports/2026-09-22-sathandlers-adversarial-fuzz.md b/agent-reports/2026-09-22-sathandlers-adversarial-fuzz.md new file mode 100644 index 0000000..40cf24e --- /dev/null +++ b/agent-reports/2026-09-22-sathandlers-adversarial-fuzz.md @@ -0,0 +1,337 @@ +# Agent report: adversarial soundness hunt for the sathandlers facts + +- **Date:** 2026-09-22 +- **Status:** tests + report on branch `test/sathandlers-adversarial` (merge of + `main` + `feature/sathandlers`); no product code touched +- **Scope:** `reasoning/tests/test_soundness_adversarial.py` and this report +- **Read this if:** you are fixing the known `~Q.complex(1/x)` Pow bug and want + to know which other facts are still unsound after the two proposed Pow guards +- **Stale after:** changes to `reasoning/sathandlers.py`, + `reasoning/functionfacts.py`, `reasoning/matrixfacts.py`, the known-fact + template, or `tools/check_soundness.py`'s model pools +- **TL;DR:** 20 adversarial tests pin soundness bugs that are *not* the known + `1/x` case. On the unfixed tip all 20 fail. With the two proposed Pow guards + applied locally, 19 still fail; the guards only fix the zero-base + algebraic/complex closure test. The fuzzer itself found two of the findings + with the guards applied (`--engine random --cases 500 --seed 1` and + `--no-matrices --cases 1000 --engine random --seed 7`); the rest are outside + the fuzzer's grammar or model pools. + +## Method + +Worktree `/tmp/opencode/test-adversarial`, `PYTHONPATH` pointed at it so the +fuzzer imports its handlers. Three passes: + +1. **Fuzzer baseline** (`tools/check_soundness.py` on the unfixed tip): curated + cases, Hypothesis engine, random engine seeds 1-7, `--strict`, and the + no-matrix 1000-case run. +2. **Targeted probing** of the families named in the task: Pow singularities, + Mul with zero/infinity, Add imaginary/sign cancellation, Abs/sign, + functionfacts at `0` and at infinities, matrix expression facts, and + declared symbol assumptions. Each candidate was checked with a concrete + model (substitution plus `ask` on ground atoms, or direct evaluation for + matrices) and with `sympy.ask` on the original query. +3. **Shallow-fix experiment.** The two guards from the other agents' + hypothesis were applied locally (uncommitted): `_pow_closure_facts` gets + `AND(_allargs(Q.complex, expr), defined)` on the complex closure, and + `_pow_algebraic_facts` gets `OR(NOT(Q.zero(base)), NOT(Q.negative(exp)))` on + the algebraic closure. The fuzzer and the probes were re-run; the local + edit was reverted before committing. + +## Fuzzer results + +| Run | Findings | Upstream-shared | +|---|---|---| +| tip, curated + 60 Hypothesis | 1 (`zero(x) \| ~complex(1/x)`) | 2 | +| tip, `--engine random --cases 500 --seed 1` | 2 (`zero(x) \| ~complex(1/x)`, antihermitian composite) | 2 | +| tip, `--strict`, curated + 60 Hypothesis | 3 (incl. `imaginary(x + y)` closed group) | 0 | +| tip, `--no-matrices --cases 1000 --engine random --seed 7` | 2 (`zero(x) \| ~complex(1/x)`, spurious inconsistency) | 2 | +| guards, curated + 60 Hypothesis | 0 | 1 | +| guards, seeds 1-5, 500 random each | seed 1: antihermitian composite; seeds 2-5: 0 | 1 per run | +| guards, `--no-matrices --cases 1000 --engine random --seed 7` | 1 (spurious inconsistency) | 1 | + +An additional audit with `use_lra_theory=True` (150 random cases, seed 3) found +nothing. + +The fuzzer's model pools explain most of the blind spots: `SCALAR_VALUES` has +no `oo`/`zoo`/`nan`, `hypothesis_cases` never uses declared symbols, matrix +atoms are always plain `MatrixSymbol`s (never `A**-2`, `A*B`, slices), and the +scalar grammar has no `acos`, `factorial`, or `evaluate=False` nodes. + +## Findings and minimal reproductions + +All line references are to the tip. "Sound" is the answer a complete sound +solver would give; "actual" is the tip's answer. Every finding below survives +the two known Pow guards (verified in step 3), except where noted. + +### 1. Imaginary-sum cancellation makes real predicates `False` + +`_extra_predicate_facts` (sympy_adapter.py:137) adds +`imaginary(subject) -> ~extended_real(subject)` for every non-`Add` subject, +but `_add_imaginary_facts` derives `imaginary(x + y)` from +`imaginary(x) & imaginary(y)` even when the sum cancels. The consequence +chain reaches every real predicate. + +```python +x, y = symbols("x y") +satask(Q.real(x + y), Q.imaginary(x) & Q.imaginary(y)) # False, sound None +satask(Q.extended_real(x + y), Q.imaginary(x) & Q.imaginary(y)) # False, sound None +satask(Q.integer(x + y), ...) # False, sound None +satask(Q.rational(x + y), ...) # False, sound None +satask(Q.zero(x + y), ...) # False, sound None +satask(Q.even(x + y), ...) # False, sound None +satask(Q.nonnegative(x + y), ...) # False, sound None +satask(Q.nonpositive(x + y), ...) # False, sound None +``` + +Model `x = I, y = -I`: `x + y = 0`, so all eight propositions are true. +`sympy.ask` returns `None` for all eight (it only shares the +`imaginary(x + y)` conclusion itself). The fuzzer can generate this class +(both `I` and `-I` are in the pool) but did not in seeds 1-7. + +### 2. `positive(acos(x))` under `zero(x - 1)` + +`_acos_facts` (functionfacts.py:100) derives `positive(acos(x))` from +`nonnegative(x + 1) & nonpositive(x - 1)`, but `acos(1) = 0`. + +```python +satask(Q.positive(acos(x)), Q.zero(x - 1)) # True, sound False (or None) +``` + +`x = 1` satisfies the assumption and `acos(1) == 0`; `ask` returns `None`. + +### 3. `integer(factorial(n))` for negative integers + +`_factorial_facts` (functionfacts.py:212) has no nonnegativity guard, but +`factorial(-1) = zoo`. + +```python +n = symbols("n", integer=True) +satask(Q.integer(factorial(n)), Q.integer(n)) # True, sound None +``` + +`n = -1` gives `zoo`; `n = 2` gives `2`. `ask` returns `None`. + +### 4. Function values at infinities claim to be finite + +`_exp_facts` and `_sin_cos_facts` assert `Q.complex(expr)` unconditionally, and +`complex -> finite`; `_re_facts`/`_im_facts` do the same. + +```python +satask(Q.finite(exp(x)), Q.infinite(x)) # True, sound None (x = -oo -> 0) +satask(Q.finite(E**x), Q.infinite(x)) # True, sound None +satask(Q.finite(re(x)), Q.infinite(x)) # True, sound False (re(oo) == oo) +satask(Q.finite(im(x)), Q.infinite(x)) # True, sound None (im(oo) == 0, im(zoo) == nan) +``` + +For `exp` and `E**x`, `sympy.ask` returns `False`, so these are +oracle-disagreements as well as model counterexamples. + +### 5. Infinite base with a negative integer exponent is not zero/rational + +`_pow_facts` (`zero(expr) <-> zero(base) & positive(exp)`) and +`_pow_rational_facts` rule 6 (`~algebraic(base) & integer(exp)` gives +`rational(expr) <-> zero(exp)`) both miss `oo**-1 = 0`. + +```python +xi = symbols("xi", infinite=True) +yi = symbols("yi", integer=True, negative=True) +satask(Q.zero(xi**yi)) # False, sound True (ask True -> oracle disagreement) +satask(Q.rational(xi**yi)) # False, sound True (ask None) +``` + +`xi = oo, yi = -1` gives `0`. + +### 6. Spurious inconsistencies on satisfiable assumptions + +All of these raise `ValueError: Inconsistent assumptions` although a model +exists, because an unconditional function fact contradicts the assumption. + +```python +satask(Q.positive(x), ~Q.finite(exp(x))) # raises; x = oo works +satask(Q.positive(x), ~Q.finite(Abs(x))) # raises; x = oo works +satask(Q.positive(x), ~Q.finite(re(x))) # raises; x = oo works +satask(Q.positive(x), ~Q.finite(im(x))) # raises; x = zoo works +satask(Q.positive(x), ~Q.finite(Abs(log(x)))) # raises; x = 0 works +satask(Q.positive(x), ~Q.complex(exp(x))) # raises; x = oo works +satask(Q.positive(x), ~Q.complex(Abs(x))) # raises; x = oo works +satask(Q.positive(x), ~Q.complex(re(x))) # raises; x = oo works +satask(Q.positive(x), ~Q.real(re(x))) # raises; x = oo works +``` + +The fuzzer found this family independently with the guards applied: +`--no-matrices --cases 1000 --engine random --seed 7` reports `random-417`, +`~Q.finite(Abs(log(x)))` with model `{x: 0, y: 1/2, z: exp(2*pi)}` (the +minimal query above is `~Q.finite(Abs(log(x)))` alone). + +A second inconsistency: with `infinite(x) & zero(y)`, `_pow_closure_facts` +claims `~complex(x**y)` (because the base is not complex) while +`_pow_rational_facts` claims `rational(x**y)` (because `~algebraic(base)` and +`integer(exp)`), and `rational -> complex`. `x = oo, y = 0` gives `1`. + +```python +satask(Q.complex(x**y), Q.infinite(x) & Q.zero(y)) # raises; sound True +satask(Q.rational(x**y), Q.infinite(x) & Q.zero(y)) # raises; sound True (ask True) +satask(Q.zero(x**y), Q.infinite(x) & Q.zero(y)) # raises; sound False +``` + +A third: a declared zero symbol makes the mixed hermitian/antihermitian Pow +rules inconsistent (`_pow_hermitian_fact` says the odd power is hermitian, +`_pow_antihermitian_facts` rule 3 says it is antihermitian, and 0 is both but +rule 1 says it is neither). `xz**3 == 0` is antihermitian. + +```python +xz = symbols("xz", zero=True) +satask(Q.antihermitian(xz**3)) # raises; sound True +satask(Q.antihermitian(1/xz)) # raises; sound False (zoo is not antihermitian) +``` + +### 7. Unevaluated Pow values answered wrongly + +The `_pow_facts` zero equivalence and the `Pow(2, 0)` rules disagree with the +actual values when `evaluate=False` is used. + +```python +satask(Q.zero(Pow(S.Zero, oo, evaluate=False))) # False, ask True (0**oo == 0) +satask(Q.zero(Pow(S.Zero, 1 + I, evaluate=False))) # False, ask True (== 0) +satask(Q.zero(Pow(oo, -1, evaluate=False))) # False, ask True (== 0) +satask(Q.complex(Pow(oo, 0, evaluate=False))) # raises (== 1) +satask(Q.real(Pow(S(2), S.Zero, evaluate=False))) # raises (== 1) +``` + +### 8. Matrix facts with concrete counterexamples + +`sympy.ask` does not decide element predicates of explicit matrices, so these +were checked by substituting the model and evaluating the result. + +```python +A, B = MatrixSymbol("A", 2, 2), MatrixSymbol("B", 2, 2) + +satask(Q.square(ZeroMatrix(2, 3))) # True, ask False +satask(Q.integer_elements(MatPow(A, -2)), + Q.integer_elements(A) & Q.invertible(A)) # True; A = diag(2, 1) +satask(Q.integer_elements(A*B), ~Q.integer_elements(A)) + # False; A = diag(1/2, 1), B = diag(2, 1) +satask(Q.real_elements(A*B), + ~Q.real_elements(A) & ~Q.real_elements(B)) # False; A = i*I, B = [[0, i], [-i, 0]] +satask(Q.integer_elements(A + B), + ~Q.integer_elements(A) & ~Q.integer_elements(B)) + # False; A = B = diag(1/2, 1) +satask(Q.real_elements(A + B), + ~Q.real_elements(A) & ~Q.real_elements(B)) # False; A = i*I, B = -i*I +satask(Q.integer_elements(HadamardProduct(A, B)), + ~Q.integer_elements(A)) # False; A = diag(1/2, 1), B = diag(2, 1) +satask(Q.fullrank(MatrixSlice(A, slice(0, 1), slice(0, 1))), + Q.fullrank(A)) # True; A = [[0, 1], [1, 0]] +``` + +The root causes are `_zeromatrix_facts` asserting `Q.square` unconditionally, +the negative exponent branch of `_matpow_facts` reusing the element-predicate +rule without an invertibility caveat for `integer_elements`, the negative +direction of `_matmul_facts` / `_matadd_facts` / `_hadamard_facts`, and +`_matrixslice_facts` transferring `fullrank` (and `invertible`, `unitary`, +`orthogonal`) to diagonal slices. + +### 9. Antihermitian Pow with a zero-capable hermitian base + +`_pow_antihermitian_facts` rule 1 says `hermitian(base) & integer(exp)` makes +the power not antihermitian, but `re(z) = 0` makes `re(z)**2 = 0`, which is +antihermitian. `sympy.ask` shares the atomic answer, so this is +`--strict`-only at the atom level, but the fuzzer reported the composite with +`--engine random --cases 500 --seed 1` on both the tip and with the guards: + +```python +satask(Q.antihermitian(re(z)**2)) # False, sound None +satask(~Q.prime(pi) ^ Q.antihermitian(re(z)**2), Q.algebraic(0)) + # True, sound None (z = I) +``` + +## What the two known guards miss + +The guards only touch the complex closure and the algebraic closure of `Pow`. +They fix exactly one test in the new file +(`test_zero_base_negative_exponent_is_not_algebraic_or_complex`); everything +else survives: + +- The `_pow_closure_facts` **exactly-one-argument** direction has no guard at + all, which is what makes `Pow(oo, 0, evaluate=False)` and + `Pow(2, 0, evaluate=False)` inconsistent. +- The closure guard uses `NOT(Q.negative(exp))`, so non-real exponents with a + zero base (`0**I = nan`, `0**(-I) = zoo`) still pass: `complex(x**I)`, + `real(x**(-1/2))`, `finite(x**I)`, `hermitian(x**-1)` under `zero(x)` stay + wrong. +- `_pow_facts`, `_pow_rational_facts`, `_pow_finite_fact`, `_pow_sign_facts`, + `_pow_hermitian_fact`, `_pow_antihermitian_facts` are untouched. +- All `Add`, `Mul`, function, matrix, and symbol-fact families are untouched. + +Upstream-shared blind spots (reported only by `--strict`, but still missed by a +narrow guard) include the zero-base non-real-exponent cases above, +`zero(x*y)` under `zero(y) & infinite(x)` (`0 * oo = nan`), and +`antihermitian(x**2)` under `antihermitian(x)`. + +## Tests added + +`reasoning/tests/test_soundness_adversarial.py`, 20 tests. Status on the +unfixed tip: **20 failed** (plus the pre-existing `201 passed, 1 xfailed`). +Status with the two local guards: **19 failed, 1 passed** +(`test_zero_base_negative_exponent_is_not_algebraic_or_complex` is the one the +guards fix). + +| Test | Tip | Guards | +|---|---|---| +| `test_imaginary_sum_cancellation_does_not_imply_not_real` | fail | fail | +| `test_acos_positivity_interval_excludes_one` | fail | fail | +| `test_factorial_integer_needs_nonnegative_argument` | fail | fail | +| `test_finite_of_unbounded_arguments` | fail | fail | +| `test_infinite_base_negative_integer_exponent_is_zero` | fail | fail | +| `test_unbounded_function_arguments_do_not_make_assumptions_inconsistent` | fail | fail | +| `test_infinite_base_zero_exponent_does_not_raise` | fail | fail | +| `test_unevaluated_pow_zero_exponent_does_not_raise` | fail | fail | +| `test_zeromatrix_shape_is_not_always_square` | fail | fail | +| `test_matpow_negative_exponent_does_not_preserve_integer_elements` | fail | fail | +| `test_matmul_element_predicates_are_not_closed_under_negation` | fail | fail | +| `test_matadd_element_predicates_are_not_closed_under_negation` | fail | fail | +| `test_hadamard_element_predicates_are_not_closed_under_negation` | fail | fail | +| `test_matrix_slice_does_not_transfer_fullrank` | fail | fail | +| `test_antihermitian_pow_with_zero_capable_hermitian_base` | fail | fail | +| `test_zero_symbol_pow_does_not_raise` | fail | fail | +| `test_zero_base_negative_exponent_is_not_algebraic_or_complex` | fail | **pass** | +| `test_zero_base_pow_values_are_not_answered_false` | fail | fail | +| `test_narrow_guard_blind_spots_for_zero_base` | fail | fail | +| `test_narrow_guard_blind_spots_for_mul_and_pow_parity` | fail | fail | + +The tests assert the sound answer rather than the current one, so the file is +expected to stay red until the underlying facts are fixed. The matrix tests +document the concrete model in a comment because `sympy.ask` cannot check +element predicates of explicit matrices. + +## Recommended follow-ups + +- Add a nonzero-base guard to the exactly-one direction of + `_pow_closure_facts` and to `_pow_facts`'s zero equivalence. +- Give `_pow_rational_facts` rule 6 and `_pow_antihermitian_facts` the same + kind of singularity guard the algebraic rule is getting. +- Do not assert `Q.complex`/`Q.real`/`Q.finite` unconditionally for + `exp`, `re`, `im`, `Abs`, `sin`, `cos`; gate them on the argument being + finite (or on the function value being defined). +- Add `~Q.zero(base)` (or `Q.nonzero(expr)`) to the hermitian Pow rules. +- Gate the negative direction of the element-predicate closures in + `_matmul_facts`, `_matadd_facts`, `_hadamard_facts`, and the `MatPow` + negative-exponent branch on the result's structure, not just the factors'. +- Restrict `_matrixslice_facts` transfers to the predicates a principal + submatrix actually preserves. + +## Caveats + +- The fuzzer's model pool has no `oo`, `zoo`, or `nan`, no declared symbols, + and no matrix expressions; five of the findings here need one of those. + Widening `SCALAR_VALUES` and the atom strategy would let the fuzzer catch + the infinite-base and function-at-infinity families automatically. +- `evaluate=False` Pow inputs are unusual, but they are accepted by `satask` + and the resulting inconsistencies show the fact set is not just incomplete + but contradictory. +- `sympy.ask` shares several of the counterexamples (noted per finding), so + `--strict` should be consulted before deciding whether to fix upstream-shared + rules or only the non-shared consequences. +- No LRA-specific unsoundness was found, but the LRA audit was small (150 + random cases). diff --git a/agent-reports/2026-09-22-sathandlers-soundness-root-cause.md b/agent-reports/2026-09-22-sathandlers-soundness-root-cause.md new file mode 100644 index 0000000..b56d836 --- /dev/null +++ b/agent-reports/2026-09-22-sathandlers-soundness-root-cause.md @@ -0,0 +1,232 @@ +# Agent report: why the Pow closure soundness bug slipped through + +- **Date:** 2026-09-22 +- **Status:** investigation complete; regression tests and this report landed on + `test/sathandlers-regressions` (base `a4f6e44`, merge of `main` + + `feature/sathandlers`). No product code was changed here; the fix is owned by + the `fix/sathandlers-soundness` agent. +- **Scope:** `reasoning/sathandlers.py` `_pow_closure_facts` / + `_pow_algebraic_facts` (git history only), new + `reasoning/tests/test_soundness_singularities.py`, run records in + `tools/check_soundness.py`; no edit to any handler. +- **Read this if:** you are fixing the zero-base Pow guards, adding closure rules + to `sathandlers.py` / `functionfacts.py`, wiring the soundness fuzzer into CI, + or updating the validation triage expectations. +- **Stale after:** the two closure rules gain a domain guard, the fuzzer becomes + a CI gate, or `validation/test_query.py`'s expectations for + `test_complex:1301` / `test_algebraic:2220` change. +- **TL;DR:** `3840c36` (tilorc-bot, 2026-09-21) added thirteen Pow rules at once + and guarded the `extended_real` and `finite` closures with + `OR(NOT(Q.zero(base)), NOT(Q.negative(exp)))`, but left the `complex` and + `algebraic` closures unguarded. Both are unsound at `0**negative = zoo`. The + port followed SymPy's zero-blind *assumption handlers* instead of the guarded + core evaluators (`Pow._eval_is_complex` calls `_eval_is_finite`; + `Pow._eval_is_algebraic` handles `base.is_zero` first). No test ever asked a + closure question with a possibly-zero base, the upstream validation suite + actually asserts the unsound closure as `True`, and `tools/check_soundness.py` + was never a CI gate. The finding was already documented in the fuzzer report + (`agent-reports/2026-09-22-soundness-fuzzer.md`, "Next steps") before the + branch merged, but the branch merged anyway. Four new regression tests fail + on the unfixed tip and all eight pass with the two known guards applied. + +## Findings + +### 1. Code: the guard convention existed, two closure rules did not get it + +`git blame` shows every line of the two rules is still from `3840c36` +("Add Add/Mul/Pow structural facts", tilorc-bot, 2026-09-21 23:25:03 +0000): + +- `_pow_closure_facts` (sathandlers.py:431-441): + - `extended_real` arm (line 439) *does* carry the guard, via a local + `defined = OR(NOT(Q.zero(base)), NOT(Q.negative(exp)))` (line 433). + - `complex` arm (line 436) has no guard. +- `_pow_algebraic_facts` (sathandlers.py:592-602): the + `algebraic(base) & rational(exp) -> algebraic(expr)` rule (line 595) has no + guard and the function does not even compute `defined`. + +The same commit and its neighbors already used the guard pattern in five other +places, so this was an omission, not a missing concept: + +| Rule | Guard | Line | +|---|---|---| +| `_pow_closure_facts` extended_real | `OR(NOT zero(base), NOT negative(exp))` | 439 | +| `_pow_finite_fact` | same | 610 | +| `_pow_real_facts` | same | 452-454 | +| `_pow_rational_facts` | `NOT zero(base)` / `OR(zero, positive(exp))` | 521-526 | +| `_pow_sign_facts` | `OR(NOT zero(base), positive(exp))` | 502-504 | + +Later commits added guards only reactively, one fuzzer/validation finding at a +time: `26df87a` (Pow imaginary-exponent realness), `15a4338` + `a629d94` (Mul +hermitian/antihermitian zero products), `98b1d61` (sin/cos realness), `fe333b3` +(`0**negative` realness). `fe333b3` is the smoking gun: it explicitly reasons +about `0**negative` being complex infinity and patches `Q.real` only, leaving +the `complex` and `algebraic` closures untouched (and consistent with the +upstream even-denominator rule it mentions in its comment). + +### 2. Why the singularity class was missed + +**Transcription source.** SymPy has two layers. The core evaluators guard the +domain: + +- `sympy/core/power.py:567-573` `Pow._eval_is_complex`: requires + `self._eval_is_finite()`. +- `sympy/core/power.py:633-637` `Pow._eval_is_finite`: `exp.is_negative and + base.is_zero -> False`. +- `sympy/core/power.py:1279-1287` `Pow._eval_is_algebraic`: `base.is_zero` is + handled before the algebraic closure. + +The *assumption handlers* do not: `ComplexPredicate` (sets.py:516) is a bare +`test_closed_group`, and `AlgebraicPredicate` (sets.py:785) returns `True` for +`base_algebraic & exp_algebraic & exp_rational` with no zero check. The port +copied the handler shape, so it inherited the handler's zero blindness and lost +the core evaluator's guard. `ask` is therefore unsound for the same queries +(`ask(Q.complex(1/x), Q.complex(x))` is `True`), which is exactly why the +oracle-only part of the fuzzer suppressed the closure rule and only the +*derived* query surfaced. + +**No singularity test matrix.** `reasoning/tests/test_structural_facts.py` +(added in `82e4186`, the companion test commit to `3840c36`) exercises Pow +closure only through generic symbols: realness/parity/imaginary rules plus +`0**negative` for `Q.real`. There is no `complex(x**...)` or `algebraic(x**...)` +test at all, and no closure test where the base may be zero in the same test +file. A grep for `complex(x**` / `algebraic(x**` across `reasoning/tests/` +returns nothing. + +**The validation suite asserts the unsound rule.** Upstream's own tests encode +the zero-blind behavior: + +- `test_query.py:1301`: `Q.complex(x**y), Q.complex(x) & Q.complex(y)` is + `True`. +- `test_query.py:2220`: `Q.algebraic(x**y), Q.algebraic(x) & Q.rational(y)` is + `True`. + +So the validation harness could never catch it: passing more of this suite and +being sound are in tension here. `test_bounded:1130` +(`Q.finite(x**y), Q.zero(x) & Q.negative(y)` is `False`) is the one upstream +expectation the current code satisfies only via the unsound complex chain, as +the guard experiment below shows. + +**The fuzzer was not a gate.** `.github/workflows/ci.yml` at `a4f6e44` runs +unit tests, mypy, the known-facts regeneration check, the old-assumptions scan, +and the (informational) validation comparison. It has no `check_soundness` +step; the README documents the tool as a manual audit. PR #8 landed the fuzzer +on `main` (`b07b332`) with the `~complex(1/x)` finding already written up, and +its "Next steps" said to fix the closure before gating CI on it. The +`feature/sathandlers` work then merged into `merge-test/sathandlers2` as +`a4f6e44` with the fuzzer red, and CI was green because nothing ran it. + +### 3. Fuzzer findings on `a4f6e44` + +Reproductions (all run with `PYTHONPATH` pointed at this worktree): + +| # | Query | satask | ask | status | +|---|---|---|---|---| +| 1 | `satask(Q.zero(x), ~Q.complex(1/x))` | `False` | `None` | reported; `x = 0` makes it `True` | +| 2 | `satask(Q.zero(x), ~Q.algebraic(1/x))` | `False` | `None` | same root cause | +| 3 | `satask(Q.complex(1/x), Q.complex(x))` | `True` | `True` | model counterexample, upstream-shared | +| 4 | `satask(Q.algebraic(1/x), Q.algebraic(x))` | `True` | `True` | model counterexample, upstream-shared | +| 5 | `satask(Q.finite(1/x), Q.zero(x))` | `True` | `False` | new in this audit; same complex->finite chain | +| 6 | `satask(Q.infinite(1/x), Q.zero(x))` | `False` | `True` | new; same chain | +| 7 | `satask(Q.finite(x**y), Q.zero(x) & Q.negative(y))` | `True` | `False` | same chain; hurts `test_bounded:1130` | +| 8 | `satask(~Q.prime(pi) ^ Q.antihermitian(re(z)**2))` | `True` | `None` | separate rule bug, see below | + +Runs: default Hypothesis (1 finding + 2 upstream-shared), `--engine random +--cases 300..800 --seed 1..24`, six 500-example and six 1000-example Hypothesis +runs. Finding 8 appeared once (random-98 of seed 1) and finding 5 appeared once +(one Hypothesis run); finding 6 was only confirmed by direct query afterwards. +Everything else the runs reported was finding 1, which the curated list already +contained. Findings 5-7 are one root cause: `complex(1/x)` plus the known fact +`complex -> finite` was the only route to `finite(1/x)`. + +**Finding 8 is a different rule and is not fixed by the two guards.** +`_pow_antihermitian_facts` (sathandlers.py:633-635) infers +`hermitian(base) & integer(exp) -> ~antihermitian(base**exp)`. At `base = 0` +with positive integer `exp` the power is `0`, which *is* antihermitian, so the +rule is unsound; the Mul analogue was guarded with `NOT(Q.zero(expr))` in +`15a4338`/`a629d94`, the Pow one was not. The atom-level claim is +upstream-shared (`ask(Q.antihermitian(re(z)**2))` is also `False`), but the +XOR query is a definite wrong answer that `ask` refuses to take a position on, +so the fuzzer reports it. Minimal repro: + +```python +satask(~Q.prime(pi) ^ Q.antihermitian(re(z)**2)) # True +# z = I: re(z)**2 = 0 is antihermitian and ~prime(pi) is True, so the XOR is False +ask(~Q.prime(pi) ^ Q.antihermitian(re(z)**2)) # None +``` + +Same class of neighbor, upstream-shared, worth an audit when the complex guard +lands: `_pow_closure_facts`' "exactly one non-complex arg" arm +(sathandlers.py:437-438) answers `False` for `Q.complex(1/x)` under +`~Q.complex(x)`, but `oo**-1 == 0` is complex. `ask` gives the same `False`, so +it is suppressed by default. + +### 4. The two guards fix the closure findings and one validation test regresses + +Applying only the two known guards locally (adding `defined` to the complex arm +and to the algebraic rule, then reverting): + +- New tests: 8/8 pass (4 fail on the unfixed tip). +- `tools/check_soundness.py --engine random --cases 300`: **0 findings** + (1 upstream-shared). +- `reasoning/tests`: 209 passed, 1 xfailed; mypy strict clean. +- Validation: **77 passed / 17 failed** (was 79/15). The two new failures are + `test_complex` at `test_query.py:1301` and `test_algebraic` at + `test_query.py:2220`, i.e. the upstream assertions that encode the unsound + rule. `test_bounded` was already failing. +- `satask(Q.finite(x**y), Q.zero(x) & Q.negative(y))` becomes `None` instead of + the upstream-expected `False`; recovering that needs a separate + `zero(base) & negative(exp) -> ~finite(expr)` rule (optional, out of scope). + +## Regression tests added + +`reasoning/tests/test_soundness_singularities.py`: + +- `test_reciprocal_counterexample_is_not_refuted`: both `Q.zero(x)` queries. +- `test_complex_closure_needs_a_defined_power`: `1/x` and `x**-2`. +- `test_algebraic_closure_needs_a_defined_power`: same for algebraic. +- `test_nonnegative_rational_exponents_still_close`: `x**(1/2)`, `x**(3/2)` + must still answer `True`, pinning the guard as `negative(exp)`, not + `nonzero(base)` or `integer(exp)`. +- `test_zero_exponent_is_defined_for_every_base`: `Pow(x, 0, evaluate=False)`. +- `test_nonzero_base_still_closes`: `~Q.zero(x)` and `Q.nonzero(x)` cases. +- `test_nonreal_nonzero_base_still_closes`: `1/x` under `imaginary(x) & + ~zero(x)`, pinning `~Q.zero` rather than `Q.nonzero`. +- `test_finiteness_does_not_leak_through_the_closure`: the `finite`/`infinite` + consequences, asserted as "not a wrong definite answer" rather than an exact + value. + +## What to do differently + +1. **Pair every closure rule with its domain guard in the same commit.** Add a + shared `_power_defined(base, exp)` helper and use it in all + closure/arithmetic rules, so a new rule cannot silently omit it. +2. **Port from `Expr.is_*`, not only from the assumption handlers.** When a + rule mirrors `sympy/assumptions/handlers/`, check the core evaluator + (`_eval_is_*`) for conditions the handler omits; the `complex` and + `algebraic` gaps are exactly `_eval_is_finite()` / `is_zero` checks. +3. **Keep a singularity test matrix for every Pow/function rule:** base in + {zero, may be zero, nonzero} x exponent in {negative int, negative rational, + 0, positive int, positive rational, symbolic}, with assertions for both + directions (no definite answer through the singularity; inference still + fires when the guard is satisfied). The new file is the Pow instance of that + matrix. +4. **Run the fuzzer before merge and then gate on it.** Wire + `tools/check_soundness.py` (curated + `--engine random --seed 30222 --cases + 300`, or a fixed-seed Hypothesis run) into CI as soon as the guards land. + A documented "Next steps" fix must be a merge blocker: this finding was + written up in the fuzzer report before `a4f6e44` merged. +5. **Treat `ask` as a secondary oracle.** Upstream shares the complex/algebraic + closure unsoundness, so oracle-only comparison suppresses it. Concrete + models (and the `--strict` shared list) are the primary signal, and a + derived query such as `~complex(1/x) -> ~zero(x)` is often the unshared + consequence that exposes a shared bad rule. +6. **Do not use the validation pass rate as a soundness gate.** Two upstream + tests assert the unsound closure. When the guards land, move + `test_complex:1301` and `test_algebraic:2220` into the documented + known-mismatch set instead of weakening the guard, and update + `agent-reports/2026-09-21-sathandlers-validation-triage.md`'s 79/104 + baseline accordingly. +7. **Audit the rest of the zero-blind family while here.** Known leftovers: + `_pow_antihermitian_facts` (finding 8), the `~complex(x) -> ~complex(1/x)` + arm (`oo**-1 == 0`), and the upstream-shared even-denominator realness rule + for `0**negative-rational`, which `fe333b3` deliberately mirrored. diff --git a/reasoning/functionfacts.py b/reasoning/functionfacts.py new file mode 100644 index 0000000..8acfeb4 --- /dev/null +++ b/reasoning/functionfacts.py @@ -0,0 +1,257 @@ +"""Facts about elementary functions from direct structural inspection. + +This module extends :mod:`reasoning.numberfacts` from numbers to the standard +elementary functions. Like that module it never reads SymPy's old +assumptions: the class of an expression selects a rule table, and every rule is +a lightweight formula over predicate applications whose single argument is a +SymPy expression the discovery loop can visit. + +Several rules mention expressions built from the argument, such as ``arg - 1`` +or ``arg/(I*pi)``. That is deliberate: the SAT layer can only relate predicates +applied to the same expression, so structural side conditions have to be spelled +out as well-known objects (``Q.positive(x - 1)`` and the like). The discovery +loop then treats those expressions as new subjects and derives their numeric +facts. + +The generic ``Add`` rules at the bottom are the only facts here that are not +function specific. They are the smallest structural facts the function rules +need in order to talk about sums such as ``log(1 + I)``; they are sound on their +own and overlap with the dedicated Add/Mul/Pow facts kept elsewhere. +""" +from __future__ import annotations + +from typing import Callable + +from sympy.core.add import Add +from sympy.core.numbers import Exp1, Number +from sympy.core.power import Pow +from sympy.core.singleton import S +from sympy.functions.combinatorial.factorials import factorial +from sympy.functions.elementary.complexes import Abs, im, re, sign +from sympy.functions.elementary.exponential import exp, log +from sympy.functions.elementary.trigonometric import ( + acos, acot, asin, atan, cos, cot, sin, tan, +) + +from reasoning.clauses import AND, EQUIVALENT, IMPLIES, NOT, OR +from reasoning.predicates import Q +from reasoning.registry import ClassFactRegistry +from reasoning.sympy_types import SymPyExpr + +PredicateCall = Callable[[SymPyExpr], object] + +_IMAGINARY_PI = S.ImaginaryUnit * S.Pi + + +def _argument(expr: SymPyExpr) -> SymPyExpr: + return expr.args[0] + + +def _allargs(predicate: PredicateCall, expr: SymPyExpr) -> object: + return AND(*(predicate(arg) for arg in expr.args)) + + +def _exactlyonearg(predicate: PredicateCall, expr: SymPyExpr) -> object: + predicates = [predicate(arg) for arg in expr.args] + return OR(*(AND(item, *(NOT(other) for other in predicates[:index] + predicates[index + 1:])) + for index, item in enumerate(predicates))) + + +def _sin_cos_facts(expr: SymPyExpr) -> list[object]: + arg = _argument(expr) + facts: list[object] = [Q.complex(expr), Q.finite(expr)] + if not isinstance(arg, Number): + # Realness is only derived for non-literal arguments. For a numeric + # argument it would give exact facts about an unevaluated value such + # as ``cos(2)**2 + sin(2)**2``, which the query suite deliberately + # leaves undecided. + facts.insert(0, IMPLIES(Q.real(arg), Q.real(expr))) + return facts + + +def _zero_algebraic_facts(expr: SymPyExpr) -> list[object]: + arg = _argument(expr) + return [ + IMPLIES(Q.zero(arg), Q.algebraic(expr)), + IMPLIES(Q.zero(arg), Q.rational(expr)), + IMPLIES(AND(Q.algebraic(arg), Q.nonzero(arg)), NOT(Q.algebraic(expr))), + ] + + +def _atan_facts(expr: SymPyExpr) -> list[object]: + arg = _argument(expr) + return [ + IMPLIES(Q.real(arg), Q.real(expr)), + EQUIVALENT(Q.positive(expr), Q.positive(arg)), + ] + + +def _asin_facts(expr: SymPyExpr) -> list[object]: + arg = _argument(expr) + return [ + IMPLIES(AND(Q.positive(arg), Q.nonpositive(arg - 1)), Q.positive(expr)), + IMPLIES(AND(Q.negative(arg), Q.nonnegative(arg + 1)), NOT(Q.positive(expr))), + ] + + +def _acos_facts(expr: SymPyExpr) -> list[object]: + arg = _argument(expr) + return [ + # acos(1) == 0 is not positive, so the upper end is excluded. + IMPLIES( + AND(Q.nonnegative(arg + 1), Q.negative(arg - 1)), + Q.positive(expr), + ), + IMPLIES(Q.zero(arg - 1), Q.algebraic(expr)), + IMPLIES(Q.zero(arg - 1), Q.rational(expr)), + IMPLIES(AND(Q.algebraic(arg), Q.nonzero(arg - 1)), NOT(Q.algebraic(expr))), + ] + + +def _acot_facts(expr: SymPyExpr) -> list[object]: + arg = _argument(expr) + return [ + IMPLIES(Q.real(arg), Q.real(expr)), + EQUIVALENT(Q.positive(expr), Q.real(arg)), + IMPLIES(Q.algebraic(arg), NOT(Q.algebraic(expr))), + ] + + +def _cot_facts(expr: SymPyExpr) -> list[object]: + arg = _argument(expr) + return [IMPLIES(Q.algebraic(arg), NOT(Q.algebraic(expr)))] + + +def _exp_facts(expr: SymPyExpr) -> list[object]: + if isinstance(expr, Pow) and not isinstance(expr.base, Exp1): + return [] + arg = expr.exp + # ``period`` is the multiple of ``I*pi`` in the exponent, so that + # ``exp(2*pi*I)`` has period 2 and ``exp(pi*I/2)`` has period 1/2. + period = arg / _IMAGINARY_PI + twice = 2 * period + return [ + # exp(oo) == oo and exp(-oo) == 0, so only a finite argument forces a + # finite complex value. + IMPLIES(Q.finite(arg), Q.complex(expr)), + IMPLIES(OR(Q.real(arg), Q.integer(period)), Q.real(expr)), + IMPLIES(AND(Q.imaginary(arg), NOT(Q.integer(period))), NOT(Q.real(expr))), + IMPLIES(Q.real(arg), Q.positive(expr)), + IMPLIES(Q.even(period), Q.positive(expr)), + IMPLIES(Q.odd(period), Q.negative(expr)), + IMPLIES(AND(Q.integer(twice), NOT(Q.integer(period))), Q.imaginary(expr)), + IMPLIES(Q.finite(arg), Q.finite(expr)), + IMPLIES(Q.zero(arg), Q.algebraic(expr)), + IMPLIES(Q.zero(arg), Q.rational(expr)), + IMPLIES(AND(Q.algebraic(arg), Q.nonzero(arg)), NOT(Q.algebraic(expr))), + ] + + +def _exp_base_pow_facts(expr: SymPyExpr) -> list[object]: + # ``exp(u)**v`` is real when both ``u`` and ``v`` are imaginary: the + # principal logarithm of ``exp(u)`` is ``u + 2*pi*I*k``, so the power + # equals ``exp(u*v + 2*pi*I*k*v)``, and both exponents are real. + base = expr.base + if isinstance(base, Pow) and isinstance(base.base, Exp1): + base_arg = base.exp + elif isinstance(base, exp): + base_arg = base.args[0] + else: + return [] + return [IMPLIES(AND(Q.imaginary(base_arg), Q.imaginary(expr.exp)), + Q.real(expr))] + + +def _log_facts(expr: SymPyExpr) -> list[object]: + arg = _argument(expr) + return [ + IMPLIES(Q.positive(arg), Q.real(expr)), + IMPLIES(Q.positive(arg - 1), Q.positive(expr)), + IMPLIES(Q.positive(arg), NOT(Q.imaginary(expr))), + IMPLIES(Q.imaginary(arg), NOT(Q.real(expr))), + IMPLIES(AND(Q.complex(arg), NOT(Q.real(arg))), NOT(Q.real(expr))), + IMPLIES(AND(Q.real(arg), NOT(Q.positive(arg))), NOT(Q.real(expr))), + IMPLIES(AND(Q.finite(arg), NOT(Q.zero(arg))), Q.finite(expr)), + IMPLIES(Q.zero(arg), NOT(Q.finite(expr))), + IMPLIES(Q.infinite(arg), NOT(Q.finite(expr))), + IMPLIES(Q.zero(arg - 1), Q.algebraic(expr)), + IMPLIES(Q.zero(arg - 1), Q.rational(expr)), + IMPLIES(AND(Q.algebraic(arg), Q.nonzero(arg - 1)), NOT(Q.algebraic(expr))), + ] + + +def _abs_facts(expr: SymPyExpr) -> list[object]: + arg = _argument(expr) + return [ + # Abs(oo) == Abs(zoo) == oo is not complex. + IMPLIES(Q.finite(arg), Q.complex(expr)), + IMPLIES(Q.nonzero(arg), Q.positive(expr)), + IMPLIES(Q.nonzero(arg), Q.nonzero(expr)), + ] + + +def _re_facts(expr: SymPyExpr) -> list[object]: + arg = _argument(expr) + # re(oo) == oo is not complex and re(nan) == nan is not real. + return [ + IMPLIES(Q.finite(arg), Q.real(expr)), + IMPLIES(Q.finite(arg), Q.complex(expr)), + IMPLIES(Q.even(arg), Q.even(expr)), + ] + + +def _im_facts(expr: SymPyExpr) -> list[object]: + arg = _argument(expr) + # im(zoo) == nan is not complex, so the argument must be finite. + return [ + IMPLIES(Q.finite(arg), Q.real(expr)), + IMPLIES(Q.finite(arg), Q.complex(expr)), + IMPLIES(Q.even(arg), Q.even(expr)), + IMPLIES(Q.real(arg), Q.even(expr)), + ] + + +def _factorial_facts(expr: SymPyExpr) -> list[object]: + arg = _argument(expr) + return [ + IMPLIES(AND(Q.integer(arg), Q.positive(arg)), Q.positive(expr)), + IMPLIES(AND(Q.integer(arg), Q.nonnegative(arg)), Q.integer(expr)), + ] + + +def _sign_facts(expr: SymPyExpr) -> list[object]: + return [Q.finite(expr)] + + +def _add_complex_facts(expr: SymPyExpr) -> list[object]: + return [IMPLIES(_allargs(Q.complex, expr), Q.complex(expr))] + + +def _add_not_real_facts(expr: SymPyExpr) -> list[object]: + return [IMPLIES( + _exactlyonearg(lambda arg: NOT(Q.real(arg)), expr), NOT(Q.real(expr)))] + + +def register_function_facts(registry: ClassFactRegistry) -> None: + """Attach the elementary-function handlers to a fact registry.""" + registry.multiregister(sin, cos)(_sin_cos_facts) + registry.multiregister(sin, tan, asin, atan, cos)(_zero_algebraic_facts) + registry.multiregister(exp)(_exp_facts) + registry.multiregister(Pow)(_exp_facts) + registry.multiregister(Pow)(_exp_base_pow_facts) + registry.multiregister(atan)(_atan_facts) + registry.multiregister(asin)(_asin_facts) + registry.multiregister(acos)(_acos_facts) + registry.multiregister(acot)(_acot_facts) + registry.multiregister(cot)(_cot_facts) + registry.multiregister(log)(_log_facts) + registry.multiregister(Abs)(_abs_facts) + registry.multiregister(re)(_re_facts) + registry.multiregister(im)(_im_facts) + registry.multiregister(factorial)(_factorial_facts) + registry.multiregister(sign)(_sign_facts) + registry.multiregister(Add)(_add_complex_facts) + registry.multiregister(Add)(_add_not_real_facts) + + +__all__ = ["register_function_facts"] diff --git a/reasoning/matrixfacts.py b/reasoning/matrixfacts.py new file mode 100644 index 0000000..27a9786 --- /dev/null +++ b/reasoning/matrixfacts.py @@ -0,0 +1,476 @@ +"""Facts about matrix expressions from direct structural inspection. + +This module extends :mod:`reasoning.numberfacts` and +:mod:`reasoning.functionfacts` from scalars to the matrix expression classes. +Like those modules it never reads SymPy's old assumptions: the class of an +expression selects a rule, and each rule is a lightweight formula over +predicate applications whose arguments the discovery loop can visit. Rules +that mention a structural subexpression (a transpose argument, a power base, a +block or a slice parent) hand that subexpression to the discovery loop as a new +subject, so the facts about it are found in a later round. + +Some facts are deliberately omitted where the pinned query suite expects an +unknown answer: non-square slices do not report their shape as square, because +``symmetric`` would then be forced to ``False`` through the imported known +facts; sums of orthogonal or unitary matrices get no closure rule; and +``fullrank`` is not reported for a non-square ``MatrixSymbol``. +""" +from __future__ import annotations + +from typing import Callable, Iterable + +from sympy.core.numbers import Integer, Number +from sympy.functions.elementary.complexes import conjugate +from sympy.matrices import MatrixBase +from sympy.matrices.expressions import ( + BlockDiagMatrix, BlockMatrix, Determinant, DiagMatrix, DiagonalMatrix, + HadamardProduct, Identity, Inverse, MatAdd, MatMul, MatPow, MatrixExpr, + MatrixSlice, MatrixSymbol, OneMatrix, Trace, Transpose, ZeroMatrix, +) +from sympy.matrices.expressions.factorizations import Factorization +from sympy.matrices.expressions.fourier import DFT +from sympy.matrices.expressions.matexpr import MatrixElement + +from reasoning.clauses import AND, EQUIVALENT, IMPLIES, NOT, OR +from reasoning.predicates import Q +from reasoning.registry import ClassFactRegistry +from reasoning.sympy_types import SymPyExpr + +PredicateCall = Callable[[SymPyExpr], object] + +_ELEMENT_PREDICATES = ( + (Q.real_elements, Q.real), + (Q.complex_elements, Q.complex), + (Q.integer_elements, Q.integer), +) + +_MATPOW_PREDICATES = ( + Q.symmetric, Q.upper_triangular, Q.lower_triangular, Q.diagonal, + Q.orthogonal, Q.unitary, Q.fullrank, Q.invertible, +) + +_IDENTITY_PREDICATES = ( + Q.square, Q.invertible, Q.fullrank, Q.symmetric, Q.diagonal, + Q.upper_triangular, Q.lower_triangular, Q.triangular, Q.unit_triangular, + Q.integer_elements, Q.positive_definite, Q.orthogonal, Q.unitary, +) + +_ZERO_PREDICATES = ( + Q.integer_elements, +) + +_ZERO_SQUARE_PREDICATES = ( + Q.symmetric, Q.diagonal, Q.upper_triangular, Q.lower_triangular, + Q.triangular, +) + +_ZERO_NEGATED = ( + Q.invertible, Q.fullrank, Q.positive_definite, Q.orthogonal, Q.unitary, +) + +_TRANSFER_PREDICATES = ( + Q.symmetric, Q.invertible, Q.fullrank, Q.unitary, Q.orthogonal, + Q.diagonal, Q.positive_definite, +) + +# A principal submatrix inherits the parent's symmetry, diagonal shape and +# positive definiteness, but none of the predicates that need the full size: +# [[0]] is the leading 1x1 slice of the full-rank, invertible, unitary and +# orthogonal [[0, 1], [1, 0]], so ``fullrank``, ``invertible``, ``unitary`` +# and ``orthogonal`` are deliberately absent. Keeping ``invertible`` here +# would also re-derive ``fullrank`` for the slice through the ``invertible -> +# fullrank`` known fact. +_SLICE_TRANSFER_PREDICATES = ( + Q.symmetric, Q.diagonal, Q.positive_definite, +) + + +def _all(predicate: PredicateCall, args: Iterable[SymPyExpr]) -> object: + return AND(*(predicate(arg) for arg in args)) + + +def _any(predicate: PredicateCall, args: Iterable[SymPyExpr]) -> object: + return OR(*(predicate(arg) for arg in args)) + + +def _allargs(predicate: PredicateCall, expr: SymPyExpr) -> object: + return _all(predicate, expr.args) + + +def _anyarg(predicate: PredicateCall, expr: SymPyExpr) -> object: + return _any(predicate, expr.args) + + +def _closed(predicate: PredicateCall, expr: SymPyExpr) -> list[object]: + return [ + IMPLIES(_allargs(predicate, expr), predicate(expr)), + IMPLIES(_anyarg(lambda arg: NOT(predicate(arg)), expr), + NOT(predicate(expr))), + ] + + +def _closed_positive(predicate: PredicateCall, expr: SymPyExpr) -> list[object]: + return [IMPLIES(_allargs(predicate, expr), predicate(expr))] + + +def _square(expr: SymPyExpr) -> bool: + return bool(expr.shape[0] == expr.shape[1]) + + +def _shape_facts(expr: SymPyExpr) -> list[object]: + if _square(expr): + return [Q.square(expr)] + return [NOT(Q.square(expr))] + + +def _empty_or_1x1(expr: SymPyExpr) -> bool: + return bool(expr.shape in ((0, 0), (1, 1))) + + +def _matrixsymbol_facts(expr: SymPyExpr) -> list[object]: + facts = _shape_facts(expr) + if _empty_or_1x1(expr): + facts.append(Q.diagonal(expr)) + return facts + + +def _identity_facts(expr: SymPyExpr) -> list[object]: + return [predicate(expr) for predicate in _IDENTITY_PREDICATES] + + +def _zeromatrix_facts(expr: SymPyExpr) -> list[object]: + facts = _shape_facts(expr) + facts.extend(predicate(expr) for predicate in _ZERO_PREDICATES) + if _square(expr): + facts.extend(predicate(expr) for predicate in _ZERO_SQUARE_PREDICATES) + facts.extend(NOT(predicate(expr)) for predicate in _ZERO_NEGATED) + return facts + + +def _onematrix_facts(expr: SymPyExpr) -> list[object]: + one_by_one = expr.shape == (1, 1) + facts = _shape_facts(expr) + facts.append(EQUIVALENT(Q.symmetric(expr), Q.square(expr))) + for predicate in (Q.invertible, Q.fullrank, Q.positive_definite, + Q.diagonal, Q.upper_triangular, Q.lower_triangular): + facts.append(predicate(expr) if one_by_one else NOT(predicate(expr))) + facts.append(Q.integer_elements(expr)) + return facts + + +def _explicit_invertible(expr: SymPyExpr) -> object: + if not all(isinstance(entry, Number) for entry in expr): + return None + determinant = expr.det() + if not isinstance(determinant, Number): + return None + return determinant != 0 + + +def _provably_nonzero(expr: SymPyExpr) -> bool: + from sympy.assumptions.ask import Q as SymPyQ + from reasoning.satask import satask + return satask(SymPyQ.zero(expr)) is False + + +def _hermitian_character(expr: SymPyExpr, negate: bool) -> bool | None: + if not _square(expr): + return None + unknown = False + for row in range(expr.rows): + for column in range(expr.cols): + mirrored = conjugate(expr[column, row]) + difference = expr[row, column] - (-mirrored if negate else mirrored) + if difference == 0: + continue + if not difference.free_symbols and _provably_nonzero(difference): + return False + unknown = True + return None if unknown else True + + +def _matrixbase_facts(expr: SymPyExpr) -> list[object]: + facts = _shape_facts(expr) + if not _square(expr): + return facts + for predicate, negate in ((Q.hermitian, False), (Q.antihermitian, True)): + character = _hermitian_character(expr, negate) + if character is not None: + facts.append(predicate(expr) if character + else NOT(predicate(expr))) + invertible = _explicit_invertible(expr) + if invertible is not None: + facts.append(Q.invertible(expr) if invertible else NOT(Q.invertible(expr))) + elif expr.shape == (1, 1) and isinstance(expr[0, 0], MatrixExpr): + facts.append(EQUIVALENT(Q.invertible(expr), Q.invertible(expr[0, 0]))) + return facts + + +def _matadd_facts(expr: SymPyExpr) -> list[object]: + facts = _shape_facts(expr) + for predicate in (Q.symmetric, Q.diagonal, Q.upper_triangular, + Q.lower_triangular, Q.positive_definite): + facts.extend(_closed_positive(predicate, expr)) + # Summands can cancel imaginary or fractional parts (diag(1/2, 1) + + # diag(1/2, 1) is integral, i*I + (-i)*I is zero), so drop only the + # negative closure: the positive direction stays. + for predicate, _scalar in _ELEMENT_PREDICATES: + facts.extend(_closed_positive(predicate, expr)) + return facts + + +def _matmul_facts(expr: SymPyExpr) -> list[object]: + facts = _shape_facts(expr) + matrices = [arg for arg in expr.args if isinstance(arg, MatrixExpr)] + scalars = [arg for arg in expr.args if not isinstance(arg, MatrixExpr)] + if not matrices: + return facts + square_factors = _all(Q.square, matrices) + facts.append(IMPLIES( + square_factors, + EQUIVALENT(Q.invertible(expr), _all(Q.invertible, matrices)))) + facts.append(IMPLIES( + AND(square_factors, + _any(lambda arg: NOT(Q.invertible(arg)), matrices)), + NOT(Q.invertible(expr)))) + facts.append(IMPLIES(_all(Q.fullrank, matrices), Q.fullrank(expr))) + coefficient = expr.as_coeff_mmul()[0] + for predicate in (Q.orthogonal, Q.unitary): + if coefficient == 1: + facts.append(IMPLIES(_all(predicate, matrices), predicate(expr))) + facts.append(IMPLIES( + AND(square_factors, + _any(lambda arg: NOT(Q.invertible(arg)), matrices)), + NOT(predicate(expr)))) + facts.append(IMPLIES( + AND(Q.positive(coefficient), _all(Q.positive_definite, matrices)), + Q.positive_definite(expr))) + if len(matrices) >= 2 and matrices[0] == matrices[-1].T: + if len(matrices) == 2: + facts.append(IMPLIES( + AND(Q.positive(coefficient), Q.square(matrices[0]), + Q.fullrank(matrices[0])), + Q.positive_definite(expr))) + facts.append(Q.symmetric(expr)) + else: + middle = MatMul(*matrices[1:-1]) + facts.append(IMPLIES( + AND(Q.positive(coefficient), Q.fullrank(matrices[0]), + Q.positive_definite(middle)), + Q.positive_definite(expr))) + facts.append(IMPLIES( + Q.symmetric(middle), Q.symmetric(expr))) + for predicate in (Q.symmetric, Q.upper_triangular, Q.lower_triangular): + facts.append(IMPLIES(_all(predicate, matrices), predicate(expr))) + if _empty_or_1x1(expr): + facts.append(Q.diagonal(expr)) + else: + facts.append(IMPLIES(_all(Q.diagonal, matrices), Q.diagonal(expr))) + # Element predicates are only closed in the positive direction: products + # can cancel imaginary or fractional parts (diag(1/2, 1)*diag(2, 1) is + # integral, i*I times [[0, i], [-i, 0]] is real), so a factor that fails + # the predicate does not make the product fail it. + for predicate, scalar_predicate in _ELEMENT_PREDICATES: + terms = ([scalar_predicate(arg) for arg in scalars] + + [predicate(arg) for arg in matrices]) + facts.append(IMPLIES(AND(*terms), predicate(expr))) + return facts + + +def _matpow_facts(expr: SymPyExpr) -> list[object]: + base, exponent = expr.base, expr.exp + facts = _shape_facts(expr) + if isinstance(exponent, Integer) and exponent >= 0: + for predicate in _MATPOW_PREDICATES: + facts.append(IMPLIES(predicate(base), predicate(expr))) + for predicate, _scalar in _ELEMENT_PREDICATES: + facts.append(IMPLIES(predicate(base), predicate(expr))) + elif isinstance(exponent, Integer): + facts.append(IMPLIES(Q.invertible(base), Q.invertible(expr))) + for predicate in (Q.symmetric, Q.upper_triangular, Q.lower_triangular, + Q.diagonal): + facts.append(IMPLIES( + AND(Q.invertible(base), predicate(base)), predicate(expr))) + for predicate in (Q.orthogonal, Q.unitary): + facts.append(IMPLIES(predicate(base), predicate(expr))) + # Inverses preserve realness and complexness, but not integrality: + # diag(2, 1)**-2 == diag(1/4, 1). + for predicate in (Q.real_elements, Q.complex_elements): + facts.append(IMPLIES( + AND(Q.invertible(base), predicate(base)), predicate(expr))) + else: + integer_nonnegative = AND(Q.integer(exponent), + NOT(Q.negative(exponent))) + for predicate in (Q.symmetric, Q.upper_triangular, Q.lower_triangular, + Q.diagonal, Q.invertible): + facts.append(IMPLIES( + AND(integer_nonnegative, predicate(base)), predicate(expr))) + for predicate, _scalar in _ELEMENT_PREDICATES: + facts.append(IMPLIES( + AND(integer_nonnegative, predicate(base)), predicate(expr))) + facts.append(IMPLIES( + AND(Q.integer(exponent), Q.negative(exponent), + Q.invertible(base), Q.real_elements(base)), + Q.real_elements(expr))) + facts.append(IMPLIES(Q.positive_definite(base), Q.positive_definite(expr))) + return facts + + +def _transpose_facts(expr: SymPyExpr) -> list[object]: + arg = expr.arg + facts = _shape_facts(expr) + for predicate in _TRANSFER_PREDICATES: + facts.append(EQUIVALENT(predicate(expr), predicate(arg))) + facts.append(EQUIVALENT(Q.upper_triangular(expr), Q.lower_triangular(arg))) + facts.append(EQUIVALENT(Q.lower_triangular(expr), Q.upper_triangular(arg))) + for predicate, _scalar in _ELEMENT_PREDICATES: + facts.append(EQUIVALENT(predicate(expr), predicate(arg))) + return facts + + +def _inverse_facts(expr: SymPyExpr) -> list[object]: + arg = expr.arg + facts = _shape_facts(expr) + facts.append(Q.invertible(expr)) + for predicate in (Q.symmetric, Q.unitary, Q.orthogonal, Q.diagonal, + Q.positive_definite): + facts.append(EQUIVALENT(predicate(expr), predicate(arg))) + facts.append(EQUIVALENT(Q.upper_triangular(expr), Q.upper_triangular(arg))) + facts.append(EQUIVALENT(Q.lower_triangular(expr), Q.lower_triangular(arg))) + facts.append(IMPLIES(Q.complex_elements(arg), Q.complex_elements(expr))) + facts.append(IMPLIES( + AND(Q.invertible(arg), Q.real_elements(arg)), Q.real_elements(expr))) + return facts + + +def _matrixslice_facts(expr: SymPyExpr) -> list[object]: + facts: list[object] = [] + if _empty_or_1x1(expr): + facts.append(Q.diagonal(expr)) + if expr.on_diag: + # A slice covering the whole parent is the parent itself, so it keeps + # the rank-like predicates as well; a proper principal submatrix only + # preserves the size-independent ones. + transfer = (_TRANSFER_PREDICATES + if expr.shape == expr.parent.shape + else _SLICE_TRANSFER_PREDICATES) + for predicate in transfer + (Q.upper_triangular, Q.lower_triangular): + facts.append(IMPLIES(predicate(expr.parent), predicate(expr))) + for predicate, _scalar in _ELEMENT_PREDICATES: + facts.append(IMPLIES(predicate(expr.parent), predicate(expr))) + return facts + + +def _blockmatrix_facts(expr: SymPyExpr) -> list[object]: + facts = _shape_facts(expr) + blocks = list(expr.blocks) + if expr.blockshape == (1, 1): + facts.append(EQUIVALENT(Q.invertible(expr), Q.invertible(blocks[0]))) + elif blocks and all(isinstance(block, MatrixBase) for block in blocks): + explicit = expr.as_explicit() + invertible = _explicit_invertible(explicit) + if invertible is not None: + facts.append(Q.invertible(expr) if invertible + else NOT(Q.invertible(expr))) + for predicate, _scalar in _ELEMENT_PREDICATES: + facts.append(IMPLIES( + AND(*(predicate(block) for block in blocks)), predicate(expr))) + facts.append(IMPLIES( + OR(*(NOT(predicate(block)) for block in blocks)), + NOT(predicate(expr)))) + return facts + + +def _blockdiag_facts(expr: SymPyExpr) -> list[object]: + if expr.rowblocksizes != expr.colblocksizes: + return [NOT(Q.square(expr))] + facts: list[object] = [Q.square(expr)] + diagonal = list(expr.diag) + if diagonal: + facts.append(EQUIVALENT( + Q.invertible(expr), + AND(*(Q.invertible(block) for block in diagonal)))) + return facts + + +def _determinant_facts(expr: SymPyExpr) -> list[object]: + arg = expr.args[0] + return [ + IMPLIES(Q.positive_definite(arg), Q.positive(expr)), + IMPLIES(Q.real_elements(arg), Q.real_elements(expr)), + IMPLIES(Q.complex_elements(arg), Q.complex_elements(expr)), + IMPLIES(Q.integer_elements(arg), Q.integer_elements(expr)), + IMPLIES(Q.integer_elements(arg), Q.integer(expr)), + ] + + +def _trace_facts(expr: SymPyExpr) -> list[object]: + arg = expr.args[0] + return [ + IMPLIES(Q.positive_definite(arg), Q.positive(expr)), + IMPLIES(Q.real_elements(arg), Q.real_elements(expr)), + IMPLIES(Q.complex_elements(arg), Q.complex_elements(expr)), + IMPLIES(Q.integer_elements(arg), Q.integer_elements(expr)), + IMPLIES(Q.integer_elements(arg), Q.integer(expr)), + ] + + +def _hadamard_facts(expr: SymPyExpr) -> list[object]: + # Entrywise products of non-integer matrices can still be integral + # (diag(1/2, 1) hadamard diag(2, 1) is the identity), so only the + # positive closure is sound. + return [fact for predicate, _scalar in _ELEMENT_PREDICATES + for fact in _closed_positive(predicate, expr)] + + +def _factorization_facts(expr: SymPyExpr) -> list[object]: + return [fact for predicate in (Q.real_elements, Q.complex_elements) + for fact in _closed(predicate, expr)] + + +def _dft_facts(expr: SymPyExpr) -> list[object]: + return [Q.square(expr), Q.unitary(expr), Q.complex_elements(expr)] + + +def _diagonal_matrix_facts(expr: SymPyExpr) -> list[object]: + return [Q.diagonal(expr)] + + +def _matrixelement_facts(expr: SymPyExpr) -> list[object]: + args = expr.args + parent = args[0] + facts = [ + IMPLIES(Q.real_elements(parent), Q.real(expr)), + IMPLIES(Q.complex_elements(parent), Q.complex(expr)), + IMPLIES(Q.integer_elements(parent), Q.integer(expr)), + ] + if len(args) == 3 and args[1] == args[2]: + facts.append(IMPLIES(Q.positive_definite(parent), Q.positive(expr))) + return facts + + +def register_matrix_facts(registry: ClassFactRegistry) -> None: + """Attach the matrix-expression handlers to a fact registry.""" + registry.multiregister(MatrixSymbol)(_matrixsymbol_facts) + registry.multiregister(Identity)(_identity_facts) + registry.multiregister(ZeroMatrix)(_zeromatrix_facts) + registry.multiregister(OneMatrix)(_onematrix_facts) + registry.multiregister(MatrixBase)(_matrixbase_facts) + registry.multiregister(MatAdd)(_matadd_facts) + registry.multiregister(MatMul)(_matmul_facts) + registry.multiregister(MatPow)(_matpow_facts) + registry.multiregister(Transpose)(_transpose_facts) + registry.multiregister(Inverse)(_inverse_facts) + registry.multiregister(MatrixSlice)(_matrixslice_facts) + registry.multiregister(BlockMatrix)(_blockmatrix_facts) + registry.multiregister(BlockDiagMatrix)(_blockdiag_facts) + registry.multiregister(Determinant)(_determinant_facts) + registry.multiregister(Trace)(_trace_facts) + registry.multiregister(HadamardProduct)(_hadamard_facts) + registry.multiregister(Factorization)(_factorization_facts) + registry.multiregister(DFT)(_dft_facts) + registry.multiregister(DiagMatrix, DiagonalMatrix)(_diagonal_matrix_facts) + registry.multiregister(MatrixElement)(_matrixelement_facts) + + +__all__ = ["register_matrix_facts"] diff --git a/reasoning/satask.py b/reasoning/satask.py index d913b45..acd83aa 100644 --- a/reasoning/satask.py +++ b/reasoning/satask.py @@ -107,5 +107,6 @@ def get_all_relevant_facts(proposition: object, assumptions: object, db = ClauseDB() visited = discover_facts(subjects, db, adapter, _iteration_limit(iterations)) if use_known_facts: - adapter.add_known_facts(subjects | visited, db) + adapter.add_known_facts(subjects | visited, db, + to_formula(assumptions)) return db diff --git a/reasoning/sathandlers.py b/reasoning/sathandlers.py index 5e6c932..78c1d4a 100644 --- a/reasoning/sathandlers.py +++ b/reasoning/sathandlers.py @@ -2,18 +2,31 @@ This module only uses SymPy to inspect expressions and create predicate atoms. The facts themselves are lightweight formulas from :mod:`reasoning.clauses`. + +Most handlers mirror the tri-state rules in SymPy's ``assumptions.handlers`` +package. :func:`_closed_group` reproduces ``test_closed_group`` (all arguments +share the predicate, or exactly one does not), while the sign and parity +handlers reproduce the corresponding ``Add``/``Mul``/``Pow`` loops. The rules +are emitted as implications so the SAT core can combine them with the imported +known predicate facts. """ from __future__ import annotations from typing import Callable -from sympy.core import Add, Mul, Pow, Number, NumberSymbol -from sympy.core.numbers import ComplexInfinity, ImaginaryUnit +from sympy.core import Add, Mul, Number, NumberSymbol, Pow +from sympy.core.numbers import ( + ComplexInfinity, Exp1, ImaginaryUnit, NegativeOne, Rational, pi, +) +from sympy.core.singleton import S from sympy.functions.elementary.complexes import Abs +from sympy.functions.elementary.exponential import log from sympy.logic.boolalg import And, Or -from sympy.matrices.expressions import MatMul +from sympy.matrices.expressions import MatMul, MatrixExpr -from reasoning.clauses import AND, EQUIVALENT, IMPLIES, NOT, OR +from reasoning.clauses import AND, EQUIVALENT, IMPLIES, NOT, OR, XOR +from reasoning.functionfacts import register_function_facts +from reasoning.matrixfacts import register_matrix_facts from reasoning.numberfacts import number_facts from reasoning.predicates import Q from reasoning.registry import ClassFactRegistry @@ -53,6 +66,47 @@ def _exactlyonearg(predicate: PredicateCall, expr: SymPyExpr) -> object: for index, item in enumerate(predicates))) +def _pow_regular(base: SymPyExpr, exp: SymPyExpr) -> object: + """Guard for rules that treat a power as an ordinary complex number. + + ``0**negative`` is complex infinity and ``0**non-real`` is undefined, so + the base must be nonzero or the exponent real and nonnegative (``0**0`` + is the ordinary value 1). + """ + return OR(NOT(Q.zero(base)), Q.nonnegative(exp)) + + +def _closed_group(predicate: PredicateCall, expr: SymPyExpr) -> list[object]: + """The two facts of SymPy's fuzzy ``test_closed_group`` rule. + + All arguments sharing the predicate makes it hold for the expression; a + single argument that lacks it (with every other argument sharing it) makes + it fail. More than one exception stays unknown. + """ + return [ + IMPLIES(_allargs(predicate, expr), predicate(expr)), + IMPLIES(_exactlyonearg(lambda arg: NOT(predicate(arg)), expr), + NOT(predicate(expr))), + ] + + +def _mul_closed_group(predicate: PredicateCall, expr: SymPyExpr) -> list[object]: + """Like :func:`_closed_group` but guarded by nonzero factors. + + A zero factor makes the product zero (and hence rational, algebraic, and + so on), so the single-exception direction only applies when every factor + is known to be nonzero. + """ + return [ + IMPLIES(_allargs(predicate, expr), predicate(expr)), + IMPLIES( + AND(_allargs(lambda arg: NOT(Q.zero(arg)), expr), + _exactlyonearg(lambda arg: NOT(predicate(arg)), expr)), + NOT(predicate(expr)), + ), + ] + + class_fact_registry = ClassFactRegistry() @@ -60,7 +114,10 @@ def _exactlyonearg(predicate: PredicateCall, expr: SymPyExpr) -> object: def _abs_facts(expr: SymPyExpr) -> list[object]: arg = expr.args[0] return [ - Q.nonnegative(expr), + # Abs is always extended-nonnegative; Abs(oo) == oo is not a finite + # nonnegative number, so the finite statement needs a finite argument. + Q.extended_nonnegative(expr), + IMPLIES(Q.finite(arg), Q.nonnegative(expr)), EQUIVALENT(NOT(Q.zero(arg)), NOT(Q.zero(expr))), IMPLIES(Q.even(arg), Q.even(expr)), IMPLIES(Q.odd(arg), Q.odd(expr)), @@ -68,57 +125,242 @@ def _abs_facts(expr: SymPyExpr) -> list[object]: ] +_ADD_CLOSURE_PREDICATES = ( + Q.real, Q.complex, Q.extended_real, Q.rational, Q.integer, + Q.algebraic, Q.hermitian, Q.antihermitian, Q.finite, +) + + @class_fact_registry.multiregister(Add) -def _add_facts(expr: SymPyExpr) -> list[object]: +def _add_closure_facts(expr: SymPyExpr) -> list[object]: return [ - IMPLIES(_allargs(Q.positive, expr), Q.positive(expr)), - IMPLIES(_allargs(Q.negative, expr), Q.negative(expr)), - IMPLIES(_allargs(Q.real, expr), Q.real(expr)), - IMPLIES(_allargs(Q.rational, expr), Q.rational(expr)), - IMPLIES(_allargs(Q.integer, expr), Q.integer(expr)), - IMPLIES(_exactlyonearg(lambda arg: NOT(Q.integer(arg)), expr), NOT(Q.integer(expr))), + fact + for predicate in _ADD_CLOSURE_PREDICATES + for fact in _closed_group(predicate, expr) ] @class_fact_registry.register(Add) def _add_irrational_fact(expr: SymPyExpr) -> object: return IMPLIES( - _allargs(Q.real, expr), - IMPLIES(_exactlyonearg(Q.irrational, expr), Q.irrational(expr)), + AND(_allargs(Q.real, expr), _exactlyonearg(Q.irrational, expr)), + Q.irrational(expr), + ) + + +@class_fact_registry.register(Add) +def _add_sign_facts(expr: SymPyExpr) -> object: + return AND( + IMPLIES( + AND(Q.real(expr), + _allargs(lambda arg: OR(Q.positive(arg), NOT(Q.negative(arg))), expr), + _anyarg(Q.positive, expr)), + Q.positive(expr)), + IMPLIES( + AND(Q.real(expr), + _allargs(lambda arg: OR(Q.negative(arg), NOT(Q.positive(arg))), expr), + _anyarg(Q.negative, expr)), + Q.negative(expr)), ) +@class_fact_registry.register(Add) +def _add_parity_facts(expr: SymPyExpr) -> object: + odd = [Q.odd(arg) for arg in expr.args] + return AND( + IMPLIES(_allargs(Q.integer, expr), EQUIVALENT(Q.odd(expr), XOR(*odd))), + IMPLIES(_allargs(Q.integer, expr), EQUIVALENT(Q.even(expr), NOT(XOR(*odd)))), + ) + + +@class_fact_registry.register(Add) +def _add_imaginary_facts(expr: SymPyExpr) -> object: + # Imaginary terms can cancel to zero, and zero is not imaginary, so a + # sum of imaginary arguments is only known to be imaginary when it cannot + # cancel; that is not expressible, so only the negative direction is kept. + # It needs the single real argument to be nonzero: a zero real part leaves + # the sum purely imaginary (x + I with x = 0), while a nonzero one cannot + # be cancelled by the imaginary terms. + imaginary_or_nonzero_real = _allargs( + lambda arg: OR(Q.imaginary(arg), AND(Q.real(arg), NOT(Q.zero(arg)))), + expr) + return IMPLIES( + AND(imaginary_or_nonzero_real, _exactlyonearg(Q.real, expr)), + NOT(Q.imaginary(expr)), + ) + + +@class_fact_registry.register(Add) +def _add_nonzero_fact(expr: SymPyExpr) -> object: + return IMPLIES( + OR(_allargs(Q.positive, expr), _allargs(Q.negative, expr)), + Q.nonzero(expr), + ) + + +@class_fact_registry.register(Add) +def _add_commutative_facts(expr: SymPyExpr) -> object: + return AND( + IMPLIES(_allargs(Q.commutative, expr), Q.commutative(expr)), + IMPLIES(_anyarg(lambda arg: NOT(Q.commutative(arg)), expr), + NOT(Q.commutative(expr))), + ) + + +@class_fact_registry.register(Add) +def _add_infinite_fact(expr: SymPyExpr) -> object: + # Same-sign infinite arguments make the sum non-finite even when more + # than one argument is unbounded: all-positive-or-finite sums with a + # ``positive_infinite`` term, and sums whose unbounded terms are all + # non-positive-extended, cannot cancel to a finite value. + positive_group = _allargs( + lambda arg: OR(Q.finite(arg), Q.extended_positive(arg)), expr) + negative_group = _allargs( + lambda arg: OR(Q.finite(arg), NOT(Q.extended_positive(arg))), expr) + return AND( + IMPLIES( + AND(_exactlyonearg(Q.infinite, expr), + _allargs(lambda arg: OR(Q.finite(arg), Q.infinite(arg)), expr)), + Q.infinite(expr), + ), + IMPLIES( + AND(positive_group, _anyarg(Q.positive_infinite, expr)), + NOT(Q.finite(expr)), + ), + IMPLIES( + AND(negative_group, + _anyarg(lambda arg: AND(NOT(Q.finite(arg)), + NOT(Q.extended_positive(arg))), expr)), + NOT(Q.finite(expr)), + ), + ) + + +_MUL_CLOSURE_PREDICATES = (Q.complex, Q.rational, Q.algebraic) + + @class_fact_registry.multiregister(Mul) -def _mul_facts(expr: SymPyExpr) -> list[object]: +def _mul_closure_facts(expr: SymPyExpr) -> list[object]: return [ - EQUIVALENT(Q.zero(expr), _anyarg(Q.zero, expr)), - IMPLIES(_allargs(Q.positive, expr), Q.positive(expr)), - IMPLIES(_allargs(Q.real, expr), Q.real(expr)), - IMPLIES(_allargs(Q.rational, expr), Q.rational(expr)), + fact + for predicate in _MUL_CLOSURE_PREDICATES + for fact in _mul_closed_group(predicate, expr) + ] + + +@class_fact_registry.register(Mul) +def _mul_facts(expr: SymPyExpr) -> object: + # A zero factor makes the product zero only when no other factor is + # infinite: ``oo*0`` is nan. The converse stays exact, so a product can + # still be shown nonzero from its factors. + finite_or_zero = _allargs( + lambda arg: OR(Q.zero(arg), Q.finite(arg)), expr) + return AND( + IMPLIES(AND(_anyarg(Q.zero, expr), finite_or_zero), Q.zero(expr)), + IMPLIES(Q.zero(expr), _anyarg(Q.zero, expr)), IMPLIES(_allargs(Q.integer, expr), Q.integer(expr)), IMPLIES( AND(_allargs(lambda arg: NOT(Q.zero(arg)), expr), _exactlyonearg(lambda arg: NOT(Q.rational(arg)), expr)), NOT(Q.integer(expr)), ), + IMPLIES(_allargs(Q.nonzero, expr), Q.nonzero(expr)), + # A zero factor keeps the product from being a nonzero number: the + # product is zero or, with an infinite factor, nan. + IMPLIES(_anyarg(Q.zero, expr), NOT(Q.nonzero(expr))), + ) + + +@class_fact_registry.register(Mul) +def _mul_commutative_facts(expr: SymPyExpr) -> object: + return AND( IMPLIES(_allargs(Q.commutative, expr), Q.commutative(expr)), - ] + IMPLIES(_anyarg(lambda arg: NOT(Q.commutative(arg)), expr), + NOT(Q.commutative(expr))), + ) @class_fact_registry.register(Mul) -def _mul_prime_fact(expr: SymPyExpr) -> object: - return IMPLIES(_allargs(Q.prime, expr), NOT(Q.prime(expr))) +def _mul_real_facts(expr: SymPyExpr) -> object: + real_or_imaginary = _allargs( + lambda arg: OR(Q.real(arg), Q.imaginary(arg)), expr) + imaginary = [Q.imaginary(arg) for arg in expr.args] + odd = XOR(*imaginary) + return AND( + IMPLIES(AND(real_or_imaginary, NOT(odd)), Q.real(expr)), + IMPLIES(AND(real_or_imaginary, odd), + EQUIVALENT(Q.real(expr), Q.zero(expr))), + IMPLIES(AND(real_or_imaginary, NOT(odd)), NOT(Q.imaginary(expr))), + IMPLIES(AND(real_or_imaginary, odd, NOT(Q.zero(expr))), + Q.imaginary(expr)), + ) @class_fact_registry.register(Mul) -def _mul_imaginary_fact(expr: SymPyExpr) -> object: - return IMPLIES( - AND(_allargs(lambda arg: OR(Q.imaginary(arg), Q.real(arg)), expr), - _allargs(lambda arg: NOT(Q.zero(arg)), expr)), - IMPLIES(_exactlyonearg(Q.imaginary, expr), Q.imaginary(expr)), +def _mul_sign_facts(expr: SymPyExpr) -> object: + sign_known = _allargs( + lambda arg: OR(Q.positive(arg), Q.negative(arg)), expr) + odd = XOR(*(Q.negative(arg) for arg in expr.args)) + return AND( + IMPLIES(sign_known, EQUIVALENT(Q.negative(expr), odd)), + IMPLIES(sign_known, EQUIVALENT(Q.positive(expr), NOT(odd))), ) +@class_fact_registry.register(Mul) +def _mul_hermitian_facts(expr: SymPyExpr) -> object: + hermitian_or_anti = _allargs( + lambda arg: OR(Q.hermitian(arg), Q.antihermitian(arg)), expr) + all_hermitian = _allargs(Q.hermitian, expr) + all_antihermitian = _allargs(Q.antihermitian, expr) + one_antihermitian = _exactlyonearg(Q.antihermitian, expr) + # SymPy's Mul._eval_herm_antiherm only reports a product as *not* having a + # parity-determined hermitian character when it is known to be nonzero: + # zero is both hermitian and antihermitian, so a zero product can satisfy + # either predicate regardless of its factors' parities. + nonzero = NOT(Q.zero(expr)) + facts = [ + IMPLIES(all_hermitian, Q.hermitian(expr)), + IMPLIES(AND(all_hermitian, nonzero), NOT(Q.antihermitian(expr))), + IMPLIES(AND(hermitian_or_anti, one_antihermitian, nonzero), + NOT(Q.hermitian(expr))), + IMPLIES(AND(hermitian_or_anti, one_antihermitian), Q.antihermitian(expr)), + ] + if len(expr.args) % 2 == 0: + facts.append(IMPLIES(all_antihermitian, Q.hermitian(expr))) + facts.append(IMPLIES(AND(all_antihermitian, nonzero), + NOT(Q.antihermitian(expr)))) + else: + facts.append(IMPLIES(AND(all_antihermitian, nonzero), + NOT(Q.hermitian(expr)))) + facts.append(IMPLIES(all_antihermitian, Q.antihermitian(expr))) + return AND(*facts) + + +@class_fact_registry.register(Mul) +def _mul_parity_facts(expr: SymPyExpr) -> object: + if isinstance(expr, MatrixExpr): + return True + integer = _allargs(Q.integer, expr) + all_odd = _allargs(Q.odd, expr) + facts = [ + IMPLIES(AND(integer, _anyarg(Q.even, expr)), Q.even(expr)), + IMPLIES(AND(integer, _allargs(lambda arg: NOT(Q.even(arg)), expr), all_odd), + NOT(Q.even(expr))), + ] + previous: SymPyExpr | None = None + for arg in expr.args: + if previous is not None: + facts.append(IMPLIES(AND(integer, Q.odd(previous + arg)), Q.even(expr))) + previous = arg + return AND(*facts) + + +@class_fact_registry.register(Mul) +def _mul_prime_fact(expr: SymPyExpr) -> object: + return IMPLIES(_allargs(Q.prime, expr), NOT(Q.prime(expr))) + + @class_fact_registry.register(Mul) def _mul_irrational_fact(expr: SymPyExpr) -> object: return IMPLIES( @@ -128,10 +370,60 @@ def _mul_irrational_fact(expr: SymPyExpr) -> object: @class_fact_registry.register(Mul) -def _mul_even_fact(expr: SymPyExpr) -> object: +def _mul_infinite_fact(expr: SymPyExpr) -> object: return IMPLIES( - _allargs(Q.integer, expr), - EQUIVALENT(_anyarg(Q.even, expr), Q.even(expr)), + AND(_anyarg(Q.infinite, expr), + _allargs(lambda arg: OR(Q.finite(arg), Q.infinite(arg)), expr), + _allargs(lambda arg: NOT(Q.zero(arg)), expr)), + Q.infinite(expr), + ) + + +@class_fact_registry.register(Mul) +def _mul_finite_facts(expr: SymPyExpr) -> object: + # Every factor finite makes the product finite. One non-finite factor + # makes it non-finite when every other factor is finite-nonzero; two + # non-finite factors suffice on their own, and a single further factor + # known to be extended-nonzero is tolerated because it cannot be zero. + def nonfinite(arg: SymPyExpr) -> object: + return NOT(Q.finite(arg)) + + def finite_nonzero(arg: SymPyExpr) -> object: + return AND(Q.finite(arg), NOT(Q.zero(arg))) + + def finite_nonzero_or_nonfinite(arg: SymPyExpr) -> object: + return OR(finite_nonzero(arg), nonfinite(arg)) + + args = expr.args + pair_terms = [ + AND(nonfinite(args[first]), nonfinite(args[second]), + *(finite_nonzero(arg) for position, arg in enumerate(args) + if position not in (first, second))) + for first in range(len(args)) + for second in range(first + 1, len(args)) + ] + tolerated_terms = [ + AND(nonfinite(args[first]), nonfinite(args[second]), + Q.extended_nonzero(args[tolerated]), + *(finite_nonzero(arg) for position, arg in enumerate(args) + if position not in (first, second, tolerated))) + for first in range(len(args)) + for second in range(first + 1, len(args)) + for tolerated in range(len(args)) + if tolerated not in (first, second) + ] + return AND( + IMPLIES(_allargs(Q.finite, expr), Q.finite(expr)), + IMPLIES( + AND( + _exactlyonearg(nonfinite, expr), + _allargs(finite_nonzero_or_nonfinite, expr), + ), + NOT(Q.finite(expr)), + ), + IMPLIES(OR(*pair_terms), NOT(Q.finite(expr))), + IMPLIES(_allargs(nonfinite, expr), NOT(Q.finite(expr))), + IMPLIES(OR(*tolerated_terms), NOT(Q.finite(expr))), ) @@ -150,13 +442,264 @@ def _pow_facts(expr: SymPyExpr) -> list[object]: IMPLIES(AND(Q.real(base), Q.even(exp), Q.nonnegative(exp)), Q.nonnegative(expr)), IMPLIES(AND(Q.nonnegative(base), Q.odd(exp), Q.nonnegative(exp)), Q.nonnegative(expr)), IMPLIES(AND(Q.nonpositive(base), Q.odd(exp), Q.nonnegative(exp)), Q.nonpositive(expr)), - EQUIVALENT(Q.zero(expr), AND(Q.zero(base), Q.positive(exp))), + # 0**positive and infinite**negative are zero. The converse only + # holds for a finite positive exponent: ``(1/2)**oo == 0`` and + # ``0**oo == 0`` are zero for other exponent shapes, while a zero + # exponent always gives the nonzero value 1. + IMPLIES(AND(Q.zero(base), Q.positive(exp)), Q.zero(expr)), + IMPLIES(AND(Q.infinite(base), Q.negative(exp)), Q.zero(expr)), + IMPLIES(Q.zero(exp), NOT(Q.zero(expr))), + IMPLIES(AND(Q.zero(expr), Q.positive(exp), Q.finite(exp)), Q.zero(base)), + # A finite nonzero base with a finite exponent gives a nonzero power. + IMPLIES(AND(Q.finite(base), NOT(Q.zero(base)), Q.finite(exp)), + NOT(Q.zero(expr))), + ] + + +@class_fact_registry.register(Pow) +def _pow_commutative_facts(expr: SymPyExpr) -> object: + return AND( + IMPLIES(_allargs(Q.commutative, expr), Q.commutative(expr)), + IMPLIES(_anyarg(lambda arg: NOT(Q.commutative(arg)), expr), + NOT(Q.commutative(expr))), + ) + + +@class_fact_registry.register(Pow) +def _pow_closure_facts(expr: SymPyExpr) -> object: + base, exp = expr.base, expr.exp + defined = OR(NOT(Q.zero(base)), NOT(Q.negative(exp))) + real_power = OR(Q.integer(exp), AND(Q.real(exp), Q.nonnegative(base))) + return AND( + IMPLIES(AND(_allargs(Q.complex, expr), _pow_regular(base, exp)), + Q.complex(expr)), + # A non-complex argument only makes the power non-complex for a + # positive integer exponent: ``oo**0 == 1`` and ``oo**-1 == 0`` are + # complex, and a finite base with an infinite exponent can be zero + # too, while an infinite base to a positive integer stays + # non-complex. + IMPLIES(AND(_exactlyonearg(lambda arg: NOT(Q.complex(arg)), expr), + Q.integer(exp), Q.positive(exp)), + NOT(Q.complex(expr))), + IMPLIES(AND(_allargs(Q.extended_real, expr), defined, real_power), + Q.extended_real(expr)), + ) + + +@class_fact_registry.register(Pow) +def _pow_real_facts(expr: SymPyExpr) -> object: + base, exp = expr.base, expr.exp + facts = [ + IMPLIES(AND(Q.imaginary(base), Q.integer(exp), + OR(Q.zero(exp), NOT(Q.zero(base)))), + EQUIVALENT(Q.real(expr), Q.even(exp))), + IMPLIES(AND(Q.real(base), Q.real(exp), Q.positive(base)), Q.real(expr)), + IMPLIES( + AND(Q.real(base), Q.real(exp), OR(Q.zero(base), Q.integer(exp)), + OR(NOT(Q.zero(base)), NOT(Q.negative(exp)))), + Q.real(expr)), + ] + if (isinstance(exp, Number) and exp < 0 + and not (isinstance(exp, Rational) and exp.q % 2 == 0)): + # 0**negative is complex infinity, which is not real. This is kept + # to concrete negative exponents with an odd denominator (e.g. the -1 + # in ``Pow(x, -1, evaluate=False)``); upstream's positive handler + # stays unknown for a symbolic negative exponent (test_query.py:2001) + # and its even-denominator rule claims 0**(negative half) is real, so + # this must not contradict the EQUIVALENT rule below. + facts.append(IMPLIES(Q.zero(base), NOT(Q.real(expr)))) + if not isinstance(base, Exp1): + facts.append(IMPLIES( + AND(Q.imaginary(exp), NOT(Q.positive(base)), NOT(Q.zero(exp))), + EQUIVALENT(Q.real(expr), Q.imaginary(log(base))))) + coefficient = exp.coeff(S.ImaginaryUnit) + if coefficient: + facts.append(IMPLIES( + AND(Q.imaginary(exp), Q.real(base), Q.rational(base), + Q.nonzero(base), NOT(Q.zero(base - 1)), + NOT(Q.zero(base + 1)), Q.rational(coefficient), + Q.nonzero(coefficient)), + NOT(Q.real(expr)))) + # Port of SymPy's "b**Imaginary -> Real iff log(b) is imaginary" rule + # for positive rational bases: log(base) is irrational, so + # base**(k*I*pi) is real only when k == 0. The exponent-zero case is + # excluded because it gives the real value 1. + facts.append(IMPLIES( + AND(Q.rational(base), Q.positive(base), NOT(Q.zero(base - 1)), + Q.integer(exp / S.ImaginaryUnit / pi), NOT(Q.zero(exp))), + NOT(Q.real(expr)))) + if isinstance(exp, Rational) and exp.q % 2 == 0: + facts.append(IMPLIES( + AND(Q.real(base), Q.real(exp), _pow_regular(base, exp)), + EQUIVALENT(Q.real(expr), Q.nonnegative(base)))) + if isinstance(base, Exp1): + facts.append(IMPLIES( + OR(Q.integer(exp / S.ImaginaryUnit / pi), Q.real(exp)), + Q.real(expr))) + return AND(*facts) + + +@class_fact_registry.register(Pow) +def _pow_sign_facts(expr: SymPyExpr) -> object: + base, exp = expr.base, expr.exp + return AND( + IMPLIES(AND(Q.real(base), Q.positive(base), Q.real(exp)), + NOT(Q.negative(expr))), + IMPLIES(AND(Q.real(base), Q.even(exp), + OR(NOT(Q.zero(base)), Q.positive(exp))), + NOT(Q.negative(expr))), + IMPLIES(AND(Q.real(base), Q.odd(exp)), + EQUIVALENT(Q.negative(expr), Q.negative(base))), + IMPLIES(AND(Q.even(exp), Q.real(base), Q.nonzero(base), + NOT(Q.negative(exp))), + Q.positive(expr)), + IMPLIES(AND(Q.even(exp), Q.real(base), Q.zero(base), Q.positive(exp)), + NOT(Q.positive(expr))), + IMPLIES(AND(Q.positive(base), Q.real(exp)), Q.positive(expr)), + IMPLIES(AND(Q.negative(base), Q.odd(exp)), NOT(Q.positive(expr))), + ) + + +@class_fact_registry.register(Pow) +def _pow_rational_facts(expr: SymPyExpr) -> object: + base, exp = expr.base, expr.exp + facts = [ + IMPLIES(AND(Q.integer(exp), Q.rational(base), NOT(Q.zero(base))), + Q.rational(expr)), + IMPLIES(AND(Q.integer(exp), Q.rational(base), Q.zero(base), Q.positive(exp)), + Q.rational(expr)), + IMPLIES(AND(Q.rational(exp), Q.zero(base), Q.positive(exp)), + Q.rational(expr)), + IMPLIES(AND(Q.rational(exp), Q.eq(base, S.One)), Q.rational(expr)), + IMPLIES(AND(Q.rational(exp), Q.prime(base), NOT(Q.integer(exp))), + NOT(Q.rational(expr))), + # For a transcendental base the exponent-zero value 1 is the only + # rational power, but an infinite base also gives 0 for a negative + # exponent (``oo**-1 == 0``), so the rule needs a finite base. + IMPLIES(AND(Q.integer(exp), NOT(Q.algebraic(base)), Q.finite(base)), + EQUIVALENT(Q.rational(expr), Q.zero(exp))), + ] + if isinstance(exp, NegativeOne): + facts.append(IMPLIES(Q.irrational(base), NOT(Q.rational(expr)))) + if isinstance(base, Exp1): + facts.append(IMPLIES(Q.rational(exp), + EQUIVALENT(Q.rational(expr), Q.zero(exp)))) + return AND(*facts) + + +@class_fact_registry.register(Pow) +def _pow_integer_fact(expr: SymPyExpr) -> object: + return IMPLIES( + AND(Q.integer(expr.base), Q.integer(expr.exp), NOT(Q.negative(expr.exp))), + Q.integer(expr), + ) + + +@class_fact_registry.register(Pow) +def _pow_parity_facts(expr: SymPyExpr) -> object: + base, exp = expr.base, expr.exp + facts = [ + IMPLIES(AND(Q.integer(exp), Q.positive(exp)), + EQUIVALENT(Q.even(expr), Q.even(base))), + IMPLIES(AND(Q.integer(exp), NOT(Q.negative(exp)), Q.odd(base)), + NOT(Q.even(expr))), ] + if isinstance(base, NegativeOne): + facts.append(IMPLIES(Q.integer(exp), Q.odd(expr))) + return AND(*facts) + + +@class_fact_registry.register(Pow) +def _pow_imaginary_facts(expr: SymPyExpr) -> object: + base, exp = expr.base, expr.exp + return AND( + IMPLIES(AND(Q.imaginary(base), Q.integer(exp), Q.odd(exp)), + Q.imaginary(expr)), + IMPLIES(AND(Q.imaginary(base), Q.integer(exp), Q.even(exp)), + NOT(Q.imaginary(expr))), + IMPLIES(AND(Q.imaginary(exp), Q.imaginary(log(base))), + NOT(Q.imaginary(expr))), + IMPLIES(AND(Q.real(base), Q.real(exp), Q.positive(base)), + NOT(Q.imaginary(expr))), + IMPLIES(AND(Q.real(base), Q.real(exp), NOT(Q.rational(exp))), + NOT(Q.imaginary(expr))), + IMPLIES(AND(Q.real(base), Q.real(exp), Q.integer(exp)), + NOT(Q.imaginary(expr))), + IMPLIES(AND(Q.real(base), Q.real(exp), Q.rational(exp), + NOT(Q.integer(exp)), NOT(Q.integer(2 * exp))), + NOT(Q.imaginary(expr))), + IMPLIES(AND(Q.real(base), Q.real(exp), Q.integer(2 * exp), + NOT(Q.integer(exp)), Q.negative(base)), + Q.imaginary(expr)), + IMPLIES(AND(Q.real(base), Q.real(exp), Q.integer(2 * exp), + NOT(Q.integer(exp)), NOT(Q.negative(base))), + NOT(Q.imaginary(expr))), + ) + + +@class_fact_registry.register(Pow) +def _pow_algebraic_facts(expr: SymPyExpr) -> object: + base, exp = expr.base, expr.exp + facts = [ + IMPLIES(AND(Q.algebraic(base), Q.rational(exp), _pow_regular(base, exp)), + Q.algebraic(expr)), + IMPLIES(AND(NOT(Q.algebraic(base)), Q.integer(exp), Q.positive(exp)), + NOT(Q.algebraic(expr))), + ] + if isinstance(base, Exp1): + facts.append(IMPLIES(AND(Q.algebraic(exp)), + EQUIVALENT(Q.algebraic(expr), Q.zero(exp)))) + return AND(*facts) + + +@class_fact_registry.register(Pow) +def _pow_finite_fact(expr: SymPyExpr) -> object: + base, exp = expr.base, expr.exp + return IMPLIES( + AND(Q.finite(base), Q.finite(exp), _pow_regular(base, exp)), + Q.finite(expr), + ) + + +@class_fact_registry.register(Pow) +def _pow_nonzero_fact(expr: SymPyExpr) -> object: + base, exp = expr.base, expr.exp + return IMPLIES( + AND(OR(Q.nonzero(base), Q.zero(exp)), Q.real(expr)), + Q.nonzero(expr), + ) + + +@class_fact_registry.register(Pow) +def _pow_hermitian_fact(expr: SymPyExpr) -> object: + base, exp = expr.base, expr.exp + return IMPLIES( + AND(Q.hermitian(base), Q.integer(exp), _pow_regular(base, exp)), + Q.hermitian(expr)) + + +@class_fact_registry.register(Pow) +def _pow_antihermitian_facts(expr: SymPyExpr) -> object: + base, exp = expr.base, expr.exp + return AND( + IMPLIES(AND(Q.hermitian(base), Q.integer(exp), + OR(NOT(Q.zero(base)), NOT(Q.positive(exp)))), + NOT(Q.antihermitian(expr))), + IMPLIES(AND(Q.antihermitian(base), Q.even(exp), + OR(NOT(Q.zero(base)), NOT(Q.nonnegative(exp)))), + NOT(Q.antihermitian(expr))), + IMPLIES(AND(Q.antihermitian(base), Q.odd(exp), + OR(NOT(Q.zero(base)), NOT(Q.negative(exp)))), + Q.antihermitian(expr)), + ) class_fact_registry.multiregister( Number, NumberSymbol, ImaginaryUnit, ComplexInfinity)(number_facts) +register_function_facts(class_fact_registry) +register_matrix_facts(class_fact_registry) + __all__ = [ 'ClassFactRegistry', 'allargs', 'anyarg', 'exactlyonearg', diff --git a/reasoning/symbolfacts.py b/reasoning/symbolfacts.py new file mode 100644 index 0000000..1427ff0 --- /dev/null +++ b/reasoning/symbolfacts.py @@ -0,0 +1,71 @@ +"""Bridge SymPy's old symbol assumptions into local predicate premises. + +A symbol created with old-assumption keywords carries facts that are only +visible through the old assumptions API, for example:: + + x = Symbol("x", positive=True) + +The reasoning core deliberately never reads those attributes (see +``tools/check_old_assumptions.py``). Instead this module harvests the +*declared* facts through the public new-assumptions entry point +:func:`sympy.assumptions.ask.ask`, which is allowed to consult them, and +returns them as plain ``(predicate name, truth value)`` pairs. The adapter +asserts the pairs as local premises, so the core keeps operating on its own +predicate vocabulary. + +Only the symbol's own declared assumptions are consulted: the upstream query +runs with an empty context, so neither ``global_assumptions`` nor the +assumptions passed to :func:`reasoning.satask.satask` leak into the harvest. +Results are cached per symbol; the cache is keyed by the symbol object, whose +equality and hash include the declared assumptions. + +Matrix symbols are skipped. Their old-assumption answers describe the fact +that a matrix is not a scalar number rather than a declared fact, and matrix +knowledge is assembled by :mod:`reasoning.matrixfacts` instead. +""" +from __future__ import annotations + +from sympy import Q as SymPyQ +from sympy.assumptions.ask import ask +from sympy.core.symbol import Symbol +from sympy.matrices.expressions.matexpr import MatrixSymbol + +# SymPy's scalar old-assumption vocabulary, mirrored by the checker's +# ``ASSUMPTION_NAMES``. These are exactly the keywords a Symbol accepts and +# the predicates whose declared truth values can be harvested. +DECLARED_ASSUMPTIONS = ( + "algebraic", "antihermitian", "commutative", "complex", "composite", + "even", "extended_negative", "extended_nonnegative", + "extended_nonpositive", "extended_nonzero", "extended_positive", + "extended_real", "finite", "hermitian", "imaginary", "infinite", + "integer", "irrational", "negative", "nonnegative", "nonpositive", + "nonzero", "odd", "positive", "prime", "rational", "real", + "transcendental", "zero", +) + +_CACHE: dict[Symbol, tuple[tuple[str, bool], ...]] = {} + + +def declared_assumptions(symbol: Symbol) -> tuple[tuple[str, bool], ...]: + """Return the declared ``(predicate, truth)`` pairs of *symbol*. + + Predicates the old assumptions leave undetermined are omitted. Matrix + symbols have no scalar declarations and return an empty tuple. + """ + if isinstance(symbol, MatrixSymbol): + return () + cached = _CACHE.get(symbol) + if cached is None: + facts: list[tuple[str, bool]] = [] + for name in DECLARED_ASSUMPTIONS: + result = ask(getattr(SymPyQ, name)(symbol), context=()) + if result is True: + facts.append((name, True)) + elif result is False: + facts.append((name, False)) + cached = tuple(facts) + _CACHE[symbol] = cached + return cached + + +__all__ = ["DECLARED_ASSUMPTIONS", "declared_assumptions"] diff --git a/reasoning/sympy_adapter.py b/reasoning/sympy_adapter.py index 66abb2c..f51ccac 100644 --- a/reasoning/sympy_adapter.py +++ b/reasoning/sympy_adapter.py @@ -4,6 +4,8 @@ from sympy import S, Symbol from sympy.assumptions.assume import AppliedPredicate +from sympy.core import Add +from sympy.core.function import Function from sympy.core.kind import NumberKind, UndefinedKind from sympy.core.relational import Eq, Ne, Gt, Lt, Ge, Le from sympy.logic.boolalg import ( @@ -13,13 +15,14 @@ from .clauses import ( ClauseDB, Formula, AND, OR, NOT, IMPLIES, EQUIVALENT, XOR, ITE as IF, - iter_atoms, + assert_formula, iter_atoms, ) from .knownfacts import template as known_facts_template from .predicates import AppliedPredicate as LocalAppliedPredicate from .predicates import Predicate as LocalPredicate from .predicates import Q as LocalQ from .sathandlers import class_fact_registry +from .symbolfacts import declared_assumptions from .sympy_types import SymPyExpr NormalizedFormula: TypeAlias = bool | Formula | LocalAppliedPredicate @@ -113,6 +116,55 @@ def _known_template(numbers: bool, matrices: bool) -> tuple[ return predicates, clauses +def _extra_predicate_facts(subject: SymPyExpr) -> Iterable[object]: + """Predicate-to-predicate facts missing from SymPy's known-fact table. + + These are universal implications, so they are asserted for every subject + alongside the imported known facts. They only mention local predicates + and the opaque subject, so the core stays SymPy-free. + + The ``imaginary -> ~hermitian`` implication is omitted for ``Add`` + subjects. SymPy's closed-group rule infers ``imaginary`` for a sum of + imaginary terms even when the terms cancel to zero, and zero is + hermitian (``x + I`` with ``x = -I``), so the implication is only sound + for subjects whose ``imaginary`` fact cannot come from that rule. + """ + facts: list[object] = [] + if not isinstance(subject, Add): + facts.append( + IMPLIES(LocalQ.imaginary(subject), NOT(LocalQ.hermitian(subject)))) + facts.extend([ + IMPLIES(LocalQ.imaginary(subject), NOT(LocalQ.extended_real(subject))), + IMPLIES(AND(LocalQ.real(subject), LocalQ.nonzero(subject)), + NOT(LocalQ.antihermitian(subject))), + IMPLIES(LocalQ.zero(subject), NOT(LocalQ.nonzero(subject))), + IMPLIES(LocalQ.nonpositive(subject), NOT(LocalQ.positive(subject))), + IMPLIES(LocalQ.nonnegative(subject), NOT(LocalQ.negative(subject))), + IMPLIES(LocalQ.integer(subject), + EQUIVALENT(LocalQ.odd(subject), NOT(LocalQ.even(subject)))), + ]) + if isinstance(subject, Function): + facts.append(IMPLIES( + AND(*(LocalQ.commutative(arg) for arg in subject.args)), + LocalQ.commutative(subject))) + facts.append(IMPLIES( + OR(*(NOT(LocalQ.commutative(arg)) for arg in subject.args)), + NOT(LocalQ.commutative(subject)))) + return facts + + +def _mentioned_predicates(formula: object) -> set[object]: + """Applied predicates that occur in a normalized formula.""" + if isinstance(formula, LocalAppliedPredicate): + return {formula} + if not isinstance(formula, Formula): + return set() + mentioned: set[object] = set() + for arg in formula.args: + mentioned |= _mentioned_predicates(arg) + return mentioned + + class SympyAdapter: def relevance_keys(self, atom: Any) -> set[SymPyExpr]: if isinstance(atom, LocalAppliedPredicate): @@ -135,10 +187,16 @@ def fact_subjects(self, atom: Any) -> Iterable[object]: def facts_for(self, subject: SymPyExpr) -> Iterable[object]: return (to_formula(fact) for fact in class_fact_registry(subject)) - def add_known_facts(self, subjects: Iterable[SymPyExpr], db: ClauseDB) -> None: + def add_known_facts(self, subjects: Iterable[SymPyExpr], db: ClauseDB, + assumptions: object = True) -> None: + subjects = list(subjects) numbers = any(expr.kind in (NumberKind, UndefinedKind) for expr in subjects) matrices = any(expr.kind == MatrixKind(NumberKind) for expr in subjects) predicates, clauses = _known_template(numbers, matrices) + mentioned = _mentioned_predicates(assumptions) + symbols: set[SymPyExpr] = set() + for subject in subjects: + symbols.update(cast("Any", subject).atoms(Symbol)) for subject in subjects: mapping: list[int | None] = [None] + [ db.literal(predicate(subject)) for predicate in predicates @@ -150,3 +208,21 @@ def add_known_facts(self, subjects: Iterable[SymPyExpr], db: ClauseDB) -> None: for lit in clause ] db.add_clause(literals) + for fact in _extra_predicate_facts(subject): + assert_formula(fact, db) + # Declared old-assumption facts are premises for the symbols they are + # declared on. An explicit assumption about the same applied predicate + # wins, so a default such as ``commutative`` stays overridable. + for symbol in symbols: + harvested = declared_assumptions(cast("Any", symbol)) + for name, truth in harvested: + predicate = LocalQ.of(name)(symbol) + if predicate in mentioned: + continue + assert_formula(predicate if truth else NOT(predicate), db) + if not any(name == "commutative" for name, _ in harvested): + # SymPy treats symbols as commutative unless an assumption + # denies it; declared non-commutativity is asserted above. + commutative = LocalQ.commutative(symbol) + if commutative not in mentioned: + assert_formula(commutative, db) diff --git a/reasoning/tests/test_functionfacts.py b/reasoning/tests/test_functionfacts.py new file mode 100644 index 0000000..abca6eb --- /dev/null +++ b/reasoning/tests/test_functionfacts.py @@ -0,0 +1,230 @@ +from __future__ import annotations + +import importlib + +import pytest +from sympy.assumptions.ask import Q +from sympy.core.numbers import I, Rational, pi +from sympy.core.parameters import _exp_is_pow +from sympy.core.singleton import S +from sympy.functions.combinatorial.factorials import factorial +from sympy.functions.elementary.complexes import Abs, im, re, sign +from sympy.functions.elementary.exponential import exp, log +from sympy.functions.elementary.trigonometric import ( + acos, acot, asin, atan, cos, cot, sin, tan, +) +from sympy.abc import p, x, y + +from reasoning.clauses import Formula, iter_atoms +from reasoning.functionfacts import register_function_facts +from reasoning.predicates import AppliedPredicate as LocalAppliedPredicate +from reasoning.predicates import Q as LocalQ +from reasoning.registry import ClassFactRegistry +from reasoning.satask import satask +from reasoning.sathandlers import class_fact_registry + +oo = S.Infinity + + +def test_trigonometric_real_and_finite_facts() -> None: + assert satask(Q.real(sin(x))) is None + assert satask(Q.real(sin(x)), Q.real(x)) is True + assert satask(Q.real(cos(x)), Q.real(x)) is True + + assert satask(Q.finite(sin(x))) is True + assert satask(Q.finite(sin(x)), ~Q.finite(x)) is True + assert satask(Q.finite(cos(x))) is True + assert satask(Q.finite(cos(x)), ~Q.finite(x)) is True + + assert satask(Q.complex(sin(x))) is True + assert satask(Q.complex(cos(x))) is True + + +def test_exponential_facts() -> None: + assert satask(Q.real(exp(x))) is None + assert satask(Q.real(exp(x)), Q.real(x)) is True + assert satask(Q.positive(exp(x)), Q.real(x)) is True + assert satask(~Q.negative(exp(x)), Q.real(x)) is True + assert satask(Q.positive(exp(x)), Q.imaginary(x)) is None + + assert satask(Q.real(exp(2*pi*I, evaluate=False))) is True + assert satask(Q.real(exp(pi*I, evaluate=False))) is True + assert satask(Q.real(exp(pi*I/2, evaluate=False))) is False + assert satask(Q.positive(exp(2*pi*I, evaluate=False))) is True + assert satask(Q.negative(exp(pi*I, evaluate=False))) is True + assert satask(Q.imaginary(exp(pi*I/2, evaluate=False))) is True + assert satask(Q.imaginary(exp(2*pi*I, evaluate=False))) is False + + assert satask(Q.positive(exp(x*pi*I)), Q.even(x)) is True + assert satask(Q.positive(exp(x*pi*I)), Q.odd(x)) is False + assert satask(Q.positive(exp(x*pi*I)), Q.real(x)) is None + + assert satask(Q.complex(exp(x))) is None + assert satask(Q.complex(exp(x)), Q.finite(x)) is True + assert satask(Q.finite(exp(x))) is None + assert satask(Q.finite(exp(x)), Q.finite(x)) is True + assert satask(Q.finite(exp(2))) is True + + assert satask(Q.algebraic(exp(0, evaluate=False))) is True + assert satask(Q.algebraic(exp(7))) is False + assert satask(Q.algebraic(exp(x)), Q.algebraic(x)) is None + assert satask(Q.algebraic(exp(x)), Q.algebraic(x) & Q.nonzero(x)) is False + + +def test_exp_is_pow_representation() -> None: + with _exp_is_pow(True): + assert satask(Q.real(exp(x)), Q.real(x)) is True + assert satask(Q.real(exp(pi*I/2, evaluate=False))) is False + assert satask(Q.positive(exp(x)), Q.real(x)) is True + assert satask(Q.positive(exp(x*pi*I)), Q.even(x)) is True + assert satask(Q.algebraic(exp(x)), Q.algebraic(x)) is None + assert satask(Q.algebraic(exp(x)), + Q.algebraic(x) & Q.nonzero(x)) is False + + +def test_logarithm_facts() -> None: + assert satask(Q.real(log(x)), Q.positive(x)) is True + assert satask(Q.real(log(x)), Q.imaginary(x)) is False + assert satask(Q.real(log(x)), Q.complex(x)) is None + assert satask(Q.real(log(2*I))) is False + assert satask(Q.real(log(I))) is False + + assert satask(Q.positive(log(x)), Q.positive(x)) is None + assert satask(Q.positive(log(x)), Q.negative(x)) is False + assert satask(Q.positive(log(x)), Q.imaginary(x)) is False + assert satask(Q.positive(log(x + 2)), Q.positive(x)) is True + + assert satask(Q.finite(log(x))) is None + assert satask(Q.finite(log(x)), Q.zero(x)) is False + assert satask(Q.finite(log(x)), Q.infinite(x)) is False + assert satask(Q.finite(log(x)), Q.finite(x)) is None + + assert satask(Q.algebraic(log(7))) is False + assert satask(Q.algebraic(log(1, evaluate=False))) is True + + +def test_absolute_value_and_parts_facts() -> None: + assert satask(Q.positive(Abs(x))) is None + assert satask(Q.positive(Abs(x)), Q.positive(x)) is True + assert satask(Q.positive(Abs(x)), Q.negative(x)) is True + assert satask(Q.nonzero(Abs(x)), Q.nonzero(x)) is True + assert satask(Q.complex(Abs(x))) is None + assert satask(Q.complex(Abs(x)), Q.finite(x)) is True + + assert satask(Q.real(re(x))) is None + assert satask(Q.real(im(x))) is None + assert satask(Q.real(re(x)), Q.finite(x)) is True + assert satask(Q.real(im(x)), Q.finite(x)) is True + assert satask(Q.complex(re(x))) is None + assert satask(Q.complex(im(x))) is None + assert satask(Q.complex(re(x)), Q.finite(x)) is True + assert satask(Q.complex(im(x)), Q.finite(x)) is True + assert satask(Q.even(re(x)), Q.even(x)) is True + assert satask(Q.even(im(x)), Q.even(x)) is True + assert satask(Q.even(im(x)), Q.real(x)) is True + + +def test_inverse_trigonometric_facts() -> None: + assert satask(Q.positive(atan(p)), Q.positive(p)) is True + assert satask(Q.positive(atan(p)), Q.negative(p)) is False + assert satask(Q.positive(atan(p)), Q.zero(p)) is False + assert satask(Q.positive(atan(x))) is None + + assert satask(Q.positive(asin(p)), Q.positive(p)) is None + assert satask(Q.positive(asin(Rational(1, 7)))) is True + assert satask(Q.positive(asin(x)), Q.positive(x) & Q.nonpositive(x - 1)) is True + assert satask(Q.positive(asin(x)), Q.negative(x) & Q.nonnegative(x + 1)) is False + + assert satask(Q.positive(acos(p)), Q.positive(p)) is None + assert satask(Q.positive(acos(Rational(1, 7)))) is True + assert satask( + Q.positive(acos(x)), + Q.nonnegative(x + 1) & Q.negative(x - 1)) is True + # acos(1) == 0 is not positive, so the closed interval is undecided. + assert satask( + Q.positive(acos(x)), + Q.nonnegative(x + 1) & Q.nonpositive(x - 1)) is None + assert satask(Q.positive(acos(x)), Q.nonnegative(x - 1)) is None + + assert satask(Q.positive(acot(x)), Q.positive(x)) is True + assert satask(Q.positive(acot(x)), Q.real(x)) is True + assert satask(Q.positive(acot(x)), Q.imaginary(x)) is False + assert satask(Q.positive(acot(x))) is None + + +def test_transcendental_function_arguments() -> None: + for function in (exp, sin, tan, asin, atan, cos): + assert satask(Q.algebraic(function(7))) is False + assert satask(Q.algebraic(function(0, evaluate=False))) is True + assert satask(Q.algebraic(function(x)), Q.algebraic(x)) is None + assert satask( + Q.algebraic(function(x)), Q.algebraic(x) & Q.nonzero(x)) is False + + for function in (log, acos): + assert satask(Q.algebraic(function(7))) is False + assert satask(Q.algebraic(function(1, evaluate=False))) is True + assert satask(Q.algebraic(function(x)), Q.algebraic(x)) is None + assert satask( + Q.algebraic(function(x)), + Q.algebraic(x) & Q.nonzero(x - 1)) is False + + for function in (cot, acot): + assert satask(Q.algebraic(function(7))) is False + assert satask(Q.algebraic(function(x)), Q.algebraic(x)) is False + + +def test_factorial_and_sign_facts() -> None: + assert satask(Q.positive(factorial(x)), Q.integer(x) & Q.positive(x)) is True + assert satask(Q.positive(factorial(x)), Q.integer(x)) is None + # factorial(-1) is complex infinity, so integer alone is not enough. + assert satask(Q.integer(factorial(x)), Q.integer(x)) is None + assert satask(Q.integer(factorial(x)), + Q.integer(x) & Q.nonnegative(x)) is True + + assert satask(Q.finite(sign(x))) is True + assert satask(Q.finite(sign(x)), ~Q.finite(x)) is True + + +def test_issue_5833_and_7246_regressions() -> None: + assert satask(Q.positive(log(x)**2), Q.positive(x)) is None + assert satask(~Q.negative(log(x)**2), Q.positive(x)) is True + + +def test_function_facts_register_local_predicate_formulas() -> None: + expression = log(x) + facts = class_fact_registry(expression) + assert facts + assert all(isinstance(fact, Formula) for fact in facts) + for fact in facts: + for atom in iter_atoms(fact): + assert isinstance(atom, LocalAppliedPredicate) + + registry = ClassFactRegistry() + register_function_facts(registry) + assert registry(expression) == facts + + atoms = [atom for fact in facts for atom in iter_atoms(fact)] + assert all(isinstance(atom, LocalAppliedPredicate) for atom in atoms) + assert LocalQ.real(expression) in atoms + + +def test_add_facts_needed_by_functions() -> None: + assert satask(Q.real(x + I), Q.real(x)) is False + assert satask(Q.complex(x + y), Q.complex(x) & Q.complex(y)) is True + + +def test_function_facts_do_not_query_old_assumptions( + monkeypatch: pytest.MonkeyPatch) -> None: + assumptions = importlib.import_module("sympy.core.assumptions") + + def fail(fact: str, obj: object) -> bool: + raise AssertionError(f"old assumptions queried for {fact!r}") + + monkeypatch.setattr(assumptions, "_ask", fail) + + assert satask(Q.real(exp(x)), Q.real(x)) is True + assert satask(Q.positive(atan(p)), Q.positive(p)) is True + assert satask(Q.algebraic(exp(7))) is False + assert satask(Q.positive(factorial(x)), Q.integer(x) & Q.positive(x)) is True + assert satask(Q.real(sin(x)), Q.real(x)) is True + assert satask(Q.finite(sign(oo))) is True diff --git a/reasoning/tests/test_matrixfacts.py b/reasoning/tests/test_matrixfacts.py new file mode 100644 index 0000000..406e288 --- /dev/null +++ b/reasoning/tests/test_matrixfacts.py @@ -0,0 +1,247 @@ +from __future__ import annotations + +import importlib + +import pytest +from sympy import I, SparseMatrix, Symbol +from sympy.assumptions.ask import Q +from sympy.matrices import Matrix +from sympy.matrices.expressions import ( + BlockDiagMatrix, BlockMatrix, Determinant, Identity, MatrixSymbol, + OneMatrix, Trace, ZeroMatrix, +) +from sympy.matrices.expressions.fourier import DFT + +from reasoning.clauses import Formula, iter_atoms +from reasoning.matrixfacts import register_matrix_facts +from reasoning.predicates import AppliedPredicate as LocalAppliedPredicate +from reasoning.predicates import Q as LocalQ +from reasoning.registry import ClassFactRegistry +from reasoning.satask import satask +from reasoning.sathandlers import class_fact_registry + +X = MatrixSymbol('X', 2, 2) +Y = MatrixSymbol('Y', 2, 3) +Z = MatrixSymbol('Z', 2, 2) +V1 = MatrixSymbol('V1', 2, 1) +A1x1 = MatrixSymbol('A1x1', 1, 1) +C0x0 = MatrixSymbol('C0x0', 0, 0) + + +def test_square_and_invertible_facts() -> None: + assert satask(Q.square(X)) is True + assert satask(Q.square(Y)) is False + assert satask(Q.square(Y*Y.T)) is True + assert satask(Q.square(A1x1)) is True + assert satask(Q.square(C0x0)) is True + + assert satask(Q.invertible(X)) is None + assert satask(Q.invertible(Y)) is False + assert satask(Q.invertible(X*Y), Q.invertible(X)) is False + assert satask(Q.invertible(X*Z), Q.invertible(X)) is None + assert satask(Q.invertible(X*Z), Q.invertible(X) & Q.invertible(Z)) is True + assert satask(Q.invertible(X.T)) is None + assert satask(Q.invertible(X.T), Q.invertible(X)) is True + assert satask(Q.invertible(X.I)) is True + assert satask(Q.invertible(Identity(3))) is True + assert satask(Q.invertible(ZeroMatrix(3, 3))) is False + assert satask(Q.invertible(OneMatrix(1, 1))) is True + assert satask(Q.invertible(OneMatrix(3, 3))) is False + assert satask(Q.invertible(Matrix([[1, 2], [3, 4]]))) is True + assert satask(Q.invertible(Matrix([[1, 2], [3, 6]]))) is False + assert satask(Q.invertible(Matrix([[1, 2, 3], [3, 5, 4]]))) is False + + +def test_symmetric_diagonal_triangular_facts() -> None: + assert satask(Q.symmetric(Y)) is False + assert satask(Q.symmetric(Y*Y.T)) is True + assert satask(Q.symmetric(Y.T*X*Y)) is None + assert satask(Q.symmetric(Y.T*X*Y), Q.symmetric(X)) is True + assert satask(Q.symmetric(X*Z), Q.symmetric(X)) is None + assert satask(Q.symmetric(X*Z), Q.symmetric(X) & Q.symmetric(Z)) is True + assert satask(Q.symmetric(X + Z), Q.symmetric(X) & Q.symmetric(Z)) is True + assert satask(Q.symmetric(X**10), Q.symmetric(X)) is True + assert satask(Q.symmetric(A1x1)) is True + assert satask(Q.symmetric(V1.T*V1)) is True + + assert satask(Q.diagonal(X + Z.T + Identity(2)), + Q.diagonal(X) & Q.diagonal(Z)) is True + assert satask(Q.diagonal(C0x0)) is True + assert satask(Q.diagonal(A1x1)) is True + assert satask(Q.diagonal(OneMatrix(1, 1))) is True + assert satask(Q.diagonal(OneMatrix(3, 3))) is False + assert satask(Q.diagonal(X**3), Q.diagonal(X)) is True + + assert satask(Q.upper_triangular(X + Z.T + Identity(2)), + Q.upper_triangular(X) & Q.lower_triangular(Z)) is True + assert satask(Q.upper_triangular(X*Z.T), + Q.upper_triangular(X) & Q.lower_triangular(Z)) is True + assert satask(Q.lower_triangular(Identity(3))) is True + assert satask(Q.upper_triangular(ZeroMatrix(3, 3))) is True + assert satask(Q.triangular(X), Q.unit_triangular(X)) is True + + +def test_fullrank_and_positive_definite_facts() -> None: + assert satask(Q.fullrank(X**2), Q.fullrank(X)) is True + assert satask(Q.fullrank(X.T), Q.fullrank(X)) is True + assert satask(Q.fullrank(Y)) is None + assert satask(Q.fullrank(Identity(3))) is True + assert satask(Q.fullrank(ZeroMatrix(3, 3))) is False + assert satask(Q.fullrank(OneMatrix(1, 1))) is True + assert satask(Q.fullrank(OneMatrix(3, 3))) is False + assert satask(Q.invertible(X), ~Q.fullrank(X)) is False + + assert satask(Q.positive_definite(X.T), Q.positive_definite(X)) is True + assert satask(Q.positive_definite(X.I), Q.positive_definite(X)) is True + assert satask(Q.positive_definite(Y)) is False + assert satask(Q.positive_definite(X)) is None + assert satask(Q.positive_definite(X + Z), + Q.positive_definite(X) & Q.positive_definite(Z)) is True + assert satask(Q.positive_definite(-X), Q.positive_definite(X)) is None + assert satask(Q.positive_definite(ZeroMatrix(3, 3))) is False + assert satask(Q.positive_definite(OneMatrix(1, 1))) is True + assert satask(Q.positive(X[1, 1]), Q.positive_definite(X)) is True + + +def test_orthogonal_and_unitary_facts() -> None: + assert satask(Q.orthogonal(X.T), Q.orthogonal(X)) is True + assert satask(Q.unitary(X.T), Q.unitary(X)) is True + assert satask(Q.orthogonal(X.I), Q.orthogonal(X)) is True + assert satask(Q.unitary(X**2), Q.unitary(X)) is True + assert satask(Q.orthogonal(Y)) is False + assert satask(Q.unitary(X)) is None + assert satask(Q.unitary(X), ~Q.invertible(X)) is False + assert satask(Q.unitary(X*Z*X), Q.unitary(X) & Q.unitary(Z)) is True + assert satask(Q.unitary(Identity(3))) is True + assert satask(Q.unitary(ZeroMatrix(3, 3))) is False + assert satask(Q.invertible(X), Q.orthogonal(X)) is True + assert satask(Q.orthogonal(X + Z), + Q.orthogonal(X) & Q.orthogonal(Z)) is None + assert satask(Q.unitary(X), Q.orthogonal(X)) is True + assert satask(Q.unitary(DFT(3))) is True + + +def test_element_facts() -> None: + M = MatrixSymbol('M', 4, 4) + assert satask(Q.real(M[1, 2]), Q.real_elements(M)) is True + assert satask(Q.integer(M[1, 2]), Q.integer_elements(M)) is True + assert satask(Q.complex(M[1, 2]), Q.complex_elements(M)) is True + assert satask(Q.integer_elements(Identity(3))) is True + assert satask(Q.integer_elements(ZeroMatrix(3, 3))) is True + assert satask(Q.integer_elements(OneMatrix(3, 3))) is True + assert satask(Q.complex_elements(DFT(3))) is True + + assert satask(Q.integer_elements(M[:, 3]), Q.integer_elements(M)) is True + assert satask(Q.integer_elements(BlockMatrix([[M], [M]])), + Q.integer_elements(M)) is True + assert satask(Q.integer(Determinant(M)), Q.integer_elements(M)) is True + assert satask(Q.integer(Trace(M)), Q.integer_elements(M)) is True + assert satask(Q.real_elements(Trace(M)), Q.real_elements(M)) is True + assert satask(Q.real_elements(M.T), Q.real_elements(M)) is True + assert satask(Q.real_elements(M.I), + Q.real_elements(M) & Q.invertible(M)) is True + assert satask(Q.integer_elements(M.I), Q.integer_elements(M)) is None + + +def test_slice_and_block_facts() -> None: + M = MatrixSymbol('M', 4, 4) + B = M[1:3, 1:3] + C = M[0:3, 1:3] + # A principal submatrix only inherits the predicates that do not need the + # full size. [[0]] is the leading 1x1 slice of the full-rank, invertible, + # orthogonal [[0, 1], [1, 0]], so rank-like predicates stay undecided. + assert satask(Q.symmetric(B), Q.symmetric(M)) is True + assert satask(Q.invertible(B), Q.invertible(M)) is None + assert satask(Q.diagonal(B), Q.diagonal(M)) is True + assert satask(Q.orthogonal(B), Q.orthogonal(M)) is None + assert satask(Q.upper_triangular(B), Q.upper_triangular(M)) is True + assert satask(Q.symmetric(C), Q.symmetric(M)) is None + assert satask(Q.invertible(C), Q.invertible(M)) is None + assert satask(Q.diagonal(C), Q.diagonal(M)) is None + assert satask(Q.orthogonal(C), Q.orthogonal(M)) is None + assert satask(Q.upper_triangular(C), Q.upper_triangular(M)) is None + + assert satask(Q.invertible(BlockMatrix([Identity(3)]))) is True + assert satask(Q.invertible(BlockMatrix([ZeroMatrix(3, 3)]))) is False + assert satask(Q.invertible(BlockDiagMatrix(Identity(3), Identity(5)))) is True + assert satask(Q.invertible( + BlockDiagMatrix(ZeroMatrix(3, 3), Identity(5)))) is False + assert satask(Q.invertible( + BlockDiagMatrix(Identity(3), OneMatrix(5, 5)))) is False + + +def test_trace_and_determinant_positivity() -> None: + M = MatrixSymbol('M', 4, 4) + assert satask(Q.positive(Trace(M)), Q.positive_definite(M)) is True + assert satask(Q.positive(Determinant(M)), Q.positive_definite(M)) is True + + +def test_hermitian_and_antihermitian_facts() -> None: + hermitian = Matrix([[2, 2 + I, 4], [2 - I, 3, I], [4, -I, 1]]) + not_hermitian = Matrix([[2, 2 + I, 4], [2 + I, 3, I], [4, -I, 1]]) + z = Symbol('z') + unknown = Matrix([[2, 2 + I, z], [2 - I, 3, I], [4, -I, 1]]) + assert satask(Q.hermitian(hermitian)) is True + assert satask(Q.hermitian(not_hermitian)) is False + assert satask(Q.hermitian(unknown)) is None + assert satask(Q.hermitian( + SparseMatrix(((25, 15, -5), (15, 18, 0), (-5, 0, 11))))) is True + assert satask(Q.hermitian( + SparseMatrix(((25, 15, -5), (15, I, 0), (-5, 0, 11))))) is False + assert satask(Q.hermitian( + SparseMatrix(((25, 15, -5), (15, z, 0), (-5, 0, 11))))) is None + + antihermitian = Matrix([[0, -2 - I, 0], [2 - I, 0, -I], [0, -I, 0]]) + assert satask(Q.antihermitian(antihermitian)) is True + assert satask(Q.antihermitian(antihermitian**2)) is False + assert satask(Q.antihermitian( + Matrix([[-I, 2 + I, 0], [-2 + I, 0, 2 + I], [0, -2 + I, -I]]))) is True + assert satask(Q.antihermitian( + Matrix([[0, -2 - I, 0], [z, 0, -I], [0, -I, 0]]))) is None + + +def test_matpow_real_elements_with_negative_integer_exponent() -> None: + e = Symbol('e') + assert satask(Q.real_elements(X**e), + Q.real_elements(X) & Q.invertible(X) + & Q.integer(e) & Q.negative(e)) is True + assert satask(Q.real_elements(X**e), Q.real_elements(X)) is None + assert satask(Q.real_elements(X**e), + Q.real_elements(X) & Q.integer(e) & Q.negative(e)) is None + + +def test_matrix_facts_register_local_predicate_formulas() -> None: + expression = Y*Y.T + registry = ClassFactRegistry() + register_matrix_facts(registry) + registered = registry(expression) + assert registered + for fact in registered: + assert isinstance(fact, (Formula, LocalAppliedPredicate)) + for atom in iter_atoms(fact): + assert isinstance(atom, LocalAppliedPredicate) + assert registered <= class_fact_registry(expression) + + atoms = [atom for fact in registered for atom in iter_atoms(fact)] + assert LocalQ.square(expression) in atoms + assert LocalQ.invertible(expression) in atoms + + +def test_matrix_facts_do_not_query_old_assumptions( + monkeypatch: pytest.MonkeyPatch) -> None: + assumptions = importlib.import_module("sympy.core.assumptions") + + def fail(fact: str, obj: object) -> bool: + raise AssertionError(f"old assumptions queried for {fact!r}") + + monkeypatch.setattr(assumptions, "_ask", fail) + + assert satask(Q.square(X)) is True + assert satask(Q.invertible(Y)) is False + assert satask(Q.invertible(Matrix([[1, 2], [3, 4]]))) is True + assert satask(Q.invertible(Matrix([[1, 2], [3, 6]]))) is False + assert satask(Q.symmetric(Y*Y.T)) is True + assert satask(Q.diagonal(X + Z.T + Identity(2)), + Q.diagonal(X) & Q.diagonal(Z)) is True + assert satask(Q.real_elements(X.T), Q.real_elements(X)) is True + assert satask(Q.positive(Trace(X)), Q.positive_definite(X)) is True diff --git a/reasoning/tests/test_matrixfacts_soundness.py b/reasoning/tests/test_matrixfacts_soundness.py new file mode 100644 index 0000000..32d4312 --- /dev/null +++ b/reasoning/tests/test_matrixfacts_soundness.py @@ -0,0 +1,132 @@ +"""Soundness regressions for the structural matrix facts. + +Each guard is paired with the positive rule it must keep, so dropping a guard +or removing the sound direction fails here: + +* ``ZeroMatrix`` only reports the shape-dependent predicates when it is square. +* ``MatPow`` keeps ``integer_elements`` for nonnegative integer exponents and + drops it for negative ones (``diag(2, 1)**-2 == diag(1/4, 1)``). +* ``MatAdd``, ``MatMul`` and ``HadamardProduct`` only close the element + predicates in the positive direction (sums and products can cancel + fractional or imaginary parts). +* A proper principal submatrix inherits the size-independent predicates but + not the rank-like ones: ``[[0]]`` is the leading slice of the full-rank, + invertible, orthogonal ``[[0, 1], [1, 0]]``. A slice covering the whole + parent keeps them. +""" +from __future__ import annotations + +from sympy import Q, Symbol +from sympy.matrices.expressions import ( + HadamardProduct, MatPow, MatrixSlice, MatrixSymbol, ZeroMatrix, +) + +from reasoning.satask import satask + +A = MatrixSymbol("A", 2, 2) +B = MatrixSymbol("B", 2, 2) +M = MatrixSymbol("M", 4, 4) + + +def test_zeromatrix_shape_dependent_predicates_need_square() -> None: + assert satask(Q.square(ZeroMatrix(2, 3))) is False + assert satask(Q.symmetric(ZeroMatrix(2, 3))) is False + assert satask(Q.invertible(ZeroMatrix(2, 3))) is False + assert satask(Q.fullrank(ZeroMatrix(2, 3))) is False + # Entry predicates do not depend on the shape. + assert satask(Q.integer_elements(ZeroMatrix(2, 3))) is True + + +def test_zeromatrix_square_facts_are_kept() -> None: + assert satask(Q.square(ZeroMatrix(3, 3))) is True + assert satask(Q.symmetric(ZeroMatrix(3, 3))) is True + assert satask(Q.diagonal(ZeroMatrix(3, 3))) is True + assert satask(Q.upper_triangular(ZeroMatrix(3, 3))) is True + assert satask(Q.lower_triangular(ZeroMatrix(3, 3))) is True + assert satask(Q.integer_elements(ZeroMatrix(3, 3))) is True + + +def test_matpow_negative_integer_exponent_drops_integer_elements() -> None: + assumptions = Q.integer_elements(A) & Q.invertible(A) + assert satask(Q.integer_elements(MatPow(A, -2)), assumptions) is None + e = Symbol("e") + assert satask(Q.integer_elements(MatPow(A, e)), + assumptions & Q.integer(e) & Q.negative(e)) is None + # Inversion still preserves real and complex elements. + assert satask(Q.real_elements(MatPow(A, -2)), + Q.real_elements(A) & Q.invertible(A)) is True + assert satask(Q.complex_elements(MatPow(A, -2)), + Q.complex_elements(A) & Q.invertible(A)) is True + + +def test_matpow_nonnegative_integer_exponent_keeps_integer_elements() -> None: + e = Symbol("e") + assert satask(Q.integer_elements(MatPow(A, 2)), + Q.integer_elements(A)) is True + assert satask(Q.integer_elements(MatPow(A, e)), + Q.integer_elements(A) & Q.integer(e) + & Q.nonnegative(e)) is True + + +def test_matmul_element_closures_keep_only_positive_direction() -> None: + assert satask(Q.integer_elements(A*B), ~Q.integer_elements(A)) is None + assert satask(Q.real_elements(A*B), + ~Q.real_elements(A) & ~Q.real_elements(B)) is None + assert satask(Q.integer_elements(A*B), + Q.integer_elements(A) & Q.integer_elements(B)) is True + assert satask(Q.real_elements(A*B), + Q.real_elements(A) & Q.real_elements(B)) is True + assert satask(Q.complex_elements(A*B), + Q.complex_elements(A) & Q.complex_elements(B)) is True + + +def test_matadd_element_closures_keep_only_positive_direction() -> None: + assert satask(Q.integer_elements(A + B), + ~Q.integer_elements(A) & ~Q.integer_elements(B)) is None + assert satask(Q.real_elements(A + B), + ~Q.real_elements(A) & ~Q.real_elements(B)) is None + assert satask(Q.integer_elements(A + B), + Q.integer_elements(A) & Q.integer_elements(B)) is True + assert satask(Q.real_elements(A + B), + Q.real_elements(A) & Q.real_elements(B)) is True + assert satask(Q.complex_elements(A + B), + Q.complex_elements(A) & Q.complex_elements(B)) is True + + +def test_hadamard_element_closures_keep_only_positive_direction() -> None: + assert satask(Q.integer_elements(HadamardProduct(A, B)), + ~Q.integer_elements(A)) is None + assert satask(Q.real_elements(HadamardProduct(A, B)), + ~Q.real_elements(A) & ~Q.real_elements(B)) is None + assert satask(Q.integer_elements(HadamardProduct(A, B)), + Q.integer_elements(A) & Q.integer_elements(B)) is True + assert satask(Q.real_elements(HadamardProduct(A, B)), + Q.real_elements(A) & Q.real_elements(B)) is True + + +def test_proper_principal_slice_does_not_inherit_rank_predicates() -> None: + slice_ = MatrixSlice(A, slice(0, 1), slice(0, 1)) + assert satask(Q.fullrank(slice_), Q.fullrank(A)) is None + assert satask(Q.fullrank(slice_), Q.invertible(A)) is None + assert satask(Q.invertible(slice_), Q.invertible(A)) is None + assert satask(Q.unitary(slice_), Q.unitary(A)) is None + assert satask(Q.orthogonal(slice_), Q.orthogonal(A)) is None + + +def test_proper_principal_slice_keeps_size_independent_predicates() -> None: + slice_ = M[1:3, 1:3] + assert satask(Q.symmetric(slice_), Q.symmetric(M)) is True + assert satask(Q.diagonal(slice_), Q.diagonal(M)) is True + assert satask(Q.upper_triangular(slice_), Q.upper_triangular(M)) is True + assert satask(Q.lower_triangular(slice_), Q.lower_triangular(M)) is True + assert satask(Q.positive_definite(slice_), + Q.positive_definite(M)) is True + assert satask(Q.integer_elements(slice_), Q.integer_elements(M)) is True + + +def test_full_parent_slice_keeps_rank_predicates() -> None: + slice_ = MatrixSlice(A, slice(0, 2), slice(0, 2)) + assert satask(Q.fullrank(slice_), Q.fullrank(A)) is True + assert satask(Q.invertible(slice_), Q.invertible(A)) is True + assert satask(Q.unitary(slice_), Q.unitary(A)) is True + assert satask(Q.orthogonal(slice_), Q.orthogonal(A)) is True diff --git a/reasoning/tests/test_satask.py b/reasoning/tests/test_satask.py index 839969f..b45173d 100644 --- a/reasoning/tests/test_satask.py +++ b/reasoning/tests/test_satask.py @@ -41,7 +41,10 @@ def test_satask() -> None: assert satask(Q.positive(x), Q.zero(x)) is False assert satask(Q.real(x), Q.zero(x)) is True assert satask(Q.zero(x), Q.zero(x*y)) is None - assert satask(Q.zero(x*y), Q.zero(x)) + # oo*0 is nan, so the product is only known to be zero when the other + # factor is finite (or zero). + assert satask(Q.zero(x*y), Q.zero(x)) is None + assert satask(Q.zero(x*y), Q.zero(x) & Q.finite(y)) is True def test_zero() -> None: @@ -52,9 +55,12 @@ def test_zero() -> None: """ assert satask(Q.zero(x) | Q.zero(y), Q.zero(x*y)) is True - assert satask(Q.zero(x*y), Q.zero(x) | Q.zero(y)) is True + assert satask(Q.zero(x*y), Q.zero(x) | Q.zero(y)) is None + assert satask(Q.zero(x*y), (Q.zero(x) | Q.zero(y)) & Q.finite(x) + & Q.finite(y)) is True - assert satask(Implies(Q.zero(x), Q.zero(x*y))) is True + assert satask(Implies(Q.zero(x), Q.zero(x*y))) is None + assert satask(Implies(Q.zero(x), Q.zero(x*y)), Q.finite(y)) is True # This one in particular requires computing the fixed-point of the # relevant facts, because going from Q.nonzero(x*y) -> ~Q.zero(x*y) and @@ -84,7 +90,11 @@ def test_zero_pow() -> None: assert satask(Q.zero(x**y), Q.zero(x) & Q.positive(y)) is True assert satask(Q.zero(x**y), Q.nonzero(x) & Q.zero(y)) is False - assert satask(Q.zero(x), Q.zero(x**y)) is True + # (1/2)**oo == 0 and 0**oo == 0, so a zero power only forces a zero base + # for a finite positive exponent. + assert satask(Q.zero(x), Q.zero(x**y)) is None + assert satask(Q.zero(x), Q.zero(x**y) & Q.positive(y) + & Q.finite(y)) is True assert satask(Q.zero(x**y), Q.zero(x)) is None @@ -251,8 +261,13 @@ def test_integer() -> None: def test_abs() -> None: - assert satask(Q.nonnegative(abs(x))) is True - assert satask(Q.positive(abs(x)), ~Q.zero(x)) is True + # Abs(oo) == oo is not a finite nonnegative number. + assert satask(Q.nonnegative(abs(x))) is None + assert satask(Q.nonnegative(abs(x)), Q.finite(x)) is True + # Abs(oo) == oo is not positive in SymPy's finite-positive sense. + assert satask(Q.positive(abs(x)), ~Q.zero(x)) is None + assert satask(Q.positive(abs(x)), + ~Q.zero(x) & Q.finite(x)) is True assert satask(Q.zero(x), ~Q.zero(abs(x))) is False assert satask(Q.zero(x), Q.zero(abs(x))) is True assert satask(Q.nonzero(x), ~Q.zero(abs(x))) is None # x could be complex @@ -342,11 +357,12 @@ def test_pow_pos_neg() -> None: assert satask(Q.negative(x**3), Q.nonpositive(x)) is None assert satask(Q.real(x**3), Q.nonpositive(x)) is True - # If x is zero, x**negative is not real. + # If x is zero, x**negative is not real; for x negative it is positive, + # so x**-2 is never nonpositive either way. assert satask(Q.nonnegative(x**-2), Q.nonpositive(x)) is None - assert satask(Q.nonpositive(x**-2), Q.nonpositive(x)) is None + assert satask(Q.nonpositive(x**-2), Q.nonpositive(x)) is False assert satask(Q.positive(x**-2), Q.nonpositive(x)) is None - assert satask(Q.negative(x**-2), Q.nonpositive(x)) is None + assert satask(Q.negative(x**-2), Q.nonpositive(x)) is False assert satask(Q.real(x**-2), Q.nonpositive(x)) is None # We could deduce things for negative powers if x is nonzero, but it @@ -387,10 +403,16 @@ def test_get_relevant_clsfacts() -> None: decoded = {frozenset((facts.symbols[abs(lit)], lit < 0) for lit in clause) for clause in facts.data} assert decoded == \ - {frozenset({(LocalQ.nonnegative(Abs(x*y)), False)}), + {frozenset({(LocalQ.extended_nonnegative(Abs(x*y)), False)}), + frozenset({(LocalQ.nonnegative(Abs(x*y)), False), + (LocalQ.finite(x*y), True)}), + frozenset({(LocalQ.complex(Abs(x*y)), False), + (LocalQ.finite(x*y), True)}), frozenset({(LocalQ.even(Abs(x*y)), False), (LocalQ.even(x*y), True)}), frozenset({(LocalQ.integer(Abs(x*y)), False), (LocalQ.integer(x*y), True)}), frozenset({(LocalQ.odd(Abs(x*y)), False), (LocalQ.odd(x*y), True)}), + frozenset({(LocalQ.positive(Abs(x*y)), False), (LocalQ.nonzero(x*y), True)}), + frozenset({(LocalQ.nonzero(Abs(x*y)), False), (LocalQ.nonzero(x*y), True)}), frozenset({(LocalQ.zero(Abs(x*y)), False), (LocalQ.zero(x*y), True)}), frozenset({(LocalQ.zero(Abs(x*y)), True), (LocalQ.zero(x*y), False)})} @@ -454,7 +476,7 @@ def test_python_boolean_constants_and_zero_iterations() -> None: raises(ValueError, lambda: satask(True, False)) raises(ValueError, lambda: satask(False, False, early_return=True)) assert satask(Q.nonnegative(Abs(x)), iterations=0) is None - assert satask(Q.nonnegative(Abs(x)), iterations=1) is True + assert satask(Q.nonnegative(Abs(x)), Q.finite(x), iterations=1) is True assert satask(Q.real(x), Q.positive(x), iterations=0) is True raises(ValueError, lambda: satask(Q.real(x), iterations=-1)) diff --git a/reasoning/tests/test_sathandlers.py b/reasoning/tests/test_sathandlers.py index 97c7a42..eee6527 100644 --- a/reasoning/tests/test_sathandlers.py +++ b/reasoning/tests/test_sathandlers.py @@ -51,8 +51,8 @@ def test_abs_facts_contain_no_sympy_boolean_connectives() -> None: expression = Abs(x) facts = class_fact_registry(expression) assert any(isinstance(fact, Formula) for fact in facts) - assert LocalQ.nonnegative(expression) in facts atoms = [atom for fact in facts for atom in iter_atoms(fact)] + assert LocalQ.nonnegative(expression) in atoms for atom in atoms: assert isinstance(atom, LocalAppliedPredicate) assert isinstance(atom.arguments[0], Basic) diff --git a/reasoning/tests/test_soundness_adversarial.py b/reasoning/tests/test_soundness_adversarial.py new file mode 100644 index 0000000..7f59d18 --- /dev/null +++ b/reasoning/tests/test_soundness_adversarial.py @@ -0,0 +1,239 @@ +"""Adversarial soundness tests for the ``satask`` handler facts. + +Every test here encodes a query whose definite ``satask`` answer is contradicted +by a concrete model, found either by ``tools/check_soundness.py`` or by +targeted probing of the handler fact families. The assertions check the +*sound* answer (``None`` when both polarities have a model, otherwise the +direction the models force), so most tests are expected to fail until the +underlying facts are fixed. Models and the value each expression takes are +listed in the comments. + +Sections +-------- +* ``Findings``: definite answers that ``sympy.ask`` does not share, so the + soundness fuzzer reports them without ``--strict``. +* ``Spurious inconsistencies``: satisfiable assumptions that make ``satask`` + raise ``Inconsistent assumptions``. +* ``Matrix facts``: concrete-matrix counterexamples. ``sympy.ask`` does not + decide element predicates of explicit matrices, so these models were checked + by evaluating the substituted expression directly. +* ``Upstream-shared blind spots``: counterexamples that ``sympy.ask`` happens + to share (reported by ``tools/check_soundness.py --strict``) but that a fix + for the two known Pow rules leaves in place. +""" +from __future__ import annotations + +from sympy import ( + Abs, E, I, Pow, Q, Rational, S, acos, exp, factorial, im, log, oo, re, + symbols, +) +from sympy.matrices.expressions import HadamardProduct, MatPow, MatrixSlice +from sympy.matrices.expressions.matexpr import MatrixSymbol +from sympy.matrices.expressions.special import ZeroMatrix + +from reasoning.satask import satask + +x, y, z = symbols("x y z") +n = symbols("n", integer=True) +xi = symbols("xi", infinite=True) +yi = symbols("yi", integer=True, negative=True) +A, B = MatrixSymbol("A", 2, 2), MatrixSymbol("B", 2, 2) + + +# -------------------------------------------------------------------------- +# Findings: sympy.ask does not share the definite answer +# -------------------------------------------------------------------------- + +def test_imaginary_sum_cancellation_does_not_imply_not_real() -> None: + # x = I, y = -I satisfies the assumptions and x + y = 0, which is real, + # extended real, integer, rational, zero, even, nonnegative and + # nonpositive; x = y = I gives 2*I, so the opposite answers are unsound + # too. The ``imaginary(x + y)`` conclusion is upstream-shared, but these + # consequences are not. + assumptions = Q.imaginary(x) & Q.imaginary(y) + assert satask(Q.real(x + y), assumptions) is None + assert satask(Q.extended_real(x + y), assumptions) is None + assert satask(Q.integer(x + y), assumptions) is None + assert satask(Q.rational(x + y), assumptions) is None + assert satask(Q.zero(x + y), assumptions) is None + assert satask(Q.even(x + y), assumptions) is None + assert satask(Q.nonnegative(x + y), assumptions) is None + assert satask(Q.nonpositive(x + y), assumptions) is None + + +def test_acos_positivity_interval_excludes_one() -> None: + # x = 1 satisfies Q.zero(x - 1), and acos(1) == 0 is not positive. + assert satask(Q.positive(acos(x)), Q.zero(x - 1)) is not True + + +def test_factorial_integer_needs_nonnegative_argument() -> None: + # n = -1 gives factorial(-1) == zoo, which is not an integer; n = 2 gives + # 2, so the answer is undetermined. + assert satask(Q.integer(factorial(n)), Q.integer(n)) is None + + +def test_finite_of_unbounded_arguments() -> None: + # x = oo gives exp(x) == oo and re(x) == oo, neither finite; x = -oo gives + # exp(-oo) == 0, and im(zoo) == nan, so those queries are undetermined. + assert satask(Q.finite(exp(x)), Q.infinite(x)) is None + assert satask(Q.finite(E**x), Q.infinite(x)) is None + assert satask(Q.finite(re(x)), Q.infinite(x)) is not True + assert satask(Q.finite(im(x)), Q.infinite(x)) is None + + +def test_infinite_base_negative_integer_exponent_is_zero() -> None: + # xi = oo and yi = -1 satisfy the declared assumptions and xi**yi == 0, + # so the expression is both zero and rational. + assert satask(Q.zero(xi**yi)) is not False + assert satask(Q.rational(xi**yi)) is not False + + +# -------------------------------------------------------------------------- +# Spurious inconsistencies +# -------------------------------------------------------------------------- + +def test_unbounded_function_arguments_do_not_make_assumptions_inconsistent() -> None: + # x = oo satisfies each assumption below (exp(oo) == oo, re(oo) == oo, + # im(zoo) == nan, Abs(oo) == oo, Abs(log(0)) == oo, ...), so raising + # ``Inconsistent assumptions`` is a bug; positive(x) is false for every + # satisfying model because positive implies finite. + assumptions = [ + ~Q.finite(exp(x)), + ~Q.finite(Abs(x)), + ~Q.finite(re(x)), + ~Q.finite(im(x)), + ~Q.finite(Abs(log(x))), + ~Q.complex(exp(x)), + ~Q.complex(Abs(x)), + ~Q.complex(re(x)), + ~Q.real(re(x)), + ] + for assumption in assumptions: + assert satask(Q.positive(x), assumption) is not True + + +def test_infinite_base_zero_exponent_does_not_raise() -> None: + # x = oo, y = 0 satisfies the assumptions and x**y == 1, so the query is + # complex and rational but not zero. ``Q.rational(x**y)`` is provable + # from ``_pow_rational_facts`` while ``_pow_closure_facts`` claims the + # expression is not complex, which makes the whole fact set inconsistent. + assumptions = Q.infinite(x) & Q.zero(y) + assert satask(Q.complex(x**y), assumptions) is not False + assert satask(Q.rational(x**y), assumptions) is not False + assert satask(Q.zero(x**y), assumptions) is False + + +def test_unevaluated_pow_zero_exponent_does_not_raise() -> None: + # oo**0 == 1 and 2**0 == 1. + assert satask(Q.complex(Pow(oo, 0, evaluate=False))) is not False + assert satask(Q.real(Pow(S(2), S.Zero, evaluate=False))) is not False + + +# -------------------------------------------------------------------------- +# Matrix facts +# -------------------------------------------------------------------------- + +def test_zeromatrix_shape_is_not_always_square() -> None: + # ZeroMatrix(2, 3) is not square; sympy.ask agrees. + assert satask(Q.square(ZeroMatrix(2, 3))) is not True + + +def test_matpow_negative_exponent_does_not_preserve_integer_elements() -> None: + # A = [[2, 0], [0, 1]] has integer elements and is invertible, but + # A**-2 == [[1/4, 0], [0, 1]] is not integral. A = I is integral, so the + # answer is undetermined. + assert satask(Q.integer_elements(MatPow(A, -2)), + Q.integer_elements(A) & Q.invertible(A)) is None + + +def test_matmul_element_predicates_are_not_closed_under_negation() -> None: + # A = diag(1/2, 1), B = diag(2, 1): A*B == I has integer elements even + # though A does not, so the negative direction is unsound. + assert satask(Q.integer_elements(A*B), ~Q.integer_elements(A)) is None + # A = i*I, B = [[0, i], [-i, 0]]: A*B == [[0, -1], [1, 0]] is real even + # though neither factor has real elements. + assert satask(Q.real_elements(A*B), + ~Q.real_elements(A) & ~Q.real_elements(B)) is None + + +def test_matadd_element_predicates_are_not_closed_under_negation() -> None: + # A = B = diag(1/2, 1) gives A + B == diag(1, 2), which is integral even + # though neither summand is; A = i*I, B = -i*I gives A + B == 0, real. + assert satask(Q.integer_elements(A + B), + ~Q.integer_elements(A) & ~Q.integer_elements(B)) is None + assert satask(Q.real_elements(A + B), + ~Q.real_elements(A) & ~Q.real_elements(B)) is None + + +def test_hadamard_element_predicates_are_not_closed_under_negation() -> None: + # A = diag(1/2, 1), B = diag(2, 1): the Hadamard product is I, integral + # even though A is not. + assert satask(Q.integer_elements(HadamardProduct(A, B)), + ~Q.integer_elements(A)) is None + + +def test_matrix_slice_does_not_transfer_fullrank() -> None: + # A = [[0, 1], [1, 0]] is full rank, but its leading 1x1 slice [[0]] is + # not; A = I gives a full rank slice, so the answer is undetermined. + slice_ = MatrixSlice(A, slice(0, 1), slice(0, 1)) + assert satask(Q.fullrank(slice_), Q.fullrank(A)) is None + + +def test_antihermitian_pow_with_zero_capable_hermitian_base() -> None: + # z = I gives re(z)**2 == 0, which is antihermitian, while z = 1 gives 1, + # which is not; the local rule claims False. ``sympy.ask`` shares the + # atomic answer, but not the composite one the fuzzer shrank to. + assert satask(Q.antihermitian(re(z)**2)) is None + proposition = ~Q.prime(S.Pi) ^ Q.antihermitian(re(z)**2) + assert satask(proposition, Q.algebraic(0)) is None + + +def test_zero_symbol_pow_does_not_raise() -> None: + # xz**3 == 0 is antihermitian, and 1/xz == zoo is not; the mixed + # hermitian/antihermitian Pow rules make the fact set inconsistent. + xz = symbols("xz", zero=True) + assert satask(Q.antihermitian(xz**3)) is not False + assert satask(Q.antihermitian(1/xz)) is not True + + +# -------------------------------------------------------------------------- +# Zero-base Pow singularities beyond the known 1/x case +# -------------------------------------------------------------------------- + +def test_zero_base_negative_exponent_is_not_algebraic_or_complex() -> None: + # x**(-1) == zoo is neither algebraic nor complex when x = 0, and the same + # holds for a negative exponent or a negative even root. + assert satask(Q.algebraic(x**-1), Q.zero(x)) is not True + assert satask(Q.complex(x**-1), Q.zero(x)) is not True + assert satask(Q.complex(x**y), Q.zero(x) & Q.negative(y)) is not True + assert satask(Q.algebraic(x**Rational(-1, 2)), Q.zero(x)) is not True + + +def test_zero_base_pow_values_are_not_answered_false() -> None: + # 0**oo == 0, 0**(1+I) == 0 and oo**-1 == 0, so none of these is not zero. + assert satask(Q.zero(Pow(S.Zero, oo, evaluate=False))) is not False + assert satask(Q.zero(Pow(S.Zero, 1 + I, evaluate=False))) is not False + assert satask(Q.zero(Pow(oo, -1, evaluate=False))) is not False + + +# -------------------------------------------------------------------------- +# Upstream-shared blind spots: --strict reports these; a narrow Pow guard +# (complex closure + algebraic closure) does not remove any of them. +# -------------------------------------------------------------------------- + +def test_narrow_guard_blind_spots_for_zero_base() -> None: + # 0**I == nan is not complex, real or finite; 0**(-1) == zoo is not + # hermitian. The complex closure guard only excludes real negative + # exponents, and the other rules have no singularity guard at all. + assert satask(Q.complex(x**I), Q.zero(x)) is not True + assert satask(Q.real(x**Rational(-1, 2)), Q.zero(x)) is not True + assert satask(Q.finite(x**I), Q.zero(x)) is not True + assert satask(Q.hermitian(x**-1), Q.zero(x)) is not True + + +def test_narrow_guard_blind_spots_for_mul_and_pow_parity() -> None: + # x = oo, y = 0 gives x*y == nan, which is not zero, and x = 0 with + # x antihermitian gives x**2 == 0, which is antihermitian; both answers + # are shared with sympy.ask. + assert satask(Q.zero(x*y), Q.zero(y) & Q.infinite(x)) is not True + assert satask(Q.antihermitian(x**2), Q.antihermitian(x)) is None diff --git a/reasoning/tests/test_soundness_guards.py b/reasoning/tests/test_soundness_guards.py new file mode 100644 index 0000000..37d4552 --- /dev/null +++ b/reasoning/tests/test_soundness_guards.py @@ -0,0 +1,81 @@ +"""Regression tests for domain guards on the Pow facts. + +``0**negative`` is complex infinity, ``0**0`` is 1, and ``0**non-real`` is +undefined, so a Pow rule that treats the power as an ordinary complex, +algebraic, finite, or hermitian value must either require a nonzero base or +restrict the exponent to the real nonnegative (or otherwise non-singular) +case. Each test below fails on the unguarded handlers. +""" +from __future__ import annotations + +from sympy import I, Q, pi, symbols, sqrt +from sympy.functions.combinatorial.factorials import factorial +from sympy.logic.boolalg import Not + +from reasoning.clauses import iter_atoms +from reasoning.predicates import Q as LocalQ +from reasoning.satask import satask +from reasoning.sathandlers import _pow_real_facts + +x, y, n = symbols('x y n') + + +def test_not_complex_inverse_does_not_force_nonzero() -> None: + # x = 0 satisfies ~Q.complex(1/x) (1/0 is zoo) and makes Q.zero(x) true, + # so a definite False would be unsound. + assert satask(Q.zero(x), Not(Q.complex(1/x))) is None + assert satask(Q.complex(1/x), Q.complex(x)) is None + + +def test_pow_closures_require_regular_base_or_exponent() -> None: + assert satask(Q.zero(x), Not(Q.algebraic(1/x))) is None + assert satask(Q.zero(x), Not(Q.finite(1/x))) is None + assert satask(Q.zero(x), Not(Q.hermitian(1/x))) is None + assert satask(Q.complex(x**y), Q.complex(x) & Q.complex(y)) is None + assert satask(Q.algebraic(x**y), Q.algebraic(x) & Q.rational(y)) is None + assert satask(Q.hermitian(x**y), Q.hermitian(x) & Q.integer(y)) is None + assert satask(Q.finite(x**y), + Q.finite(x) & Q.finite(y) & Q.zero(x)) is None + + +def test_pow_closures_keep_nonzero_base_answers() -> None: + assert satask(Q.complex(1/x), Q.complex(x) & Q.nonzero(x)) is True + assert satask(Q.algebraic(1/x), Q.algebraic(x) & Q.nonzero(x)) is True + assert satask(Q.finite(1/x), Q.finite(x) & Q.nonzero(x)) is True + assert satask(Q.complex(x**y), + Q.complex(x) & Q.complex(y) & Q.nonzero(x)) is True + assert satask(Q.algebraic(x**y), + Q.algebraic(x) & Q.rational(y) & Q.nonzero(x)) is True + assert satask(Q.hermitian(x**y), + Q.hermitian(x) & Q.integer(y) & Q.nonzero(x)) is True + + +def test_pow_real_rules_require_nonzero_exponent() -> None: + atoms = set(iter_atoms(_pow_real_facts(x**y))) + assert LocalQ.zero(y) in atoms + assert satask(Q.real(5**(2*I*pi*n)), Q.integer(n)) is None + assert satask(Q.real(5**(2*I*pi*n)), + Q.integer(n) & Q.nonzero(n)) is False + + +def test_pow_real_and_finite_rules_reject_singular_powers() -> None: + assert satask(Q.real(1/sqrt(x)), Q.real(x) & Q.zero(x)) is None + assert satask(Q.finite(x**I), Q.zero(x)) is None + + +def test_pow_antihermitian_guards() -> None: + assert satask(Q.antihermitian(x**y), + Q.antihermitian(x) & Q.even(y)) is None + assert satask(Q.antihermitian(x**y), + Q.antihermitian(x) & Q.odd(y)) is None + assert satask(Q.antihermitian(x**y), + Q.antihermitian(x) & Q.odd(y) & Not(Q.zero(x))) is True + assert satask(Q.antihermitian(x**y), + Q.antihermitian(x) & Q.even(y) & Not(Q.zero(x))) is False + + +def test_factorial_integer_requires_nonnegative_argument() -> None: + # factorial(-1) is zoo, so integer alone is not enough. + assert satask(Q.integer(factorial(x)), Q.integer(x)) is None + assert satask(Q.integer(factorial(x)), + Q.integer(x) & Q.nonnegative(x)) is True diff --git a/reasoning/tests/test_soundness_scalar_guards.py b/reasoning/tests/test_soundness_scalar_guards.py new file mode 100644 index 0000000..b3d3662 --- /dev/null +++ b/reasoning/tests/test_soundness_scalar_guards.py @@ -0,0 +1,125 @@ +"""Regression tests for the scalar domain guards. + +Each test pins one guard added to ``reasoning/sathandlers.py`` or +``reasoning/functionfacts.py``: a rule that used to ignore a singularity or an +infinite value now either requires the finite/nonzero domain in which it is +sound or is restricted to its sound direction. The second half of every test +checks that the guard did not remove the inference it was meant to keep. +""" +from __future__ import annotations + +from sympy import ( + Abs, E, I, Pow, Q, S, acos, exp, im, log, oo, re, symbols, +) +from sympy.logic.boolalg import Not + +from reasoning.satask import satask + +x, y = symbols('x y') +xi = symbols('xi', infinite=True) +yi = symbols('yi', integer=True, negative=True) + + +def test_imaginary_sum_needs_a_nonzero_real_part() -> None: + # x = I, y = -I gives x + y == 0, so the closed-group rule cannot infer + # imaginary(x + y); antihermitian is the sound closure (zero is + # antihermitian). + assumptions = Q.imaginary(x) & Q.imaginary(y) + assert satask(Q.real(x + y), assumptions) is None + assert satask(Q.imaginary(x + y), assumptions) is None + assert satask(Q.antihermitian(x + y), assumptions) is True + + # The one-real-argument direction needs that argument nonzero: x = 0 + # leaves x + I purely imaginary. + assert satask(Q.imaginary(x + y), Q.imaginary(x) & Q.real(y)) is None + assert satask(Q.imaginary(x + y), + Q.imaginary(x) & Q.real(y) & Q.nonzero(y)) is False + + +def test_acos_positivity_excludes_one() -> None: + # acos(1) == 0 is not positive, so the upper end must be excluded. + assert satask(Q.positive(acos(x)), Q.zero(x - 1)) is not True + assert satask(Q.positive(acos(x)), + Q.nonnegative(x + 1) & Q.negative(x - 1)) is True + + +def test_function_facts_require_finite_arguments() -> None: + # exp(oo) == oo and exp(-oo) == 0, re(oo) == oo, im(zoo) == nan, and + # Abs(oo) == oo. + assert satask(Q.finite(exp(x)), Q.infinite(x)) is None + assert satask(Q.finite(E**x), Q.infinite(x)) is None + assert satask(Q.complex(exp(x)), Q.finite(x)) is True + + assert satask(Q.finite(re(x)), Q.infinite(x)) is not True + assert satask(Q.finite(im(x)), Q.infinite(x)) is None + assert satask(Q.real(re(x)), Q.finite(x)) is True + assert satask(Q.real(im(x)), Q.finite(x)) is True + + assert satask(Q.finite(Abs(x)), ~Q.finite(x)) is not True + assert satask(Q.nonnegative(Abs(x)), Q.finite(x)) is True + assert satask(Q.positive(Abs(x)), ~Q.zero(x)) is None + assert satask(Q.positive(Abs(x)), ~Q.zero(x) & Q.finite(x)) is True + + +def test_unbounded_function_assumptions_are_satisfiable() -> None: + # Every assumption has a model (x = oo, x = zoo, x = 0 for log), so it + # must not raise, and positive(x) is false in those models. + for assumption in ( + ~Q.finite(exp(x)), ~Q.finite(Abs(x)), ~Q.finite(re(x)), + ~Q.finite(im(x)), ~Q.finite(Abs(log(x))), ~Q.complex(exp(x)), + ~Q.complex(Abs(x)), ~Q.complex(re(x)), ~Q.real(re(x))): + assert satask(Q.positive(x), assumption) is not True + + +def test_infinite_base_negative_exponent_is_zero() -> None: + # xi = oo, yi = -1 gives oo**-1 == 0. + assert satask(Q.zero(xi**yi)) is True + assert satask(Q.rational(xi**yi)) is not False + + +def test_pow_zero_exponent_is_one() -> None: + # oo**0 == 1, so the power is complex and rational but not zero. + assumptions = Q.infinite(x) & Q.zero(y) + assert satask(Q.zero(x**y), assumptions) is False + assert satask(Q.complex(x**y), assumptions) is not False + assert satask(Q.rational(x**y), assumptions) is not False + + assert satask(Q.complex(Pow(oo, 0, evaluate=False))) is not False + assert satask(Q.real(Pow(S(2), S.Zero, evaluate=False))) is not False + + +def test_zero_base_pow_values_are_not_refuted() -> None: + # 0**oo == 0, 0**(1+I) == 0 and oo**-1 == 0. + assert satask(Q.zero(Pow(S.Zero, oo, evaluate=False))) is not False + assert satask(Q.zero(Pow(S.Zero, 1 + I, evaluate=False))) is not False + assert satask(Q.zero(Pow(oo, -1, evaluate=False))) is True + + +def test_finite_nonzero_pow_stays_nonzero() -> None: + # The zero equivalence was replaced by guarded directions; the nonzero + # base direction still refutes a zero power. + assert satask(Q.zero(x**y), Q.finite(x) & ~Q.zero(x) & Q.finite(y)) is False + assert satask(Q.zero(x**y), Q.zero(x)) is None + + +def test_zero_product_requires_finite_factors() -> None: + # oo*0 == nan, so a zero factor only makes the product zero when the + # other factors are finite; the converse still refutes a zero factor + # from a nonzero product. + assert satask(Q.zero(x*y), Q.zero(y) & Q.infinite(x)) is None + assert satask(Q.zero(x*y), Q.zero(y) & Q.finite(x)) is True + assert satask(Q.zero(x) | Q.zero(y), Q.nonzero(x*y)) is False + + +def test_pow_antihermitian_parity_needs_nonzero_base() -> None: + # x = 0 is antihermitian and 0**2 == 0 is antihermitian too. + assert satask(Q.antihermitian(x**2), Q.antihermitian(x)) is None + assert satask(Q.antihermitian(x**2), + Q.antihermitian(x) & Not(Q.zero(x))) is False + + +def test_pow_complex_closure_needs_a_positive_integer_exponent() -> None: + # oo**0 == 1 and oo**-1 == 0 are complex, while oo**2 is not. + assert satask(Q.complex(Pow(oo, 0, evaluate=False))) is not False + assert satask(Q.complex(Pow(oo, 2, evaluate=False))) is False + assert satask(Q.complex(x**2), ~Q.complex(x)) is False diff --git a/reasoning/tests/test_soundness_singularities.py b/reasoning/tests/test_soundness_singularities.py new file mode 100644 index 0000000..7c4afe6 --- /dev/null +++ b/reasoning/tests/test_soundness_singularities.py @@ -0,0 +1,90 @@ +"""Soundness regressions for zero-base power singularities. + +The Pow class facts used to close ``complex`` and ``algebraic`` over every +complex/algebraic base and rational exponent: + +* ``complex(base) -> complex(base**exp)`` in ``_pow_closure_facts`` +* ``algebraic(base) & rational(exp) -> algebraic(base**exp)`` in + ``_pow_algebraic_facts`` + +Both are unsound when the base can be zero and the exponent negative: +``0**-1`` is ``zoo``, which is neither complex nor algebraic. The sound +form adds the same definedness guard the ``extended_real`` rule in +``_pow_closure_facts`` already used:: + + OR(NOT(Q.zero(base)), NOT(Q.negative(exp))) + +The counterexample that exposed this is ``satask(Q.zero(x), ~Q.complex(1/x))`` +returning ``False``: the unguarded closure derives ``complex(x) -> complex(1/x)``, +contraposition gives ``~complex(1/x) -> ~complex(x)``, and ``zero -> complex`` +turns that into ``~zero(x)``. ``x = 0`` satisfies the assumption (``1/0 = zoo`` +is not complex) and makes ``Q.zero(x)`` true, so the answer was unsound. + +These tests pin both directions: no inference may pass through the +singularity, and the inference must still fire for zero and positive rational +exponents, where ``0**0 == 1`` and ``0**(p/q) == 0`` are defined. See +``agent-reports/2026-09-22-sathandlers-soundness-root-cause.md``. +""" +from __future__ import annotations + +from sympy import Pow, Q, Rational, symbols + +from reasoning.satask import satask + +x = symbols('x') + + +def test_reciprocal_counterexample_is_not_refuted() -> None: + # Fuzzer counterexample: x = 0 satisfies ~complex(1/x) and is zero. + # The unguarded closure answered False for Q.zero(x). + assert satask(Q.zero(x), ~Q.complex(1/x)) is None + assert satask(Q.zero(x), ~Q.algebraic(1/x)) is None + + +def test_complex_closure_needs_a_defined_power() -> None: + # 0**-1 and 0**-2 are zoo, so the closure must stay undecided for a base + # that may be zero. + assert satask(Q.complex(1/x), Q.complex(x)) is None + assert satask(Q.complex(x**-2), Q.complex(x)) is None + + +def test_algebraic_closure_needs_a_defined_power() -> None: + assert satask(Q.algebraic(1/x), Q.algebraic(x)) is None + assert satask(Q.algebraic(x**-2), Q.algebraic(x)) is None + + +def test_nonnegative_rational_exponents_still_close() -> None: + # 0**(1/2) == 0 and 0**(3/2) == 0 are defined, so the guard must allow + # nonnegative exponents even when the base can be zero. + assert satask(Q.complex(x**Rational(1, 2)), Q.complex(x)) is True + assert satask(Q.complex(x**Rational(3, 2)), Q.complex(x)) is True + assert satask(Q.algebraic(x**Rational(1, 2)), Q.algebraic(x)) is True + assert satask(Q.algebraic(x**Rational(3, 2)), Q.algebraic(x)) is True + + +def test_zero_exponent_is_defined_for_every_base() -> None: + # 0**0 == 1, so an explicit zero exponent must not be treated as a + # singularity. + zero_power = Pow(x, 0, evaluate=False) + assert satask(Q.complex(zero_power), Q.complex(x)) is True + assert satask(Q.algebraic(zero_power), Q.algebraic(x)) is True + + +def test_nonzero_base_still_closes() -> None: + assert satask(Q.complex(1/x), Q.complex(x) & ~Q.zero(x)) is True + assert satask(Q.complex(x**-2), Q.complex(x) & Q.nonzero(x)) is True + assert satask(Q.algebraic(1/x), Q.algebraic(x) & ~Q.zero(x)) is True + assert satask(Q.algebraic(x**-2), Q.algebraic(x) & ~Q.zero(x)) is True + + +def test_nonreal_nonzero_base_still_closes() -> None: + # The guard has to be ``~Q.zero``, not ``Q.nonzero``: an imaginary base + # is not "nonzero" in SymPy's sense, but ``1/I == -I`` is still complex. + assert satask(Q.complex(1/x), Q.imaginary(x) & ~Q.zero(x)) is True + + +def test_finiteness_does_not_leak_through_the_closure() -> None: + # Same chain: complex(1/x) would imply finite(1/x), but 1/0 is zoo, which + # is infinite. These are soundness assertions, not exact answers. + assert satask(Q.finite(1/x), Q.zero(x)) is not True + assert satask(Q.infinite(1/x), Q.zero(x)) is not False diff --git a/reasoning/tests/test_structural_facts.py b/reasoning/tests/test_structural_facts.py new file mode 100644 index 0000000..1c0420e --- /dev/null +++ b/reasoning/tests/test_structural_facts.py @@ -0,0 +1,181 @@ +from __future__ import annotations + +from sympy import I, Pow, Q, oo, pi, sqrt, symbols +from sympy.core.numbers import Rational + +from reasoning.satask import satask + +x, y, z = symbols('x y z') +n = symbols('n') + + +def test_add_closure_facts() -> None: + assert satask(Q.real(x + y), Q.real(x) & Q.real(y)) is True + assert satask(Q.real(x + I), Q.real(x)) is False + assert satask(Q.real(x + y), Q.imaginary(x) & Q.real(y)) is False + + assert satask(Q.complex(x + y), Q.complex(x) & Q.complex(y)) is True + assert satask(Q.complex(x + I), Q.imaginary(x)) is True + + assert satask(Q.rational(x + y), Q.rational(x) & Q.rational(y)) is True + assert satask(Q.rational(x + pi), Q.rational(x)) is False + assert satask(Q.integer(x + y), Q.integer(x) & Q.integer(y)) is True + assert satask(Q.integer(x + Rational(1, 2)), Q.integer(x)) is False + assert satask(Q.algebraic(x + pi), Q.algebraic(x)) is False + + assert satask(Q.hermitian(x + 1), Q.imaginary(x)) is False + assert satask(Q.antihermitian(x + I), Q.imaginary(x)) is True + + +def test_add_sign_parity_and_imaginary_facts() -> None: + assert satask(Q.positive(x + 1), Q.positive(x)) is True + assert satask(Q.negative(x + y), Q.negative(x) & Q.nonpositive(y)) is True + assert satask(Q.nonzero(x + y), Q.positive(x) & Q.positive(y)) is True + + assert satask(Q.odd(x + 1), Q.even(x)) is True + assert satask(Q.even(x + 1), Q.odd(x)) is True + assert satask(Q.odd(x + y), Q.odd(x) & Q.odd(y)) is False + assert satask(Q.odd(x + y + z), Q.odd(x) & Q.odd(y) & Q.even(z)) is False + + # A sum of imaginary terms can cancel to zero and a zero real part leaves + # the sum imaginary, so the closed-group conclusion is guarded. + assert satask(Q.imaginary(x + I), Q.real(x)) is None + assert satask(Q.imaginary(x + I), Q.real(x) & Q.nonzero(x)) is False + assert satask(Q.imaginary(x + I), Q.imaginary(x)) is None + assert satask(Q.imaginary(x + y), Q.imaginary(x) & Q.real(y)) is None + assert satask(Q.imaginary(x + y), + Q.imaginary(x) & Q.real(y) & Q.nonzero(y)) is False + assert satask(Q.imaginary(x + y + z), + Q.real(x) & Q.imaginary(y) & Q.imaginary(z)) is None + assert satask(Q.imaginary(x + y + z), + Q.real(x) & Q.nonzero(x) & Q.imaginary(y) + & Q.imaginary(z)) is False + assert satask(Q.antihermitian(x + I), Q.imaginary(x)) is True + + +def test_mul_sign_and_parity_facts() -> None: + assert satask(Q.negative(-x), Q.positive(x)) is True + assert satask(Q.negative(-x), ~Q.positive(x)) is None + assert satask(Q.positive(2*x), Q.positive(x)) is True + assert satask(Q.negative(x*y), Q.positive(x) & Q.negative(y)) is True + assert satask(Q.negative(x*y), Q.positive(x) & Q.positive(y)) is False + + assert satask(Q.even(x*y), Q.even(x) & Q.odd(y)) is True + assert satask(Q.odd(x*y), Q.odd(x) & Q.odd(y)) is True + assert satask(Q.odd(x*y), Q.even(x) & Q.odd(y)) is False + assert satask(Q.odd(x*(x + y)), Q.integer(x) & Q.odd(y)) is False + assert satask(Q.odd(x*(x + y)), Q.integer(x) & Q.even(y)) is None + + +def test_mul_closure_and_imaginary_facts() -> None: + assert satask(Q.rational(2*x), Q.rational(x)) is True + assert satask(Q.rational(2*x), Q.irrational(x)) is False + assert satask(Q.algebraic(2*pi)) is False + assert satask(Q.complex(x*y), Q.complex(x) & Q.complex(y)) is True + + assert satask(Q.imaginary(I*x), Q.imaginary(x)) is False + assert satask(Q.imaginary(x*y), Q.imaginary(x) & Q.real(y)) is None + assert satask(Q.imaginary(x*y), Q.imaginary(x) & Q.imaginary(y)) is False + assert satask(Q.hermitian(I*x), Q.imaginary(x)) is True + + assert satask(Q.antihermitian(x*y), Q.hermitian(x) & Q.hermitian(y)) is None + assert satask(Q.antihermitian(x*y), + Q.hermitian(x) & Q.hermitian(y) & ~Q.zero(x*y)) is False + assert satask(Q.antihermitian(x*y), + Q.antihermitian(x) & Q.antihermitian(y)) is None + assert satask(Q.antihermitian(x*y), + Q.antihermitian(x) & Q.antihermitian(y) & ~Q.zero(x*y)) is False + + +def test_pow_real_and_rational_facts() -> None: + assert satask(Q.real(x**2), Q.real(x)) is True + assert satask(Q.real(sqrt(x)), Q.negative(x)) is False + assert satask(Q.real(x**y), Q.positive(x) & Q.real(y)) is True + assert satask(Q.real(x**y), Q.imaginary(x) & Q.odd(y)) is False + assert satask(Q.real(x**y), Q.imaginary(x) & Q.even(y)) is True + + # 0**negative with a concrete odd-denominator exponent is complex infinity; + # a symbolic negative exponent stays unknown like upstream's handler. + assert satask(Q.real(Pow(x, -1, evaluate=False)), Q.zero(x)) is False + assert satask(Q.real(Pow(x, Rational(-2, 3), evaluate=False)), + Q.zero(x)) is False + assert satask(Q.real(x**y), Q.zero(x) & Q.negative(y)) is None + assert satask(Q.positive(x**y), Q.zero(x) & Q.negative(y)) is None + + # Positive rational base with a nonzero integer multiple of I*pi as + # exponent is not real, so it cannot be nonzero either. n = 0 gives + # 5**0 = 1, so the exponent must be known nonzero. + assert satask(Q.real(Pow(5, 2*I*pi*n)), Q.integer(n)) is None + assert satask(Q.real(Pow(5, 2*I*pi*n)), + Q.integer(n) & Q.nonzero(n)) is False + assert satask(Q.nonzero(Pow(5, 2*I*pi*n)), + Q.integer(n) & Q.nonzero(n)) is False + + assert satask(Q.rational(1/x), Q.rational(x) & Q.nonzero(x)) is True + assert satask(Q.rational(1/x), Q.irrational(x)) is False + assert satask(Q.rational(1/x), Q.integer(x) & Q.nonzero(x)) is True + + +def test_pow_algebraic_parity_and_imaginary_facts() -> None: + assert satask(Q.algebraic(sqrt(2))) is True + assert satask(Q.algebraic(pi**2)) is False + assert satask(Q.transcendental(pi**2)) is True + + assert satask(Q.odd(x**2), Q.even(x)) is False + assert satask(Q.odd(x**2), Q.odd(x)) is True + assert satask(Q.odd((-1)**x), Q.integer(x)) is True + + assert satask(Q.imaginary(x**y), Q.imaginary(x) & Q.odd(y)) is True + assert satask(Q.imaginary(x**y), Q.imaginary(x) & Q.even(y)) is False + + +def test_commutative_facts() -> None: + assert satask(Q.commutative(x)) is True + assert satask(Q.commutative(x), ~Q.commutative(x)) is False + assert satask(Q.commutative(2*x)) is True + assert satask(Q.commutative(2*x), ~Q.commutative(x)) is False + assert satask(Q.commutative(x + 1)) is True + assert satask(Q.commutative(x + 1), ~Q.commutative(x)) is False + assert satask(Q.commutative(x**2)) is True + assert satask(Q.commutative(x**2), ~Q.commutative(x)) is False + + +def test_extra_predicate_facts() -> None: + assert satask(Q.hermitian(x), Q.imaginary(x)) is False + assert satask(Q.antihermitian(x), Q.real(x) & Q.nonzero(x)) is False + assert satask(Q.extended_real(x), Q.imaginary(x)) is False + assert satask(Q.odd(x), Q.even(x)) is False + assert satask(Q.zero(x), Q.nonzero(x)) is False + assert satask(Q.positive(x), Q.nonpositive(x)) is False + assert satask(Q.negative(x), Q.nonnegative(x)) is False + + +def test_extended_real_and_infinite_facts() -> None: + assert satask(Q.extended_real(x + oo), Q.real(x)) is True + assert satask(Q.infinite(I*oo)) is True + assert satask(Q.infinite(1 + I*oo)) is True + assert satask(Q.infinite(1/x), Q.finite(x) & ~Q.zero(x)) is False + assert satask(Q.positive_infinite(x + I), Q.real(x)) is False + assert satask(Q.positive_infinite(x*I), Q.real(x)) is False + + +def test_mul_finite_extended_nonzero_pattern_is_forced() -> None: + """The global fact base cannot mirror ``FiniteHandler_Mul`` at + ``test_bounded`` line 1108. + + SymPy's handler-local rule returns None for ``finite(x*y*z)`` given + ``~finite(z)`` and extended-nonzero factors, but ``extended_nonzero`` + splits into positive/negative (finite and nonzero) or the two + infinities, so every model of that pattern also satisfies one of the + explicit patterns below. A sound global fact base therefore cannot + answer None there without regressing them. + """ + a = x*y*z + assert satask(Q.finite(a), Q.finite(x) & ~Q.zero(x) & Q.finite(y) + & ~Q.zero(y) & ~Q.finite(z)) is False + assert satask(Q.finite(a), Q.finite(x) & ~Q.zero(x) & ~Q.finite(y) + & ~Q.finite(z)) is False + assert satask(Q.finite(a), ~Q.finite(x) & ~Q.finite(y) + & ~Q.finite(z)) is False + assert satask(Q.finite(a), ~Q.finite(z) & Q.extended_nonzero(x) + & Q.extended_nonzero(y) & Q.extended_nonzero(z)) is False diff --git a/reasoning/tests/test_symbolfacts.py b/reasoning/tests/test_symbolfacts.py new file mode 100644 index 0000000..0fb82f8 --- /dev/null +++ b/reasoning/tests/test_symbolfacts.py @@ -0,0 +1,114 @@ +from __future__ import annotations + +from sympy import Q, MatrixSymbol, Symbol, symbols + +from reasoning.satask import satask +from reasoning.symbolfacts import declared_assumptions + +x, y, z = symbols('x y z') + + +def _symbol(name: str, declarations: dict[str, bool]) -> Symbol: + # Assumption keywords at a call site are reported by the advisory checker + # (tools/check_old_assumptions.py), so tests build declared symbols from a + # mapping instead. + return Symbol(name, **declarations) + + +def _harvested(declarations: dict[str, bool]) -> dict[str, bool]: + return dict(declared_assumptions(_symbol('s', declarations))) + + +def test_declared_assumptions_are_harvested() -> None: + real = _harvested({"real": True}) + assert real["real"] is True + assert real["imaginary"] is False + + imaginary = _harvested({"imaginary": True}) + assert imaginary["imaginary"] is True + assert imaginary["real"] is False + + positive = _harvested({"positive": True}) + assert positive["positive"] is True + assert positive["negative"] is False + + negative = _harvested({"negative": True}) + assert negative["negative"] is True + assert negative["positive"] is False + + assert _harvested({"finite": True})["finite"] is True + + prime = _harvested({"prime": True}) + assert prime["prime"] is True + assert prime["composite"] is False + + composite = _harvested({"composite": True}) + assert composite["composite"] is True + assert composite["prime"] is False + + assert _harvested({"even": True})["odd"] is False + assert _harvested({"odd": True})["even"] is False + + nonzero = _harvested({"nonzero": True}) + assert nonzero["nonzero"] is True + assert nonzero["zero"] is False + assert _harvested({"zero": True})["zero"] is True + + assert _harvested({"integer": True})["integer"] is True + + rational = _harvested({"rational": True}) + assert rational["rational"] is True + assert rational["irrational"] is False + + irrational = _harvested({"irrational": True}) + assert irrational["irrational"] is True + assert irrational["rational"] is False + + assert _harvested({"transcendental": True})["transcendental"] is True + assert _harvested({"commutative": False})["commutative"] is False + + +def test_plain_symbol_harvest_is_commutative_only() -> None: + assert declared_assumptions(Symbol('plain')) == (("commutative", True),) + + +def test_harvest_is_cached_per_symbol() -> None: + first = declared_assumptions(_symbol('cached', {"positive": True})) + assert first is declared_assumptions(_symbol('cached', {"positive": True})) + # Symbols with the same name but different declarations are distinct keys. + assert declared_assumptions(_symbol('cached', {"positive": True})) \ + != declared_assumptions(_symbol('cached', {"negative": True})) + + +def test_satask_uses_declared_assumptions() -> None: + positive = _symbol('p', {"positive": True}) + assert satask(Q.positive(positive)) is True + assert satask(Q.negative(positive)) is False + assert satask(Q.real(positive)) is True + + imaginary = _symbol('i', {"imaginary": True}) + assert satask(Q.imaginary(imaginary)) is True + assert satask(Q.real(imaginary)) is False + + integer = _symbol('n', {"integer": True, "negative": True}) + assert satask(Q.integer(integer)) is True + assert satask(Q.negative(integer)) is True + + noncommutative = _symbol('nc', {"commutative": False}) + assert satask(Q.commutative(noncommutative)) is False + + # Undeclared facts stay undetermined. + assert satask(Q.positive(Symbol('u'))) is None + assert satask(Q.rational(Symbol('u'))) is None + + +def test_explicit_assumptions_override_harvest() -> None: + assert satask(Q.commutative(x), ~Q.commutative(x)) is False + assert satask(Q.commutative(x), Q.commutative(x)) is True + + +def test_matrix_symbols_are_not_harvested() -> None: + matrix = MatrixSymbol('M', 2, 2) + assert declared_assumptions(matrix) == () + # Old assumptions would call a matrix non-real; the bridge stays out. + assert satask(Q.real(matrix)) is None