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

Open

mcourteaux wants to merge 19 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

Navigation Menu

Uh oh!

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

Allow the simplifier to use facts in its can_prove() predicates.#9400
mcourteaux wants to merge 19 commits into
mainfrom
mcourteaux/can-prove-facts

Commits on Sep 5, 2026

Let can_prove predicates use the simplifier's known facts

Make fact lookup aware of comparison direction and strictness

Don't re-enter fact-driven rewrite rules from inside a can_prove

Express the can_prove re-entry guard as a depth limit

Add a non-recursive known_true predicate for rewrite rules

Fix parenthesis of Simplify_Div.

Guard against can_prove recursion at its source

Fall back to fact lookup at the can_prove depth cap

Use a direct fact lookup at the can_prove depth cap, not a tree walk

Answer ordering questions from constant bounds on differences, not IR

Lower the can_prove depth limit to two

Let known_difference reason without facts

Test the fact-free reasoning in known_difference

Reject known_difference candidates on a summary before comparing Exprs

Gate the difference rules on the difference table, not on any fact

Reject a difference lookup against the whole table in one test

Key same-type pairs by their kind rather than collapsing them onto one bit

Don't order a min or max from the condition of an if

Order a min or max from an if's condition only once regions are derived