Merge pull request conjure-cp#174 from gskorokhod/xyz-minion

Getting the XYZ problem working with Minion

conjure_oxide/src/lib.rs

@@ -1,7 +1,7 @@
 pub mod error;
 pub mod find_conjure;
 pub mod parse;
-mod rewrite;
+pub mod rewrite;
 mod rules;
 pub mod solvers;
 mod utils;

conjure_oxide/src/main.rs

@@ -1,23 +1,41 @@
 // (niklasdewally): temporary, gut this if you want!
 
 use anyhow::{anyhow, bail};
+use std::collections::HashMap;
+use std::ops::Deref;
 use std::path::PathBuf;
+use std::sync::Mutex;
 
 use anyhow::Result as AnyhowResult;
 use clap::{arg, command, Parser};
 use conjure_oxide::find_conjure::conjure_executable;
 use conjure_oxide::parse::model_from_json;
+use conjure_oxide::rewrite::rewrite_model;
+use conjure_oxide::solvers::FromConjureModel;
+use minion_rs::ast::{Constant, Model as MinionModel, VarName};
+use minion_rs::run_minion;
 
 #[derive(Parser)]
 #[command(author, version, about, long_about = None)]
 struct Cli {
     #[arg(long, value_name = "SOLVER")]
     solver: Option<String>,
 
-    #[arg(value_name = "INPUT_ESSENCE")]
+    #[arg(
+        value_name = "INPUT_ESSENCE",
+        default_value = "./conjure_oxide/tests/integration/xyz/input.essence"
+    )]
     input_file: PathBuf,
 }
 
