Module symbolic_assumptions 

Simplification under assumptions (Gap analysis §3.3) — CAS simplifications that are only valid when the simplifier knows a variable’s sign / nonzero-ness.

Plain simplify must stay sound for all real inputs, so it cannot turn √(x²) into x (that is |x|), or ln(a·b) into ln a + ln b (the log laws need positivity). This module takes an explicit Assumptions set (x > 0, n ≠ 0, …) and applies exactly those rewrites the assumptions license — and no others. Every rewrite is gated on a proof of the needed sign from the assumptions (see Assumptions::is_positive etc.); when the sign cannot be established the node is left untouched (fail-closed: never an unsound rewrite).

Structs

Assumptions

A set of per-variable sign assumptions used to license otherwise-unsound rewrites.

Enums

Sign

A sign / domain assumption about a single variable.

Functions

simplify_with_assumptions

Simplify expr using assumption-gated rewrites on top of the plain (always-sound) simplify. Applied to a bounded fixpoint. Rewrites performed (each only when the assumptions prove the side condition):