Simplification API

Apply the algebraic rewrite-rule simplifier.

exprExpr or DerivedResult

assumptionsAssumptions, optional

Explicit assumption context to authorize condition-gated rewrites (e.g. sqrt(x**2) -> x under x > 0). When omitted, falls back to the active alkahest.context(assumptions=...) (see _context.active_assumptions()), if any. Static Domain.Positive / Domain.NonZero symbol domains in expr always authorize their rewrites regardless of this argument.

DerivedResult

>>> p = ExprPool(); x = p.symbol("x")
>>> simplify(x + 0).value   # x

alkahest.simplify_with(expr, rules) — simplify using a custom rule list.

rules is a list of RewriteRule objects (e.g. from make_rule). The default arithmetic rules are NOT included; combine with alkahest.default_rules() if needed.

Trigonometric identity simplifier.

exprExpr or DerivedResult

DerivedResult

Logarithm / exponential simplifier.

Branch-cut identities such as exp(log(x)) → x and log(x) + log(y) → log(x*y) require positivity facts from assumptions (an Assumptions context) or symbols declared with Domain.Positive. Safe identities log(exp(x)) → x and exp(x)*exp(y) → exp(x+y) always apply.

exprExpr or DerivedResult

assumptionsAssumptions, optional

When omitted, falls back to the active alkahest.context(assumptions=...), if any (see _context.active_assumptions()).

DerivedResult

Expand-then-simplify.

exprExpr or DerivedResult

DerivedResult

UserWarning

When a power of a sum was left unexpanded because its expansion is too large (the derivation then carries an expand_pow_limit_reached step naming it). Powers whose expansion is small are always expanded: simplify_expanded((x+1)**13) is the 14-term polynomial.

Decide whether expr is identically zero on its symbols' domains.

exprExpr or DerivedResult

assumptionsAssumptions, optional

Extra facts (x > 0, x != 0, …). Defaults to the active alkahest.context(assumptions=...), if any. Symbol domains (Domain.Positive, Domain.Integer, …) always apply.

bool or None

True only when proved by exact symbolic reasoning; False when proved non-zero (exactly, or by a rigorous Arb ball at an admissible point); None when undetermined. Use equals() to see the provenance (status, method, evidence).

>>> p = ExprPool(); x = p.symbol("x")
>>> is_zero(sin(x)**2 + cos(x)**2 - 1)
True
>>> is_zero(sin(x) - x)
False

Decide whether a == b identically, with provenance.

Runs the is_zero() procedure on a - b.

a, bExpr, DerivedResult or number

assumptionsAssumptions, optional

As for is_zero().

ZeroTest

.value is True / False / None; .status and .method say how it was reached. status == "probably_zero" means numerically indistinguishable but not proved (value is None).

>>> p = ExprPool(); x = p.symbol("x")
>>> equals(exp(2*x), exp(x)**2).value
True

alkahest.to_real_form(expr, assumptions=None) -> Expr

Rewrite expr into an equal expression with no imaginary unit and no square root of a negative quantity: exp(±i·θ) pairs become cos/sin, exp(a ± √(−b)) with b > 0 becomes e^a·(cos √b ± i sin √b), cosh(i·x) becomes cos x, and perfect squares leave square roots (√(c²·k) → |c|·√k, → c·√k once c ≥ 0 is known). The real part is returned only when the imaginary part is proved identically zero; otherwise expr comes back unchanged. Free symbols must be real (any domain but Complex).

expr

the expression to rewrite.

assumptions

optional Assumptions (k > 0, a >= 0…); the active alkahest.context(assumptions=...) and symbol domains always apply.

Expr

an equal expression, real-valued where it could be proved so.

>>> p = ExprPool(); a = p.symbol("a")
>>> to_real_form(sqrt(4*a**2))
(2 * abs(a))

alkahest.rewrite_piecewise(expr) -> Expr

Lower abs, sign, heaviside, min and max to piecewise(), everywhere in expr.

abs(g) becomes Piecewise((g >= 0, g); -g); min(a, b) becomes Piecewise((a <= b, a); b) and max(a, b) the >= form (more than two arguments fold to the right); sign and heaviside use their registry values at 0 (0 and 1/2). The lowered form agrees with the original at every point. floor/ceil/round have infinitely many pieces and are left alone. integrate() applies this itself.

>>> p = ExprPool(); x = p.symbol("x")
>>> rewrite_piecewise(abs(x))
Piecewise((x >= 0, x); -x)

Simplify an expression using a recursive fork-join traversal.

Requires the parallel feature at build time; without it this falls back to sequential simplify(), so the call is always available. Check alkahest.capabilities()["features"]["parallel"] to tell which you have.

Fork-join keeps each subtree on one worker, which suits wide expressions — a large sum or product of independent terms. For deep, narrow expressions prefer simplify_redex(), or let simplify_auto() choose.

The result matches simplify() exactly. The derivation log may vary in order between runs, because two workers can reach the same node concurrently; simplify_redex() does not have that property.

Simplify an expression by scheduling independent rewrites level by level.

Requires the parallel feature at build time; without it this falls back to sequential simplify(), so the call is always available.

Nodes are bucketed by height, so every node at a given height is rewritten concurrently regardless of its type. That suits deep expressions, where simplify_par() finds no wide node to fork on and ends up running essentially sequentially. It also visits each node exactly once, so unlike simplify_par() the derivation log is deterministic — identical across runs and across CPU counts.

The result matches simplify() exactly.

Simplify in parallel, choosing the strategy from the expression's shape.

Requires the parallel feature at build time; without it this falls back to sequential simplify(), so the call is always available.

