Lines
0 %
Functions
// Tests for rewriting/simplifying parts of the AST
use conjure_core::rule::Rule;
use conjure_rules::{get_rule_by_name, get_rules};
use core::panic;
use std::collections::HashMap;
use conjure_oxide::{ast::*, eval_constant, rewrite::rewrite, solvers::FromConjureModel};
use minion_rs::ast::{Constant as MinionConstant, VarName};
#[test]
fn rules_present() {
let rules = conjure_rules::get_rules();
assert!(!rules.is_empty());
}
fn sum_of_constants() {
let valid_sum_expression = Expression::Sum(vec![
Expression::Constant(Constant::Int(1)),
Expression::Constant(Constant::Int(2)),
Expression::Constant(Constant::Int(3)),
]);
let invalid_sum_expression = Expression::Sum(vec![
Expression::Reference(Name::UserName(String::from("a"))),
match evaluate_sum_of_constants(&valid_sum_expression) {
Some(result) => assert_eq!(result, 6),
None => panic!(),
if evaluate_sum_of_constants(&invalid_sum_expression).is_some() {
panic!()
fn evaluate_sum_of_constants(expr: &Expression) -> Option<i32> {
match expr {
Expression::Sum(expressions) => {
let mut sum = 0;
for e in expressions {
match e {
Expression::Constant(Constant::Int(value)) => {
sum += value;
_ => return None,
Some(sum)
_ => None,
fn recursive_sum_of_constants() {
let complex_expression = Expression::Eq(
Box::new(Expression::Sum(vec![
Expression::Sum(vec![
]),
])),
Box::new(Expression::Constant(Constant::Int(3))),
);
let correct_simplified_expression = Expression::Eq(
let simplified_expression = simplify_expression(complex_expression.clone());
assert_eq!(simplified_expression, correct_simplified_expression);
fn simplify_expression(expr: Expression) -> Expression {
if let Some(result) = evaluate_sum_of_constants(&Expression::Sum(expressions.clone())) {
Expression::Constant(Constant::Int(result))
} else {
Expression::Sum(expressions.into_iter().map(simplify_expression).collect())
Expression::Eq(left, right) => Expression::Eq(
Box::new(simplify_expression(*left)),
Box::new(simplify_expression(*right)),
),
Expression::Geq(left, right) => Expression::Geq(
_ => expr,
fn rule_sum_constants() {
let sum_constants = get_rule_by_name("sum_constants").unwrap();
let unwrap_sum = get_rule_by_name("unwrap_sum").unwrap();
let mut expr = Expression::Sum(vec![
expr = sum_constants.apply(&expr).unwrap();
expr = unwrap_sum.apply(&expr).unwrap();
assert_eq!(expr, Expression::Constant(Constant::Int(6)));
fn rule_sum_mixed() {
assert_eq!(
expr,
])
fn rule_sum_geq() {
let flatten_sum_geq = get_rule_by_name("flatten_sum_geq").unwrap();
let mut expr = Expression::Geq(
expr = flatten_sum_geq.apply(&expr).unwrap();
Expression::SumGeq(
vec![
],
Box::new(Expression::Constant(Constant::Int(3)))
)
fn callback(solution: HashMap<VarName, MinionConstant>) -> bool {
println!("Solution: {:?}", solution);
false
///
/// Reduce and solve:
/// ```text
/// find a,b,c : int(1..3)
/// such that a + b + c <= 2 + 3 - 1
/// such that a < b
/// ```
fn reduce_solve_xyz() {
println!("Rules: {:?}", conjure_rules::get_rules());
let lt_to_ineq = get_rule_by_name("lt_to_ineq").unwrap();
let sum_leq_to_sumleq = get_rule_by_name("sum_leq_to_sumleq").unwrap();
// 2 + 3 - 1
let mut expr1 = Expression::Sum(vec![
Expression::Constant(Constant::Int(-1)),
expr1 = sum_constants.apply(&expr1).unwrap();
expr1 = unwrap_sum.apply(&expr1).unwrap();
assert_eq!(expr1, Expression::Constant(Constant::Int(4)));
// a + b + c = 4
expr1 = Expression::Leq(
Expression::Reference(Name::UserName(String::from("b"))),
Expression::Reference(Name::UserName(String::from("c"))),
Box::new(expr1),
expr1 = sum_leq_to_sumleq.apply(&expr1).unwrap();
expr1,
Expression::SumLeq(
Box::new(Expression::Constant(Constant::Int(4)))
// a < b
let mut expr2 = Expression::Lt(
Box::new(Expression::Reference(Name::UserName(String::from("a")))),
Box::new(Expression::Reference(Name::UserName(String::from("b")))),
expr2 = lt_to_ineq.apply(&expr2).unwrap();
expr2,
Expression::Ineq(
Box::new(Expression::Constant(Constant::Int(-1)))
let mut model = Model {
variables: HashMap::new(),
constraints: Expression::And(vec![expr1, expr2]),
};
model.variables.insert(
Name::UserName(String::from("a")),
DecisionVariable {
domain: Domain::IntDomain(vec![Range::Bounded(1, 3)]),
},
Name::UserName(String::from("b")),
Name::UserName(String::from("c")),
let minion_model = conjure_oxide::solvers::minion::MinionModel::from_conjure(model).unwrap();
minion_rs::run_minion(minion_model, callback).unwrap();
fn rule_remove_double_negation() {
let remove_double_negation = get_rule_by_name("remove_double_negation").unwrap();
let mut expr = Expression::Not(Box::new(Expression::Not(Box::new(Expression::Constant(
Constant::Bool(true),
)))));
expr = remove_double_negation.apply(&expr).unwrap();
assert_eq!(expr, Expression::Constant(Constant::Bool(true)));
fn rule_unwrap_nested_or() {
let unwrap_nested_or = get_rule_by_name("unwrap_nested_or").unwrap();
let mut expr = Expression::Or(vec![
Expression::Or(vec![
Expression::Constant(Constant::Bool(true)),
Expression::Constant(Constant::Bool(false)),
expr = unwrap_nested_or.apply(&expr).unwrap();
fn rule_unwrap_nested_and() {
let unwrap_nested_and = get_rule_by_name("unwrap_nested_and").unwrap();
let mut expr = Expression::And(vec![
Expression::And(vec![
expr = unwrap_nested_and.apply(&expr).unwrap();
fn unwrap_nested_or_not_changed() {
let expr = Expression::Or(vec![
let result = unwrap_nested_or.apply(&expr);
assert!(result.is_err());
fn unwrap_nested_and_not_changed() {
let expr = Expression::And(vec![
let result = unwrap_nested_and.apply(&expr);
fn remove_trivial_and_or() {
let remove_trivial_and = get_rule_by_name("remove_trivial_and").unwrap();
let remove_trivial_or = get_rule_by_name("remove_trivial_or").unwrap();
let mut expr_and = Expression::And(vec![Expression::Constant(Constant::Bool(true))]);
let mut expr_or = Expression::Or(vec![Expression::Constant(Constant::Bool(false))]);
expr_and = remove_trivial_and.apply(&expr_and).unwrap();
expr_or = remove_trivial_or.apply(&expr_or).unwrap();
assert_eq!(expr_and, Expression::Constant(Constant::Bool(true)));
assert_eq!(expr_or, Expression::Constant(Constant::Bool(false)));
fn rule_remove_constants_from_or() {
let remove_constants_from_or = get_rule_by_name("remove_constants_from_or").unwrap();
expr = remove_constants_from_or.apply(&expr).unwrap();
fn rule_remove_constants_from_and() {
let remove_constants_from_and = get_rule_by_name("remove_constants_from_and").unwrap();
expr = remove_constants_from_and.apply(&expr).unwrap();
assert_eq!(expr, Expression::Constant(Constant::Bool(false)));
fn remove_constants_from_or_not_changed() {
let result = remove_constants_from_or.apply(&expr);
fn remove_constants_from_and_not_changed() {
let result = remove_constants_from_and.apply(&expr);
fn rule_distribute_not_over_and() {
let distribute_not_over_and = get_rule_by_name("distribute_not_over_and").unwrap();
let mut expr = Expression::Not(Box::new(Expression::And(vec![
])));
expr = distribute_not_over_and.apply(&expr).unwrap();
Expression::Not(Box::new(Expression::Reference(Name::UserName(
String::from("a")
)))),
String::from("b")
fn rule_distribute_not_over_or() {
let distribute_not_over_or = get_rule_by_name("distribute_not_over_or").unwrap();
let mut expr = Expression::Not(Box::new(Expression::Or(vec![
expr = distribute_not_over_or.apply(&expr).unwrap();
fn rule_distribute_not_over_and_not_changed() {
let expr = Expression::Not(Box::new(Expression::Reference(Name::UserName(
String::from("a"),
))));
let result = distribute_not_over_and.apply(&expr);
fn rule_distribute_not_over_or_not_changed() {
let result = distribute_not_over_or.apply(&expr);
fn rule_distribute_or_over_and() {
let distribute_or_over_and = get_rule_by_name("distribute_or_over_and").unwrap();
Expression::Reference(Name::MachineName(1)),
Expression::Reference(Name::MachineName(2)),
Expression::Reference(Name::MachineName(3)),
expr = distribute_or_over_and.apply(&expr).unwrap();
/// such that a + b + c = 4
/// This test uses the rewrite function to simplify the expression instead
/// of applying the rules manually.
fn rewrite_solve_xyz() {
// 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(
Expression::Reference(variable_a.clone()),
Expression::Reference(variable_b.clone()),
Expression::Reference(variable_c.clone()),
Box::new(Expression::Constant(Constant::Int(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
constraints: rewritten_expr,
// Insert variables and domains
variable_a.clone(),
domain: domain.clone(),
variable_b.clone(),
variable_c.clone(),
// Convert the model to MinionModel
// Run the solver with the rewritten model
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
/// - 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);
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
/// - A list of RuleResults after applying all rules to `expression`.
/// - An empty list if no rules are applicable.
fn apply_all_rules<'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
/// - 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())
fn eval_const_int() {
let expr = Expression::Constant(Constant::Int(1));
let result = eval_constant(&expr);
assert_eq!(result, Some(Constant::Int(1)));
fn eval_const_bool() {
let expr = Expression::Constant(Constant::Bool(true));
assert_eq!(result, Some(Constant::Bool(true)));
fn eval_const_and() {
assert_eq!(result, Some(Constant::Bool(false)));
fn eval_const_ref() {
let expr = Expression::Reference(Name::UserName(String::from("a")));
assert_eq!(result, None);
fn eval_const_nested_ref() {
let expr = Expression::Sum(vec![
fn eval_const_eq_int() {
let expr = Expression::Eq(
Box::new(Expression::Constant(Constant::Int(1))),
fn eval_const_eq_bool() {
Box::new(Expression::Constant(Constant::Bool(true))),
fn eval_const_eq_mixed() {
fn eval_const_sum_mixed() {
fn eval_const_sum_xyz() {
Expression::Reference(Name::UserName(String::from("x"))),
Expression::Reference(Name::UserName(String::from("y"))),
Expression::Reference(Name::UserName(String::from("z"))),
Expression::Geq(
Box::new(Expression::Reference(Name::UserName(String::from("x")))),
Box::new(Expression::Reference(Name::UserName(String::from("y")))),
fn eval_const_or() {