Grcov report - base.rs

1

use conjure_cp::essence_expr;

2

use conjure_cp::{

3

    ast::Metadata,

4

    ast::{Atom, Expression as Expr, Moo, SymbolTable},

5

    into_matrix_expr,

6

    rule_engine::{

7

        ApplicationError, ApplicationResult, Reduction, register_rule, register_rule_set,

8

},

9

};

10

use uniplate::Uniplate;

11

12

use ApplicationError::RuleNotApplicable;

13

14

register_rule_set!("Base", ());

15

16

/// This rule simplifies expressions where the operator is applied to an empty set of sub-expressions.

17

///

18

/// For example:

19

/// - `or([])` simplifies to `false` since no disjunction exists.

20

/// - `and([])` simplifies to `true` since no conjunction exists.

21

///

22

/// **Applicable examples:**

23

/// ```text

24

/// or([])  ~> false

25

/// X([]) ~> Nothing

26

/// ```

27

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

28

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

29

    // excluded expressions

30

    if matches!(

31

        expr,

32

        Expr::Atomic(_, _)

33

            | Expr::Root(_, _)

34

            | Expr::Comprehension(_, _)

35

            | Expr::FlatIneq(_, _, _, _)

36

            | Expr::FlatMinusEq(_, _, _)

37

            | Expr::FlatSumGeq(_, _, _)

38

            | Expr::FlatSumLeq(_, _, _)

39

            | Expr::FlatProductEq(_, _, _, _)

40

            | Expr::FlatWatchedLiteral(_, _, _)

41

            | Expr::FlatWeightedSumGeq(_, _, _, _)

42

            | Expr::FlatWeightedSumLeq(_, _, _, _)

43

            | Expr::MinionDivEqUndefZero(_, _, _, _)

44

            | Expr::MinionModuloEqUndefZero(_, _, _, _)

45

            | Expr::MinionWInIntervalSet(_, _, _)

46

            | Expr::MinionWInSet(_, _, _)

47

            | Expr::MinionElementOne(_, _, _, _)

48

            | Expr::MinionPow(_, _, _, _)

49

            | Expr::MinionReify(_, _, _)

50

            | Expr::MinionReifyImply(_, _, _)

51

            | Expr::FlatAbsEq(_, _, _)

52

            | Expr::Min(_, _)

53

            | Expr::Max(_, _)

54

            | Expr::AllDiff(_, _)

55

            | Expr::FlatAllDiff(_, _)

56

            | Expr::AbstractLiteral(_, _)

57

) {

58

        return Err(ApplicationError::RuleNotApplicable);

59

60

61

    if !expr.children().is_empty() {

62

        return Err(ApplicationError::RuleNotApplicable);

63

64

65

    let new_expr = match expr {

66

        Expr::Or(_, _) => essence_expr!(false),

67

        Expr::And(_, _) => essence_expr!(true),

68

        _ => {

69

            return Err(ApplicationError::RuleNotApplicable);

70

        } // _ => And(Metadata::new(), Box::new(matrix_expr![])),

71

};

72

73

    Ok(Reduction::pure(new_expr))

74

75

76

/**

77

 * Turn a Min into a new variable and post a top-level constraint to ensure the new variable is the minimum.

78

 * ```text

79

 * min([a, b]) ~> c ; c <= a & c <= b & (c = a | c = b)

80

 * ```

81

*/

82

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

83

fn min_to_var(expr: &Expr, symbols: &SymbolTable) -> ApplicationResult {

84

    let Expr::Min(_, inside_min_expr) = expr else {

85

        return Err(RuleNotApplicable);

86

};

87

88

    let Some(exprs) = inside_min_expr.as_ref().clone().unwrap_list() else {

89

        return Err(RuleNotApplicable);

90

};

91

92

    let domain = expr.domain_of().ok_or(ApplicationError::DomainError)?;

93

    let mut symbols = symbols.clone();

94

95

    let atom_inner = Atom::new_ref(symbols.gensym(&domain));

96

    let atom_expr = Expr::Atomic(Metadata::new(), atom_inner);

97

98

    let mut new_top = Vec::new();

99

    let mut disjunction = Vec::new();

100

    for e in exprs {

101

        // Use the Expr::Atomic version in constraints

102

        new_top.push(essence_expr!(&atom_expr <= &e));

103

        disjunction.push(essence_expr!(&atom_expr = &e));

104

105

    // TODO: deal with explicit index domains

106

    new_top.push(Expr::Or(

107

        Metadata::new(),

108

        Moo::new(into_matrix_expr![disjunction]),

109

));

110

111

    Ok(Reduction::new(

112

        // Return the Expr::Atomic

113

        essence_expr!(&atom_expr),

114

        new_top,

115

        symbols.clone(),

116

))

117

118

119

/**

120

 * Turn a Max into a new variable and post a top level constraint to ensure the new variable is the maximum.

121

 * ```text

122

 * max([a, b]) ~> c ; c >= a & c >= b & (c = a | c = b)

123

 * ```

124

*/

125

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

126

fn max_to_var(expr: &Expr, symbols: &SymbolTable) -> ApplicationResult {

127

    let Expr::Max(_, inside_max_expr) = expr else {

128

        return Err(RuleNotApplicable);

129

};

130

131

    let Some(exprs) = inside_max_expr.as_ref().clone().unwrap_list() else {

132

        return Err(RuleNotApplicable);

133

};

134

135

    let domain = expr.domain_of().ok_or(ApplicationError::DomainError)?;

136

    let mut symbols: SymbolTable = symbols.clone();

137

138

    let atom_inner = Atom::new_ref(symbols.gensym(&domain));

139

    let atom_expr = Expr::Atomic(Metadata::new(), atom_inner);

140

141

    let mut new_top = Vec::new(); // the new variable must be more than or equal to all the other variables

142

    let mut disjunction = Vec::new(); // the new variable must more than or equal to one of the variables

143

    for e in exprs {

144

        new_top.push(essence_expr!(&atom_expr >= &e));

145

        disjunction.push(essence_expr!(&atom_expr = &e));

146

147

    // FIXME: deal with explicitly given domains

148

    new_top.push(Expr::Or(

149

        Metadata::new(),

150

        Moo::new(into_matrix_expr![disjunction]),

151

));

152

153

    Ok(Reduction::new(essence_expr!(&atom_expr), new_top, symbols))

154