Module rules 

Public rewrite-rule engine: Rule, RuleSet, Bindings, RewriteOpts, Step. Public rewrite-rule engine and simplification extensions on Ex.

This module is the user-facing half of the pattern-matching engine in crate::transforms::pattern (crate-internal). It provides:

• Rule — a named rewrite rule built from two expressions (lhs → rhs) whose symbols ending in _ are wildcards, optionally with a guard closure or a closure-computed right-hand side;
• RuleSet — an ordered collection of rules;
• Bindings — the wildcard → sub-expression map handed to guards;
• RewriteOpts / RewriteStrategy — traversal configuration;
• Step — one entry of a rewrite / simplification trace;
• the Ex methods rewrite, rewrite_once, rewrite_traced, rewrite_with, simplify_with_rules, simplify_traced and subs_algebraic.

Wildcard conventions

Name	Meaning
a_	matches any single sub-expression (in Add/Mul: one term, or the remaining terms if it is the last plain wildcard)
rest__	sequence wildcard: absorbs the remaining terms of an Add/Mul, possibly none (binding to 0/1)

Add and Mul are matched associatively and commutatively with a bounded backtracking search (see the internal MATCH_BUDGET constant); every other node is matched structurally.

Example

use symplex::prelude::*;
use symplex::macros::{Rule, RuleSet};

let ctx = Context::new();
let (x, a) = (ctx.symbol("x"), ctx.symbol("a_"));
// sin(a_)^2 → 1 - cos(a_)^2
let rule = Rule::new("sin_sq", &a.sin().powi(2), &(1 - &a.cos().powi(2)));
let rules = RuleSet::from_rules(vec![rule]);
let expr = &x.sin().powi(2) + 3;
let result = expr.rewrite(&rules);
assert_eq!(format!("{result}"), "-cos(x)^2 + 4");

Structs

Bindings

Wildcard bindings produced by a successful match: wildcard name → matched sub-expression.

RewriteOpts

Options controlling Ex::rewrite_with.

Rule

A named rewrite rule lhs → rhs over expressions of one Context.

RuleSet

An ordered collection of Rules.

Step

One step of a rewrite or simplification trace.

Enums

RewriteStrategy

Traversal order used by Ex::rewrite_with.

Constants

MAX_REWRITE_OPS

Tree-size ceiling for rewriting: a pass whose result has more than this many nodes (counted with multiplicity, i.e. the unfolded tree rather than the hash-consed DAG) stops the fixpoint iteration and the previous result is kept. Guards against rules that grow expressions without bound.