+static ALL_SOLUTIONS: Mutex<Vec<HashMap<VarName, Constant>>> = Mutex::new(vec![]);
+
+fn callback(solutions: HashMap<VarName, Constant>) -> bool {
+    let mut guard = ALL_SOLUTIONS.lock().unwrap();
+    guard.push(solutions);
+    true
+}
+
 pub fn main() -> AnyhowResult<()> {
     println!(
         "Rules: {:?}",
@@ -53,8 +71,32 @@ pub fn main() -> AnyhowResult<()> {
 
     let astjson = String::from_utf8(output.stdout)?;
 
-    let model = model_from_json(&astjson)?;
+    let mut model = model_from_json(&astjson)?;
+
+    println!("Initial model:");
+    println!("{:?}", model);
+
+    println!("Rewriting model...");
+    model = rewrite_model(&model);
+
+    println!("\nRewritten model:");
     println!("{:?}", model);
 
+    println!("Building Minion model...");
+    let minion_model = MinionModel::from_conjure(model)?;
+
+    println!("Running Minion...");
+    let res = run_minion(minion_model, callback);
+    res.expect("Error occurred");
+
+    // Get solutions
+    let guard = ALL_SOLUTIONS.lock().unwrap();
+    guard.deref().iter().for_each(|solution_set| {
+        println!("Solution set:");
+        solution_set.iter().for_each(|(var, val)| {
+            println!("{}: {:?}", var, val);
+        });
+    });
+
     Ok(())
 }

conjure_oxide/src/parse.rs

@@ -35,7 +35,7 @@ pub fn model_from_json(str: &str) -> Result<Model> {
                     .iter()
                     .flat_map(parse_expression)
                     .collect();
-                m.constraints.extend(constraints);
+                m.add_constraints(constraints);
                 // println!("Nb constraints {}", m.constraints.len());
             }
             otherwise => panic!("Unhandled Statement {:#?}", otherwise),

conjure_oxide/src/rewrite.rs

@@ -1,4 +1,4 @@
-use conjure_core::ast::Expression;
+use conjure_core::ast::{Expression, Model};
 use conjure_core::rule::Rule;
 use conjure_rules::get_rules;
 
@@ -27,11 +27,15 @@ fn rewrite_iteration<'a>(
     if let Some(new) = choose_rewrite(&rule_results) {
         return Some(new);
     } else {
-        let mut sub = expression.sub_expressions();
-        for i in 0..sub.len() {
-            if let Some(new) = rewrite_iteration(sub[i], rules) {
-                sub[i] = &new;
-                return Some(expression.with_sub_expressions(sub));
+        match expression.sub_expressions() {
+            None => {}
+            Some(mut sub) => {
+                for i in 0..sub.len() {
+                    if let Some(new) = rewrite_iteration(sub[i], rules) {
+                        sub[i] = &new;
+                        return Some(expression.with_sub_expressions(sub));
+                    }
+                }
             }
         }
     }
@@ -62,5 +66,14 @@ fn choose_rewrite(results: &Vec<RuleResult>) -> Option<Expression> {
         return None;
     }
     // Return the first result for now
+    // println!("Applying rule: {:?}", results[0].rule);
     Some(results[0].new_expression.clone())
 }
+
+pub fn rewrite_model(model: &Model) -> Model {
+    let mut new_model = model.clone();
+
+    new_model.constraints = rewrite(&model.constraints);
+
+    new_model
+}

conjure_oxide/src/rules/base.rs

@@ -1,3 +1,4 @@
+use conjure_core::ast::Expression;
 use conjure_core::{ast::Expression as Expr, rule::RuleApplicationError};
 use conjure_rules::register_rule;
 
@@ -10,6 +11,94 @@ use conjure_rules::register_rule;
 //     Ok(expr.clone())
 // }
 
+/**
+ * Remove nothings from expressions:
+ * ```text
+ * and([a, nothing, b]) = and([a, b])
+ * sum([a, nothing, b]) = sum([a, b])
+ * sum_leq([a, nothing, b], c) = sum_leq([a, b], c)
+ * ...
+ * ```
+*/
+#[register_rule]
+fn remove_nothings(expr: &Expr) -> Result<Expr, RuleApplicationError> {
+    fn remove_nothings(exprs: Vec<&Expr>) -> Result<Vec<&Expr>, RuleApplicationError> {
+        let mut changed = false;
+        let mut new_exprs = Vec::new();
+
+        for e in exprs {
+            match e.clone() {
+                Expr::Nothing => {
+                    changed = true;
+                }
+                _ => new_exprs.push(e),
+            }
+        }
+
+        if changed {
+            Ok(new_exprs)
+        } else {
+            Err(RuleApplicationError::RuleNotApplicable)
+        }
+    }
+
+    match expr {
+        Expr::And(_) | Expr::Or(_) | Expression::Sum(_) => match expr.sub_expressions() {
+            None => Err(RuleApplicationError::RuleNotApplicable),
+            Some(sub) => {
+                let new_sub = remove_nothings(sub)?;
+                let new_expr = expr.with_sub_expressions(new_sub);
+                Ok(new_expr)
+            }
+        },
+        Expression::SumEq(_, _) | Expression::SumLeq(_, _) | Expression::SumGeq(_, _) => {
+            match expr.sub_expressions() {
+                None => Err(RuleApplicationError::RuleNotApplicable),
+                Some(sub) => {
+                    // Keep the last sub expression, which is the right hand side expression
+                    let new_rhs = sub[sub.len() - 1];
+
+                    // Remove all nothings from the left hand side expressions
+                    let mut new_sub_exprs = remove_nothings(sub[..sub.len() - 1].to_vec())?;
+
+                    // Add the right hand side expression back
+                    new_sub_exprs.push(new_rhs);
+
+                    let new_expr = expr.with_sub_expressions(new_sub_exprs);
+                    Ok(new_expr)
+                }
+            }
+        }
+        _ => Err(RuleApplicationError::RuleNotApplicable),
+    }
+}
+
+/**
+ * Remove empty expressions:
+ * ```text
+ * [] = Nothing
+ * ```
+ */
+#[register_rule]
+fn empty_to_nothing(expr: &Expr) -> Result<Expr, RuleApplicationError> {
+    match expr.sub_expressions() {
+        None => Err(RuleApplicationError::RuleNotApplicable),
+        Some(sub) => {
+            if sub.is_empty() {
+                Ok(Expr::Nothing)
+            } else {
+                Err(RuleApplicationError::RuleNotApplicable)
+            }
+        }
+    }
+}
+
+/**
+ * Evaluate sum of constants:
+ * ```text
+ * sum([1, 2, 3]) = 6
+ * ```
+ */
 #[register_rule]
 fn sum_constants(expr: &Expr) -> Result<Expr, RuleApplicationError> {
     match expr {
@@ -36,6 +125,12 @@ fn sum_constants(expr: &Expr) -> Result<Expr, RuleApplicationError> {
     }
 }
 
+/**
+ * Unwrap trivial sums:
+ * ```text
+ * sum([a]) = a
+ * ```
+ */
 #[register_rule]
 fn unwrap_sum(expr: &Expr) -> Result<Expr, RuleApplicationError> {
     match expr {
@@ -44,46 +139,38 @@ fn unwrap_sum(expr: &Expr) -> Result<Expr, RuleApplicationError> {
     }
 }
 
+/**
+ * Flatten nested sums:
+ * ```text
+ * sum(sum(a, b), c) = sum(a, b, c)
+ * ```
+ */
 #[register_rule]
-fn flatten_sum_geq(expr: &Expr) -> Result<Expr, RuleApplicationError> {
-    match expr {
-        Expr::Geq(a, b) => {
-            let exprs = match a.as_ref() {
-                Expr::Sum(exprs) => Ok(exprs),
-                _ => Err(RuleApplicationError::RuleNotApplicable),
-            }?;
-            Ok(Expr::SumGeq(exprs.clone(), b.clone()))
-        }
-        _ => Err(RuleApplicationError::RuleNotApplicable),
-    }
-}
-
-#[register_rule]
-fn sum_leq_to_sumleq(expr: &Expr) -> Result<Expr, RuleApplicationError> {
+pub fn flatten_nested_sum(expr: &Expr) -> Result<Expr, RuleApplicationError> {
     match expr {
-        Expr::Leq(a, b) => {
-            let exprs = match a.as_ref() {
-                Expr::Sum(exprs) => Ok(exprs),
-                _ => Err(RuleApplicationError::RuleNotApplicable),
-            }?;
-            Ok(Expr::SumLeq(exprs.clone(), b.clone()))
+        Expr::Sum(exprs) => {
+            let mut new_exprs = Vec::new();
+            let mut changed = false;
+            for e in exprs {
+                match e {
+                    Expr::Sum(sub_exprs) => {
+                        changed = true;
+                        for e in sub_exprs {
+                            new_exprs.push(e.clone());
+                        }
+                    }
+                    _ => new_exprs.push(e.clone()),
+                }
+            }
+            if !changed {
+                return Err(RuleApplicationError::RuleNotApplicable);
+            }
+            Ok(Expr::Sum(new_exprs))
         }
         _ => Err(RuleApplicationError::RuleNotApplicable),
     }
 }
 
-#[register_rule]
-fn lt_to_ineq(expr: &Expr) -> Result<Expr, RuleApplicationError> {
-    match expr {
-        Expr::Lt(a, b) => Ok(Expr::Ineq(
-            a.clone(),
-            b.clone(),
-            Box::new(Expr::ConstantInt(-1)),
-        )),
-        _ => Err(RuleApplicationError::RuleNotApplicable),
-    }
-}
-
 /**
 * Unwrap nested `or`