// Consequently, if A contains B and both are rewriteable at the same priority, A must be selected
// scheduled when no enclosing expression rewrites first. The rewriter does not require old full-scan
// A selected rule always replaces the focused expression. It may also append top-level constraints,
// append CNF clauses, add symbol declarations, or change existing symbol declarations (for example
// by tightening a domain). Rewriting a value-letting surface writes the replacement expression back
// to that symbol declaration. Symbol changes invalidate rule-application context caches; changed
fn record_worklist_stale_pop(&mut self, mode: ScheduledMode, reason: WorklistStaleReason) {
self.candidates_with_arena(config, arena.expression(node_id), Some((arena, node_id)))
self.has_candidates_with_arena(config, arena.expression(node_id), Some((arena, node_id)))
/// A rewrite normalises its own replacement subtree straight away and records its ancestors here.
/// Ancestors waiting to have their rules re-checked, held until the worklist is about to move on
/// Rewriting a child can make a higher-priority rule apply to an expression enclosing it, so those
/// ancestors have to be re-checked before any lower-priority work runs. Collecting them up while
/// the current priority finishes means a shared wide root is visited once per priority instead of
let nodes = deferred_nodes_in_bottom_up_order(std::mem::take(&mut self.nodes), surfaces);
self.enqueue_children_at_level(context, node_id, level, dirty_trace.as_deref_mut());
/// `is_value` is false for a matrix's index domains, which describe which entries exist rather
fn domain_needs_abstract_repr_at(domain: &crate::ast::DomainPtr, is_value: bool) -> bool {
/// Rewrites a model by applying rules in priority order, trying enclosing expressions before their
let (mut surfaces, mut value_letting_surfaces) = build_worklist_surfaces(submodel, arena);
if !rule_group.has_candidates_at_node(ctx.config, &surfaces[surface_index].arena, node_id) {
let selected = choose_rule_result_index(results.iter().map(|(result, _, _, _, _)| result));
/// Nodes are handled deepest first, so each parent is rebuilt once from children that are already
/// copying the whole matrix/`and`/root chain above it. The surfaces that changed go back on the
// Cache each rarely needed path once. Reconstructing paths inside the comparison closure would
/// This is the initial half of the evaluator normalisation hook. Evaluation is a privileged pure
/// simplification rather than an ordinary rule: before normal rule scheduling starts, each surface
/// is normalised bottom-up so parent evaluators can assume already-normal children. Comprehensions
fn normalise_evaluators_bottom_up(arena: &mut ExpressionArena, dirty_trace: &mut DirtyTrace) {
normalise_evaluator_node_to_fixpoint_without_ancestor_sync(arena, node_id, dirty_trace);
/// exception: after an ordinary rule changes a subtree, local full/partial evaluation is allowed to
/// fire immediately at that node and then at each ancestor because such simplification is always
/// `child_id` must be a direct child of the arena root. Sibling constraints are left untouched.
/// would clone every sibling constraint and re-import the whole model into the arena, which this
fn write_worklist_surfaces_to_model(submodel: &mut Model, surfaces: &[RewriteSurface]) {
fn move_worklist_surfaces_to_model(submodel: &mut Model, surfaces: Vec<RewriteSurface>) {
let written = write_value_letting_surface_to_model_without_refresh(submodel, name, arena);
/// The rewrite pass treats comprehensions as atomic here; comprehension expansion is responsible
fn rule_matches_self_discriminant(rule_data: &RuleData<'_>, expr_discriminant: usize) -> bool {
matches!(prefilter, RulePrefilter::Variant(discriminant) if *discriminant == expr_discriminant)
/// Direct children are walked rather than read off the arena's cached child discriminants, which