Grcov report - base.rs

1

use std::rc::Rc;

2

3

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

4

use conjure_core::metadata::Metadata;

5

use conjure_core::rule_engine::{

6

    register_rule, register_rule_set, ApplicationError, ApplicationResult, Reduction,

7

};

8

use uniplate::Uniplate;

9

10

use Atom::*;

11

use Expr::*;

12

use Lit::*;

13

14

use crate::ast::declaration::Declaration;

15

16

register_rule_set!("Base", ());

17

18

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

19

///

20

/// For example:

21

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

22

///

23

/// **Applicable examples:**

24

/// ```text

25

/// or([])  ~> false

26

/// X([]) ~> Nothing

27

/// ```

28

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

29

294865

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

30

    // excluded expressions

31

109208

    if matches!(

32

294865

        expr,

33

        Atomic(_, _)

34

            | Root(_, _)

35

            | FlatIneq(_, _, _, _)

36

            | FlatMinusEq(_, _, _)

37

            | FlatSumGeq(_, _, _)

38

            | FlatSumLeq(_, _, _)

39

            | FlatProductEq(_, _, _, _)

40

            | FlatWatchedLiteral(_, _, _)

41

            | FlatWeightedSumGeq(_, _, _, _)

42

            | FlatWeightedSumLeq(_, _, _, _)

43

            | MinionDivEqUndefZero(_, _, _, _)

44

            | MinionModuloEqUndefZero(_, _, _, _)

45

            | MinionPow(_, _, _, _)

46

            | MinionReify(_, _, _)

47

            | MinionReifyImply(_, _, _)

48

            | FlatAbsEq(_, _, _)

49

) {

50

185657

        return Err(ApplicationError::RuleNotApplicable);

51

109208

52

109208

53

109208

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

54

109208

        return Err(ApplicationError::RuleNotApplicable);

55

56

57

    let new_expr = match expr {

58

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

59

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

60

};

61

62

    Ok(Reduction::pure(new_expr))

63

294865

64

65

/**

66

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

67

 * ```text

68

1

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

69

1

 * ```

70

1

*/

71

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

72

224672

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

73

224672

    match expr {

74

102

        Min(_, exprs) => {

75

102

            let mut symbols = symbols.clone();

76

102

            let new_name = symbols.gensym();

77

102

78

102

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

79

102

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

80

306

            for e in exprs {

81

204

                new_top.push(Leq(

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

                disjunction.push(Eq(

87

204

                    Metadata::new(),

88

204

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

89

204

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

90

204

));

91

204

92

102

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

93

94

102

            let domain = expr

95

102

                .domain_of(&symbols)

96

102

                .ok_or(ApplicationError::DomainError)?;

97

102

            symbols.insert(Rc::new(Declaration::new_var(new_name.clone(), domain)));

98

102

99

102

            Ok(Reduction::new(

100

102

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

101

102

                new_top,

102

                symbols,

103

102

))

104

105

224570

        _ => Err(ApplicationError::RuleNotApplicable),

106

107

224672

108

109

/**

110

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

111

 * ```text

112

1

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

113

1

 * ```

114

1

*/

115

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

116

224672

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

117

224672

    match expr {

118

51

        Max(_, exprs) => {

119

51

            let mut symbols = symbols.clone();

120

51

            let new_name = symbols.gensym();

121

51

122

51

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

123

51

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

124

153

            for e in exprs {

125

102

                new_top.push(Geq(

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

                disjunction.push(Eq(

131

102

                    Metadata::new(),

132

102

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

133

102

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

134

102

));

135

102

136

51

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

137

138

51

            let domain = expr

139

51

                .domain_of(&symbols)

140

51

                .ok_or(ApplicationError::DomainError)?;

141

51

            symbols.insert(Rc::new(Declaration::new_var(new_name.clone(), domain)));

142

51

143

51

            Ok(Reduction::new(

144

51

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

145

51

                new_top,

146

51

                symbols,

147

51

))

148

149

224621

        _ => Err(ApplicationError::RuleNotApplicable),

150

151

224672