conjure_core/rules/normalisers/
neg_minus.rs

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::metadata::Metadata;
38use std::collections::VecDeque;
39
40/// Eliminates double negation
41///
42/// ```text
43/// --x ~> x
44/// ```
45#[register_rule(("Base", 8400))]
46fn elmininate_double_negation(expr: &Expr, _: &SymbolTable) -> ApplicationResult {
47    match expr {
48        Neg(_, a) if matches!(**a, Neg(_, _)) => Ok(Reduction::pure(a.children()[0].clone())),
49        _ => Err(RuleNotApplicable),
50    }
51}
52
53/// Distributes negation over sums
54///
55/// ```text
56/// -(x + y) ~> -x + -y
57/// ```
58#[register_rule(("Base", 8400))]
59fn distribute_negation_over_sum(expr: &Expr, _: &SymbolTable) -> ApplicationResult {
60    let inner_expr = match expr {
61        Neg(_, e) if matches!(**e, Sum(_, _)) => Ok(*e.clone()),
62        _ => Err(RuleNotApplicable),
63    }?;
64
65    let mut child_vecs: VecDeque<Vec<Expr>> = inner_expr.children_bi();
66
67    if child_vecs.is_empty() {
68        return Err(RuleNotApplicable);
69    }
70
71    for child in child_vecs[0].iter_mut() {
72        *child = Neg(Metadata::new(), Box::new(child.clone()))
73    }
74
75    Ok(Reduction::pure(inner_expr.with_children_bi(child_vecs)))
76}
77
78/// Simplifies the negation of a product
79///
80/// ```text
81/// -(x * y) ~> -1 * x * y
82/// ```
83#[register_rule(("Base", 8400))]
84fn simplify_negation_of_product(expr: &Expr, _: &SymbolTable) -> ApplicationResult {
85    let Expr::Neg(_, expr1) = expr.clone() else {
86        return Err(RuleNotApplicable);
87    };
88
89    let Expr::Product(_, mut factors) = *expr1 else {
90        return Err(RuleNotApplicable);
91    };
92
93    factors.push(Expr::Atomic(Metadata::new(), Atom::Literal(Lit::Int(-1))));
94
95    Ok(Reduction::pure(Expr::Product(Metadata::new(), factors)))
96}
97
98/// Converts a minus to a sum
99///
100/// ```text
101/// x - y ~> x + -y
102/// ```
103#[register_rule(("Base", 8400))]
104fn minus_to_sum(expr: &Expr, _: &SymbolTable) -> ApplicationResult {
105    let (lhs, rhs) = match expr {
106        Minus(_, lhs, rhs) => Ok((lhs.clone(), rhs.clone())),
107        _ => Err(RuleNotApplicable),
108    }?;
109
110    Ok(Reduction::pure(Sum(
111        Metadata::new(),
112        vec![*lhs, Neg(Metadata::new(), rhs)],
113    )))
114}
conjure_core/rules/normalisers/neg_minus.rs

conjure_core/rules/normalisers/
neg_minus.rs
