Grcov report - base.rs

1

use conjure_core::ast::{Atom, DecisionVariable, Expression as Expr, Literal as Lit, SymbolTable};

2

use conjure_core::metadata::Metadata;

3

use conjure_core::rule_engine::{

4

    register_rule, register_rule_set, ApplicationError, ApplicationResult, Reduction,

5

};

6

use conjure_core::Model;

7

use uniplate::Uniplate;

8

9

use Atom::*;

10

use Expr::*;

11

use Lit::*;

12

13

register_rule_set!("Base", 100, ());

14

15

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

16

///

17

/// For example:

18

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

19

///

20

/// **Applicable examples:**

21

/// ```text

22

/// or([])  ~> false

23

/// X([]) ~> Nothing

24

/// ```

25

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

26

286416

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

27

    // excluded expressions

28

107491

    if matches!(

29

286416

        expr,

30

        Atomic(_, _)

31

            | FlatIneq(_, _, _, _)

32

            | FlatMinusEq(_, _, _)

33

            | FlatSumGeq(_, _, _)

34

            | FlatSumLeq(_, _, _)

35

            | FlatProductEq(_, _, _, _)

36

            | FlatWatchedLiteral(_, _, _)

37

            | FlatWeightedSumGeq(_, _, _, _)

38

            | FlatWeightedSumLeq(_, _, _, _)

39

            | MinionDivEqUndefZero(_, _, _, _)

40

            | MinionModuloEqUndefZero(_, _, _, _)

41

            | MinionPow(_, _, _, _)

42

            | MinionReify(_, _, _)

43

            | MinionReifyImply(_, _, _)

44

            | FlatAbsEq(_, _, _)

45

) {

46

178925

        return Err(ApplicationError::RuleNotApplicable);

47

107491

48

107491

49

107491

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

50

107491

        return Err(ApplicationError::RuleNotApplicable);

51

52

53

    let new_expr = match expr {

54

        Or(_, _) => Atomic(Metadata::new(), Literal(Bool(false))),

55

        _ => And(Metadata::new(), vec![]), // TODO: (yb33) Change it to a simple vector after we refactor our model,

56

};

57

58

    Ok(Reduction::pure(new_expr))

59

286416

60

61

/**

62

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

63

 * ```text

64

1

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

65

1

 * ```

66

1

*/

67

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

68

217906

fn min_to_var(expr: &Expr, mdl: &Model) -> ApplicationResult {

69

217906

    match expr {

70

102

        Min(_, exprs) => {

71

102

            let new_name = mdl.gensym();

72

102

73

102

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

74

102

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

75

306

            for e in exprs {

76

204

                new_top.push(Leq(

77

204

                    Metadata::new(),

78

204

                    Box::new(Atomic(Metadata::new(), Reference(new_name.clone()))),

79

204

                    Box::new(e.clone()),

80

204

));

81

204

                disjunction.push(Eq(

82

204

                    Metadata::new(),

83

204

                    Box::new(Atomic(Metadata::new(), Reference(new_name.clone()))),

84

204

                    Box::new(e.clone()),

85

204

));

86

204

87

102

            new_top.push(Or(Metadata::new(), disjunction));

88

102

89

102

            let mut new_vars = SymbolTable::new();

90

102

            let domain = expr

91

102

                .domain_of(mdl.symbols())

92

102

                .ok_or(ApplicationError::DomainError)?;

93

102

            new_vars.add_var(new_name.clone(), DecisionVariable::new(domain));

94

102

95

102

            Ok(Reduction::new(

96

102

                Atomic(Metadata::new(), Reference(new_name)),

97

102

                new_top,

98

102

                new_vars,

99

102

))

100

101

217804

        _ => Err(ApplicationError::RuleNotApplicable),

102

103

217906

104

105

/**

106

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

107

 * ```text

108

1

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

109

1

 * ```

110

1

*/

111

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

112

217906

fn max_to_var(expr: &Expr, mdl: &Model) -> ApplicationResult {

113

217906

    match expr {

114

51

        Max(_, exprs) => {

115

51

            let new_name = mdl.gensym();

116

51

117

51

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

118

51

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

119

153

            for e in exprs {

120

102

                new_top.push(Geq(

121

102

                    Metadata::new(),

122

102

                    Box::new(Atomic(Metadata::new(), Reference(new_name.clone()))),

123

102

                    Box::new(e.clone()),

124

102

));

125

102

                disjunction.push(Eq(

126

102

                    Metadata::new(),

127

102

                    Box::new(Atomic(Metadata::new(), Reference(new_name.clone()))),

128

102

                    Box::new(e.clone()),

129

102

));

130

102

131

51

            new_top.push(Or(Metadata::new(), disjunction));

132

51

133

51

            let mut new_vars = SymbolTable::new();

134

51

            let domain = expr

135

51

                .domain_of(mdl.symbols())

136

51

                .ok_or(ApplicationError::DomainError)?;

137

51

            new_vars.add_var(new_name.clone(), DecisionVariable::new(domain));

138

51

139

51

            Ok(Reduction::new(

140

51

                Atomic(Metadata::new(), Reference(new_name)),

141

51

                new_top,

142

51

                new_vars,

143

51

))

144

145

217855

        _ => Err(ApplicationError::RuleNotApplicable),

146

147

217906