Lines
0 %
Functions
use conjure_core::{ast::Constant as Const, ast::Expression as Expr, rule::RuleApplicationError};
use conjure_rules::register_rule;
/*****************************************************************************/
/* This file contains basic rules for simplifying expressions */
/**
* 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(_) | Expr::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)
},
Expr::SumEq(_, _) | Expr::SumLeq(_, _) | Expr::SumGeq(_, _) => {
match expr.sub_expressions() {
// 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);
_ => Err(RuleApplicationError::RuleNotApplicable),
* Remove empty expressions:
* [] = Nothing
fn empty_to_nothing(expr: &Expr) -> Result<Expr, RuleApplicationError> {
if sub.is_empty() {
Ok(Expr::Nothing)
* Evaluate sum of constants:
* sum([1, 2, 3]) = 6
fn sum_constants(expr: &Expr) -> Result<Expr, RuleApplicationError> {
Expr::Sum(exprs) => {
let mut sum = 0;
match e {
Expr::Constant(Const::Int(i)) => {
sum += i;
_ => new_exprs.push(e.clone()),
if !changed {
return Err(RuleApplicationError::RuleNotApplicable);
new_exprs.push(Expr::Constant(Const::Int(sum)));
Ok(Expr::Sum(new_exprs)) // Let other rules handle only one Expr being contained in the sum
* Unwrap trivial sums:
* sum([a]) = a
fn unwrap_sum(expr: &Expr) -> Result<Expr, RuleApplicationError> {
Expr::Sum(exprs) if (exprs.len() == 1) => Ok(exprs[0].clone()),
* Flatten nested sums:
* sum(sum(a, b), c) = sum(a, b, c)
pub fn flatten_nested_sum(expr: &Expr) -> Result<Expr, RuleApplicationError> {
Expr::Sum(sub_exprs) => {
for e in sub_exprs {
new_exprs.push(e.clone());
Ok(Expr::Sum(new_exprs))
* Unwrap nested `or`
* or(or(a, b), c) = or(a, b, c)
fn unwrap_nested_or(expr: &Expr) -> Result<Expr, RuleApplicationError> {
Expr::Or(exprs) => {
Ok(Expr::Or(new_exprs))
* Unwrap nested `and`
* and(and(a, b), c) = and(a, b, c)
fn unwrap_nested_and(expr: &Expr) -> Result<Expr, RuleApplicationError> {
Expr::And(exprs) => {
Ok(Expr::And(new_exprs))
* Remove double negation:
* not(not(a)) = a
fn remove_double_negation(expr: &Expr) -> Result<Expr, RuleApplicationError> {
Expr::Not(contents) => match contents.as_ref() {
Expr::Not(expr_box) => Ok(*expr_box.clone()),
* Remove trivial `and` (only one element):
* and([a]) = a
fn remove_trivial_and(expr: &Expr) -> Result<Expr, RuleApplicationError> {
if exprs.len() == 1 {
return Ok(exprs[0].clone());
* Remove trivial `or` (only one element):
* or([a]) = a
fn remove_trivial_or(expr: &Expr) -> Result<Expr, RuleApplicationError> {
* Remove constant bools from or expressions
* or([true, a]) = true
* or([false, a]) = a
fn remove_constants_from_or(expr: &Expr) -> Result<Expr, RuleApplicationError> {
Expr::Constant(Const::Bool(val)) => {
if *val {
// If we find a true, the whole expression is true
return Ok(Expr::Constant(Const::Bool(true)));
// If we find a false, we can ignore it
* Remove constant bools from and expressions
* and([true, a]) = a
* and([false, a]) = false
fn remove_constants_from_and(expr: &Expr) -> Result<Expr, RuleApplicationError> {
if !*val {
// If we find a false, the whole expression is false
return Ok(Expr::Constant(Const::Bool(false)));
// If we find a true, we can ignore it
* Evaluate Not expressions with constant bools
* not(true) = false
* not(false) = true
fn evaluate_constant_not(expr: &Expr) -> Result<Expr, RuleApplicationError> {
Expr::Constant(Const::Bool(val)) => Ok(Expr::Constant(Const::Bool(!val))),