Lines
0 %
Functions
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::{Biplate, Uniplate};
fn var_name_from_atom(a: &Atom) -> Name {
<Atom as Biplate<Name>>::universe_bi(a)[0].clone()
}
#[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::Atomic(Metadata::new(), Atom::Literal(Literal::Int(1))),
Expression::Atomic(Metadata::new(), Atom::Literal(Literal::Int(2))),
Expression::Atomic(Metadata::new(), Atom::Literal(Literal::Int(3))),
],
);
let invalid_sum_expression = Expression::Sum(
Expression::Atomic(
Atom::Reference(Name::UserName(String::from("a"))),
),
assert_eq!(evaluate_sum_of_constants(&valid_sum_expression), Some(6));
assert_eq!(evaluate_sum_of_constants(&invalid_sum_expression), None);
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::Atomic(_, Atom::Literal(Literal::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::Atomic(
Atom::Literal(Literal::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::Atomic(Metadata::new(), Atom::Literal(Literal::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("partial_evaluator").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::Atomic(Metadata::new(), Atom::Literal(Literal::Int(6)))
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(
Atom::Literal(Literal::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::Atomic(Metadata::new(), Atom::Literal(Literal::Int(-1))),
expr1 = sum_constants
.apply(&expr1, &Model::new_empty(Default::default()))
expr1 = unwrap_sum
expr1,
Expression::Atomic(Metadata::new(), Atom::Literal(Literal::Int(4)))
// a + b + c = 4
expr1 = Expression::Leq(
Atom::Reference(Name::UserName(String::from("b"))),
Atom::Reference(Name::UserName(String::from("c"))),
Box::new(expr1),
expr1 = sum_leq_to_sumleq
Expression::SumLeq(
Atom::Reference(Name::UserName(String::from("a")))
Atom::Reference(Name::UserName(String::from("b")))
Atom::Reference(Name::UserName(String::from("c")))
Atom::Literal(Literal::Int(4))
// a < b
let mut expr2 = Expression::Lt(
expr2 = lt_to_ineq
.apply(&expr2, &Model::new_empty(Default::default()))
expr2,
Expression::Ineq(
Atom::Literal(Literal::Int(-1))
let mut model = Model::new(HashMap::new(), vec![expr1, expr2], Default::default());
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 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(
Atom::Literal(Literal::Bool(true)),
expr = remove_double_negation
Expression::Atomic(Metadata::new(), Atom::Literal(Literal::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::Atomic(Metadata::new(), Atom::Literal(Literal::Bool(true))),
Expression::Atomic(Metadata::new(), Atom::Literal(Literal::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::Atomic(
)],
let mut expr_or = Expression::Or(
Atom::Literal(Literal::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::Atomic(Metadata::new(), Atom::Literal(Literal::Bool(false)))
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::Atomic(Metadata::new(), Atom::Reference(Name::MachineName(1))),
Expression::Atomic(Metadata::new(), Atom::Reference(Name::MachineName(2))),
Expression::Atomic(Metadata::new(), Atom::Reference(Name::MachineName(3))),
let red = distribute_or_over_and
.unwrap();
red.new_expression,
/// 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 = Atom::Reference(Name::UserName(String::from("a")));
let variable_b = Atom::Reference(Name::UserName(String::from("b")));
let variable_c = Atom::Reference(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::Atomic(Metadata::new(), variable_a.clone()),
Expression::Atomic(Metadata::new(), variable_b.clone()),
Expression::Atomic(Metadata::new(), variable_c.clone()),
Atom::Literal(Literal::Int(4)),
Expression::Lt(
Box::new(Expression::Atomic(Metadata::new(), variable_a.clone())),
Box::new(Expression::Atomic(Metadata::new(), variable_b.clone())),
// Apply rewrite function to the nested expression
let rewritten_expr = rewrite_model(
&Model::new(HashMap::new(), vec![nested_expr], Default::default()),
&rule_sets,
.constraints;
// Check if the expression is in its simplest form
assert!(rewritten_expr.iter().all(|expr| is_simple(expr)));
// Create model with variables and constraints
let mut model = Model::new(HashMap::new(), rewritten_expr, Default::default());
// Insert variables and domains
var_name_from_atom(&variable_a.clone()),
domain: domain.clone(),
var_name_from_atom(&variable_b.clone()),
var_name_from_atom(&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(),
vec![nested_expr.clone()],
Default::default(),
let model_for_rewrite_unoptimized = Model::new(
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,
assert!(rewritten_expr_unoptimized
.iter()
.all(|expr| is_simple(expr)));
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::Atomic(Metadata::new(), Atom::Literal(Literal::Int(1)));
let result = eval_constant(&expr);
assert_eq!(result, Some(Literal::Int(1)));
fn eval_const_bool() {
let expr = Expression::Atomic(Metadata::new(), Atom::Literal(Literal::Bool(true)));
assert_eq!(result, Some(Literal::Bool(true)));
fn eval_const_and() {
assert_eq!(result, Some(Literal::Bool(false)));
fn eval_const_ref() {
let expr = Expression::Atomic(
assert_eq!(result, None);
fn eval_const_nested_ref() {
let expr = Expression::Sum(
fn eval_const_eq_int() {
let expr = Expression::Eq(
Atom::Literal(Literal::Int(1)),
fn eval_const_eq_bool() {
fn eval_const_eq_mixed() {
fn eval_const_sum_mixed() {
fn eval_const_sum_xyz() {
Atom::Reference(Name::UserName(String::from("x"))),
Atom::Reference(Name::UserName(String::from("y"))),
Atom::Reference(Name::UserName(String::from("z"))),
Expression::Geq(
fn eval_const_or() {