Merge pull request #179 from Kieranoski702/rewrite_test

Add test that checks if the write function can simplify the xyz problem

conjure_oxide/src/rewrite.rs

@@ -7,6 +7,9 @@ struct RuleResult<'a> {
     new_expression: Expression,
 }
 
+/// # Returns
+/// - A new expression after applying the rules to `expression` and its sub-expressions.
+/// - The same expression if no rules are applicable.
 pub fn rewrite(expression: &Expression) -> Expression {
     let rules = get_rules();
     let mut new = expression.clone();
@@ -42,6 +45,9 @@ fn rewrite_iteration<'a>(
     None // No rules applicable to this branch of the expression
 }
 
+/// # Returns
+/// - A list of RuleResults after applying all rules to `expression`.
+/// - An empty list if no rules are applicable.
 fn apply_all_rules<'a>(
     expression: &'a Expression,
     rules: &'a Vec<Rule<'a>>,
@@ -61,6 +67,9 @@ fn apply_all_rules<'a>(
     results
 }
 
+/// # Returns
+/// - Some(<new_expression>) after applying the first rule in `results`.
+/// - None if `results` is empty.
 fn choose_rewrite(results: &Vec<RuleResult>) -> Option<Expression> {
     if results.is_empty() {
         return None;
@@ -70,6 +79,10 @@ fn choose_rewrite(results: &Vec<RuleResult>) -> Option<Expression> {
     Some(results[0].new_expression.clone())
 }
 
+/// This rewrites the model by applying the rules to all constraints.
+/// # Returns
+/// - A new model with rewritten constraints.
+/// - The same model if no rules are applicable.
 pub fn rewrite_model(model: &Model) -> Model {
     let mut new_model = model.clone();
 

conjure_oxide/tests/rewrite_tests.rs

@@ -1,9 +1,11 @@
 // Tests for rewriting/simplifying parts of the AST
 
+use conjure_core::rule::Rule;
+use conjure_rules::get_rules;
 use core::panic;
 use std::collections::HashMap;
 
-use conjure_oxide::{ast::*, solvers::FromConjureModel};
+use conjure_oxide::{ast::*, rewrite::rewrite, solvers::FromConjureModel};
 use conjure_rules::get_rule_by_name;
 use minion_rs::ast::{Constant, VarName};
 
@@ -521,3 +523,156 @@ fn rule_distribute_or_over_and() {
         ]),
     );
 }
+
+///
+/// Reduce and solve:
+/// ```text
+/// find a,b,c : int(1..3)
+/// such that a + b + c = 4
+/// such that a < b
+/// ```
+///
+/// This test uses the rewrite function to simplify the expression instead
+/// of applying the rules manually.
+#[test]
+fn rewrite_solve_xyz() {
+    println!("Rules: {:?}", conjure_rules::get_rules());
+
+    // Create variables and domains
+    let variable_a = Name::UserName(String::from("a"));
+    let variable_b = Name::UserName(String::from("b"));
+    let variable_c = Name::UserName(String::from("c"));
+    let domain = Domain::IntDomain(vec![Range::Bounded(1, 3)]);
+
+    // Construct nested expression
+    let nested_expr = Expression::And(vec![
+        Expression::Eq(
+            Box::new(Expression::Sum(vec![
+                Expression::Reference(variable_a.clone()),
+                Expression::Reference(variable_b.clone()),
+                Expression::Reference(variable_c.clone()),
+            ])),
+            Box::new(Expression::ConstantInt(4)),
+        ),
+        Expression::Lt(
+            Box::new(Expression::Reference(variable_a.clone())),
+            Box::new(Expression::Reference(variable_b.clone())),
+        ),
+    ]);
+
+    // Apply rewrite function to the nested expression
+    let rewritten_expr = rewrite(&nested_expr);
+
+    // Check if the expression is in its simplest form
+    let expr = rewritten_expr.clone();
+    assert!(is_simple(&expr));
+
+    // Create model with variables and constraints
+    let mut model = Model {
+        variables: HashMap::new(),
+        constraints: rewritten_expr,
+    };
+
+    // Insert variables and domains
+    model.variables.insert(
+        variable_a.clone(),
+        DecisionVariable {
+            domain: domain.clone(),
+        },
+    );
+    model.variables.insert(
+        variable_b.clone(),
+        DecisionVariable {
+            domain: domain.clone(),
+        },
+    );
+    model.variables.insert(
+        variable_c.clone(),
+        DecisionVariable {
+            domain: domain.clone(),
+        },
+    );
+
+    // Convert the model to MinionModel
+    let minion_model = conjure_oxide::solvers::minion::MinionModel::from_conjure(model).unwrap();
+
+    // Run the solver with the rewritten model
+    minion_rs::run_minion(minion_model, callback).unwrap();
+}
+
+struct RuleResult<'a> {
+    rule: Rule<'a>,
+    new_expression: Expression,
+}
+
+/// # Returns
+/// - True if `expression` is in its simplest form.
+/// - False otherwise.
+pub fn is_simple(expression: &Expression) -> bool {
+    let rules = get_rules();
+    let mut new = expression.clone();
+    while let Some(step) = is_simple_iteration(&new, &rules) {
+        new = step;
+    }
+    new == *expression
+}
+
+/// # Returns
+/// - Some(<new_expression>) after applying the first applicable rule to `expr` or a sub-expression.
+/// - None if no rule is applicable to the expression or any sub-expression.
+fn is_simple_iteration<'a>(
+    expression: &'a Expression,
+    rules: &'a Vec<Rule<'a>>,
+) -> Option<Expression> {
+    let rule_results = apply_all_rules(expression, rules);
+    if let Some(new) = choose_rewrite(&rule_results) {
+        return Some(new);
+    } else {
+        match expression.sub_expressions() {
+            None => {}
+            Some(mut sub) => {
+                for i in 0..sub.len() {
+                    if let Some(new) = is_simple_iteration(sub[i], rules) {
+                        sub[i] = &new;
+                        return Some(expression.with_sub_expressions(sub));
+                    }
+                }
+            }
+        }
+    }
+    None // No rules applicable to this branch of the expression
+}
+
+/// # Returns
+/// - A list of RuleResults after applying all rules to `expression`.
+/// - An empty list if no rules are applicable.
+fn apply_all_rules<'a>(
+    expression: &'a Expression,
+    rules: &'a Vec<Rule<'a>>,
+) -> Vec<RuleResult<'a>> {
+    let mut results = Vec::new();
+    for rule in rules {
+        match rule.apply(expression) {
+            Ok(new) => {
+                results.push(RuleResult {
+                    rule: rule.clone(),
+                    new_expression: new,
+                });
+            }
+            Err(_) => continue,
+        }
+    }
+    results
+}
+
+/// # Returns
+/// - Some(<new_expression>) after applying the first rule in `results`.
+/// - None if `results` is empty.
+fn choose_rewrite(results: &Vec<RuleResult>) -> Option<Expression> {
+    if results.is_empty() {
+        return None;
+    }
+    // Return the first result for now
+    // println!("Applying rule: {:?}", results[0].rule);
+    Some(results[0].new_expression.clone())
+}