Grcov report - neg

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

29

use conjure_cp::essence_expr;

30

use conjure_cp::{

31

    ast::Metadata,

32

    ast::{Expression as Expr, Moo, ReturnType::Set, SymbolTable, Typeable},

33

    into_matrix_expr,

34

    rule_engine::{

35

        ApplicationError::RuleNotApplicable, ApplicationResult, Reduction, register_rule,

36

},

37

};

38

use std::collections::VecDeque;

39

use uniplate::{Biplate, Uniplate as _};

40

41

/// Eliminates double negation

42

///

43

/// ```text

44

/// --x ~> x

45

/// ```

46

#[register_rule(("Base", 8400))]

47

fn elmininate_double_negation(expr: &Expr, _: &SymbolTable) -> ApplicationResult {

48

    match expr {

49

        Expr::Neg(_, a) if matches!(**a, Expr::Neg(_, _)) => {

50

            let first_child: Expr = a.as_ref().children()[0].clone();

51

            Ok(Reduction::pure(first_child))

52

53

        _ => Err(RuleNotApplicable),

54

55

56

57

/// Distributes negation over sums

58

///

59

/// ```text

60

/// -(x + y) ~> -x + -y

61

/// ```

62

#[register_rule(("Base", 8400))]

63

fn distribute_negation_over_sum(expr: &Expr, _: &SymbolTable) -> ApplicationResult {

64

    let inner_expr = match expr {

65

        Expr::Neg(_, e) if matches!(**e, Expr::Sum(_, _)) => Ok(e),

66

        _ => Err(RuleNotApplicable),

67

}?;

68

69

    let mut child_vecs: VecDeque<Vec<Expr>> = inner_expr.children_bi();

70

71

    if child_vecs.is_empty() {

72

        return Err(RuleNotApplicable);

73

74

75

    for child in child_vecs[0].iter_mut() {

76

        *child = essence_expr!(-&child);

77

78

79

    Ok(Reduction::pure(Moo::unwrap_or_clone(

80

        inner_expr.with_children_bi(child_vecs),

81

)))

82

83

84

/// Simplifies the negation of a product

85

///

86

/// ```text

87

/// -(x * y) ~> -1 * x * y

88

/// ```

89

#[register_rule(("Base", 8400))]

90

fn simplify_negation_of_product(expr: &Expr, _: &SymbolTable) -> ApplicationResult {

91

    let Expr::Neg(_, expr1) = expr.clone() else {

92

        return Err(RuleNotApplicable);

93

};

94

95

    let Expr::Product(_, factors) = Moo::unwrap_or_clone(expr1) else {

96

        return Err(RuleNotApplicable);

97

};

98

99

    let mut factors = Moo::unwrap_or_clone(factors)

100

        .unwrap_list()

101

        .ok_or(RuleNotApplicable)?;

102

103

    factors.push(essence_expr!(-1));

104

105

    Ok(Reduction::pure(Expr::Product(

106

        Metadata::new(),

107

        Moo::new(into_matrix_expr!(factors)),

108

)))

109

110

111

/// Converts a minus to a sum

112

///

113

/// ```text

114

/// x - y ~> x + -y

115

/// ```

116

/// does not apply to sets.

117

/// TODO: need rule to define set difference as a special case of minus, comprehensions needed

118

/// return type and domain of minus need to be altered too, see expressions.rs

119

#[register_rule(("Base", 8400))]

120

fn minus_to_sum(expr: &Expr, _: &SymbolTable) -> ApplicationResult {

121

    let (lhs, rhs) = match expr {

122

        Expr::Minus(_, lhs, rhs) => {

123

            if matches!(lhs.as_ref().return_type(), Set(_)) {

124

                return Err(RuleNotApplicable);

125

126

            if matches!(rhs.as_ref().return_type(), Set(_)) {

127

                return Err(RuleNotApplicable);

128

129

            (lhs.clone(), rhs.clone())

130

131

        _ => return Err(RuleNotApplicable),

132

};

133

134

    Ok(Reduction::pure(essence_expr!(&lhs + (-&rhs))))

135