Struct RuleEffect 

#[non_exhaustive]
pub struct RuleEffect {
    pub new_expression: Expression,
    pub new_top: Vec<Expression>,
    pub symbols: SymbolTable,
    pub new_clauses: Vec<CnfClause>,
    /* private fields */
}

Represents the result of applying a rule to an expression within a model.

A RuleEffect encapsulates the changes made to a model during a rule application. It includes a new expression to replace the original one, an optional top-level constraint to be added to the model, and any updates to the model’s symbol table.

This struct allows for representing side-effects of rule applications, ensuring that all modifications, including symbol table expansions and additional constraints, are accounted for and can be applied to the model consistently.

Fields

• new_expression: The updated Expression that replaces the original one after applying the rule.
• new_top: An additional top-level Vec<Expression> constraint that should be added to the model. If no top-level constraint is needed, this field can be set to an empty vector Vec::new().
• symbols: A SymbolTable containing any new symbol definitions or modifications to be added to the model’s symbol table. If no symbols are modified, this field can be set to an empty symbol table.

Usage

A RuleEffect can be created using one of the provided constructors:

• RuleEffect::new: Creates an effect with a new expression, top-level constraint, and symbol modifications.
• RuleEffect::pure: Creates an effect with only a new expression and no side-effects on the symbol table or constraints.
• RuleEffect::with_symbols: Creates an effect with a new expression and symbol table modifications, but no top-level constraint.
• RuleEffect::with_top: Creates an effect with a new expression and a top-level constraint, but no symbol table modifications.
• RuleEffect::cnf: Creates an effect with a new expression, cnf clauses and symbol modifications, but no top-level constraints.

The apply method allows for applying the changes represented by the RuleEffect to a Model.

Example

// Need to add an example

See Also

• ApplicationResult: Represents the result of applying a rule, which may either be a RuleEffect or an ApplicationError.
• Model: The structure to which the RuleEffect changes are applied.

Fields (Non-exhaustive)

Non-exhaustive structs could have additional fields added in future. Therefore, non-exhaustive structs cannot be constructed in external crates using the traditional Struct { .. } syntax; cannot be matched against without a wildcard ..; and struct update syntax will not work.

new_expression: Expression

new_top: Vec<Expression>

symbols: SymbolTable

new_clauses: Vec<CnfClause>

Implementations

impl RuleEffect

pub fn new( new_expression: Expression, new_top: Vec<Expression>, symbols: SymbolTable, ) -> Self

pub fn pure(new_expression: Expression) -> Self

Represents an effect with no side effects on the model.

pub fn with_symbols(new_expression: Expression, symbols: SymbolTable) -> Self

Represents an effect that also modifies the symbol table.

pub fn with_top(new_expression: Expression, new_top: Vec<Expression>) -> Self

Represents an effect that also adds a top-level constraint to the model.

pub fn cnf( new_expression: Expression, new_clauses: Vec<CnfClause>, symbols: SymbolTable, ) -> Self

Represents an effect that also adds clauses to the model.

pub fn deferred( materialise: impl Fn(&SymbolTable) -> RuleEffect + Send + Sync + 'static, ) -> Self

Defers constructing a concrete effect until the rewriter chooses to apply this rule.

This is intended for rule effects that allocate fresh names or otherwise depend on global model state. Applicability checks can return a deferred effect without consuming those effects; the rewriter calls RuleEffect::materialise only for the selected rule.

pub fn materialise(self, symbols: &SymbolTable) -> Self

Returns the concrete effect for the current symbol table.

This consumes the selected effect: cloning a concrete effect can duplicate its expression, top-level constraints, clauses, and speculative symbol table. Before returning, the symbol snapshot is reduced to the bindings that the effect actually changes.

pub fn with_declaration_updates( self, updates: impl IntoIterator<Item = (DeclarationPtr, DeclarationKind)>, ) -> Self

Adds declaration replacements that are committed only if this effect is selected.

pub fn updated_declaration_names(&self) -> impl Iterator<Item = Name> + '_

Iterates over the names changed by deferred declaration updates.

pub fn apply(self, model: &mut Model)

Applies side-effects (e.g. symbol table updates)

pub fn added_symbols(&self, initial_symbols: &SymbolTable) -> BTreeSet<Name>

Gets symbols added by this effect.

Walks this effect’s own symbols rather than diffing two whole tables. The rewriter asks this once per applied rule, and most effects are pure, so diffing made every rewrite cost a clone and a sort of the entire model symbol table.

pub fn changed_symbols( &self, initial_symbols: &SymbolTable, ) -> Vec<(Name, DeclarationPtr, DeclarationPtr)>

Gets symbols changed by this effect.

Returns a list of tuples of (name, domain before effect, domain after effect), ordered by name.

Walks this effect’s symbols for the same reason as RuleEffect::added_symbols: a symbol can only have changed if this effect carries its new value.

Trait Implementations

impl Clone for RuleEffect

fn clone(&self) -> RuleEffect

Returns a duplicate of the value.

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl Debug for RuleEffect

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.

Layout

Note: Most layout information is completely unstable and may even differ between compilations. The only exception is types with certain repr(...) attributes. Please see the Rust Reference's “Type Layout” chapter for details on type layout guarantees.

Size: 352 bytes