Err(_) => false, // Assume optimizations are disabled if the environment variable is not set
/// 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.
/// - `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 [`RuleSet`]s 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
/// - `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
/// - `Err(RewriteError)`: If an error occurs during rule application (e.g., invalid rules or failed constraints),
/// - 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
/// A model containing the expression is created. The variables of the model are represented by a SymbolTable and contain a,x,y.
/// After getting the rules by their priorities and getting additional statistics the while loop of single interations is executed.
/// 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)
/// - The function checks if optimizations are enabled before applying rules, which may affect the performance
/// - 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`)
/// - This function may panic if the model's context is unavailable or if there is an issue with locking the context.
/// - [`rewrite_iteration`]: Executes a single iteration of rewriting the model using the specified rules.
/// Attempts to apply a set of rules to the given expression and its sub-expressions in the model.
/// This function recursively traverses the provided expression, applying any applicable rules from the given set.
/// If a rule is successfully applied to the expression or any of its sub-expressions, it returns a `Reduction`
/// containing the new expression, modified top-level constraints, and any changes to symbols. If no rules can be
/// - `expression`: A reference to the [`Expression`] to be rewritten. This is the main expression that the function
/// - `model`: A reference to the [`Model`] that provides context and additional constraints for evaluating the rules.
/// - `rules`: A vector of references to [`Rule`]s that define the transformations to apply to the expression.
/// - `apply_optimizations`: A boolean flag that indicates whether optimization checks should be applied during the rewriting process.
/// If `true`, the function skips already "clean" (fully optimized or processed) expressions and marks them accordingly
/// - `stats`: A mutable reference to [`RewriterStats`] to collect statistics about the rule application process, such as
/// - `Some(<Reduction>)`: A [`Reduction`] containing the new expression and any associated modifications if a rule was applied
/// - If `apply_optimizations` is enabled, the function will skip "clean" expressions and mark successfully rewritten
/// expressions as "dirty". This is done to avoid unnecessary recomputation of expressions that have already been
/// Initially [`if apply_optimizations && expression.is_clean()`] is not true yet since intially our expression is dirty.
/// After calling function [`children`] on the expression a vector of sub-expression [`[a, min(x, y)]`] is returned.
/// The function iterates through the vector of the children from the top expression and calls itself.
/// [rewrite_iteration] on on the child [`a`] returns None, but on [`min(x, y)`] returns a [`Reduction`] object [`red`].
/// - d is added to the SymbolTable and the variables field is updated in the model. new_top is the side effects: (d<=x ^ d<=y)
/// - [`sub[1] = red.new_expression`] - Updates the second element in the vector of sub-expressions from [`min(x, y)`] to [`d`]
/// Since a child expression [`min(x, y)`] was rewritten to d, the parent expression [`a + min(x, y)`] is updated with the new child [`a+d`].
/// The condition [`Some(step) = Some(new reduction)`] in the while loop in [`rewrite_model`] is met -> side effects are applied.
/// No more rules in our example can apply to the modified model -> mark all the children as clean and return a pure [`Reduction`].
/// On the last execution of rewrite_iteration condition [`apply_optimizations && expression.is_clean()`] is met, [`None`] is returned.
/// - This function works recursively, meaning it traverses all sub-expressions within the given `expression` to find the
/// first rule that can be applied. If a rule is applied, it immediately returns the modified expression and stops
if let Some(red) = rewrite_iteration(&sub[i], model, rules, apply_optimizations, stats) {
/// This function iterates through the provided rules and attempts to apply each rule to the given `expression`.
/// If a rule is successfully applied, it creates a [`RuleResult`] containing the original rule and the resulting
/// [`Reduction`]. The statistics (`stats`) are updated to reflect the number of rule application attempts and successful
/// The function does not modify the provided `expression` directly. Instead, it collects all applicable rule results
/// into a vector, which can then be used for further processing or selection (e.g., with [`choose_rewrite`]).
/// - `expression`: A reference to the [`Expression`] that will be evaluated against the given rules. This is the main
/// target for rule transformations and is expected to remain unchanged during the function execution.
/// - `model`: A reference to the [`Model`] that provides context for rule evaluation, such as constraints and symbols.
/// - `rules`: A vector of references to [`Rule`]s that define the transformations to be applied to the expression.
/// - `stats`: A mutable reference to [`RewriterStats`] used to track statistics about rule application, such as
/// - A `Vec<RuleResult>` containing all rule applications that were successful. Each element in the vector represents
/// - The function updates the provided `stats` with the number of rule application attempts and successful applications.
/// - Debug or trace logging may be performed to track which rules were applicable or not for a given expression.
/// - This function does not modify the input `expression` or `model` directly. The returned `RuleResult` vector
/// provides information about successful transformations, allowing the caller to decide how to process them.
/// - The function performs independent rule applications. If rules have dependencies or should be applied in a
/// - [`choose_rewrite`]: Chooses a single reduction from the rule results provided by `apply_all_rules`.
// assert!(!red.new_expression.children().iter().any(|c| c.is_clean()), "Rule that caused assertion to fail: {:?}", rule.name);
// assert!(!red.new_expression.children().iter().any(|c| c.children().iter().any(|c| c.is_clean())));
/// This function selects a reduction from the provided `RuleResult` list, prioritizing the first rule
/// that successfully transforms the expression. This strategy can be modified in the future to incorporate
/// more complex selection criteria, such as prioritizing rules based on cost, complexity, or other heuristic metrics.
/// The function also checks the priorities of all the applicable rules and detects if there are multiple rules of the same proirity
/// - `results`: A slice of [`RuleResult`] containing potential rule applications to be considered. Each element
/// represents a rule that was successfully applied to the expression, along with the resulting transformation.
/// - `Some(<Reduction>)`: Returns a [`Reduction`] representing the first rule's application if there is at least one
/// - `None`: If no rule applications are available in the `results` slice (i.e., it is empty), it returns `None`.
fn choose_rewrite(results: &[RuleResult], initial_expression: &Expression) -> Option<Reduction> {
/// In the case where there are multiple rules of the same prioriy, a bug! is thrown listing all those duplicates.
/// Otherwise, if there are multiple rules applicable but they all have different priorities, a warning message is dispalyed.
/// - `rules`: a vector of [`Rule`] containing all the applicable rules and their metadata for a specific expression.
//a map with keys being rule priorities and their values neing all the rules of that priority found in the rule_sets
let mut message = format!("Found multiple rules of the same priority applicable to to expression: {:?} \n resulting in expression: {:?}", initial_expr, new_expr);
log::warn!("Multiple rules of different priorities are applicable to expression {:?} \n resulting in expression: {:?}