Allow the simplifier to use facts in its can_prove() predicates. - #9400

Open

mcourteaux wants to merge 58 commits into

mainfrom

mcourteaux/can-prove-facts

Commits on Sep 5, 2026

Let can_prove predicates use the simplifier's known facts

mcourteaux
and
claude
committed
1399d13
Make fact lookup aware of comparison direction and strictness

mcourteaux
and
claude
committed
6fa6d43
Don't re-enter fact-driven rewrite rules from inside a can_prove

mcourteaux
and
claude
committed
bd22e41
Express the can_prove re-entry guard as a depth limit

mcourteaux
and
claude
committed
0c73eea
Add a non-recursive known_true predicate for rewrite rules

mcourteaux
and
claude
committed
e6866e7
Fix parenthesis of Simplify_Div.
mcourteaux
committed
6664311
Guard against can_prove recursion at its source

mcourteaux
and
claude
committed
8af31a8
Fall back to fact lookup at the can_prove depth cap

mcourteaux
and
claude
committed
abda89a
Use a direct fact lookup at the can_prove depth cap, not a tree walk

mcourteaux
and
claude
committed
f7bf9b7
Answer ordering questions from constant bounds on differences, not IR

mcourteaux
and
claude
committed
1e9eb9c
Lower the can_prove depth limit to two

mcourteaux
and
claude
committed
d82b2ec
Let known_difference reason without facts

mcourteaux
and
claude
committed
01a2108
Test the fact-free reasoning in known_difference

mcourteaux
and
claude
committed
9ace36b
Reject known_difference candidates on a summary before comparing Exprs

mcourteaux
and
claude
committed
5b7483c
Gate the difference rules on the difference table, not on any fact

mcourteaux
and
claude
committed
74e1d92
Reject a difference lookup against the whole table in one test

mcourteaux
and
claude
committed
185ead5
Key same-type pairs by their kind rather than collapsing them onto one bit

mcourteaux
and
claude
committed
260cc16
Don't order a min or max from the condition of an if

mcourteaux
and
claude
committed
1915e46
Order a min or max from an if's condition only once regions are derived

mcourteaux
and
claude
committed
fa3b132

Commits on Sep 6, 2026

Review fixes: type-gate the structural bound, and drop what nothing reads

mcourteaux
and
claude
committed
9e825cd
Gate every fact on the phase, not just the ones from ifs

mcourteaux
and
claude
committed
8be980b
Test that a wrapping type is not ordered from a fact about a sum

mcourteaux
and
claude
committed
0d05e92
Add a cheap hash to Expr nodes for fast IREquality pre-checks

abadams
and
claude
committed
ee827e9
Pack the Expr hash into IRNode::node_type's spare bits

abadams
and
claude
committed
bc1eaee
Fix set_hash on big-endian: shift the high-quality bits into place

abadams
and
claude
committed
3b7820c

Commits on Sep 7, 2026

Fix (U)IntImm hash discarding small values entirely

abadams
and
claude
committed
566b056
Tighten IRNode hash comment

abadams
and
claude
committed
2b43673
Merge remote-tracking branch 'origin/abadams/expr_hash' into mcourteaux/can-prove-facts
mcourteaux
committed
739cae9
Use the Expr hash as the difference filter's summary

mcourteaux
and
claude
committed
ef93203
Read the Expr hash directly rather than through a wrapper

mcourteaux
and
claude
committed
6169aca
Drop the cached hashes from KnownBound

mcourteaux
and
claude
committed
9b0688c

Commits on Sep 9, 2026

Commits on Sep 10, 2026

Commits on Sep 11, 2026

Merge branch 'main' into mcourteaux/can-prove-facts
mcourteaux
committed
618e337
Merge branch 'main' into mcourteaux/can-prove-facts
mcourteaux
committed
6b59abd
cleanup
mcourteaux
committed
e7169af

Commits on Sep 26, 2026

Merge DiffBound into LinearDiffBound and remove KnownTrue

mcourteaux
and
claude
committed
0c32b78
Drop the cap on peeled division denominators

mcourteaux
and
claude
committed
db62c66
Round in solve_scaled_bound with div_imp

mcourteaux
and
claude
committed
c986d1c
Leave INT64_MIN / -1 open in solve_scaled_bound

mcourteaux
and
claude
committed
d6ec950

Commits on Sep 27, 2026

Require simplified facts in learn_true/learn_false

mcourteaux
and
claude
committed
71222e3
Test that an RDom's where clause doesn't remove a clamp on its index

mcourteaux
and
claude
committed
0ee94a7
Test a where clause on a scaled reduction variable

mcourteaux
and
claude
committed
9fd71f0
Name the indices an if condition bounds, and drop ScopedRegionsInferred

mcourteaux
and
claude
committed
0fe2aaf
Keep the original if condition outside the one on the named index

mcourteaux
and
claude
committed
7712b54
Test that a where clause on a compound index still bounds its parts

mcourteaux
and
claude
committed
d19a4a0
Rename the test to what it checks: bounds of a compound index from a where clause

mcourteaux
and
claude
committed
0c7cc7e
Merge branch 'main' into mcourteaux/can-prove-facts
mcourteaux
committed
f992206
Chain the difference facts per bucket instead of scanning the whole table

mcourteaux
and
claude
committed
070b53a
Skip the work a difference query can't use

mcourteaux
and
claude
committed
90ff0d0
Decide a min or max from one difference lookup, not two rules

mcourteaux
and
claude
committed
f518796

Commits on Sep 28, 2026

Branch explicitly around the gcd for a unit coefficient

mcourteaux
and
claude
committed
dd88275
Merge branch 'main' into mcourteaux/can-prove-facts
mcourteaux
committed
2f35b21
Name a select inside an index too

mcourteaux
and
claude
committed
da02d71