Dispatches to simplify_par() for wide expressions when enough CPU cores are available, and to simplify_redex() otherwise. Use simplify_strategy() to see which it would pick without running it.

This is the one to reach for if you do not want to think about shape. The result matches simplify() exactly.

Report which strategy simplify_auto() would use for expr.

Returns "fork_join" (simplify_par()), "level_scheduled" (simplify_redex()), or "sequential" when the extension was built without the parallel feature and both parallel entry points fall back to simplify().

The answer depends on the number of worker threads available as well as the expression, so it can differ between machines.

Collect like terms in a sum.

exprExpr or DerivedResult

DerivedResult

Expand and collect expr as a polynomial in vars.

Substitute variables in expr according to mapping.

exprExpr or DerivedResult

Source expression. DerivedResult is auto-coerced to .value.

mappingdict[Expr, Expr | DerivedResult | int | float]

Substitution map. Values (and keys that are symbols) may be Expr, DerivedResult, or Python int/float (coerced into the expression pool).

Expr

>>> p = ExprPool(); x = p.symbol("x")
>>> subs(x**2, {x: 3})         # int values coerced — OK
>>> r = diff(x**2, x)          # DerivedResult
>>> subs(r, {x: 1})            # DerivedResult first arg — OK

E-graph equality-saturation simplifier.

exprExpr or DerivedResult

DerivedResult

Simplify using the e-graph backend with a custom [EgraphConfig].

Use this when you want to disable specific rule sets (e.g. trig or log/exp rules) or tune the phase iteration counts.

alkahest.make_rule(lhs, rhs, sequence=None) — create a rewrite rule from two expressions.

Symbols whose names start with a lower-case letter in lhs are wildcards that bind to any sub-expression; the same names in rhs are replaced by the bound values.

sequence lists noncommutative symbols of lhs that are sequence wildcards: in make_rule(A*X*B, ..., sequence=[X]) the symbol X matches any contiguous run of noncommutative factors between A and B (possibly empty), and X in rhs is replaced by that run. Matching is leftmost, and each sequence wildcard takes the shortest run that lets the rest match. A sequence rule only fires inside a product of at least two noncommutative factors, and applies through simplify_with (not nc_rewrite). Raises NcError E-NC-009 for a malformed pattern.

Example:

rule = alkahest.make_rule(a*b + a*c, a*(b + c))  # factoring rule
result = alkahest.simplify_with(expr, [rule])

alkahest.match_pattern(pattern_expr, expr) -> list[dict[str, Expr]]

Find all AC-aware matches of pattern_expr anywhere in expr. Each match is returned as a dict mapping wildcard names to matched sub-expressions. Wildcards are symbols whose names start with a lower-case letter. Set wildcards=False to treat every symbol as a literal (e.g. when the pattern is a single variable like x).

Opaque handle to a rewrite rule created by make_rule().

Partial-fraction decomposition of expr as a rational function of var.

Decomposes p(x)/q(x) into poly_part + Σ A_ij(x) / f_i(x)**j where the f_i are the distinct ℚ-irreducible factors of the denominator and deg A_ij < deg f_i.

exprExpr or DerivedResult

A rational function of var. DerivedResult is coerced to .value.

varExpr

The variable to decompose in.

Expr

ValueError

If expr is not a rational function of var, or denominator factorization fails.

Decomposition is over ℚ: irreducible quadratics (and higher) are kept intact, not split into complex/algebraic linear factors.

>>> p = ExprPool(); x = p.symbol("x")
>>> apart(1 / (x**2 - 1), x)   # 1/(2(x-1)) - 1/(2(x+1))

Combine expr over a common denominator and cancel common polynomial factors.

Non-polynomial sub-expressions (e.g. sin(x) or symbols not in vars) are treated as opaque generators. Accepts DerivedResult as expr.

If vars is omitted, free symbols of expr are inferred.

Combine expr over a single common denominator (alias of cancel()).

If vars is omitted, free symbols of expr are inferred.

Trigonometric normal-form simplifier.

Runs the full algebraic core with bounded polynomial expansion plus the sin/cos-polynomial trig identities (argument-sign normalization and the Pythagorean identity, including its multi-angle case), driven to a fixed point. Unlike simplify_trig() (identities only, no expansion), this composes product expansion, constant folding, like-term collection, and Pythagorean reduction in a single call.

The headline use case is verifying orthogonality of a rotation (direction-cosine) matrix: every entry of R.T @ R - I collapses to 0. It reduces in the sin/cos monomial basis and does not introduce compound-angle (sin(2u), sin(u+v), …) forms. This bundle is heavier than simplify() and is opt-in.

exprExpr or DerivedResult

DerivedResult

Simplify with default rules plus orthogonal Clifford anticommutation on cliff_e1, cliff_e2.

Simplify with default arithmetic rules plus the Pauli product table on sx, sy, sz.

Python-visible configuration for the e-graph simplifier.

All arguments are keyword-only with the same defaults as the Rust EgraphConfig.

shrink_iters

explore_iters

const_fold_iters

node_limit

iter_limit

include_trig_rules

include_log_exp_rules

disjoint_schedule

Verdict of equals() (or of a zero test) with its provenance.

valuebool or None

True (proved equal / zero), False (proved different / non-zero) or None (undetermined).

statusstr

"proved_zero", "proved_nonzero", "probably_zero" or "unknown".

methodstr

"simplify", "rational_normal_form", "arb_ball", "arb_sampling", "complex_f64_sampling" or "none".

evidencelist[str]

Human-readable sample points and enclosures, when numeric.

bool(test) is the proved verdict; it raises ValueError when the verdict is None so that an undecided comparison cannot silently read as "different" in an if.

proved: bool