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, until no more rules can be applied.

Rules are applied in order of priority (from highest to lowest) Rules can:

• Apply transformations to the constraints in the model (or their sub-expressions)
• Add new constraints to the model
• Modify the symbol table (e.g. add new variables)

Parameters

• model: A reference to the Model to be rewritten.
• rule_sets: A vector of references to RuleSets to be applied.

Each RuleSet contains a map of rules to priorities.

Returns

• Ok(Model): If successful, it returns a modified copy of the Model
• Err(RewriteError): If an error occurs during rule application (e.g., invalid rules)

Side-Effects

• Rules can apply side-effects to the model (e.g. adding new constraints or variables). The original model is cloned and a modified copy is returned.
• Rule engine statistics (e.g. number of rule applications, run time) are collected and stored in the new model’s context.

Example

• Using rewrite_model with the constraint (a + min(x, y)) = b

  Original model:

  model: {
    constraints: [(a + min(x, y) + 42 - 10) = b],
    symbols: [a, b, x, y]
  }
  rule_sets: [{
      name: "MyRuleSet",
      rules: [
        min_to_var: 10,
        const_eval: 20
      ]
    }]

  Rules:

  • min_to_var: min([a, b]) ~> c ; c <= a & c <= b & (c = a / c = b)
  • const_eval: c1 + c2 ~> (c1 + c2) ; c1, c2 are constants

  Result:

  model: {
    constraints: [
      (a + aux + 32) = b,
      aux <= x,
      aux <= y,
      aux = x \/ aux = y
    ],
    symbols: [a, b, x, y, aux]
  }

  Process:

  1. We traverse the expression tree until a rule can be applied.
  2. If multiple rules can be applied to the same expression, the higher priority one goes first. In this case, const_eval is applied before min_to_var.
  3. The rule min_to_var adds a new variable aux and new constraints to the model.
  4. When no more rules can be applied, the resulting model is returned.

  Details for this process can be found in [rewrite_iteration] documentation.

Performance Considerations

• We recursively traverse the tree multiple times to check if any rules can be applied.
• Expressions are cloned on each rule application

This can be expensive for large models

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_rules: Resolves the rules from the provided rule sets and sorts them by priority.
• [rewrite_iteration]: Executes a single iteration of rewriting the model using the specified rules.