Lines
0 %
Functions
use core::panic;
use std::collections::HashMap;
use std::env;
use std::process::exit;
use conjure_core::rules::eval_constant;
use conjure_core::solver::SolverFamily;
use conjure_oxide::{
ast::*,
get_rule_by_name, get_rules,
rule_engine::{resolve_rule_sets, rewrite_model},
solver::{adaptors, Solver},
utils::testing::save_stats_json,
Metadata, Model, Rule,
};
use uniplate::Uniplate;
#[test]
fn rules_present() {
let rules = get_rules();
assert!(!rules.is_empty());
}
fn sum_of_constants() {
let valid_sum_expression = Expression::Sum(
Metadata::new(),
vec![
Expression::Constant(Metadata::new(), Constant::Int(1)),
Expression::Constant(Metadata::new(), Constant::Int(2)),
Expression::Constant(Metadata::new(), Constant::Int(3)),
],
);
let invalid_sum_expression = Expression::Sum(
Expression::Reference(Metadata::new(), 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(_metadata, 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(
Expression::Sum(
),
)),
Box::new(Expression::Constant(Metadata::new(), 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(Metadata::new(), expressions.clone()))
{
Expression::Constant(Metadata::new(), Constant::Int(result))
} else {
expressions.into_iter().map(simplify_expression).collect(),
)
Expression::Eq(_metadata, left, right) => Expression::Eq(
Box::new(simplify_expression(*left)),
Box::new(simplify_expression(*right)),
Expression::Geq(_metadata, 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(
expr = sum_constants
.apply(&expr, &Model::new_empty(Default::default()))
.unwrap()
.new_expression;
expr = unwrap_sum
assert_eq!(
expr,
Expression::Constant(Metadata::new(), Constant::Int(6))
fn rule_sum_mixed() {
]
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
Expression::SumGeq(
Box::new(Expression::Constant(Metadata::new(), Constant::Int(3)))
///
/// 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: {:?}", 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(
Expression::Constant(Metadata::new(), Constant::Int(-1)),
expr1 = sum_constants
.apply(&expr1, &Model::new_empty(Default::default()))
expr1 = unwrap_sum
expr1,
Expression::Constant(Metadata::new(), Constant::Int(4))
// a + b + c = 4
expr1 = Expression::Leq(
Expression::Reference(Metadata::new(), Name::UserName(String::from("b"))),
Expression::Reference(Metadata::new(), Name::UserName(String::from("c"))),
Box::new(expr1),
expr1 = sum_leq_to_sumleq
Expression::SumLeq(
Box::new(Expression::Constant(Metadata::new(), Constant::Int(4)))
// a < b
let mut expr2 = Expression::Lt(
Box::new(Expression::Reference(
Name::UserName(String::from("a")),
Name::UserName(String::from("b")),
expr2 = lt_to_ineq
.apply(&expr2, &Model::new_empty(Default::default()))
expr2,
Expression::Ineq(
Name::UserName(String::from("a"))
Name::UserName(String::from("b"))
Box::new(Expression::Constant(Metadata::new(), Constant::Int(-1)))
let mut model = Model::new(
HashMap::new(),
Expression::And(Metadata::new(), vec![expr1, expr2]),
Default::default(),
model.variables.insert(
DecisionVariable {
domain: Domain::IntDomain(vec![Range::Bounded(1, 3)]),
},
Name::UserName(String::from("c")),
let solver: Solver<adaptors::Minion> = Solver::new(adaptors::Minion::new());
let solver = solver.load_model(model).unwrap();
solver.solve(Box::new(|_| true)).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(Metadata::new(), Constant::Bool(true))),
expr = remove_double_negation
Expression::Constant(Metadata::new(), 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(
Expression::Or(
Expression::Constant(Metadata::new(), Constant::Bool(true)),
Expression::Constant(Metadata::new(), Constant::Bool(false)),
expr = unwrap_nested_or
fn rule_unwrap_nested_and() {
let unwrap_nested_and = get_rule_by_name("unwrap_nested_and").unwrap();
let mut expr = Expression::And(
Expression::And(
expr = unwrap_nested_and
fn unwrap_nested_or_not_changed() {
let expr = Expression::Or(
let result = unwrap_nested_or.apply(&expr, &Model::new_empty(Default::default()));
assert!(result.is_err());
fn unwrap_nested_and_not_changed() {
let expr = Expression::And(
let result = unwrap_nested_and.apply(&expr, &Model::new_empty(Default::default()));
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(Metadata::new(), Constant::Bool(true))],
let mut expr_or = Expression::Or(
vec![Expression::Constant(Metadata::new(), Constant::Bool(false))],
expr_and = remove_trivial_and
.apply(&expr_and, &Model::new_empty(Default::default()))
expr_or = remove_trivial_or
.apply(&expr_or, &Model::new_empty(Default::default()))
expr_and,
expr_or,
Expression::Constant(Metadata::new(), 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
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
fn remove_constants_from_or_not_changed() {
let result = remove_constants_from_or.apply(&expr, &Model::new_empty(Default::default()));
fn remove_constants_from_and_not_changed() {
let result = remove_constants_from_and.apply(&expr, &Model::new_empty(Default::default()));
fn rule_distribute_not_over_and() {
let distribute_not_over_and = get_rule_by_name("distribute_not_over_and").unwrap();
Box::new(Expression::And(
expr = distribute_not_over_and
Expression::Not(
))
fn rule_distribute_not_over_or() {
let distribute_not_over_or = get_rule_by_name("distribute_not_over_or").unwrap();
Box::new(Expression::Or(
expr = distribute_not_over_or
fn rule_distribute_not_over_and_not_changed() {
let expr = Expression::Not(
let result = distribute_not_over_and.apply(&expr, &Model::new_empty(Default::default()));
fn rule_distribute_not_over_or_not_changed() {
let result = distribute_not_over_or.apply(&expr, &Model::new_empty(Default::default()));
fn rule_distribute_or_over_and() {
let distribute_or_over_and = get_rule_by_name("distribute_or_over_and").unwrap();
Expression::Reference(Metadata::new(), Name::MachineName(1)),
Expression::Reference(Metadata::new(), Name::MachineName(2)),
Expression::Reference(Metadata::new(), Name::MachineName(3)),
let red = distribute_or_over_and
.unwrap();
red.new_expression,
// #[test]
// fn rule_ensure_div() {
// let ensure_div = get_rule_by_name("ensure_div").unwrap();
// let expr = Expression::Div(
// Metadata::new(),
// Box::new(Expression::Reference(
// Name::UserName("a".to_string()),
// )),
// Name::UserName("b".to_string()),
// );
// let red = ensure_div.apply(&expr, &Model::new_empty(Default::default())).unwrap();
// assert_eq!(
// red.new_expression,
// Expression::SafeDiv(
// Name::UserName("a".to_string())
// Name::UserName("b".to_string())
// ),
// red.new_top,
// Expression::Neq(
// Box::new(Expression::Constant(Metadata::new(), Constant::Int(0)))
// )
// }
/// 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() {
let rule_sets = match resolve_rule_sets(SolverFamily::Minion, &vec!["Constant".to_string()]) {
Ok(rs) => rs,
Err(e) => {
eprintln!("Error resolving rule sets: {}", e);
exit(1);
println!("Rule sets: {:?}", rule_sets);
// 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(
Expression::Eq(
Expression::Reference(Metadata::new(), variable_a.clone()),
Expression::Reference(Metadata::new(), variable_b.clone()),
Expression::Reference(Metadata::new(), variable_c.clone()),
Box::new(Expression::Constant(Metadata::new(), Constant::Int(4))),
Expression::Lt(
Box::new(Expression::Reference(Metadata::new(), variable_a.clone())),
Box::new(Expression::Reference(Metadata::new(), variable_b.clone())),
// Apply rewrite function to the nested expression
let rewritten_expr = rewrite_model(
&Model::new(HashMap::new(), nested_expr, Default::default()),
&rule_sets,
.constraints;
// 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::new(HashMap::new(), rewritten_expr, Default::default());
// Insert variables and domains
variable_a.clone(),
domain: domain.clone(),
variable_b.clone(),
variable_c.clone(),
fn rewrite_solve_xyz_parameterized() {
// Create variables and domain
// Create a vector of test cases with varying number of OR clauses
let test_cases = vec![1, 2, 3, 4];
for num_or_clauses in test_cases {
// Construct OR'd expression
let mut or_exprs = Vec::new();
for _i in 0..num_or_clauses {
or_exprs.push(expr);
let nested_expr = Expression::Or(Metadata::new(), or_exprs);
let model_for_rewrite = Model::new(HashMap::new(), nested_expr.clone(), Default::default());
let model_for_rewrite_unoptimized =
Model::new(HashMap::new(), nested_expr.clone(), Default::default());
let rewritten_expr = rewrite_model(&model_for_rewrite, &rule_sets)
env::set_var("OPTIMIZATIONS", "0");
let rewritten_expr_unoptimized = rewrite_model(&model_for_rewrite_unoptimized, &rule_sets)
env::remove_var("OPTIMIZATIONS");
let info_file_name_optimized = format!("rewrite_solve_xyz_optimized_{}", num_or_clauses);
let info_file_name_unoptimized =
format!("rewrite_solve_xyz_unoptimized_{}", num_or_clauses);
save_stats_json(
model_for_rewrite.context,
"tests",
&info_file_name_optimized,
.expect("Could not save stats!");
model_for_rewrite_unoptimized.context,
&info_file_name_unoptimized,
let expr_unoptimized = rewritten_expr_unoptimized.clone();
assert!(is_simple(&expr_unoptimized));
let mut model_unoptimized = Model::new(
rewritten_expr_unoptimized,
model_unoptimized.variables.insert(
let solver_unoptimized: Solver<adaptors::Minion> = Solver::new(adaptors::Minion::new());
let solver_unoptimized = solver_unoptimized.load_model(model_unoptimized).unwrap();
solver_unoptimized.solve(Box::new(|_| true)).unwrap();
struct RuleResult<'a> {
#[allow(dead_code)]
rule: &'a Rule<'a>,
new_expression: Expression,
/// # Returns
/// - True if `expression` is in its simplest form.
/// - False otherwise.
pub fn is_simple(expression: &Expression) -> bool {
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<&'a Rule<'a>>,
) -> Option<Expression> {
let rule_results = apply_all_rules(expression, rules);
if let Some(new) = choose_rewrite(&rule_results) {
return Some(new);
let mut sub = expression.children();
for i in 0..sub.len() {
if let Some(new) = is_simple_iteration(&sub[i], rules) {
sub[i] = new;
return Some(expression.with_children(sub.clone()));
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, &Model::new_empty(Default::default())) {
Ok(red) => {
results.push(RuleResult {
rule,
new_expression: red.new_expression,
});
Err(_) => continue,
results
/// - Some(<new_expression>) after applying the first rule in `results`.
/// - None if `results` is empty.
fn choose_rewrite(results: &[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(Metadata::new(), Constant::Int(1));
let result = eval_constant(&expr);
assert_eq!(result, Some(Constant::Int(1)));
fn eval_const_bool() {
let expr = Expression::Constant(Metadata::new(), 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(Metadata::new(), Name::UserName(String::from("a")));
assert_eq!(result, None);
fn eval_const_nested_ref() {
let expr = Expression::Sum(
fn eval_const_eq_int() {
let expr = Expression::Eq(
Box::new(Expression::Constant(Metadata::new(), Constant::Int(1))),
fn eval_const_eq_bool() {
fn eval_const_eq_mixed() {
fn eval_const_sum_mixed() {
fn eval_const_sum_xyz() {
Expression::Reference(Metadata::new(), Name::UserName(String::from("x"))),
Expression::Reference(Metadata::new(), Name::UserName(String::from("y"))),
Expression::Reference(Metadata::new(), Name::UserName(String::from("z"))),
Expression::Geq(
Name::UserName(String::from("x")),
Name::UserName(String::from("y")),
fn eval_const_or() {