Function rewrite_model

pub fn rewrite_model<'a>(
    model: &Model,
    rule_sets: &Vec<&'a RuleSet<'a>>,
) -> Result<Model, RewriteError>

Rewrites the given model by applying a set of rules to all its constraints.

This function iteratively applies transformations to the model’s constraints using the specified rule sets. It returns a modified version of the model with all applicable rules applied, ensuring that any side-effects such as updates to the symbol table and top-level constraints are properly reflected in the returned model.

Parameters

• model: A reference to the Model to be rewritten. The function will clone this model to produce a modified version.
• rule_sets: A vector of references to RuleSets that define the rules to be applied to the model’s constraints. Each RuleSet is expected to contain a collection of rules that can transform one or more constraints within the model. The lifetime parameter 'a ensures that the rules’ references are valid for the duration of the function execution.

Returns

• Ok(Model): If successful, it returns a modified copy of the Model after all applicable rules have been applied. This new model includes any side-effects such as updates to the symbol table or modifications to the constraints.
• Err(RewriteError): If an error occurs during rule application (e.g., invalid rules or failed constraints), it returns a RewriteError with details about the failure.

Side-Effects

• When the model is rewritten, related data structures such as the symbol table (which tracks variable names and types) or other top-level constraints may also be updated to reflect these changes. These updates are applied to the returned model, ensuring that all related components stay consistent and aligned with the changes made during the rewrite.
• The function collects statistics about the rewriting process, including the number of rule applications and the total runtime of the rewriter. These statistics are then stored in the model’s context for performance monitoring and analysis.

Example

• Using rewrite_model with the Expression a + min(x, y)

  Initial expression: a + min(x, y) A model containing the expression is created. The variables of the model are represented by a SymbolTable and contain a,x,y. The contraints of the initail model is the expression itself.

  After getting the rules by their priorities and getting additional statistics the while loop of single interations is executed. Details for this process can be found in [rewrite_iteration] documentation.

  The loop is exited only when no more rules can be applied, when rewrite_iteration returns None and [while let Some(step) = None] occurs

  Will result in side effects ((d<=x ^ d<=y) being the [new_top] and the model will now be a conjuction of that and (a+d) Rewritten expression: ((a + d) ^ (d<=x ^ d<=y))

Performance Considerations

• The function checks if optimizations are enabled before applying rules, which may affect the performance of the rewriting process.
• Depending on the size of the model and the number of rules, the rewriting process might take a significant amount of time. Use the statistics collected (rewriter_run_time and rewriter_rule_application_attempts) to monitor and optimize performance.

Panics

• This function may panic if the model’s context is unavailable or if there is an issue with locking the context.

See Also

• get_rule_priorities: Retrieves the priorities for the given rules.
• [rewrite_iteration]: Executes a single iteration of rewriting the model using the specified rules.