conjure_core/rules/normalisers/
neg_minus.rs

Help
1//! Normalising rules for negations and minus operations.
2//!
3//!
4//! ```text
5//! 1. --x ~> x  (eliminate_double_negation)
6//! 2. -( x + y ) ~> -x + -y (distribute_negation_over_addition)
7//! 3. x - b ~>  x + -b (minus_to_sum)
8//! 4. -(x*y) ~> -1 * x * y (simplify_negation_of_product
9//! ```
10//!
11//! ## Rationale for `x - y ~> x + -y`
12//!
13//! I normalise `Minus` expressions into sums of negations.
14//!
15//! Once all negations are in one sum expression, partial evaluation becomes easier, and we can do
16//! further normalisations like collecting like terms, removing nesting, and giving things an
17//! ordering.
18//!
19//! Converting to a sum is especially helpful for converting the model to Minion as:
20//!
21//! 1. normalise_associative_commutative concatenates nested sums, reducing the
22//!    amount of flattening we need to do to convert this to Minion (reducing the number of
23//!    auxiliary variables needed).
24//!
25//! 2. A sum of variables with constant coefficients can be trivially converted into the
26//!    weightedsumgeq and weightedsumleq constraints. A negated number is just a number
27//!    with a coefficient of -1.
28
29use conjure_core::ast::Expression as Expr;
30use conjure_core::rule_engine::{
31    register_rule, ApplicationError::RuleNotApplicable, ApplicationResult, Reduction,
32};
33use uniplate::{Biplate, Uniplate as _};
34use Expr::*;
35
36use crate::ast::{Atom, Literal as Lit, SymbolTable};
37use crate::matrix_expr;
38use crate::metadata::Metadata;
39use std::collections::VecDeque;
40
41/// Eliminates double negation
42///
43/// ```text
44/// --x ~> x
45/// ```
46#[register_rule(("Base", 8400))]
47fn elmininate_double_negation(expr: &Expr, _: &SymbolTable) -> ApplicationResult {
48    match expr {
49        Neg(_, a) if matches!(**a, Neg(_, _)) => Ok(Reduction::pure(a.children()[0].clone())),
50        _ => Err(RuleNotApplicable),
51    }
52}
53
54/// Distributes negation over sums
55///
56/// ```text
57/// -(x + y) ~> -x + -y
58/// ```
59#[register_rule(("Base", 8400))]
60fn distribute_negation_over_sum(expr: &Expr, _: &SymbolTable) -> ApplicationResult {
61    let inner_expr = match expr {
62        Neg(_, e) if matches!(**e, Sum(_, _)) => Ok(*e.clone()),
63        _ => Err(RuleNotApplicable),
64    }?;
65
66    let mut child_vecs: VecDeque<Vec<Expr>> = inner_expr.children_bi();
67
68    if child_vecs.is_empty() {
69        return Err(RuleNotApplicable);
70    }
71
72    for child in child_vecs[0].iter_mut() {
73        *child = Neg(Metadata::new(), Box::new(child.clone()))
74    }
75
76    Ok(Reduction::pure(inner_expr.with_children_bi(child_vecs)))
77}
78
79/// Simplifies the negation of a product
80///
81/// ```text
82/// -(x * y) ~> -1 * x * y
83/// ```
84#[register_rule(("Base", 8400))]
85fn simplify_negation_of_product(expr: &Expr, _: &SymbolTable) -> ApplicationResult {
86    let Expr::Neg(_, expr1) = expr.clone() else {
87        return Err(RuleNotApplicable);
88    };
89
90    let Expr::Product(_, mut factors) = *expr1 else {
91        return Err(RuleNotApplicable);
92    };
93
94    factors.push(Expr::Atomic(Metadata::new(), Atom::Literal(Lit::Int(-1))));
95
96    Ok(Reduction::pure(Expr::Product(Metadata::new(), factors)))
97}
98
99/// Converts a minus to a sum
100///
101/// ```text
102/// x - y ~> x + -y
103/// ```
104#[register_rule(("Base", 8400))]
105fn minus_to_sum(expr: &Expr, _: &SymbolTable) -> ApplicationResult {
106    let (lhs, rhs) = match expr {
107        Minus(_, lhs, rhs) => Ok((lhs.clone(), rhs.clone())),
108        _ => Err(RuleNotApplicable),
109    }?;
110
111    Ok(Reduction::pure(Sum(
112        Metadata::new(),
113        Box::new(matrix_expr![*lhs, Neg(Metadata::new(), rhs)]),
114    )))
115}
conjure_core/rules/normalisers/neg_minus.rs

conjure_core/rules/normalisers/
neg_minus.rs
