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 crate::shared::utils::{single_vec_child, with_single_vec_child};

30

use conjure_cp::essence_expr;

31

use conjure_cp::{

32

    ast::Metadata,

33

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

34

    into_matrix_expr,

35

    rule_engine::{

36

        ApplicationError::RuleNotApplicable, ApplicationResult, RuleEffect, register_rule,

37

},

38

};

39

40

/// Eliminates double negation

41

///

42

/// ```text

43

/// --x ~> x

44

/// ```

45

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

46

19779

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

47

19779

    match expr {

48

15710

        Expr::Neg(_, a) => match a.as_ref() {

49

42

            Expr::Neg(_, inner) => Ok(RuleEffect::pure(Moo::unwrap_or_clone(inner.clone()))),

50

15668

            _ => Err(RuleNotApplicable),

51

},

52

4069

        _ => Err(RuleNotApplicable),

53

54

19779

55

56

/// Distributes negation over sums

57

///

58

/// ```text

59

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

60

/// ```

61

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

62

19779

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

63

19779

    let inner_expr = match expr {

64

15710

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

65

19758

        _ => Err(RuleNotApplicable),

66

19758

}?;

67

68

21

    let mut children = single_vec_child(inner_expr.as_ref()).ok_or(RuleNotApplicable)?;

69

21

    for child in children.iter_mut() {

70

63

        *child = essence_expr!(-&child);

71

72

73

21

    Ok(RuleEffect::pure(with_single_vec_child(

74

21

        inner_expr.as_ref(),

75

21

        children,

76

21

)))

77

19779

78

79

/// Simplifies the negation of a product

80

///

81

/// ```text

82

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

83

/// ```

84

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

85

19779

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

86

19779

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

87

4069

        return Err(RuleNotApplicable);

88

};

89

90

15710

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

91

14597

        return Err(RuleNotApplicable);

92

};

93

94

1113

    let mut factors = Moo::unwrap_or_clone(factors)

95

1113

        .into_list()

96

1113

        .ok_or(RuleNotApplicable)?;

97

98

1113

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

99

100

1113

    Ok(RuleEffect::pure(Expr::Product(

101

1113

        Metadata::new(),

102

1113

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

103

1113

)))

104

19779

105

106

/// Converts a minus to a sum

107

///

108

/// ```text

109

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

110

/// ```

111

/// does not apply to sets.

112

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

113

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

114

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

115

15653

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

116

15653

    let (lhs, rhs) = match expr {

117

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

118

11584

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

119

                return Err(RuleNotApplicable);

120

11584

121

11584

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

122

                return Err(RuleNotApplicable);

123

11584

124

11584

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

125

126

4069

        _ => return Err(RuleNotApplicable),

127

};

128

129

11584

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

130

15653