Skip to content

Commit

Permalink
Merge branch 'main' into nd60/new-solver-interface
Browse files Browse the repository at this point in the history
  • Loading branch information
niklasdewally authored Feb 9, 2024
2 parents 4e32afd + b3036d7 commit efb93c8
Show file tree
Hide file tree
Showing 8 changed files with 402 additions and 2 deletions.
4 changes: 4 additions & 0 deletions Cargo.lock

Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.

2 changes: 2 additions & 0 deletions Cargo.toml
Original file line number Diff line number Diff line change
Expand Up @@ -7,6 +7,7 @@ default-members = [
"crates/conjure_rules",
"solvers/kissat",
"solvers/minion",
"crates/uniplate",
]

members = [
Expand All @@ -15,6 +16,7 @@ members = [
"crates/doc_solver_support",
"crates/conjure_rules_proc_macro",
"crates/conjure_rules",
"crates/uniplate",
"solvers/kissat",
"solvers/minion",
"solvers/chuffed",
Expand Down
13 changes: 13 additions & 0 deletions conjure_oxide/src/rewrite.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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();
Expand Down Expand Up @@ -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>>,
Expand All @@ -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;
Expand All @@ -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();

Expand Down
157 changes: 156 additions & 1 deletion conjure_oxide/tests/rewrite_tests.rs
Original file line number Diff line number Diff line change
@@ -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};

Expand Down Expand Up @@ -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())
}
13 changes: 13 additions & 0 deletions crates/uniplate/Cargo.toml
Original file line number Diff line number Diff line change
@@ -0,0 +1,13 @@
[package]
name = "uniplate"
version = "0.1.0"
edition = "2021"
description="Boilerplate-free generic operations on data, Haskell style."
license = "MPL-2.0"

# See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html

[dependencies]

[lints]
workspace = true
109 changes: 109 additions & 0 deletions crates/uniplate/src/lib.rs
Original file line number Diff line number Diff line change
@@ -0,0 +1,109 @@
//! A port of Haskell's [Uniplate](https://hackage.haskell.org/package/uniplate) in Rust.
//!
//!
//! # Examples
//!
//! ## A Calculator Input Language
//!
//! Consider the AST of a calculator input language:
//!
//! ```
//! pub enum AST {
//! Int(i32),
//! Add(Box<AST>,Box<AST>),
//! Sub(Box<AST>,Box<AST>),
//! Div(Box<AST>,Box<AST>),
//! Mul(Box<AST>,Box<AST>)
//! }
//!```
//!
//! Using uniplate, one can implement a single function for this AST that can be used in a whole
//! range of traversals.
//!
//! While this does not seem helpful in this toy example, the benefits amplify when the number of
//! enum variants increase, and the different types contained in their fields increase.
//!
//!
//! The below example implements [`Uniplate`](uniplate::Uniplate) for this language AST, and uses uniplate methods to
//! evaluate the encoded equation.
//!
//!```
//! use uniplate::uniplate::Uniplate;
//!
//! #[derive(Clone,Eq,PartialEq,Debug)]
//! pub enum AST {
//! Int(i32),
//! Add(Box<AST>,Box<AST>),
//! Sub(Box<AST>,Box<AST>),
//! Div(Box<AST>,Box<AST>),
//! Mul(Box<AST>,Box<AST>)
//! }
//!
//! // In the future would be automatically derived.
//! impl Uniplate for AST {
//! fn uniplate(&self) -> (Vec<AST>, Box<dyn Fn(Vec<AST>) -> AST +'_>) {
//! let context: Box<dyn Fn(Vec<AST>) -> AST> = match self {
//! AST::Int(i) => Box::new(|_| AST::Int(*i)),
//! AST::Add(_, _) => Box::new(|exprs: Vec<AST>| AST::Add(Box::new(exprs[0].clone()),Box::new(exprs[1].clone()))),
//! AST::Sub(_, _) => Box::new(|exprs: Vec<AST>| AST::Sub(Box::new(exprs[0].clone()),Box::new(exprs[1].clone()))),
//! AST::Div(_, _) => Box::new(|exprs: Vec<AST>| AST::Div(Box::new(exprs[0].clone()),Box::new(exprs[1].clone()))),
//! AST::Mul(_, _) => Box::new(|exprs: Vec<AST>| AST::Mul(Box::new(exprs[0].clone()),Box::new(exprs[1].clone())))
//! };
//!
//! let children: Vec<AST> = match self {
//! AST::Add(a,b) => vec![*a.clone(),*b.clone()],
//! AST::Sub(a,b) => vec![*a.clone(),*b.clone()],
//! AST::Div(a,b) => vec![*a.clone(),*b.clone()],
//! AST::Mul(a,b) => vec![*a.clone(),*b.clone()],
//! _ => vec![]
//! };
//!
//! (children,context)
//! }
//! }
//!
//! pub fn my_rule(e: AST) -> AST{
//! match e {
//! AST::Int(a) => AST::Int(a),
//! AST::Add(a,b) => {match (&*a,&*b) { (AST::Int(a), AST::Int(b)) => AST::Int(a+b), _ => AST::Add(a,b) }},
//! AST::Sub(a,b) => {match (&*a,&*b) { (AST::Int(a), AST::Int(b)) => AST::Int(a-b), _ => AST::Sub(a,b) }},
//! AST::Mul(a,b) => {match (&*a,&*b) { (AST::Int(a), AST::Int(b)) => AST::Int(a*b), _ => AST::Mul(a,b) }},
//! AST::Div(a,b) => {match (&*a,&*b) { (AST::Int(a), AST::Int(b)) => AST::Int(a/b), _ => AST::Div(a,b) }}
//! }
//! }
//! pub fn main() {
//! let mut ast = AST::Add(
//! Box::new(AST::Int(1)),
//! Box::new(AST::Mul(
//! Box::new(AST::Int(2)),
//! Box::new(AST::Div(
//! Box::new(AST::Add(Box::new(AST::Int(1)),Box::new(AST::Int(2)))),
//! Box::new(AST::Int(3))
//! )))));
//!
//! ast = ast.transform(my_rule);
//! println!("{:?}",ast);
//! assert_eq!(ast,AST::Int(3));
//! }
//! ```
//!
//! ....MORE DOCS TO COME....
//!
//! # Acknowledgements / Related Work
//!
//! *This crate implements programming constructs from the following Haskell libraries and
//! papers:*
//!
//! * [Uniplate](https://hackage.haskell.org/package/uniplate).
//!
//! * Neil Mitchell and Colin Runciman. 2007. Uniform boilerplate and list processing. In
//! Proceedings of the ACM SIGPLAN workshop on Haskell workshop (Haskell '07). Association for
//! Computing Machinery, New York, NY, USA, 49–60. <https://doi.org/10.1145/1291201.1291208>
//! [(free copy)](https://www.cs.york.ac.uk/plasma/publications/pdf/MitchellRuncimanHW07.pdf)
//!
//! * Huet G. The Zipper. Journal of Functional Programming. 1997;7(5):549–54. <https://doi.org/10.1017/S0956796897002864>
//! [(free copy)](https://www.cambridge.org/core/services/aop-cambridge-core/content/view/0C058890B8A9B588F26E6D68CF0CE204/S0956796897002864a.pdf/zipper.pdf)

//!

pub mod uniplate;
Loading

0 comments on commit efb93c8

Please sign in to comment.